536372f · Idris-dev · git.iko.soy

libs/prelude/Builtins.idr+16−13

compare with master

unifiedsplit

@@ -106,38 +106,41 @@ sym Refl = Refl

106trans : {a:x} -> {b:y} -> {c:z} -> a = b -> b = c -> a = c

107trans Refl Refl = Refl

108

109−||| There are two types of laziness: that arising from lazy functions, and that

109+||| Two types of delayed computation: that arising from lazy functions, and that

110−||| arising from codata. They differ in their totality condition.

110+||| arising from infinite data. They differ in their totality condition.

111−data LazyType = LazyCodata | LazyEval

111+data DelayReason = Infinite | LazyValue

112

113||| The underlying implementation of Lazy and Inf.

114%error_reverse

115−data Lazy' : LazyType -> Type -> Type where

115+data Delayed : DelayReason -> Type -> Type where

116 ||| A delayed computation.

117 |||

118 ||| Delay is inserted automatically by the elaborator where necessary.

119 |||

120 ||| Note that compiled code gives `Delay` special semantics.

121− ||| @ t whether this is laziness from codata or normal lazy evaluation

121+ ||| @ t whether this is laziness from an infinite structure or lazy evaluation

122 ||| @ a the type of the eventual value

123 ||| @ val a computation that will produce a value

124− Delay : {t, a : _} -> (val : a) -> Lazy' t a

124+ Delay : {t, a : _} -> (val : a) -> Delayed t a

125

126||| Compute a value from a delayed computation.

127|||

128||| Inserted by the elaborator where necessary.

129−Force : {t, a : _} -> Lazy' t a -> a

129+Force : {t, a : _} -> Delayed t a -> a

130Force (Delay x) = x

131

132−||| Lazily evaluated values. This has special evaluation semantics.

132+||| Lazily evaluated values.

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

134+||| a case split.

133Lazy : Type -> Type

135Lazy : Type -> Type

134−Lazy t = Lazy' LazyEval t

136+Lazy t = Delayed LazyValue t

135

137

136−||| Recursive parameters to codata. Inserted automatically by the elaborator

138+||| Possibly infinite data.

137−||| on a "codata" definition but is necessary by hand if mixing inductive and

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

138−||| coinductive parameters.

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

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

139Inf : Type -> Type

142Inf : Type -> Type

140−Inf t = Lazy' LazyCodata t

143+Inf t = Delayed Infinite t

141

144

142namespace Ownership

145namespace Ownership

143 ||| A read-only version of a unique value

146 ||| A read-only version of a unique value

libs/prelude/Prelude/Stream.idr+2−2

@@ -13,8 +13,8 @@ import Prelude.List

13%default total

14

15||| An infinite stream

16−codata Stream : Type -> Type where

16+data Stream : Type -> Type where

17− (::) : (e : a) -> Stream a -> Stream a

17+ (::) : (e : a) -> Inf (Stream a) -> Stream a

18

19-- Hints for interactive editing

20%name Stream xs,ys,zs,ws

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

@@ -712,9 +712,9 @@ envPos x i ((y, _) : ys) | x == y = i

712-- Issue #1722 on the issue tracker https://github.com/idris-lang/Idris-dev/issues/1722

713--

714recoverable t@(App _ _ _) _

715− | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False

715+ | (P _ (UN l) _, _) <- unApply t, l == txt "Delayed" = False

716recoverable _ t@(App _ _ _)

717− | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False

717+ | (P _ (UN l) _, _) <- unApply t, l == txt "Delayed" = False

718recoverable (P (DCon _ _ _) x _) (P (DCon _ _ _) y _) = x == y

719recoverable (P (TCon _ _) x _) (P (TCon _ _) y _) = x == y

720recoverable (TType _) (P (DCon _ _ _) y _) = False

src/Idris/Coverage.hs+2−2

@@ -493,9 +493,9 @@ delazy' all t@(App _ f a)

493 | (P _ (UN l) _, [_, _, arg]) <- unApply t,

494 l == txt "Force" = delazy' all arg

495 | (P _ (UN l) _, [P _ (UN lty) _, _, arg]) <- unApply t,

