git.iko.soy/Idris-dev
on master help sign in
Change evaluation of partial functions at REPL

To prevent infinite recursion at the REPL under binders, which results in a neverending display of a diverging term, the evaluator at the REPL will now block on a partial function when there is a free variable in the context. This means that you can still test partial functions at the REPL with canonical values, but if they are recursive and non-terminating under binders, you won't get infinite evaluation. Fixes #3535

commit4c4a07a17f87409786892f67c0b3c9b6ecabf1f7 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 9 Dec 2016, 14:18 (10 years ago) parent6d8bfbc
1 file changed+18−6
compare with master
unifiedsplit
src/Idris/Core/Evaluate.hs+18−6
src/Idris/Core/Evaluate.hs+18−6
@@ -72,6 +72,16 @@ data Value = VP NameType Name Value
7272-- | VLazy Env [Value] Term
7373 | VTmp Int
7474
75+canonical :: Value -> Bool
76+canonical (VP (DCon _ _ _) _ _) = True
77+canonical (VApp f a) = canonical f
78+canonical (VConstant _) = True
79+canonical (VType _) = True
80+canonical (VUType _) = True
81+canonical VErased = True
82+canonical _ = False
83+
84+
7585instance Show Value where
7686 show x = show $ evalState (quote 100 x) initEval
7787
@@ -254,6 +264,8 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
254264 atRepl = AtREPL `elem` opts
255265 unfold = Unfold `elem` opts
256266
267+ noFree = all canonical . map snd
268+
257269 -- returns 'True' if the function should block
258270 -- normal evaluation should return false
259271 blockSimplify (CaseInfo inl always dict) n stk
@@ -274,11 +286,11 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
274286 ev ntimes_in stk top env (P Ref n ty)
275287 = do let limit = if simpl then 100 else 10000
276288 (u, ntimes) <- usable spec unfold limit n ntimes_in
277− let red = u && (tcReducible n ctxt || spec || atRepl
289+ let red = u && (tcReducible n ctxt || spec || (atRepl && noFree env)
278290 || runtime || unfold
279291 || sUN "assert_total" `elem` stk)
280292 if red then
281− do let val = lookupDefAccExact n (spec || unfold || atRepl || runtime) ctxt
293+ do let val = lookupDefAccExact n (spec || unfold || (atRepl && noFree env) || runtime) ctxt
282294 case val of
283295 Just (Function _ tm, Public) ->
284296 ev ntimes (n:stk) True env tm
@@ -347,7 +359,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
347359 evApply ntimes' stk top env [l',t',arg'] d'
348360 -- Treat "assert_total" specially, as long as it's defined!
349361 ev ntimes stk top env (App _ (App _ (P _ n@(UN at) _) _) arg)
350− | Just (CaseOp _ _ _ _ _ _, _) <- lookupDefAccExact n (spec || atRepl || runtime) ctxt,
362+ | Just (CaseOp _ _ _ _ _ _, _) <- lookupDefAccExact n (spec || (atRepl && noFree env)|| runtime) ctxt,
351363 at == txt "assert_total" && not (simpl || unfold)
352364 = ev ntimes (n : stk) top env arg
353365 ev ntimes stk top env (App _ f a)
@@ -376,7 +388,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
376388 = apply ntimes stk top env f args
377389
378390 reapply ntimes stk top env f@(VP Ref n ty) args
379− = let val = lookupDefAccExact n (spec || atRepl || runtime) ctxt in
391+ = let val = lookupDefAccExact n (spec || (atRepl && noFree env) || runtime) ctxt in
380392 case val of
381393 Just (CaseOp ci _ _ _ _ cd, acc) ->
382394 let (ns, tree) = getCases cd in
@@ -398,11 +410,11 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
398410 apply ntimes_in stk top env f@(VP Ref n ty) args
399411 = do let limit = if simpl then 100 else 10000
400412 (u, ntimes) <- usable spec unfold limit n ntimes_in
401− let red = u && (tcReducible n ctxt || spec || atRepl
413+ let red = u && (tcReducible n ctxt || spec || (atRepl && noFree env)
402414 || unfold || runtime
403415 || sUN "assert_total" `elem` stk)
404416 if red then
405− do let val = lookupDefAccExact n (spec || unfold || atRepl || runtime) ctxt
417+ do let val = lookupDefAccExact n (spec || unfold || (atRepl && noFree env) || runtime) ctxt
406418 case val of
407419 Just (CaseOp ci _ _ _ _ cd, acc)
408420 | acc == Public || acc == Hidden ->