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).

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).

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

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 f with
      | Val (v, _) =>
          Ref.set r (Value v);
      | Err e =>
          Ref.set r (Thunk (fun () => e));

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)).

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 (fun () => f v) with
      | Val (v, _) => from_val v
      | Err e => from_fun (fun () => e)
  | Thunk t => from_fun (fun () => f (t ()))

Module Export Notations.
  Ltac2 Notation "lazy!" f(thunk(self)) := from_fun f.
End Notations.