open import Pervasives_extra
open import Machine_word
open import Sail_impl_base
open import Sail_values
open import Sail_operators

(* Specialisation of operators to machine words *)

val access_vec_inc : forall 'a. Size 'a => mword 'a -> integer -> bitU
let access_vec_inc = access_bv_inc

val access_vec_dec : forall 'a. Size 'a => mword 'a -> integer -> bitU
let access_vec_dec = access_bv_dec

val update_vec_inc : forall 'a. Size 'a => mword 'a -> integer -> bitU -> mword 'a
let update_vec_inc = update_bv_inc

val update_vec_dec : forall 'a. Size 'a => mword 'a -> integer -> bitU -> mword 'a
let update_vec_dec = update_bv_dec

val subrange_vec_inc : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b
let subrange_vec_inc = subrange_bv_inc

val subrange_vec_dec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b
let subrange_vec_dec = subrange_bv_dec

val update_subrange_vec_inc : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b -> mword 'a
let update_subrange_vec_inc = update_subrange_bv_inc

val update_subrange_vec_dec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b -> mword 'a
let update_subrange_vec_dec = update_subrange_bv_dec

val extz_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b
let extz_vec = extz_bv

val exts_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b
let exts_vec = exts_bv

val concat_vec : forall 'a 'b 'c. Size 'a, Size 'b, Size 'c => mword 'a -> mword 'b -> mword 'c
let concat_vec = concat_bv

val cons_vec : forall 'a 'b 'c. Size 'a, Size 'b => bitU -> mword 'a -> mword 'b
let cons_vec = cons_bv

val bool_of_vec : mword ty1 -> bitU
let bool_of_vec = bool_of_bv

val cast_unit_vec : bitU -> mword ty1
let cast_unit_vec = cast_unit_bv

val vec_of_bit : forall 'a. Size 'a => integer -> bitU -> mword 'a
let vec_of_bit = bv_of_bit

val msb : forall 'a. Size 'a => mword 'a -> bitU
let msb = most_significant

val int_of_vec : forall 'a. Size 'a => bool -> mword 'a -> integer
let int_of_vec = int_of_bv

val and_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
val or_vec  : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
val xor_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
val not_vec : forall 'a. Size 'a => mword 'a -> mword 'a
let and_vec = and_bv
let or_vec  = or_bv
let xor_vec = xor_bv
let not_vec = not_bv

val add_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
val addS_vec  : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
val sub_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
val mult_vec  : forall 'a 'b. Size 'a, Size 'b => mword 'a -> mword 'a -> mword 'b
val multS_vec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> mword 'a -> mword 'b
let add_vec   = add_bv
let addS_vec  = addS_bv
let sub_vec   = sub_bv
let mult_vec  = mult_bv
let multS_vec = multS_bv

val add_vec_int   : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
val addS_vec_int  : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
val sub_vec_int   : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
val mult_vec_int  : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
val multS_vec_int : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
let add_vec_int   = add_bv_int
let addS_vec_int  = addS_bv_int
let sub_vec_int   = sub_bv_int
let mult_vec_int  = mult_bv_int
let multS_vec_int = multS_bv_int

val add_int_vec   : forall 'a. Size 'a => integer -> mword 'a -> mword 'a
val addS_int_vec  : forall 'a. Size 'a => integer -> mword 'a -> mword 'a
val sub_int_vec   : forall 'a. Size 'a => integer -> mword 'a -> mword 'a
val mult_int_vec  : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b
val multS_int_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b
let add_int_vec   = add_int_bv
let addS_int_vec  = addS_int_bv
let sub_int_vec   = sub_int_bv
let mult_int_vec  = mult_int_bv
let multS_int_vec = multS_int_bv

val add_vec_bit  : forall 'a. Size 'a => mword 'a -> bitU -> mword 'a
val addS_vec_bit : forall 'a. Size 'a => mword 'a -> bitU -> mword 'a
val sub_vec_bit  : forall 'a. Size 'a => mword 'a -> bitU -> mword 'a
let add_vec_bit  = add_bv_bit
let addS_vec_bit = addS_bv_bit
let sub_vec_bit  = sub_bv_bit

val add_overflow_vec         : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU)
val add_overflow_vec_signed  : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU)
val sub_overflow_vec         : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU)
val sub_overflow_vec_signed  : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU)
val mult_overflow_vec        : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU)
val mult_overflow_vec_signed : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU)
let add_overflow_vec         = add_overflow_bv
let add_overflow_vec_signed  = add_overflow_bv_signed
let sub_overflow_vec         = sub_overflow_bv
let sub_overflow_vec_signed  = sub_overflow_bv_signed
let mult_overflow_vec        = mult_overflow_bv
let mult_overflow_vec_signed = mult_overflow_bv_signed

val add_overflow_vec_bit         : forall 'a. Size 'a => mword 'a -> bitU -> (mword 'a * bitU * bitU)
val add_overflow_vec_bit_signed  : forall 'a. Size 'a => mword 'a -> bitU -> (mword 'a * bitU * bitU)
val sub_overflow_vec_bit         : forall 'a. Size 'a => mword 'a -> bitU -> (mword 'a * bitU * bitU)
val sub_overflow_vec_bit_signed  : forall 'a. Size 'a => mword 'a -> bitU -> (mword 'a * bitU * bitU)
let add_overflow_vec_bit         = add_overflow_bv_bit
let add_overflow_vec_bit_signed  = add_overflow_bv_bit_signed
let sub_overflow_vec_bit         = sub_overflow_bv_bit
let sub_overflow_vec_bit_signed  = sub_overflow_bv_bit_signed

val shiftl       : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
val shiftr       : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
val arith_shiftr : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
val rotl         : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
val rotr         : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
let shiftl       = shiftl_bv
let shiftr       = shiftr_bv
let arith_shiftr = arith_shiftr_bv
let rotl         = rotl_bv
let rotr         = rotr_bv

val mod_vec         : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
val quot_vec        : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
val quot_vec_signed : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
let mod_vec         = mod_bv
let quot_vec        = quot_bv
let quot_vec_signed = quot_bv_signed

val mod_vec_int  : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
val quot_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
let mod_vec_int  = mod_bv_int
let quot_vec_int = quot_bv_int

val replicate_bits : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
let replicate_bits = replicate_bits_bv

val duplicate : forall 'a. Size 'a => bitU -> integer -> mword 'a
let duplicate = duplicate_bit_bv

val eq_vec    : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
val neq_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
val ult_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
val slt_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
val ugt_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
val sgt_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
val ulteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
val slteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
val ugteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
val sgteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
let eq_vec    = eq_bv
let neq_vec   = neq_bv
let ult_vec   = ult_bv
let slt_vec   = slt_bv
let ugt_vec   = ugt_bv
let sgt_vec   = sgt_bv
let ulteq_vec = ulteq_bv
let slteq_vec = slteq_bv
let ugteq_vec = ugteq_bv
let sgteq_vec = sgteq_bv