d43a279 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Change TCGen flag to Dictionary, update evaluator accordingly

d43a279Edwin Brady13 years ago

src/Core/Evaluate.hs+42−27

compare with master

unifiedsplit

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

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

5 simplify, specialise, hnf, convEq, convEq',

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

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

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

7 Context, initContext, ctxtAlist, uconstraints, next_tvar,

8 Context, initContext, ctxtAlist, uconstraints, next_tvar,

8 addToCtxt, setAccess, setTotal, addCtxtDef, addTyDecl,

9 addToCtxt, setAccess, setTotal, addCtxtDef, addTyDecl,

9 addDatatype, addCasedef, simplifyCasedef, addOperator,

10 addDatatype, addCasedef, simplifyCasedef, addOperator,

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

25type Eval a = State EvalState a

26type Eval a = State EvalState a

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

28 deriving (Show, Eq)

33 deriving (Show, Eq)

30initEval = ES [] 0

35initEval = ES [] 0

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

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

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

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

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

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

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

98−simplify ctxt runtime env t

103+simplify ctxt alldicts env t

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

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

100 (UN "assert_smaller", 0),

105 (UN "assert_smaller", 0),

101 (UN "par", 0),

106 (UN "par", 0),

102 (UN "prim__syntactic_eq", 0),

107 (UN "prim__syntactic_eq", 0),

103 (UN "fork", 0)]

108 (UN "fork", 0)]

104 (map finalEntry env) (finalise t)

109 (map finalEntry env) (finalise t)

105− [Simplify runtime]

110+ [Simplify alldicts]

106 quote 0 val) initEval

111 quote 0 val) initEval

107

112

108-- | Reduce a term to head normal form

113-- | Reduce a term to head normal form

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

168 atRepl = AtREPL `elem` opts

173 atRepl = AtREPL `elem` opts

169 hnf = HNF `elem` opts

174 hnf = HNF `elem` opts

170

175

171− canSimplify inl inr n stk

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

177+ -- normal evaluation should return false

178+ blockSimplify (CaseInfo inl dict) n stk

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

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

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

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

174

181

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

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

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

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

185 ev ntimes (n:stk) True env tm

192 ev ntimes (n:stk) True env tm

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

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

187 return $ VP nt n vty

194 return $ VP nt n vty

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

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

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

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

190− if canSimplify inl inr n stk

197+ if blockSimplify ci n stk

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

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

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

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

193 case c of

200 case c of

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

260 if u then

267 if u then

261 do let val = lookupDefAcc n atRepl ctxt

268 do let val = lookupDefAcc n atRepl ctxt

262 case val of

269 case val of

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

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

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

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

265− if canSimplify inl inr n stk

272+ if blockSimplify ci n stk

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

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

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

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

268 case c of

275 case c of

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

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

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

471 [Function _ t] -> ev env t

478 [Function _ t] -> ev env t

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

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

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

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

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

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

475 case c of

482 case c of

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

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

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

500 app <- apply env sc' as

507 app <- apply env sc' as

501 wknH (-1) app

508 wknH (-1) app

502 apply env (HP Ref n ty) args

509 apply env (HP Ref n ty) args

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

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

504 = do c <- evCase env ns args tree

511 = do c <- evCase env ns args tree

505 case c of

512 case c of

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

644 _ -> return False

651 _ -> return False

645

652

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

661data Def = Function Type Term

668data Def = Function Type Term

662 | TyDecl NameType Type

669 | TyDecl NameType Type

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

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

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

671+ | CaseOp CaseInfo

665 Type

672 Type

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

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

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

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

668 [Name] SC -- Compile time case definition

675 [Name] SC -- Compile time case definition

669 [Name] SC -- Run time cae definitions

676 [Name] SC -- Run time cae definitions

677+

678+data CaseInfo = CaseInfo {

679+ case_inlinable :: Bool,

680+ tc_dictionary :: Bool

681+ }

682+

670{-!

683{-!

671deriving instance Binary Def

684deriving instance Binary Def

672!-}

685!-}

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

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

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

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

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

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

690 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')

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

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

680 show ns ++ " " ++ show sc ++ "\n" ++

693 show ns ++ " " ++ show sc ++ "\n" ++

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

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

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

