source: extracted/iOMonad.ml @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

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 Option
32
33open Setoids
34
35open Monad
36
37open Positive
38
39open Char
40
41open String
42
43open PreIdentifiers
44
45open Errors
46
47type ('output, 'input, 't) iO =
48| Interact of 'output * ('input -> ('output, 'input, 't) iO)
49| Value of 't
50| Wrong of Errors.errmsg
51
52(** val iO_rect_Type4 :
53    ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 ->
54    'a4) -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4 **)
55let rec iO_rect_Type4 h_Interact h_Value h_Wrong = function
56| Interact (o, x_3606) ->
57  h_Interact o x_3606 (fun x_3605 ->
58    iO_rect_Type4 h_Interact h_Value h_Wrong (x_3606 x_3605))
59| Value x_3607 -> h_Value x_3607
60| Wrong x_3608 -> h_Wrong x_3608
61
62(** val iO_rect_Type3 :
63    ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 ->
64    'a4) -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4 **)
65let rec iO_rect_Type3 h_Interact h_Value h_Wrong = function
66| Interact (o, x_3622) ->
67  h_Interact o x_3622 (fun x_3621 ->
68    iO_rect_Type3 h_Interact h_Value h_Wrong (x_3622 x_3621))
69| Value x_3623 -> h_Value x_3623
70| Wrong x_3624 -> h_Wrong x_3624
71
72(** val iO_rect_Type2 :
73    ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 ->
74    'a4) -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4 **)
75let rec iO_rect_Type2 h_Interact h_Value h_Wrong = function
76| Interact (o, x_3630) ->
77  h_Interact o x_3630 (fun x_3629 ->
78    iO_rect_Type2 h_Interact h_Value h_Wrong (x_3630 x_3629))
79| Value x_3631 -> h_Value x_3631
80| Wrong x_3632 -> h_Wrong x_3632
81
82(** val iO_rect_Type1 :
83    ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 ->
84    'a4) -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4 **)
85let rec iO_rect_Type1 h_Interact h_Value h_Wrong = function
86| Interact (o, x_3638) ->
87  h_Interact o x_3638 (fun x_3637 ->
88    iO_rect_Type1 h_Interact h_Value h_Wrong (x_3638 x_3637))
89| Value x_3639 -> h_Value x_3639
90| Wrong x_3640 -> h_Wrong x_3640
91
92(** val iO_rect_Type0 :
93    ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 ->
94    'a4) -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4 **)
95let rec iO_rect_Type0 h_Interact h_Value h_Wrong = function
96| Interact (o, x_3646) ->
97  h_Interact o x_3646 (fun x_3645 ->
98    iO_rect_Type0 h_Interact h_Value h_Wrong (x_3646 x_3645))
99| Value x_3647 -> h_Value x_3647
100| Wrong x_3648 -> h_Wrong x_3648
101
102(** val iO_inv_rect_Type4 :
103    ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __
104    -> 'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ ->
105    'a4) -> 'a4 **)
106let iO_inv_rect_Type4 hterm h1 h2 h3 =
107  let hcut = iO_rect_Type4 h1 h2 h3 hterm in hcut __
108
109(** val iO_inv_rect_Type3 :
110    ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __
111    -> 'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ ->
112    'a4) -> 'a4 **)
113let iO_inv_rect_Type3 hterm h1 h2 h3 =
114  let hcut = iO_rect_Type3 h1 h2 h3 hterm in hcut __
115
116(** val iO_inv_rect_Type2 :
117    ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __
118    -> 'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ ->
119    'a4) -> 'a4 **)
120let iO_inv_rect_Type2 hterm h1 h2 h3 =
121  let hcut = iO_rect_Type2 h1 h2 h3 hterm in hcut __
122
123(** val iO_inv_rect_Type1 :
124    ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __
125    -> 'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ ->
126    'a4) -> 'a4 **)
127let iO_inv_rect_Type1 hterm h1 h2 h3 =
128  let hcut = iO_rect_Type1 h1 h2 h3 hterm in hcut __
129
130(** val iO_inv_rect_Type0 :
131    ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __
132    -> 'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ ->
133    'a4) -> 'a4 **)
134let iO_inv_rect_Type0 hterm h1 h2 h3 =
135  let hcut = iO_rect_Type0 h1 h2 h3 hterm in hcut __
136
137(** val iO_discr : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3) iO -> __ **)
138let iO_discr x y =
139  Logic.eq_rect_Type2 x
140    (match x with
141     | Interact (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
142     | Value a0 -> Obj.magic (fun _ dH -> dH __)
143     | Wrong a0 -> Obj.magic (fun _ dH -> dH __)) y
144
145(** val iO_jmdiscr : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3) iO -> __ **)
146let iO_jmdiscr x y =
147  Logic.eq_rect_Type2 x
148    (match x with
149     | Interact (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
150     | Value a0 -> Obj.magic (fun _ dH -> dH __)
151     | Wrong a0 -> Obj.magic (fun _ dH -> dH __)) y
152
153open Proper
154
155(** val bindIO :
156    ('a1, 'a2, 'a3) iO -> ('a3 -> ('a1, 'a2, 'a4) iO) -> ('a1, 'a2, 'a4) iO **)
157let rec bindIO v f =
158  match v with
159  | Interact (out, k) -> Interact (out, (fun res1 -> bindIO (k res1) f))
160  | Value v' -> f v'
161  | Wrong m -> Wrong m
162
163(** val iOMonad : Monad.monadProps **)
164let iOMonad =
165  Monad.makeMonadProps (fun _ x -> Value x) (fun _ _ -> bindIO)
166
167(** val bindIO2 : __ -> ('a3 -> 'a4 -> __) -> __ **)
168let bindIO2 m f =
169  Monad.m_bind2 (Monad.max_def iOMonad) m f
170
171type rel_io = __
172
173(** val iORel : Monad.monadRel **)
174let iORel =
175  Monad.Mk_MonadRel
176
177type pred_io = __
178
179(** val pred_io_inject :
180    ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3 Types.sig0) iO **)
181let rec pred_io_inject a =
182  (match a with
183   | Interact (o, f) ->
184     (fun _ -> Interact (o, (fun x -> pred_io_inject (f x))))
185   | Value x ->
186     (fun _ -> Obj.magic (Monad.m_return0 (Monad.max_def iOMonad) x))
187   | Wrong e0 -> (fun _ -> Wrong e0)) __
188
189(** val iOPred : Monad.injMonadPred **)
190let iOPred =
191  { Monad.im_pred = Monad.Mk_MonadPred; Monad.mp_inject = (fun _ _ a_sig ->
192    let a = a_sig in Obj.magic (pred_io_inject (Obj.magic a))) }
193
194(** val err_to_io : 'a3 Errors.res -> ('a1, 'a2, 'a3) iO **)
195let err_to_io = function
196| Errors.OK v' -> Value v'
197| Errors.Error m -> Wrong m
198
199(** val err_to_io_sig :
200    'a3 Types.sig0 Errors.res -> ('a1, 'a2, 'a3 Types.sig0) iO **)
201let err_to_io_sig = function
202| Errors.OK v' -> Value v'
203| Errors.Error m -> Wrong m
204
205type p_io = __
206
207type p_io' = __
208
209(** val io_inject_0 : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3 Types.sig0) iO **)
210let rec io_inject_0 a =
211  (match a with
212   | Interact (out, k) ->
213     (fun _ -> Interact (out, (fun v -> io_inject_0 (k v))))
214   | Value c -> (fun _ -> Value c)
215   | Wrong m -> (fun _ -> Wrong m)) __
216
217(** val io_inject :
218    ('a1, 'a2, 'a3) iO Types.option -> ('a1, 'a2, 'a3 Types.sig0) iO **)
219let io_inject a =
220  (match a with
221   | Types.None -> (fun _ -> Logic.false_rect_Type0 __)
222   | Types.Some b -> (fun _ -> io_inject_0 b)) __
223
224(** val io_eject : ('a1, 'a2, 'a3 Types.sig0) iO -> ('a1, 'a2, 'a3) iO **)
225let rec io_eject = function
226| Interact (out, k) -> Interact (out, (fun v -> io_eject (k v)))
227| Value b -> let w = b in Value w
228| Wrong m -> Wrong m
229
230(** val opt_to_io :
231    Errors.errmsg -> 'a3 Types.option -> ('a1, 'a2, 'a3) iO **)
232let opt_to_io m = function
233| Types.None -> Wrong m
234| Types.Some v' -> Value v'
235
236(** val bind_res_value :
237    'a3 Errors.res -> ('a3 -> 'a4 Errors.res) -> 'a4 -> ('a3 -> __ -> __ ->
238    'a5) -> 'a5 **)
239let bind_res_value clearme f v x =
240  (match clearme with
241   | Errors.OK a -> (fun f0 v0 _ h _ -> h a __ __)
242   | Errors.Error m ->
243     (fun f0 v0 _ h _ -> Obj.magic iO_discr (Wrong m) (Value v0) __)) f v __
244    x __
245
246(** val bindIO_value :
247    ('a1, 'a2, 'a3) iO -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a4 -> ('a3 -> __ ->
248    __ -> 'a5) -> 'a5 **)
249let bindIO_value clearme f v x =
250  (match clearme with
251   | Interact (o, k) ->
252     (fun f0 v0 _ h _ ->
253       Obj.magic iO_discr (Interact (o, (fun res1 -> bindIO (k res1) f0)))
254         (Value v0) __)
255   | Value a -> (fun f0 v0 _ h _ -> h a __ __)
256   | Wrong m ->
257     (fun f0 v0 _ h _ -> Obj.magic iO_discr (Wrong m) (Value v0) __)) f v __
258    x __
259
260(** val bindIO_res_interact :
261    'a3 Errors.res -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a1 -> ('a2 -> ('a1,
262    'a2, 'a4) iO) -> ('a3 -> __ -> __ -> 'a5) -> 'a5 **)
263let bindIO_res_interact clearme f o k x =
264  (match clearme with
265   | Errors.OK a -> (fun f0 o0 k0 _ h _ -> h a __ __)
266   | Errors.Error m ->
267     (fun f0 o0 k0 _ x0 _ ->
268       Obj.magic iO_discr (Wrong m) (Interact (o0, k0)) __)) f o k __ x __
269
270(** val bindIO_opt_interact :
271    Errors.errmsg -> 'a3 Types.option -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a1
272    -> ('a2 -> ('a1, 'a2, 'a4) iO) -> ('a3 -> __ -> __ -> 'a5) -> 'a5 **)
273let bindIO_opt_interact m clearme f o k x =
274  (match clearme with
275   | Types.None ->
276     (fun f0 o0 k0 _ x0 _ ->
277       Obj.magic iO_discr (Wrong m) (Interact (o0, k0)) __)
278   | Types.Some a -> (fun f0 o0 k0 _ h _ -> h a __ __)) f o k __ x __
279
Note: See TracBrowser for help on using the repository browser.