source: extracted/iOMonad.ml @ 2731

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

Exported again.

File size: 8.4 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_8433) ->
55  h_Interact o x_8433 (fun x_8432 ->
56    iO_rect_Type4 h_Interact h_Value h_Wrong (x_8433 x_8432))
57| Value x_8434 -> h_Value x_8434
58| Wrong x_8435 -> h_Wrong x_8435
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_8449) ->
65  h_Interact o x_8449 (fun x_8448 ->
66    iO_rect_Type3 h_Interact h_Value h_Wrong (x_8449 x_8448))
67| Value x_8450 -> h_Value x_8450
68| Wrong x_8451 -> h_Wrong x_8451
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_8457) ->
75  h_Interact o x_8457 (fun x_8456 ->
76    iO_rect_Type2 h_Interact h_Value h_Wrong (x_8457 x_8456))
77| Value x_8458 -> h_Value x_8458
78| Wrong x_8459 -> h_Wrong x_8459
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_8465) ->
85  h_Interact o x_8465 (fun x_8464 ->
86    iO_rect_Type1 h_Interact h_Value h_Wrong (x_8465 x_8464))
87| Value x_8466 -> h_Value x_8466
88| Wrong x_8467 -> h_Wrong x_8467
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_8473) ->
95  h_Interact o x_8473 (fun x_8472 ->
96    iO_rect_Type0 h_Interact h_Value h_Wrong (x_8473 x_8472))
97| Value x_8474 -> h_Value x_8474
98| Wrong x_8475 -> h_Wrong x_8475
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 rel_io = __
170
171(** val iORel : Monad.monadRel **)
172let iORel =
173  Monad.Mk_MonadRel
174
175type 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 err_to_io_sig :
198    'a3 Types.sig0 Errors.res -> ('a1, 'a2, 'a3 Types.sig0) iO **)
199let err_to_io_sig = function
200| Errors.OK v' -> Value v'
201| Errors.Error m -> Wrong m
202
203type p_io = __
204
205type p_io' = __
206
207(** val io_inject_0 : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3 Types.sig0) iO **)
208let rec io_inject_0 a =
209  (match a with
210   | Interact (out, k) ->
211     (fun _ -> Interact (out, (fun v -> io_inject_0 (k v))))
212   | Value c -> (fun _ -> Value c)
213   | Wrong m -> (fun _ -> Wrong m)) __
214
215(** val io_inject :
216    ('a1, 'a2, 'a3) iO Types.option -> ('a1, 'a2, 'a3 Types.sig0) iO **)
217let io_inject a =
218  (match a with
219   | Types.None -> (fun _ -> Logic.false_rect_Type0 __)
220   | Types.Some b -> (fun _ -> io_inject_0 b)) __
221
222(** val io_eject : ('a1, 'a2, 'a3 Types.sig0) iO -> ('a1, 'a2, 'a3) iO **)
223let rec io_eject = function
224| Interact (out, k) -> Interact (out, (fun v -> io_eject (k v)))
225| Value b -> let w = b in Value w
226| Wrong m -> Wrong m
227
228(** val opt_to_io :
229    Errors.errmsg -> 'a3 Types.option -> ('a1, 'a2, 'a3) iO **)
230let opt_to_io m = function
231| Types.None -> Wrong m
232| Types.Some v' -> Value v'
233
234(** val bind_res_value :
235    'a3 Errors.res -> ('a3 -> 'a4 Errors.res) -> 'a4 -> ('a3 -> __ -> __ ->
236    'a5) -> 'a5 **)
237let bind_res_value clearme f v x =
238  (match clearme with
239   | Errors.OK a -> (fun f0 v0 _ h _ -> h a __ __)
240   | Errors.Error m ->
241     (fun f0 v0 _ h _ -> Obj.magic iO_discr (Wrong m) (Value v0) __)) f v __
242    x __
243
244(** val bindIO_value :
245    ('a1, 'a2, 'a3) iO -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a4 -> ('a3 -> __ ->
246    __ -> 'a5) -> 'a5 **)
247let bindIO_value clearme f v x =
248  (match clearme with
249   | Interact (o, k) ->
250     (fun f0 v0 _ h _ ->
251       Obj.magic iO_discr (Interact (o, (fun res1 -> bindIO (k res1) f0)))
252         (Value v0) __)
253   | Value a -> (fun f0 v0 _ h _ -> h a __ __)
254   | Wrong m ->
255     (fun f0 v0 _ h _ -> Obj.magic iO_discr (Wrong m) (Value v0) __)) f v __
256    x __
257
258(** val bindIO_res_interact :
259    'a3 Errors.res -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a1 -> ('a2 -> ('a1,
260    'a2, 'a4) iO) -> ('a3 -> __ -> __ -> 'a5) -> 'a5 **)
261let bindIO_res_interact clearme f o k x =
262  (match clearme with
263   | Errors.OK a -> (fun f0 o0 k0 _ h _ -> h a __ __)
264   | Errors.Error m ->
265     (fun f0 o0 k0 _ x0 _ ->
266       Obj.magic iO_discr (Wrong m) (Interact (o0, k0)) __)) f o k __ x __
267
268(** val bindIO_opt_interact :
269    Errors.errmsg -> 'a3 Types.option -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a1
270    -> ('a2 -> ('a1, 'a2, 'a4) iO) -> ('a3 -> __ -> __ -> 'a5) -> 'a5 **)
271let bindIO_opt_interact m clearme f o k x =
272  (match clearme with
273   | Types.None ->
274     (fun f0 o0 k0 _ x0 _ ->
275       Obj.magic iO_discr (Wrong m) (Interact (o0, k0)) __)
276   | Types.Some a -> (fun f0 o0 k0 _ h _ -> h a __ __)) f o k __ x __
277
Note: See TracBrowser for help on using the repository browser.