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
167
168
169
170
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* To deal with side effects we have to save/restore the system state *)
let freeze = ref (fun () -> assert false : unit -> Dyn.t)
let unfreeze = ref (fun _ -> () : Dyn.t -> unit)
let set_freeze f g = freeze := f; unfreeze := g
exception NotReady
exception NotHere
let _ = Errors.register_handler (function
| NotReady ->
Pp.strbrk("The value you are asking for is not ready yet. " ^
"Please wait or pass "^
"the \"-coq-slaves off\" option to CoqIDE to disable "^
"asynchronous script processing.")
| NotHere ->
Pp.strbrk("The value you are asking for is not available "^
"in this process. If you really need this, pass "^
"the \"-coq-slaves off\" option to CoqIDE to disable"^
"asynchronous script processing.")
| _ -> raise Errors.Unhandled)
type fix_exn = exn -> exn
let id x = prerr_endline "no fix_exn"; x
(* Val is not necessarily a final state, so the
computation restarts from the state stocked into Val *)
type 'a comp =
| Delegated
(* TODO in some cases one would like to block, sock here
a mutex and a condition to make this possible *)
| Closure of (unit -> 'a)
| Val of 'a * Dyn.t option
| Exn of exn
(* Invariant: this exception is always "fixed" as in fix_exn *)
type 'a comput =
| Ongoing of (fix_exn * 'a comp ref) Ephemeron.key
| Finished of 'a
type 'a computation = 'a comput ref
let create f x = ref (Ongoing (Ephemeron.create (f, Pervasives.ref x)))
let get x =
match !x with
| Finished v -> (fun x -> x), ref( Val (v,None))
| Ongoing x ->
try Ephemeron.get x
with Ephemeron.InvalidKey -> (fun x -> x), ref (Exn NotHere)
type 'a value = [ `Val of 'a | `Exn of exn ]
let is_over kx = let _, x = get kx in match !x with
| Val _ | Exn _ -> true
| Closure _ | Delegated -> false
let is_val kx = let _, x = get kx in match !x with
| Val _ -> true
| Exn _ | Closure _ | Delegated -> false
let is_exn kx = let _, x = get kx in match !x with
| Exn _ -> true
| Val _ | Closure _ | Delegated -> false
let peek_val kx = let _, x = get kx in match !x with
| Val (v, _) -> Some v
| Exn _ | Closure _ | Delegated -> None
let from_val ?(fix_exn=id) v = create fix_exn (Val (v, None))
let from_here ?(fix_exn=id) v = create fix_exn (Val (v, Some (!freeze ())))
type 'a assignement = [ `Val of 'a | `Exn of exn | `Comp of 'a computation]
let create_delegate fix_exn =
let ck = create fix_exn Delegated in
ck, fun v ->
let fix_exn, c = get ck in
assert (!c == Delegated);
match v with
| `Val v -> c := Val (v, None)
| `Exn e -> c := Exn (fix_exn e)
| `Comp f -> let _, comp = get f in c := !comp
(* TODO: get rid of try/catch to be stackless *)
let compute ~pure ck : 'a value =
let fix_exn, c = get ck in
match !c with
| Val (x, _) -> `Val x
| Exn e -> `Exn e
| Delegated -> `Exn NotReady
| Closure f ->
try
let data = f () in
let state = if pure then None else Some (!freeze ()) in
c := Val (data, state); `Val data
with e ->
let e = Errors.push e in
let e = fix_exn e in
match e with
| NotReady -> `Exn e
| _ -> c := Exn e; `Exn e
let force ~pure x = match compute ~pure x with
| `Val v -> v
| `Exn e -> raise e
let chain ~pure ck f =
let fix_exn, c = get ck in
create fix_exn (match !c with
| Closure _ | Delegated -> Closure (fun () -> f (force ~pure ck))
| Exn _ as x -> x
| Val (v, None) when pure -> Closure (fun () -> f v)
| Val (v, Some _) when pure -> Closure (fun () -> f v)
| Val (v, Some state) -> Closure (fun () -> !unfreeze state; f v)
| Val (v, None) ->
match !ck with
| Finished _ -> Errors.anomaly(Pp.str
"Future.chain ~pure:false call on an already joined computation")
| Ongoing _ -> Errors.anomaly(Pp.strbrk(
"Future.chain ~pure:false call on a pure computation. "^
"This can happen if the computation was initial created with "^
"Future.from_val or if it was Future.chain ~pure:true with a "^
"function and later forced.")))
let create fix_exn f = create fix_exn (Closure f)
let replace kx y =
let _, x = get kx in
match !x with
| Exn _ -> x := Closure (fun () -> force ~pure:false y)
| _ -> Errors.anomaly (Pp.str "Only Exn futures can be replaced")
let purify f x =
let state = !freeze () in
try
let v = f x in
!unfreeze state;
v
with e -> let e = Errors.push e in !unfreeze state; raise e
let transactify f x =
let state = !freeze () in
try f x
with e -> let e = Errors.push e in !unfreeze state; raise e
let purify_future f x = if is_over x then f x else purify f x
let compute x = purify_future (compute ~pure:false) x
let force x = purify_future (force ~pure:false) x
let join kx =
let v = force kx in
kx := Finished v;
v
let split2 x =
chain ~pure:true x (fun x -> fst x),
chain ~pure:true x (fun x -> snd x)
let map2 f x l =
CList.map_i (fun i y ->
let xi = chain ~pure:true x (fun x ->
try List.nth x i
with Failure _ | Invalid_argument _ ->
Errors.anomaly (Pp.str "Future.map2 length mismatch")) in
f xi y) 0 l
|
