git.iko.soy/Idris-dev
on master help sign in
Change totality checking and inlining
7537cc4Edwin Brady
libs/prelude/Builtins.idr+2−1
compare with master
unifiedsplit
@@ -160,7 +160,8 @@ par : Lazy a -> a -- Doesn't actually do anything yet. Maybe a 'Par a' type
160par (Delay x) = x
160par (Delay x) = x
161
161
162||| Assert to the totality checker that y is always structurally smaller than
162||| Assert to the totality checker that y is always structurally smaller than
163−||| x (which is typically a pattern argument)
163+||| x (which is typically a pattern argument, and *must* be in normal form
164+||| for this to work)
164||| @ x the larger value (typically a pattern argument)
165||| @ x the larger value (typically a pattern argument)
165||| @ y the smaller value (typically an argument to a recursive call)
166||| @ y the smaller value (typically an argument to a recursive call)
166assert_smaller : (x : a) -> (y : b) -> b
167assert_smaller : (x : a) -> (y : b) -> b
libs/prelude/Prelude/Show.idr+2−2
@@ -46,7 +46,7 @@ interface Show ty where
46 ||| @ x the value to convert
46 ||| @ x the value to convert
47 partial
47 partial
48 show : (x : ty) -> String
48 show : (x : ty) -> String
49− show = showPrec Open
49+ show x = showPrec Open x -- Eta expand to help totality checker
50
50
51 ||| Convert a value to its `String` representation in a certain precedence
51 ||| Convert a value to its `String` representation in a certain precedence
52 ||| context.
52 ||| context.
@@ -63,7 +63,7 @@ interface Show ty where
63 ||| @ x the value to convert
63 ||| @ x the value to convert
64 partial
64 partial
65 showPrec : (d : Prec) -> (x : ty) -> String
65 showPrec : (d : Prec) -> (x : ty) -> String
66− showPrec _ = show
66+ showPrec _ x = show x
67
67
68||| Surround a `String` with parentheses depending on a condition.
68||| Surround a `String` with parentheses depending on a condition.
69|||
69|||
libs/prelude/Prelude/Strings.idr+2−2
@@ -328,7 +328,7 @@ toLower : String -> String
328toLower x with (strM x)
328toLower x with (strM x)
329 toLower "" | StrNil = ""
329 toLower "" | StrNil = ""
330 toLower (strCons c cs) | (StrCons c cs) =
330 toLower (strCons c cs) | (StrCons c cs) =
331− strCons (toLower c) (toLower (assert_smaller (strCons c cs) cs))
331+ strCons (toLower c) (toLower (assert_smaller (prim__strCons c cs) cs))
332
332
333||| Uppercases all characters in the string.
333||| Uppercases all characters in the string.
334|||
334|||
@@ -339,7 +339,7 @@ toUpper : String -> String
339toUpper x with (strM x)
339toUpper x with (strM x)
340 toUpper "" | StrNil = ""
340 toUpper "" | StrNil = ""
341 toUpper (strCons c cs) | (StrCons c cs) =
341 toUpper (strCons c cs) | (StrCons c cs) =
342− strCons (toUpper c) (toUpper (assert_smaller (strCons c cs) cs ))
342+ strCons (toUpper c) (toUpper (assert_smaller (prim__strCons c cs) cs ))
343
343
344--------------------------------------------------------------------------------
344--------------------------------------------------------------------------------
345-- Predicates
345-- Predicates
src/Idris/AbsSyntax.hs+7
@@ -208,6 +208,13 @@ clear_totcheck = do i <- getIState; putIState $ i { idris_totcheck = [] }
208setFlags :: Name -> [FnOpt] -> Idris ()
208setFlags :: Name -> [FnOpt] -> Idris ()
209setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }
209setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }
210
210
211+addFnOpt :: Name -> FnOpt -> Idris ()
212+addFnOpt n f = do i <- getIState
213+ let fls = case lookupCtxtExact n (idris_flags i) of
214+ Nothing -> []
215+ Just x -> x
216+ setFlags n (f : fls)
217+
211setFnInfo :: Name -> FnInfo -> Idris ()
218setFnInfo :: Name -> FnInfo -> Idris ()
212setFnInfo n fs = do i <- getIState; putIState $ i { idris_fninfo = addDef n fs (idris_fninfo i) }
219setFnInfo n fs = do i <- getIState; putIState $ i { idris_fninfo = addDef n fs (idris_fninfo i) }
213
220
src/Idris/AbsSyntaxTree.hs+9−2
@@ -361,7 +361,7 @@ data IBCWrite = IBCFix FixDecl
361 | IBCMetaInformation Name MetaInformation
361 | IBCMetaInformation Name MetaInformation
362 | IBCTotal Name Totality
362 | IBCTotal Name Totality
363 | IBCInjective Name Injectivity
363 | IBCInjective Name Injectivity
364− | IBCFlags Name [FnOpt]
364+ | IBCFlags Name
365 | IBCFnInfo Name FnInfo
365 | IBCFnInfo Name FnInfo
366 | IBCTrans Name (Term, Term)
366 | IBCTrans Name (Term, Term)
367 | IBCErrRev (Term, Term)
367 | IBCErrRev (Term, Term)
@@ -636,7 +636,8 @@ tacimpl t = TacImp [] Dynamic t
636
636
637data FnOpt = Inlinable -- ^ always evaluate when simplifying
637data FnOpt = Inlinable -- ^ always evaluate when simplifying
638 | TotalFn | PartialFn | CoveringFn
638 | TotalFn | PartialFn | CoveringFn
639+ | AllGuarded -- ^ all delayed arguments guaranteed guarded by constructors
639− | Coinductive | AssertTotal
640+ | AssertTotal
640
641
641 -- | interface dictionary, eval only when a function
642 -- | interface dictionary, eval only when a function
642 -- argument, and further evaluation results.
643 -- argument, and further evaluation results.
@@ -649,6 +650,12 @@ data FnOpt = Inlinable -- ^ always evaluate when simplifying
649 | ErrorReverse -- ^ attempt to reverse normalise before showing in error
650 | ErrorReverse -- ^ attempt to reverse normalise before showing in error
650 | Reflection -- ^ a reflecting function, compile-time only
651 | Reflection -- ^ a reflecting function, compile-time only
651 | Specialise [(Name, Maybe Int)] -- ^ specialise it, freeze these names
652 | Specialise [(Name, Maybe Int)] -- ^ specialise it, freeze these names
653+ | UnfoldIface Name [Name]
654+ -- ^ Unfold given interface name in the definition, the
655+ -- top level methods, and anything which has
656+ -- the interface name as an argument. This is to unfold
657+ -- things for termination checking, as interfaces will otherwise
658+ -- cause problems
652 | Constructor -- ^ Data constructor type
659 | Constructor -- ^ Data constructor type
653 | AutoHint -- ^ use in auto implicit search
660 | AutoHint -- ^ use in auto implicit search
654 | PEGenerated -- ^ generated by partial evaluator
661 | PEGenerated -- ^ generated by partial evaluator
src/Idris/Core/Elaborate.hs+1−1
@@ -697,7 +697,7 @@ apply_elab n args =
697 do ty <- get_type (Var n)
697 do ty <- get_type (Var n)
698 ctxt <- get_context
698 ctxt <- get_context
699 env <- get_env
699 env <- get_env
700− claims <- doClaims (hnf ctxt env ty) args []
700+ claims <- doClaims (normalise ctxt env ty) args []
701 prep_fill n (map fst claims)
701 prep_fill n (map fst claims)
702 let eclaims = sortBy (\ (_, x) (_,y) -> priOrder x y) claims
702 let eclaims = sortBy (\ (_, x) (_,y) -> priOrder x y) claims
703 elabClaims [] False claims
703 elabClaims [] False claims
src/Idris/Core/Evaluate.hs+64−42
@@ -11,7 +11,7 @@ Maintainer : The Idris Community.
11
11
12module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,
12module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,
13 normaliseAll, normaliseBlocking, toValue, quoteTerm,
13 normaliseAll, normaliseBlocking, toValue, quoteTerm,
14− rt_simplify, simplify, specialise, hnf, convEq, convEq',
14+ rt_simplify, simplify, specialise, unfold, convEq, convEq',
15 Def(..), CaseInfo(..), CaseDefs(..),
15 Def(..), CaseInfo(..), CaseDefs(..),
16 Accessibility(..), Injectivity, Totality(..), PReason(..), MetaInformation(..),
16 Accessibility(..), Injectivity, Totality(..), PReason(..), MetaInformation(..),
17 Context, initContext, ctxtAlist, next_tvar,
17 Context, initContext, ctxtAlist, next_tvar,
@@ -45,10 +45,10 @@ data EvalState = ES { limited :: [(Name, Int)],
45type Eval a = State EvalState a
45type Eval a = State EvalState a
46
46
47data EvalOpt = Spec
47data EvalOpt = Spec
48− | HNF
48+ | Simplify Bool -- ^ whether to expand lets or not
49− | Simplify
50 | AtREPL
49 | AtREPL
51 | RunTT
50 | RunTT
51+ | Unfold
52 deriving (Show, Eq)
52 deriving (Show, Eq)
53
53
54initEval = ES [] 0 False
54initEval = ES [] 0 False
@@ -131,10 +131,7 @@ specialise ctxt env limits t
131 (tm, limited st)
131 (tm, limited st)
132
132
133-- | Like normalise, but we only reduce functions that are marked as okay to
133-- | Like normalise, but we only reduce functions that are marked as okay to
134−-- inline (and probably shouldn't reduce lets?)
134+-- inline, and lets
135−-- 20130908: now only used to reduce for totality checking. Inlining should
136−-- be done elsewhere.
137−
138simplify :: Context -> Env -> TT Name -> TT Name
135simplify :: Context -> Env -> TT Name -> TT Name
139simplify ctxt env t
136simplify ctxt env t
140 = evalState (do val <- eval False ctxt [(sUN "lazy", 0),
137 = evalState (do val <- eval False ctxt [(sUN "lazy", 0),
@@ -146,7 +143,23 @@ simplify ctxt env t
146 (sUN "prim__syntactic_eq", 0),
143 (sUN "prim__syntactic_eq", 0),
147 (sUN "fork", 0)]
144 (sUN "fork", 0)]
148 (map finalEntry env) (finalise t)
145 (map finalEntry env) (finalise t)
149− [Simplify]
146+ [Simplify True]
147+ quote 0 val) initEval
148+
149+-- | Like simplify, but we only reduce functions that are marked as okay to
150+-- inline, and don't reduce lets
151+inline :: Context -> Env -> TT Name -> TT Name
152+inline ctxt env t
153+ = evalState (do val <- eval False ctxt [(sUN "lazy", 0),
154+ (sUN "force", 0),
155+ (sUN "Force", 0),
156+ (sUN "assert_smaller", 0),
157+ (sUN "assert_total", 0),
158+ (sUN "par", 0),
159+ (sUN "prim__syntactic_eq", 0),
160+ (sUN "fork", 0)]
161+ (map finalEntry env) (finalise t)
162+ [Simplify False]
150 quote 0 val) initEval
163 quote 0 val) initEval
151
164
152-- | Simplify for run-time (i.e. basic inlining)
165-- | Simplify for run-time (i.e. basic inlining)
@@ -162,12 +175,19 @@ rt_simplify ctxt env t
162 [RunTT]
175 [RunTT]
163 quote 0 val) initEval
176 quote 0 val) initEval
164
177
165−-- | Reduce a term to head normal form
178+-- | Unfold the given names in a term, the given number of times in a stack.
179+-- Preserves 'let'.
180+-- This is primarily to support inlining of the given names, and can also
181+-- help with partial evaluation by allowing a rescursive definition to be
182+-- unfolded once only.
183+-- Specifically used to unfold definitions using interfaces before going to
184+-- the totality checker (otherwise mutually recursive definitions in
185+-- implementations will not work...)
166−hnf :: Context -> Env -> TT Name -> TT Name
186+unfold :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name
167−hnf ctxt env t
187+unfold ctxt env ns t
168− = evalState (do val <- eval False ctxt []
188+ = evalState (do val <- eval False ctxt ns
169− (map finalEntry env)
189+ (map finalEntry env) (finalise t)
170− (finalise t) [HNF]
190+ [Unfold]
171 quote 0 val) initEval
191 quote 0 val) initEval
172
192
173
193
@@ -187,22 +207,25 @@ unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc
187unbindEnv env tm = error "Impossible case occurred: couldn't unbind env."
207unbindEnv env tm = error "Impossible case occurred: couldn't unbind env."
188
208
189usable :: Bool -- specialising
209usable :: Bool -- specialising
210+ -> Bool -- unfolding only
190 -> Int -- Reduction depth limit (when simplifying/at REPL)
211 -> Int -- Reduction depth limit (when simplifying/at REPL)
191 -> Name -> [(Name, Int)] -> Eval (Bool, [(Name, Int)])
212 -> Name -> [(Name, Int)] -> Eval (Bool, [(Name, Int)])
192-- usable _ _ ns@((MN 0 "STOP", _) : _) = return (False, ns)
213-- usable _ _ ns@((MN 0 "STOP", _) : _) = return (False, ns)
193−usable False depthlimit n [] = return (True, [])
214+usable False uf depthlimit n [] = return (True, [])
194−usable True depthlimit n ns
215+usable True uf depthlimit n ns
195 = do ES ls num b <- get
216 = do ES ls num b <- get
196 if b then return (False, ns)
217 if b then return (False, ns)
197 else case lookup n ls of
218 else case lookup n ls of
198 Just 0 -> return (False, ns)
219 Just 0 -> return (False, ns)
199 Just i -> return (True, ns)
220 Just i -> return (True, ns)
200 _ -> return (False, ns)
221 _ -> return (False, ns)
201−usable False depthlimit n ns
222+usable False uf depthlimit n ns
202 = case lookup n ns of
223 = case lookup n ns of
203 Just 0 -> return (False, ns)
224 Just 0 -> return (False, ns)
204 Just i -> return $ (True, (n, abs (i-1)) : filter (\ (n', _) -> n/=n') ns)
225 Just i -> return $ (True, (n, abs (i-1)) : filter (\ (n', _) -> n/=n') ns)
226+ _ -> return $ if uf
227+ then (False, ns)
205− _ -> return $ (True, (n, depthlimit) : filter (\ (n', _) -> n/=n') ns)
228+ else (True, (n, depthlimit) : filter (\ (n', _) -> n/=n') ns)
206
229
207
230
208fnCount :: Int -> Name -> Eval ()
231fnCount :: Int -> Name -> Eval ()
@@ -231,10 +254,11 @@ eval :: Bool -> Context -> [(Name, Int)] -> Env -> TT Name ->
231 [EvalOpt] -> Eval Value
254 [EvalOpt] -> Eval Value
232eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
255eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
233 spec = Spec `elem` opts
256 spec = Spec `elem` opts
234− simpl = Simplify `elem` opts
257+ simpl = Simplify True `elem` opts || Simplify False `elem` opts
258+ simpl_inline = Simplify False `elem` opts
235 runtime = RunTT `elem` opts
259 runtime = RunTT `elem` opts
236 atRepl = AtREPL `elem` opts
260 atRepl = AtREPL `elem` opts
237− hnf = HNF `elem` opts
261+ unfold = Unfold `elem` opts
238
262
239 -- returns 'True' if the function should block
263 -- returns 'True' if the function should block
240 -- normal evaluation should return false
264 -- normal evaluation should return false
@@ -243,7 +267,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
243 = if always then False
267 = if always then False
244 else not (inl || dict) || elem n stk
268 else not (inl || dict) || elem n stk
245 | simpl
269 | simpl
246− = (not (inl || dict) || elem n stk)
270+ = (not inl || elem n stk)
247 || (n == sUN "prim__syntactic_eq")
271 || (n == sUN "prim__syntactic_eq")
248 | otherwise = False
272 | otherwise = False
249
273
@@ -254,21 +278,21 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
254 ev ntimes stk top env (P _ n ty)
278 ev ntimes stk top env (P _ n ty)
255 | Just (Let t v) <- lookup n genv = ev ntimes stk top env v
279 | Just (Let t v) <- lookup n genv = ev ntimes stk top env v
256 ev ntimes_in stk top env (P Ref n ty)
280 ev ntimes_in stk top env (P Ref n ty)
257− | not top && hnf = liftM (VP Ref n) (ev ntimes stk top env ty)
258− | otherwise
259 = do let limit = if simpl then 100 else 10000
281 = do let limit = if simpl then 100 else 10000
260− (u, ntimes) <- usable spec limit n ntimes_in
282+ (u, ntimes) <- usable spec unfold limit n ntimes_in
261− let red = u && (tcReducible n ctxt || spec || atRepl || runtime
283+ let red = u && (tcReducible n ctxt || spec || atRepl
284+ || runtime || unfold
262 || sUN "assert_total" `elem` stk)
285 || sUN "assert_total" `elem` stk)
263 if red then
286 if red then
264− do let val = lookupDefAcc n (spec || atRepl || runtime) ctxt
287+ do let val = lookupDefAcc n (spec || unfold || atRepl || runtime) ctxt
265 case val of
288 case val of
266 [(Function _ tm, Public)] ->
289 [(Function _ tm, Public)] ->
267 ev ntimes (n:stk) True env tm
290 ev ntimes (n:stk) True env tm
268 [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty
291 [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty
269 return $ VP nt n vty
292 return $ VP nt n vty
270 [(CaseOp ci _ _ _ _ cd, acc)]
293 [(CaseOp ci _ _ _ _ cd, acc)]
294+ | (acc == Public || acc == Hidden) &&
271− | (acc == Public || acc == Hidden || sUN "assert_total" `elem` stk) &&
295+-- || sUN "assert_total" `elem` stk) &&
272 null (fst (cases_totcheck cd)) -> -- unoptimised version
296 null (fst (cases_totcheck cd)) -> -- unoptimised version
273 let (ns, tree) = getCases cd in
297 let (ns, tree) = getCases cd in
274 if blockSimplify ci n stk
298 if blockSimplify ci n stk
@@ -281,12 +305,12 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
281 _ -> liftM (VP Ref n) (ev ntimes stk top env ty)
305 _ -> liftM (VP Ref n) (ev ntimes stk top env ty)
282 else liftM (VP Ref n) (ev ntimes stk top env ty)
306 else liftM (VP Ref n) (ev ntimes stk top env ty)
283 ev ntimes stk top env (P nt n ty)
307 ev ntimes stk top env (P nt n ty)
284− = liftM (VP nt n) (ev ntimes stk top env ty)
308+ = liftM (VP nt n) (ev ntimes stk top env ty)
285 ev ntimes stk top env (V i)
309 ev ntimes stk top env (V i)
286− | i < length env && i >= 0 = return $ snd (env !! i)
310+ | i < length env && i >= 0 = return $ snd (env !! i)
287− | otherwise = return $ VV i
311+ | otherwise = return $ VV i
288 ev ntimes stk top env (Bind n (Let t v) sc)
312 ev ntimes stk top env (Bind n (Let t v) sc)
289− | not runtime || occurrences n sc < 2
313+ | (not (runtime || simpl_inline || unfold)) || occurrences n sc < 2
290 = do v' <- ev ntimes stk top env v --(finalise v)
314 = do v' <- ev ntimes stk top env v --(finalise v)
291 sc' <- ev ntimes stk top ((n, v') : env) sc
315 sc' <- ev ntimes stk top ((n, v') : env) sc
292 wknV (-1) sc'
316 wknV (-1) sc'
@@ -315,7 +339,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
315 -- block reduction immediately under codata (and not forced)
339 -- block reduction immediately under codata (and not forced)
316 ev ntimes stk top env
340 ev ntimes stk top env
317 (App _ (App _ (App _ d@(P _ (UN dly) _) l@(P _ (UN lco) _)) t) arg)
341 (App _ (App _ (App _ d@(P _ (UN dly) _) l@(P _ (UN lco) _)) t) arg)
318− | dly == txt "Delay" && lco == txt "Infinite" && not simpl
342+ | dly == txt "Delay" && lco == txt "Infinite" && not (unfold || simpl)
319 = do let (f, _) = unApply arg
343 = do let (f, _) = unApply arg
320 let ntimes' = case f of
344 let ntimes' = case f of
321 P _ fn _ -> (fn, 0) : ntimes
345 P _ fn _ -> (fn, 0) : ntimes
@@ -330,7 +354,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
330 -- Treat "assert_total" specially, as long as it's defined!
354 -- Treat "assert_total" specially, as long as it's defined!
331 ev ntimes stk top env (App _ (App _ (P _ n@(UN at) _) _) arg)
355 ev ntimes stk top env (App _ (App _ (P _ n@(UN at) _) _) arg)
332 | [(CaseOp _ _ _ _ _ _, _)] <- lookupDefAcc n (spec || atRepl || runtime) ctxt,
356 | [(CaseOp _ _ _ _ _ _, _)] <- lookupDefAcc n (spec || atRepl || runtime) ctxt,
333− at == txt "assert_total" && not simpl
357+ at == txt "assert_total" && not (simpl || unfold)
334 = ev ntimes (n : stk) top env arg
358 = ev ntimes (n : stk) top env arg
335 ev ntimes stk top env (App _ f a)
359 ev ntimes stk top env (App _ f a)
336 = do f' <- ev ntimes stk False env f
360 = do f' <- ev ntimes stk False env f
@@ -377,16 +401,13 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
377 app <- apply ntimes stk top env a' as
401 app <- apply ntimes stk top env a' as
378 wknV 1 app
402 wknV 1 app
379 apply ntimes_in stk top env f@(VP Ref n ty) args
403 apply ntimes_in stk top env f@(VP Ref n ty) args
380− | not top && hnf = case args of
381− [] -> return f
382− _ -> return $ unload env f args
383− | otherwise
384 = do let limit = if simpl then 100 else 10000
404 = do let limit = if simpl then 100 else 10000
385− (u, ntimes) <- usable spec limit n ntimes_in
405+ (u, ntimes) <- usable spec unfold limit n ntimes_in
386− let red = u && (tcReducible n ctxt || spec || atRepl || runtime
406+ let red = u && (tcReducible n ctxt || spec || atRepl
407+ || unfold || runtime
387 || sUN "assert_total" `elem` stk)
408 || sUN "assert_total" `elem` stk)
388 if red then
409 if red then
389− do let val = lookupDefAcc n (spec || atRepl || runtime) ctxt
410+ do let val = lookupDefAcc n (spec || unfold || atRepl || runtime) ctxt
390 case val of
411 case val of
391 [(CaseOp ci _ _ _ _ cd, acc)]
412 [(CaseOp ci _ _ _ _ cd, acc)]
392 | acc == Public || acc == Hidden ->
413 | acc == Public || acc == Hidden ->
@@ -975,7 +996,8 @@ simplifyCasedef n ei uctxt
975 pdef = map debind ps_in'
996 pdef = map debind ps_in'
976 CaseDef args sc _ <- simpleCase False (STerm Erased) False CompileTime emptyFC [] atys pdef ei
997 CaseDef args sc _ <- simpleCase False (STerm Erased) False CompileTime emptyFC [] atys pdef ei
977 return $ addDef n (CaseOp ci
998 return $ addDef n (CaseOp ci
978− ty atys ps_in' ps (cd { cases_totcheck = (args, sc) }),
999+ ty atys ps_in' ps (cd { cases_totcheck = (args, sc),
1000+ cases_compiletime = (args, sc) }),
979 inj, acc, tot, metainf) ctxt
1001 inj, acc, tot, metainf) ctxt
980
1002
981 _ -> return ctxt
1003 _ -> return ctxt
@@ -989,7 +1011,7 @@ simplifyCasedef n ei uctxt
989 (vs, x', y')
1011 (vs, x', y')
990 debind (Left x) = let (vs, x') = depat [] x in
1012 debind (Left x) = let (vs, x') = depat [] x in
991 (vs, x', Impossible)
1013 (vs, x', Impossible)
992− simpl (Right (x, y)) = Right (x, simplify uctxt [] y)
1014+ simpl (Right (x, y)) = Right (x, y) -- inline uctxt [] y)
993 simpl t = t
1015 simpl t = t
994
1016
995addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) ->
1017addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) ->
src/Idris/Core/ProofState.hs+4−4
@@ -651,7 +651,7 @@ introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
651 Nothing -> x
651 Nothing -> x
652 let t' = case t of
652 let t' = case t of
653 x@(Bind y (Pi _ s _) _) -> x
653 x@(Bind y (Pi _ s _) _) -> x
654− _ -> hnf ctxt env t
654+ _ -> normalise ctxt env t
655 (tyv, tyt) <- lift $ check ctxt env ty
655 (tyv, tyt) <- lift $ check ctxt env ty
656-- ns <- lift $ unify ctxt env tyv t'
656-- ns <- lift $ unify ctxt env tyv t'
657 case t' of
657 case t' of
@@ -668,7 +668,7 @@ intro :: Maybe Name -> RunTactic
668intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
668intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
669 do let t' = case t of
669 do let t' = case t of
670 x@(Bind y (Pi _ s _) _) -> x
670 x@(Bind y (Pi _ s _) _) -> x
671− _ -> hnf ctxt env t
671+ _ -> normalise ctxt env t
672 case t' of
672 case t' of
673 Bind y (Pi _ s _) t ->
673 Bind y (Pi _ s _) t ->
674 let n = case mn of
674 let n = case mn of
@@ -825,7 +825,7 @@ patbind :: Name -> RunTactic
825patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
825patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
826 do let t' = case t of
826 do let t' = case t of
827 x@(Bind y (PVTy s) t) -> x
827 x@(Bind y (PVTy s) t) -> x
828− _ -> hnf ctxt env t
828+ _ -> normalise ctxt env t
829 case t' of
829 case t' of
830 Bind y (PVTy s) t -> let t' = updsubst y (P Bound n s) t in
830 Bind y (PVTy s) t -> let t' = updsubst y (P Bound n s) t in
831 return $ Bind n (PVar s) (Bind x (Hole t') (P Bound x t'))
831 return $ Bind n (PVar s) (Bind x (Hole t') (P Bound x t'))
@@ -839,7 +839,7 @@ compute ctxt env t = return t
839
839
840hnf_compute :: RunTactic
840hnf_compute :: RunTactic
841hnf_compute ctxt env (Bind x (Hole ty) sc) =
841hnf_compute ctxt env (Bind x (Hole ty) sc) =
842− do let ty' = hnf ctxt env ty in
842+ do let ty' = normalise ctxt env ty in
843-- trace ("HNF " ++ show (ty, ty')) $
843-- trace ("HNF " ++ show (ty, ty')) $
844 return $ Bind x (Hole ty') sc
844 return $ Bind x (Hole ty') sc
845hnf_compute ctxt env t = return t
845hnf_compute ctxt env t = return t
src/Idris/Core/Typecheck.hs+2−2
@@ -116,7 +116,7 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) Nothing env top wh
116 let fty' = case uniqueBinders (map fst env) (finalise fty) of
116 let fty' = case uniqueBinders (map fst env) (finalise fty) of
117 ty@(Bind x (Pi i s k) t) -> ty
117 ty@(Bind x (Pi i s k) t) -> ty
118 _ -> uniqueBinders (map fst env)
118 _ -> uniqueBinders (map fst env)
119− $ case hnf ctxt env fty of
119+ $ case normalise ctxt env fty of
120 ty@(Bind x (Pi i s k) t) -> ty
120 ty@(Bind x (Pi i s k) t) -> ty
121 _ -> normalise ctxt env fty
121 _ -> normalise ctxt env fty
122 case fty' of
122 case fty' of
@@ -138,7 +138,7 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) Nothing env top wh
138 let fty' = case uniqueBinders (map fst env) (finalise fty) of
138 let fty' = case uniqueBinders (map fst env) (finalise fty) of
139 ty@(Bind x (Pi i s k) t) -> ty
139 ty@(Bind x (Pi i s k) t) -> ty
140 _ -> uniqueBinders (map fst env)
140 _ -> uniqueBinders (map fst env)
141− $ case hnf ctxt env fty of
141+ $ case normalise ctxt env fty of
142 ty@(Bind x (Pi i s k) t) -> ty
142 ty@(Bind x (Pi i s k) t) -> ty
143 _ -> normalise ctxt env fty
143 _ -> normalise ctxt env fty
144 (av, aty) <- chk u Nothing env a
144 (av, aty) <- chk u Nothing env a
src/Idris/Coverage.hs+62−2
@@ -372,6 +372,58 @@ checkAllCovering fc done top n | not (n `elem` done)
372 x -> return () -- stop if total
372 x -> return () -- stop if total
373checkAllCovering _ _ _ _ = return ()
373checkAllCovering _ _ _ _ = return ()
374
374
375+-- | Check whether all 'Inf' arguments to the name end up guaranteed to be
376+-- guarded by constructors (conservatively... maybe this can do better later).
377+-- Essentially, all it does is check that every branch is a constructor application
378+-- with no other function applications.
379+--
380+-- If so, set the 'AllGuarded' flag which can be used by the productivity check
381+checkIfGuarded :: Name -> Idris ()
382+checkIfGuarded n
383+ = do i <- get
384+ let ctxt = tt_ctxt i
385+ case lookupDefExact n ctxt of
386+ Just (CaseOp _ ty _ _ _ cases) ->
387+ let gnames = fst (cases_compiletime cases) in
388+ if allGuarded gnames i (snd (cases_compiletime cases))
389+ then -- trace (show (n, gnames, ty, cases_compiletime cases)) $
390+ addFnOpt n AllGuarded
391+ else return ()
392+ _ -> return ()
393+ where
394+ guard n ist = isConName n (tt_ctxt ist) || guardFlag n ist
395+ guardFlag n ist = case lookupCtxtExact n (idris_flags ist) of
396+ Nothing -> False
397+ Just fs -> AllGuarded `elem` fs
398+
399+ -- Top level thing always needs to be a constructor application if
400+ -- the delayed things are going to be definitely guarded by this definition
401+ allGuarded names i (STerm t)
402+ | (P _ fn _, args) <- unApply t,
403+ guard fn i
404+ = and (map (guardedTerm names i) args)
405+ | otherwise = False
406+ allGuarded names i (ProjCase _ alts) = and (map (guardedAlt names i) alts)
407+ allGuarded names i (Case _ _ alts) = and (map (guardedAlt names i) alts)
408+ allGuarded names i _ = True
409+
410+ guardedTerm names i (P _ v _) = v `elem` names || guard v i
411+ guardedTerm names i (Bind n (Let t v) sc)
412+ = guardedTerm names i v && guardedTerm names i sc
413+ guardedTerm names i (Bind n b sc) = False
414+ guardedTerm names i ap@(App _ _ _)
415+ | (P _ fn _, args) <- unApply ap,
416+ guard fn i || fn `elem` names
417+ = and (map (guardedTerm names i) args)
418+ guardedTerm names i (App _ f a) = False
419+ guardedTerm names i tm = True
420+
421+ guardedAlt names i (ConCase _ _ _ t) = allGuarded names i t
422+ guardedAlt names i (FnCase _ _ t) = allGuarded names i t
423+ guardedAlt names i (ConstCase _ t) = allGuarded names i t
424+ guardedAlt names i (SucCase _ t) = allGuarded names i t
425+ guardedAlt names i (DefaultCase t) = allGuarded names i t
426+
375-- | Check if, in a given group of type declarations mut_ns, the
427-- | Check if, in a given group of type declarations mut_ns, the
376-- constructor cn : ty is strictly positive, and update the context
428-- constructor cn : ty is strictly positive, and update the context
377-- accordingly
429-- accordingly
@@ -605,7 +657,7 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where
605 = findCalls cases Delayed arg pvs pargs
657 = findCalls cases Delayed arg pvs pargs
606 | (P _ n _, args) <- unApply ap,
658 | (P _ n _, args) <- unApply ap,
607 Delayed <- guarded,
659 Delayed <- guarded,
608− isConName n (tt_ctxt ist)
660+ isConName n (tt_ctxt ist) || allGuarded n ist
609 = -- Still under a 'Delay' and constructor guarded, so check
661 = -- Still under a 'Delay' and constructor guarded, so check
610 -- just the arguments to the constructor, remaining Delayed
662 -- just the arguments to the constructor, remaining Delayed
611 concatMap (\x -> findCalls cases guarded x pvs pargs) args
663 concatMap (\x -> findCalls cases guarded x pvs pargs) args
@@ -637,6 +689,7 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where
637 = let nguarded = case guarded of
689 = let nguarded = case guarded of
638 Unguarded -> Unguarded
690 Unguarded -> Unguarded
639 x -> if isConName n (tt_ctxt ist)
691 x -> if isConName n (tt_ctxt ist)
692+ || allGuarded n ist
640 then Guarded
693 then Guarded
641 else Unguarded in
694 else Unguarded in
642 mkChange n args pargs ++
695 mkChange n args pargs ++
@@ -647,7 +700,10 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where
647 = findCalls cases Unguarded f pvs pargs ++ findCalls cases Unguarded a pvs pargs
700 = findCalls cases Unguarded f pvs pargs ++ findCalls cases Unguarded a pvs pargs
648 findCalls cases guarded (Bind n (Let t v) e) pvs pargs
701 findCalls cases guarded (Bind n (Let t v) e) pvs pargs
649 = findCalls cases Unguarded t pvs pargs ++
702 = findCalls cases Unguarded t pvs pargs ++
650− findCalls cases Unguarded v pvs pargs ++ findCalls cases guarded e (n : pvs) pargs
703+ findCalls cases Unguarded v pvs pargs ++
704+ -- Substitute in the scope since this might reveal some useful
705+ -- structure
706+ findCalls cases guarded (substV v e) pvs pargs
651 findCalls cases guarded (Bind n t e) pvs pargs
707 findCalls cases guarded (Bind n t e) pvs pargs
652 = findCalls cases Unguarded (binderTy t) pvs pargs ++
708 = findCalls cases Unguarded (binderTy t) pvs pargs ++
653 findCalls cases guarded e (n : pvs) pargs
709 findCalls cases guarded e (n : pvs) pargs
@@ -757,6 +813,10 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where
757 patvars (Bind x (PVar _) sc) = x : patvars sc
813 patvars (Bind x (PVar _) sc) = x : patvars sc
758 patvars _ = []
814 patvars _ = []
759
815
816+ allGuarded n ist = case lookupCtxtExact n (idris_flags ist) of
817+ Nothing -> False
818+ Just fs -> AllGuarded `elem` fs
819+
760checkSizeChange :: Name -> Idris Totality
820checkSizeChange :: Name -> Idris Totality
761checkSizeChange n = do
821checkSizeChange n = do
762 ist <- getIState
822 ist <- getIState
src/Idris/Elab/Clause.hs+83−7
@@ -277,6 +277,10 @@ elabClauses info' fc opts n_in cs =
277 -- all called functions, and fail if any of them are also
277 -- all called functions, and fail if any of them are also
278 -- 'Partial NotCovering'
278 -- 'Partial NotCovering'
279 when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n
279 when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n
280+ -- Add the 'AllGuarded' flag if it's guaranteed that every
281+ -- 'Inf' argument will be guarded by constructors in the result
282+ -- (allows productivity check to go under this function)
283+ checkIfGuarded n
280 where
284 where
281 noMatch i cs tm = all (\x -> case trim_matchClause i (delab' i x True True) tm of
285 noMatch i cs tm = all (\x -> case trim_matchClause i (delab' i x True True) tm of
282 Right _ -> False
286 Right _ -> False
@@ -546,6 +550,34 @@ findUnique ctxt env (Bind n b sc)
546 else findUnique ctxt ((n, b) : env) sc
550 else findUnique ctxt ((n, b) : env) sc
547findUnique _ _ _ = []
551findUnique _ _ _ = []
548
552
553+getUnfolds (UnfoldIface n ns : _) = Just (n, ns)
554+getUnfolds (_ : xs) = getUnfolds xs
555+getUnfolds [] = Nothing
556+
557+-- Unfold the given name, interface methdods, and any function which uses it as
558+-- an argument directly. This is specifically for finding applications of
559+-- interface dictionaries and inlining them both for totality checking and for
560+-- a small performance gain.
561+getNamesToUnfold :: Name -> [Name] -> Term -> [Name]
562+getNamesToUnfold iname ms tm = nub $ iname : getNames Nothing tm ++ ms
563+ where
564+ getNames under fn@(App _ _ _)
565+ | (f, args) <- unApply fn
566+ = let under' = case f of
567+ P _ fn _ -> Just fn
568+ _ -> Nothing
569+ in
570+ getNames under f ++ concatMap (getNames under') args
571+ getNames (Just under) (P _ ref _)
572+ = if ref == iname then [under] else []
573+ getNames under (Bind n (Let t v) sc)
574+ = getNames Nothing t ++
575+ getNames Nothing v ++
576+ getNames Nothing sc
577+ getNames under (Bind n b sc) = getNames Nothing (binderTy b) ++
578+ getNames Nothing sc
579+ getNames _ _ = []
580+
549-- | Return the elaborated LHS/RHS, and the original LHS with implicits added
581-- | Return the elaborated LHS/RHS, and the original LHS with implicits added
550elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->
582elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->
551 Idris (Either Term (Term, Term), PTerm)
583 Idris (Either Term (Term, Term), PTerm)
@@ -684,7 +716,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
684 logElab 2 $ "RHS: " ++ show (map fst newargs_all) ++ " " ++ showTmImpls rhs
716 logElab 2 $ "RHS: " ++ show (map fst newargs_all) ++ " " ++ showTmImpls rhs
685 ctxt <- getContext -- new context with where block added
717 ctxt <- getContext -- new context with where block added
686 logElab 5 "STARTING CHECK"
718 logElab 5 "STARTING CHECK"
687− ((rhs', defer, holes, is, probs, ctxt', newDecls, highlights, newGName), _) <-
719+ ((rhsElab, defer, holes, is, probs, ctxt', newDecls, highlights, newGName), _) <-
688 tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patRHS") clhsty initEState
720 tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patRHS") clhsty initEState
689 (do pbinds ist lhs_tm
721 (do pbinds ist lhs_tm
690 -- proof search can use explicitly written names
722 -- proof search can use explicitly written names
@@ -713,7 +745,20 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
713 when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)
745 when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)
714
746
715 logElab 5 "DONE CHECK"
747 logElab 5 "DONE CHECK"
716− logElab 4 $ "---> " ++ show rhs'
748+ logElab 3 $ "---> " ++ show rhsElab
749+ ctxt <- getContext
750+
751+ let rhs' = case getUnfolds opts of
752+ Just (n, ms) ->
753+ let ns = getNamesToUnfold n ms rhsElab in
754+ unfold ctxt [] (map (\n -> (n, 1)) ns) rhsElab
755+ _ -> rhsElab
756+
757+ when (not (null (getUnfolds opts))) $
758+ logElab 1 $ "----- " ++ show (getUnfolds opts) ++
759+ "\nUnfolded " ++ show rhsElab ++ "\n" ++
760+ "to " ++ show rhs'
761+
717 when (not (null defer)) $ logElab 1 $ "DEFERRED " ++
762 when (not (null defer)) $ logElab 1 $ "DEFERRED " ++
718 show (map (\ (n, (_,_,t,_)) -> (n, t)) defer)
763 show (map (\ (n, (_,_,t,_)) -> (n, t)) defer)
719
764
@@ -880,7 +925,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
880 let wval = rhs_trans info $ addImplBound i (map fst bargs) wval_in
925 let wval = rhs_trans info $ addImplBound i (map fst bargs) wval_in
881 logElab 5 ("Checking " ++ showTmImpls wval)
926 logElab 5 ("Checking " ++ showTmImpls wval)
882 -- Elaborate wval in this context
927 -- Elaborate wval in this context
883− ((wval', defer, is, ctxt', newDecls, highlights, newGName), _) <-
928+ ((wvalElab, defer, is, ctxt', newDecls, highlights, newGName), _) <-
884 tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "withRHS")
929 tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "withRHS")
885 (bindTyArgs PVTy bargs infP) initEState
930 (bindTyArgs PVTy bargs infP) initEState
886 (do pbinds i lhs_tm
931 (do pbinds i lhs_tm
@@ -902,7 +947,20 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
902 let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'
947 let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'
903 addDeferred def''
948 addDeferred def''
904 mapM_ (elabCaseBlock info opts) is
949 mapM_ (elabCaseBlock info opts) is
950+
951+ let wval' = case getUnfolds opts of
952+ Just (n, ms) ->
953+ let ns = getNamesToUnfold n ms wvalElab in
954+ unfold ctxt [] (map (\n -> (n, 1)) ns) wvalElab
955+ _ -> wvalElab
956+
905 logElab 5 ("Checked wval " ++ show wval')
957 logElab 5 ("Checked wval " ++ show wval')
958+
959+ when (not (null (getUnfolds opts))) $
960+ logElab 1 $ "----- " ++ show (getUnfolds opts) ++
961+ "\nUnfolded wval " ++ show wvalElab ++ "\n" ++
962+ "to " ++ show wval'
963+
906
964
907 ctxt <- getContext
965 ctxt <- getContext
908 (cwval, cwvalty) <- recheckC (constraintNS info) fc id [] (getInferTerm wval')
966 (cwval, cwvalty) <- recheckC (constraintNS info) fc id [] (getInferTerm wval')
@@ -973,9 +1031,13 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
973 wb <- mapM (mkAuxC mpn wname lhs (map fst bargs_pre) (map fst bargs_post))
1031 wb <- mapM (mkAuxC mpn wname lhs (map fst bargs_pre) (map fst bargs_post))
974 withblock
1032 withblock
975 logElab 3 ("with block " ++ show wb)
1033 logElab 3 ("with block " ++ show wb)
976− -- propagate totality assertion to the new definitions
1034+ -- propagate totality assertion and unfold flags to the new definitions
1035+ let uflags = case getUnfolds opts of
1036+ Just (n, ns) -> [UnfoldIface n ns]
1037+ _ -> []
977− setFlags wname [Inlinable]
1038+ setFlags wname ([Inlinable] ++ uflags)
1039+ when (AssertTotal `elem` opts) $
978− when (AssertTotal `elem` opts) $ setFlags wname [Inlinable, AssertTotal]
1040+ setFlags wname ([Inlinable, AssertTotal] ++ uflags)
979 i <- getIState
1041 i <- getIState
980 let rhstrans' = updateWithTerm i mpn wname lhs (map fst bargs_pre) (map fst (bargs_post))
1042 let rhstrans' = updateWithTerm i mpn wname lhs (map fst bargs_pre) (map fst (bargs_post))
981 . rhs_trans info
1043 . rhs_trans info
@@ -995,7 +1057,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
995 logElab 5 ("New RHS " ++ showTmImpls rhs)
1057 logElab 5 ("New RHS " ++ showTmImpls rhs)
996 ctxt <- getContext -- New context with block added
1058 ctxt <- getContext -- New context with block added
997 i <- getIState
1059 i <- getIState
998− ((rhs', defer, is, ctxt', newDecls, highlights, newGName), _) <-
1060+ ((rhsElab, defer, is, ctxt', newDecls, highlights, newGName), _) <-
999 tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "wpatRHS") clhsty initEState
1061 tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "wpatRHS") clhsty initEState
1000 (do pbinds i lhs_tm
1062 (do pbinds i lhs_tm
1001 setNextName
1063 setNextName
@@ -1005,9 +1067,23 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
1005 tt <- get_term
1067 tt <- get_term
1006 return (tt, d, is, ctxt', newDecls, highlights, newGName))
1068 return (tt, d, is, ctxt', newDecls, highlights, newGName))
1007 setContext ctxt'
1069 setContext ctxt'
1070+
1008 processTacticDecls info newDecls
1071 processTacticDecls info newDecls
1009 sendHighlighting highlights
1072 sendHighlighting highlights
1010 updateIState $ \i -> i { idris_name = newGName }
1073 updateIState $ \i -> i { idris_name = newGName }
1074+
1075+ ctxt <- getContext
1076+ let rhs' = case getUnfolds opts of
1077+ Just (n, ms) ->
1078+ let ns = getNamesToUnfold n ms rhsElab in
1079+ unfold ctxt [] (map (\n -> (n, 1)) ns) rhsElab
1080+ _ -> rhsElab
1081+
1082+ when (not (null (getUnfolds opts))) $
1083+ logElab 3 $ "----- " ++ show (getUnfolds opts) ++
1084+ "\nUnfolded with RHS " ++ show rhsElab ++ "\n" ++
1085+ "to " ++ show rhs'
1086+
1011
1087
1012 def' <- checkDef info fc iderr True defer
1088 def' <- checkDef info fc iderr True defer
1013 let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'
1089 let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'
src/Idris/Elab/Implementation.hs+10−1
@@ -148,11 +148,14 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex
148 (decorate ns iname n,
148 (decorate ns iname n,
149 op, coninsert cs pextra t', t'))
149 op, coninsert cs pextra t', t'))
150 (interface_methods ci)
150 (interface_methods ci)
151+
151 logElab 5 (show (mtys, (iimpps ++ ips)))
152 logElab 5 (show (mtys, (iimpps ++ ips)))
152 logElab 5 ("Before defaults: " ++ show ds ++ "\n" ++ show (map fst (interface_methods ci)))
153 logElab 5 ("Before defaults: " ++ show ds ++ "\n" ++ show (map fst (interface_methods ci)))
153 let ds_defs = insertDefaults ist iname (interface_defaults ci) ns ds
154 let ds_defs = insertDefaults ist iname (interface_defaults ci) ns ds
154 logElab 3 ("After defaults: " ++ show ds_defs ++ "\n")
155 logElab 3 ("After defaults: " ++ show ds_defs ++ "\n")
156+
157+ let ds' = map (addUnfold iname (map fst (interface_methods ci))) $
155− let ds' = reorderDefs (map fst (interface_methods ci)) ds_defs
158+ reorderDefs (map fst (interface_methods ci)) ds_defs
156 logElab 1 ("Reordered: " ++ show ds' ++ "\n")
159 logElab 1 ("Reordered: " ++ show ds' ++ "\n")
157
160
158 mapM_ (warnMissing ds' ns iname) (map fst (interface_methods ci))
161 mapM_ (warnMissing ds' ns iname) (map fst (interface_methods ci))
@@ -220,6 +223,12 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex
220 [PConstant NoFC (AType (ATInt ITNative))] -> True
223 [PConstant NoFC (AType (ATInt ITNative))] -> True
221 _ -> False
224 _ -> False
222
225
226+ addUnfold iname ms (PTy doc docs syn fc opts n fc' tm)
227+ = PTy doc docs syn fc (UnfoldIface iname ms : opts) n fc' tm
228+ addUnfold iname ms (PClauses fc opts n cs)
229+ = PClauses fc (UnfoldIface iname ms : opts) n cs
230+ addUnfold iname ms dec = dec
231+
223 mkiname n' ns ps' expn' =
232 mkiname n' ns ps' expn' =
224 case expn' of
233 case expn' of
225 Nothing -> case ns of
234 Nothing -> case ns of
src/Idris/Elab/Term.hs+4−4
@@ -387,7 +387,7 @@ elab ist info emode opts fn tm
387 highlightSource fc' (AnnConst c)
387 highlightSource fc' (AnnConst c)
388 elab' ina fc (PQuote r) = do fill r; solve
388 elab' ina fc (PQuote r) = do fill r; solve
389 elab' ina _ (PTrue fc _) =
389 elab' ina _ (PTrue fc _) =
390− do hnf_compute
390+ do compute
391 g <- goal
391 g <- goal
392 case g of
392 case g of
393 TType _ -> elab' ina (Just fc) (PRef fc [] unitTy)
393 TType _ -> elab' ina (Just fc) (PRef fc [] unitTy)
@@ -421,7 +421,7 @@ elab ist info emode opts fn tm
421 pexp l, pexp r]))
421 pexp l, pexp r]))
422
422
423 elab' ina _ (PPair fc hls _ l r)
423 elab' ina _ (PPair fc hls _ l r)
424− = do hnf_compute
424+ = do compute
425 g <- goal
425 g <- goal
426 let (tc, _) = unApply g
426 let (tc, _) = unApply g
427 case g of
427 case g of
@@ -444,7 +444,7 @@ elab ist info emode opts fn tm
444 IsType -> asType
444 IsType -> asType
445 IsTerm -> asValue
445 IsTerm -> asValue
446 TypeOrTerm ->
446 TypeOrTerm ->
447− do hnf_compute
447+ do compute
448 g <- goal
448 g <- goal
449 case g of
449 case g of
450 TType _ -> asType
450 TType _ -> asType
@@ -2634,7 +2634,7 @@ runTac autoSolve ist perhapsFC fn tac
2634 (value, _) <- get_type_val (Var letn)
2634 (value, _) <- get_type_val (Var letn)
2635 ctxt <- get_context
2635 ctxt <- get_context
2636 env <- get_env
2636 env <- get_env
2637− let value' = hnf ctxt env value
2637+ let value' = normalise ctxt env value
2638 runTac autoSolve ist perhapsFC fn (Exact $ PQuote (reflect value'))
2638 runTac autoSolve ist perhapsFC fn (Exact $ PQuote (reflect value'))
2639 runT (Fill v) = do attack -- let x = fill x in ...
2639 runT (Fill v) = do attack -- let x = fill x in ...
2640 tyn <- getNameFrom (sMN 0 "letty")
2640 tyn <- getNameFrom (sMN 0 "letty")
src/Idris/Elab/Type.hs+1−1
@@ -210,7 +210,7 @@ elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (par
210 return (n, d')) argDocs
210 return (n, d')) argDocs
211 addDocStr n doc' argDocs'
211 addDocStr n doc' argDocs'
212 addIBC (IBCDoc n)
212 addIBC (IBCDoc n)
213− addIBC (IBCFlags n opts')
213+ addIBC (IBCFlags n)
214 fputState (opt_inaccessible . ist_optimisation n) inacc
214 fputState (opt_inaccessible . ist_optimisation n) inacc
215 addIBC (IBCOpt n)
215 addIBC (IBCOpt n)
216 when (Implicit `elem` opts') $ do addCoercion n
216 when (Implicit `elem` opts') $ do addCoercion n
src/Idris/IBC.hs+13−4
@@ -47,7 +47,7 @@ import System.Directory
47import System.FilePath
47import System.FilePath
48
48
49ibcVersion :: Word16
49ibcVersion :: Word16
50−ibcVersion = 151
50+ibcVersion = 152
51
51
52-- | When IBC is being loaded - we'll load different things (and omit
52-- | When IBC is being loaded - we'll load different things (and omit
53-- different structures/definitions) depending on which phase we're in.
53-- different structures/definitions) depending on which phase we're in.
@@ -313,7 +313,10 @@ ibc i (IBCCG n) f = case lookupCtxtExact n (idris_callgraph i) of
313 _ -> ifail "IBC write failed"
313 _ -> ifail "IBC write failed"
314ibc i (IBCCoercion n) f = return f { ibc_coercions = n : ibc_coercions f }
314ibc i (IBCCoercion n) f = return f { ibc_coercions = n : ibc_coercions f }
315ibc i (IBCAccess n a) f = return f { ibc_access = (n,a) : ibc_access f }
315ibc i (IBCAccess n a) f = return f { ibc_access = (n,a) : ibc_access f }
316+ibc i (IBCFlags n) f
317+ = case lookupCtxtExact n (idris_flags i) of
316−ibc i (IBCFlags n a) f = return f { ibc_flags = (n,a) : ibc_flags f }
318+ Just a -> return f { ibc_flags = (n,a): ibc_flags f }
319+ _ -> ifail "IBC write failed"
317ibc i (IBCFnInfo n a) f = return f { ibc_fninfo = (n,a) : ibc_fninfo f }
320ibc i (IBCFnInfo n a) f = return f { ibc_fninfo = (n,a) : ibc_fninfo f }
318ibc i (IBCTotal n a) f = return f { ibc_total = (n,a) : ibc_total f }
321ibc i (IBCTotal n a) f = return f { ibc_total = (n,a) : ibc_total f }
319ibc i (IBCInjective n a) f = return f { ibc_injective = (n,a) : ibc_injective f }
322ibc i (IBCInjective n a) f = return f { ibc_injective = (n,a) : ibc_injective f }
@@ -1208,7 +1211,7 @@ instance Binary FnOpt where
1208 AssertTotal -> putWord8 3
1211 AssertTotal -> putWord8 3
1209 Specialise x -> do putWord8 4
1212 Specialise x -> do putWord8 4
1210 put x
1213 put x
1211− Coinductive -> putWord8 5
1214+ AllGuarded -> putWord8 5
1212 PartialFn -> putWord8 6
1215 PartialFn -> putWord8 6
1213 Implicit -> putWord8 7
1216 Implicit -> putWord8 7
1214 Reflection -> putWord8 8
1217 Reflection -> putWord8 8
@@ -1223,6 +1226,9 @@ instance Binary FnOpt where
1223 PEGenerated -> putWord8 16
1226 PEGenerated -> putWord8 16
1224 StaticFn -> putWord8 17
1227 StaticFn -> putWord8 17
1225 OverlappingDictionary -> putWord8 18
1228 OverlappingDictionary -> putWord8 18
1229+ UnfoldIface x ns -> do putWord8 19
1230+ put x
1231+ put ns
1226 get
1232 get
1227 = do i <- getWord8
1233 = do i <- getWord8
1228 case i of
1234 case i of
@@ -1232,7 +1238,7 @@ instance Binary FnOpt where
1232 3 -> return AssertTotal
1238 3 -> return AssertTotal
1233 4 -> do x <- get
1239 4 -> do x <- get
1234 return (Specialise x)
1240 return (Specialise x)
1235− 5 -> return Coinductive
1241+ 5 -> return AllGuarded
1236 6 -> return PartialFn
1242 6 -> return PartialFn
1237 7 -> return Implicit
1243 7 -> return Implicit
1238 8 -> return Reflection
1244 8 -> return Reflection
@@ -1247,6 +1253,9 @@ instance Binary FnOpt where
1247 16 -> return PEGenerated
1253 16 -> return PEGenerated
1248 17 -> return StaticFn
1254 17 -> return StaticFn
1249 18 -> return OverlappingDictionary
1255 18 -> return OverlappingDictionary
1256+ 19 -> do x <- get
1257+ ns <- get
1258+ return (UnfoldIface x ns)
1250 _ -> error "Corrupted binary data for FnOpt"
1259 _ -> error "Corrupted binary data for FnOpt"
1251
1260
1252instance Binary Fixity where
1261instance Binary Fixity where
test/totality013/expected+2−3
@@ -1,4 +1,3 @@
1totality013a.idr:5:3:
1totality013a.idr:5:3:
2−Main.foo is possibly not total due to recursive path Main.mtot --> Main.mtot --> Main.mtot --> Main.mtot
2+Main.foo is possibly not total due to recursive path Main.foo --> Main.mtot --> Main.mtot --> Main.mtot
3−totality013a.idr:9:3:
4−Main.mtot is possibly not total due to recursive path Main.mtot --> Main.mtot --> Main.mtot
3+totality013a.idr:9:3:Main.mtot is possibly not total due to: Main.foo
test/totality015/totality015.idr+1−1
@@ -12,7 +12,7 @@ data ConsoleIO : Type -> Type where
12 Do : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b
12 Do : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b
13
13
14(>>=) : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b
14(>>=) : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b
15−(>>=) = Do
15+(>>=) = Do
16
16
17data Fuel = Dry | More (Lazy Fuel)
17data Fuel = Dry | More (Lazy Fuel)
18
18