open Preamble

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open List

open Div_and_mod

open Jmeq

open Russell

open Util

open Setoids

open Monad

open Option

open Extranat

type 'a vector =
| VEmpty
| VCons of Nat.nat * 'a * 'a vector

(** val vector_rect_Type4 :
    'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
    vector -> 'a2 **)
let rec vector_rect_Type4 h_VEmpty h_VCons x_1293 = function
| VEmpty -> h_VEmpty
| VCons (n, x_1296, x_1295) ->
  h_VCons n x_1296 x_1295 (vector_rect_Type4 h_VEmpty h_VCons n x_1295)

(** val vector_rect_Type3 :
    'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
    vector -> 'a2 **)
let rec vector_rect_Type3 h_VEmpty h_VCons x_1305 = function
| VEmpty -> h_VEmpty
| VCons (n, x_1308, x_1307) ->
  h_VCons n x_1308 x_1307 (vector_rect_Type3 h_VEmpty h_VCons n x_1307)

(** val vector_rect_Type2 :
    'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
    vector -> 'a2 **)
let rec vector_rect_Type2 h_VEmpty h_VCons x_1311 = function
| VEmpty -> h_VEmpty
| VCons (n, x_1314, x_1313) ->
  h_VCons n x_1314 x_1313 (vector_rect_Type2 h_VEmpty h_VCons n x_1313)

(** val vector_rect_Type1 :
    'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
    vector -> 'a2 **)
let rec vector_rect_Type1 h_VEmpty h_VCons x_1317 = function
| VEmpty -> h_VEmpty
| VCons (n, x_1320, x_1319) ->
  h_VCons n x_1320 x_1319 (vector_rect_Type1 h_VEmpty h_VCons n x_1319)

(** val vector_rect_Type0 :
    'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
    vector -> 'a2 **)
let rec vector_rect_Type0 h_VEmpty h_VCons x_1323 = function
| VEmpty -> h_VEmpty
| VCons (n, x_1326, x_1325) ->
  h_VCons n x_1326 x_1325 (vector_rect_Type0 h_VEmpty h_VCons n x_1325)

(** val vector_inv_rect_Type4 :
    Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1
    vector -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2 **)
let vector_inv_rect_Type4 x2 hterm h1 h2 =
  let hcut = vector_rect_Type4 h1 h2 x2 hterm in hcut __ __

(** val vector_inv_rect_Type3 :
    Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1
    vector -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2 **)
let vector_inv_rect_Type3 x2 hterm h1 h2 =
  let hcut = vector_rect_Type3 h1 h2 x2 hterm in hcut __ __

(** val vector_inv_rect_Type2 :
    Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1
    vector -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2 **)
let vector_inv_rect_Type2 x2 hterm h1 h2 =
  let hcut = vector_rect_Type2 h1 h2 x2 hterm in hcut __ __

(** val vector_inv_rect_Type1 :
    Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1
    vector -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2 **)
let vector_inv_rect_Type1 x2 hterm h1 h2 =
  let hcut = vector_rect_Type1 h1 h2 x2 hterm in hcut __ __

(** val vector_inv_rect_Type0 :
    Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1
    vector -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2 **)
let vector_inv_rect_Type0 x2 hterm h1 h2 =
  let hcut = vector_rect_Type0 h1 h2 x2 hterm in hcut __ __

(** val vector_discr : Nat.nat -> 'a1 vector -> 'a1 vector -> __ **)
let vector_discr a2 x y =
  Logic.eq_rect_Type2 x
    (match x with
     | VEmpty -> Obj.magic (fun _ dH -> dH)
     | VCons (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)) y

(** val vector_jmdiscr : Nat.nat -> 'a1 vector -> 'a1 vector -> __ **)
let vector_jmdiscr a2 x y =
  Logic.eq_rect_Type2 x
    (match x with
     | VEmpty -> Obj.magic (fun _ dH -> dH)
     | VCons (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)) y

(** val get_index_v : Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 **)
let rec get_index_v n v m =
  (match m with
   | Nat.O ->
     (match v with
      | VEmpty -> (fun _ -> assert false (* absurd case *))
      | VCons (p, hd, tl) -> (fun _ -> hd))
   | Nat.S o ->
     (match v with
      | VEmpty -> (fun _ -> assert false (* absurd case *))
      | VCons (p, hd, tl) -> (fun _ -> get_index_v p tl o))) __

(** val get_index' : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 **)
let get_index' n m b =
  get_index_v (Nat.S (Nat.plus n m)) b n

(** val get_index_weak_v :
    Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 Types.option **)
let rec get_index_weak_v n v = function
| Nat.O ->
  (match v with
   | VEmpty -> Types.None
   | VCons (p, hd, tl) -> Types.Some hd)
| Nat.S o ->
  (match v with
   | VEmpty -> Types.None
   | VCons (p, hd, tl) -> get_index_weak_v p tl o)

(** val set_index : Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 -> 'a1 vector **)
let rec set_index n v m a =
  (match m with
   | Nat.O ->
     (match v with
      | VEmpty -> (fun _ -> VEmpty)
      | VCons (p, hd, tl) -> (fun _ -> VCons (p, a, tl)))
   | Nat.S o ->
     (match v with
      | VEmpty -> (fun _ -> VEmpty)
      | VCons (p, hd, tl) -> (fun _ -> VCons (p, hd, (set_index p tl o a)))))
    __

(** val set_index_weak :
    Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 -> 'a1 vector Types.option **)
let rec set_index_weak n v m a =
  match m with
  | Nat.O ->
    (match v with
     | VEmpty -> Types.None
     | VCons (o, hd, tl) -> Types.Some v)
  | Nat.S o ->
    (match v with
     | VEmpty -> Types.None
     | VCons (p, hd, tl) ->
       let settail = set_index_weak p tl o a in
       (match settail with
        | Types.None -> Types.None
        | Types.Some j -> Types.Some v))

(** val drop :
    Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 vector Types.option **)
let rec drop n v = function
| Nat.O -> Types.Some v
| Nat.S o ->
  (match v with
   | VEmpty -> Types.None
   | VCons (p, hd, tl) -> Types.None)

(** val head' : Nat.nat -> 'a1 vector -> 'a1 **)
let head' n = function
| VEmpty -> Obj.magic __
| VCons (x, hd, x0) -> hd

(** val tail : Nat.nat -> 'a1 vector -> 'a1 vector **)
let tail n = function
| VEmpty -> Obj.magic __
| VCons (m, hd, tl) -> tl

(** val vsplit' :
    Nat.nat -> Nat.nat -> 'a1 vector -> ('a1 vector, 'a1 vector) Types.prod **)
let rec vsplit' m n =
  match m with
  | Nat.O -> (fun v -> { Types.fst = VEmpty; Types.snd = v })
  | Nat.S m' ->
    (fun v ->
      let { Types.fst = l; Types.snd = r } =
        vsplit' m' n (tail (Nat.plus m' n) v)
      in
      { Types.fst = (VCons (m', (head' (Nat.plus m' n) v), l)); Types.snd =
      r })

(** val vsplit :
    Nat.nat -> Nat.nat -> 'a1 vector -> ('a1 vector, 'a1 vector) Types.prod **)
let rec vsplit m n v =
  vsplit' m n v

(** val head : Nat.nat -> 'a1 vector -> ('a1, 'a1 vector) Types.prod **)
let head n v =
  (match v with
   | VEmpty -> (fun _ -> assert false (* absurd case *))
   | VCons (o, he, tl) -> (fun _ -> { Types.fst = he; Types.snd = tl })) __

(** val from_singl : 'a1 vector -> 'a1 **)
let from_singl v =
  (head Nat.O v).Types.fst

(** val fold_right :
    Nat.nat -> ('a1 -> 'a2 -> 'a2) -> 'a2 -> 'a1 vector -> 'a2 **)
let rec fold_right n f x = function
| VEmpty -> x
| VCons (n0, hd, tl) -> f hd (fold_right n0 f x tl)

(** val fold_right_i :
    Nat.nat -> (Nat.nat -> 'a1 -> 'a2 -> 'a2) -> 'a2 -> 'a1 vector -> 'a2 **)
let rec fold_right_i n f x = function
| VEmpty -> x
| VCons (n0, hd, tl) -> f n0 hd (fold_right_i n0 f x tl)

(** val fold_right2_i :
    (Nat.nat -> 'a1 -> 'a2 -> 'a3 -> 'a3) -> 'a3 -> Nat.nat -> 'a1 vector ->
    'a2 vector -> 'a3 **)
let rec fold_right2_i f c n v q =
  (match v with
   | VEmpty ->
     (match q with
      | VEmpty -> (fun _ -> c)
      | VCons (o, hd, tl) -> (fun _ -> assert false (* absurd case *)))
   | VCons (o, hd, tl) ->
     (match q with
      | VEmpty -> (fun _ -> assert false (* absurd case *))
      | VCons (p, hd', tl') ->
        (fun _ -> f o hd hd' (fold_right2_i f c o tl tl')))) __

(** val fold_left :
    Nat.nat -> ('a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 vector -> 'a1 **)
let rec fold_left n f x = function
| VEmpty -> x
| VCons (n0, hd, tl) -> fold_left n0 f (f x hd) tl

(** val map : Nat.nat -> ('a1 -> 'a2) -> 'a1 vector -> 'a2 vector **)
let rec map n f = function
| VEmpty -> VEmpty
| VCons (n0, hd, tl) -> VCons (n0, (f hd), (map n0 f tl))

(** val zip_with :
    Nat.nat -> ('a1 -> 'a2 -> 'a3) -> 'a1 vector -> 'a2 vector -> 'a3 vector **)
let rec zip_with n f v q =
  (match v with
   | VEmpty -> (fun _ -> VEmpty)
   | VCons (n0, hd, tl) ->
     (match q with
      | VEmpty -> (fun _ -> Obj.magic Nat.nat_discr (Nat.S n0) Nat.O __)
      | VCons (m, hd', tl') ->
        (fun _ -> VCons (n0, (f hd hd'),
          (zip_with n0 f tl (Util.eq_rect_Type0_r m tl' n0)))))) __

(** val zip :
    Nat.nat -> 'a1 vector -> 'a2 vector -> ('a1, 'a2) Types.prod vector **)
let zip n v q =
  zip_with n (fun x x0 -> { Types.fst = x; Types.snd = x0 }) v q

(** val replicate : Nat.nat -> 'a1 -> 'a1 vector **)
let rec replicate n h =
  match n with
  | Nat.O -> VEmpty
  | Nat.S m -> VCons (m, h, (replicate m h))

(** val append :
    Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector -> 'a1 vector **)
let rec append n m v q =
  match v with
  | VEmpty -> q
  | VCons (o, hd, tl) -> VCons ((Nat.plus o m), hd, (append o m tl q))

(** val scan_left :
    Nat.nat -> ('a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 vector -> 'a1 vector **)
let rec scan_left n f a v =
  VCons (n, a,
    (match v with
     | VEmpty -> VEmpty
     | VCons (o, hd, tl) -> scan_left o f (f a hd) tl))

(** val scan_right :
    Nat.nat -> ('a1 -> 'a2 -> 'a1) -> 'a2 -> 'a1 vector -> 'a1 List.list **)
let rec scan_right n f b = function
| VEmpty -> List.Nil
| VCons (o, hd, tl) -> List.Cons ((f hd b), (scan_right o f b tl))

(** val revapp :
    Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector -> 'a1 vector **)
let rec revapp n m v acc =
  match v with
  | VEmpty -> acc
  | VCons (o, hd, tl) -> revapp o (Nat.S m) tl (VCons (m, hd, acc))

(** val reverse : Nat.nat -> 'a1 vector -> 'a1 vector **)
let rec reverse n v =
  revapp n Nat.O v VEmpty

(** val pad_vector :
    'a1 -> Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector **)
let rec pad_vector a n m v =
  match n with
  | Nat.O -> v
  | Nat.S n' -> VCons ((Nat.plus n' m), a, (pad_vector a n' m v))

(** val list_of_vector : Nat.nat -> 'a1 vector -> 'a1 List.list **)
let rec list_of_vector n = function
| VEmpty -> List.Nil
| VCons (o, hd, tl) -> List.Cons (hd, (list_of_vector o tl))

(** val vector_of_list : 'a1 List.list -> 'a1 vector **)
let rec vector_of_list = function
| List.Nil -> VEmpty
| List.Cons (hd, tl) -> VCons ((List.length tl), hd, (vector_of_list tl))

(** val rotate_left : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector **)
let rec rotate_left n m v =
  match m with
  | Nat.O -> v
  | Nat.S o ->
    (match v with
     | VEmpty -> VEmpty
     | VCons (p, hd, tl) ->
       rotate_left (Nat.S p) o
         (append p (Nat.S Nat.O) tl (VCons (Nat.O, hd, VEmpty))))

(** val rotate_right : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector **)
let rotate_right n m v =
  reverse n (rotate_left n m (reverse n v))

(** val shift_left_1 : Nat.nat -> 'a1 vector -> 'a1 -> 'a1 vector **)
let shift_left_1 n v a =
  (match v with
   | VEmpty -> (fun _ -> assert false (* absurd case *))
   | VCons (o, hd, tl) ->
     (fun _ -> reverse (Nat.S o) (VCons (o, a, (reverse o tl))))) __

(** val switch_bv_plus : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector **)
let switch_bv_plus n m i =
  i

(** val shift_right_1 : Nat.nat -> 'a1 vector -> 'a1 -> 'a1 vector **)
let shift_right_1 n v a =
  let { Types.fst = v'; Types.snd = dropped } =
    vsplit n (Nat.S Nat.O) (switch_bv_plus (Nat.S Nat.O) n v)
  in
  VCons (n, a, v')

(** val shift_left :
    Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 -> 'a1 vector **)
let shift_left n m =
  match Extranat.nat_compare n m with
  | Extranat.Nat_lt (x, x0) -> (fun v a -> replicate x a)
  | Extranat.Nat_eq x -> (fun v a -> replicate x a)
  | Extranat.Nat_gt (d, m0) ->
    (fun v a ->
      let { Types.fst = v0; Types.snd = v' } = vsplit m0 (Nat.S d) v in
      switch_bv_plus (Nat.S d) m0 (append (Nat.S d) m0 v' (replicate m0 a)))

(** val shift_right :
    Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 -> 'a1 vector **)
let shift_right n m v a =
  Util.iterate (fun x -> shift_right_1 n x a) v m

(** val eq_v :
    Nat.nat -> ('a1 -> 'a1 -> Bool.bool) -> 'a1 vector -> 'a1 vector ->
    Bool.bool **)
let rec eq_v n f b c =
  (match b with
   | VEmpty ->
     (fun c0 ->
       match c0 with
       | VEmpty -> Bool.True
       | VCons (x, x0, x1) -> Obj.magic __ x x0 x1)
   | VCons (m, hd, tl) ->
     (fun c0 -> Bool.andb (f hd (head' m c0)) (eq_v m f tl (tail m c0)))) c

(** val vector_inv_n : Nat.nat -> 'a1 vector -> __ **)
let vector_inv_n n v =
  (match v with
   | VEmpty -> (fun _ -> Obj.magic (fun auto -> auto))
   | VCons (n0, auto, auto') ->
     (fun _ -> Obj.magic (fun auto'' -> auto'' auto auto'))) __

(** val eq_v_elim :
    ('a2 -> 'a2 -> Bool.bool) -> (__ -> 'a2 -> 'a2 -> (__ -> __) -> (__ ->
    __) -> __) -> Nat.nat -> 'a2 vector -> 'a2 vector -> (__ -> 'a1) -> (__
    -> 'a1) -> 'a1 **)
let eq_v_elim f f_elim n x =
  vector_rect_Type0 (fun y ->
    Obj.magic vector_inv_n Nat.O y (fun auto auto' -> auto __))
    (fun m h t iH y ->
    Obj.magic vector_inv_n (Nat.S m) y (fun h' t' ht hf ->
      Obj.magic f_elim __ h h' (fun _ ->
        iH (tail m (VCons (m, h', t'))) (fun _ -> ht __) (fun _ -> hf __))
        (fun _ -> hf __))) n x

(** val mem :
    ('a1 -> 'a1 -> Bool.bool) -> Nat.nat -> 'a1 vector -> 'a1 -> Bool.bool **)
let mem eq_a n l x =
  fold_right n (fun y v -> Bool.orb (eq_a x y) v) Bool.False l

(** val subvector_with :
    Nat.nat -> Nat.nat -> ('a1 -> 'a1 -> Bool.bool) -> 'a1 vector -> 'a1
    vector -> Bool.bool **)
let rec subvector_with n m eq sub sup =
  match sub with
  | VEmpty -> Bool.True
  | VCons (n', hd, tl) ->
    (match mem eq m sup hd with
     | Bool.True -> subvector_with n' m eq tl sup
     | Bool.False -> Bool.False)

(** val vprefix :
    Nat.nat -> Nat.nat -> ('a1 -> 'a1 -> Bool.bool) -> 'a1 vector -> 'a1
    vector -> Bool.bool **)
let rec vprefix n m test v1 v2 =
  match v1 with
  | VEmpty -> Bool.True
  | VCons (n', hd1, tl1) ->
    (match v2 with
     | VEmpty -> Bool.False
     | VCons (m', hd2, tl2) ->
       Bool.andb (test hd1 hd2) (vprefix n' m' test tl1 tl2))

(** val vsuffix :
    Nat.nat -> Nat.nat -> ('a1 -> 'a1 -> Bool.bool) -> 'a1 vector -> 'a1
    vector -> Bool.bool **)
let rec vsuffix n m test v1 v2 =
  Util.if_then_else_safe (Nat.leb (Nat.S n) m) (fun _ ->
    (match v2 with
     | VEmpty -> (fun _ -> assert false (* absurd case *))
     | VCons (m', hd2, tl2) -> (fun _ -> vsuffix n m' test v1 tl2)) __)
    (fun _ ->
    match Nat.eqb n m with
    | Bool.True -> vprefix n m test v1 v2
    | Bool.False -> Bool.False)

(** val rvsplit : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector vector **)
let rec rvsplit n m =
  match n with
  | Nat.O -> (fun x -> VEmpty)
  | Nat.S k ->
    (fun v ->
      let { Types.fst = pre; Types.snd = post } = vsplit m (Nat.times k m) v
      in
      VCons (k, pre, (rvsplit k m post)))

(** val vflatten : Nat.nat -> Nat.nat -> 'a1 vector vector -> 'a1 vector **)
let rec vflatten n m = function
| VEmpty -> VEmpty
| VCons (n', hd, tl) -> append m (Nat.times n' m) hd (vflatten n' m tl)