extracted/monad.ml

   1 open Preamble
   2
   3 open Hints_declaration
   4
   5 open Core_notation
   6
   7 open Pts
   8
   9 open Logic
  10
  11 open Types
  12
  13 open Relations
  14
  15 open Setoids
  16
  17 type ('a, 'b) pred_transformer = __
  18
  19 type ('a, 'b, 'c, 'd) rel_transformer = __
  20
  21 type monad = { m_return : (__ -> __ -> __);
  22                m_bind : (__ -> __ -> __ -> (__ -> __) -> __) }
  23
  24 (** val monad_rect_Type4 :
  25     (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1)
  26     -> monad -> 'a1 **)
  27 let 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 **)
  34 let 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 **)
  41 let 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 **)
  48 let 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 **)
  55 let 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 **)
  62 let 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
  66 type 'x monad0 = __
  67
  68 (** val m_return0 : monad -> 'a1 -> __ **)
  69 let 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 -> __) -> __ **)
  73 let 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 **)
  80 let 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 **)
  86 let 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 **)
  92 let 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 **)
  98 let 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 **)
 104 let monad_inv_rect_Type0 hterm h1 =
 105   let hcut = monad_rect_Type0 h1 hterm in hcut __
 106
 107 type monadProps =
 108   monad
 109   (* singleton inductive, whose constructor was mk_MonadProps *)
 110
 111 (** val monadProps_rect_Type4 :
 112     (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1 **)
 113 let 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 **)
 118 let 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 **)
 123 let 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 **)
 128 let 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 **)
 133 let 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 **)
 138 let 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 **)
 142 let rec max_def xxx =
 143   let yyy = xxx in yyy
 144
 145 (** val monadProps_inv_rect_Type4 :
 146     monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 147 let 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 **)
 152 let 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 **)
 157 let 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 **)
 162 let 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 **)
 167 let monadProps_inv_rect_Type0 hterm h1 =
 168   let hcut = monadProps_rect_Type0 h1 hterm in hcut __
 169
 170 type 'x_772 max_def__o__monad = __
 171
 172 type setoidMonadProps =
 173   monad
 174   (* singleton inductive, whose constructor was mk_SetoidMonadProps *)
 175
 176 (** val setoidMonadProps_rect_Type4 :
 177     (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
 178     setoidMonadProps -> 'a1 **)
 179 let 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 **)
 186 let 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 **)
 193 let 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 **)
 200 let 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 **)
 207 let 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 **)
 214 let 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 **)
 219 let rec smax_def xxx =
 220   let yyy = xxx in yyy
 221
 222 (** val setoidMonadProps_inv_rect_Type4 :
 223     setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
 224     __ -> __ -> __ -> 'a1) -> 'a1 **)
 225 let 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 **)
 231 let 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 **)
 237 let 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 **)
 243 let 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 **)
 249 let setoidMonadProps_inv_rect_Type0 hterm h1 =
 250   let hcut = setoidMonadProps_rect_Type0 h1 hterm in hcut __
 251
 252 type 'x_772 smax_def__o__monad = __
 253
 254 (** val setoid_of_monad : setoidMonadProps -> Setoids.setoid **)
 255 let setoid_of_monad m =
 256   Setoids.Mk_Setoid
 257
 258 open Bool
 259
 260 open Nat
 261
 262 open List
 263
 264 (** val m_map : monad -> ('a1 -> 'a2) -> __ -> __ **)
 265 let 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) -> __ -> __ -> __ **)
 269 let 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 -> __) -> __ **)
 273 let 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 -> __) -> __ **)
 277 let 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 -> __ -> __ **)
 282 let m_join m m0 =
 283   m_bind0 m m0 (fun x -> x)
 284
 285 (** val m_sigbind2 : monad -> __ -> ('a1 -> 'a2 -> __ -> __) -> __ **)
 286 let 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 -> __ **)
 292 let 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 -> __ **)
 299 let 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) -> __ -> __ -> __ **)
 308 let 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 -> __ **)
 313 let 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 **)
 321 let 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 **)
 327 let makeSetoidMonadProps m_return1 m_bind1 =
 328   { m_return = (Obj.magic m_return1); m_bind = (Obj.magic m_bind1) }
 329
 330 open Jmeq
 331
 332 open Russell
 333
 334 type monadPred =
 335 | Mk_MonadPred
 336
 337 (** val monadPred_rect_Type4 :
 338     monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1 **)
 339 let 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 **)
 344 let 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 **)
 349 let 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 **)
 354 let 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 **)
 359 let 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 **)
 364 let 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 **)
 369 let 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 **)
 374 let 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 **)
 379 let 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 **)
 384 let 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 **)
 389 let 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 -> __ **)
 393 let monadPred_jmdiscr a1 x y =
 394   Logic.eq_rect_Type2 x
 395     (let Mk_MonadPred = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y
 396
 397 type injMonadPred = { im_pred : monadPred;
 398                       mp_inject : (__ -> __ -> __ Types.sig0 -> __) }
 399
 400 (** val injMonadPred_rect_Type4 :
 401     monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
 402     injMonadPred -> 'a1 **)
 403 let 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 **)
 410 let 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 **)
 417 let 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 **)
 424 let 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 **)
 431 let 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 **)
 438 let 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 **)
 443 let rec im_pred m xxx =
 444   xxx.im_pred
 445
 446 (** val mp_inject0 : monad -> injMonadPred -> __ Types.sig0 -> __ **)
 447 let 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 **)
 453 let 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 **)
 459 let 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 **)
 465 let 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 **)
 471 let 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 **)
 477 let 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 -> __ **)
 482 let 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
 487 type monadRel =
 488 | Mk_MonadRel
 489
 490 (** val monadRel_rect_Type4 :
 491     monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1 **)
 492 let 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 **)
 497 let 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 **)
 502 let 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 **)
 507 let 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 **)
 512 let 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 **)
 517 let 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 **)
 522 let 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 **)
 527 let 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 **)
 532 let 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 **)
 537 let 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 **)
 542 let 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 -> __ **)
 546 let 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