@@ -185,21 +185,22 @@ unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc
185unbindEnv env tm = error $ "Impossible case occurred: couldn't unbind env."
185unbindEnv env tm = error $ "Impossible case occurred: couldn't unbind env."
187usable :: Bool -- specialising
187usable :: Bool -- specialising
188+ -> Int -- Reduction depth limit (when simplifying/at REPL)
188 -> Name -> [(Name, Int)] -> Eval (Bool, [(Name, Int)])
189 -> Name -> [(Name, Int)] -> Eval (Bool, [(Name, Int)])
189-- usable _ _ ns@((MN 0 "STOP", _) : _) = return (False, ns)
190-- usable _ _ ns@((MN 0 "STOP", _) : _) = return (False, ns)
190−usable False n [] = return (True, [])
191+usable False depthlimit n [] = return (True, [])
191−usable True n ns
192+usable True depthlimit n ns
192 = do ES ls num b <- get
193 = do ES ls num b <- get
193 if b then return (False, ns)
194 if b then return (False, ns)
194 else case lookup n ls of
195 else case lookup n ls of
195 Just 0 -> return (False, ns)
196 Just 0 -> return (False, ns)
196 Just i -> return (True, ns)
197 Just i -> return (True, ns)
197 _ -> return (False, ns)
198 _ -> return (False, ns)
198−usable False n ns
199+usable False depthlimit n ns
199 = case lookup n ns of
200 = case lookup n ns of
200 Just 0 -> return (False, ns)
201 Just 0 -> return (False, ns)
201 Just i -> return $ (True, (n, abs (i-1)) : filter (\ (n', _) -> n/=n') ns)
202 Just i -> return $ (True, (n, abs (i-1)) : filter (\ (n', _) -> n/=n') ns)
202− _ -> return $ (True, (n, 1000000) : filter (\ (n', _) -> n/=n') ns)
203+ _ -> return $ (True, (n, depthlimit) : filter (\ (n', _) -> n/=n') ns)
205fnCount :: Int -> Name -> Eval ()
206fnCount :: Int -> Name -> Eval ()
@@ -253,7 +254,8 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
253 ev ntimes_in stk top env (P Ref n ty)
254 ev ntimes_in stk top env (P Ref n ty)
254 | not top && hnf = liftM (VP Ref n) (ev ntimes stk top env ty)
255 | not top && hnf = liftM (VP Ref n) (ev ntimes stk top env ty)
255 | otherwise
256 | otherwise
257+ = do let limit = if simpl then 100 else 10000
256− = do (u, ntimes) <- usable spec n ntimes_in
258+ (u, ntimes) <- usable spec limit n ntimes_in
257 let red = u && (tcReducible n ctxt || spec || atRepl || runtime
259 let red = u && (tcReducible n ctxt || spec || atRepl || runtime
258 || sUN "assert_total" `elem` stk)
260 || sUN "assert_total" `elem` stk)
259 if red then
261 if red then
@@ -377,7 +379,8 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
377 [] -> return f
379 [] -> return f
378 _ -> return $ unload env f args
380 _ -> return $ unload env f args
379 | otherwise
381 | otherwise
382+ = do let limit = if simpl then 100 else 10000
380− = do (u, ntimes) <- usable spec n ntimes_in
383+ (u, ntimes) <- usable spec limit n ntimes_in
381 let red = u && (tcReducible n ctxt || spec || atRepl || runtime
384 let red = u && (tcReducible n ctxt || spec || atRepl || runtime
382 || sUN "assert_total" `elem` stk)
385 || sUN "assert_total" `elem` stk)
383 if red then
386 if red then