source: extracted/iOMonad.ml @ 2746

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

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File size: 18.7 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_4633) ->
55  h_Interact o x_4633 (fun x_4632 ->
56    iO_rect_Type4 h_Interact h_Value h_Wrong (x_4633 x_4632))
57| Value x_4634 -> h_Value x_4634
58| Wrong x_4635 -> h_Wrong x_4635
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_4649) ->
65  h_Interact o x_4649 (fun x_4648 ->
66    iO_rect_Type3 h_Interact h_Value h_Wrong (x_4649 x_4648))
67| Value x_4650 -> h_Value x_4650
68| Wrong x_4651 -> h_Wrong x_4651
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_4657) ->
75  h_Interact o x_4657 (fun x_4656 ->
76    iO_rect_Type2 h_Interact h_Value h_Wrong (x_4657 x_4656))
77| Value x_4658 -> h_Value x_4658
78| Wrong x_4659 -> h_Wrong x_4659
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_4665) ->
85  h_Interact o x_4665 (fun x_4664 ->
86    iO_rect_Type1 h_Interact h_Value h_Wrong (x_4665 x_4664))
87| Value x_4666 -> h_Value x_4666
88| Wrong x_4667 -> h_Wrong x_4667
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_4673) ->
95  h_Interact o x_4673 (fun x_4672 ->
96    iO_rect_Type0 h_Interact h_Value h_Wrong (x_4673 x_4672))
97| Value x_4674 -> h_Value x_4674
98| Wrong x_4675 -> h_Wrong x_4675
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 res1 -> bindIO (k res1) 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
169type ('x, 'x0, 'x1, 'x2) rel_io = __
170
171(** val iORel : Monad.monadRel **)
172let iORel =
173  Monad.Mk_MonadRel
174
175type ('x, 'x0, 'x1) pred_io = __
176
177(** val pred_io_inject :
178    ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3 Types.sig0) iO **)
179let rec pred_io_inject a =
180  (match a with
181   | Interact (o, f) ->
182     (fun _ -> Interact (o, (fun x -> pred_io_inject (f x))))
183   | Value x ->
184     (fun _ -> Obj.magic (Monad.m_return0 (Monad.max_def iOMonad) x))
185   | Wrong e0 -> (fun _ -> Wrong e0)) __
186
187(** val iOPred : Monad.injMonadPred **)
188let iOPred =
189  { Monad.im_pred = Monad.Mk_MonadPred; Monad.mp_inject = (fun _ _ a_sig ->
190    let a = a_sig in Obj.magic (pred_io_inject (Obj.magic a))) }
191
192(** val err_to_io : 'a3 Errors.res -> ('a1, 'a2, 'a3) iO **)
193let err_to_io = function
194| Errors.OK v' -> Value v'
195| Errors.Error m -> Wrong m
196
197(** val dpi1__o__err_to_io__o__inject :
198    ('a2 Errors.res, 'a3) Types.dPair -> ('a1, 'a4, 'a2) iO Types.sig0 **)
199let dpi1__o__err_to_io__o__inject x4 =
200  err_to_io x4.Types.dpi1
201
202(** val eject__o__err_to_io__o__inject :
203    'a2 Errors.res Types.sig0 -> ('a1, 'a3, 'a2) iO Types.sig0 **)
204let eject__o__err_to_io__o__inject x4 =
205  err_to_io (Types.pi1 x4)
206
207(** val err_to_io__o__inject :
208    'a2 Errors.res -> ('a1, 'a3, 'a2) iO Types.sig0 **)
209let err_to_io__o__inject x3 =
210  err_to_io x3
211
212(** val dpi1__o__err_to_io :
213    ('a2 Errors.res, 'a3) Types.dPair -> ('a1, 'a4, 'a2) iO **)
214let dpi1__o__err_to_io x4 =
215  err_to_io x4.Types.dpi1
216
217(** val eject__o__err_to_io :
218    'a2 Errors.res Types.sig0 -> ('a1, 'a3, 'a2) iO **)
219let eject__o__err_to_io x4 =
220  err_to_io (Types.pi1 x4)
221
222(** val err_to_io_sig :
223    'a3 Types.sig0 Errors.res -> ('a1, 'a2, 'a3 Types.sig0) iO **)
224let err_to_io_sig = function
225| Errors.OK v' -> Value v'
226| Errors.Error m -> Wrong m
227
228type ('x, 'x0, 'x1) p_io = __
229
230type ('x, 'x0, 'x1) p_io' = __
231
232(** val io_inject_0 : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3 Types.sig0) iO **)
233let rec io_inject_0 a =
234  (match a with
235   | Interact (out, k) ->
236     (fun _ -> Interact (out, (fun v -> io_inject_0 (k v))))
237   | Value c -> (fun _ -> Value c)
238   | Wrong m -> (fun _ -> Wrong m)) __
239
240(** val io_inject :
241    ('a1, 'a2, 'a3) iO Types.option -> ('a1, 'a2, 'a3 Types.sig0) iO **)
242let io_inject a =
243  (match a with
244   | Types.None -> (fun _ -> Logic.false_rect_Type0 __)
245   | Types.Some b -> (fun _ -> io_inject_0 b)) __
246
247(** val io_eject : ('a1, 'a2, 'a3 Types.sig0) iO -> ('a1, 'a2, 'a3) iO **)
248let rec io_eject = function
249| Interact (out, k) -> Interact (out, (fun v -> io_eject (k v)))
250| Value b -> let w = b in Value w
251| Wrong m -> Wrong m
252
253(** val dpi1__o__io_inject__o__inject :
254    (('a1, 'a3, 'a2) iO Types.option, 'a4) Types.dPair -> ('a1, 'a3, 'a2
255    Types.sig0) iO Types.sig0 **)
256let dpi1__o__io_inject__o__inject x6 =
257  io_inject x6.Types.dpi1
258
259(** val eject__o__io_inject__o__inject :
260    ('a1, 'a3, 'a2) iO Types.option Types.sig0 -> ('a1, 'a3, 'a2 Types.sig0)
261    iO Types.sig0 **)
262let eject__o__io_inject__o__inject x6 =
263  io_inject (Types.pi1 x6)
264
265(** val io_inject__o__inject :
266    ('a1, 'a3, 'a2) iO Types.option -> ('a1, 'a3, 'a2 Types.sig0) iO
267    Types.sig0 **)
268let io_inject__o__inject x5 =
269  io_inject x5
270
271(** val dpi1__o__io_inject :
272    (('a1, 'a3, 'a2) iO Types.option, 'a4) Types.dPair -> ('a1, 'a3, 'a2
273    Types.sig0) iO **)
274let dpi1__o__io_inject x5 =
275  io_inject x5.Types.dpi1
276
277(** val eject__o__io_inject :
278    ('a1, 'a3, 'a2) iO Types.option Types.sig0 -> ('a1, 'a3, 'a2 Types.sig0)
279    iO **)
280let eject__o__io_inject x5 =
281  io_inject (Types.pi1 x5)
282
283(** val io_inject__o__io_eject__o__inject :
284    ('a1, 'a3, 'a2) iO Types.option -> ('a1, 'a3, 'a2) iO Types.sig0 **)
285let io_inject__o__io_eject__o__inject x4 =
286  io_eject (io_inject x4)
287
288(** val dpi1__o__err_to_io__o__io_eject__o__inject :
289    ('a2 Types.sig0 Errors.res, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO
290    Types.sig0 **)
291let dpi1__o__err_to_io__o__io_eject__o__inject x6 =
292  io_eject (dpi1__o__err_to_io x6)
293
294(** val dpi1__o__io_inject__o__io_eject__o__inject :
295    (('a1, 'a3, 'a2) iO Types.option, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO
296    Types.sig0 **)
297let dpi1__o__io_inject__o__io_eject__o__inject x6 =
298  io_eject (dpi1__o__io_inject x6)
299
300(** val eject__o__err_to_io__o__io_eject__o__inject :
301    'a2 Types.sig0 Errors.res Types.sig0 -> ('a1, 'a3, 'a2) iO Types.sig0 **)
302let eject__o__err_to_io__o__io_eject__o__inject x6 =
303  io_eject (eject__o__err_to_io x6)
304
305(** val eject__o__io_inject__o__io_eject__o__inject :
306    ('a1, 'a3, 'a2) iO Types.option Types.sig0 -> ('a1, 'a3, 'a2) iO
307    Types.sig0 **)
308let eject__o__io_inject__o__io_eject__o__inject x6 =
309  io_eject (eject__o__io_inject x6)
310
311(** val err_to_io__o__io_eject__o__inject :
312    'a2 Types.sig0 Errors.res -> ('a1, 'a3, 'a2) iO Types.sig0 **)
313let err_to_io__o__io_eject__o__inject x4 =
314  io_eject (err_to_io x4)
315
316(** val dpi1__o__io_eject__o__inject :
317    (('a1, 'a3, 'a2 Types.sig0) iO, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO
318    Types.sig0 **)
319let dpi1__o__io_eject__o__inject x6 =
320  io_eject x6.Types.dpi1
321
322(** val eject__o__io_eject__o__inject :
323    ('a1, 'a3, 'a2 Types.sig0) iO Types.sig0 -> ('a1, 'a3, 'a2) iO Types.sig0 **)
324let eject__o__io_eject__o__inject x6 =
325  io_eject (Types.pi1 x6)
326
327(** val io_eject__o__inject :
328    ('a1, 'a3, 'a2 Types.sig0) iO -> ('a1, 'a3, 'a2) iO Types.sig0 **)
329let io_eject__o__inject x5 =
330  io_eject x5
331
332(** val io_inject__o__io_eject :
333    ('a1, 'a3, 'a2) iO Types.option -> ('a1, 'a3, 'a2) iO **)
334let io_inject__o__io_eject x4 =
335  io_eject (io_inject x4)
336
337(** val dpi1__o__err_to_io__o__io_eject :
338    ('a2 Types.sig0 Errors.res, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO **)
339let dpi1__o__err_to_io__o__io_eject x5 =
340  io_eject (dpi1__o__err_to_io x5)
341
342(** val dpi1__o__io_inject__o__io_eject :
343    (('a1, 'a3, 'a2) iO Types.option, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO **)
344let dpi1__o__io_inject__o__io_eject x5 =
345  io_eject (dpi1__o__io_inject x5)
346
347(** val eject__o__err_to_io__o__io_eject :
348    'a2 Types.sig0 Errors.res Types.sig0 -> ('a1, 'a3, 'a2) iO **)
349let eject__o__err_to_io__o__io_eject x5 =
350  io_eject (eject__o__err_to_io x5)
351
352(** val eject__o__io_inject__o__io_eject :
353    ('a1, 'a3, 'a2) iO Types.option Types.sig0 -> ('a1, 'a3, 'a2) iO **)
354let eject__o__io_inject__o__io_eject x5 =
355  io_eject (eject__o__io_inject x5)
356
357(** val err_to_io__o__io_eject :
358    'a2 Types.sig0 Errors.res -> ('a1, 'a3, 'a2) iO **)
359let err_to_io__o__io_eject x4 =
360  io_eject (err_to_io x4)
361
362(** val dpi1__o__io_eject :
363    (('a1, 'a3, 'a2 Types.sig0) iO, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO **)
364let dpi1__o__io_eject x5 =
365  io_eject x5.Types.dpi1
366
367(** val eject__o__io_eject :
368    ('a1, 'a3, 'a2 Types.sig0) iO Types.sig0 -> ('a1, 'a3, 'a2) iO **)
369let eject__o__io_eject x5 =
370  io_eject (Types.pi1 x5)
371
372(** val opt_to_io :
373    Errors.errmsg -> 'a3 Types.option -> ('a1, 'a2, 'a3) iO **)
374let opt_to_io m = function
375| Types.None -> Wrong m
376| Types.Some v' -> Value v'
377
378(** val bind_res_value :
379    'a3 Errors.res -> ('a3 -> 'a4 Errors.res) -> 'a4 -> ('a3 -> __ -> __ ->
380    'a5) -> 'a5 **)
381let bind_res_value clearme f v x =
382  (match clearme with
383   | Errors.OK a -> (fun f0 v0 _ h _ -> h a __ __)
384   | Errors.Error m ->
385     (fun f0 v0 _ h _ -> Obj.magic iO_discr (Wrong m) (Value v0) __)) f v __
386    x __
387
388(** val bindIO_value :
389    ('a1, 'a2, 'a3) iO -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a4 -> ('a3 -> __ ->
390    __ -> 'a5) -> 'a5 **)
391let bindIO_value clearme f v x =
392  (match clearme with
393   | Interact (o, k) ->
394     (fun f0 v0 _ h _ ->
395       Obj.magic iO_discr (Interact (o, (fun res1 -> bindIO (k res1) f0)))
396         (Value v0) __)
397   | Value a -> (fun f0 v0 _ h _ -> h a __ __)
398   | Wrong m ->
399     (fun f0 v0 _ h _ -> Obj.magic iO_discr (Wrong m) (Value v0) __)) f v __
400    x __
401
402(** val bindIO_res_interact :
403    'a3 Errors.res -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a1 -> ('a2 -> ('a1,
404    'a2, 'a4) iO) -> ('a3 -> __ -> __ -> 'a5) -> 'a5 **)
405let bindIO_res_interact clearme f o k x =
406  (match clearme with
407   | Errors.OK a -> (fun f0 o0 k0 _ h _ -> h a __ __)
408   | Errors.Error m ->
409     (fun f0 o0 k0 _ x0 _ ->
410       Obj.magic iO_discr (Wrong m) (Interact (o0, k0)) __)) f o k __ x __
411
412(** val bindIO_opt_interact :
413    Errors.errmsg -> 'a3 Types.option -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a1
414    -> ('a2 -> ('a1, 'a2, 'a4) iO) -> ('a3 -> __ -> __ -> 'a5) -> 'a5 **)
415let bindIO_opt_interact m clearme f o k x =
416  (match clearme with
417   | Types.None ->
418     (fun f0 o0 k0 _ x0 _ ->
419       Obj.magic iO_discr (Wrong m) (Interact (o0, k0)) __)
420   | Types.Some a -> (fun f0 o0 k0 _ h _ -> h a __ __)) f o k __ x __
421
422(** val eq_to_rel_io__o__io_eq_from_res__o__inject :
423    'a2 Errors.res -> 'a2 -> __ Types.sig0 **)
424let eq_to_rel_io__o__io_eq_from_res__o__inject x3 x4 =
425  __
426
427(** val eq_to_rel_io__o__io_eq_from_res__o__opt_eq_from_res__o__inject :
428    Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 **)
429let eq_to_rel_io__o__io_eq_from_res__o__opt_eq_from_res__o__inject x2 x4 x5 =
430  Errors.opt_eq_from_res__o__inject x2 x4 x5
431
432(** val jmeq_to_eq__o__io_eq_from_res__o__inject :
433    'a2 Errors.res -> 'a2 -> __ Types.sig0 **)
434let jmeq_to_eq__o__io_eq_from_res__o__inject x3 x4 =
435  __
436
437(** val jmeq_to_eq__o__io_eq_from_res__o__opt_eq_from_res__o__inject :
438    Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 **)
439let jmeq_to_eq__o__io_eq_from_res__o__opt_eq_from_res__o__inject x1 x3 x4 =
440  Errors.opt_eq_from_res__o__inject x1 x3 x4
441
442(** val dpi1__o__io_eq_from_res__o__inject :
443    'a2 Errors.res -> 'a2 -> (__, 'a4) Types.dPair -> __ Types.sig0 **)
444let dpi1__o__io_eq_from_res__o__inject x3 x4 x7 =
445  __
446
447(** val dpi1__o__io_eq_from_res__o__opt_eq_from_res__o__inject :
448    Errors.errmsg -> 'a1 Types.option -> 'a1 -> (__, 'a4) Types.dPair -> __
449    Types.sig0 **)
450let dpi1__o__io_eq_from_res__o__opt_eq_from_res__o__inject x1 x3 x4 x8 =
451  Errors.opt_eq_from_res__o__inject x1 x3 x4
452
453(** val eject__o__io_eq_from_res__o__inject :
454    'a2 Errors.res -> 'a2 -> __ Types.sig0 -> __ Types.sig0 **)
455let eject__o__io_eq_from_res__o__inject x3 x4 x7 =
456  __
457
458(** val eject__o__io_eq_from_res__o__opt_eq_from_res__o__inject :
459    Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 -> __
460    Types.sig0 **)
461let eject__o__io_eq_from_res__o__opt_eq_from_res__o__inject x1 x3 x4 x8 =
462  Errors.opt_eq_from_res__o__inject x1 x3 x4
463
464(** val io_eq_from_res__o__opt_eq_from_res__o__inject :
465    Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 **)
466let io_eq_from_res__o__opt_eq_from_res__o__inject x1 x3 x4 =
467  Errors.opt_eq_from_res__o__inject x1 x3 x4
468
469(** val io_eq_from_res__o__inject :
470    'a2 Errors.res -> 'a2 -> __ Types.sig0 **)
471let io_eq_from_res__o__inject x3 x4 =
472  __
473
474(** val jmeq_to_eq__o__io_monad_eq_from_res__o__inject :
475    'a2 Errors.res -> 'a2 -> __ Types.sig0 **)
476let jmeq_to_eq__o__io_monad_eq_from_res__o__inject x3 x4 =
477  __
478
479(** val jmeq_to_eq__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject :
480    Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 **)
481let jmeq_to_eq__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject x1 x3 x4 =
482  Errors.opt_eq_from_res__o__inject x1 x3 x4
483
484(** val dpi1__o__io_monad_eq_from_res__o__inject :
485    'a2 Errors.res -> 'a2 -> (__, 'a4) Types.dPair -> __ Types.sig0 **)
486let dpi1__o__io_monad_eq_from_res__o__inject x3 x4 x7 =
487  __
488
489(** val dpi1__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject :
490    Errors.errmsg -> 'a1 Types.option -> 'a1 -> (__, 'a4) Types.dPair -> __
491    Types.sig0 **)
492let dpi1__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject x1 x3 x4 x8 =
493  Errors.opt_eq_from_res__o__inject x1 x3 x4
494
495(** val eject__o__io_monad_eq_from_res__o__inject :
496    'a2 Errors.res -> 'a2 -> __ Types.sig0 -> __ Types.sig0 **)
497let eject__o__io_monad_eq_from_res__o__inject x3 x4 x7 =
498  __
499
500(** val eject__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject :
501    Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 -> __
502    Types.sig0 **)
503let eject__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject x1 x3 x4 x8 =
504  Errors.opt_eq_from_res__o__inject x1 x3 x4
505
506(** val io_monad_eq_from_res__o__opt_eq_from_res__o__inject :
507    Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 **)
508let io_monad_eq_from_res__o__opt_eq_from_res__o__inject x1 x3 x4 =
509  Errors.opt_eq_from_res__o__inject x1 x3 x4
510
511(** val io_monad_eq_from_res__o__inject :
512    'a2 Errors.res -> 'a2 -> __ Types.sig0 **)
513let io_monad_eq_from_res__o__inject x3 x4 =
514  __
515
516(** val eq_to_rel_io__o__io_eq_from_opt__o__inject :
517    Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 **)
518let eq_to_rel_io__o__io_eq_from_opt__o__inject x2 x4 x5 =
519  __
520
521(** val jmeq_to_eq__o__io_eq_from_opt__o__inject :
522    Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 **)
523let jmeq_to_eq__o__io_eq_from_opt__o__inject x2 x4 x5 =
524  __
525
526(** val dpi1__o__io_eq_from_opt__o__inject :
527    Errors.errmsg -> 'a2 Types.option -> 'a2 -> (__, 'a4) Types.dPair -> __
528    Types.sig0 **)
529let dpi1__o__io_eq_from_opt__o__inject x2 x4 x5 x8 =
530  __
531
532(** val eject__o__io_eq_from_opt__o__inject :
533    Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 -> __
534    Types.sig0 **)
535let eject__o__io_eq_from_opt__o__inject x2 x4 x5 x8 =
536  __
537
538(** val io_eq_from_opt__o__inject :
539    Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 **)
540let io_eq_from_opt__o__inject x2 x4 x5 =
541  __
542
543(** val jmeq_to_eq__o__io_monad_eq_from_opt__o__inject :
544    Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 **)
545let jmeq_to_eq__o__io_monad_eq_from_opt__o__inject x2 x4 x5 =
546  __
547
548(** val dpi1__o__io_monad_eq_from_opt__o__inject :
549    Errors.errmsg -> 'a2 Types.option -> 'a2 -> (__, 'a4) Types.dPair -> __
550    Types.sig0 **)
551let dpi1__o__io_monad_eq_from_opt__o__inject x2 x4 x5 x8 =
552  __
553
554(** val eject__o__io_monad_eq_from_opt__o__inject :
555    Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 -> __
556    Types.sig0 **)
557let eject__o__io_monad_eq_from_opt__o__inject x2 x4 x5 x8 =
558  __
559
560(** val io_monad_eq_from_opt__o__inject :
561    Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 **)
562let io_monad_eq_from_opt__o__inject x2 x4 x5 =
563  __
564
Note: See TracBrowser for help on using the repository browser.