source: driver/extracted/extraMonads.ml @ 3106

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

New extraction

File size: 10.2 KB
Line 
1open Preamble
2
3open ErrorMessages
4
5open Option
6
7open Setoids
8
9open Monad
10
11open Jmeq
12
13open Russell
14
15open Positive
16
17open PreIdentifiers
18
19open Bool
20
21open Relations
22
23open Nat
24
25open List
26
27open Hints_declaration
28
29open Core_notation
30
31open Pts
32
33open Logic
34
35open Types
36
37open Errors
38
39open Proper
40
41open Div_and_mod
42
43open Util
44
45open Extralib
46
47open IOMonad
48
49type monadFunctRel =
50| Mk_MonadFunctRel
51
52(** val monadFunctRel_rect_Type4 :
53    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
54    monadFunctRel -> 'a1 **)
55let rec monadFunctRel_rect_Type4 m1 m2 h_mk_MonadFunctRel = function
56| Mk_MonadFunctRel -> h_mk_MonadFunctRel __ __ __ __
57
58(** val monadFunctRel_rect_Type5 :
59    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
60    monadFunctRel -> 'a1 **)
61let rec monadFunctRel_rect_Type5 m1 m2 h_mk_MonadFunctRel = function
62| Mk_MonadFunctRel -> h_mk_MonadFunctRel __ __ __ __
63
64(** val monadFunctRel_rect_Type3 :
65    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
66    monadFunctRel -> 'a1 **)
67let rec monadFunctRel_rect_Type3 m1 m2 h_mk_MonadFunctRel = function
68| Mk_MonadFunctRel -> h_mk_MonadFunctRel __ __ __ __
69
70(** val monadFunctRel_rect_Type2 :
71    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
72    monadFunctRel -> 'a1 **)
73let rec monadFunctRel_rect_Type2 m1 m2 h_mk_MonadFunctRel = function
74| Mk_MonadFunctRel -> h_mk_MonadFunctRel __ __ __ __
75
76(** val monadFunctRel_rect_Type1 :
77    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
78    monadFunctRel -> 'a1 **)
79let rec monadFunctRel_rect_Type1 m1 m2 h_mk_MonadFunctRel = function
80| Mk_MonadFunctRel -> h_mk_MonadFunctRel __ __ __ __
81
82(** val monadFunctRel_rect_Type0 :
83    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
84    monadFunctRel -> 'a1 **)
85let rec monadFunctRel_rect_Type0 m1 m2 h_mk_MonadFunctRel = function
86| Mk_MonadFunctRel -> h_mk_MonadFunctRel __ __ __ __
87
88(** val monadFunctRel_inv_rect_Type4 :
89    Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ ->
90    __ -> 'a1) -> 'a1 **)
91let monadFunctRel_inv_rect_Type4 x1 x2 hterm h1 =
92  let hcut = monadFunctRel_rect_Type4 x1 x2 h1 hterm in hcut __
93
94(** val monadFunctRel_inv_rect_Type3 :
95    Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ ->
96    __ -> 'a1) -> 'a1 **)
97let monadFunctRel_inv_rect_Type3 x1 x2 hterm h1 =
98  let hcut = monadFunctRel_rect_Type3 x1 x2 h1 hterm in hcut __
99
100(** val monadFunctRel_inv_rect_Type2 :
101    Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ ->
102    __ -> 'a1) -> 'a1 **)
103let monadFunctRel_inv_rect_Type2 x1 x2 hterm h1 =
104  let hcut = monadFunctRel_rect_Type2 x1 x2 h1 hterm in hcut __
105
106(** val monadFunctRel_inv_rect_Type1 :
107    Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ ->
108    __ -> 'a1) -> 'a1 **)
109let monadFunctRel_inv_rect_Type1 x1 x2 hterm h1 =
110  let hcut = monadFunctRel_rect_Type1 x1 x2 h1 hterm in hcut __
111
112(** val monadFunctRel_inv_rect_Type0 :
113    Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ ->
114    __ -> 'a1) -> 'a1 **)
115let monadFunctRel_inv_rect_Type0 x1 x2 hterm h1 =
116  let hcut = monadFunctRel_rect_Type0 x1 x2 h1 hterm in hcut __
117
118(** val monadFunctRel_jmdiscr :
119    Monad.monad -> Monad.monad -> monadFunctRel -> monadFunctRel -> __ **)
120let monadFunctRel_jmdiscr a1 a2 x y =
121  Logic.eq_rect_Type2 x
122    (let Mk_MonadFunctRel = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y
123
124type monadFunctRel1 =
125| Mk_MonadFunctRel1
126
127(** val monadFunctRel1_rect_Type4 :
128    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
129    monadFunctRel1 -> 'a1 **)
130let rec monadFunctRel1_rect_Type4 m1 m2 h_mk_MonadFunctRel1 = function
131| Mk_MonadFunctRel1 -> h_mk_MonadFunctRel1 __ __ __ __ __
132
133(** val monadFunctRel1_rect_Type5 :
134    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
135    monadFunctRel1 -> 'a1 **)
136let rec monadFunctRel1_rect_Type5 m1 m2 h_mk_MonadFunctRel1 = function
137| Mk_MonadFunctRel1 -> h_mk_MonadFunctRel1 __ __ __ __ __
138
139(** val monadFunctRel1_rect_Type3 :
140    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
141    monadFunctRel1 -> 'a1 **)
142let rec monadFunctRel1_rect_Type3 m1 m2 h_mk_MonadFunctRel1 = function
143| Mk_MonadFunctRel1 -> h_mk_MonadFunctRel1 __ __ __ __ __
144
145(** val monadFunctRel1_rect_Type2 :
146    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
147    monadFunctRel1 -> 'a1 **)
148let rec monadFunctRel1_rect_Type2 m1 m2 h_mk_MonadFunctRel1 = function
149| Mk_MonadFunctRel1 -> h_mk_MonadFunctRel1 __ __ __ __ __
150
151(** val monadFunctRel1_rect_Type1 :
152    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
153    monadFunctRel1 -> 'a1 **)
154let rec monadFunctRel1_rect_Type1 m1 m2 h_mk_MonadFunctRel1 = function
155| Mk_MonadFunctRel1 -> h_mk_MonadFunctRel1 __ __ __ __ __
156
157(** val monadFunctRel1_rect_Type0 :
158    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
159    monadFunctRel1 -> 'a1 **)
160let rec monadFunctRel1_rect_Type0 m1 m2 h_mk_MonadFunctRel1 = function
161| Mk_MonadFunctRel1 -> h_mk_MonadFunctRel1 __ __ __ __ __
162
163(** val monadFunctRel1_inv_rect_Type4 :
164    Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ ->
165    __ -> __ -> 'a1) -> 'a1 **)
166let monadFunctRel1_inv_rect_Type4 x1 x2 hterm h1 =
167  let hcut = monadFunctRel1_rect_Type4 x1 x2 h1 hterm in hcut __
168
169(** val monadFunctRel1_inv_rect_Type3 :
170    Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ ->
171    __ -> __ -> 'a1) -> 'a1 **)
172let monadFunctRel1_inv_rect_Type3 x1 x2 hterm h1 =
173  let hcut = monadFunctRel1_rect_Type3 x1 x2 h1 hterm in hcut __
174
175(** val monadFunctRel1_inv_rect_Type2 :
176    Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ ->
177    __ -> __ -> 'a1) -> 'a1 **)
178let monadFunctRel1_inv_rect_Type2 x1 x2 hterm h1 =
179  let hcut = monadFunctRel1_rect_Type2 x1 x2 h1 hterm in hcut __
180
181(** val monadFunctRel1_inv_rect_Type1 :
182    Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ ->
183    __ -> __ -> 'a1) -> 'a1 **)
184let monadFunctRel1_inv_rect_Type1 x1 x2 hterm h1 =
185  let hcut = monadFunctRel1_rect_Type1 x1 x2 h1 hterm in hcut __
186
187(** val monadFunctRel1_inv_rect_Type0 :
188    Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ ->
189    __ -> __ -> 'a1) -> 'a1 **)
190let monadFunctRel1_inv_rect_Type0 x1 x2 hterm h1 =
191  let hcut = monadFunctRel1_rect_Type0 x1 x2 h1 hterm in hcut __
192
193(** val monadFunctRel1_jmdiscr :
194    Monad.monad -> Monad.monad -> monadFunctRel1 -> monadFunctRel1 -> __ **)
195let monadFunctRel1_jmdiscr a1 a2 x y =
196  Logic.eq_rect_Type2 x
197    (let Mk_MonadFunctRel1 = x in Obj.magic (fun _ dH -> dH __ __ __ __ __))
198    y
199
200type monadGenRel =
201| Mk_MonadGenRel
202
203(** val monadGenRel_rect_Type4 :
204    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
205    monadGenRel -> 'a1 **)
206let rec monadGenRel_rect_Type4 m1 m2 h_mk_MonadGenRel = function
207| Mk_MonadGenRel -> h_mk_MonadGenRel __ __ __ __ __
208
209(** val monadGenRel_rect_Type5 :
210    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
211    monadGenRel -> 'a1 **)
212let rec monadGenRel_rect_Type5 m1 m2 h_mk_MonadGenRel = function
213| Mk_MonadGenRel -> h_mk_MonadGenRel __ __ __ __ __
214
215(** val monadGenRel_rect_Type3 :
216    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
217    monadGenRel -> 'a1 **)
218let rec monadGenRel_rect_Type3 m1 m2 h_mk_MonadGenRel = function
219| Mk_MonadGenRel -> h_mk_MonadGenRel __ __ __ __ __
220
221(** val monadGenRel_rect_Type2 :
222    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
223    monadGenRel -> 'a1 **)
224let rec monadGenRel_rect_Type2 m1 m2 h_mk_MonadGenRel = function
225| Mk_MonadGenRel -> h_mk_MonadGenRel __ __ __ __ __
226
227(** val monadGenRel_rect_Type1 :
228    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
229    monadGenRel -> 'a1 **)
230let rec monadGenRel_rect_Type1 m1 m2 h_mk_MonadGenRel = function
231| Mk_MonadGenRel -> h_mk_MonadGenRel __ __ __ __ __
232
233(** val monadGenRel_rect_Type0 :
234    Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
235    monadGenRel -> 'a1 **)
236let rec monadGenRel_rect_Type0 m1 m2 h_mk_MonadGenRel = function
237| Mk_MonadGenRel -> h_mk_MonadGenRel __ __ __ __ __
238
239(** val monadGenRel_inv_rect_Type4 :
240    Monad.monad -> Monad.monad -> monadGenRel -> (__ -> __ -> __ -> __ -> __
241    -> __ -> 'a1) -> 'a1 **)
242let monadGenRel_inv_rect_Type4 x1 x2 hterm h1 =
243  let hcut = monadGenRel_rect_Type4 x1 x2 h1 hterm in hcut __
244
245(** val monadGenRel_inv_rect_Type3 :
246    Monad.monad -> Monad.monad -> monadGenRel -> (__ -> __ -> __ -> __ -> __
247    -> __ -> 'a1) -> 'a1 **)
248let monadGenRel_inv_rect_Type3 x1 x2 hterm h1 =
249  let hcut = monadGenRel_rect_Type3 x1 x2 h1 hterm in hcut __
250
251(** val monadGenRel_inv_rect_Type2 :
252    Monad.monad -> Monad.monad -> monadGenRel -> (__ -> __ -> __ -> __ -> __
253    -> __ -> 'a1) -> 'a1 **)
254let monadGenRel_inv_rect_Type2 x1 x2 hterm h1 =
255  let hcut = monadGenRel_rect_Type2 x1 x2 h1 hterm in hcut __
256
257(** val monadGenRel_inv_rect_Type1 :
258    Monad.monad -> Monad.monad -> monadGenRel -> (__ -> __ -> __ -> __ -> __
259    -> __ -> 'a1) -> 'a1 **)
260let monadGenRel_inv_rect_Type1 x1 x2 hterm h1 =
261  let hcut = monadGenRel_rect_Type1 x1 x2 h1 hterm in hcut __
262
263(** val monadGenRel_inv_rect_Type0 :
264    Monad.monad -> Monad.monad -> monadGenRel -> (__ -> __ -> __ -> __ -> __
265    -> __ -> 'a1) -> 'a1 **)
266let monadGenRel_inv_rect_Type0 x1 x2 hterm h1 =
267  let hcut = monadGenRel_rect_Type0 x1 x2 h1 hterm in hcut __
268
269(** val monadGenRel_jmdiscr :
270    Monad.monad -> Monad.monad -> monadGenRel -> monadGenRel -> __ **)
271let monadGenRel_jmdiscr a1 a2 x y =
272  Logic.eq_rect_Type2 x
273    (let Mk_MonadGenRel = x in Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
274
275(** val res_preserve : monadFunctRel **)
276let res_preserve =
277  Mk_MonadFunctRel
278
279(** val res_preserve1 : monadFunctRel1 **)
280let res_preserve1 =
281  Mk_MonadFunctRel1
282
283(** val gen_res_preserve : monadGenRel **)
284let gen_res_preserve =
285  Mk_MonadGenRel
286
287(** val opt_preserve : monadFunctRel **)
288let opt_preserve =
289  Mk_MonadFunctRel
290
291(** val opt_preserve1 : monadFunctRel1 **)
292let opt_preserve1 =
293  Mk_MonadFunctRel1
294
295(** val gen_opt_preserve : monadGenRel **)
296let gen_opt_preserve =
297  Mk_MonadGenRel
298
299(** val io_preserve : monadFunctRel **)
300let io_preserve =
301  Mk_MonadFunctRel
302
303(** val io_preserve1 : monadFunctRel1 **)
304let io_preserve1 =
305  Mk_MonadFunctRel1
306
307(** val gen_io_preserve : monadGenRel **)
308let gen_io_preserve =
309  Mk_MonadGenRel
310
Note: See TracBrowser for help on using the repository browser.