@@ -106,38 +106,41 @@ sym Refl = Refl
106106trans : {a:x} -> {b:y} -> {c:z} -> a = b -> b = c -> a = c
107107trans Refl Refl = Refl
108108
109−||| There are two types of laziness: that arising from lazy functions, and that
110−||| arising from codata. They differ in their totality condition.
111−data LazyType = LazyCodata | LazyEval
109+||| Two types of delayed computation: that arising from lazy functions, and that
110+||| arising from infinite data. They differ in their totality condition.
111+data DelayReason = Infinite | LazyValue
112112
113113||| The underlying implementation of Lazy and Inf.
114114%error_reverse
115−data Lazy' : LazyType -> Type -> Type where
115+data Delayed : DelayReason -> Type -> Type where
116116 ||| A delayed computation.
117117 |||
118118 ||| Delay is inserted automatically by the elaborator where necessary.
119119 |||
120120 ||| 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
122122 ||| @ a the type of the eventual value
123123 ||| @ 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
125125
126126||| Compute a value from a delayed computation.
127127|||
128128||| Inserted by the elaborator where necessary.
129−Force : {t, a : _} -> Lazy' t a -> a
129+Force : {t, a : _} -> Delayed t a -> a
130130Force (Delay x) = x
131131
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.
133135Lazy : Type -> Type
134−Lazy t = Lazy' LazyEval t
136+Lazy t = Delayed LazyValue t
135137
136−||| Recursive parameters to codata. Inserted automatically by the elaborator
137−||| on a "codata" definition but is necessary by hand if mixing inductive and
138−||| coinductive parameters.
138+||| Possibly infinite data.
139+||| 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+||| only be computed when required by a case split.
139142Inf : Type -> Type
140−Inf t = Lazy' LazyCodata t
143+Inf t = Delayed Infinite t
141144
142145namespace Ownership
143146 ||| A read-only version of a unique value