Library Ltac2.Lazy

Type of a lazy cell, similar to OCaml's 'a Lazy.t type. The functions of this module do not have any specific backtracking support, so any function passed to primitives of this module is handled as if it had one success at most (potential other successes are ignored).

from_val v creates a new lazy cell storing (already-computed) value v. Forcing (i.e., using the force function on) the produced cell gives back value v, and never gives an exception.

from_fun f creates a new lazy cell from the given thunk f. There is no specific support for backtracking in the Lazy module, so if f has more than one success, only the first one will be considered.

is_val r indicates whether the given lazy cell r holds a forced value. In particular, is_val r always returns true if r was created via the from_val function. If r was created using from_fun, then true will only be returned if the value of r was previously forced (e.g., with the force function), and if no exception was produced by said forcing.

Exception raised in case of a "cyclic" lazy cell.

force r gives the value represented by the lazy cell r, which requires forcing a thunk and updating r to the produced value if r does not yet have a value. Note that if forcing produces an exception, subsequent calls to force will immediately yield the same exception (without re-computing the whole thunk). Additionally, the Undefined exception is produced (and set to be produced by r on subsequent calls to force) if r relies on its own value for its definition (i.e., if r is "cyclic").

map f r is equivalent to from_fun (fun () => f (force r)).

map_val f r is similar to map f r, but the function f is immediately applied if r contains a forced value. If the immediate application gives an exception, then any subsequent forcing of produced lazy cell will raise the same exception.