Library Ltac2.Lazy
Require Import Ltac2.Init.
Require Ltac2.Ref.
Require Ltac2.Control.
Ltac2 Type 'a lazy_data := [ Value ('a) | Thunk (unit -> 'a) ].
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).
Ltac2 Type 'a t := 'a lazy_data Ref.ref.
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.
Ltac2 from_val (v : 'a) : 'a t :=
Ref.ref (Value v).
Ref.ref (Value v).
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.
Ltac2 from_fun (f : unit -> 'a) : 'a t :=
Ref.ref (Thunk f).
Ref.ref (Thunk f).
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.
Ltac2 is_val (r : 'a t) : bool :=
match Ref.get r with
| Value _ => true
| Thunk _ => false
end.
match Ref.get r with
| Value _ => true
| Thunk _ => false
end.
Exception raised in case of a "cyclic" lazy cell.
Ltac2 Type exn ::= [ Undefined ].
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").
Ltac2 force (r : 'a t) : 'a :=
match Ref.get r with
| Value v => v
| Thunk f =>
Ref.set r (Thunk (fun () => Control.throw Undefined));
match Control.case f with
| Val (v, _) =>
Ref.set r (Value v);
v
| Err e =>
Ref.set r (Thunk (fun () => Control.zero e));
Control.zero e
end
end.
match Ref.get r with
| Value v => v
| Thunk f =>
Ref.set r (Thunk (fun () => Control.throw Undefined));
match Control.case f with
| Val (v, _) =>
Ref.set r (Value v);
v
| Err e =>
Ref.set r (Thunk (fun () => Control.zero e));
Control.zero e
end
end.
map f r is equivalent to from_fun (fun () => f (force r)).
Ltac2 map (f : 'a -> 'b) (r : 'a t) : 'b t :=
from_fun (fun () => f (force r)).
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.
Ltac2 map_val (f : 'a -> 'b) (r : 'a t) : 'b t :=
match Ref.get r with
| Value v =>
match Control.case (fun () => f v) with
| Val (v, _) => from_val v
| Err e => from_fun (fun () => Control.zero e)
end
| Thunk t => from_fun (fun () => f (t ()))
end.
Module Export Notations.
Ltac2 Notation "lazy!" f(thunk(self)) := from_fun f.
End Notations.
match Ref.get r with
| Value v =>
match Control.case (fun () => f v) with
| Val (v, _) => from_val v
| Err e => from_fun (fun () => Control.zero e)
end
| Thunk t => from_fun (fun () => f (t ()))
end.
Module Export Notations.
Ltac2 Notation "lazy!" f(thunk(self)) := from_fun f.
End Notations.