1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
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
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.
(** [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 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.
|