open Preamble

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Bool

open Relations

open Nat

open List

open Positive

open PreIdentifiers

open Jmeq

open Russell

open Setoids

open Monad

open Option

open ErrorMessages

type errcode =
| MSG of ErrorMessages.errorMessage
| CTX of PreIdentifiers.identifierTag * PreIdentifiers.identifier

(** val errcode_rect_Type4 :
    (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
    PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1 **)
let rec errcode_rect_Type4 h_MSG h_CTX = function
| MSG x_3113 -> h_MSG x_3113
| CTX (tag, x_3114) -> h_CTX tag x_3114

(** val errcode_rect_Type5 :
    (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
    PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1 **)
let rec errcode_rect_Type5 h_MSG h_CTX = function
| MSG x_3118 -> h_MSG x_3118
| CTX (tag, x_3119) -> h_CTX tag x_3119

(** val errcode_rect_Type3 :
    (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
    PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1 **)
let rec errcode_rect_Type3 h_MSG h_CTX = function
| MSG x_3123 -> h_MSG x_3123
| CTX (tag, x_3124) -> h_CTX tag x_3124

(** val errcode_rect_Type2 :
    (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
    PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1 **)
let rec errcode_rect_Type2 h_MSG h_CTX = function
| MSG x_3128 -> h_MSG x_3128
| CTX (tag, x_3129) -> h_CTX tag x_3129

(** val errcode_rect_Type1 :
    (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
    PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1 **)
let rec errcode_rect_Type1 h_MSG h_CTX = function
| MSG x_3133 -> h_MSG x_3133
| CTX (tag, x_3134) -> h_CTX tag x_3134

(** val errcode_rect_Type0 :
    (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
    PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1 **)
let rec errcode_rect_Type0 h_MSG h_CTX = function
| MSG x_3138 -> h_MSG x_3138
| CTX (tag, x_3139) -> h_CTX tag x_3139

(** val errcode_inv_rect_Type4 :
    errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
    (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1)
    -> 'a1 **)
let errcode_inv_rect_Type4 hterm h1 h2 =
  let hcut = errcode_rect_Type4 h1 h2 hterm in hcut __

(** val errcode_inv_rect_Type3 :
    errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
    (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1)
    -> 'a1 **)
let errcode_inv_rect_Type3 hterm h1 h2 =
  let hcut = errcode_rect_Type3 h1 h2 hterm in hcut __

(** val errcode_inv_rect_Type2 :
    errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
    (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1)
    -> 'a1 **)
let errcode_inv_rect_Type2 hterm h1 h2 =
  let hcut = errcode_rect_Type2 h1 h2 hterm in hcut __

(** val errcode_inv_rect_Type1 :
    errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
    (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1)
    -> 'a1 **)
let errcode_inv_rect_Type1 hterm h1 h2 =
  let hcut = errcode_rect_Type1 h1 h2 hterm in hcut __

(** val errcode_inv_rect_Type0 :
    errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
    (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1)
    -> 'a1 **)
let errcode_inv_rect_Type0 hterm h1 h2 =
  let hcut = errcode_rect_Type0 h1 h2 hterm in hcut __

(** val errcode_discr : errcode -> errcode -> __ **)
let errcode_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | MSG a0 -> Obj.magic (fun _ dH -> dH __)
     | CTX (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y

(** val errcode_jmdiscr : errcode -> errcode -> __ **)
let errcode_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | MSG a0 -> Obj.magic (fun _ dH -> dH __)
     | CTX (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y

type errmsg = errcode List.list

(** val msg : ErrorMessages.errorMessage -> errmsg **)
let msg s =
  List.Cons ((MSG s), List.Nil)

type 'a res =
| OK of 'a
| Error of errmsg

(** val res_rect_Type4 :
    ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
let rec res_rect_Type4 h_OK h_Error = function
| OK x_3178 -> h_OK x_3178
| Error x_3179 -> h_Error x_3179

(** val res_rect_Type5 :
    ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
let rec res_rect_Type5 h_OK h_Error = function
| OK x_3183 -> h_OK x_3183
| Error x_3184 -> h_Error x_3184

(** val res_rect_Type3 :
    ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
let rec res_rect_Type3 h_OK h_Error = function
| OK x_3188 -> h_OK x_3188
| Error x_3189 -> h_Error x_3189

(** val res_rect_Type2 :
    ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
let rec res_rect_Type2 h_OK h_Error = function
| OK x_3193 -> h_OK x_3193
| Error x_3194 -> h_Error x_3194

(** val res_rect_Type1 :
    ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
let rec res_rect_Type1 h_OK h_Error = function
| OK x_3198 -> h_OK x_3198
| Error x_3199 -> h_Error x_3199

(** val res_rect_Type0 :
    ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
let rec res_rect_Type0 h_OK h_Error = function
| OK x_3203 -> h_OK x_3203
| Error x_3204 -> h_Error x_3204

(** val res_inv_rect_Type4 :
    'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2 **)
let res_inv_rect_Type4 hterm h1 h2 =
  let hcut = res_rect_Type4 h1 h2 hterm in hcut __

(** val res_inv_rect_Type3 :
    'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2 **)
let res_inv_rect_Type3 hterm h1 h2 =
  let hcut = res_rect_Type3 h1 h2 hterm in hcut __

(** val res_inv_rect_Type2 :
    'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2 **)
let res_inv_rect_Type2 hterm h1 h2 =
  let hcut = res_rect_Type2 h1 h2 hterm in hcut __

(** val res_inv_rect_Type1 :
    'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2 **)
let res_inv_rect_Type1 hterm h1 h2 =
  let hcut = res_rect_Type1 h1 h2 hterm in hcut __

(** val res_inv_rect_Type0 :
    'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2 **)
let res_inv_rect_Type0 hterm h1 h2 =
  let hcut = res_rect_Type0 h1 h2 hterm in hcut __

(** val res_discr : 'a1 res -> 'a1 res -> __ **)
let res_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | OK a0 -> Obj.magic (fun _ dH -> dH __)
     | Error a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val res_jmdiscr : 'a1 res -> 'a1 res -> __ **)
let res_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | OK a0 -> Obj.magic (fun _ dH -> dH __)
     | Error a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val res0 : Monad.monadProps **)
let res0 =
  Monad.makeMonadProps (fun _ x -> OK x) (fun _ _ m f ->
    match m with
    | OK x -> f x
    | Error msg0 -> Error msg0)

(** val mfold_left_i_aux :
    (Nat.nat -> 'a1 -> 'a2 -> 'a1 res) -> 'a1 res -> Nat.nat -> 'a2 List.list
    -> __ **)
let rec mfold_left_i_aux f x i = function
| List.Nil -> Obj.magic x
| List.Cons (hd, tl) ->
  Monad.m_bind0 (Monad.max_def res0) (Obj.magic x) (fun x0 ->
    mfold_left_i_aux f (f i x0 hd) (Nat.S i) tl)

(** val mfold_left_i :
    (Nat.nat -> 'a1 -> 'a2 -> 'a1 res) -> 'a1 res -> 'a2 List.list -> __ **)
let mfold_left_i f x =
  mfold_left_i_aux f x Nat.O

(** val mfold_left2 :
    ('a1 -> 'a2 -> 'a3 -> 'a1 res) -> 'a1 res -> 'a2 List.list -> 'a3
    List.list -> 'a1 res **)
let rec mfold_left2 f accu left right =
  match left with
  | List.Nil ->
    (match right with
     | List.Nil -> accu
     | List.Cons (hd, tl) -> Error (msg ErrorMessages.WrongLength))
  | List.Cons (hd, tl) ->
    (match right with
     | List.Nil -> Error (msg ErrorMessages.WrongLength)
     | List.Cons (hd', tl') ->
       Obj.magic
         (Monad.m_bind0 (Monad.max_def res0) (Obj.magic accu) (fun accu0 ->
           Obj.magic (mfold_left2 f (f accu0 hd hd') tl tl'))))

(** val opt_to_res : errmsg -> 'a1 Types.option -> 'a1 res **)
let opt_to_res msg0 = function
| Types.None -> Error msg0
| Types.Some v0 -> OK v0

(** val jmeq_to_eq__o__opt_eq_from_res__o__inject :
    errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 **)
let jmeq_to_eq__o__opt_eq_from_res__o__inject x1 x2 x3 =
  __

(** val dpi1__o__opt_eq_from_res__o__inject :
    errmsg -> 'a1 Types.option -> 'a1 -> (__, 'a2) Types.dPair -> __
    Types.sig0 **)
let dpi1__o__opt_eq_from_res__o__inject x1 x2 x3 x6 =
  __

(** val eject__o__opt_eq_from_res__o__inject :
    errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 -> __ Types.sig0 **)
let eject__o__opt_eq_from_res__o__inject x1 x2 x3 x6 =
  __

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

(** val bind_eq : 'a1 res -> ('a1 -> __ -> 'a2 res) -> 'a2 res **)
let bind_eq f g =
  (match f with
   | OK x -> g x
   | Error msg0 -> (fun _ -> Error msg0)) __

(** val bind2_eq :
    ('a1, 'a2) Types.prod res -> ('a1 -> 'a2 -> __ -> 'a3 res) -> 'a3 res **)
let bind2_eq f g =
  (match f with
   | OK x -> let { Types.fst = a; Types.snd = b } = x in g a b
   | Error msg0 -> (fun _ -> Error msg0)) __

(** val res_to_opt : 'a1 res -> 'a1 Types.option **)
let res_to_opt = function
| OK v0 -> Types.Some v0
| Error x -> Types.None

(** val bind : __ -> ('a1 -> __) -> __ **)
let bind x_768 x_769 =
  Monad.m_bind0 (Monad.max_def res0) x_768 x_769

(** val bind2 : __ -> ('a1 -> 'a2 -> __) -> __ **)
let bind2 m f =
  Monad.m_bind2 (Monad.max_def res0) m f

(** val bind3 : __ -> ('a1 -> 'a2 -> 'a3 -> __) -> __ **)
let bind3 x x0 =
  Monad.m_bind3 (Monad.max_def res0) x x0

(** val mmap : ('a1 -> __) -> 'a1 List.list -> __ **)
let mmap x x0 =
  Monad.m_list_map (Monad.max_def res0) x x0

(** val mmap_sigma : ('a1 -> __) -> 'a1 List.list -> __ **)
let mmap_sigma x x0 =
  Monad.m_list_map_sigma (Monad.max_def res0) x x0