open Preamble

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Bool

open Relations

open Nat

open Positive

open Setoids

open Monad

open Option

open Div_and_mod

open Jmeq

open Russell

open Util

open List

open Lists

open Extralib

open ErrorMessages

open PreIdentifiers

open Errors

type universe =
  Positive.pos
  (* singleton inductive, whose constructor was mk_universe *)

(** val universe_rect_Type4 :
    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
let rec universe_rect_Type4 tag h_mk_universe x_3239 =
  let next_identifier = x_3239 in h_mk_universe next_identifier

(** val universe_rect_Type5 :
    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
let rec universe_rect_Type5 tag h_mk_universe x_3241 =
  let next_identifier = x_3241 in h_mk_universe next_identifier

(** val universe_rect_Type3 :
    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
let rec universe_rect_Type3 tag h_mk_universe x_3243 =
  let next_identifier = x_3243 in h_mk_universe next_identifier

(** val universe_rect_Type2 :
    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
let rec universe_rect_Type2 tag h_mk_universe x_3245 =
  let next_identifier = x_3245 in h_mk_universe next_identifier

(** val universe_rect_Type1 :
    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
let rec universe_rect_Type1 tag h_mk_universe x_3247 =
  let next_identifier = x_3247 in h_mk_universe next_identifier

(** val universe_rect_Type0 :
    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
let rec universe_rect_Type0 tag h_mk_universe x_3249 =
  let next_identifier = x_3249 in h_mk_universe next_identifier

(** val next_identifier :
    PreIdentifiers.identifierTag -> universe -> Positive.pos **)
let rec next_identifier tag xxx =
  let yyy = xxx in yyy

(** val universe_inv_rect_Type4 :
    PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1)
    -> 'a1 **)
let universe_inv_rect_Type4 x1 hterm h1 =
  let hcut = universe_rect_Type4 x1 h1 hterm in hcut __

(** val universe_inv_rect_Type3 :
    PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1)
    -> 'a1 **)
let universe_inv_rect_Type3 x1 hterm h1 =
  let hcut = universe_rect_Type3 x1 h1 hterm in hcut __

(** val universe_inv_rect_Type2 :
    PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1)
    -> 'a1 **)
let universe_inv_rect_Type2 x1 hterm h1 =
  let hcut = universe_rect_Type2 x1 h1 hterm in hcut __

(** val universe_inv_rect_Type1 :
    PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1)
    -> 'a1 **)
let universe_inv_rect_Type1 x1 hterm h1 =
  let hcut = universe_rect_Type1 x1 h1 hterm in hcut __

(** val universe_inv_rect_Type0 :
    PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1)
    -> 'a1 **)
let universe_inv_rect_Type0 x1 hterm h1 =
  let hcut = universe_rect_Type0 x1 h1 hterm in hcut __

(** val universe_discr :
    PreIdentifiers.identifierTag -> universe -> universe -> __ **)
let universe_discr a1 x y =
  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y

(** val universe_jmdiscr :
    PreIdentifiers.identifierTag -> universe -> universe -> __ **)
let universe_jmdiscr a1 x y =
  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y

(** val new_universe : PreIdentifiers.identifierTag -> universe **)
let new_universe tag =
  Positive.One

(** val fresh :
    PreIdentifiers.identifierTag -> universe -> (PreIdentifiers.identifier,
    universe) Types.prod **)
let rec fresh tag u =
  let id = next_identifier tag u in
  { Types.fst = id; Types.snd = (Positive.succ id) }

(** val eq_identifier :
    PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
    PreIdentifiers.identifier -> Bool.bool **)
let eq_identifier t l r =
  let l' = l in let r' = r in Positive.eqb l' r'

(** val eq_identifier_elim :
    PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
    PreIdentifiers.identifier -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let eq_identifier_elim t clearme =
  let x = clearme in
  (fun clearme0 ->
  let y = clearme0 in
  (fun t0 f -> Positive.eqb_elim x y (fun _ -> t0 __) (fun _ -> f __)))

open Deqsets

(** val deq_identifier : PreIdentifiers.identifierTag -> Deqsets.deqSet **)
let deq_identifier tag =
  Obj.magic (eq_identifier tag)

(** val word_of_identifier :
    PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> Positive.pos **)
let word_of_identifier t l =
  let l' = l in l'

(** val identifier_eq :
    PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
    PreIdentifiers.identifier -> (__, __) Types.sum **)
let identifier_eq tag clearme =
  let x = clearme in
  (fun clearme0 ->
  let y = clearme0 in
  (match Positive.eqb x y with
   | Bool.True -> (fun _ -> Types.Inl __)
   | Bool.False -> (fun _ -> Types.Inr __)) __)

(** val identifier_of_nat :
    PreIdentifiers.identifierTag -> Nat.nat -> PreIdentifiers.identifier **)
let identifier_of_nat tag n =
  Positive.succ_pos_of_nat n

(** val check_member_env :
    PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
    (PreIdentifiers.identifier, 'a1) Types.prod List.list -> __ Errors.res **)
let rec check_member_env tag id = function
| List.Nil -> Errors.OK __
| List.Cons (hd, tl) ->
  (match identifier_eq tag id hd.Types.fst with
   | Types.Inl _ ->
     Errors.Error (List.Cons ((Errors.MSG ErrorMessages.DuplicateVariable),
       (List.Cons ((Errors.CTX (tag, id)), List.Nil))))
   | Types.Inr _ ->
     Obj.magic
       (Monad.m_bind0 (Monad.max_def Errors.res0)
         (Obj.magic (check_member_env tag id tl)) (fun _ ->
         Obj.magic (Errors.OK __))))

(** val check_distinct_env :
    PreIdentifiers.identifierTag -> (PreIdentifiers.identifier, 'a1)
    Types.prod List.list -> __ Errors.res **)
let rec check_distinct_env tag = function
| List.Nil -> Errors.OK __
| List.Cons (hd, tl) ->
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Errors.res0)
      (Obj.magic (check_member_env tag hd.Types.fst tl)) (fun _ ->
      Monad.m_bind0 (Monad.max_def Errors.res0)
        (Obj.magic (check_distinct_env tag tl)) (fun _ ->
        Obj.magic (Errors.OK __))))

open PositiveMap

type 'a identifier_map =
  'a PositiveMap.positive_map
  (* singleton inductive, whose constructor was an_id_map *)

(** val identifier_map_rect_Type4 :
    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
    'a1 identifier_map -> 'a2 **)
let rec identifier_map_rect_Type4 tag h_an_id_map x_3411 =
  let x_3412 = x_3411 in h_an_id_map x_3412

(** val identifier_map_rect_Type5 :
    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
    'a1 identifier_map -> 'a2 **)
let rec identifier_map_rect_Type5 tag h_an_id_map x_3414 =
  let x_3415 = x_3414 in h_an_id_map x_3415

(** val identifier_map_rect_Type3 :
    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
    'a1 identifier_map -> 'a2 **)
let rec identifier_map_rect_Type3 tag h_an_id_map x_3417 =
  let x_3418 = x_3417 in h_an_id_map x_3418

(** val identifier_map_rect_Type2 :
    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
    'a1 identifier_map -> 'a2 **)
let rec identifier_map_rect_Type2 tag h_an_id_map x_3420 =
  let x_3421 = x_3420 in h_an_id_map x_3421

(** val identifier_map_rect_Type1 :
    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
    'a1 identifier_map -> 'a2 **)
let rec identifier_map_rect_Type1 tag h_an_id_map x_3423 =
  let x_3424 = x_3423 in h_an_id_map x_3424

(** val identifier_map_rect_Type0 :
    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
    'a1 identifier_map -> 'a2 **)
let rec identifier_map_rect_Type0 tag h_an_id_map x_3426 =
  let x_3427 = x_3426 in h_an_id_map x_3427

(** val identifier_map_inv_rect_Type4 :
    PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
    PositiveMap.positive_map -> __ -> 'a2) -> 'a2 **)
let identifier_map_inv_rect_Type4 x1 hterm h1 =
  let hcut = identifier_map_rect_Type4 x1 h1 hterm in hcut __

(** val identifier_map_inv_rect_Type3 :
    PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
    PositiveMap.positive_map -> __ -> 'a2) -> 'a2 **)
let identifier_map_inv_rect_Type3 x1 hterm h1 =
  let hcut = identifier_map_rect_Type3 x1 h1 hterm in hcut __

(** val identifier_map_inv_rect_Type2 :
    PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
    PositiveMap.positive_map -> __ -> 'a2) -> 'a2 **)
let identifier_map_inv_rect_Type2 x1 hterm h1 =
  let hcut = identifier_map_rect_Type2 x1 h1 hterm in hcut __

(** val identifier_map_inv_rect_Type1 :
    PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
    PositiveMap.positive_map -> __ -> 'a2) -> 'a2 **)
let identifier_map_inv_rect_Type1 x1 hterm h1 =
  let hcut = identifier_map_rect_Type1 x1 h1 hterm in hcut __

(** val identifier_map_inv_rect_Type0 :
    PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
    PositiveMap.positive_map -> __ -> 'a2) -> 'a2 **)
let identifier_map_inv_rect_Type0 x1 hterm h1 =
  let hcut = identifier_map_rect_Type0 x1 h1 hterm in hcut __

(** val identifier_map_discr :
    PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a1 identifier_map
    -> __ **)
let identifier_map_discr a1 x y =
  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y

(** val identifier_map_jmdiscr :
    PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a1 identifier_map
    -> __ **)
let identifier_map_jmdiscr a1 x y =
  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y

(** val empty_map : PreIdentifiers.identifierTag -> 'a1 identifier_map **)
let empty_map tag =
  PositiveMap.Pm_leaf

(** val lookup :
    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
    PreIdentifiers.identifier -> 'a1 Types.option **)
let rec lookup tag m l =
  PositiveMap.lookup_opt (let l' = l in l') (let m' = m in m')

(** val lookup_def :
    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
    PreIdentifiers.identifier -> 'a1 -> 'a1 **)
let lookup_def tag m l d =
  match lookup tag m l with
  | Types.None -> d
  | Types.Some x -> x

(** val member :
    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
    PreIdentifiers.identifier -> Bool.bool **)
let member tag m l =
  match lookup tag m l with
  | Types.None -> Bool.False
  | Types.Some x -> Bool.True

(** val lookup_safe :
    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
    PreIdentifiers.identifier -> 'a1 **)
let lookup_safe tag m i =
  (match lookup tag m i with
   | Types.None -> (fun _ -> assert false (* absurd case *))
   | Types.Some x -> (fun _ -> x)) __

(** val add :
    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
    PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map **)
let rec add tag m l a =
  PositiveMap.insert (let l' = l in l') a (let m' = m in m')

(** val elements :
    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
    (PreIdentifiers.identifier, 'a1) Types.prod List.list **)
let elements tag m =
  PositiveMap.fold (fun l a el -> List.Cons ({ Types.fst = l; Types.snd =
    a }, el)) (let m' = m in m') List.Nil

(** val idmap_all :
    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
    (PreIdentifiers.identifier -> 'a1 -> __ -> Bool.bool) -> Bool.bool **)
let idmap_all tag m f =
  PositiveMap.pm_all (let m' = m in m') (fun p a _ -> f p a __)

(** val update :
    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
    PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map Errors.res **)
let update tag m l a =
  match PositiveMap.update (let l' = l in l') a (let m' = m in m') with
  | Types.None ->
    Errors.Error (List.Cons ((Errors.MSG ErrorMessages.MissingId), (List.Cons
      ((Errors.CTX (tag, l)), List.Nil))))
  | Types.Some m' -> Errors.OK m'

(** val remove :
    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
    PreIdentifiers.identifier -> 'a1 identifier_map **)
let remove tag m id =
  PositiveMap.pm_set (let p = id in p) Types.None (let m0 = m in m0)

(** val foldi :
    PreIdentifiers.identifierTag -> (PreIdentifiers.identifier -> 'a1 -> 'a2
    -> 'a2) -> 'a1 identifier_map -> 'a2 -> 'a2 **)
let foldi tag f m b =
  let m' = m in PositiveMap.fold (fun bv -> f bv) m' b

(** val fold_inf :
    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
    (PreIdentifiers.identifier -> 'a1 -> __ -> 'a2 -> 'a2) -> 'a2 -> 'a2 **)
let fold_inf tag m =
  let m' = m in
  (fun f b -> PositiveMap.pm_fold_inf m' (fun bv a _ -> f bv a __) b)

(** val find :
    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
    (PreIdentifiers.identifier -> 'a1 -> Bool.bool) ->
    (PreIdentifiers.identifier, 'a1) Types.prod Types.option **)
let find tag m p =
  let m' = m in
  Types.option_map (fun x -> { Types.fst = x.Types.fst; Types.snd =
    x.Types.snd }) (PositiveMap.pm_find m' (fun id -> p id))

(** val lookup_present :
    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
    PreIdentifiers.identifier -> 'a1 **)
let lookup_present tag m id =
  (match lookup tag m id with
   | Types.None -> (fun _ -> assert false (* absurd case *))
   | Types.Some a -> (fun _ -> a)) __

(** val update_present :
    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
    PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map **)
let update_present tag m l a =
  let l' = let l' = l in l' in
  let m' = let m' = m in m' in
  let u' = PositiveMap.update l' a m' in
  (match u' with
   | Types.None -> (fun _ -> assert false (* absurd case *))
   | Types.Some m'0 -> (fun _ -> m'0)) __

type identifier_set = Types.unit0 identifier_map

(** val empty_set : PreIdentifiers.identifierTag -> identifier_set **)
let empty_set tag =
  empty_map tag

(** val add_set :
    PreIdentifiers.identifierTag -> identifier_set ->
    PreIdentifiers.identifier -> identifier_set **)
let add_set tag s i =
  add tag s i Types.It

(** val singleton_set :
    PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
    identifier_set **)
let singleton_set tag i =
  add_set tag (empty_set tag) i

(** val union_set :
    PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a2 identifier_map
    -> identifier_set **)
let rec union_set tag s s' =
  PositiveMap.merge (fun o o' ->
    match o with
    | Types.None ->
      Obj.magic
        (Monad.m_bind0 (Monad.max_def Option.option) (Obj.magic o') (fun x ->
          Monad.m_return0 (Monad.max_def Option.option) Types.It))
    | Types.Some x -> Types.Some Types.It) (let s0 = s in s0)
    (let s1 = s' in s1)

(** val minus_set :
    PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a2 identifier_map
    -> 'a1 identifier_map **)
let rec minus_set tag s s' =
  PositiveMap.merge (fun o o' ->
    match o' with
    | Types.None -> o
    | Types.Some x -> Types.None) (let s0 = s in s0) (let s1 = s' in s1)

(** val identifierSet : PreIdentifiers.identifierTag -> Setoids.setoid **)
let identifierSet tag =
  Setoids.Mk_Setoid

(** val id_map_size :
    PreIdentifiers.identifierTag -> 'a1 identifier_map -> Nat.nat **)
let id_map_size tag s =
  let p = s in PositiveMap.domain_size p

open Proper

(** val set_from_list :
    PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
    Types.unit0 identifier_map **)
let set_from_list tag =
  Util.foldl (add_set tag) (empty_set tag)

(** val dpi1__o__id_set_from_list__o__inject :
    PreIdentifiers.identifierTag -> (PreIdentifiers.identifier List.list,
    'a1) Types.dPair -> Types.unit0 identifier_map Types.sig0 **)
let dpi1__o__id_set_from_list__o__inject x0 x3 =
  set_from_list x0 x3.Types.dpi1

(** val eject__o__id_set_from_list__o__inject :
    PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list
    Types.sig0 -> Types.unit0 identifier_map Types.sig0 **)
let eject__o__id_set_from_list__o__inject x0 x3 =
  set_from_list x0 (Types.pi1 x3)

(** val id_set_from_list__o__inject :
    PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
    Types.unit0 identifier_map Types.sig0 **)
let id_set_from_list__o__inject x0 x2 =
  set_from_list x0 x2

(** val dpi1__o__id_set_from_list :
    PreIdentifiers.identifierTag -> (PreIdentifiers.identifier List.list,
    'a1) Types.dPair -> Types.unit0 identifier_map **)
let dpi1__o__id_set_from_list x0 x2 =
  set_from_list x0 x2.Types.dpi1

(** val eject__o__id_set_from_list :
    PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list
    Types.sig0 -> Types.unit0 identifier_map **)
let eject__o__id_set_from_list x0 x2 =
  set_from_list x0 (Types.pi1 x2)

(** val choose :
    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
    ((PreIdentifiers.identifier, 'a1) Types.prod, 'a1 identifier_map)
    Types.prod Types.option **)
let choose tag m =
  match PositiveMap.pm_choose (let m' = m in m') with
  | Types.None -> Types.None
  | Types.Some x ->
    Types.Some { Types.fst = { Types.fst = x.Types.fst.Types.fst; Types.snd =
      x.Types.fst.Types.snd }; Types.snd = x.Types.snd }

(** val try_remove :
    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
    PreIdentifiers.identifier -> ('a1, 'a1 identifier_map) Types.prod
    Types.option **)
let try_remove tag m id =
  match PositiveMap.pm_try_remove (let id' = id in id') (let m' = m in m') with
  | Types.None -> Types.None
  | Types.Some x ->
    Types.Some { Types.fst = x.Types.fst; Types.snd = x.Types.snd }

(** val id_set_of_map :
    PreIdentifiers.identifierTag -> 'a1 identifier_map -> identifier_set **)
let id_set_of_map tag m =
  PositiveMap.map (fun x -> Types.It) (let m' = m in m')

(** val set_of_list :
    PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
    identifier_set **)
let set_of_list tag l =
  Util.foldl (fun s id -> add_set tag s id) (empty_set tag) l

(** val domain_of_map :
    PreIdentifiers.identifierTag -> 'a1 identifier_map -> identifier_set **)
let domain_of_map tag m =
  PositiveMap.domain_of_pm (let m0 = m in m0)