793 addCons (tag+1) cons (addDef n

806 addCons (tag+1) cons (addDef n

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

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

795

808

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

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

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

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

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

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

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

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

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

800 Type -> Context -> Context

814 Type -> Context -> Context

815+addCasedef n ci@(CaseInfo alwaysInline tcdict)

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

816+ tcase covering reflect asserted ps_in ps psrt ty uctxt

802 = let ctxt = definitions uctxt

817 = let ctxt = definitions uctxt

803 access = case lookupDefAcc n False uctxt of

818 access = case lookupDefAcc n False uctxt of

804 [(_, acc)] -> acc

819 [(_, acc)] -> acc

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

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

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

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

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

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

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

809− let inl = alwaysInline

824+ let inl = alwaysInline || tcdict

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

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

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

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

812− addDef n (CaseOp inlc inlr

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

813 ty ps_in ps args sc args' sc',

828 ty ps_in ps args sc args' sc',

814 access, Unchecked) ctxt in

829 access, Unchecked) ctxt in

815 uctxt { definitions = ctxt' }

830 uctxt { definitions = ctxt' }

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

818simplifyCasedef n uctxt

833simplifyCasedef n uctxt

819 = let ctxt = definitions uctxt

834 = let ctxt = definitions uctxt

820 ctxt' = case lookupCtxt n ctxt of

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

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

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

824 let ps_in' = map simpl ps_in

839 let ps_in' = map simpl ps_in

825 pdef = map debind ps_in' in

840 pdef = map debind ps_in' in

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

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

827 OK (CaseDef args sc _) ->

842 OK (CaseDef args sc _) ->

828− addDef n (CaseOp inl inr

843+ addDef n (CaseOp ci

829 ty ps_in' ps args sc args' sc',

844 ty ps_in' ps args sc args' sc',

830 acc, tot) ctxt

845 acc, tot) ctxt

831 _ -> ctxt in

846 _ -> ctxt in

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

863 (Function ty _) -> return ty

878 (Function ty _) -> return ty

864 (TyDecl _ ty) -> return ty

879 (TyDecl _ ty) -> return ty

865 (Operator ty _ _) -> return ty

880 (Operator ty _ _) -> return ty

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

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

867

882

868isConName :: Name -> Context -> Bool

883isConName :: Name -> Context -> Bool

869isConName n ctxt

884isConName n ctxt

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

879 case tfst def of

894 case tfst def of

880 (Function _ _) -> return True

895 (Function _ _) -> return True

881 (Operator _ _ _) -> return True

896 (Operator _ _ _) -> return True

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

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

883 _ -> return False

898 _ -> return False

884

899

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

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

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

888 p <- case def of

903 p <- case def of

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

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

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

905 (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)

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

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

893 case snd p of

908 case snd p of

894 Hidden -> []

909 Hidden -> []

src/Core/Execute.hs+4−4

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

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

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

183 [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

185 doExec env ctxt tm

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

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

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

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

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

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

301 execApp' env ctxt r (drop arity args)

302 Nothing -> return (mkEApp f args)

303 else return (mkEApp f args)

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

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

305 do rhs <- doExec env ctxt tm

306 execApp' env ctxt rhs args

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

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

308 do res <- execCase env ctxt ns sc args

309 return $ fromMaybe (mkEApp f args) res

310 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

159

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

161 return (declArgs [] True n e)

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

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

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

163− return (declArgs [] inl n e)

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

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

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

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

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

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

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

src/Idris/AbsSyntaxTree.hs+8−2

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

330constraint = Constraint False Dynamic ""

331tacimpl t = TacImp False Dynamic t ""

332

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

333−data FnOpt = Inlinable | TotalFn | PartialFn

334+ | TotalFn | PartialFn

334− | Coinductive | AssertTotal | TCGen

335+ | Coinductive | AssertTotal

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

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

335 | Implicit -- implicit coercion

338 | Implicit -- implicit coercion

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

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

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

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

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

346inlinable :: FnOpts -> Bool

349inlinable :: FnOpts -> Bool

347inlinable = elem Inlinable

350inlinable = elem Inlinable

348

351

352+dictionary :: FnOpts -> Bool

353+dictionary = elem Dictionary

354+

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

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

350-- datatypes and typeclasses.

356-- datatypes and typeclasses.

351data PDecl' t

357data PDecl' t

src/Idris/Coverage.hs+2−2

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

303 t' <- case t of

304 Unchecked ->

305 case lookupDef n ctxt of

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

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

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

308 then return $ Total []

309 else calcTotality path fc n pats

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

367 ist <- getIState

368 case lookupCtxt n (idris_callgraph ist) of

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

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

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

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

372 ++ show pats ++ "\n" ++ show sc

373 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

521 -- question: CAFs in where blocks?

522 tclift $ tfail $ At fc (NoTypeDecl n)

523 [ty] -> return ty

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

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

525 (zip [0..] cs)

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

527 -- just do nothing

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

623 ist <- getIState

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

625 (idris_patdefs ist) })

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

626 case lookupTy n ctxt of

627 case lookupTy n ctxt of

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

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

628 tcase knowncovering

629 tcase knowncovering

629 reflect

630 reflect

630 (AssertTotal `elem` opts)

631 (AssertTotal `elem` opts)

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

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

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

637 i <- getIState

638 i <- getIState

638 case lookupDef n (tt_ctxt i) of

639 case lookupDef n (tt_ctxt i) of

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

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

640 do let calls = findCalls sc' scargs'

641 do let calls = findCalls sc' scargs'

641 let used = findUsedArgs sc' scargs'

642 let used = findUsedArgs sc' scargs'

642 -- let scg = buildSCG i sc scargs

643 -- let scg = buildSCG i sc scargs

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

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

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

1117 let ds = map (decorateid defaultdec)

1118 let ds = map (decorateid defaultdec)

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

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

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

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

1120 iLOG (show ds)

1121 iLOG (show ds)

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

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

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

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

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

1130 clause (PClauses _ _ _ _) = True

1131 clause (PClauses _ _ _ _) = True

1131 clause _ = False

1132 clause _ = False

1132

1133

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

1133 cfun cn c syn all con

1135 cfun cn c syn all con

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

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

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

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

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

1150 addIBC (IBCInstance False conn' cfn)

1152 addIBC (IBCInstance False conn' cfn)

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

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

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

1154 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 []]]

1154

1156

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

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

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

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

1156 = do let ty' = insertConstraint c ty

1160 = do let ty' = insertConstraint c ty

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

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

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

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

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

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

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

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

1170 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 []]]

