38 | MSG of ErrorMessages.errorMessage
39 | CTX of PreIdentifiers.identifierTag * PreIdentifiers.identifier
41 (** val errcode_rect_Type4 :
42 (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
43 PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1 **)
44 let rec errcode_rect_Type4 h_MSG h_CTX = function
45 | MSG x_3113 -> h_MSG x_3113
46 | CTX (tag, x_3114) -> h_CTX tag x_3114
48 (** val errcode_rect_Type5 :
49 (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
50 PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1 **)
51 let rec errcode_rect_Type5 h_MSG h_CTX = function
52 | MSG x_3118 -> h_MSG x_3118
53 | CTX (tag, x_3119) -> h_CTX tag x_3119
55 (** val errcode_rect_Type3 :
56 (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
57 PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1 **)
58 let rec errcode_rect_Type3 h_MSG h_CTX = function
59 | MSG x_3123 -> h_MSG x_3123
60 | CTX (tag, x_3124) -> h_CTX tag x_3124
62 (** val errcode_rect_Type2 :
63 (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
64 PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1 **)
65 let rec errcode_rect_Type2 h_MSG h_CTX = function
66 | MSG x_3128 -> h_MSG x_3128
67 | CTX (tag, x_3129) -> h_CTX tag x_3129
69 (** val errcode_rect_Type1 :
70 (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
71 PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1 **)
72 let rec errcode_rect_Type1 h_MSG h_CTX = function
73 | MSG x_3133 -> h_MSG x_3133
74 | CTX (tag, x_3134) -> h_CTX tag x_3134
76 (** val errcode_rect_Type0 :
77 (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
78 PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1 **)
79 let rec errcode_rect_Type0 h_MSG h_CTX = function
80 | MSG x_3138 -> h_MSG x_3138
81 | CTX (tag, x_3139) -> h_CTX tag x_3139
83 (** val errcode_inv_rect_Type4 :
84 errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
85 (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1)
87 let errcode_inv_rect_Type4 hterm h1 h2 =
88 let hcut = errcode_rect_Type4 h1 h2 hterm in hcut __
90 (** val errcode_inv_rect_Type3 :
91 errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
92 (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1)
94 let errcode_inv_rect_Type3 hterm h1 h2 =
95 let hcut = errcode_rect_Type3 h1 h2 hterm in hcut __
97 (** val errcode_inv_rect_Type2 :
98 errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
99 (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1)
101 let errcode_inv_rect_Type2 hterm h1 h2 =
102 let hcut = errcode_rect_Type2 h1 h2 hterm in hcut __
104 (** val errcode_inv_rect_Type1 :
105 errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
106 (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1)
108 let errcode_inv_rect_Type1 hterm h1 h2 =
109 let hcut = errcode_rect_Type1 h1 h2 hterm in hcut __
111 (** val errcode_inv_rect_Type0 :
112 errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
113 (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1)
115 let errcode_inv_rect_Type0 hterm h1 h2 =
116 let hcut = errcode_rect_Type0 h1 h2 hterm in hcut __
118 (** val errcode_discr : errcode -> errcode -> __ **)
119 let errcode_discr x y =
120 Logic.eq_rect_Type2 x
122 | MSG a0 -> Obj.magic (fun _ dH -> dH __)
123 | CTX (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
125 (** val errcode_jmdiscr : errcode -> errcode -> __ **)
126 let errcode_jmdiscr x y =
127 Logic.eq_rect_Type2 x
129 | MSG a0 -> Obj.magic (fun _ dH -> dH __)
130 | CTX (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
132 type errmsg = errcode List.list
134 (** val msg : ErrorMessages.errorMessage -> errmsg **)
136 List.Cons ((MSG s), List.Nil)
142 (** val res_rect_Type4 :
143 ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
144 let rec res_rect_Type4 h_OK h_Error = function
145 | OK x_3178 -> h_OK x_3178
146 | Error x_3179 -> h_Error x_3179
148 (** val res_rect_Type5 :
149 ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
150 let rec res_rect_Type5 h_OK h_Error = function
151 | OK x_3183 -> h_OK x_3183
152 | Error x_3184 -> h_Error x_3184
154 (** val res_rect_Type3 :
155 ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
156 let rec res_rect_Type3 h_OK h_Error = function
157 | OK x_3188 -> h_OK x_3188
158 | Error x_3189 -> h_Error x_3189
160 (** val res_rect_Type2 :
161 ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
162 let rec res_rect_Type2 h_OK h_Error = function
163 | OK x_3193 -> h_OK x_3193
164 | Error x_3194 -> h_Error x_3194
166 (** val res_rect_Type1 :
167 ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
168 let rec res_rect_Type1 h_OK h_Error = function
169 | OK x_3198 -> h_OK x_3198
170 | Error x_3199 -> h_Error x_3199
172 (** val res_rect_Type0 :
173 ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
174 let rec res_rect_Type0 h_OK h_Error = function
175 | OK x_3203 -> h_OK x_3203
176 | Error x_3204 -> h_Error x_3204
178 (** val res_inv_rect_Type4 :
179 'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2 **)
180 let res_inv_rect_Type4 hterm h1 h2 =
181 let hcut = res_rect_Type4 h1 h2 hterm in hcut __
183 (** val res_inv_rect_Type3 :
184 'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2 **)
185 let res_inv_rect_Type3 hterm h1 h2 =
186 let hcut = res_rect_Type3 h1 h2 hterm in hcut __
188 (** val res_inv_rect_Type2 :
189 'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2 **)
190 let res_inv_rect_Type2 hterm h1 h2 =
191 let hcut = res_rect_Type2 h1 h2 hterm in hcut __
193 (** val res_inv_rect_Type1 :
194 'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2 **)
195 let res_inv_rect_Type1 hterm h1 h2 =
196 let hcut = res_rect_Type1 h1 h2 hterm in hcut __
198 (** val res_inv_rect_Type0 :
199 'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2 **)
200 let res_inv_rect_Type0 hterm h1 h2 =
201 let hcut = res_rect_Type0 h1 h2 hterm in hcut __
203 (** val res_discr : 'a1 res -> 'a1 res -> __ **)
205 Logic.eq_rect_Type2 x
207 | OK a0 -> Obj.magic (fun _ dH -> dH __)
208 | Error a0 -> Obj.magic (fun _ dH -> dH __)) y
210 (** val res_jmdiscr : 'a1 res -> 'a1 res -> __ **)
211 let res_jmdiscr x y =
212 Logic.eq_rect_Type2 x
214 | OK a0 -> Obj.magic (fun _ dH -> dH __)
215 | Error a0 -> Obj.magic (fun _ dH -> dH __)) y
217 (** val res0 : Monad.monadProps **)
219 Monad.makeMonadProps (fun _ x -> OK x) (fun _ _ m f ->
222 | Error msg0 -> Error msg0)
224 (** val mfold_left_i_aux :
225 (Nat.nat -> 'a1 -> 'a2 -> 'a1 res) -> 'a1 res -> Nat.nat -> 'a2 List.list
227 let rec mfold_left_i_aux f x i = function
228 | List.Nil -> Obj.magic x
229 | List.Cons (hd, tl) ->
230 Monad.m_bind0 (Monad.max_def res0) (Obj.magic x) (fun x0 ->
231 mfold_left_i_aux f (f i x0 hd) (Nat.S i) tl)
233 (** val mfold_left_i :
234 (Nat.nat -> 'a1 -> 'a2 -> 'a1 res) -> 'a1 res -> 'a2 List.list -> __ **)
235 let mfold_left_i f x =
236 mfold_left_i_aux f x Nat.O
238 (** val mfold_left2 :
239 ('a1 -> 'a2 -> 'a3 -> 'a1 res) -> 'a1 res -> 'a2 List.list -> 'a3
240 List.list -> 'a1 res **)
241 let rec mfold_left2 f accu left right =
246 | List.Cons (hd, tl) -> Error (msg ErrorMessages.WrongLength))
247 | List.Cons (hd, tl) ->
249 | List.Nil -> Error (msg ErrorMessages.WrongLength)
250 | List.Cons (hd', tl') ->
252 (Monad.m_bind0 (Monad.max_def res0) (Obj.magic accu) (fun accu0 ->
253 Obj.magic (mfold_left2 f (f accu0 hd hd') tl tl'))))
255 (** val opt_to_res : errmsg -> 'a1 Types.option -> 'a1 res **)
256 let opt_to_res msg0 = function
257 | Types.None -> Error msg0
258 | Types.Some v0 -> OK v0
260 (** val jmeq_to_eq__o__opt_eq_from_res__o__inject :
261 errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 **)
262 let jmeq_to_eq__o__opt_eq_from_res__o__inject x1 x2 x3 =
265 (** val dpi1__o__opt_eq_from_res__o__inject :
266 errmsg -> 'a1 Types.option -> 'a1 -> (__, 'a2) Types.dPair -> __
268 let dpi1__o__opt_eq_from_res__o__inject x1 x2 x3 x6 =
271 (** val eject__o__opt_eq_from_res__o__inject :
272 errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 -> __ Types.sig0 **)
273 let eject__o__opt_eq_from_res__o__inject x1 x2 x3 x6 =
276 (** val opt_eq_from_res__o__inject :
277 errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 **)
278 let opt_eq_from_res__o__inject x1 x2 x3 =
281 (** val bind_eq : 'a1 res -> ('a1 -> __ -> 'a2 res) -> 'a2 res **)
285 | Error msg0 -> (fun _ -> Error msg0)) __
288 ('a1, 'a2) Types.prod res -> ('a1 -> 'a2 -> __ -> 'a3 res) -> 'a3 res **)
291 | OK x -> let { Types.fst = a; Types.snd = b } = x in g a b
292 | Error msg0 -> (fun _ -> Error msg0)) __
294 (** val res_to_opt : 'a1 res -> 'a1 Types.option **)
295 let res_to_opt = function
296 | OK v0 -> Types.Some v0
297 | Error x -> Types.None
299 (** val bind : __ -> ('a1 -> __) -> __ **)
300 let bind x_768 x_769 =
301 Monad.m_bind0 (Monad.max_def res0) x_768 x_769
303 (** val bind2 : __ -> ('a1 -> 'a2 -> __) -> __ **)
305 Monad.m_bind2 (Monad.max_def res0) m f
307 (** val bind3 : __ -> ('a1 -> 'a2 -> 'a3 -> __) -> __ **)
309 Monad.m_bind3 (Monad.max_def res0) x x0
311 (** val mmap : ('a1 -> __) -> 'a1 List.list -> __ **)
313 Monad.m_list_map (Monad.max_def res0) x x0
315 (** val mmap_sigma : ('a1 -> __) -> 'a1 List.list -> __ **)
316 let mmap_sigma x x0 =
317 Monad.m_list_map_sigma (Monad.max_def res0) x x0