17 open Hints_declaration
29 type ('b, 'e) bind_new =
31 | Bnew of ('b -> ('b, 'e) bind_new)
33 (** val bind_new_rect_Type4 :
34 ('a2 -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new) -> ('a1 -> 'a3) -> 'a3) ->
35 ('a1, 'a2) bind_new -> 'a3 **)
36 let rec bind_new_rect_Type4 h_bret h_bnew = function
37 | Bret x_18204 -> h_bret x_18204
39 h_bnew x_18206 (fun x_18205 ->
40 bind_new_rect_Type4 h_bret h_bnew (x_18206 x_18205))
42 (** val bind_new_rect_Type3 :
43 ('a2 -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new) -> ('a1 -> 'a3) -> 'a3) ->
44 ('a1, 'a2) bind_new -> 'a3 **)
45 let rec bind_new_rect_Type3 h_bret h_bnew = function
46 | Bret x_18216 -> h_bret x_18216
48 h_bnew x_18218 (fun x_18217 ->
49 bind_new_rect_Type3 h_bret h_bnew (x_18218 x_18217))
51 (** val bind_new_rect_Type2 :
52 ('a2 -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new) -> ('a1 -> 'a3) -> 'a3) ->
53 ('a1, 'a2) bind_new -> 'a3 **)
54 let rec bind_new_rect_Type2 h_bret h_bnew = function
55 | Bret x_18222 -> h_bret x_18222
57 h_bnew x_18224 (fun x_18223 ->
58 bind_new_rect_Type2 h_bret h_bnew (x_18224 x_18223))
60 (** val bind_new_rect_Type1 :
61 ('a2 -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new) -> ('a1 -> 'a3) -> 'a3) ->
62 ('a1, 'a2) bind_new -> 'a3 **)
63 let rec bind_new_rect_Type1 h_bret h_bnew = function
64 | Bret x_18228 -> h_bret x_18228
66 h_bnew x_18230 (fun x_18229 ->
67 bind_new_rect_Type1 h_bret h_bnew (x_18230 x_18229))
69 (** val bind_new_rect_Type0 :
70 ('a2 -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new) -> ('a1 -> 'a3) -> 'a3) ->
71 ('a1, 'a2) bind_new -> 'a3 **)
72 let rec bind_new_rect_Type0 h_bret h_bnew = function
73 | Bret x_18234 -> h_bret x_18234
75 h_bnew x_18236 (fun x_18235 ->
76 bind_new_rect_Type0 h_bret h_bnew (x_18236 x_18235))
78 (** val bind_new_inv_rect_Type4 :
79 ('a1, 'a2) bind_new -> ('a2 -> __ -> 'a3) -> (('a1 -> ('a1, 'a2)
80 bind_new) -> ('a1 -> __ -> 'a3) -> __ -> 'a3) -> 'a3 **)
81 let bind_new_inv_rect_Type4 hterm h1 h2 =
82 let hcut = bind_new_rect_Type4 h1 h2 hterm in hcut __
84 (** val bind_new_inv_rect_Type3 :
85 ('a1, 'a2) bind_new -> ('a2 -> __ -> 'a3) -> (('a1 -> ('a1, 'a2)
86 bind_new) -> ('a1 -> __ -> 'a3) -> __ -> 'a3) -> 'a3 **)
87 let bind_new_inv_rect_Type3 hterm h1 h2 =
88 let hcut = bind_new_rect_Type3 h1 h2 hterm in hcut __
90 (** val bind_new_inv_rect_Type2 :
91 ('a1, 'a2) bind_new -> ('a2 -> __ -> 'a3) -> (('a1 -> ('a1, 'a2)
92 bind_new) -> ('a1 -> __ -> 'a3) -> __ -> 'a3) -> 'a3 **)
93 let bind_new_inv_rect_Type2 hterm h1 h2 =
94 let hcut = bind_new_rect_Type2 h1 h2 hterm in hcut __
96 (** val bind_new_inv_rect_Type1 :
97 ('a1, 'a2) bind_new -> ('a2 -> __ -> 'a3) -> (('a1 -> ('a1, 'a2)
98 bind_new) -> ('a1 -> __ -> 'a3) -> __ -> 'a3) -> 'a3 **)
99 let bind_new_inv_rect_Type1 hterm h1 h2 =
100 let hcut = bind_new_rect_Type1 h1 h2 hterm in hcut __
102 (** val bind_new_inv_rect_Type0 :
103 ('a1, 'a2) bind_new -> ('a2 -> __ -> 'a3) -> (('a1 -> ('a1, 'a2)
104 bind_new) -> ('a1 -> __ -> 'a3) -> __ -> 'a3) -> 'a3 **)
105 let bind_new_inv_rect_Type0 hterm h1 h2 =
106 let hcut = bind_new_rect_Type0 h1 h2 hterm in hcut __
108 (** val bind_new_discr : ('a1, 'a2) bind_new -> ('a1, 'a2) bind_new -> __ **)
109 let bind_new_discr x y =
110 Logic.eq_rect_Type2 x
112 | Bret a0 -> Obj.magic (fun _ dH -> dH __)
113 | Bnew a0 -> Obj.magic (fun _ dH -> dH __)) y
115 (** val bind_new_jmdiscr :
116 ('a1, 'a2) bind_new -> ('a1, 'a2) bind_new -> __ **)
117 let bind_new_jmdiscr x y =
118 Logic.eq_rect_Type2 x
120 | Bret a0 -> Obj.magic (fun _ dH -> dH __)
121 | Bnew a0 -> Obj.magic (fun _ dH -> dH __)) y
124 Nat.nat -> ('a1 List.list -> ('a1, 'a2) bind_new) -> ('a1, 'a2) bind_new **)
127 | Nat.O -> f List.Nil
128 | Nat.S x -> Bnew (fun y -> bnews x (fun l -> f (List.Cons (y, l))))
130 (** val bnews_strong :
131 Nat.nat -> ('a1 List.list -> __ -> ('a1, 'a2) bind_new) -> ('a1, 'a2)
133 let rec bnews_strong n f =
135 | Nat.O -> (fun _ -> f List.Nil __)
137 (fun _ -> Bnew (fun x ->
138 bnews_strong n' (fun l' _ -> f (List.Cons (x, l')) __)))) __
141 ('a1, 'a2) bind_new -> ('a2 -> ('a1, 'a3) bind_new) -> ('a1, 'a3)
146 | Bnew n -> Bnew (fun x -> bbind (n x) f)
148 (** val bindNew : Monad.monadProps **)
150 Monad.makeMonadProps (fun _ x -> Bret x) (fun _ _ -> bbind)
155 'a2 Monad.smax_def__o__monad -> ('a2, 'a3) bind_new -> 'a3
156 Monad.smax_def__o__monad **)
157 let rec bcompile fresh = function
158 | Bret x -> Monad.m_return0 (Monad.smax_def State.state_monad) x
160 Monad.m_bind0 (Monad.smax_def State.state_monad) fresh (fun r ->
161 bcompile fresh (f r))