d43a279 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Change TCGen flag to Dictionary, update evaluator accordingly

commitd43a2797d8e22896f271e9b75f5b7aea149c67e9 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 7 Aug 2013, 20:04 (13 years ago) parent3fe14c7

8 files changed+82−52

compare with master

unifiedsplit

src/Core/Evaluate.hs+42−27 src/Core/Execute.hs+4−4 src/IRTS/Compiler.hs+3−2 src/Idris/AbsSyntaxTree.hs+8−2 src/Idris/Coverage.hs+2−2 src/Idris/ElabDecls.hs+12−8 src/Idris/IBC.hs+10−6 src/Idris/Prover.hs+1−1

src/Core/Evaluate.hs+42−27

@@ -3,7 +3,8 @@

44module Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

55 simplify, specialise, hnf, convEq, convEq',

6− Def(..), Accessibility(..), Totality(..), PReason(..),

6+ Def(..), CaseInfo(..),

7+ Accessibility(..), Totality(..), PReason(..),

78 Context, initContext, ctxtAlist, uconstraints, next_tvar,

89 addToCtxt, setAccess, setTotal, addCtxtDef, addTyDecl,

910 addDatatype, addCasedef, simplifyCasedef, addOperator,

@@ -24,7 +25,11 @@ data EvalState = ES { limited :: [(Name, Int)],

2425

2526type Eval a = State EvalState a

2627

27−data EvalOpt = Spec | HNF | Simplify Bool | AtREPL

28+data EvalOpt = Spec

29+ | HNF

30+ | Simplify Bool -- simplifying - if True, we're doing it to help

31+ -- totality checking so reduce dictionaries too

32+ | AtREPL

2833 deriving (Show, Eq)

2934

3035initEval = ES [] 0

@@ -95,14 +100,14 @@ specialise ctxt env limits t

95100-- | Like normalise, but we only reduce functions that are marked as okay to

96101-- inline (and probably shouldn't reduce lets?)

97102simplify :: Context -> Bool -> Env -> TT Name -> TT Name

98−simplify ctxt runtime env t

103+simplify ctxt alldicts env t

99104 = evalState (do val <- eval False ctxt [(UN "lazy", 0),

100105 (UN "assert_smaller", 0),

101106 (UN "par", 0),

102107 (UN "prim__syntactic_eq", 0),

103108 (UN "fork", 0)]

104109 (map finalEntry env) (finalise t)

105− [Simplify runtime]

110+ [Simplify alldicts]

106111 quote 0 val) initEval

107112

108113-- | Reduce a term to head normal form

@@ -168,9 +173,11 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

168173 atRepl = AtREPL `elem` opts

169174 hnf = HNF `elem` opts

170175

171− canSimplify inl inr n stk

172− = (Simplify False `elem` opts && (not inl || elem n stk))

173− || (Simplify True `elem` opts && (not inr || elem n stk))

176+ -- returns 'True' if the function should block

177+ -- normal evaluation should return false

178+ blockSimplify (CaseInfo inl dict) n stk

179+ = (Simplify False `elem` opts && (not (inl || dict) || elem n stk))

180+ || (Simplify True `elem` opts && (not inl || elem n stk))

174181

175182 ev ntimes stk top env (P _ n ty)

176183 | Just (Let t v) <- lookup n genv = ev ntimes stk top env v

@@ -185,9 +192,9 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

185192 ev ntimes (n:stk) True env tm

186193 [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty

187194 return $ VP nt n vty

188− [(CaseOp inl inr _ _ _ [] tree _ _, acc)]

195+ [(CaseOp ci _ _ _ [] tree _ _, acc)]

189196 | acc == Public || simpl -> -- unoptimised version

190− if canSimplify inl inr n stk

197+ if blockSimplify ci n stk

191198 then liftM (VP Ref n) (ev ntimes stk top env ty)

192199 else do c <- evCase ntimes n (n:stk) top env [] [] tree

193200 case c of

@@ -260,9 +267,9 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

260267 if u then

261268 do let val = lookupDefAcc n atRepl ctxt

262269 case val of

263− [(CaseOp inl inr _ _ _ ns tree _ _, acc)]

270+ [(CaseOp ci _ _ _ ns tree _ _, acc)]

264271 | acc == Public -> -- unoptimised version

265− if canSimplify inl inr n stk

272+ if blockSimplify ci n stk

266273 then return $ unload env (VP Ref n ty) args

267274 else do c <- evCase ntimes n (n:stk) top env ns args tree

268275 case c of

@@ -470,7 +477,7 @@ eval_hnf ctxt statics genv tm = ev [] tm where

470477 ev env (P Ref n ty) = case lookupDef n ctxt of

471478 [Function _ t] -> ev env t

472479 [TyDecl nt ty] -> return $ HP nt n ty

473− [CaseOp inl _ _ _ _ [] tree _ _] ->

480+ [CaseOp _ _ _ _ [] tree _ _] ->

474481 do c <- evCase env [] [] tree

475482 case c of

476483 (Nothing, _, _) -> return $ HP Ref n ty

@@ -500,7 +507,7 @@ eval_hnf ctxt statics genv tm = ev [] tm where

500507 app <- apply env sc' as

501508 wknH (-1) app

502509 apply env (HP Ref n ty) args

503− | [CaseOp _ _ _ _ _ ns tree _ _] <- lookupDef n ctxt

510+ | [CaseOp _ _ _ _ ns tree _ _] <- lookupDef n ctxt

504511 = do c <- evCase env ns args tree

505512 case c of

506513 (Nothing, _, env') -> return $ unload env' (HP Ref n ty) args

@@ -638,8 +645,8 @@ convEq ctxt = ceq [] where

638645 sameDefs ps x y = case (lookupDef x ctxt, lookupDef y ctxt) of

639646 ([Function _ xdef], [Function _ ydef])

640647 -> ceq ((x,y):ps) xdef ydef

641− ([CaseOp _ _ _ _ _ _ xdef _ _],

642− [CaseOp _ _ _ _ _ _ ydef _ _])

648+ ([CaseOp _ _ _ _ _ xdef _ _],

649+ [CaseOp _ _ _ _ _ ydef _ _])

643650 -> caseeq ((x,y):ps) xdef ydef

644651 _ -> return False

645652

@@ -661,12 +668,18 @@ spec ctxt statics genv tm = error "spec undefined"

661668data Def = Function Type Term

662669 | TyDecl NameType Type

663670 | Operator Type Int ([Value] -> Maybe Value)

664− | CaseOp Bool Bool -- compile-time/run-time inlinable

671+ | CaseOp CaseInfo

665672 Type

666673 [Either Term (Term, Term)] -- original definition

667674 [([Name], Term, Term)] -- simplified definition

668675 [Name] SC -- Compile time case definition

669676 [Name] SC -- Run time cae definitions

677+

678+data CaseInfo = CaseInfo {

679+ case_inlinable :: Bool,

680+ tc_dictionary :: Bool

681+ }

682+

670683{-!

671684deriving instance Binary Def

672685!-}

@@ -675,7 +688,7 @@ instance Show Def where

675688 show (Function ty tm) = "Function: " ++ show (ty, tm)

676689 show (TyDecl nt ty) = "TyDecl: " ++ show nt ++ " " ++ show ty

677690 show (Operator ty _ _) = "Operator: " ++ show ty

678− show (CaseOp inlc inlr ty ps_in ps ns sc ns' sc')

691+ show (CaseOp (CaseInfo inlc inlr) ty ps_in ps ns sc ns' sc')

679692 = "Case: " ++ show ty ++ " " ++ show ps ++ "\n" ++

680693 show ns ++ " " ++ show sc ++ "\n" ++

681694 show ns' ++ " " ++ show sc' ++ "\n" ++

@@ -793,12 +806,14 @@ addDatatype (Data n tag ty cons) uctxt

793806 addCons (tag+1) cons (addDef n

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

795808

796−addCasedef :: Name -> Bool -> Bool -> Bool -> Bool -> Bool ->

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

810+addCasedef :: Name -> CaseInfo -> Bool -> Bool -> Bool -> Bool ->

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

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

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

800814 Type -> Context -> Context

801−addCasedef n alwaysInline tcase covering reflect asserted ps_in ps psrt ty uctxt

815+addCasedef n ci@(CaseInfo alwaysInline tcdict)

816+ tcase covering reflect asserted ps_in ps psrt ty uctxt

802817 = let ctxt = definitions uctxt

803818 access = case lookupDefAcc n False uctxt of

804819 [(_, acc)] -> acc

@@ -806,10 +821,10 @@ addCasedef n alwaysInline tcase covering reflect asserted ps_in ps psrt ty uctxt

806821 ctxt' = case (simpleCase tcase covering reflect CompileTime (FC "" 0) ps,

807822 simpleCase tcase covering reflect RunTime (FC "" 0) psrt) of

808823 (OK (CaseDef args sc _), OK (CaseDef args' sc' _)) ->

809− let inl = alwaysInline

824+ let inl = alwaysInline || tcdict

810825 inlc = (inl || small n args sc') && (not asserted)

811826 inlr = inl || small n args sc' in

812− addDef n (CaseOp inlc inlr

827+ addDef n (CaseOp (ci { case_inlinable = inlc })

813828 ty ps_in ps args sc args' sc',

814829 access, Unchecked) ctxt in

815830 uctxt { definitions = ctxt' }

@@ -818,14 +833,14 @@ simplifyCasedef :: Name -> Context -> Context

818833simplifyCasedef n uctxt

819834 = let ctxt = definitions uctxt

820835 ctxt' = case lookupCtxt n ctxt of

821− [(CaseOp inl inr ty [] ps args sc args' sc', acc, tot)] ->

836+ [(CaseOp ci ty [] ps args sc args' sc', acc, tot)] ->

822837 ctxt -- nothing to simplify (or already done...)

823− [(CaseOp inl inr ty ps_in ps args sc args' sc', acc, tot)] ->

838+ [(CaseOp ci ty ps_in ps args sc args' sc', acc, tot)] ->

824839 let ps_in' = map simpl ps_in

825840 pdef = map debind ps_in' in

826841 case simpleCase False True False CompileTime (FC "" 0) pdef of

827842 OK (CaseDef args sc _) ->

828− addDef n (CaseOp inl inr

843+ addDef n (CaseOp ci

829844 ty ps_in' ps args sc args' sc',

830845 acc, tot) ctxt

831846 _ -> ctxt in

@@ -863,7 +878,7 @@ lookupTy n ctxt

863878 (Function ty _) -> return ty

864879 (TyDecl _ ty) -> return ty

865880 (Operator ty _ _) -> return ty

866− (CaseOp _ _ ty _ _ _ _ _ _) -> return ty

881+ (CaseOp _ ty _ _ _ _ _ _) -> return ty

867882

868883isConName :: Name -> Context -> Bool

869884isConName n ctxt

@@ -879,7 +894,7 @@ isFnName n ctxt

879894 case tfst def of

880895 (Function _ _) -> return True

881896 (Operator _ _ _) -> return True

882− (CaseOp _ _ _ _ _ _ _ _ _) -> return True

897+ (CaseOp _ _ _ _ _ _ _ _) -> return True

883898 _ -> return False

884899

885900lookupP :: Name -> Context -> [Term]

@@ -888,7 +903,7 @@ lookupP n ctxt

888903 p <- case def of

889904 (Function ty tm, a, _) -> return (P Ref n ty, a)

890905 (TyDecl nt ty, a, _) -> return (P nt n ty, a)

891− (CaseOp _ _ ty _ _ _ _ _ _, a, _) -> return (P Ref n ty, a)

906+ (CaseOp _ ty _ _ _ _ _ _, a, _) -> return (P Ref n ty, a)

892907 (Operator ty _ _, a, _) -> return (P Ref n ty, a)

893908 case snd p of

894909 Hidden -> []

src/Core/Execute.hs+4−4

@@ -181,9 +181,9 @@ doExec env ctxt p@(P Ref n ty) =

181181 [Function _ tm] -> doExec env ctxt tm

182182 [TyDecl _ _] -> return (EP Ref n EErased) -- abstract def

183183 [Operator tp arity op] -> return (EP Ref n EErased) -- will be special-cased later

184− [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun

184+ [CaseOp _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun

185185 doExec env ctxt tm

186− [CaseOp _ _ _ _ _ ns sc _ _] -> return (EP Ref n EErased)

186+ [CaseOp _ _ _ _ ns sc _ _] -> return (EP Ref n EErased)

187187 [] -> execFail $ "Could not find " ++ show n ++ " in definitions."

188188 thing -> trace (take 200 $ "got to " ++ show thing ++ " lookup up " ++ show n) $ undefined

189189doExec env ctxt p@(P Bound n ty) =

@@ -301,10 +301,10 @@ execApp' env ctxt f@(EP _ n _) args =

301301 execApp' env ctxt r (drop arity args)

302302 Nothing -> return (mkEApp f args)

303303 else return (mkEApp f args)

304− [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun

304+ [CaseOp _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun

305305 do rhs <- doExec env ctxt tm

306306 execApp' env ctxt rhs args

307− [CaseOp _ _ _ _ _ ns sc _ _] ->

307+ [CaseOp _ _ _ _ ns sc _ _] ->

308308 do res <- execCase env ctxt ns sc args

309309 return $ fromMaybe (mkEApp f args) res

310310 thing -> return $ mkEApp f args

src/IRTS/Compiler.hs+3−2

@@ -159,8 +159,9 @@ declArgs args inl n x = LFun (if inl then [Inline] else []) n args x

159159

160160mkLDecl n (Function tm _) = do e <- ir tm

161161 return (declArgs [] True n e)

162−mkLDecl n (CaseOp _ inl _ _ pats _ _ args sc) = do e <- ir (args, sc)

163− return (declArgs [] inl n e)

162+mkLDecl n (CaseOp ci _ _ pats _ _ args sc)

163+ = do e <- ir (args, sc)

164+ return (declArgs [] (case_inlinable ci) n e)

164165mkLDecl n (TyDecl (DCon t a) _) = return $ LConstructor n t a

165166mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a

166167mkLDecl n _ = return (LFun [] n [] (LError ("Impossible declaration " ++ show n)))

src/Idris/AbsSyntaxTree.hs+8−2

@@ -330,8 +330,11 @@ expl = Exp False Dynamic ""

330330constraint = Constraint False Dynamic ""

331331tacimpl t = TacImp False Dynamic t ""

332332

333−data FnOpt = Inlinable | TotalFn | PartialFn

334− | Coinductive | AssertTotal | TCGen

333+data FnOpt = Inlinable -- always evaluate when simplifying

334+ | TotalFn | PartialFn

335+ | Coinductive | AssertTotal

336+ | Dictionary -- type class dictionary, eval only when

337+ -- a function argument, and further evaluation resutls

335338 | Implicit -- implicit coercion

336339 | CExport String -- export, with a C name

337340 | Reflection -- a reflecting function, compile-time only

@@ -346,6 +349,9 @@ type FnOpts = [FnOpt]

346349inlinable :: FnOpts -> Bool

347350inlinable = elem Inlinable

348351

352+dictionary :: FnOpts -> Bool

353+dictionary = elem Dictionary

354+

349355-- | Top-level declarations such as compiler directives, definitions,

350356-- datatypes and typeclasses.

351357data PDecl' t

src/Idris/Coverage.hs+2−2

@@ -303,7 +303,7 @@ checkTotality path fc n

303303 t' <- case t of

304304 Unchecked ->

305305 case lookupDef n ctxt of

306− [CaseOp _ _ _ _ pats _ _ _ _] ->

306+ [CaseOp _ _ _ pats _ _ _ _] ->

307307 do t' <- if AssertTotal `elem` opts

308308 then return $ Total []

309309 else calcTotality path fc n pats

@@ -367,7 +367,7 @@ buildSCG (_, n) = do

367367 ist <- getIState

368368 case lookupCtxt n (idris_callgraph ist) of

369369 [cg] -> case lookupDef n (tt_ctxt ist) of

370− [CaseOp _ _ _ pats _ args sc _ _] ->

370+ [CaseOp _ _ pats _ args sc _ _] ->

371371 do logLvl 2 $ "Building SCG for " ++ show n ++ " from\n"

372372 ++ show pats ++ "\n" ++ show sc

373373 let newscg = buildSCG' ist (rights pats) args

src/Idris/ElabDecls.hs+12−8

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

521521 -- question: CAFs in where blocks?

522522 tclift $ tfail $ At fc (NoTypeDecl n)

523523 [ty] -> return ty

524− pats_in <- mapM (elabClause info (TCGen `elem` opts))

524+ pats_in <- mapM (elabClause info (Dictionary `elem` opts))

525525 (zip [0..] cs)

526526 -- if the return type of 'ty' is collapsible, the optimised version should

527527 -- just do nothing

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

623623 ist <- getIState

624624 putIState (ist { idris_patdefs = addDef n (pdef', pmissing)

625625 (idris_patdefs ist) })

626+ let caseInfo = CaseInfo (inlinable opts) (dictionary opts)

626627 case lookupTy n ctxt of

627− [ty] -> do updateContext (addCasedef n (inlinable opts)

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

628629 tcase knowncovering

629630 reflect

630631 (AssertTotal `elem` opts)

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

636637 when (tot /= Unchecked) $ addIBC (IBCTotal n tot)

637638 i <- getIState

638639 case lookupDef n (tt_ctxt i) of

639− (CaseOp _ _ _ _ _ scargs sc scargs' sc' : _) ->

640+ (CaseOp _ _ _ _ scargs sc scargs' sc' : _) ->

640641 do let calls = findCalls sc' scargs'

641642 let used = findUsedArgs sc' scargs'

642643 -- let scg = buildSCG i sc scargs

@@ -1116,7 +1117,7 @@ elabClass info syn doc fc constraints tn ps ds

11161117 Just (syn, o, ty) -> do let ty' = insertConstraint c ty

11171118 let ds = map (decorateid defaultdec)

11181119 [PTy "" syn fc [] n ty',

1119− PClauses fc (Inlinable:TCGen:o ++ opts) n cs]

1120+ PClauses fc (o ++ opts) n cs]

11201121 iLOG (show ds)

11211122 return (n, ((defaultdec n, ds!!1), ds))

11221123 _ -> fail $ show n ++ " is not a method"

@@ -1130,6 +1131,7 @@ elabClass info syn doc fc constraints tn ps ds

11301131 clause (PClauses _ _ _ _) = True

11311132 clause _ = False

11321133

1134+ -- Generate a function for chasing a dictionary constraint

11331135 cfun cn c syn all con

11341136 = do let cfn = UN ('@':'@':show cn ++ "#" ++ show con)

11351137 let mnames = take (length all) $ map (\x -> MN x "meth") [0..]

@@ -1150,8 +1152,10 @@ elabClass info syn doc fc constraints tn ps ds

11501152 addIBC (IBCInstance False conn' cfn)

11511153-- iputStrLn ("Added " ++ show (conn, cfn, ty))

11521154 return [PTy "" syn fc [] cfn ty,

1153− PClauses fc [Inlinable,TCGen] cfn [PClause fc cfn lhs [] rhs []]]

1155+ PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]

11541156

1157+ -- Generate a top level function which looks up a method in a given

1158+ -- dictionary (this is inlinable, always)

11551159 tfun cn c syn all (m, (doc, o, ty))

11561160 = do let ty' = insertConstraint c ty

11571161 let mnames = take (length all) $ map (\x -> MN x "meth") [0..]

@@ -1164,7 +1168,7 @@ elabClass info syn doc fc constraints tn ps ds

11641168 iLOG (show (m, ty', capp, margs))

11651169 iLOG (showImp True lhs ++ " = " ++ showImp True rhs)

11661170 return [PTy doc syn fc o m ty',

1167− PClauses fc [Inlinable,TCGen] m [PClause fc m lhs [] rhs []]]

1171+ PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]

11681172

11691173 getMArgs (PPi (Imp _ _ _) n ty sc) = IA : getMArgs sc

11701174 getMArgs (PPi (Exp _ _ _) n ty sc) = EA : getMArgs sc

@@ -1247,7 +1251,7 @@ elabInstance info syn fc cs n ps t expn ds

12471251 let lhs = PRef fc iname

12481252 let rhs = PApp fc (PRef fc (instanceName ci))

12491253 (map (pexp . mkMethApp) mtys)

1250− let idecls = [PClauses fc [Inlinable, TCGen] iname

1254+ let idecls = [PClauses fc [Dictionary] iname

12511255 [PClause fc iname lhs [] rhs wb]]

12521256 iLOG (show idecls)

12531257 mapM (elabDecl EAll info) idecls

@@ -1369,7 +1373,7 @@ elabInstance info syn fc cs n ps t expn ds

13691373 addIBC (IBCInstance False conn' cfn)

13701374 iputStrLn ("Added " ++ show (conn, cfn, ty) ++ "\n" ++ show (lhs, rhs))

13711375 return [PTy "" syn fc [] cfn ty,

1372− PClauses fc [Inlinable,TCGen] cfn [PClause fc cfn lhs [] rhs []]]

1376+ PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]

13731377-}

13741378

13751379decorateid decorate (PTy doc s f o n t) = PTy doc s f o (decorate n) t

src/Idris/IBC.hs+10−6

@@ -685,6 +685,12 @@ instance Binary CaseAlt where

685685 return (FnCase x1 x2 x3)

686686 _ -> error "Corrupted binary data for CaseAlt"

687687

688+instance Binary CaseInfo where

689+ put x@(CaseInfo x1 x2) = do put x1

690+ put x2

691+ get = do x1 <- get

692+ x2 <- get

693+ return (CaseInfo x1 x2)

688694

689695instance Binary Def where

690696 put x

@@ -698,7 +704,7 @@ instance Binary Def where

698704 put x2

699705 -- all primitives just get added at the start, don't write

700706 Operator x1 x2 x3 -> do return ()

701− CaseOp x1 x2 x3 x3a x4 x5 x6 x7 x8 ->

707+ CaseOp x1 x2 x3 x3a x4 x5 x6 x7 ->

702708 do putWord8 3

703709 put x1

704710 put x2

@@ -708,7 +714,6 @@ instance Binary Def where

708714 put x5

709715 put x6

710716 put x7

711− put x8

712717 get

713718 = do i <- getWord8

714719 case i of

@@ -730,8 +735,7 @@ instance Binary Def where

730735 x5 <- get

731736 x6 <- get

732737 x7 <- get

733− x8 <- get

734− return (CaseOp x1 x2 x3 [] x4 x5 x6 x7 x8)

738+ return (CaseOp x1 x2 x3 [] x4 x5 x6 x7)

735739 _ -> error "Corrupted binary data for Def"

736740

737741instance Binary Accessibility where

@@ -857,7 +861,7 @@ instance Binary FnOpt where

857861 = case x of

858862 Inlinable -> putWord8 0

859863 TotalFn -> putWord8 1

860− TCGen -> putWord8 2

864+ Dictionary -> putWord8 2

861865 AssertTotal -> putWord8 3

862866 Specialise x -> do putWord8 4

863867 put x

@@ -870,7 +874,7 @@ instance Binary FnOpt where

870874 case i of

871875 0 -> return Inlinable

872876 1 -> return TotalFn

873− 2 -> return TCGen

877+ 2 -> return Dictionary

874878 3 -> return AssertTotal

875879 4 -> do x <- get

876880 return (Specialise x)

src/Idris/Prover.hs+1−1

@@ -72,7 +72,7 @@ prove ctxt lit n ty

7272 OK _ -> return ()

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

7474 ptm' <- applyOpts ptm

75− updateContext (addCasedef n True False False True False

75+ updateContext (addCasedef n (CaseInfo True False) False False True False

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

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

7878 [([], P Ref n ty, ptm')] ty)