1168

1172

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

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

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

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

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

1247 let lhs = PRef fc iname

1251 let lhs = PRef fc iname

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

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

1249 (map (pexp . mkMethApp) mtys)

1253 (map (pexp . mkMethApp) mtys)

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

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

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

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

1252 iLOG (show idecls)

1256 iLOG (show idecls)

1253 mapM (elabDecl EAll info) idecls

1257 mapM (elabDecl EAll info) idecls

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

1369 addIBC (IBCInstance False conn' cfn)

1373 addIBC (IBCInstance False conn' cfn)

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

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

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

1375 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 []]]

1373-}

1377-}

1374

1378

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

1379decorateid 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

685 return (FnCase x1 x2 x3)

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

687

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)

688

694

689instance Binary Def where

695instance Binary Def where

690 put x

696 put x

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

698 put x2

704 put x2

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

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

700 Operator x1 x2 x3 -> do return ()

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

702 do putWord8 3

708 do putWord8 3

703 put x1

709 put x1

704 put x2

710 put x2

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

708 put x5

714 put x5

709 put x6

715 put x6

710 put x7

716 put x7

711− put x8

712 get

717 get

713 = do i <- getWord8

718 = do i <- getWord8

714 case i of

719 case i of

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

730 x5 <- get

735 x5 <- get

731 x6 <- get

736 x6 <- get

732 x7 <- get

737 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)

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

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

736

740

737instance Binary Accessibility where

741instance Binary Accessibility where

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

857 = case x of

861 = case x of

858 Inlinable -> putWord8 0

862 Inlinable -> putWord8 0

859 TotalFn -> putWord8 1

863 TotalFn -> putWord8 1

860− TCGen -> putWord8 2

864+ Dictionary -> putWord8 2

861 AssertTotal -> putWord8 3

865 AssertTotal -> putWord8 3

862 Specialise x -> do putWord8 4

866 Specialise x -> do putWord8 4

863 put x

867 put x

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

870 case i of

874 case i of

871 0 -> return Inlinable

875 0 -> return Inlinable

872 1 -> return TotalFn

876 1 -> return TotalFn

873− 2 -> return TCGen

877+ 2 -> return Dictionary

874 3 -> return AssertTotal

878 3 -> return AssertTotal

875 4 -> do x <- get

879 4 -> do x <- get

876 return (Specialise x)

880 return (Specialise x)

src/Idris/Prover.hs+1−1

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

72 OK _ -> return ()

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

74 ptm' <- applyOpts ptm

75− updateContext (addCasedef n True False False True False

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

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

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

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