c201192 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Bring erasure info to the case tree builder.

commitc201192844fd6397b4c918dec5856b73eb29120c authorMatus Tejiscak <ziman@functor.sk> dateFri 4 Jul 2014, 17:22 (12 years ago) parentd8ed044

7 files changed+26−22

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+2−2 src/Idris/Core/CaseTree.hs+4−4 src/Idris/Core/Evaluate.hs+10−9 src/Idris/Coverage.hs+2−1 src/Idris/ElabDecls.hs+5−4 src/Idris/Parser.hs+1−1 src/Idris/Prover.hs+2−1

src/Idris/AbsSyntaxTree.hs+2−2

@@ -1733,8 +1733,8 @@ usedNamesIn vars ist tm = nub $ ni [] tm

17331733 niTacImp _ _ = []

17341734

17351735-- Return the list of unused positions for a name.

1736−getInaccessibleArgs :: IState -> Name -> [Int]

1737−getInaccessibleArgs ist n =

1736+getErasureInfo :: IState -> Name -> [Int]

1737+getErasureInfo ist n =

17381738 case lookupCtxtExact n (idris_optimisation ist) of

17391739 Just (Optimise inacc detagg) -> map fst inacc

17401740 Nothing -> []

src/Idris/Core/CaseTree.hs+4−4

@@ -1,6 +1,6 @@

11{-# LANGUAGE PatternGuards, DeriveFunctor, TypeSynonymInstances #-}

3−module Idris.Core.CaseTree(CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..),

3+module Idris.Core.CaseTree(CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..), ErasureInfo,

44 Phase(..), CaseTree,

55 simpleCase, small, namesUsed, findCalls, findUsedArgs,

66 substSC, substAlt, mkForce) where

@@ -229,8 +229,9 @@ data Phase = CompileTime | RunTime

229229simpleCase :: Bool -> Bool -> Bool ->

230230 Phase -> FC -> [Int] -> [Type] ->

231231 [([Name], Term, Term)] ->

232+ ErasureInfo ->

232233 TC CaseDef

233−simpleCase tc cover reflect phase fc inacc argtys cs

234+simpleCase tc cover reflect phase fc inacc argtys cs erInfo

234235 = sc' tc cover phase fc (filter (\(_, _, r) ->

235236 case r of

236237 Impossible -> False

@@ -249,8 +250,7 @@ simpleCase tc cover reflect phase fc inacc argtys cs

249250 let numargs = length (fst (head pats))

250251 ns = take numargs args

251252 (ns', ps') = order [(n, i `elem` inacc) | (i,n) <- zip [0..] ns] pats

252− (tree, st) = runCaseBuilder

253− undefined -- TODO

253+ (tree, st) = runCaseBuilder erInfo

254254 (match ns' ps' (defaultCase cover))

255255 ([], numargs, [])

