source: extracted/iOMonad.ml @ 3043

Last change on this file since 3043 was 3043, checked in by sacerdot, 7 years ago

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File size: 18.6 KB
Line 
1open Preamble
2
3open Div_and_mod
4
5open Jmeq
6
7open Russell
8
9open Util
10
11open Bool
12
13open Relations
14
15open Nat
16
17open List
18
19open Hints_declaration
20
21open Core_notation
22
23open Pts
24
25open Logic
26
27open Types
28
29open Extralib
30
31open ErrorMessages
32
33open Option
34
35open Setoids
36
37open Monad
38
39open Positive
40
41open PreIdentifiers
42
43open Errors
44
45type ('output, 'input, 't) iO =
46| Interact of 'output * ('input -> ('output, 'input, 't) iO)
47| Value of 't
48| Wrong of Errors.errmsg
49
50(** val iO_rect_Type4 :
51    ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 ->
52    'a4) -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4 **)
53let rec iO_rect_Type4 h_Interact h_Value h_Wrong = function
54| Interact (o, x_4685) ->
55  h_Interact o x_4685 (fun x_4684 ->
56    iO_rect_Type4 h_Interact h_Value h_Wrong (x_4685 x_4684))
57| Value x_4686 -> h_Value x_4686
58| Wrong x_4687 -> h_Wrong x_4687
59
60(** val iO_rect_Type3 :
61    ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 ->
62    'a4) -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4 **)
63let rec iO_rect_Type3 h_Interact h_Value h_Wrong = function
64| Interact (o, x_4701) ->
65  h_Interact o x_4701 (fun x_4700 ->
66    iO_rect_Type3 h_Interact h_Value h_Wrong (x_4701 x_4700))
67| Value x_4702 -> h_Value x_4702
68| Wrong x_4703 -> h_Wrong x_4703
69
70(** val iO_rect_Type2 :
71    ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 ->
72    'a4) -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4 **)
73let rec iO_rect_Type2 h_Interact h_Value h_Wrong = function
74| Interact (o, x_4709) ->
75  h_Interact o x_4709 (fun x_4708 ->
76    iO_rect_Type2 h_Interact h_Value h_Wrong (x_4709 x_4708))
77| Value x_4710 -> h_Value x_4710
78| Wrong x_4711 -> h_Wrong x_4711
79
80(** val iO_rect_Type1 :
81    ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 ->
82    'a4) -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4 **)
83let rec iO_rect_Type1 h_Interact h_Value h_Wrong = function
84| Interact (o, x_4717) ->
85  h_Interact o x_4717 (fun x_4716 ->
86    iO_rect_Type1 h_Interact h_Value h_Wrong (x_4717 x_4716))
87| Value x_4718 -> h_Value x_4718
88| Wrong x_4719 -> h_Wrong x_4719
89
90(** val iO_rect_Type0 :
91    ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 ->
92    'a4) -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4 **)
93let rec iO_rect_Type0 h_Interact h_Value h_Wrong = function
94| Interact (o, x_4725) ->
95  h_Interact o x_4725 (fun x_4724 ->
96    iO_rect_Type0 h_Interact h_Value h_Wrong (x_4725 x_4724))
97| Value x_4726 -> h_Value x_4726
98| Wrong x_4727 -> h_Wrong x_4727
99
100(** val iO_inv_rect_Type4 :
101    ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __
102    -> 'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ ->
103    'a4) -> 'a4 **)
104let iO_inv_rect_Type4 hterm h1 h2 h3 =
105  let hcut = iO_rect_Type4 h1 h2 h3 hterm in hcut __
106
107(** val iO_inv_rect_Type3 :
108    ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __
109    -> 'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ ->
110    'a4) -> 'a4 **)
111let iO_inv_rect_Type3 hterm h1 h2 h3 =
112  let hcut = iO_rect_Type3 h1 h2 h3 hterm in hcut __
113
114(** val iO_inv_rect_Type2 :
115    ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __
116    -> 'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ ->
117    'a4) -> 'a4 **)
118let iO_inv_rect_Type2 hterm h1 h2 h3 =
119  let hcut = iO_rect_Type2 h1 h2 h3 hterm in hcut __
120
121(** val iO_inv_rect_Type1 :
122    ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __
123    -> 'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ ->
124    'a4) -> 'a4 **)
125let iO_inv_rect_Type1 hterm h1 h2 h3 =
126  let hcut = iO_rect_Type1 h1 h2 h3 hterm in hcut __
127
128(** val iO_inv_rect_Type0 :
129    ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __
130    -> 'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ ->
131    'a4) -> 'a4 **)
132let iO_inv_rect_Type0 hterm h1 h2 h3 =
133  let hcut = iO_rect_Type0 h1 h2 h3 hterm in hcut __
134
135(** val iO_discr : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3) iO -> __ **)
136let iO_discr x y =
137  Logic.eq_rect_Type2 x
138    (match x with
139     | Interact (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
140     | Value a0 -> Obj.magic (fun _ dH -> dH __)
141     | Wrong a0 -> Obj.magic (fun _ dH -> dH __)) y
142
143(** val iO_jmdiscr : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3) iO -> __ **)
144let iO_jmdiscr x y =
145  Logic.eq_rect_Type2 x
146    (match x with
147     | Interact (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
148     | Value a0 -> Obj.magic (fun _ dH -> dH __)
149     | Wrong a0 -> Obj.magic (fun _ dH -> dH __)) y
150
151open Proper
152
153(** val bindIO :
154    ('a1, 'a2, 'a3) iO -> ('a3 -> ('a1, 'a2, 'a4) iO) -> ('a1, 'a2, 'a4) iO **)
155let rec bindIO v f =
156  match v with
157  | Interact (out, k) -> Interact (out, (fun res -> bindIO (k res) f))
158  | Value v' -> f v'
159  | Wrong m -> Wrong m
160
161(** val iOMonad : Monad.monadProps **)
162let iOMonad =
163  Monad.makeMonadProps (fun _ x -> Value x) (fun _ _ -> bindIO)
164
165(** val bindIO2 : __ -> ('a3 -> 'a4 -> __) -> __ **)
166let bindIO2 m f =
167  Monad.m_bind2 (Monad.max_def iOMonad) m f
168
169(** val iORel : Monad.monadRel **)
170let iORel =
171  Monad.Mk_MonadRel
172
173(** val pred_io_inject :
174    ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3 Types.sig0) iO **)
175let rec pred_io_inject a =
176  (match a with
177   | Interact (o, f) ->
178     (fun _ -> Interact (o, (fun x -> pred_io_inject (f x))))
179   | Value x ->
180     (fun _ -> Obj.magic (Monad.m_return0 (Monad.max_def iOMonad) x))
181   | Wrong e -> (fun _ -> Wrong e)) __
182
183(** val iOPred : Monad.injMonadPred **)
184let iOPred =
185  { Monad.im_pred = Monad.Mk_MonadPred; Monad.mp_inject = (fun _ _ a_sig ->
186    let a = a_sig in Obj.magic (pred_io_inject (Obj.magic a))) }
187
188(** val err_to_io : 'a3 Errors.res -> ('a1, 'a2, 'a3) iO **)
189let err_to_io = function
190| Errors.OK v' -> Value v'
191| Errors.Error m -> Wrong m
192
193(** val dpi1__o__err_to_io__o__inject :
194    ('a2 Errors.res, 'a3) Types.dPair -> ('a1, 'a4, 'a2) iO Types.sig0 **)
195let dpi1__o__err_to_io__o__inject x4 =
196  err_to_io x4.Types.dpi1
197
198(** val eject__o__err_to_io__o__inject :
199    'a2 Errors.res Types.sig0 -> ('a1, 'a3, 'a2) iO Types.sig0 **)
200let eject__o__err_to_io__o__inject x4 =
201  err_to_io (Types.pi1 x4)
202
203(** val err_to_io__o__inject :
204    'a2 Errors.res -> ('a1, 'a3, 'a2) iO Types.sig0 **)
205let err_to_io__o__inject x3 =
206  err_to_io x3
207
208(** val dpi1__o__err_to_io :
209    ('a2 Errors.res, 'a3) Types.dPair -> ('a1, 'a4, 'a2) iO **)
210let dpi1__o__err_to_io x4 =
211  err_to_io x4.Types.dpi1
212
213(** val eject__o__err_to_io :
214    'a2 Errors.res Types.sig0 -> ('a1, 'a3, 'a2) iO **)
215let eject__o__err_to_io x4 =
216  err_to_io (Types.pi1 x4)
217
218(** val err_to_io_sig :
219    'a3 Types.sig0 Errors.res -> ('a1, 'a2, 'a3 Types.sig0) iO **)
220let err_to_io_sig = function
221| Errors.OK v' -> Value v'
222| Errors.Error m -> Wrong m
223
224(** val io_inject_0 : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3 Types.sig0) iO **)
225let rec io_inject_0 a =
226  (match a with
227   | Interact (out, k) ->
228     (fun _ -> Interact (out, (fun v -> io_inject_0 (k v))))
229   | Value c -> (fun _ -> Value c)
230   | Wrong m -> (fun _ -> Wrong m)) __
231
232(** val io_inject :
233    ('a1, 'a2, 'a3) iO Types.option -> ('a1, 'a2, 'a3 Types.sig0) iO **)
234let io_inject a =
235  (match a with
236   | Types.None -> (fun _ -> Logic.false_rect_Type0 __)
237   | Types.Some b -> (fun _ -> io_inject_0 b)) __
238
239(** val io_eject : ('a1, 'a2, 'a3 Types.sig0) iO -> ('a1, 'a2, 'a3) iO **)
240let rec io_eject = function
241| Interact (out, k) -> Interact (out, (fun v -> io_eject (k v)))
242| Value b -> let w = b in Value w
243| Wrong m -> Wrong m
244
245(** val dpi1__o__io_inject__o__inject :
246    (('a1, 'a3, 'a2) iO Types.option, 'a4) Types.dPair -> ('a1, 'a3, 'a2
247    Types.sig0) iO Types.sig0 **)
248let dpi1__o__io_inject__o__inject x6 =
249  io_inject x6.Types.dpi1
250
251(** val eject__o__io_inject__o__inject :
252    ('a1, 'a3, 'a2) iO Types.option Types.sig0 -> ('a1, 'a3, 'a2 Types.sig0)
253    iO Types.sig0 **)
254let eject__o__io_inject__o__inject x6 =
255  io_inject (Types.pi1 x6)
256
257(** val io_inject__o__inject :
258    ('a1, 'a3, 'a2) iO Types.option -> ('a1, 'a3, 'a2 Types.sig0) iO
259    Types.sig0 **)
260let io_inject__o__inject x5 =
261  io_inject x5
262
263(** val dpi1__o__io_inject :
264    (('a1, 'a3, 'a2) iO Types.option, 'a4) Types.dPair -> ('a1, 'a3, 'a2
265    Types.sig0) iO **)
266let dpi1__o__io_inject x5 =
267  io_inject x5.Types.dpi1
268
269(** val eject__o__io_inject :
270    ('a1, 'a3, 'a2) iO Types.option Types.sig0 -> ('a1, 'a3, 'a2 Types.sig0)
271    iO **)
272let eject__o__io_inject x5 =
273  io_inject (Types.pi1 x5)
274
275(** val io_inject__o__io_eject__o__inject :
276    ('a1, 'a3, 'a2) iO Types.option -> ('a1, 'a3, 'a2) iO Types.sig0 **)
277let io_inject__o__io_eject__o__inject x4 =
278  io_eject (io_inject x4)
279
280(** val dpi1__o__err_to_io__o__io_eject__o__inject :
281    ('a2 Types.sig0 Errors.res, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO
282    Types.sig0 **)
283let dpi1__o__err_to_io__o__io_eject__o__inject x6 =
284  io_eject (dpi1__o__err_to_io x6)
285
286(** val dpi1__o__io_inject__o__io_eject__o__inject :
287    (('a1, 'a3, 'a2) iO Types.option, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO
288    Types.sig0 **)
289let dpi1__o__io_inject__o__io_eject__o__inject x6 =
290  io_eject (dpi1__o__io_inject x6)
291
292(** val eject__o__err_to_io__o__io_eject__o__inject :
293    'a2 Types.sig0 Errors.res Types.sig0 -> ('a1, 'a3, 'a2) iO Types.sig0 **)
294let eject__o__err_to_io__o__io_eject__o__inject x6 =
295  io_eject (eject__o__err_to_io x6)
296
297(** val eject__o__io_inject__o__io_eject__o__inject :
298    ('a1, 'a3, 'a2) iO Types.option Types.sig0 -> ('a1, 'a3, 'a2) iO
299    Types.sig0 **)
300let eject__o__io_inject__o__io_eject__o__inject x6 =
301  io_eject (eject__o__io_inject x6)
302
303(** val err_to_io__o__io_eject__o__inject :
304    'a2 Types.sig0 Errors.res -> ('a1, 'a3, 'a2) iO Types.sig0 **)
305let err_to_io__o__io_eject__o__inject x4 =
306  io_eject (err_to_io x4)
307
308(** val dpi1__o__io_eject__o__inject :
309    (('a1, 'a3, 'a2 Types.sig0) iO, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO
310    Types.sig0 **)
311let dpi1__o__io_eject__o__inject x6 =
312  io_eject x6.Types.dpi1
313
314(** val eject__o__io_eject__o__inject :
315    ('a1, 'a3, 'a2 Types.sig0) iO Types.sig0 -> ('a1, 'a3, 'a2) iO Types.sig0 **)
316let eject__o__io_eject__o__inject x6 =
317  io_eject (Types.pi1 x6)
318
319(** val io_eject__o__inject :
320    ('a1, 'a3, 'a2 Types.sig0) iO -> ('a1, 'a3, 'a2) iO Types.sig0 **)
321let io_eject__o__inject x5 =
322  io_eject x5
323
324(** val io_inject__o__io_eject :
325    ('a1, 'a3, 'a2) iO Types.option -> ('a1, 'a3, 'a2) iO **)
326let io_inject__o__io_eject x4 =
327  io_eject (io_inject x4)
328
329(** val dpi1__o__err_to_io__o__io_eject :
330    ('a2 Types.sig0 Errors.res, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO **)
331let dpi1__o__err_to_io__o__io_eject x5 =
332  io_eject (dpi1__o__err_to_io x5)
333
334(** val dpi1__o__io_inject__o__io_eject :
335    (('a1, 'a3, 'a2) iO Types.option, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO **)
336let dpi1__o__io_inject__o__io_eject x5 =
337  io_eject (dpi1__o__io_inject x5)
338
339(** val eject__o__err_to_io__o__io_eject :
340    'a2 Types.sig0 Errors.res Types.sig0 -> ('a1, 'a3, 'a2) iO **)
341let eject__o__err_to_io__o__io_eject x5 =
342  io_eject (eject__o__err_to_io x5)
343
344(** val eject__o__io_inject__o__io_eject :
345    ('a1, 'a3, 'a2) iO Types.option Types.sig0 -> ('a1, 'a3, 'a2) iO **)
346let eject__o__io_inject__o__io_eject x5 =
347  io_eject (eject__o__io_inject x5)
348
349(** val err_to_io__o__io_eject :
350    'a2 Types.sig0 Errors.res -> ('a1, 'a3, 'a2) iO **)
351let err_to_io__o__io_eject x4 =
352  io_eject (err_to_io x4)
353
354(** val dpi1__o__io_eject :
355    (('a1, 'a3, 'a2 Types.sig0) iO, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO **)
356let dpi1__o__io_eject x5 =
357  io_eject x5.Types.dpi1
358
359(** val eject__o__io_eject :
360    ('a1, 'a3, 'a2 Types.sig0) iO Types.sig0 -> ('a1, 'a3, 'a2) iO **)
361let eject__o__io_eject x5 =
362  io_eject (Types.pi1 x5)
363
364(** val opt_to_io :
365    Errors.errmsg -> 'a3 Types.option -> ('a1, 'a2, 'a3) iO **)
366let opt_to_io m = function
367| Types.None -> Wrong m
368| Types.Some v' -> Value v'
369
370(** val bind_res_value :
371    'a3 Errors.res -> ('a3 -> 'a4 Errors.res) -> 'a4 -> ('a3 -> __ -> __ ->
372    'a5) -> 'a5 **)
373let bind_res_value clearme f v x =
374  (match clearme with
375   | Errors.OK a -> (fun f0 v0 _ h _ -> h a __ __)
376   | Errors.Error m ->
377     (fun f0 v0 _ h _ -> Obj.magic iO_discr (Wrong m) (Value v0) __)) f v __
378    x __
379
380(** val bindIO_value :
381    ('a1, 'a2, 'a3) iO -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a4 -> ('a3 -> __ ->
382    __ -> 'a5) -> 'a5 **)
383let bindIO_value clearme f v x =
384  (match clearme with
385   | Interact (o, k) ->
386     (fun f0 v0 _ h _ ->
387       Obj.magic iO_discr (Interact (o, (fun res -> bindIO (k res) f0)))
388         (Value v0) __)
389   | Value a -> (fun f0 v0 _ h _ -> h a __ __)
390   | Wrong m ->
391     (fun f0 v0 _ h _ -> Obj.magic iO_discr (Wrong m) (Value v0) __)) f v __
392    x __
393
394(** val bindIO_res_interact :
395    'a3 Errors.res -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a1 -> ('a2 -> ('a1,
396    'a2, 'a4) iO) -> ('a3 -> __ -> __ -> 'a5) -> 'a5 **)
397let bindIO_res_interact clearme f o k x =
398  (match clearme with
399   | Errors.OK a -> (fun f0 o0 k0 _ h _ -> h a __ __)
400   | Errors.Error m ->
401     (fun f0 o0 k0 _ x0 _ ->
402       Obj.magic iO_discr (Wrong m) (Interact (o0, k0)) __)) f o k __ x __
403
404(** val bindIO_opt_interact :
405    Errors.errmsg -> 'a3 Types.option -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a1
406    -> ('a2 -> ('a1, 'a2, 'a4) iO) -> ('a3 -> __ -> __ -> 'a5) -> 'a5 **)
407let bindIO_opt_interact m clearme f o k x =
408  (match clearme with
409   | Types.None ->
410     (fun f0 o0 k0 _ x0 _ ->
411       Obj.magic iO_discr (Wrong m) (Interact (o0, k0)) __)
412   | Types.Some a -> (fun f0 o0 k0 _ h _ -> h a __ __)) f o k __ x __
413
414(** val eq_to_rel_io__o__io_eq_from_res__o__inject :
415    'a2 Errors.res -> 'a2 -> __ Types.sig0 **)
416let eq_to_rel_io__o__io_eq_from_res__o__inject x3 x4 =
417  __
418
419(** val eq_to_rel_io__o__io_eq_from_res__o__opt_eq_from_res__o__inject :
420    Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 **)
421let eq_to_rel_io__o__io_eq_from_res__o__opt_eq_from_res__o__inject x2 x4 x5 =
422  Errors.opt_eq_from_res__o__inject x2 x4 x5
423
424(** val jmeq_to_eq__o__io_eq_from_res__o__inject :
425    'a2 Errors.res -> 'a2 -> __ Types.sig0 **)
426let jmeq_to_eq__o__io_eq_from_res__o__inject x3 x4 =
427  __
428
429(** val jmeq_to_eq__o__io_eq_from_res__o__opt_eq_from_res__o__inject :
430    Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 **)
431let jmeq_to_eq__o__io_eq_from_res__o__opt_eq_from_res__o__inject x1 x3 x4 =
432  Errors.opt_eq_from_res__o__inject x1 x3 x4
433
434(** val dpi1__o__io_eq_from_res__o__inject :
435    'a2 Errors.res -> 'a2 -> (__, 'a4) Types.dPair -> __ Types.sig0 **)
436let dpi1__o__io_eq_from_res__o__inject x3 x4 x7 =
437  __
438
439(** val dpi1__o__io_eq_from_res__o__opt_eq_from_res__o__inject :
440    Errors.errmsg -> 'a1 Types.option -> 'a1 -> (__, 'a4) Types.dPair -> __
441    Types.sig0 **)
442let dpi1__o__io_eq_from_res__o__opt_eq_from_res__o__inject x1 x3 x4 x8 =
443  Errors.opt_eq_from_res__o__inject x1 x3 x4
444
445(** val eject__o__io_eq_from_res__o__inject :
446    'a2 Errors.res -> 'a2 -> __ Types.sig0 -> __ Types.sig0 **)
447let eject__o__io_eq_from_res__o__inject x3 x4 x7 =
448  __
449
450(** val eject__o__io_eq_from_res__o__opt_eq_from_res__o__inject :
451    Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 -> __
452    Types.sig0 **)
453let eject__o__io_eq_from_res__o__opt_eq_from_res__o__inject x1 x3 x4 x8 =
454  Errors.opt_eq_from_res__o__inject x1 x3 x4
455
456(** val io_eq_from_res__o__opt_eq_from_res__o__inject :
457    Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 **)
458let io_eq_from_res__o__opt_eq_from_res__o__inject x1 x3 x4 =
459  Errors.opt_eq_from_res__o__inject x1 x3 x4
460
461(** val io_eq_from_res__o__inject :
462    'a2 Errors.res -> 'a2 -> __ Types.sig0 **)
463let io_eq_from_res__o__inject x3 x4 =
464  __
465
466(** val jmeq_to_eq__o__io_monad_eq_from_res__o__inject :
467    'a2 Errors.res -> 'a2 -> __ Types.sig0 **)
468let jmeq_to_eq__o__io_monad_eq_from_res__o__inject x3 x4 =
469  __
470
471(** val jmeq_to_eq__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject :
472    Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 **)
473let jmeq_to_eq__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject x1 x3 x4 =
474  Errors.opt_eq_from_res__o__inject x1 x3 x4
475
476(** val dpi1__o__io_monad_eq_from_res__o__inject :
477    'a2 Errors.res -> 'a2 -> (__, 'a4) Types.dPair -> __ Types.sig0 **)
478let dpi1__o__io_monad_eq_from_res__o__inject x3 x4 x7 =
479  __
480
481(** val dpi1__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject :
482    Errors.errmsg -> 'a1 Types.option -> 'a1 -> (__, 'a4) Types.dPair -> __
483    Types.sig0 **)
484let dpi1__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject x1 x3 x4 x8 =
485  Errors.opt_eq_from_res__o__inject x1 x3 x4
486
487(** val eject__o__io_monad_eq_from_res__o__inject :
488    'a2 Errors.res -> 'a2 -> __ Types.sig0 -> __ Types.sig0 **)
489let eject__o__io_monad_eq_from_res__o__inject x3 x4 x7 =
490  __
491
492(** val eject__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject :
493    Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 -> __
494    Types.sig0 **)
495let eject__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject x1 x3 x4 x8 =
496  Errors.opt_eq_from_res__o__inject x1 x3 x4
497
498(** val io_monad_eq_from_res__o__opt_eq_from_res__o__inject :
499    Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 **)
500let io_monad_eq_from_res__o__opt_eq_from_res__o__inject x1 x3 x4 =
501  Errors.opt_eq_from_res__o__inject x1 x3 x4
502
503(** val io_monad_eq_from_res__o__inject :
504    'a2 Errors.res -> 'a2 -> __ Types.sig0 **)
505let io_monad_eq_from_res__o__inject x3 x4 =
506  __
507
508(** val eq_to_rel_io__o__io_eq_from_opt__o__inject :
509    Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 **)
510let eq_to_rel_io__o__io_eq_from_opt__o__inject x2 x4 x5 =
511  __
512
513(** val jmeq_to_eq__o__io_eq_from_opt__o__inject :
514    Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 **)
515let jmeq_to_eq__o__io_eq_from_opt__o__inject x2 x4 x5 =
516  __
517
518(** val dpi1__o__io_eq_from_opt__o__inject :
519    Errors.errmsg -> 'a2 Types.option -> 'a2 -> (__, 'a4) Types.dPair -> __
520    Types.sig0 **)
521let dpi1__o__io_eq_from_opt__o__inject x2 x4 x5 x8 =
522  __
523
524(** val eject__o__io_eq_from_opt__o__inject :
525    Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 -> __
526    Types.sig0 **)
527let eject__o__io_eq_from_opt__o__inject x2 x4 x5 x8 =
528  __
529
530(** val io_eq_from_opt__o__inject :
531    Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 **)
532let io_eq_from_opt__o__inject x2 x4 x5 =
533  __
534
535(** val jmeq_to_eq__o__io_monad_eq_from_opt__o__inject :
536    Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 **)
537let jmeq_to_eq__o__io_monad_eq_from_opt__o__inject x2 x4 x5 =
538  __
539
540(** val dpi1__o__io_monad_eq_from_opt__o__inject :
541    Errors.errmsg -> 'a2 Types.option -> 'a2 -> (__, 'a4) Types.dPair -> __
542    Types.sig0 **)
543let dpi1__o__io_monad_eq_from_opt__o__inject x2 x4 x5 x8 =
544  __
545
546(** val eject__o__io_monad_eq_from_opt__o__inject :
547    Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 -> __
548    Types.sig0 **)
549let eject__o__io_monad_eq_from_opt__o__inject x2 x4 x5 x8 =
550  __
551
552(** val io_monad_eq_from_opt__o__inject :
553    Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 **)
554let io_monad_eq_from_opt__o__inject x2 x4 x5 =
555  __
556
Note: See TracBrowser for help on using the repository browser.