extracted/iOMonad.ml

   1 open Preamble
   2
   3 open Div_and_mod
   4
   5 open Jmeq
   6
   7 open Russell
   8
   9 open Util
  10
  11 open Bool
  12
  13 open Relations
  14
  15 open Nat
  16
  17 open List
  18
  19 open Hints_declaration
  20
  21 open Core_notation
  22
  23 open Pts
  24
  25 open Logic
  26
  27 open Types
  28
  29 open Extralib
  30
  31 open ErrorMessages
  32
  33 open Option
  34
  35 open Setoids
  36
  37 open Monad
  38
  39 open Positive
  40
  41 open PreIdentifiers
  42
  43 open Errors
  44
  45 type ('output, 'input, 't) iO =
  46 | Interact of 'output * ('input -> ('output, 'input, 't) iO)
  47 | Value of 't
  48 | Wrong of Errors.errmsg
  49
  50 (** val iO_rect_Type4 :
  51     ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 ->
  52     'a4) -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4 **)
  53 let rec iO_rect_Type4 h_Interact h_Value h_Wrong = function
  54 | Interact (o, x_4685) ->
  55   h_Interact o x_4685 (fun x_4684 ->
  56     iO_rect_Type4 h_Interact h_Value h_Wrong (x_4685 x_4684))
  57 | Value x_4686 -> h_Value x_4686
  58 | Wrong x_4687 -> h_Wrong x_4687
  59
  60 (** val iO_rect_Type3 :
  61     ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 ->
  62     'a4) -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4 **)
  63 let rec iO_rect_Type3 h_Interact h_Value h_Wrong = function
  64 | Interact (o, x_4701) ->
  65   h_Interact o x_4701 (fun x_4700 ->
  66     iO_rect_Type3 h_Interact h_Value h_Wrong (x_4701 x_4700))
  67 | Value x_4702 -> h_Value x_4702
  68 | Wrong x_4703 -> h_Wrong x_4703
  69
  70 (** val iO_rect_Type2 :
  71     ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 ->
  72     'a4) -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4 **)
  73 let rec iO_rect_Type2 h_Interact h_Value h_Wrong = function
  74 | Interact (o, x_4709) ->
  75   h_Interact o x_4709 (fun x_4708 ->
  76     iO_rect_Type2 h_Interact h_Value h_Wrong (x_4709 x_4708))
  77 | Value x_4710 -> h_Value x_4710
  78 | Wrong x_4711 -> h_Wrong x_4711
  79
  80 (** val iO_rect_Type1 :
  81     ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 ->
  82     'a4) -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4 **)
  83 let rec iO_rect_Type1 h_Interact h_Value h_Wrong = function
  84 | Interact (o, x_4717) ->
  85   h_Interact o x_4717 (fun x_4716 ->
  86     iO_rect_Type1 h_Interact h_Value h_Wrong (x_4717 x_4716))
  87 | Value x_4718 -> h_Value x_4718
  88 | Wrong x_4719 -> h_Wrong x_4719
  89
  90 (** val iO_rect_Type0 :
  91     ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 ->
  92     'a4) -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4 **)
  93 let rec iO_rect_Type0 h_Interact h_Value h_Wrong = function
  94 | Interact (o, x_4725) ->
  95   h_Interact o x_4725 (fun x_4724 ->
  96     iO_rect_Type0 h_Interact h_Value h_Wrong (x_4725 x_4724))
  97 | Value x_4726 -> h_Value x_4726
  98 | Wrong x_4727 -> h_Wrong x_4727
  99
 100 (** val iO_inv_rect_Type4 :
 101     ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __
 102     -> 'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ ->
 103     'a4) -> 'a4 **)
 104 let iO_inv_rect_Type4 hterm h1 h2 h3 =
 105   let hcut = iO_rect_Type4 h1 h2 h3 hterm in hcut __
 106
 107 (** val iO_inv_rect_Type3 :
 108     ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __
 109     -> 'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ ->
 110     'a4) -> 'a4 **)
 111 let iO_inv_rect_Type3 hterm h1 h2 h3 =
 112   let hcut = iO_rect_Type3 h1 h2 h3 hterm in hcut __
 113
 114 (** val iO_inv_rect_Type2 :
 115     ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __
 116     -> 'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ ->
 117     'a4) -> 'a4 **)
 118 let iO_inv_rect_Type2 hterm h1 h2 h3 =
 119   let hcut = iO_rect_Type2 h1 h2 h3 hterm in hcut __
 120
 121 (** val iO_inv_rect_Type1 :
 122     ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __
 123     -> 'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ ->
 124     'a4) -> 'a4 **)
 125 let iO_inv_rect_Type1 hterm h1 h2 h3 =
 126   let hcut = iO_rect_Type1 h1 h2 h3 hterm in hcut __
 127
 128 (** val iO_inv_rect_Type0 :
 129     ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __
 130     -> 'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ ->
 131     'a4) -> 'a4 **)
 132 let iO_inv_rect_Type0 hterm h1 h2 h3 =
 133   let hcut = iO_rect_Type0 h1 h2 h3 hterm in hcut __
 134
 135 (** val iO_discr : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3) iO -> __ **)
 136 let iO_discr x y =
 137   Logic.eq_rect_Type2 x
 138     (match x with
 139      | Interact (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 140      | Value a0 -> Obj.magic (fun _ dH -> dH __)
 141      | Wrong a0 -> Obj.magic (fun _ dH -> dH __)) y
 142
 143 (** val iO_jmdiscr : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3) iO -> __ **)
 144 let iO_jmdiscr x y =
 145   Logic.eq_rect_Type2 x
 146     (match x with
 147      | Interact (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 148      | Value a0 -> Obj.magic (fun _ dH -> dH __)
 149      | Wrong a0 -> Obj.magic (fun _ dH -> dH __)) y
 150
 151 open Proper
 152
 153 (** val bindIO :
 154     ('a1, 'a2, 'a3) iO -> ('a3 -> ('a1, 'a2, 'a4) iO) -> ('a1, 'a2, 'a4) iO **)
 155 let rec bindIO v f =
 156   match v with
 157   | Interact (out, k) -> Interact (out, (fun res -> bindIO (k res) f))
 158   | Value v' -> f v'
 159   | Wrong m -> Wrong m
 160
 161 (** val iOMonad : Monad.monadProps **)
 162 let iOMonad =
 163   Monad.makeMonadProps (fun _ x -> Value x) (fun _ _ -> bindIO)
 164
 165 (** val bindIO2 : __ -> ('a3 -> 'a4 -> __) -> __ **)
 166 let bindIO2 m f =
 167   Monad.m_bind2 (Monad.max_def iOMonad) m f
 168
 169 (** val iORel : Monad.monadRel **)
 170 let iORel =
 171   Monad.Mk_MonadRel
 172
 173 (** val pred_io_inject :
 174     ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3 Types.sig0) iO **)
 175 let rec pred_io_inject a =
 176   (match a with
 177    | Interact (o, f) ->
 178      (fun _ -> Interact (o, (fun x -> pred_io_inject (f x))))
 179    | Value x ->
 180      (fun _ -> Obj.magic (Monad.m_return0 (Monad.max_def iOMonad) x))
 181    | Wrong e -> (fun _ -> Wrong e)) __
 182
 183 (** val iOPred : Monad.injMonadPred **)
 184 let iOPred =
 185   { Monad.im_pred = Monad.Mk_MonadPred; Monad.mp_inject = (fun _ _ a_sig ->
 186     let a = a_sig in Obj.magic (pred_io_inject (Obj.magic a))) }
 187
 188 (** val err_to_io : 'a3 Errors.res -> ('a1, 'a2, 'a3) iO **)
 189 let err_to_io = function
 190 | Errors.OK v' -> Value v'
 191 | Errors.Error m -> Wrong m
 192
 193 (** val dpi1__o__err_to_io__o__inject :
 194     ('a2 Errors.res, 'a3) Types.dPair -> ('a1, 'a4, 'a2) iO Types.sig0 **)
 195 let dpi1__o__err_to_io__o__inject x4 =
 196   err_to_io x4.Types.dpi1
 197
 198 (** val eject__o__err_to_io__o__inject :
 199     'a2 Errors.res Types.sig0 -> ('a1, 'a3, 'a2) iO Types.sig0 **)
 200 let eject__o__err_to_io__o__inject x4 =
 201   err_to_io (Types.pi1 x4)
 202
 203 (** val err_to_io__o__inject :
 204     'a2 Errors.res -> ('a1, 'a3, 'a2) iO Types.sig0 **)
 205 let err_to_io__o__inject x3 =
 206   err_to_io x3
 207
 208 (** val dpi1__o__err_to_io :
 209     ('a2 Errors.res, 'a3) Types.dPair -> ('a1, 'a4, 'a2) iO **)
 210 let dpi1__o__err_to_io x4 =
 211   err_to_io x4.Types.dpi1
 212
 213 (** val eject__o__err_to_io :
 214     'a2 Errors.res Types.sig0 -> ('a1, 'a3, 'a2) iO **)
 215 let eject__o__err_to_io x4 =
 216   err_to_io (Types.pi1 x4)
 217
 218 (** val err_to_io_sig :
 219     'a3 Types.sig0 Errors.res -> ('a1, 'a2, 'a3 Types.sig0) iO **)
 220 let err_to_io_sig = function
 221 | Errors.OK v' -> Value v'
 222 | Errors.Error m -> Wrong m
 223
 224 (** val io_inject_0 : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3 Types.sig0) iO **)
 225 let rec io_inject_0 a =
 226   (match a with
 227    | Interact (out, k) ->
 228      (fun _ -> Interact (out, (fun v -> io_inject_0 (k v))))
 229    | Value c -> (fun _ -> Value c)
 230    | Wrong m -> (fun _ -> Wrong m)) __
 231
 232 (** val io_inject :
 233     ('a1, 'a2, 'a3) iO Types.option -> ('a1, 'a2, 'a3 Types.sig0) iO **)
 234 let io_inject a =
 235   (match a with
 236    | Types.None -> (fun _ -> Logic.false_rect_Type0 __)
 237    | Types.Some b -> (fun _ -> io_inject_0 b)) __
 238
 239 (** val io_eject : ('a1, 'a2, 'a3 Types.sig0) iO -> ('a1, 'a2, 'a3) iO **)
 240 let rec io_eject = function
 241 | Interact (out, k) -> Interact (out, (fun v -> io_eject (k v)))
 242 | Value b -> let w = b in Value w
 243 | Wrong m -> Wrong m
 244
 245 (** val dpi1__o__io_inject__o__inject :
 246     (('a1, 'a3, 'a2) iO Types.option, 'a4) Types.dPair -> ('a1, 'a3, 'a2
 247     Types.sig0) iO Types.sig0 **)
 248 let dpi1__o__io_inject__o__inject x6 =
 249   io_inject x6.Types.dpi1
 250
 251 (** val eject__o__io_inject__o__inject :
 252     ('a1, 'a3, 'a2) iO Types.option Types.sig0 -> ('a1, 'a3, 'a2 Types.sig0)
 253     iO Types.sig0 **)
 254 let eject__o__io_inject__o__inject x6 =
 255   io_inject (Types.pi1 x6)
 256
 257 (** val io_inject__o__inject :
 258     ('a1, 'a3, 'a2) iO Types.option -> ('a1, 'a3, 'a2 Types.sig0) iO
 259     Types.sig0 **)
 260 let io_inject__o__inject x5 =
 261   io_inject x5
 262
 263 (** val dpi1__o__io_inject :
 264     (('a1, 'a3, 'a2) iO Types.option, 'a4) Types.dPair -> ('a1, 'a3, 'a2
 265     Types.sig0) iO **)
 266 let dpi1__o__io_inject x5 =
 267   io_inject x5.Types.dpi1
 268
 269 (** val eject__o__io_inject :
 270     ('a1, 'a3, 'a2) iO Types.option Types.sig0 -> ('a1, 'a3, 'a2 Types.sig0)
 271     iO **)
 272 let eject__o__io_inject x5 =
 273   io_inject (Types.pi1 x5)
 274
 275 (** val io_inject__o__io_eject__o__inject :
 276     ('a1, 'a3, 'a2) iO Types.option -> ('a1, 'a3, 'a2) iO Types.sig0 **)
 277 let io_inject__o__io_eject__o__inject x4 =
 278   io_eject (io_inject x4)
 279
 280 (** val dpi1__o__err_to_io__o__io_eject__o__inject :
 281     ('a2 Types.sig0 Errors.res, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO
 282     Types.sig0 **)
 283 let dpi1__o__err_to_io__o__io_eject__o__inject x6 =
 284   io_eject (dpi1__o__err_to_io x6)
 285
 286 (** val dpi1__o__io_inject__o__io_eject__o__inject :
 287     (('a1, 'a3, 'a2) iO Types.option, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO
 288     Types.sig0 **)
 289 let dpi1__o__io_inject__o__io_eject__o__inject x6 =
 290   io_eject (dpi1__o__io_inject x6)
 291
 292 (** val eject__o__err_to_io__o__io_eject__o__inject :
 293     'a2 Types.sig0 Errors.res Types.sig0 -> ('a1, 'a3, 'a2) iO Types.sig0 **)
 294 let eject__o__err_to_io__o__io_eject__o__inject x6 =
 295   io_eject (eject__o__err_to_io x6)
 296
 297 (** val eject__o__io_inject__o__io_eject__o__inject :
 298     ('a1, 'a3, 'a2) iO Types.option Types.sig0 -> ('a1, 'a3, 'a2) iO
 299     Types.sig0 **)
 300 let eject__o__io_inject__o__io_eject__o__inject x6 =
 301   io_eject (eject__o__io_inject x6)
 302
 303 (** val err_to_io__o__io_eject__o__inject :
 304     'a2 Types.sig0 Errors.res -> ('a1, 'a3, 'a2) iO Types.sig0 **)
 305 let err_to_io__o__io_eject__o__inject x4 =
 306   io_eject (err_to_io x4)
 307
 308 (** val dpi1__o__io_eject__o__inject :
 309     (('a1, 'a3, 'a2 Types.sig0) iO, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO
 310     Types.sig0 **)
 311 let dpi1__o__io_eject__o__inject x6 =
 312   io_eject x6.Types.dpi1
 313
 314 (** val eject__o__io_eject__o__inject :
 315     ('a1, 'a3, 'a2 Types.sig0) iO Types.sig0 -> ('a1, 'a3, 'a2) iO Types.sig0 **)
 316 let eject__o__io_eject__o__inject x6 =
 317   io_eject (Types.pi1 x6)
 318
 319 (** val io_eject__o__inject :
 320     ('a1, 'a3, 'a2 Types.sig0) iO -> ('a1, 'a3, 'a2) iO Types.sig0 **)
 321 let io_eject__o__inject x5 =
 322   io_eject x5
 323
 324 (** val io_inject__o__io_eject :
 325     ('a1, 'a3, 'a2) iO Types.option -> ('a1, 'a3, 'a2) iO **)
 326 let io_inject__o__io_eject x4 =
 327   io_eject (io_inject x4)
 328
 329 (** val dpi1__o__err_to_io__o__io_eject :
 330     ('a2 Types.sig0 Errors.res, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO **)
 331 let dpi1__o__err_to_io__o__io_eject x5 =
 332   io_eject (dpi1__o__err_to_io x5)
 333
 334 (** val dpi1__o__io_inject__o__io_eject :
 335     (('a1, 'a3, 'a2) iO Types.option, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO **)
 336 let dpi1__o__io_inject__o__io_eject x5 =
 337   io_eject (dpi1__o__io_inject x5)
 338
 339 (** val eject__o__err_to_io__o__io_eject :
 340     'a2 Types.sig0 Errors.res Types.sig0 -> ('a1, 'a3, 'a2) iO **)
 341 let eject__o__err_to_io__o__io_eject x5 =
 342   io_eject (eject__o__err_to_io x5)
 343
 344 (** val eject__o__io_inject__o__io_eject :
 345     ('a1, 'a3, 'a2) iO Types.option Types.sig0 -> ('a1, 'a3, 'a2) iO **)
 346 let eject__o__io_inject__o__io_eject x5 =
 347   io_eject (eject__o__io_inject x5)
 348
 349 (** val err_to_io__o__io_eject :
 350     'a2 Types.sig0 Errors.res -> ('a1, 'a3, 'a2) iO **)
 351 let err_to_io__o__io_eject x4 =
 352   io_eject (err_to_io x4)
 353
 354 (** val dpi1__o__io_eject :
 355     (('a1, 'a3, 'a2 Types.sig0) iO, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO **)
 356 let dpi1__o__io_eject x5 =
 357   io_eject x5.Types.dpi1
 358
 359 (** val eject__o__io_eject :
 360     ('a1, 'a3, 'a2 Types.sig0) iO Types.sig0 -> ('a1, 'a3, 'a2) iO **)
 361 let eject__o__io_eject x5 =
 362   io_eject (Types.pi1 x5)
 363
 364 (** val opt_to_io :
 365     Errors.errmsg -> 'a3 Types.option -> ('a1, 'a2, 'a3) iO **)
 366 let opt_to_io m = function
 367 | Types.None -> Wrong m
 368 | Types.Some v' -> Value v'
 369
 370 (** val bind_res_value :
 371     'a3 Errors.res -> ('a3 -> 'a4 Errors.res) -> 'a4 -> ('a3 -> __ -> __ ->
 372     'a5) -> 'a5 **)
 373 let bind_res_value clearme f v x =
 374   (match clearme with
 375    | Errors.OK a -> (fun f0 v0 _ h _ -> h a __ __)
 376    | Errors.Error m ->
 377      (fun f0 v0 _ h _ -> Obj.magic iO_discr (Wrong m) (Value v0) __)) f v __
 378     x __
 379
 380 (** val bindIO_value :
 381     ('a1, 'a2, 'a3) iO -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a4 -> ('a3 -> __ ->
 382     __ -> 'a5) -> 'a5 **)
 383 let bindIO_value clearme f v x =
 384   (match clearme with
 385    | Interact (o, k) ->
 386      (fun f0 v0 _ h _ ->
 387        Obj.magic iO_discr (Interact (o, (fun res -> bindIO (k res) f0)))
 388          (Value v0) __)
 389    | Value a -> (fun f0 v0 _ h _ -> h a __ __)
 390    | Wrong m ->
 391      (fun f0 v0 _ h _ -> Obj.magic iO_discr (Wrong m) (Value v0) __)) f v __
 392     x __
 393
 394 (** val bindIO_res_interact :
 395     'a3 Errors.res -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a1 -> ('a2 -> ('a1,
 396     'a2, 'a4) iO) -> ('a3 -> __ -> __ -> 'a5) -> 'a5 **)
 397 let bindIO_res_interact clearme f o k x =
 398   (match clearme with
 399    | Errors.OK a -> (fun f0 o0 k0 _ h _ -> h a __ __)
 400    | Errors.Error m ->
 401      (fun f0 o0 k0 _ x0 _ ->
 402        Obj.magic iO_discr (Wrong m) (Interact (o0, k0)) __)) f o k __ x __
 403
 404 (** val bindIO_opt_interact :
 405     Errors.errmsg -> 'a3 Types.option -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a1
 406     -> ('a2 -> ('a1, 'a2, 'a4) iO) -> ('a3 -> __ -> __ -> 'a5) -> 'a5 **)
 407 let bindIO_opt_interact m clearme f o k x =
 408   (match clearme with
 409    | Types.None ->
 410      (fun f0 o0 k0 _ x0 _ ->
 411        Obj.magic iO_discr (Wrong m) (Interact (o0, k0)) __)
 412    | Types.Some a -> (fun f0 o0 k0 _ h _ -> h a __ __)) f o k __ x __
 413
 414 (** val eq_to_rel_io__o__io_eq_from_res__o__inject :
 415     'a2 Errors.res -> 'a2 -> __ Types.sig0 **)
 416 let eq_to_rel_io__o__io_eq_from_res__o__inject x3 x4 =
 417   __
 418
 419 (** val eq_to_rel_io__o__io_eq_from_res__o__opt_eq_from_res__o__inject :
 420     Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 **)
 421 let eq_to_rel_io__o__io_eq_from_res__o__opt_eq_from_res__o__inject x2 x4 x5 =
 422   Errors.opt_eq_from_res__o__inject x2 x4 x5
 423
 424 (** val jmeq_to_eq__o__io_eq_from_res__o__inject :
 425     'a2 Errors.res -> 'a2 -> __ Types.sig0 **)
 426 let jmeq_to_eq__o__io_eq_from_res__o__inject x3 x4 =
 427   __
 428
 429 (** val jmeq_to_eq__o__io_eq_from_res__o__opt_eq_from_res__o__inject :
 430     Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 **)
 431 let jmeq_to_eq__o__io_eq_from_res__o__opt_eq_from_res__o__inject x1 x3 x4 =
 432   Errors.opt_eq_from_res__o__inject x1 x3 x4
 433
 434 (** val dpi1__o__io_eq_from_res__o__inject :
 435     'a2 Errors.res -> 'a2 -> (__, 'a4) Types.dPair -> __ Types.sig0 **)
 436 let dpi1__o__io_eq_from_res__o__inject x3 x4 x7 =
 437   __
 438
 439 (** val dpi1__o__io_eq_from_res__o__opt_eq_from_res__o__inject :
 440     Errors.errmsg -> 'a1 Types.option -> 'a1 -> (__, 'a4) Types.dPair -> __
 441     Types.sig0 **)
 442 let dpi1__o__io_eq_from_res__o__opt_eq_from_res__o__inject x1 x3 x4 x8 =
 443   Errors.opt_eq_from_res__o__inject x1 x3 x4
 444
 445 (** val eject__o__io_eq_from_res__o__inject :
 446     'a2 Errors.res -> 'a2 -> __ Types.sig0 -> __ Types.sig0 **)
 447 let eject__o__io_eq_from_res__o__inject x3 x4 x7 =
 448   __
 449
 450 (** val eject__o__io_eq_from_res__o__opt_eq_from_res__o__inject :
 451     Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 -> __
 452     Types.sig0 **)
 453 let eject__o__io_eq_from_res__o__opt_eq_from_res__o__inject x1 x3 x4 x8 =
 454   Errors.opt_eq_from_res__o__inject x1 x3 x4
 455
 456 (** val io_eq_from_res__o__opt_eq_from_res__o__inject :
 457     Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 **)
 458 let io_eq_from_res__o__opt_eq_from_res__o__inject x1 x3 x4 =
 459   Errors.opt_eq_from_res__o__inject x1 x3 x4
 460
 461 (** val io_eq_from_res__o__inject :
 462     'a2 Errors.res -> 'a2 -> __ Types.sig0 **)
 463 let io_eq_from_res__o__inject x3 x4 =
 464   __
 465
 466 (** val jmeq_to_eq__o__io_monad_eq_from_res__o__inject :
 467     'a2 Errors.res -> 'a2 -> __ Types.sig0 **)
 468 let jmeq_to_eq__o__io_monad_eq_from_res__o__inject x3 x4 =
 469   __
 470
 471 (** val jmeq_to_eq__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject :
 472     Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 **)
 473 let jmeq_to_eq__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject x1 x3 x4 =
 474   Errors.opt_eq_from_res__o__inject x1 x3 x4
 475
 476 (** val dpi1__o__io_monad_eq_from_res__o__inject :
 477     'a2 Errors.res -> 'a2 -> (__, 'a4) Types.dPair -> __ Types.sig0 **)
 478 let dpi1__o__io_monad_eq_from_res__o__inject x3 x4 x7 =
 479   __
 480
 481 (** val dpi1__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject :
 482     Errors.errmsg -> 'a1 Types.option -> 'a1 -> (__, 'a4) Types.dPair -> __
 483     Types.sig0 **)
 484 let dpi1__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject x1 x3 x4 x8 =
 485   Errors.opt_eq_from_res__o__inject x1 x3 x4
 486
 487 (** val eject__o__io_monad_eq_from_res__o__inject :
 488     'a2 Errors.res -> 'a2 -> __ Types.sig0 -> __ Types.sig0 **)
 489 let eject__o__io_monad_eq_from_res__o__inject x3 x4 x7 =
 490   __
 491
 492 (** val eject__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject :
 493     Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 -> __
 494     Types.sig0 **)
 495 let eject__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject x1 x3 x4 x8 =
 496   Errors.opt_eq_from_res__o__inject x1 x3 x4
 497
 498 (** val io_monad_eq_from_res__o__opt_eq_from_res__o__inject :
 499     Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 **)
 500 let io_monad_eq_from_res__o__opt_eq_from_res__o__inject x1 x3 x4 =
 501   Errors.opt_eq_from_res__o__inject x1 x3 x4
 502
 503 (** val io_monad_eq_from_res__o__inject :
 504     'a2 Errors.res -> 'a2 -> __ Types.sig0 **)
 505 let io_monad_eq_from_res__o__inject x3 x4 =
 506   __
 507
 508 (** val eq_to_rel_io__o__io_eq_from_opt__o__inject :
 509     Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 **)
 510 let eq_to_rel_io__o__io_eq_from_opt__o__inject x2 x4 x5 =
 511   __
 512
 513 (** val jmeq_to_eq__o__io_eq_from_opt__o__inject :
 514     Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 **)
 515 let jmeq_to_eq__o__io_eq_from_opt__o__inject x2 x4 x5 =
 516   __
 517
 518 (** val dpi1__o__io_eq_from_opt__o__inject :
 519     Errors.errmsg -> 'a2 Types.option -> 'a2 -> (__, 'a4) Types.dPair -> __
 520     Types.sig0 **)
 521 let dpi1__o__io_eq_from_opt__o__inject x2 x4 x5 x8 =
 522   __
 523
 524 (** val eject__o__io_eq_from_opt__o__inject :
 525     Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 -> __
 526     Types.sig0 **)
 527 let eject__o__io_eq_from_opt__o__inject x2 x4 x5 x8 =
 528   __
 529
 530 (** val io_eq_from_opt__o__inject :
 531     Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 **)
 532 let io_eq_from_opt__o__inject x2 x4 x5 =
 533   __
 534
 535 (** val jmeq_to_eq__o__io_monad_eq_from_opt__o__inject :
 536     Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 **)
 537 let jmeq_to_eq__o__io_monad_eq_from_opt__o__inject x2 x4 x5 =
 538   __
 539
 540 (** val dpi1__o__io_monad_eq_from_opt__o__inject :
 541     Errors.errmsg -> 'a2 Types.option -> 'a2 -> (__, 'a4) Types.dPair -> __
 542     Types.sig0 **)
 543 let dpi1__o__io_monad_eq_from_opt__o__inject x2 x4 x5 x8 =
 544   __
 545
 546 (** val eject__o__io_monad_eq_from_opt__o__inject :
 547     Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 -> __
 548     Types.sig0 **)
 549 let eject__o__io_monad_eq_from_opt__o__inject x2 x4 x5 x8 =
 550   __
 551
 552 (** val io_monad_eq_from_opt__o__inject :
 553     Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 **)
 554 let io_monad_eq_from_opt__o__inject x2 x4 x5 =
 555   __
 556