git.iko.soy/Idris-dev
on master help sign in
Remove some redundancy in case trees
d47e95bEdwin Brady
src/IRTS/CodegenC.hs+1−1
compare with master
unifiedsplit
@@ -221,7 +221,7 @@ bcc i (PROJECT l loc a) = indent i ++ "PROJECT(vm, " ++ creg l ++ ", " ++ show l
221bcc i (PROJECTINTO r t idx)
221bcc i (PROJECTINTO r t idx)
222 = indent i ++ creg r ++ " = GETARG(" ++ creg t ++ ", " ++ show idx ++ ");\n"
222 = indent i ++ creg r ++ " = GETARG(" ++ creg t ++ ", " ++ show idx ++ ");\n"
223bcc i (CASE True r code def)
223bcc i (CASE True r code def)
224− | length code < 4 = showCase i def code
224+ | length code < 4 && length code > 0 = showCase i def code
225 where
225 where
226 showCode :: Int -> [BC] -> String
226 showCode :: Int -> [BC] -> String
227 showCode i bc = "{\n" ++ concatMap (bcc (i + 1)) bc ++
227 showCode i bc = "{\n" ++ concatMap (bcc (i + 1)) bc ++
src/Idris/Core/CaseTree.hs+52−1
@@ -279,7 +279,8 @@ simpleCase tc defcase reflect phase fc inacc argtys cs erInfo
279 (tree, st) = runCaseBuilder erInfo
279 (tree, st) = runCaseBuilder erInfo
280 (match ns' ps' defcase)
280 (match ns' ps' defcase)
281 ([], numargs, [])
281 ([], numargs, [])
282− t = CaseDef ns (prune proj (depatt ns' tree)) (fstT st) in
282+ sc = removeUnreachable (prune proj (depatt ns' tree))
283+ t = CaseDef ns sc (fstT st) in
283 if proj then return (stripLambdas t)
284 if proj then return (stripLambdas t)
284 else return t
285 else return t
285 Error err -> Error (At fc err)
286 Error err -> Error (At fc err)
@@ -765,6 +766,56 @@ prune proj (Case up n alts) = case alts' of
765
766
766prune _ t = t
767prune _ t = t
767
768
769+-- Remove any branches we can't reach because of variables we've already
770+-- tested
771+removeUnreachable :: SC -> SC
772+removeUnreachable sc = ru [] sc
773+ where
774+ -- keep a mapping from variable names, to the constructor tag we've
775+ -- already checked it as in this branch
776+ ru :: [(Name, Int)] -> SC -> SC
777+ ru checked (Case t n alts)
778+ = let alts' = map (ruAlt checked n) (dropImpossible (lookup n checked) alts) in
779+ Case t n alts'
780+ ru checked t = t
781+
782+ dropImpossible Nothing alts = alts
783+ dropImpossible (Just t) [] = []
784+ dropImpossible (Just t) (ConCase con tag args sc : rest)
785+ | t == tag = [ConCase con tag args sc] -- must be this case
786+ | otherwise = dropImpossible (Just t) rest -- can't be this case
787+ dropImpossible (Just t) (c : rest)
788+ = c : dropImpossible (Just t) rest
789+
790+ ruAlt :: [(Name, Int)] -> Name -> CaseAlt -> CaseAlt
791+ ruAlt checked var (ConCase con tag args sc)
792+ = let checked' = dropChecked args (updateChecked var tag checked)
793+ sc' = ru checked' sc in
794+ ConCase con tag args sc'
795+ ruAlt checked var (FnCase n args sc)
796+ = let checked' = dropChecked [var] checked
797+ sc' = ru checked' sc in
798+ FnCase n args sc'
799+ ruAlt checked var (ConstCase c sc)
800+ = let checked' = dropChecked [var] checked
801+ sc' = ru checked' sc in
802+ ConstCase c sc'
803+ ruAlt checked var (SucCase n sc)
804+ = let checked' = dropChecked [var] checked
805+ sc' = ru checked' sc in
806+ SucCase n sc'
807+ ruAlt checked var (DefaultCase sc)
808+ = let checked' = dropChecked [var] checked
809+ sc' = ru checked' sc in
810+ DefaultCase sc'
811+
812+ updateChecked :: Name -> Int -> [(Name, Int)] -> [(Name, Int)]
813+ updateChecked n i checked
814+ = (n, i) : filter (\x -> fst x /= n) checked
815+
816+ dropChecked :: [Name] -> [(Name, Int)] -> [(Name, Int)]
817+ dropChecked ns checked = filter (\x -> fst x `notElem` ns) checked
818+
768stripLambdas :: CaseDef -> CaseDef
819stripLambdas :: CaseDef -> CaseDef
769stripLambdas (CaseDef ns (STerm (Bind x (Lam _ _) sc)) tm)
820stripLambdas (CaseDef ns (STerm (Bind x (Lam _ _) sc)) tm)
770 = stripLambdas (CaseDef (ns ++ [x]) (STerm (instantiate (P Bound x Erased) sc)) tm)
821 = stripLambdas (CaseDef (ns ++ [x]) (STerm (instantiate (P Bound x Erased) sc)) tm)