d9513aa · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1360 from ziman/case-elab-erasure

d9513aaEdwin Brady12 years ago

src/Idris/AbsSyntaxTree.hs+7

compare with master

unifiedsplit

@@ -1731,3 +1731,10 @@ usedNamesIn vars ist tm = nub $ ni [] tm

1731

1732 niTacImp env (TacImp _ _ scr) = ni env scr

1733 niTacImp _ _ = []

1734+

1735+-- Return the list of inaccessible (= dotted) positions for a name.

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

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+121−83

@@ -1,13 +1,15 @@

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

8import Idris.Core.TT

10+import Control.Applicative hiding (Const)

10import Control.Monad.State

11import Control.Monad.State

12+import Control.Monad.Reader

11import Data.Maybe

13import Data.Maybe

12import Data.List hiding (partition)

14import Data.List hiding (partition)

13import qualified Data.List(partition)

15import qualified Data.List(partition)

@@ -24,7 +26,7 @@ data CaseDef = CaseDef [Name] !SC [Term]

24-- in the function `prune` as a means of optimisation

26-- in the function `prune` as a means of optimisation

25-- of already built case trees.

27-- of already built case trees.

26--

28--

27−-- While the intermediate representation (follows in the pipeline)

29+-- While the intermediate representation (follows in the pipeline, named LExp)

28-- allows casing on arbitrary terms, here we choose to maintain the distinction

30-- allows casing on arbitrary terms, here we choose to maintain the distinction

29-- in order to allow for better optimisation opportunities.

31-- in order to allow for better optimisation opportunities.

30--

32--

@@ -213,6 +215,11 @@ isUsed sc n = used sc where

213 usedA (SucCase _ sc) = used sc

215 usedA (SucCase _ sc) = used sc

214 usedA (DefaultCase sc) = used sc

216 usedA (DefaultCase sc) = used sc

215

217

218+type ErasureInfo = Name -> [Int] -- name to list of inaccessible arguments; empty list if name not found

219+type CaseBuilder a = ReaderT ErasureInfo (State CS) a

220+

221+runCaseBuilder :: ErasureInfo -> CaseBuilder a -> (CS -> (a, CS))

222+runCaseBuilder ei bld = runState $ runReaderT bld ei

216

223

217data Phase = CompileTime | RunTime

224data Phase = CompileTime | RunTime

218 deriving (Show, Eq)

225 deriving (Show, Eq)

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

223simpleCase :: Bool -> Bool -> Bool ->

230simpleCase :: Bool -> Bool -> Bool ->

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

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

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

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

233+ ErasureInfo ->

226 TC CaseDef

234 TC CaseDef

227−simpleCase tc cover reflect phase fc inacc argtys cs

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

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

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

229 case r of

237 case r of

230 Impossible -> False

238 Impossible -> False

@@ -243,7 +251,7 @@ simpleCase tc cover reflect phase fc inacc argtys cs

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

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

244 ns = take numargs args

252 ns = take numargs args

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

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

246− (tree, st) = runState

254+ (tree, st) = runCaseBuilder erInfo

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

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

248 ([], numargs, [])

256 ([], numargs, [])

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

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

@@ -334,18 +342,20 @@ toPats reflect tc f = reverse (toPat reflect tc (getArgs f)) where

334 getArgs _ = []

342 getArgs _ = []

335

343

336toPat :: Bool -> Bool -> [Term] -> [Pat]

344toPat :: Bool -> Bool -> [Term] -> [Pat]

