git.iko.soy/Idris-dev
on master help sign in
Better strategy for building case trees at compile time
20627e4Edwin Brady
src/Core/CaseTree.hs+4−2
compare with master
unifiedsplit
@@ -156,7 +156,7 @@ data Phase = CompileTime | RunTime
156 deriving (Show, Eq)
156 deriving (Show, Eq)
157
157
158-- Generate a simple case tree
158-- Generate a simple case tree
159−-- Work Left to Right at Compile Time
159+-- Work Right to Left
160
160
161simpleCase :: Bool -> Bool -> Phase -> FC -> [([Name], Term, Term)] ->
161simpleCase :: Bool -> Bool -> Phase -> FC -> [([Name], Term, Term)] ->
162 TC CaseDef
162 TC CaseDef
@@ -190,7 +190,9 @@ simpleCase tc cover phase fc cs
190 acc (PCon _ _ ps : xs) n = acc (ps ++ xs) n
190 acc (PCon _ _ ps : xs) n = acc (ps ++ xs) n
191 acc (_ : xs) n = acc xs n
191 acc (_ : xs) n = acc xs n
192
192
193+-- right to left gives more chance of discriminating on interesting arguments
194+-- rather than indices which are likely to be repeated.
193−rev CompileTime = id
195+-- rev CompileTime = id
194rev _ = reverse
196rev _ = reverse
195
197
196data Pat = PCon Name Int [Pat]
198data Pat = PCon Name Int [Pat]
src/Idris/Coverage.hs+7−5
@@ -383,6 +383,7 @@ checkDeclTotality :: (FC, Name) -> Idris Totality
383checkDeclTotality (fc, n)
383checkDeclTotality (fc, n)
384 = do logLvl 2 $ "Checking " ++ show n ++ " for totality"
384 = do logLvl 2 $ "Checking " ++ show n ++ " for totality"
385 buildSCG (fc, n)
385 buildSCG (fc, n)
386+ logLvl 2 $ "Built SCG"
386 checkTotality [] fc n
387 checkTotality [] fc n
387
388
388-- Calculate the size change graph for this definition
389-- Calculate the size change graph for this definition
@@ -411,8 +412,9 @@ buildSCG (_, n) = do
411 x -> error $ "buildSCG: " ++ show (n, x)
412 x -> error $ "buildSCG: " ++ show (n, x)
412
413
413buildSCG' :: IState -> SC -> [Name] -> [SCGEntry]
414buildSCG' :: IState -> SC -> [Name] -> [SCGEntry]
415+buildSCG' ist sc args = -- trace ("Building SCG for " ++ show sc) $
414−buildSCG' ist sc args = nub $ scg sc (zip args args)
416+ nub $ scg sc (zip args args)
415− (zip args (zip args (repeat Same)))
417+ (zip args (zip args (repeat Same)))
416 where
418 where
417 scg :: SC -> [(Name, Name)] -> -- local var, originating top level var
419 scg :: SC -> [(Name, Name)] -> -- local var, originating top level var
418 [(Name, (Name, SizeChange))] -> -- orig to new, and relationship
420 [(Name, (Name, SizeChange))] -> -- orig to new, and relationship
@@ -448,7 +450,7 @@ buildSCG' ist sc args = nub $ scg sc (zip args args)
448 = let arel = argRels n
450 = let arel = argRels n
449 szs' = zipWith (\arg (_,t) -> (arg, (x, t))) args arel
451 szs' = zipWith (\arg (_,t) -> (arg, (x, t))) args arel
450 ++ szs
452 ++ szs
451− vars' = zip args (repeat tvar) ++ vars in
453+ vars' = nub (zip args (repeat tvar) ++ vars) in
452 scg sc vars' szs'
454 scg sc vars' szs'
453 | otherwise = scg sc vars szs
455 | otherwise = scg sc vars szs
454 scgAlt x vars szs (ConstCase _ sc) = scg sc vars szs
456 scgAlt x vars szs (ConstCase _ sc) = scg sc vars szs
@@ -461,13 +463,13 @@ buildSCG' ist sc args = nub $ scg sc (zip args args)
461 = let rest = concatMap (\x -> scgTerm x vars szs) args in
463 = let rest = concatMap (\x -> scgTerm x vars szs) args in
462 case lookup fn vars of
464 case lookup fn vars of
463 Just _ -> rest
465 Just _ -> rest
464− Nothing -> (fn, map (mkChange szs) args) : rest
466+ Nothing -> nub $ (fn, map (mkChange szs) args) : rest
465 scgTerm (App f a) vars szs
467 scgTerm (App f a) vars szs
466 = scgTerm f vars szs ++ scgTerm a vars szs
468 = scgTerm f vars szs ++ scgTerm a vars szs
467 scgTerm (Bind n (Let t v) e) vars szs
469 scgTerm (Bind n (Let t v) e) vars szs
468 = scgTerm v vars szs ++ scgTerm e vars szs
470 = scgTerm v vars szs ++ scgTerm e vars szs
469 scgTerm (Bind n _ e) vars szs
471 scgTerm (Bind n _ e) vars szs
470− = scgTerm e ((n, n) : vars) szs
472+ = scgTerm e (nub ((n, n) : vars)) szs
471 scgTerm (P _ fn _) vars szs
473 scgTerm (P _ fn _) vars szs
472 = case lookup fn vars of
474 = case lookup fn vars of
473 Just _ -> []
475 Just _ -> []
src/Idris/ElabDecls.hs+3−1
@@ -363,8 +363,10 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
363 return missing'
363 return missing'
364 else return []
364 else return []
365 let pcover = null pmissing
365 let pcover = null pmissing
366+ logLvl 2 $ "Optimising patterns"
366 pdef' <- applyOpts optpdef
367 pdef' <- applyOpts optpdef
367− logLvl 5 $ "Optimised patterns:\n" ++ show pdef'
368+ logLvl 2 $ "Optimised patterns"
369+ logLvl 5 $ show pdef'
368 ist <- get
370 ist <- get
369 -- let wf = wellFounded ist n sc
371 -- let wf = wellFounded ist n sc
370 let tot = if pcover || AssertTotal `elem` opts
372 let tot = if pcover || AssertTotal `elem` opts