open Preamble

open Types

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Positive

open Z

open Setoids

open Monad

open Option

open Extranat

open Vector

open Div_and_mod

open Jmeq

open Russell

open List

open Util

open FoldStuff

open BitVector

open Exp

open Arithmetic

open Division

(** val z_of_unsigned_bitvector : Nat.nat -> BitVector.bitVector -> Z.z **)
let rec z_of_unsigned_bitvector n = function
| Vector.VEmpty -> Z.OZ
| Vector.VCons (n', h, t) ->
  (match h with
   | Bool.True ->
     Z.Pos
       (Vector.fold_left n' (fun acc b ->
         match b with
         | Bool.True -> Positive.P1 acc
         | Bool.False -> Positive.P0 acc) Positive.One t)
   | Bool.False -> z_of_unsigned_bitvector n' t)

(** val z_of_signed_bitvector : Nat.nat -> BitVector.bitVector -> Z.z **)
let z_of_signed_bitvector n = function
| Vector.VEmpty -> Z.OZ
| Vector.VCons (n', h, t) ->
  (match h with
   | Bool.True ->
     Z.zopp
       (Z.zsucc (z_of_unsigned_bitvector n' (BitVector.negation_bv n' t)))
   | Bool.False -> z_of_unsigned_bitvector n' t)

(** val bits_of_pos : Positive.pos -> Bool.bool List.list **)
let rec bits_of_pos = function
| Positive.One -> List.Cons (Bool.True, List.Nil)
| Positive.P1 p' -> List.Cons (Bool.True, (bits_of_pos p'))
| Positive.P0 p' -> List.Cons (Bool.False, (bits_of_pos p'))

(** val zeroext_reversed :
    Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
let rec zeroext_reversed n m bv =
  match m with
  | Nat.O -> Vector.VEmpty
  | Nat.S m' ->
    (match bv with
     | Vector.VEmpty -> BitVector.zero (Nat.S m')
     | Vector.VCons (n', h, t) ->
       Vector.VCons (m', h, (zeroext_reversed n' m' t)))

(** val bitvector_of_Z : Nat.nat -> Z.z -> BitVector.bitVector **)
let rec bitvector_of_Z n = function
| Z.OZ -> BitVector.zero n
| Z.Pos p ->
  let bits = bits_of_pos p in
  Vector.reverse n
    (zeroext_reversed (List.length bits) n (Vector.vector_of_list bits))
| Z.Neg p ->
  (match p with
   | Positive.One -> BitVector.maximum n
   | Positive.P1 x ->
     let bits = bits_of_pos (Positive.pred p) in
     let pz =
       Vector.reverse n
         (zeroext_reversed (List.length bits) n (Vector.vector_of_list bits))
     in
     BitVector.negation_bv n pz
   | Positive.P0 x ->
     let bits = bits_of_pos (Positive.pred p) in
     let pz =
       Vector.reverse n
         (zeroext_reversed (List.length bits) n (Vector.vector_of_list bits))
     in
     BitVector.negation_bv n pz)

(** val pos_length : Positive.pos -> Nat.nat **)
let rec pos_length = function
| Positive.One -> Nat.O
| Positive.P1 q -> Nat.S (pos_length q)
| Positive.P0 q -> Nat.S (pos_length q)