@@ -165,7 +165,7 @@ eval ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
165 ev ntimes_in stk top env (P Ref n ty)
165 ev ntimes_in stk top env (P Ref n ty)
166 | (True, ntimes) <- usable n ntimes_in
166 | (True, ntimes) <- usable n ntimes_in
167 = do let val = lookupDefAcc Nothing n atRepl ctxt
167 = do let val = lookupDefAcc Nothing n atRepl ctxt
168− step maxred
168+ when (not atRepl) $ step maxred
169 case val of
169 case val of
170 [(Function _ tm, Public)] ->
170 [(Function _ tm, Public)] ->
171 ev ntimes (n:stk) True env tm
171 ev ntimes (n:stk) True env tm
@@ -184,24 +184,24 @@ eval ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
184 | otherwise = return $ VV i
184 | otherwise = return $ VV i
185 ev ntimes stk top env (Bind n (Let t v) sc)
185 ev ntimes stk top env (Bind n (Let t v) sc)
186 = do v' <- ev ntimes stk top env v --(finalise v)
186 = do v' <- ev ntimes stk top env v --(finalise v)
187− step maxred
187+ when (not atRepl) $ step maxred
188 sc' <- ev ntimes stk top (v' : env) sc
188 sc' <- ev ntimes stk top (v' : env) sc
189 wknV (-1) sc'
189 wknV (-1) sc'
190 ev ntimes stk top env (Bind n (NLet t v) sc)
190 ev ntimes stk top env (Bind n (NLet t v) sc)
191 = do t' <- ev ntimes stk top env (finalise t)
191 = do t' <- ev ntimes stk top env (finalise t)
192 v' <- ev ntimes stk top env (finalise v)
192 v' <- ev ntimes stk top env (finalise v)
193− step maxred
193+ when (not atRepl) $ step maxred
194 sc' <- ev ntimes stk top (v' : env) sc
194 sc' <- ev ntimes stk top (v' : env) sc
195 return $ VBind n (Let t' v') (\x -> return sc')
195 return $ VBind n (Let t' v') (\x -> return sc')
196 ev ntimes stk top env (Bind n b sc)
196 ev ntimes stk top env (Bind n b sc)
197 = do b' <- vbind env b
197 = do b' <- vbind env b
198− step maxred
198+ when (not atRepl) $ step maxred
199 return $ VBind n b' (\x -> ev ntimes stk top (x:env) sc)
199 return $ VBind n b' (\x -> ev ntimes stk top (x:env) sc)
200 where vbind env t = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t
200 where vbind env t = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t
201 ev ntimes stk top env (App f a)
201 ev ntimes stk top env (App f a)
202 = do f' <- ev ntimes stk top env f
202 = do f' <- ev ntimes stk top env f
203 a' <- ev ntimes stk False env a
203 a' <- ev ntimes stk False env a
204− step maxred
204+ when (not atRepl) $ step maxred
205 evApply ntimes stk top env [a'] f'
205 evApply ntimes stk top env [a'] f'
206 ev ntimes stk top env (Constant c) = return $ VConstant c
206 ev ntimes stk top env (Constant c) = return $ VConstant c
207 ev ntimes stk top env Erased = return VErased
207 ev ntimes stk top env Erased = return VErased
@@ -209,7 +209,7 @@ eval ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
210 evApply ntimes stk top env args (VApp f a) =
210 evApply ntimes stk top env args (VApp f a) =
211 evApply ntimes stk top env (a:args) f
211 evApply ntimes stk top env (a:args) f
212− evApply ntimes stk top env args f = do step maxred
212+ evApply ntimes stk top env args f = do when (not atRepl) $ step maxred
213 apply ntimes stk top env f args
213 apply ntimes stk top env f args
215 apply ntimes stk top env (VBind n (Lam t) sc) (a:as)
215 apply ntimes stk top env (VBind n (Lam t) sc) (a:as)