c201192 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Bring erasure info to the case tree builder.

c201192Matus Tejiscak12 years ago

src/Idris/AbsSyntaxTree.hs+2−2

compare with master

unifiedsplit

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

1733 niTacImp _ _ = []

1734

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

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

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

1737−getInaccessibleArgs ist n =

1737+getErasureInfo ist n =

1738 case lookupCtxtExact n (idris_optimisation ist) of

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

1740 Nothing -> []

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

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

1{-# 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,

4 Phase(..), CaseTree,

5 simpleCase, small, namesUsed, findCalls, findUsedArgs,

6 substSC, substAlt, mkForce) where

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

229simpleCase :: Bool -> Bool -> Bool ->

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

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

232+ ErasureInfo ->

232 TC CaseDef

233 TC CaseDef

233−simpleCase tc cover reflect phase fc inacc argtys cs

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

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

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

235 case r of

236 case r of

236 Impossible -> False

237 Impossible -> False

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

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

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

250 ns = take numargs args

251 ns = take numargs args

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

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

252− (tree, st) = runCaseBuilder

253+ (tree, st) = runCaseBuilder erInfo

253− undefined -- TODO

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

255 ([], numargs, [])

256 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

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

789

790-- 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 ->

792 [Type] -> -- argument types

793 [Type] -> -- argument types

793 [Int] -> -- inaccessible arguments

794 [Int] -> -- inaccessible arguments

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

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

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

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

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

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

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

799 Type -> Context -> Context

800 Type -> Context -> Context

800−addCasedef n ci@(CaseInfo alwaysInline tcdict)

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

801 tcase covering reflect asserted argtys inacc

802 tcase covering reflect asserted argtys inacc

802 ps_in ps_tot ps_inl ps_ct ps_rt ty uctxt

803 ps_in ps_tot ps_inl ps_ct ps_rt ty uctxt

803 = let ctxt = definitions uctxt

804 = let ctxt = definitions uctxt

804 access = case lookupDefAcc n False uctxt of

805 access = case lookupDefAcc n False uctxt of

805 [(_, acc)] -> acc

806 [(_, acc)] -> acc

806 _ -> Public

807 _ -> Public

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

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

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

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

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

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

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

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

811 (OK (CaseDef args_tot sc_tot _),

812 (OK (CaseDef args_tot sc_tot _),

812 OK (CaseDef args_ct sc_ct _),

813 OK (CaseDef args_ct sc_ct _),

813 OK (CaseDef args_inl sc_inl _),

814 OK (CaseDef args_inl sc_inl _),

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

825 uctxt { definitions = ctxt' }

826 uctxt { definitions = ctxt' }

826

827

827-- simplify a definition for totality checking

828-- simplify a definition for totality checking

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

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

829−simplifyCasedef n uctxt

830+simplifyCasedef n ei uctxt

830 = let ctxt = definitions uctxt

831 = let ctxt = definitions uctxt

831 ctxt' = case lookupCtxt n ctxt of

832 ctxt' = case lookupCtxt n ctxt of

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

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

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

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

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

835 let ps_in' = map simpl ps_in

836 let ps_in' = map simpl ps_in

836 pdef = map debind ps_in' in

837 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

838 OK (CaseDef args sc _) ->

839 OK (CaseDef args sc _) ->

839 addDef n (CaseOp ci

840 addDef n (CaseOp ci

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

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

src/Idris/Coverage.hs+2−1

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

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

377 | otherwise = do

378 t <- getTotality n

379+ i <- getIState

379− updateContext (simplifyCasedef n)

380+ updateContext (simplifyCasedef n $ getErasureInfo i)

380 ctxt <- getContext

381 ctxt <- getContext

381 i <- getIState

382 i <- getIState

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

383 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

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

1084 _ -> return ()

1085

1086+ erInfo <- getErasureInfo <$> getIState

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

1087 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

1088 cov <- coverage

1089 cov <- coverage

1089 pmissing <-

1090 pmissing <-

1090 if cov && not (hasDefault cs)

1091 if cov && not (hasDefault cs)

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

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

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

1134

1135

1135 tree' <- tclift $ simpleCase tcase knowncovering reflect

1136 tree' <- tclift $ simpleCase tcase knowncovering reflect

1136− RunTime fc inacc atys pdef'

1137+ RunTime fc inacc atys pdef' erInfo

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

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

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

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

1139 ctxt <- getContext

1140 ctxt <- getContext

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

1143 (idris_patdefs ist) })

1144 (idris_patdefs ist) })

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

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

1145 case lookupTy n ctxt of

1146 case lookupTy n ctxt of

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

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

1147 tcase knowncovering

1148 tcase knowncovering

1148 reflect

1149 reflect

1149 (AssertTotal `elem` opts)

1150 (AssertTotal `elem` opts)

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

2360 -- Do totality checking after entire mutual block

2361 -- Do totality checking after entire mutual block

2361 i <- get

2362 i <- get

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

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

2363− updateContext (simplifyCasedef n))

2364+ updateContext (simplifyCasedef n $ getErasureInfo i))

2364 (map snd (idris_totcheck i))

2365 (map snd (idris_totcheck i))

2365 mapM_ buildSCG (idris_totcheck i)

2366 mapM_ buildSCG (idris_totcheck i)

2366 mapM_ checkDeclTotality (idris_totcheck i)

2367 mapM_ checkDeclTotality (idris_totcheck i)

src/Idris/Parser.hs+1−1

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

1282 -- simplify every definition do give the totality checker

1283 -- a better chance

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

1285− updateContext (simplifyCasedef n))

1285+ updateContext (simplifyCasedef n $ getErasureInfo i))

1286 (map snd (idris_totcheck i))

1287 -- build size change graph from simplified definitions

1288 iLOG "Totality checking"

src/Idris/Prover.hs+2−1

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

78 OK _ -> return ()

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

80 ptm' <- applyOpts ptm

81+ ei <- getErasureInfo `fmap` getIState

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

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

82 [] [] -- argtys, inaccArgs

83 [] [] -- argtys, inaccArgs

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

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

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

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