337−toPat reflect tc tms = evalState (mapM (\x -> toPat' x []) tms) []

345+toPat reflect tc = map $ toPat' []

338 where

346 where

339− toPat' (P (DCon t a) nm@(UN n) _) [_,_,arg]

347+ toPat' [_,_,arg](P (DCon t a) nm@(UN n) _)

340− | n == txt "Delay" = do arg' <- toPat' arg []

348+ | n == txt "Delay"

341− return $ PCon nm t [PAny, PAny, arg']

349+ = PCon nm t [PAny, PAny, toPat' [] arg]

350+

342− toPat' (P (DCon t a) n _) args = do args' <- mapM (\x -> toPat' x []) args

351+ toPat' args (P (DCon t a) n _)

343− return $ PCon n t args'

352+ = PCon n t $ map (toPat' []) args

353+

344 -- n + 1

354 -- n + 1

345− toPat' (P _ (UN pabi) _)

355+ toPat' [p, Constant (BI 1)] (P _ (UN pabi) _)

346− [p, Constant (BI 1)] | pabi == txt "prim__addBigInt"

356+ | pabi == txt "prim__addBigInt"

347− = do p' <- toPat' p []

357+ = PSuc $ toPat' [] p

348− return $ PSuc p'

358+

349 -- Typecase

359 -- Typecase

350-- toPat' (P (TCon t a) n _) args | tc

360-- toPat' (P (TCon t a) n _) args | tc

351-- = do args' <- mapM (\x -> toPat' x []) args

361-- = do args' <- mapM (\x -> toPat' x []) args

@@ -360,26 +370,25 @@ toPat reflect tc tms = evalState (mapM (\x -> toPat' x []) tms) []

360-- | tc = return $ PCon (UN "Integer") 6 []

370-- | tc = return $ PCon (UN "Integer") 6 []

361-- toPat' (Constant (AType (ATInt (ITFixed n)))) []

371-- toPat' (Constant (AType (ATInt (ITFixed n)))) []

362-- | tc = return $ PCon (UN (fixedN n)) (7 + fromEnum n) [] -- 7-10 inclusive

372-- | tc = return $ PCon (UN (fixedN n)) (7 + fromEnum n) [] -- 7-10 inclusive

363− toPat' (P Bound n ty) [] = -- trace (show (n, ty)) $

373+--

364− do ns <- get

374+

365− if n `elem` ns

375+ toPat' [] (P Bound n ty) = PV n ty

366− then return PAny

367− else do put (n : ns)

368− return (PV n ty)

369− toPat' (App f a) args = toPat' f (a : args)

376+ toPat' args (App f a) = toPat' (a : args) f

370− toPat' (Constant (AType _)) [] = return PTyPat

377+ toPat' [] (Constant (AType _)) = PTyPat

371− toPat' (Constant StrType) [] = return PTyPat

378+ toPat' [] (Constant StrType) = PTyPat

372− toPat' (Constant PtrType) [] = return PTyPat

379+ toPat' [] (Constant PtrType) = PTyPat

373− toPat' (Constant VoidType) [] = return PTyPat

380+ toPat' [] (Constant VoidType) = PTyPat

374− toPat' (Constant x) [] = return $ PConst x

381+ toPat' [] (Constant x) = PConst x

382+

383+ toPat' [] (Bind n (Pi t) sc)

375− toPat' (Bind n (Pi t) sc) [] | reflect && noOccurrence n sc

384+ | reflect && noOccurrence n sc

376− = do t' <- toPat' t []

377− sc' <- toPat' sc []

378− return $ PReflected (sUN "->") (t':sc':[])

385+ = PReflected (sUN "->") [toPat' [] t, toPat' [] sc]

386+

379− toPat' (P _ n _) args | reflect

387+ toPat' args (P _ n _)

388+ | reflect

380− = do args' <- mapM (\x -> toPat' x []) args

389+ = PReflected n $ map (toPat' []) args

381− return $ PReflected n args'

390+

382− toPat' t _ = return PAny

391+ toPat' _ t = PAny

383

392

384 fixedN IT8 = "Bits8"

393 fixedN IT8 = "Bits8"

385 fixedN IT16 = "Bits16"

394 fixedN IT16 = "Bits16"

@@ -459,7 +468,7 @@ order ns' cs = let patnames = transpose (map (zip ns') (map fst cs))

459 numNames xs [] = length xs

468 numNames xs [] = length xs

460

469

461match :: [Name] -> [Clause] -> SC -- error case

470match :: [Name] -> [Clause] -> SC -- error case

462− -> State CS SC

471+ -> CaseBuilder SC

463match [] (([], ret) : xs) err

472match [] (([], ret) : xs) err

464 = do (ts, v, ntys) <- get

473 = do (ts, v, ntys) <- get

465 put (ts ++ (map (fst.snd) xs), v, ntys)

474 put (ts ++ (map (fst.snd) xs), v, ntys)

@@ -469,13 +478,19 @@ match [] (([], ret) : xs) err

469match vs cs err = do let ps = partition cs

478match vs cs err = do let ps = partition cs

470 mixture vs ps err

479 mixture vs ps err

471

480

472−mixture :: [Name] -> [Partition] -> SC -> State CS SC

481+mixture :: [Name] -> [Partition] -> SC -> CaseBuilder SC

473mixture vs [] err = return err

482mixture vs [] err = return err

474mixture vs (Cons ms : ps) err = do fallthrough <- mixture vs ps err

483mixture vs (Cons ms : ps) err = do fallthrough <- mixture vs ps err

475 conRule vs ms fallthrough

484 conRule vs ms fallthrough

476mixture vs (Vars ms : ps) err = do fallthrough <- mixture vs ps err

485mixture vs (Vars ms : ps) err = do fallthrough <- mixture vs ps err

477 varRule vs ms fallthrough

486 varRule vs ms fallthrough

478

487

488+-- Return the list of inaccessible arguments of a data constructor.

489+inaccessibleArgs :: Name -> CaseBuilder [Int]

490+inaccessibleArgs n = do

491+ getInaccessiblePositions <- ask -- this function is the only thing in the environment

492+ return $ getInaccessiblePositions n

493+

479data ConType = CName Name Int -- named constructor

494data ConType = CName Name Int -- named constructor

480 | CFn Name -- reflected function name

495 | CFn Name -- reflected function name

481 | CSuc -- n+1

496 | CSuc -- n+1

@@ -486,76 +501,99 @@ data Group = ConGroup ConType -- Constructor

486 [([Pat], Clause)] -- arguments and rest of alternative

501 [([Pat], Clause)] -- arguments and rest of alternative

487 deriving Show

502 deriving Show

488

503

489−conRule :: [Name] -> [Clause] -> SC -> State CS SC

504+conRule :: [Name] -> [Clause] -> SC -> CaseBuilder SC

490conRule (v:vs) cs err = do groups <- groupCons cs

505conRule (v:vs) cs err = do groups <- groupCons cs

491 caseGroups (v:vs) groups err

506 caseGroups (v:vs) groups err

492

507

493−caseGroups :: [Name] -> [Group] -> SC -> State CS SC

508+caseGroups :: [Name] -> [Group] -> SC -> CaseBuilder SC

494caseGroups (v:vs) gs err = do g <- altGroups gs

509caseGroups (v:vs) gs err = do g <- altGroups gs

495 return $ Case v (sort g)

510 return $ Case v (sort g)

496 where

511 where

497 altGroups [] = return [DefaultCase err]

512 altGroups [] = return [DefaultCase err]

513+

498 altGroups (ConGroup (CName n i) args : cs)

514 altGroups (ConGroup (CName n i) args : cs)

499− = do g <- altGroup n i args

515+ = (:) <$> altGroup n i args <*> altGroups cs

500− rest <- altGroups cs

516+

501− return (g : rest)

502 altGroups (ConGroup (CFn n) args : cs)

517 altGroups (ConGroup (CFn n) args : cs)

503− = do g <- altFnGroup n args

518+ = (:) <$> altFnGroup n args <*> altGroups cs

504− rest <- altGroups cs

519+

505− return (g : rest)

506 altGroups (ConGroup CSuc args : cs)

520 altGroups (ConGroup CSuc args : cs)

507− = do g <- altSucGroup args

521+ = (:) <$> altSucGroup args <*> altGroups cs

508− rest <- altGroups cs

522+

509− return (g : rest)

510 altGroups (ConGroup (CConst c) args : cs)

523 altGroups (ConGroup (CConst c) args : cs)

511− = do g <- altConstGroup c args

524+ = (:) <$> altConstGroup c args <*> altGroups cs

512− rest <- altGroups cs

525+

513− return (g : rest)

526+ altGroup n i args = do inacc <- inaccessibleArgs n

514−

527+ (newVars, accVars, inaccVars, nextCs) <- argsToAlt inacc args

515− altGroup n i gs = do (newArgs, nextCs) <- argsToAlt gs

516− matchCs <- match (newArgs ++ vs) nextCs err

528+ matchCs <- match (accVars ++ vs ++ inaccVars) nextCs err

517− return $ ConCase n i newArgs matchCs

529+ return $ ConCase n i newVars matchCs

530+

518− altFnGroup n gs = do (newArgs, nextCs) <- argsToAlt gs

531+ altFnGroup n args = do (newVars, _, [], nextCs) <- argsToAlt [] args

519− matchCs <- match (newArgs ++ vs) nextCs err

532+ matchCs <- match (newVars ++ vs) nextCs err

520− return $ FnCase n newArgs matchCs

533+ return $ FnCase n newVars matchCs

534+

521− altSucGroup gs = do ([newArg], nextCs) <- argsToAlt gs

535+ altSucGroup args = do ([newVar], _, [], nextCs) <- argsToAlt [] args

522− matchCs <- match (newArg:vs) nextCs err

536+ matchCs <- match (newVar:vs) nextCs err

523− return $ SucCase newArg matchCs

537+ return $ SucCase newVar matchCs

538+

524− altConstGroup n gs = do (_, nextCs) <- argsToAlt gs

539+ altConstGroup n args = do (_, _, [], nextCs) <- argsToAlt [] args

525− matchCs <- match vs nextCs err

540+ matchCs <- match vs nextCs err

526− return $ ConstCase n matchCs

541+ return $ ConstCase n matchCs

527−

542+

543+-- Returns:

544+-- * names of all variables arising from match

545+-- * names of accessible variables (subset of all variables)

546+-- * names of inaccessible variables (subset of all variables)

547+-- * clauses corresponding to (accVars ++ origVars ++ inaccVars)

528−argsToAlt :: [([Pat], Clause)] -> State CS ([Name], [Clause])

548+argsToAlt :: [Int] -> [([Pat], Clause)] -> CaseBuilder ([Name], [Name], [Name], [Clause])

529−argsToAlt [] = return ([], [])

549+argsToAlt _ [] = return ([], [], [], [])

530−argsToAlt rs@((r, m) : rest)

550+argsToAlt inacc rs@((r, m) : rest) = do

531− = do newArgs <- getNewVars r

551+ newVars <- getNewVars r

552+ let (accVars, inaccVars) = partitionAcc newVars

532− return (newArgs, addRs rs)

553+ return (newVars, accVars, inaccVars, addRs rs)

533 where

554 where

555+ -- Create names for new variables arising from the given patterns.

556+ getNewVars :: [Pat] -> CaseBuilder [Name]

534 getNewVars [] = return []

557 getNewVars [] = return []

535 getNewVars ((PV n t) : ns) = do v <- getVar "e"

558 getNewVars ((PV n t) : ns) = do v <- getVar "e"

559+ nsv <- getNewVars ns

560+

561+ -- Record the type of the variable.

562+ --

563+ -- It seems that the ordering is not important

564+ -- and we can put (v,t) always in front of "ntys"

565+ -- (the varName-type pairs seem to represent a mapping).

566+ --

567+ -- The code that reads this is currently

568+ -- commented out, anyway.

536 (cs, i, ntys) <- get

569 (cs, i, ntys) <- get

537 put (cs, i, (v, t) : ntys)

570 put (cs, i, (v, t) : ntys)

538− nsv <- getNewVars ns

571+

539 return (v : nsv)

572 return (v : nsv)

573+

540− getNewVars (PAny : ns) = do v <- getVar "i"

574+ getNewVars (PAny : ns) = (:) <$> getVar "i" <*> getNewVars ns

541− nsv <- getNewVars ns

542− return (v : nsv)

543− getNewVars (PTyPat : ns) = do v <- getVar "t"

575+ getNewVars (PTyPat : ns) = (:) <$> getVar "t" <*> getNewVars ns

544− nsv <- getNewVars ns

545− return (v : nsv)

546− getNewVars (_ : ns) = do v <- getVar "e"

576+ getNewVars (_ : ns) = (:) <$> getVar "e" <*> getNewVars ns

547− nsv <- getNewVars ns

577+

548− return (v : nsv)

578+ -- Partition a list of things into (accessible, inaccessible) things,

579+ -- according to the list of inaccessible indices.

580+ partitionAcc xs =

581+ ( [x | (i,x) <- zip [0..] xs, i `notElem` inacc]

582+ , [x | (i,x) <- zip [0..] xs, i `elem` inacc]

583+ )

584+

549 addRs [] = []

585 addRs [] = []

550− addRs ((r, (ps, res)) : rs) = ((r++ps, res) : addRs rs)

586+ addRs ((r, (ps, res)) : rs) = ((acc++ps++inacc, res) : addRs rs)

587+ where

588+ (acc, inacc) = partitionAcc r

551

589

552 uniq i (UN n) = MN i n

590 uniq i (UN n) = MN i n

553 uniq i n = n

591 uniq i n = n

554

592

555−getVar :: String -> State CS Name

593+getVar :: String -> CaseBuilder Name

556getVar b = do (t, v, ntys) <- get; put (t, v+1, ntys); return (sMN v b)

594getVar b = do (t, v, ntys) <- get; put (t, v+1, ntys); return (sMN v b)

557

595

558−groupCons :: [Clause] -> State CS [Group]

596+groupCons :: [Clause] -> CaseBuilder [Group]

559groupCons cs = gc [] cs

597groupCons cs = gc [] cs

560 where

598 where

561 gc acc [] = return acc

599 gc acc [] = return acc

@@ -581,7 +619,7 @@ groupCons cs = gc [] cs

581-- | otherwise = g : addConG con res gs

619-- | otherwise = g : addConG con res gs

582 addConG con res (g : gs) = g : addConG con res gs

620 addConG con res (g : gs) = g : addConG con res gs

583

621

584−varRule :: [Name] -> [Clause] -> SC -> State CS SC

622+varRule :: [Name] -> [Clause] -> SC -> CaseBuilder SC

585varRule (v : vs) alts err =

623varRule (v : vs) alts err =

586 do alts' <- mapM (repVar v) alts

624 do alts' <- mapM (repVar v) alts

587 match vs alts' err

625 match vs alts' err

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)

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

2361 -- Do totality checking after entire mutual block

2362 -- Do totality checking after entire mutual block

2362 i <- get

2363 i <- get

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

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

2364− updateContext (simplifyCasedef n))

2365+ updateContext (simplifyCasedef n $ getErasureInfo i))

2365 (map snd (idris_totcheck i))

2366 (map snd (idris_totcheck i))

2366 mapM_ buildSCG (idris_totcheck i)

2367 mapM_ buildSCG (idris_totcheck i)

2367 mapM_ checkDeclTotality (idris_totcheck i)

2368 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)]