@@ -72,6 +72,16 @@ data Value = VP NameType Name Value
72-- | VLazy Env [Value] Term
72-- | VLazy Env [Value] Term
73 | VTmp Int
73 | VTmp Int
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
75instance Show Value where
85instance Show Value where
76 show x = show $ evalState (quote 100 x) initEval
86 show x = show $ evalState (quote 100 x) initEval
@@ -254,6 +264,8 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
254 atRepl = AtREPL `elem` opts
264 atRepl = AtREPL `elem` opts
255 unfold = Unfold `elem` opts
265 unfold = Unfold `elem` opts
267+ noFree = all canonical . map snd
257 -- returns 'True' if the function should block
269 -- returns 'True' if the function should block
258 -- normal evaluation should return false
270 -- normal evaluation should return false
259 blockSimplify (CaseInfo inl always dict) n stk
271 blockSimplify (CaseInfo inl always dict) n stk
@@ -274,11 +286,11 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
274 ev ntimes_in stk top env (P Ref n ty)
286 ev ntimes_in stk top env (P Ref n ty)
275 = do let limit = if simpl then 100 else 10000
287 = do let limit = if simpl then 100 else 10000
276 (u, ntimes) <- usable spec unfold limit n ntimes_in
288 (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)
278 || runtime || unfold
290 || runtime || unfold
279 || sUN "assert_total" `elem` stk)
291 || sUN "assert_total" `elem` stk)
280 if red then
292 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
282 case val of
294 case val of
283 Just (Function _ tm, Public) ->
295 Just (Function _ tm, Public) ->
284 ev ntimes (n:stk) True env tm
296 ev ntimes (n:stk) True env tm
@@ -347,7 +359,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
347 evApply ntimes' stk top env [l',t',arg'] d'
359 evApply ntimes' stk top env [l',t',arg'] d'
348 -- Treat "assert_total" specially, as long as it's defined!
360 -- Treat "assert_total" specially, as long as it's defined!
349 ev ntimes stk top env (App _ (App _ (P _ n@(UN at) _) _) arg)
361 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,
351 at == txt "assert_total" && not (simpl || unfold)
363 at == txt "assert_total" && not (simpl || unfold)
352 = ev ntimes (n : stk) top env arg
364 = ev ntimes (n : stk) top env arg
353 ev ntimes stk top env (App _ f a)
365 ev ntimes stk top env (App _ f a)
@@ -376,7 +388,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
376 = apply ntimes stk top env f args
388 = apply ntimes stk top env f args
378 reapply ntimes stk top env f@(VP Ref n ty) args
390 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
380 case val of
392 case val of
381 Just (CaseOp ci _ _ _ _ cd, acc) ->
393 Just (CaseOp ci _ _ _ _ cd, acc) ->
382 let (ns, tree) = getCases cd in
394 let (ns, tree) = getCases cd in
@@ -398,11 +410,11 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
398 apply ntimes_in stk top env f@(VP Ref n ty) args
410 apply ntimes_in stk top env f@(VP Ref n ty) args
399 = do let limit = if simpl then 100 else 10000
411 = do let limit = if simpl then 100 else 10000
400 (u, ntimes) <- usable spec unfold limit n ntimes_in
412 (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)
402 || unfold || runtime
414 || unfold || runtime
403 || sUN "assert_total" `elem` stk)
415 || sUN "assert_total" `elem` stk)
404 if red then
416 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
406 case val of
418 case val of
407 Just (CaseOp ci _ _ _ _ cd, acc)
419 Just (CaseOp ci _ _ _ _ cd, acc)
408 | acc == Public || acc == Hidden ->
420 | acc == Public || acc == Hidden ->