@@ -17,6 +17,7 @@ getWitness (a ** v) = a
17getProof : {P : a -> Type} -> (s : Exists a P) -> P (getWitness s)
17getProof : {P : a -> Type} -> (s : Exists a P) -> P (getWitness s)
18getProof (a ** v) = v
18getProof (a ** v) = v
20+||| The eliminator for the empty type.
20FalseElim : _|_ -> a
21FalseElim : _|_ -> a
22||| For 'symbol syntax. 'foo becomes Symbol_ "foo"
23||| For 'symbol syntax. 'foo becomes Symbol_ "foo"
@@ -43,17 +44,35 @@ lazy x = x -- compiled specially
43force : a -> a
44force : a -> a
44force x = x -- compiled specially
45force x = x -- compiled specially
47+||| There are two types of laziness: that arising from lazy functions, and that
48+||| arising from codata. They differ in their totality condition.
46data LazyType = LazyCodata | LazyEval
49data LazyType = LazyCodata | LazyEval
51+||| The underlying implementation of Lazy and Inf.
48data Lazy' : LazyType -> Type -> Type where
52data Lazy' : LazyType -> Type -> Type where
53+ ||| A delayed computation.
55+ |||Delay is inserted automatically by the elaborator where necessary.
57+ ||| Note that compiled code gives `Delay` special semantics.
58+ ||| @ t whether this is laziness from codata or normal lazy evaluation
59+ ||| @ a the type of the eventual value
60+ ||| @ val a computation that will produce a value
49 Delay : {t, a : _} -> (val : a) -> Lazy' t a
61 Delay : {t, a : _} -> (val : a) -> Lazy' t a
63+||| Compute a value from a delayed computation.
65+||| Inserted by the elaborator where necessary.
51Force : {t, a : _} -> Lazy' t a -> a
66Force : {t, a : _} -> Lazy' t a -> a
52Force (Delay x) = x
67Force (Delay x) = x
69+||| Lazily evaluated values. This has special evaluation semantics.
54Lazy : Type -> Type
70Lazy : Type -> Type
55Lazy t = Lazy' LazyEval t
71Lazy t = Lazy' LazyEval t
73+||| Recursive parameters to codata. Inserted automatically by the elaborator
74+||| on a "codata" definition but is necessary by hand if mixing inductive and
75+||| coinductive parameters.
57Inf : Type -> Type
76Inf : Type -> Type
58Inf t = Lazy' LazyCodata t
77Inf t = Lazy' LazyCodata t