source: driver/extracted/monad.ml @ 3106

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

The compiler now computes also the stack cost model.

File size: 20.1 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Types
12
13open Relations
14
15open Setoids
16
17type ('a, 'b) pred_transformer = __
18
19type ('a, 'b, 'c, 'd) rel_transformer = __
20
21type monad = { m_return : (__ -> __ -> __);
22               m_bind : (__ -> __ -> __ -> (__ -> __) -> __) }
23
24(** val monad_rect_Type4 :
25    (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1)
26    -> monad -> 'a1 **)
27let rec monad_rect_Type4 h_mk_Monad x_744 =
28  let { m_return = m_return0; m_bind = m_bind0 } = x_744 in
29  h_mk_Monad __ m_return0 m_bind0
30
31(** val monad_rect_Type5 :
32    (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1)
33    -> monad -> 'a1 **)
34let rec monad_rect_Type5 h_mk_Monad x_746 =
35  let { m_return = m_return0; m_bind = m_bind0 } = x_746 in
36  h_mk_Monad __ m_return0 m_bind0
37
38(** val monad_rect_Type3 :
39    (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1)
40    -> monad -> 'a1 **)
41let rec monad_rect_Type3 h_mk_Monad x_748 =
42  let { m_return = m_return0; m_bind = m_bind0 } = x_748 in
43  h_mk_Monad __ m_return0 m_bind0
44
45(** val monad_rect_Type2 :
46    (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1)
47    -> monad -> 'a1 **)
48let rec monad_rect_Type2 h_mk_Monad x_750 =
49  let { m_return = m_return0; m_bind = m_bind0 } = x_750 in
50  h_mk_Monad __ m_return0 m_bind0
51
52(** val monad_rect_Type1 :
53    (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1)
54    -> monad -> 'a1 **)
55let rec monad_rect_Type1 h_mk_Monad x_752 =
56  let { m_return = m_return0; m_bind = m_bind0 } = x_752 in
57  h_mk_Monad __ m_return0 m_bind0
58
59(** val monad_rect_Type0 :
60    (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1)
61    -> monad -> 'a1 **)
62let rec monad_rect_Type0 h_mk_Monad x_754 =
63  let { m_return = m_return0; m_bind = m_bind0 } = x_754 in
64  h_mk_Monad __ m_return0 m_bind0
65
66type 'x monad0 = __
67
68(** val m_return0 : monad -> 'a1 -> __ **)
69let rec m_return0 xxx x_771 =
70  (let { m_return = yyy; m_bind = x0 } = xxx in Obj.magic yyy) __ x_771
71
72(** val m_bind0 : monad -> __ -> ('a1 -> __) -> __ **)
73let rec m_bind0 xxx x_768 x_769 =
74  (let { m_return = x0; m_bind = yyy } = xxx in Obj.magic yyy) __ __ x_768
75    x_769
76
77(** val monad_inv_rect_Type4 :
78    monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __)
79    -> __ -> 'a1) -> 'a1 **)
80let monad_inv_rect_Type4 hterm h1 =
81  let hcut = monad_rect_Type4 h1 hterm in hcut __
82
83(** val monad_inv_rect_Type3 :
84    monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __)
85    -> __ -> 'a1) -> 'a1 **)
86let monad_inv_rect_Type3 hterm h1 =
87  let hcut = monad_rect_Type3 h1 hterm in hcut __
88
89(** val monad_inv_rect_Type2 :
90    monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __)
91    -> __ -> 'a1) -> 'a1 **)
92let monad_inv_rect_Type2 hterm h1 =
93  let hcut = monad_rect_Type2 h1 hterm in hcut __
94
95(** val monad_inv_rect_Type1 :
96    monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __)
97    -> __ -> 'a1) -> 'a1 **)
98let monad_inv_rect_Type1 hterm h1 =
99  let hcut = monad_rect_Type1 h1 hterm in hcut __
100
101(** val monad_inv_rect_Type0 :
102    monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __)
103    -> __ -> 'a1) -> 'a1 **)
104let monad_inv_rect_Type0 hterm h1 =
105  let hcut = monad_rect_Type0 h1 hterm in hcut __
106
107type monadProps =
108  monad
109  (* singleton inductive, whose constructor was mk_MonadProps *)
110
111(** val monadProps_rect_Type4 :
112    (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1 **)
113let rec monadProps_rect_Type4 h_mk_MonadProps x_775 =
114  let max_def = x_775 in h_mk_MonadProps max_def __ __ __ __
115
116(** val monadProps_rect_Type5 :
117    (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1 **)
118let rec monadProps_rect_Type5 h_mk_MonadProps x_777 =
119  let max_def = x_777 in h_mk_MonadProps max_def __ __ __ __
120
121(** val monadProps_rect_Type3 :
122    (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1 **)
123let rec monadProps_rect_Type3 h_mk_MonadProps x_779 =
124  let max_def = x_779 in h_mk_MonadProps max_def __ __ __ __
125
126(** val monadProps_rect_Type2 :
127    (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1 **)
128let rec monadProps_rect_Type2 h_mk_MonadProps x_781 =
129  let max_def = x_781 in h_mk_MonadProps max_def __ __ __ __
130
131(** val monadProps_rect_Type1 :
132    (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1 **)
133let rec monadProps_rect_Type1 h_mk_MonadProps x_783 =
134  let max_def = x_783 in h_mk_MonadProps max_def __ __ __ __
135
136(** val monadProps_rect_Type0 :
137    (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1 **)
138let rec monadProps_rect_Type0 h_mk_MonadProps x_785 =
139  let max_def = x_785 in h_mk_MonadProps max_def __ __ __ __
140
141(** val max_def : monadProps -> monad **)
142let rec max_def xxx =
143  let yyy = xxx in yyy
144
145(** val monadProps_inv_rect_Type4 :
146    monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
147let monadProps_inv_rect_Type4 hterm h1 =
148  let hcut = monadProps_rect_Type4 h1 hterm in hcut __
149
150(** val monadProps_inv_rect_Type3 :
151    monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
152let monadProps_inv_rect_Type3 hterm h1 =
153  let hcut = monadProps_rect_Type3 h1 hterm in hcut __
154
155(** val monadProps_inv_rect_Type2 :
156    monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
157let monadProps_inv_rect_Type2 hterm h1 =
158  let hcut = monadProps_rect_Type2 h1 hterm in hcut __
159
160(** val monadProps_inv_rect_Type1 :
161    monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
162let monadProps_inv_rect_Type1 hterm h1 =
163  let hcut = monadProps_rect_Type1 h1 hterm in hcut __
164
165(** val monadProps_inv_rect_Type0 :
166    monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
167let monadProps_inv_rect_Type0 hterm h1 =
168  let hcut = monadProps_rect_Type0 h1 hterm in hcut __
169
170type 'x_772 max_def__o__monad = __
171
172type setoidMonadProps =
173  monad
174  (* singleton inductive, whose constructor was mk_SetoidMonadProps *)
175
176(** val setoidMonadProps_rect_Type4 :
177    (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
178    setoidMonadProps -> 'a1 **)
179let rec setoidMonadProps_rect_Type4 h_mk_SetoidMonadProps x_807 =
180  let smax_def = x_807 in
181  h_mk_SetoidMonadProps smax_def __ __ __ __ __ __ __ __ __
182
183(** val setoidMonadProps_rect_Type5 :
184    (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
185    setoidMonadProps -> 'a1 **)
186let rec setoidMonadProps_rect_Type5 h_mk_SetoidMonadProps x_809 =
187  let smax_def = x_809 in
188  h_mk_SetoidMonadProps smax_def __ __ __ __ __ __ __ __ __
189
190(** val setoidMonadProps_rect_Type3 :
191    (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
192    setoidMonadProps -> 'a1 **)
193let rec setoidMonadProps_rect_Type3 h_mk_SetoidMonadProps x_811 =
194  let smax_def = x_811 in
195  h_mk_SetoidMonadProps smax_def __ __ __ __ __ __ __ __ __
196
197(** val setoidMonadProps_rect_Type2 :
198    (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
199    setoidMonadProps -> 'a1 **)
200let rec setoidMonadProps_rect_Type2 h_mk_SetoidMonadProps x_813 =
201  let smax_def = x_813 in
202  h_mk_SetoidMonadProps smax_def __ __ __ __ __ __ __ __ __
203
204(** val setoidMonadProps_rect_Type1 :
205    (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
206    setoidMonadProps -> 'a1 **)
207let rec setoidMonadProps_rect_Type1 h_mk_SetoidMonadProps x_815 =
208  let smax_def = x_815 in
209  h_mk_SetoidMonadProps smax_def __ __ __ __ __ __ __ __ __
210
211(** val setoidMonadProps_rect_Type0 :
212    (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
213    setoidMonadProps -> 'a1 **)
214let rec setoidMonadProps_rect_Type0 h_mk_SetoidMonadProps x_817 =
215  let smax_def = x_817 in
216  h_mk_SetoidMonadProps smax_def __ __ __ __ __ __ __ __ __
217
218(** val smax_def : setoidMonadProps -> monad **)
219let rec smax_def xxx =
220  let yyy = xxx in yyy
221
222(** val setoidMonadProps_inv_rect_Type4 :
223    setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
224    __ -> __ -> __ -> 'a1) -> 'a1 **)
225let setoidMonadProps_inv_rect_Type4 hterm h1 =
226  let hcut = setoidMonadProps_rect_Type4 h1 hterm in hcut __
227
228(** val setoidMonadProps_inv_rect_Type3 :
229    setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
230    __ -> __ -> __ -> 'a1) -> 'a1 **)
231let setoidMonadProps_inv_rect_Type3 hterm h1 =
232  let hcut = setoidMonadProps_rect_Type3 h1 hterm in hcut __
233
234(** val setoidMonadProps_inv_rect_Type2 :
235    setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
236    __ -> __ -> __ -> 'a1) -> 'a1 **)
237let setoidMonadProps_inv_rect_Type2 hterm h1 =
238  let hcut = setoidMonadProps_rect_Type2 h1 hterm in hcut __
239
240(** val setoidMonadProps_inv_rect_Type1 :
241    setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
242    __ -> __ -> __ -> 'a1) -> 'a1 **)
243let setoidMonadProps_inv_rect_Type1 hterm h1 =
244  let hcut = setoidMonadProps_rect_Type1 h1 hterm in hcut __
245
246(** val setoidMonadProps_inv_rect_Type0 :
247    setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
248    __ -> __ -> __ -> 'a1) -> 'a1 **)
249let setoidMonadProps_inv_rect_Type0 hterm h1 =
250  let hcut = setoidMonadProps_rect_Type0 h1 hterm in hcut __
251
252type 'x_772 smax_def__o__monad = __
253
254(** val setoid_of_monad : setoidMonadProps -> Setoids.setoid **)
255let setoid_of_monad m =
256  Setoids.Mk_Setoid
257
258open Bool
259
260open Nat
261
262open List
263
264(** val m_map : monad -> ('a1 -> 'a2) -> __ -> __ **)
265let m_map m f m0 =
266  m_bind0 m m0 (fun x -> m_return0 m (f x))
267
268(** val m_map2 : monad -> ('a1 -> 'a2 -> 'a3) -> __ -> __ -> __ **)
269let m_map2 m f m0 n =
270  m_bind0 m m0 (fun x -> m_bind0 m n (fun y -> m_return0 m (f x y)))
271
272(** val m_bind2 : monad -> __ -> ('a1 -> 'a2 -> __) -> __ **)
273let m_bind2 m m0 f =
274  m_bind0 m m0 (fun p -> f p.Types.fst p.Types.snd)
275
276(** val m_bind3 : monad -> __ -> ('a1 -> 'a2 -> 'a3 -> __) -> __ **)
277let m_bind3 m m0 f =
278  m_bind0 m m0 (fun p ->
279    f p.Types.fst.Types.fst p.Types.fst.Types.snd p.Types.snd)
280
281(** val m_join : monad -> __ -> __ **)
282let m_join m m0 =
283  m_bind0 m m0 (fun x -> x)
284
285(** val m_sigbind2 : monad -> __ -> ('a1 -> 'a2 -> __ -> __) -> __ **)
286let m_sigbind2 m e f =
287  m_bind0 m e (fun e_sig ->
288    let p = e_sig in
289    (let { Types.fst = a; Types.snd = b } = p in (fun _ -> f a b __)) __)
290
291(** val m_list_map : monad -> ('a1 -> __) -> 'a1 List.list -> __ **)
292let m_list_map m f l =
293  List.foldr (fun el macc ->
294    m_bind0 m (f el) (fun r ->
295      m_bind0 m macc (fun acc -> m_return0 m (List.Cons (r, acc)))))
296    (m_return0 m List.Nil) l
297
298(** val m_list_map_sigma : monad -> ('a1 -> __) -> 'a1 List.list -> __ **)
299let m_list_map_sigma m f l =
300  List.foldr (fun el macc ->
301    m_bind0 m (f el) (fun eta285 ->
302      let r = eta285 in
303      m_bind0 m macc (fun eta284 ->
304        let acc = eta284 in m_return0 m (List.Cons (r, acc)))))
305    (m_return0 m List.Nil) l
306
307(** val m_bin_op : monad -> ('a1 -> 'a2 -> 'a3) -> __ -> __ -> __ **)
308let m_bin_op m op m0 n =
309  m_bind0 m m0 (fun x -> m_bind0 m n (fun y -> m_return0 m (op x y)))
310
311(** val m_fold :
312    monad -> ('a1 -> 'a2 -> __) -> 'a1 List.list -> 'a2 -> __ **)
313let rec m_fold m f l init =
314  match l with
315  | List.Nil -> m_return0 m init
316  | List.Cons (hd, tl) -> m_bind0 m (f hd init) (fun y -> m_fold m f tl y)
317
318(** val makeMonadProps :
319    (__ -> __ -> 'a1) -> (__ -> __ -> 'a1 -> (__ -> 'a1) -> 'a1) ->
320    monadProps **)
321let makeMonadProps m_return1 m_bind1 =
322  { m_return = (Obj.magic m_return1); m_bind = (Obj.magic m_bind1) }
323
324(** val makeSetoidMonadProps :
325    (__ -> __ -> 'a1) -> (__ -> __ -> 'a1 -> (__ -> 'a1) -> 'a1) ->
326    setoidMonadProps **)
327let makeSetoidMonadProps m_return1 m_bind1 =
328  { m_return = (Obj.magic m_return1); m_bind = (Obj.magic m_bind1) }
329
330open Jmeq
331
332open Russell
333
334type monadPred =
335| Mk_MonadPred
336
337(** val monadPred_rect_Type4 :
338    monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1 **)
339let rec monadPred_rect_Type4 m h_mk_MonadPred = function
340| Mk_MonadPred -> h_mk_MonadPred __ __ __ __
341
342(** val monadPred_rect_Type5 :
343    monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1 **)
344let rec monadPred_rect_Type5 m h_mk_MonadPred = function
345| Mk_MonadPred -> h_mk_MonadPred __ __ __ __
346
347(** val monadPred_rect_Type3 :
348    monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1 **)
349let rec monadPred_rect_Type3 m h_mk_MonadPred = function
350| Mk_MonadPred -> h_mk_MonadPred __ __ __ __
351
352(** val monadPred_rect_Type2 :
353    monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1 **)
354let rec monadPred_rect_Type2 m h_mk_MonadPred = function
355| Mk_MonadPred -> h_mk_MonadPred __ __ __ __
356
357(** val monadPred_rect_Type1 :
358    monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1 **)
359let rec monadPred_rect_Type1 m h_mk_MonadPred = function
360| Mk_MonadPred -> h_mk_MonadPred __ __ __ __
361
362(** val monadPred_rect_Type0 :
363    monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1 **)
364let rec monadPred_rect_Type0 m h_mk_MonadPred = function
365| Mk_MonadPred -> h_mk_MonadPred __ __ __ __
366
367(** val monadPred_inv_rect_Type4 :
368    monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
369let monadPred_inv_rect_Type4 x1 hterm h1 =
370  let hcut = monadPred_rect_Type4 x1 h1 hterm in hcut __
371
372(** val monadPred_inv_rect_Type3 :
373    monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
374let monadPred_inv_rect_Type3 x1 hterm h1 =
375  let hcut = monadPred_rect_Type3 x1 h1 hterm in hcut __
376
377(** val monadPred_inv_rect_Type2 :
378    monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
379let monadPred_inv_rect_Type2 x1 hterm h1 =
380  let hcut = monadPred_rect_Type2 x1 h1 hterm in hcut __
381
382(** val monadPred_inv_rect_Type1 :
383    monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
384let monadPred_inv_rect_Type1 x1 hterm h1 =
385  let hcut = monadPred_rect_Type1 x1 h1 hterm in hcut __
386
387(** val monadPred_inv_rect_Type0 :
388    monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
389let monadPred_inv_rect_Type0 x1 hterm h1 =
390  let hcut = monadPred_rect_Type0 x1 h1 hterm in hcut __
391
392(** val monadPred_jmdiscr : monad -> monadPred -> monadPred -> __ **)
393let monadPred_jmdiscr a1 x y =
394  Logic.eq_rect_Type2 x
395    (let Mk_MonadPred = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y
396
397type injMonadPred = { im_pred : monadPred;
398                      mp_inject : (__ -> __ -> __ Types.sig0 -> __) }
399
400(** val injMonadPred_rect_Type4 :
401    monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
402    injMonadPred -> 'a1 **)
403let rec injMonadPred_rect_Type4 m h_mk_InjMonadPred x_1048 =
404  let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1048 in
405  h_mk_InjMonadPred im_pred0 mp_inject0 __
406
407(** val injMonadPred_rect_Type5 :
408    monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
409    injMonadPred -> 'a1 **)
410let rec injMonadPred_rect_Type5 m h_mk_InjMonadPred x_1050 =
411  let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1050 in
412  h_mk_InjMonadPred im_pred0 mp_inject0 __
413
414(** val injMonadPred_rect_Type3 :
415    monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
416    injMonadPred -> 'a1 **)
417let rec injMonadPred_rect_Type3 m h_mk_InjMonadPred x_1052 =
418  let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1052 in
419  h_mk_InjMonadPred im_pred0 mp_inject0 __
420
421(** val injMonadPred_rect_Type2 :
422    monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
423    injMonadPred -> 'a1 **)
424let rec injMonadPred_rect_Type2 m h_mk_InjMonadPred x_1054 =
425  let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1054 in
426  h_mk_InjMonadPred im_pred0 mp_inject0 __
427
428(** val injMonadPred_rect_Type1 :
429    monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
430    injMonadPred -> 'a1 **)
431let rec injMonadPred_rect_Type1 m h_mk_InjMonadPred x_1056 =
432  let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1056 in
433  h_mk_InjMonadPred im_pred0 mp_inject0 __
434
435(** val injMonadPred_rect_Type0 :
436    monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
437    injMonadPred -> 'a1 **)
438let rec injMonadPred_rect_Type0 m h_mk_InjMonadPred x_1058 =
439  let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1058 in
440  h_mk_InjMonadPred im_pred0 mp_inject0 __
441
442(** val im_pred : monad -> injMonadPred -> monadPred **)
443let rec im_pred m xxx =
444  xxx.im_pred
445
446(** val mp_inject0 : monad -> injMonadPred -> __ Types.sig0 -> __ **)
447let rec mp_inject0 m xxx x_1073 =
448  (xxx.mp_inject) __ __ x_1073
449
450(** val injMonadPred_inv_rect_Type4 :
451    monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __)
452    -> __ -> __ -> 'a1) -> 'a1 **)
453let injMonadPred_inv_rect_Type4 x1 hterm h1 =
454  let hcut = injMonadPred_rect_Type4 x1 h1 hterm in hcut __
455
456(** val injMonadPred_inv_rect_Type3 :
457    monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __)
458    -> __ -> __ -> 'a1) -> 'a1 **)
459let injMonadPred_inv_rect_Type3 x1 hterm h1 =
460  let hcut = injMonadPred_rect_Type3 x1 h1 hterm in hcut __
461
462(** val injMonadPred_inv_rect_Type2 :
463    monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __)
464    -> __ -> __ -> 'a1) -> 'a1 **)
465let injMonadPred_inv_rect_Type2 x1 hterm h1 =
466  let hcut = injMonadPred_rect_Type2 x1 h1 hterm in hcut __
467
468(** val injMonadPred_inv_rect_Type1 :
469    monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __)
470    -> __ -> __ -> 'a1) -> 'a1 **)
471let injMonadPred_inv_rect_Type1 x1 hterm h1 =
472  let hcut = injMonadPred_rect_Type1 x1 h1 hterm in hcut __
473
474(** val injMonadPred_inv_rect_Type0 :
475    monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __)
476    -> __ -> __ -> 'a1) -> 'a1 **)
477let injMonadPred_inv_rect_Type0 x1 hterm h1 =
478  let hcut = injMonadPred_rect_Type0 x1 h1 hterm in hcut __
479
480(** val injMonadPred_jmdiscr :
481    monad -> injMonadPred -> injMonadPred -> __ **)
482let injMonadPred_jmdiscr a1 x y =
483  Logic.eq_rect_Type2 x
484    (let { im_pred = a0; mp_inject = a10 } = x in
485    Obj.magic (fun _ dH -> dH __ __ __)) y
486
487type monadRel =
488| Mk_MonadRel
489
490(** val monadRel_rect_Type4 :
491    monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1 **)
492let rec monadRel_rect_Type4 m1 m2 h_mk_MonadRel = function
493| Mk_MonadRel -> h_mk_MonadRel __ __ __ __
494
495(** val monadRel_rect_Type5 :
496    monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1 **)
497let rec monadRel_rect_Type5 m1 m2 h_mk_MonadRel = function
498| Mk_MonadRel -> h_mk_MonadRel __ __ __ __
499
500(** val monadRel_rect_Type3 :
501    monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1 **)
502let rec monadRel_rect_Type3 m1 m2 h_mk_MonadRel = function
503| Mk_MonadRel -> h_mk_MonadRel __ __ __ __
504
505(** val monadRel_rect_Type2 :
506    monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1 **)
507let rec monadRel_rect_Type2 m1 m2 h_mk_MonadRel = function
508| Mk_MonadRel -> h_mk_MonadRel __ __ __ __
509
510(** val monadRel_rect_Type1 :
511    monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1 **)
512let rec monadRel_rect_Type1 m1 m2 h_mk_MonadRel = function
513| Mk_MonadRel -> h_mk_MonadRel __ __ __ __
514
515(** val monadRel_rect_Type0 :
516    monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1 **)
517let rec monadRel_rect_Type0 m1 m2 h_mk_MonadRel = function
518| Mk_MonadRel -> h_mk_MonadRel __ __ __ __
519
520(** val monadRel_inv_rect_Type4 :
521    monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
522let monadRel_inv_rect_Type4 x1 x2 hterm h1 =
523  let hcut = monadRel_rect_Type4 x1 x2 h1 hterm in hcut __
524
525(** val monadRel_inv_rect_Type3 :
526    monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
527let monadRel_inv_rect_Type3 x1 x2 hterm h1 =
528  let hcut = monadRel_rect_Type3 x1 x2 h1 hterm in hcut __
529
530(** val monadRel_inv_rect_Type2 :
531    monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
532let monadRel_inv_rect_Type2 x1 x2 hterm h1 =
533  let hcut = monadRel_rect_Type2 x1 x2 h1 hterm in hcut __
534
535(** val monadRel_inv_rect_Type1 :
536    monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
537let monadRel_inv_rect_Type1 x1 x2 hterm h1 =
538  let hcut = monadRel_rect_Type1 x1 x2 h1 hterm in hcut __
539
540(** val monadRel_inv_rect_Type0 :
541    monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
542let monadRel_inv_rect_Type0 x1 x2 hterm h1 =
543  let hcut = monadRel_rect_Type0 x1 x2 h1 hterm in hcut __
544
545(** val monadRel_jmdiscr : monad -> monad -> monadRel -> monadRel -> __ **)
546let monadRel_jmdiscr a1 a2 x y =
547  Logic.eq_rect_Type2 x
548    (let Mk_MonadRel = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y
549
Note: See TracBrowser for help on using the repository browser.