496− l == txt "Delay" && (all || lty == txt "LazyEval") = delazy arg

496+ l == txt "Delay" && (all || lty /= txt "Infinite") = delazy arg

497 | (P _ (UN l) _, [P _ (UN lty) _, arg]) <- unApply t,

498− l == txt "Lazy'" && (all || lty == txt "LazyEval") = delazy' all arg

498+ l == txt "Delayed" && (all || lty /= txt "Infinite") = delazy' all arg

499delazy' all (App s f a) = App s (delazy' all f) (delazy' all a)

500delazy' all (Bind n b sc) = Bind n (fmap (delazy' all) b) (delazy' all sc)

501delazy' all t = t

src/Idris/Elab/Data.hs+2−2

@@ -216,8 +216,8 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcen

216

217 mkLazy (PPi pl n nfc ty sc)

218 = let ty' = if getTyName ty

219− then PApp fc (PRef fc [] (sUN "Lazy'"))

219+ then PApp fc (PRef fc [] (sUN "Delayed"))

220− [pexp (PRef fc [] (sUN "LazyCodata")),

220+ [pexp (PRef fc [] (sUN "Infinite")),

221 pexp ty]

222 else ty in

223 PPi pl n nfc ty' (mkLazy sc)

src/Idris/Elab/Term.hs+5−5

@@ -313,13 +313,13 @@ elab ist info emode opts fn tm

313

314 forceErr orig env (CantUnify _ (t,_) (t',_) _ _ _)

315 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),

316− ht == txt "Lazy'" = notDelay orig

316+ ht == txt "Delayed" = notDelay orig

317 forceErr orig env (CantUnify _ (t,_) (t',_) _ _ _)

318 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t'),

319− ht == txt "Lazy'" = notDelay orig

319+ ht == txt "Delayed" = notDelay orig

320 forceErr orig env (InfiniteUnify _ t _)

321 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),

322− ht == txt "Lazy'" = notDelay orig

322+ ht == txt "Delayed" = notDelay orig

323 forceErr orig env (Elaborating _ _ _ t) = forceErr orig env t

324 forceErr orig env (ElaboratingArg _ _ _ t) = forceErr orig env t

325 forceErr orig env (At _ t) = forceErr orig env t

@@ -482,7 +482,7 @@ elab ist info emode opts fn tm

482 return $ pruneByType env tc (unDelay ty) ist as

483

484 unDelay t | (P _ (UN l) _, [_, arg]) <- unApply t,

485− l == txt "Lazy'" = unDelay arg

485+ l == txt "Delayed" = unDelay arg

486 | otherwise = t

487

488 isAmbiguous (CantResolveAlts _) = delayok

@@ -1400,7 +1400,7 @@ elab ist info emode opts fn tm

1400 let (tyh, _) = unApply (normalise (tt_ctxt ist) env ty)

1401 let tries = [mkDelay env t, t]

1402 case tyh of

1403− P _ (UN l) _ | l == txt "Lazy'"

1403+ P _ (UN l) _ | l == txt "Delayed"

1404 -> return (PAlternative [] FirstSuccess tries)

1405 _ -> return t

1406 where

src/Idris/TypeSearch.hs+2−2

@@ -101,10 +101,10 @@ typeFromDef (def, _, _, _, _) = get def where

101 get (CaseOp _ ty _ _ _ _) = Just ty

102 get _ = Nothing

103

104−-- Replace all occurences of `Lazy' s t` with `t` in a type

104+-- Replace all occurences of `Delayed s t` with `t` in a type

105unLazy :: Type -> Type

106unLazy typ = case typ of

107− App _ (App _ (P _ lazy _) _) ty | lazy == sUN "Lazy'" -> unLazy ty

107+ App _ (App _ (P _ lazy _) _) ty | lazy == sUN "Delayed" -> unLazy ty

108 Bind name binder ty -> Bind name (fmap unLazy binder) (unLazy ty)

109 App s t1 t2 -> App s (unLazy t1) (unLazy t2)

110 Proj ty i -> Proj (unLazy ty) i