bbf672a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix evaluator problem

Didn't test this properly in last patch, sorry! Need to be careful in evaluator in simplify mode lest it break totality checking.

commitbbf672a5564885ab94c75cc500d82097da6124d8 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 21 Feb 2015, 21:48 (12 years ago) parent7c9a1d0

1 file changed+3−3

unifiedsplit

src/Idris/Core/Evaluate.hs+3−3

@@ -286,17 +286,17 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

286286 -- block reduction immediately under codata (and not forced)

287287 ev ntimes stk top env

288288 (App (App (App d@(P _ (UN dly) _) l@(P _ (UN lco) _)) t) arg)

289− | dly == txt "Delay" && lco == txt "LazyCodata" -- && not simpl

289+ | dly == txt "Delay" && lco == txt "LazyCodata" && not simpl

290290 = do let (f, _) = unApply arg

291291 let ntimes' = case f of

292292 P _ fn _ -> (fn, 0) : ntimes

293293 _ -> ntimes

294− when (spec || simpl) $ setBlock True

294+ when spec $ setBlock True

295295 d' <- ev ntimes' stk False env d

296296 l' <- ev ntimes' stk False env l

297297 t' <- ev ntimes' stk False env t

298298 arg' <- ev ntimes' stk False env arg

299− when (spec || simpl) $ setBlock False

299+ when spec $ setBlock False

300300 evApply ntimes' stk top env [l',t',arg'] d'

301301 -- Treat "assert_total" specially, as long as it's defined!

302302 ev ntimes stk top env (App (App (P _ n@(UN at) _) _) arg)