b03f823 · Idris-dev · git.iko.soy

libs/prelude/Builtins.idr+2

compare with master

unifiedsplit

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

132||| Lazily evaluated values.

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

134||| a case split.

135+%error_reverse

135Lazy : Type -> Type

136Lazy : Type -> Type

136Lazy t = Delayed LazyValue t

137Lazy t = Delayed LazyValue t

137

138

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

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

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

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

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

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

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

143+%error_reverse

142Inf : Type -> Type

144Inf : Type -> Type

143Inf t = Delayed Infinite t

145Inf t = Delayed Infinite t

144

146

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

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

199 = case lookup n ns of

200 Just 0 -> return (False, ns)

201 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)

203

204

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

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

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

312 ev ntimes stk top env

313 (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

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

316 let ntimes' = case f of

317 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

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

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

543 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

545 -- check under guarded constructors.

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

547 Guarded <- guarded,