open Preamble

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Bool

open Relations

open Nat

open Positive

open Div_and_mod

open Jmeq

open Russell

open List

open Util

open Setoids

open Monad

open Option

type 'a positive_map =
| Pm_leaf
| Pm_node of 'a Types.option * 'a positive_map * 'a positive_map

(** val positive_map_rect_Type4 :
    'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2
    -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 **)
let rec positive_map_rect_Type4 h_pm_leaf h_pm_node = function
| Pm_leaf -> h_pm_leaf
| Pm_node (x_3300, x_3299, x_3298) ->
  h_pm_node x_3300 x_3299 x_3298
    (positive_map_rect_Type4 h_pm_leaf h_pm_node x_3299)
    (positive_map_rect_Type4 h_pm_leaf h_pm_node x_3298)

(** val positive_map_rect_Type3 :
    'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2
    -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 **)
let rec positive_map_rect_Type3 h_pm_leaf h_pm_node = function
| Pm_leaf -> h_pm_leaf
| Pm_node (x_3312, x_3311, x_3310) ->
  h_pm_node x_3312 x_3311 x_3310
    (positive_map_rect_Type3 h_pm_leaf h_pm_node x_3311)
    (positive_map_rect_Type3 h_pm_leaf h_pm_node x_3310)

(** val positive_map_rect_Type2 :
    'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2
    -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 **)
let rec positive_map_rect_Type2 h_pm_leaf h_pm_node = function
| Pm_leaf -> h_pm_leaf
| Pm_node (x_3318, x_3317, x_3316) ->
  h_pm_node x_3318 x_3317 x_3316
    (positive_map_rect_Type2 h_pm_leaf h_pm_node x_3317)
    (positive_map_rect_Type2 h_pm_leaf h_pm_node x_3316)

(** val positive_map_rect_Type1 :
    'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2
    -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 **)
let rec positive_map_rect_Type1 h_pm_leaf h_pm_node = function
| Pm_leaf -> h_pm_leaf
| Pm_node (x_3324, x_3323, x_3322) ->
  h_pm_node x_3324 x_3323 x_3322
    (positive_map_rect_Type1 h_pm_leaf h_pm_node x_3323)
    (positive_map_rect_Type1 h_pm_leaf h_pm_node x_3322)

(** val positive_map_rect_Type0 :
    'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2
    -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 **)
let rec positive_map_rect_Type0 h_pm_leaf h_pm_node = function
| Pm_leaf -> h_pm_leaf
| Pm_node (x_3330, x_3329, x_3328) ->
  h_pm_node x_3330 x_3329 x_3328
    (positive_map_rect_Type0 h_pm_leaf h_pm_node x_3329)
    (positive_map_rect_Type0 h_pm_leaf h_pm_node x_3328)

