20627e4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Better strategy for building case trees at compile time

commit20627e445947a1ebefaf6d256a41c09da9d5cfd7 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 29 Nov 2012, 14:57 (14 years ago) parent0136305

3 files changed+14−8

compare with master

unifiedsplit

src/Core/CaseTree.hs+4−2 src/Idris/Coverage.hs+7−5 src/Idris/ElabDecls.hs+3−1

src/Core/CaseTree.hs+4−2

@@ -156,7 +156,7 @@ data Phase = CompileTime | RunTime

156156 deriving (Show, Eq)

157157

158158-- Generate a simple case tree

159−-- Work Left to Right at Compile Time

159+-- Work Right to Left

160160

161161simpleCase :: Bool -> Bool -> Phase -> FC -> [([Name], Term, Term)] ->

162162 TC CaseDef

@@ -190,7 +190,9 @@ simpleCase tc cover phase fc cs

190190 acc (PCon _ _ ps : xs) n = acc (ps ++ xs) n

191191 acc (_ : xs) n = acc xs n

192192

193−rev CompileTime = id

193+-- right to left gives more chance of discriminating on interesting arguments

194+-- rather than indices which are likely to be repeated.

195+-- rev CompileTime = id

194196rev _ = reverse

195197

196198data Pat = PCon Name Int [Pat]

src/Idris/Coverage.hs+7−5

@@ -383,6 +383,7 @@ checkDeclTotality :: (FC, Name) -> Idris Totality

383383checkDeclTotality (fc, n)

384384 = do logLvl 2 $ "Checking " ++ show n ++ " for totality"

385385 buildSCG (fc, n)

386+ logLvl 2 $ "Built SCG"

386387 checkTotality [] fc n

387388

388389-- Calculate the size change graph for this definition

@@ -411,8 +412,9 @@ buildSCG (_, n) = do

411412 x -> error $ "buildSCG: " ++ show (n, x)

412413

413414buildSCG' :: IState -> SC -> [Name] -> [SCGEntry]

414−buildSCG' ist sc args = nub $ scg sc (zip args args)

415− (zip args (zip args (repeat Same)))

415+buildSCG' ist sc args = -- trace ("Building SCG for " ++ show sc) $

416+ nub $ scg sc (zip args args)

417+ (zip args (zip args (repeat Same)))

416418 where

417419 scg :: SC -> [(Name, Name)] -> -- local var, originating top level var

418420 [(Name, (Name, SizeChange))] -> -- orig to new, and relationship

@@ -448,7 +450,7 @@ buildSCG' ist sc args = nub $ scg sc (zip args args)

448450 = let arel = argRels n

449451 szs' = zipWith (\arg (_,t) -> (arg, (x, t))) args arel

450452 ++ szs

451− vars' = zip args (repeat tvar) ++ vars in

453+ vars' = nub (zip args (repeat tvar) ++ vars) in

452454 scg sc vars' szs'

453455 | otherwise = scg sc vars szs

454456 scgAlt x vars szs (ConstCase _ sc) = scg sc vars szs

@@ -461,13 +463,13 @@ buildSCG' ist sc args = nub $ scg sc (zip args args)

461463 = let rest = concatMap (\x -> scgTerm x vars szs) args in

462464 case lookup fn vars of

463465 Just _ -> rest

464− Nothing -> (fn, map (mkChange szs) args) : rest

466+ Nothing -> nub $ (fn, map (mkChange szs) args) : rest

465467 scgTerm (App f a) vars szs

466468 = scgTerm f vars szs ++ scgTerm a vars szs

467469 scgTerm (Bind n (Let t v) e) vars szs

468470 = scgTerm v vars szs ++ scgTerm e vars szs

469471 scgTerm (Bind n _ e) vars szs

470− = scgTerm e ((n, n) : vars) szs

472+ = scgTerm e (nub ((n, n) : vars)) szs

471473 scgTerm (P _ fn _) vars szs

472474 = case lookup fn vars of

473475 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

363363 return missing'

364364 else return []

365365 let pcover = null pmissing

366+ logLvl 2 $ "Optimising patterns"

366367 pdef' <- applyOpts optpdef

367− logLvl 5 $ "Optimised patterns:\n" ++ show pdef'

368+ logLvl 2 $ "Optimised patterns"

369+ logLvl 5 $ show pdef'

368370 ist <- get

369371 -- let wf = wellFounded ist n sc

370372 let tot = if pcover || AssertTotal `elem` opts