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
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* Futures: asynchronous computations with some purity enforcing
*
* A Future.computation is like a lazy_t but with some extra bells and whistles
* to deal with imperative code and eventual delegation to a slave process.
*
* Example of a simple scenario taken into account:
*
* let f = Future.from_here (number_of_constants (Global.env())) in
* let g = Future.chain ~pure:false f (fun n ->
* n = number_of_constants (Global.env())) in
* ...
* Lemmas.save_named ...;
* ...
* let b = Future.force g in
*
* The Future.computation f holds a (immediate, no lazy here) value.
* We then chain to obtain g that (will) hold false if (when it will be
* run) the global environment has a different number of constants, true
* if nothing changed.
* Before forcing g, we add to the global environment one more constant.
* When finally we force g. Its value is going to be *true*.
* This because Future.from_here stores in the computation not only the initial
* value but the entire system state. When g is forced the state is restored,
* hence Global.env() returns the environment that was actual when f was
* created.
* Last, forcing g is run protecting the system state, hence when g finishes,
* the actual system state is restored.
*
* If you compare this with lazy_t, you see that the value returned is *false*,
* that is counter intuitive and error prone.
*
* Still not all computations are impure and access/alter the system state.
* This class can be optimized by using ~pure:true, but there is no way to
* statically check if this flag is misused, hence use it with care.
*
* Other differences with lazy_t is that a future computation that produces
* and exception can be substituted for another computation of the same type.
* Moreover a future computation can be delegated to another execution entity
* that will be allowed to set the result. Finally future computations can
* always be marshalled: if they were joined before marshalling, they will
* hold the computed value (assuming it is itself marshallable), otherwise
* they will become invalid and accessing them raises a private exception.
*)
(* Each computation has a unique id that is inherited by each offspring
* computation (chain, split, map...). Joined computations lose it. *)
module UUID : sig
type t
val invalid : t
val compare : t -> t -> int
val equal : t -> t -> bool
end
module UUIDMap : Map.S with type key = UUID.t
module UUIDSet : Set.S with type elt = UUID.t
exception NotReady of string
type 'a computation
type 'a value = [ `Val of 'a | `Exn of Exninfo.iexn ]
type fix_exn = Exninfo.iexn -> Exninfo.iexn
(* Build a computation, no snapshot of the global state is taken. If you need
to grab a copy of the state start with from_here () and then chain.
fix_exn is used to enrich any exception raised
by forcing the computations or any computation that is chained after
it. It is used by STM to attach errors to their corresponding states,
and to communicate to the code catching the exception a valid state id. *)
val create : fix_exn -> (unit -> 'a) -> 'a computation
(* Usually from_val is used to create "fake" futures, to use the same API
as if a real asynchronous computations was there. In this case fixing
the exception is not needed, but *if* the future is chained, the fix_exn
argument should really be given *)
val from_val : ?fix_exn:fix_exn -> 'a -> 'a computation
(* Like from_val, but also takes a snapshot of the global state. Morally
the value is not just the 'a but also the global system state *)
val from_here : ?fix_exn:fix_exn -> 'a -> 'a computation
(* To get the fix_exn of a computation and build a Lemmas.declaration_hook.
* When a future enters the environment a corresponding hook is run to perform
* some work. If this fails, then its failure has to be annotated with the
* same state id that corresponds to the future computation end. I.e. Qed
* is split into two parts, the lazy one (the future) and the eager one
* (the hook), both performing some computations for the same state id. *)
val fix_exn_of : 'a computation -> fix_exn
(* Run remotely, returns the function to assign.
If not blocking (the default) it raises NotReady if forced before the
delegate assigns it. *)
type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation]
val create_delegate :
?blocking:bool -> name:string ->
fix_exn -> 'a computation * ('a assignement -> unit)
(* Given a computation that is_exn, replace it by another one *)
val replace : 'a computation -> 'a computation -> unit
(* Inspect a computation *)
val is_over : 'a computation -> bool
val is_val : 'a computation -> bool
val is_exn : 'a computation -> bool
val peek_val : 'a computation -> 'a option
val uuid : 'a computation -> UUID.t
(* [chain pure c f] chains computation [c] with [f].
* [chain] forces immediately the new computation if the old one is_over (Exn or Val).
* The [pure] parameter is tricky:
* [pure]:
* When pure is true, the returned computation will not keep a copy
* of the global state.
* [let c' = chain ~pure:true c f in let c'' = chain ~pure:false c' g in]
* is invalid. It works if one forces [c''] since the whole computation
* will be executed in one go. It will not work, and raise an anomaly, if
* one forces c' and then c''.
* [join c; chain ~pure:false c g] is invalid and fails at runtime.
* [force c; chain ~pure:false c g] is correct.
*)
val chain : pure:bool ->
'a computation -> ('a -> 'b) -> 'b computation
(* Forcing a computation *)
val force : 'a computation -> 'a
val compute : 'a computation -> 'a value
(* Final call, no more *inpure* chain allowed since the state is lost.
* Also the fix_exn function is lost, hence error reporting can be incomplete
* in a computation obtained by chaining on a joined future. *)
val join : 'a computation -> 'a
(* Call this before stocking the future. If it is_val then it is joined *)
val sink : 'a computation -> unit
(*** Utility functions ************************************************* ***)
val split2 :
('a * 'b) computation -> 'a computation * 'b computation
val map2 :
('a computation -> 'b -> 'c) ->
'a list computation -> 'b list -> 'c list
(* Once set_freeze is called we can purify a computation *)
val purify : ('a -> 'b) -> 'a -> 'b
(* And also let a function alter the state but backtrack if it raises exn *)
val transactify : ('a -> 'b) -> 'a -> 'b
(** Debug: print a computation given an inner printing function. *)
val print : ('a -> Pp.std_ppcmds) -> 'a computation -> Pp.std_ppcmds
type freeze
(* These functions are needed to get rid of side effects.
Thy are set for the outermos layer of the system, since they have to
deal with the whole system state. *)
val set_freeze : (unit -> freeze) -> (freeze -> unit) -> unit
val customize_not_ready_msg : (string -> Pp.std_ppcmds) -> unit
val customize_not_here_msg : (string -> Pp.std_ppcmds) -> unit
|
