source: driver/extracted/iOMonad.ml @ 3085

open Preamble

open Div_and_mod

open Jmeq

open Russell

open Util

open Bool

open Relations

open Nat

open List

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Extralib

open ErrorMessages

open Option

open Setoids

open Monad

open Positive

open PreIdentifiers

open Errors

type ('output, 'input, 't) iO =
| Interact of 'output * ('input -> ('output, 'input, 't) iO)
| Value of 't
| Wrong of Errors.errmsg

(** val iO_rect_Type4 :
    ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 ->
    'a4) -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4 **)
let rec iO_rect_Type4 h_Interact h_Value h_Wrong = function
| Interact (o, x_4685) ->
  h_Interact o x_4685 (fun x_4684 ->
    iO_rect_Type4 h_Interact h_Value h_Wrong (x_4685 x_4684))
| Value x_4686 -> h_Value x_4686
| Wrong x_4687 -> h_Wrong x_4687

(** val iO_rect_Type3 :
    ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 ->
    'a4) -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4 **)
let rec iO_rect_Type3 h_Interact h_Value h_Wrong = function
| Interact (o, x_4701) ->
  h_Interact o x_4701 (fun x_4700 ->
    iO_rect_Type3 h_Interact h_Value h_Wrong (x_4701 x_4700))
| Value x_4702 -> h_Value x_4702
| Wrong x_4703 -> h_Wrong x_4703

(** val iO_rect_Type2 :
    ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 ->
    'a4) -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4 **)
let rec iO_rect_Type2 h_Interact h_Value h_Wrong = function
| Interact (o, x_4709) ->
  h_Interact o x_4709 (fun x_4708 ->
    iO_rect_Type2 h_Interact h_Value h_Wrong (x_4709 x_4708))
| Value x_4710 -> h_Value x_4710
| Wrong x_4711 -> h_Wrong x_4711

(** val iO_rect_Type1 :
    ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 ->
    'a4) -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4 **)
let rec iO_rect_Type1 h_Interact h_Value h_Wrong = function
| Interact (o, x_4717) ->
  h_Interact o x_4717 (fun x_4716 ->
    iO_rect_Type1 h_Interact h_Value h_Wrong (x_4717 x_4716))
| Value x_4718 -> h_Value x_4718
| Wrong x_4719 -> h_Wrong x_4719

(** val iO_rect_Type0 :
    ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 ->
    'a4) -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4 **)
let rec iO_rect_Type0 h_Interact h_Value h_Wrong = function
| Interact (o, x_4725) ->
  h_Interact o x_4725 (fun x_4724 ->
    iO_rect_Type0 h_Interact h_Value h_Wrong (x_4725 x_4724))
| Value x_4726 -> h_Value x_4726
| Wrong x_4727 -> h_Wrong x_4727

(** val iO_inv_rect_Type4 :
    ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __
    -> 'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ ->
    'a4) -> 'a4 **)
let iO_inv_rect_Type4 hterm h1 h2 h3 =
  let hcut = iO_rect_Type4 h1 h2 h3 hterm in hcut __

(** val iO_inv_rect_Type3 :
    ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __
    -> 'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ ->
    'a4) -> 'a4 **)
let iO_inv_rect_Type3 hterm h1 h2 h3 =
  let hcut = iO_rect_Type3 h1 h2 h3 hterm in hcut __

(** val iO_inv_rect_Type2 :
    ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __
    -> 'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ ->
    'a4) -> 'a4 **)
let iO_inv_rect_Type2 hterm h1 h2 h3 =
  let hcut = iO_rect_Type2 h1 h2 h3 hterm in hcut __

(** val iO_inv_rect_Type1 :
    ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __
    -> 'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ ->
    'a4) -> 'a4 **)
let iO_inv_rect_Type1 hterm h1 h2 h3 =
  let hcut = iO_rect_Type1 h1 h2 h3 hterm in hcut __

(** val iO_inv_rect_Type0 :
    ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __
    -> 'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ ->
    'a4) -> 'a4 **)
let iO_inv_rect_Type0 hterm h1 h2 h3 =
  let hcut = iO_rect_Type0 h1 h2 h3 hterm in hcut __

(** val iO_discr : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3) iO -> __ **)
let iO_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Interact (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Value a0 -> Obj.magic (fun _ dH -> dH __)
     | Wrong a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val iO_jmdiscr : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3) iO -> __ **)
let iO_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Interact (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Value a0 -> Obj.magic (fun _ dH -> dH __)
     | Wrong a0 -> Obj.magic (fun _ dH -> dH __)) y

open Proper

(** val bindIO :
    ('a1, 'a2, 'a3) iO -> ('a3 -> ('a1, 'a2, 'a4) iO) -> ('a1, 'a2, 'a4) iO **)
let rec bindIO v f =
  match v with
  | Interact (out, k) -> Interact (out, (fun res -> bindIO (k res) f))
  | Value v' -> f v'
  | Wrong m -> Wrong m

(** val iOMonad : Monad.monadProps **)
let iOMonad =
  Monad.makeMonadProps (fun _ x -> Value x) (fun _ _ -> bindIO)

(** val bindIO2 : __ -> ('a3 -> 'a4 -> __) -> __ **)
let bindIO2 m f =
  Monad.m_bind2 (Monad.max_def iOMonad) m f

(** val iORel : Monad.monadRel **)
let iORel =
  Monad.Mk_MonadRel

(** val pred_io_inject :
    ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3 Types.sig0) iO **)
let rec pred_io_inject a =
  (match a with
   | Interact (o, f) ->
     (fun _ -> Interact (o, (fun x -> pred_io_inject (f x))))
   | Value x ->
     (fun _ -> Obj.magic (Monad.m_return0 (Monad.max_def iOMonad) x))
   | Wrong e -> (fun _ -> Wrong e)) __

(** val iOPred : Monad.injMonadPred **)
let iOPred =
  { Monad.im_pred = Monad.Mk_MonadPred; Monad.mp_inject = (fun _ _ a_sig ->
    let a = a_sig in Obj.magic (pred_io_inject (Obj.magic a))) }

(** val err_to_io : 'a3 Errors.res -> ('a1, 'a2, 'a3) iO **)
let err_to_io = function
| Errors.OK v' -> Value v'
| Errors.Error m -> Wrong m

(** val dpi1__o__err_to_io__o__inject :
    ('a2 Errors.res, 'a3) Types.dPair -> ('a1, 'a4, 'a2) iO Types.sig0 **)
let dpi1__o__err_to_io__o__inject x4 =
  err_to_io x4.Types.dpi1

(** val eject__o__err_to_io__o__inject :
    'a2 Errors.res Types.sig0 -> ('a1, 'a3, 'a2) iO Types.sig0 **)
let eject__o__err_to_io__o__inject x4 =
  err_to_io (Types.pi1 x4)

(** val err_to_io__o__inject :
    'a2 Errors.res -> ('a1, 'a3, 'a2) iO Types.sig0 **)
let err_to_io__o__inject x3 =
  err_to_io x3

(** val dpi1__o__err_to_io :
    ('a2 Errors.res, 'a3) Types.dPair -> ('a1, 'a4, 'a2) iO **)
let dpi1__o__err_to_io x4 =
  err_to_io x4.Types.dpi1

(** val eject__o__err_to_io :
    'a2 Errors.res Types.sig0 -> ('a1, 'a3, 'a2) iO **)
let eject__o__err_to_io x4 =
  err_to_io (Types.pi1 x4)

(** val err_to_io_sig :
    'a3 Types.sig0 Errors.res -> ('a1, 'a2, 'a3 Types.sig0) iO **)
let err_to_io_sig = function
| Errors.OK v' -> Value v'
| Errors.Error m -> Wrong m

(** val io_inject_0 : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3 Types.sig0) iO **)
let rec io_inject_0 a =
  (match a with
   | Interact (out, k) ->
     (fun _ -> Interact (out, (fun v -> io_inject_0 (k v))))
   | Value c -> (fun _ -> Value c)
   | Wrong m -> (fun _ -> Wrong m)) __

(** val io_inject :
    ('a1, 'a2, 'a3) iO Types.option -> ('a1, 'a2, 'a3 Types.sig0) iO **)
let io_inject a =
  (match a with
   | Types.None -> (fun _ -> Logic.false_rect_Type0 __)
   | Types.Some b -> (fun _ -> io_inject_0 b)) __

(** val io_eject : ('a1, 'a2, 'a3 Types.sig0) iO -> ('a1, 'a2, 'a3) iO **)
let rec io_eject = function
| Interact (out, k) -> Interact (out, (fun v -> io_eject (k v)))
| Value b -> let w = b in Value w
| Wrong m -> Wrong m

(** val dpi1__o__io_inject__o__inject :
    (('a1, 'a3, 'a2) iO Types.option, 'a4) Types.dPair -> ('a1, 'a3, 'a2
    Types.sig0) iO Types.sig0 **)
let dpi1__o__io_inject__o__inject x6 =
  io_inject x6.Types.dpi1

(** val eject__o__io_inject__o__inject :
    ('a1, 'a3, 'a2) iO Types.option Types.sig0 -> ('a1, 'a3, 'a2 Types.sig0)
    iO Types.sig0 **)
let eject__o__io_inject__o__inject x6 =
  io_inject (Types.pi1 x6)

(** val io_inject__o__inject :
    ('a1, 'a3, 'a2) iO Types.option -> ('a1, 'a3, 'a2 Types.sig0) iO
    Types.sig0 **)
let io_inject__o__inject x5 =
  io_inject x5

(** val dpi1__o__io_inject :
    (('a1, 'a3, 'a2) iO Types.option, 'a4) Types.dPair -> ('a1, 'a3, 'a2
    Types.sig0) iO **)
let dpi1__o__io_inject x5 =
  io_inject x5.Types.dpi1

(** val eject__o__io_inject :
    ('a1, 'a3, 'a2) iO Types.option Types.sig0 -> ('a1, 'a3, 'a2 Types.sig0)
    iO **)
let eject__o__io_inject x5 =
  io_inject (Types.pi1 x5)

(** val io_inject__o__io_eject__o__inject :
    ('a1, 'a3, 'a2) iO Types.option -> ('a1, 'a3, 'a2) iO Types.sig0 **)
let io_inject__o__io_eject__o__inject x4 =
  io_eject (io_inject x4)

(** val dpi1__o__err_to_io__o__io_eject__o__inject :
    ('a2 Types.sig0 Errors.res, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO
    Types.sig0 **)
let dpi1__o__err_to_io__o__io_eject__o__inject x6 =
  io_eject (dpi1__o__err_to_io x6)

(** val dpi1__o__io_inject__o__io_eject__o__inject :
    (('a1, 'a3, 'a2) iO Types.option, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO
    Types.sig0 **)
let dpi1__o__io_inject__o__io_eject__o__inject x6 =
  io_eject (dpi1__o__io_inject x6)

(** val eject__o__err_to_io__o__io_eject__o__inject :
    'a2 Types.sig0 Errors.res Types.sig0 -> ('a1, 'a3, 'a2) iO Types.sig0 **)
let eject__o__err_to_io__o__io_eject__o__inject x6 =
  io_eject (eject__o__err_to_io x6)

(** val eject__o__io_inject__o__io_eject__o__inject :
    ('a1, 'a3, 'a2) iO Types.option Types.sig0 -> ('a1, 'a3, 'a2) iO
    Types.sig0 **)
let eject__o__io_inject__o__io_eject__o__inject x6 =
  io_eject (eject__o__io_inject x6)

(** val err_to_io__o__io_eject__o__inject :
    'a2 Types.sig0 Errors.res -> ('a1, 'a3, 'a2) iO Types.sig0 **)
let err_to_io__o__io_eject__o__inject x4 =
  io_eject (err_to_io x4)

(** val dpi1__o__io_eject__o__inject :
    (('a1, 'a3, 'a2 Types.sig0) iO, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO
    Types.sig0 **)
let dpi1__o__io_eject__o__inject x6 =
  io_eject x6.Types.dpi1

(** val eject__o__io_eject__o__inject :
    ('a1, 'a3, 'a2 Types.sig0) iO Types.sig0 -> ('a1, 'a3, 'a2) iO Types.sig0 **)
let eject__o__io_eject__o__inject x6 =
  io_eject (Types.pi1 x6)

(** val io_eject__o__inject :
    ('a1, 'a3, 'a2 Types.sig0) iO -> ('a1, 'a3, 'a2) iO Types.sig0 **)
let io_eject__o__inject x5 =
  io_eject x5

(** val io_inject__o__io_eject :
    ('a1, 'a3, 'a2) iO Types.option -> ('a1, 'a3, 'a2) iO **)
let io_inject__o__io_eject x4 =
  io_eject (io_inject x4)

(** val dpi1__o__err_to_io__o__io_eject :
    ('a2 Types.sig0 Errors.res, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO **)
let dpi1__o__err_to_io__o__io_eject x5 =
  io_eject (dpi1__o__err_to_io x5)

(** val dpi1__o__io_inject__o__io_eject :
    (('a1, 'a3, 'a2) iO Types.option, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO **)
let dpi1__o__io_inject__o__io_eject x5 =
  io_eject (dpi1__o__io_inject x5)

(** val eject__o__err_to_io__o__io_eject :
    'a2 Types.sig0 Errors.res Types.sig0 -> ('a1, 'a3, 'a2) iO **)
let eject__o__err_to_io__o__io_eject x5 =
  io_eject (eject__o__err_to_io x5)

(** val eject__o__io_inject__o__io_eject :
    ('a1, 'a3, 'a2) iO Types.option Types.sig0 -> ('a1, 'a3, 'a2) iO **)
let eject__o__io_inject__o__io_eject x5 =
  io_eject (eject__o__io_inject x5)

(** val err_to_io__o__io_eject :
    'a2 Types.sig0 Errors.res -> ('a1, 'a3, 'a2) iO **)
let err_to_io__o__io_eject x4 =
  io_eject (err_to_io x4)

(** val dpi1__o__io_eject :
    (('a1, 'a3, 'a2 Types.sig0) iO, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO **)
let dpi1__o__io_eject x5 =
  io_eject x5.Types.dpi1

(** val eject__o__io_eject :
    ('a1, 'a3, 'a2 Types.sig0) iO Types.sig0 -> ('a1, 'a3, 'a2) iO **)
let eject__o__io_eject x5 =
  io_eject (Types.pi1 x5)

(** val opt_to_io :
    Errors.errmsg -> 'a3 Types.option -> ('a1, 'a2, 'a3) iO **)
let opt_to_io m = function
| Types.None -> Wrong m
| Types.Some v' -> Value v'

(** val bind_res_value :
    'a3 Errors.res -> ('a3 -> 'a4 Errors.res) -> 'a4 -> ('a3 -> __ -> __ ->
    'a5) -> 'a5 **)
let bind_res_value clearme f v x =
  (match clearme with
   | Errors.OK a -> (fun f0 v0 _ h _ -> h a __ __)
   | Errors.Error m ->
     (fun f0 v0 _ h _ -> Obj.magic iO_discr (Wrong m) (Value v0) __)) f v __
    x __

(** val bindIO_value :
    ('a1, 'a2, 'a3) iO -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a4 -> ('a3 -> __ ->
    __ -> 'a5) -> 'a5 **)
let bindIO_value clearme f v x =
  (match clearme with
   | Interact (o, k) ->
     (fun f0 v0 _ h _ ->
       Obj.magic iO_discr (Interact (o, (fun res -> bindIO (k res) f0)))
         (Value v0) __)
   | Value a -> (fun f0 v0 _ h _ -> h a __ __)
   | Wrong m ->
     (fun f0 v0 _ h _ -> Obj.magic iO_discr (Wrong m) (Value v0) __)) f v __
    x __

(** val bindIO_res_interact :
    'a3 Errors.res -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a1 -> ('a2 -> ('a1,
    'a2, 'a4) iO) -> ('a3 -> __ -> __ -> 'a5) -> 'a5 **)
let bindIO_res_interact clearme f o k x =
  (match clearme with
   | Errors.OK a -> (fun f0 o0 k0 _ h _ -> h a __ __)
   | Errors.Error m ->
     (fun f0 o0 k0 _ x0 _ ->
       Obj.magic iO_discr (Wrong m) (Interact (o0, k0)) __)) f o k __ x __

(** val bindIO_opt_interact :
    Errors.errmsg -> 'a3 Types.option -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a1
    -> ('a2 -> ('a1, 'a2, 'a4) iO) -> ('a3 -> __ -> __ -> 'a5) -> 'a5 **)
let bindIO_opt_interact m clearme f o k x =
  (match clearme with
   | Types.None ->
     (fun f0 o0 k0 _ x0 _ ->
       Obj.magic iO_discr (Wrong m) (Interact (o0, k0)) __)
   | Types.Some a -> (fun f0 o0 k0 _ h _ -> h a __ __)) f o k __ x __

(** val eq_to_rel_io__o__io_eq_from_res__o__inject :
    'a2 Errors.res -> 'a2 -> __ Types.sig0 **)
let eq_to_rel_io__o__io_eq_from_res__o__inject x3 x4 =
  __

(** val eq_to_rel_io__o__io_eq_from_res__o__opt_eq_from_res__o__inject :
    Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 **)
let eq_to_rel_io__o__io_eq_from_res__o__opt_eq_from_res__o__inject x2 x4 x5 =
  Errors.opt_eq_from_res__o__inject x2 x4 x5

(** val jmeq_to_eq__o__io_eq_from_res__o__inject :
    'a2 Errors.res -> 'a2 -> __ Types.sig0 **)
let jmeq_to_eq__o__io_eq_from_res__o__inject x3 x4 =
  __

(** val jmeq_to_eq__o__io_eq_from_res__o__opt_eq_from_res__o__inject :
    Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 **)
let jmeq_to_eq__o__io_eq_from_res__o__opt_eq_from_res__o__inject x1 x3 x4 =
  Errors.opt_eq_from_res__o__inject x1 x3 x4

(** val dpi1__o__io_eq_from_res__o__inject :
    'a2 Errors.res -> 'a2 -> (__, 'a4) Types.dPair -> __ Types.sig0 **)
let dpi1__o__io_eq_from_res__o__inject x3 x4 x7 =
  __

(** val dpi1__o__io_eq_from_res__o__opt_eq_from_res__o__inject :
    Errors.errmsg -> 'a1 Types.option -> 'a1 -> (__, 'a4) Types.dPair -> __
    Types.sig0 **)
let dpi1__o__io_eq_from_res__o__opt_eq_from_res__o__inject x1 x3 x4 x8 =
  Errors.opt_eq_from_res__o__inject x1 x3 x4

(** val eject__o__io_eq_from_res__o__inject :
    'a2 Errors.res -> 'a2 -> __ Types.sig0 -> __ Types.sig0 **)
let eject__o__io_eq_from_res__o__inject x3 x4 x7 =
  __

(** val eject__o__io_eq_from_res__o__opt_eq_from_res__o__inject :
    Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 -> __
    Types.sig0 **)
let eject__o__io_eq_from_res__o__opt_eq_from_res__o__inject x1 x3 x4 x8 =
  Errors.opt_eq_from_res__o__inject x1 x3 x4

(** val io_eq_from_res__o__opt_eq_from_res__o__inject :
    Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 **)
let io_eq_from_res__o__opt_eq_from_res__o__inject x1 x3 x4 =
  Errors.opt_eq_from_res__o__inject x1 x3 x4

(** val io_eq_from_res__o__inject :
    'a2 Errors.res -> 'a2 -> __ Types.sig0 **)
let io_eq_from_res__o__inject x3 x4 =
  __

(** val jmeq_to_eq__o__io_monad_eq_from_res__o__inject :
    'a2 Errors.res -> 'a2 -> __ Types.sig0 **)
let jmeq_to_eq__o__io_monad_eq_from_res__o__inject x3 x4 =
  __

(** val jmeq_to_eq__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject :
    Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 **)
let jmeq_to_eq__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject x1 x3 x4 =
  Errors.opt_eq_from_res__o__inject x1 x3 x4

(** val dpi1__o__io_monad_eq_from_res__o__inject :
    'a2 Errors.res -> 'a2 -> (__, 'a4) Types.dPair -> __ Types.sig0 **)
let dpi1__o__io_monad_eq_from_res__o__inject x3 x4 x7 =
  __

(** val dpi1__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject :
    Errors.errmsg -> 'a1 Types.option -> 'a1 -> (__, 'a4) Types.dPair -> __
    Types.sig0 **)
let dpi1__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject x1 x3 x4 x8 =
  Errors.opt_eq_from_res__o__inject x1 x3 x4

(** val eject__o__io_monad_eq_from_res__o__inject :
    'a2 Errors.res -> 'a2 -> __ Types.sig0 -> __ Types.sig0 **)
let eject__o__io_monad_eq_from_res__o__inject x3 x4 x7 =
  __

(** val eject__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject :
    Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 -> __
    Types.sig0 **)
let eject__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject x1 x3 x4 x8 =
  Errors.opt_eq_from_res__o__inject x1 x3 x4

(** val io_monad_eq_from_res__o__opt_eq_from_res__o__inject :
    Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 **)
let io_monad_eq_from_res__o__opt_eq_from_res__o__inject x1 x3 x4 =
  Errors.opt_eq_from_res__o__inject x1 x3 x4

(** val io_monad_eq_from_res__o__inject :
    'a2 Errors.res -> 'a2 -> __ Types.sig0 **)
let io_monad_eq_from_res__o__inject x3 x4 =
  __

(** val eq_to_rel_io__o__io_eq_from_opt__o__inject :
    Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 **)
let eq_to_rel_io__o__io_eq_from_opt__o__inject x2 x4 x5 =
  __

(** val jmeq_to_eq__o__io_eq_from_opt__o__inject :
    Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 **)
let jmeq_to_eq__o__io_eq_from_opt__o__inject x2 x4 x5 =
  __

(** val dpi1__o__io_eq_from_opt__o__inject :
    Errors.errmsg -> 'a2 Types.option -> 'a2 -> (__, 'a4) Types.dPair -> __
    Types.sig0 **)
let dpi1__o__io_eq_from_opt__o__inject x2 x4 x5 x8 =
  __

(** val eject__o__io_eq_from_opt__o__inject :
    Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 -> __
    Types.sig0 **)
let eject__o__io_eq_from_opt__o__inject x2 x4 x5 x8 =
  __

(** val io_eq_from_opt__o__inject :
    Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 **)
let io_eq_from_opt__o__inject x2 x4 x5 =
  __

(** val jmeq_to_eq__o__io_monad_eq_from_opt__o__inject :
    Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 **)
let jmeq_to_eq__o__io_monad_eq_from_opt__o__inject x2 x4 x5 =
  __

(** val dpi1__o__io_monad_eq_from_opt__o__inject :
    Errors.errmsg -> 'a2 Types.option -> 'a2 -> (__, 'a4) Types.dPair -> __
    Types.sig0 **)
let dpi1__o__io_monad_eq_from_opt__o__inject x2 x4 x5 x8 =
  __

(** val eject__o__io_monad_eq_from_opt__o__inject :
    Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 -> __
    Types.sig0 **)
let eject__o__io_monad_eq_from_opt__o__inject x2 x4 x5 x8 =
  __

(** val io_monad_eq_from_opt__o__inject :
    Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 **)
let io_monad_eq_from_opt__o__inject x2 x4 x5 =
  __