256256 t = CaseDef ns (prune proj (depatt ns' tree)) (fstT st) in

src/Idris/Core/Evaluate.hs+10−9

@@ -788,7 +788,8 @@ addDatatype (Data n tag ty cons) uctxt

788788 (TyDecl (DCon tag (arity ty')) ty, Public, Unchecked, EmptyMI) ctxt)

789789

790790-- FIXME: Too many arguments! Refactor all these Bools.

791−addCasedef :: Name -> CaseInfo -> Bool -> Bool -> Bool -> Bool ->

791+addCasedef :: Name -> ErasureInfo -> CaseInfo ->

792+ Bool -> Bool -> Bool -> Bool ->

792793 [Type] -> -- argument types

793794 [Int] -> -- inaccessible arguments

794795 [Either Term (Term, Term)] ->

@@ -797,17 +798,17 @@ addCasedef :: Name -> CaseInfo -> Bool -> Bool -> Bool -> Bool ->

797798 [([Name], Term, Term)] -> -- inlined

798799 [([Name], Term, Term)] -> -- run time

799800 Type -> Context -> Context

800−addCasedef n ci@(CaseInfo alwaysInline tcdict)

801+addCasedef n ei ci@(CaseInfo alwaysInline tcdict)

801802 tcase covering reflect asserted argtys inacc

802803 ps_in ps_tot ps_inl ps_ct ps_rt ty uctxt

803804 = let ctxt = definitions uctxt

804805 access = case lookupDefAcc n False uctxt of

805806 [(_, acc)] -> acc

806807 _ -> Public

807− ctxt' = case (simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_tot,

808− simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_ct,

809− simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_inl,

810− simpleCase tcase covering reflect RunTime emptyFC inacc argtys ps_rt) of

808+ ctxt' = case (simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_tot ei,

809+ simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_ct ei,

810+ simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_inl ei,

811+ simpleCase tcase covering reflect RunTime emptyFC inacc argtys ps_rt ei) of

811812 (OK (CaseDef args_tot sc_tot _),

812813 OK (CaseDef args_ct sc_ct _),

813814 OK (CaseDef args_inl sc_inl _),

@@ -825,8 +826,8 @@ addCasedef n ci@(CaseInfo alwaysInline tcdict)

825826 uctxt { definitions = ctxt' }

826827

827828-- simplify a definition for totality checking

828−simplifyCasedef :: Name -> Context -> Context

829−simplifyCasedef n uctxt

829+simplifyCasedef :: Name -> ErasureInfo -> Context -> Context

830+simplifyCasedef n ei uctxt

830831 = let ctxt = definitions uctxt

831832 ctxt' = case lookupCtxt n ctxt of

832833 [(CaseOp ci ty atys [] ps _, acc, tot, metainf)] ->

@@ -834,7 +835,7 @@ simplifyCasedef n uctxt

834835 [(CaseOp ci ty atys ps_in ps cd, acc, tot, metainf)] ->

835836 let ps_in' = map simpl ps_in

836837 pdef = map debind ps_in' in

837− case simpleCase False True False CompileTime emptyFC [] atys pdef of

838+ case simpleCase False True False CompileTime emptyFC [] atys pdef ei of

838839 OK (CaseDef args sc _) ->

839840 addDef n (CaseOp ci

840841 ty atys ps_in' ps (cd { cases_totcheck = (args, sc) }),

src/Idris/Coverage.hs+2−1

@@ -376,7 +376,8 @@ checkTotality path fc n

376376 | n `elem` path = return (Partial (Mutual (n : path)))

377377 | otherwise = do

378378 t <- getTotality n

379− updateContext (simplifyCasedef n)

379+ i <- getIState

380+ updateContext (simplifyCasedef n $ getErasureInfo i)

380381 ctxt <- getContext

381382 i <- getIState

382383 let opts = case lookupCtxt n (idris_flags i) of

src/Idris/ElabDecls.hs+5−4

@@ -1083,8 +1083,9 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

10831083 Just _ -> logLvl 5 $ "Partially evaluated:\n" ++ show pats

10841084 _ -> return ()

10851085

1086+ erInfo <- getErasureInfo <$> getIState

10861087 tree@(CaseDef scargs sc _) <- tclift $

1087− simpleCase tcase False reflect CompileTime fc inacc atys pdef

1088+ simpleCase tcase False reflect CompileTime fc inacc atys pdef erInfo

10881089 cov <- coverage

10891090 pmissing <-

10901091 if cov && not (hasDefault cs)

@@ -1133,7 +1134,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

11331134 let knowncovering = (pcover && cov) || AssertTotal `elem` opts

11341135

11351136 tree' <- tclift $ simpleCase tcase knowncovering reflect

1136− RunTime fc inacc atys pdef'

1137+ RunTime fc inacc atys pdef' erInfo

11371138 logLvl 3 $ "Unoptimised " ++ show n ++ ": " ++ show tree

11381139 logLvl 3 $ "Optimised: " ++ show tree'

11391140 ctxt <- getContext

@@ -1143,7 +1144,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

11431144 (idris_patdefs ist) })

11441145 let caseInfo = CaseInfo (inlinable opts) (dictionary opts)

11451146 case lookupTy n ctxt of

1146− [ty] -> do updateContext (addCasedef n caseInfo

1147+ [ty] -> do updateContext (addCasedef n erInfo caseInfo

11471148 tcase knowncovering

11481149 reflect

11491150 (AssertTotal `elem` opts)

@@ -2360,7 +2361,7 @@ elabDecl' what info (PMutual f ps)

23602361 -- Do totality checking after entire mutual block

23612362 i <- get

23622363 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n

2363− updateContext (simplifyCasedef n))

2364+ updateContext (simplifyCasedef n $ getErasureInfo i))

23642365 (map snd (idris_totcheck i))

23652366 mapM_ buildSCG (idris_totcheck i)

23662367 mapM_ checkDeclTotality (idris_totcheck i)

src/Idris/Parser.hs+1−1

@@ -1282,7 +1282,7 @@ loadSource h lidr f toline

12821282 -- simplify every definition do give the totality checker

12831283 -- a better chance

12841284 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n

1285− updateContext (simplifyCasedef n))

1285+ updateContext (simplifyCasedef n $ getErasureInfo i))

12861286 (map snd (idris_totcheck i))

12871287 -- build size change graph from simplified definitions

12881288 iLOG "Totality checking"

src/Idris/Prover.hs+2−1

@@ -78,7 +78,8 @@ prove opt ctxt lit n ty

7878 OK _ -> return ()

7979 Error e -> ierror (CantUnify False ty pty e [] 0)

8080 ptm' <- applyOpts ptm

81− updateContext (addCasedef n (CaseInfo True False) False False True False

81+ ei <- getErasureInfo `fmap` getIState

82+ updateContext (addCasedef n ei (CaseInfo True False) False False True False

8283 [] [] -- argtys, inaccArgs

8384 [Right (P Ref n ty, ptm)]

8485 [([], P Ref n ty, ptm)]