b03f823 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix evaluation of Inf

The evaluator was treating the old name LazyCodata specially, rather than the up to date name Delayed Infinite. Also, we shouldn't treat infinite data specially at the REPL, but rather only evaluate under Delay when explicitly Forced (in the same way as the type checker itself does).

commitb03f8236fe2ad45984fb2fa343cf9cbcea760087 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 11 Jun 2016, 14:26 (10 years ago) parenta854972

3 files changed+5−3

compare with master

unifiedsplit

libs/prelude/Builtins.idr+2 src/Idris/Core/Evaluate.hs+2−2 src/Idris/Coverage.hs+1−1

libs/prelude/Builtins.idr+2

@@ -132,6 +132,7 @@ Force (Delay x) = x

132132||| Lazily evaluated values.

133133||| At run time, the delayed value will only be computed when required by

134134||| a case split.

135+%error_reverse

135136Lazy : Type -> Type

136137Lazy t = Delayed LazyValue t

137138

@@ -139,6 +140,7 @@ Lazy t = Delayed LazyValue t

139140||| A value which may be infinite is accepted by the totality checker if

140141||| it appears under a data constructor. At run time, the delayed value will

141142||| only be computed when required by a case split.

143+%error_reverse

142144Inf : Type -> Type

143145Inf t = Delayed Infinite t

144146

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

@@ -199,7 +199,7 @@ usable False n ns

199199 = case lookup n ns of

200200 Just 0 -> return (False, ns)

201201 Just i -> return $ (True, (n, abs (i-1)) : filter (\ (n', _) -> n/=n') ns)

202− _ -> return $ (True, (n, 100) : filter (\ (n', _) -> n/=n') ns)

202+ _ -> return $ (True, (n, 1000000) : filter (\ (n', _) -> n/=n') ns)

203203

204204

205205fnCount :: Int -> Name -> Eval ()

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

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

312312 ev ntimes stk top env

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

314− | dly == txt "Delay" && lco == txt "LazyCodata" && not (simpl || atRepl)

314+ | dly == txt "Delay" && lco == txt "Infinite" && not simpl

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

316316 let ntimes' = case f of

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

src/Idris/Coverage.hs+1−1

@@ -541,7 +541,7 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

541541 | (P _ n _, _) <- unApply ap,

542542 Just opts <- lookupCtxtExact n (idris_flags ist),

543543 AssertTotal `elem` opts = []

544− -- under a guarded call to "Delay LazyCodata", we are 'Delayed', so don't

544+ -- under a guarded call to "Delay Infinite", we are 'Delayed', so don't

545545 -- check under guarded constructors.

546546 | (P _ (UN del) _, [_,_,arg]) <- unApply ap,

547547 Guarded <- guarded,