d47e95b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Remove some redundancy in case trees

Sometimes the algorithm leaves branches which are impossible to reach, especially when there's lots of overlapping cases, so look out for these and delete them. This can make coverage checking and compilation times significantly better when the case trees are complicated.

commitd47e95bf47a36d2f0df038cb509cb13b03c8b43f authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 10 Dec 2017, 15:00 (9 years ago) parent664253c

2 files changed+53−2

compare with master

unifiedsplit

src/IRTS/CodegenC.hs+1−1 src/Idris/Core/CaseTree.hs+52−1

src/IRTS/CodegenC.hs+1−1

@@ -221,7 +221,7 @@ bcc i (PROJECT l loc a) = indent i ++ "PROJECT(vm, " ++ creg l ++ ", " ++ show l

221221bcc i (PROJECTINTO r t idx)

222222 = indent i ++ creg r ++ " = GETARG(" ++ creg t ++ ", " ++ show idx ++ ");\n"

223223bcc 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

225225 where

226226 showCode :: Int -> [BC] -> String

227227 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

279279 (tree, st) = runCaseBuilder erInfo

280280 (match ns' ps' defcase)

281281 ([], 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

283284 if proj then return (stripLambdas t)

284285 else return t

285286 Error err -> Error (At fc err)

@@ -765,6 +766,56 @@ prune proj (Case up n alts) = case alts' of

765766

766767prune _ t = t

767768

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+

768819stripLambdas :: CaseDef -> CaseDef

769820stripLambdas (CaseDef ns (STerm (Bind x (Lam _ _) sc)) tm)

770821 = stripLambdas (CaseDef (ns ++ [x]) (STerm (instantiate (P Bound x Erased) sc)) tm)