(** val positive_map_inv_rect_Type4 :
    'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map
    -> 'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **)
let positive_map_inv_rect_Type4 hterm h1 h2 =
  let hcut = positive_map_rect_Type4 h1 h2 hterm in hcut __

(** val positive_map_inv_rect_Type3 :
    'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map
    -> 'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **)
let positive_map_inv_rect_Type3 hterm h1 h2 =
  let hcut = positive_map_rect_Type3 h1 h2 hterm in hcut __

(** val positive_map_inv_rect_Type2 :
    'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map
    -> 'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **)
let positive_map_inv_rect_Type2 hterm h1 h2 =
  let hcut = positive_map_rect_Type2 h1 h2 hterm in hcut __

(** val positive_map_inv_rect_Type1 :
    'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map
    -> 'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **)
let positive_map_inv_rect_Type1 hterm h1 h2 =
  let hcut = positive_map_rect_Type1 h1 h2 hterm in hcut __

(** val positive_map_inv_rect_Type0 :
    'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map
    -> 'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **)
let positive_map_inv_rect_Type0 hterm h1 h2 =
  let hcut = positive_map_rect_Type0 h1 h2 hterm in hcut __

(** val positive_map_discr : 'a1 positive_map -> 'a1 positive_map -> __ **)
let positive_map_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Pm_leaf -> Obj.magic (fun _ dH -> dH)
     | Pm_node (a0, a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y

(** val positive_map_jmdiscr : 'a1 positive_map -> 'a1 positive_map -> __ **)
let positive_map_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Pm_leaf -> Obj.magic (fun _ dH -> dH)
     | Pm_node (a0, a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y

(** val lookup_opt : Positive.pos -> 'a1 positive_map -> 'a1 Types.option **)
let rec lookup_opt b = function
| Pm_leaf -> Types.None
| Pm_node (a, l, r) ->
  (match b with
   | Positive.One -> a
   | Positive.P1 tl -> lookup_opt tl r
   | Positive.P0 tl -> lookup_opt tl l)

(** val lookup : Positive.pos -> 'a1 positive_map -> 'a1 -> 'a1 **)
let lookup b t x =
  match lookup_opt b t with
  | Types.None -> x
  | Types.Some r -> r

(** val pm_set :
    Positive.pos -> 'a1 Types.option -> 'a1 positive_map -> 'a1 positive_map **)
let rec pm_set b a t =
  match b with
  | Positive.One ->
    (match t with
     | Pm_leaf -> Pm_node (a, Pm_leaf, Pm_leaf)
     | Pm_node (x, l, r) -> Pm_node (a, l, r))
  | Positive.P1 tl ->
    (match t with
     | Pm_leaf -> Pm_node (Types.None, Pm_leaf, (pm_set tl a Pm_leaf))
     | Pm_node (x, l, r) -> Pm_node (x, l, (pm_set tl a r)))
  | Positive.P0 tl ->
    (match t with
     | Pm_leaf -> Pm_node (Types.None, (pm_set tl a Pm_leaf), Pm_leaf)
     | Pm_node (x, l, r) -> Pm_node (x, (pm_set tl a l), r))

(** val insert :
    Positive.pos -> 'a1 -> 'a1 positive_map -> 'a1 positive_map **)
let insert p a =
  pm_set p (Types.Some a)

(** val update :
    Positive.pos -> 'a1 -> 'a1 positive_map -> 'a1 positive_map Types.option **)
let rec update b a t =
  match b with
  | Positive.One ->
    (match t with
     | Pm_leaf -> Types.None
     | Pm_node (x, l, r) ->
       Types.option_map (fun x0 -> Pm_node ((Types.Some a), l, r)) x)
  | Positive.P1 tl ->
    (match t with
     | Pm_leaf -> Types.None
     | Pm_node (x, l, r) ->
       Types.option_map (fun r0 -> Pm_node (x, l, r0)) (update tl a r))
  | Positive.P0 tl ->
    (match t with
     | Pm_leaf -> Types.None
     | Pm_node (x, l, r) ->
       Types.option_map (fun l0 -> Pm_node (x, l0, r)) (update tl a l))

(** val fold :
    (Positive.pos -> 'a1 -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 -> 'a2 **)
let rec fold f t b =
  match t with
  | Pm_leaf -> b
  | Pm_node (a, l, r) ->
    let b0 =
      match a with
      | Types.None -> b
      | Types.Some a0 -> f Positive.One a0 b
    in
    let b1 = fold (fun x -> f (Positive.P0 x)) l b0 in
    fold (fun x -> f (Positive.P1 x)) r b1

(** val domain_of_pm : 'a1 positive_map -> Types.unit0 positive_map **)
let domain_of_pm t =
  fold (fun p a b -> insert p Types.It b) t Pm_leaf

(** val is_none : 'a1 Types.option -> Bool.bool **)
let is_none = function
| Types.None -> Bool.True
| Types.Some x -> Bool.False

(** val is_pm_leaf : 'a1 positive_map -> Bool.bool **)
let is_pm_leaf = function
| Pm_leaf -> Bool.True
| Pm_node (x, x0, x1) -> Bool.False

(** val map_opt :
    ('a1 -> 'a2 Types.option) -> 'a1 positive_map -> 'a2 positive_map **)
let rec map_opt f = function
| Pm_leaf -> Pm_leaf
| Pm_node (a, l, r) ->
  let a' =
    Monad.m_bind0 (Monad.max_def Option.option) (Obj.magic a) (fun x ->
      Obj.magic f x)
  in
  let l' = map_opt f l in
  let r' = map_opt f r in
  (match Bool.andb (Bool.andb (is_none (Obj.magic a')) (is_pm_leaf l'))
           (is_pm_leaf r') with
   | Bool.True -> Pm_leaf
   | Bool.False -> Pm_node ((Obj.magic a'), l', r'))

(** val map : ('a1 -> 'a2) -> 'a1 positive_map -> 'a2 positive_map **)
let map f =
  map_opt (fun x -> Types.Some (f x))

(** val merge :
    ('a1 Types.option -> 'a2 Types.option -> 'a3 Types.option) -> 'a1
    positive_map -> 'a2 positive_map -> 'a3 positive_map **)
let rec merge choice a b =
  match a with
  | Pm_leaf -> map_opt (fun x -> choice Types.None (Types.Some x)) b
  | Pm_node (o, l, r) ->
    (match b with
     | Pm_leaf -> map_opt (fun x -> choice (Types.Some x) Types.None) a
     | Pm_node (o', l', r') ->
       let o'' = choice o o' in
       let l'' = merge choice l l' in
       let r'' = merge choice r r' in
       (match Bool.andb (Bool.andb (is_none o'') (is_pm_leaf l''))
                (is_pm_leaf r'') with
        | Bool.True -> Pm_leaf
        | Bool.False -> Pm_node (o'', l'', r'')))

(** val domain_size : 'a1 positive_map -> Nat.nat **)
let rec domain_size = function
| Pm_leaf -> Nat.O
| Pm_node (a, l, r) ->
  Nat.plus
    (Nat.plus
      (match a with
       | Types.None -> Nat.O
       | Types.Some x -> Nat.S Nat.O) (domain_size l)) (domain_size r)

(** val pm_all_aux :
    'a1 positive_map -> 'a1 positive_map -> (Positive.pos -> Positive.pos) ->
    (Positive.pos -> 'a1 -> __ -> Bool.bool) -> Bool.bool **)
let rec pm_all_aux m t pre x =
  (match t with
   | Pm_leaf -> (fun _ x0 -> Bool.True)
   | Pm_node (a, l, r) ->
     (fun _ f ->
       Bool.andb
         (Bool.andb (pm_all_aux m l (fun x0 -> pre (Positive.P0 x0)) f)
           ((match a with
             | Types.None -> (fun _ -> Bool.True)
             | Types.Some a' -> (fun _ -> f (pre Positive.One) a' __)) __))
         (pm_all_aux m r (fun x0 -> pre (Positive.P1 x0)) f))) __ x

(** val pm_all :
    'a1 positive_map -> (Positive.pos -> 'a1 -> __ -> Bool.bool) -> Bool.bool **)
let pm_all m f =
  pm_all_aux m m (fun x -> x) f

(** val pm_choose :
    'a1 positive_map -> ((Positive.pos, 'a1) Types.prod, 'a1 positive_map)
    Types.prod Types.option **)
let rec pm_choose = function
| Pm_leaf -> Types.None
| Pm_node (a, l, r) ->
  (match pm_choose l with
   | Types.None ->
     (match pm_choose r with
      | Types.None ->
        (match a with
         | Types.None -> Types.None
         | Types.Some a0 ->
           Types.Some { Types.fst = { Types.fst = Positive.One; Types.snd =
             a0 }; Types.snd = Pm_leaf })
      | Types.Some x ->
        Types.Some { Types.fst = { Types.fst = (Positive.P1
          x.Types.fst.Types.fst); Types.snd = x.Types.fst.Types.snd };
          Types.snd = (Pm_node (a, l, x.Types.snd)) })
   | Types.Some x ->
     Types.Some { Types.fst = { Types.fst = (Positive.P0
       x.Types.fst.Types.fst); Types.snd = x.Types.fst.Types.snd };
       Types.snd = (Pm_node (a, x.Types.snd, r)) })

(** val pm_try_remove :
    Positive.pos -> 'a1 positive_map -> ('a1, 'a1 positive_map) Types.prod
    Types.option **)
let rec pm_try_remove b t =
  match b with
  | Positive.One ->
    (match t with
     | Pm_leaf -> Types.None
     | Pm_node (x, l, r) ->
       Types.option_map (fun x0 -> { Types.fst = x0; Types.snd = (Pm_node
         (Types.None, l, r)) }) x)
  | Positive.P1 tl ->
    (match t with
     | Pm_leaf -> Types.None
     | Pm_node (x, l, r) ->
       Types.option_map (fun xr -> { Types.fst = xr.Types.fst; Types.snd =
         (Pm_node (x, l, xr.Types.snd)) }) (pm_try_remove tl r))
  | Positive.P0 tl ->
    (match t with
     | Pm_leaf -> Types.None
     | Pm_node (x, l, r) ->
       Types.option_map (fun xl -> { Types.fst = xl.Types.fst; Types.snd =
         (Pm_node (x, xl.Types.snd, r)) }) (pm_try_remove tl l))

(** val pm_fold_inf_aux :
    'a1 positive_map -> (Positive.pos -> 'a1 -> __ -> 'a2 -> 'a2) -> 'a1
    positive_map -> (Positive.pos -> Positive.pos) -> 'a2 -> 'a2 **)
let rec pm_fold_inf_aux t f t' pre b =
  (match t' with
   | Pm_leaf -> (fun _ -> b)
   | Pm_node (a, l, r) ->
     (fun _ ->
       let b0 =
         (match a with
          | Types.None -> (fun _ -> b)
          | Types.Some a0 -> (fun _ -> f (pre Positive.One) a0 __ b)) __
       in
       let b1 = pm_fold_inf_aux t f l (fun x -> pre (Positive.P0 x)) b0 in
       pm_fold_inf_aux t f r (fun x -> pre (Positive.P1 x)) b1)) __

(** val pm_fold_inf :
    'a1 positive_map -> (Positive.pos -> 'a1 -> __ -> 'a2 -> 'a2) -> 'a2 ->
    'a2 **)
let pm_fold_inf t f b =
  pm_fold_inf_aux t f t (fun x -> x) b

(** val pm_find_aux :
    (Positive.pos -> Positive.pos) -> 'a1 positive_map -> (Positive.pos ->
    'a1 -> Bool.bool) -> (Positive.pos, 'a1) Types.prod Types.option **)
let rec pm_find_aux pre t p =
  match t with
  | Pm_leaf -> Types.None
  | Pm_node (a, l, r) ->
    let x =
      match a with
      | Types.None -> Types.None
      | Types.Some a0 ->
        (match p (pre Positive.One) a0 with
         | Bool.True ->
           Types.Some { Types.fst = (pre Positive.One); Types.snd = a0 }
         | Bool.False -> Types.None)
    in
    (match x with
     | Types.None ->
       (match pm_find_aux (fun x0 -> pre (Positive.P0 x0)) l p with
        | Types.None -> pm_find_aux (fun x0 -> pre (Positive.P1 x0)) r p
        | Types.Some y -> Types.Some y)
     | Types.Some x0 -> Types.Some x0)

(** val pm_find :
    'a1 positive_map -> (Positive.pos -> 'a1 -> Bool.bool) -> (Positive.pos,
    'a1) Types.prod Types.option **)
let pm_find x x0 =
  pm_find_aux (fun x1 -> x1) x x0