git.iko.soy/Idris-dev
on master help sign in
Check assert_total is defined before evaluating

Otherwise it goes bad when defining it! This is just a bit of a hack to make sure we fully evaluate under assert_total, and probably ought to be done a bit more tidily later.

commit93c06b59359088550222a79bd70f7d47f3fd52ba authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 2 Feb 2014, 01:32 (13 years ago) parentf650e7e
1 file changed+5−7
compare with master
unifiedsplit
src/Idris/Core/Evaluate.hs+5−7
src/Idris/Core/Evaluate.hs+5−7
@@ -257,14 +257,12 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
257257 return $ VBind True -- (vinstances 0 sc < 2)
258258 n' b' (\x -> ev ntimes stk False ((n, x):env) sc)
259259 where vbind env t
260−-- | simpl
261−-- = fmapMB (\tm -> ev ((MN 0 "STOP", 0) : ntimes)
262−-- stk top env (finalise tm)) t
263−-- | otherwise
264260 = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t
265− ev ntimes stk top env (App (App (P _ (UN at) _) _) arg)
266− | at == txt "assert_total" && not simpl
267− = ev ntimes (UN at : stk) top env arg
261+ -- Treat "assert_total" specially, as long as it's defined!
262+ ev ntimes stk top env (App (App (P _ n@(UN at) _) _) arg)
263+ | [(CaseOp _ _ _ _ _ _, _)] <- lookupDefAcc n (spec || atRepl) ctxt,
264+ at == txt "assert_total" && not simpl
265+ = ev ntimes (n : stk) top env arg
268266 ev ntimes stk top env (App f a)
269267 = do f' <- ev ntimes stk False env f
270268 a' <- ev ntimes stk False env a