Add wrappers around Lem operators using bitvector type class

Makes bitvector typeclass instance dictionaries disappear from generated
Isabelle output.

1 files changed, 173 insertions, 597 deletions

diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index ff25c37b..3762eb7f 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -2,600 +2,176 @@ open import Pervasives_extra
 open import Machine_word
 open import Sail_impl_base
 open import Sail_values
-
-(* Translating between a type level number (itself 'n) and an integer *)
-
-let size_itself_int x = integerFromNat (size_itself x)
-
-(* NB: the corresponding sail type is forall 'n. atom('n) -> itself('n),
-   the actual integer is ignored. *)
-
-val make_the_value : forall 'n. integer -> itself 'n
-let inline make_the_value x = the_value
-
-(*** Bit vector operations *)
-
-let bitvector_length bs = integerFromNat (word_length bs)
-
-(*val set_bitvector_start : forall 'a. (integer * bitvector 'a) -> bitvector 'a
-let set_bitvector_start (new_start, Bitvector bs _ is_inc) =
-  Bitvector bs new_start is_inc
-
-let reset_bitvector_start v =
-  set_bitvector_start (if (bvget_dir v) then 0 else (bvlength v - 1), v)
-
-let set_bitvector_start_to_length v =
-  set_bitvector_start (bvlength v - 1, v)
-
-let bitvector_concat (Bitvector bs start is_inc, Bitvector bs' _ _) =
-  Bitvector (word_concat bs bs') start is_inc*)
-
-let bitvector_concat (bs, bs') = word_concat bs bs'
-
-let inline (^^^) = bitvector_concat
-
-val bvslice : forall 'a 'b. Size 'a => bool -> integer -> bitvector 'a -> integer -> integer -> bitvector 'b
-let bvslice is_inc start bs i j =
-  let iN = natFromInteger i in
-  let jN = natFromInteger j in
-  let startN = natFromInteger start in
-  let top = word_length bs - 1 in
-  let (hi,lo) = if is_inc then (top+startN-iN,top+startN-jN) else (top-startN+iN,top-startN+jN) in
-  word_extract lo hi bs
-
-let bitvector_subrange_inc (start, v, i, j) = bvslice true start v i j
-let bitvector_subrange_dec (start, v, i, j) = bvslice false start v i j
-
-let vector_subrange_bl_dec (start, v, i, j) =
-  let v' = slice (bvec_to_vec false start v) i j in
-  get_elems v'
-
-(* this is for the vector slicing introduced in vector-concat patterns: i and j
-index into the "raw data", the list of bits. Therefore getting the bit list is
-easy, but the start index has to be transformed to match the old vector start
-and the direction. *)
-val bvslice_raw : forall 'a 'b. Size 'b => bitvector 'a -> integer -> integer -> bitvector 'b
-let bvslice_raw bs i j =
-  let iN = natFromInteger i in
-  let jN = natFromInteger j in
-  (*let bits =*) word_extract iN jN bs (*in
-  let len = integerFromNat (word_length bits) in
-  Bitvector bits (if is_inc then 0 else len - 1) is_inc*)
-
-val bvupdate_aux : forall 'a 'b. Size 'a => bool -> integer -> bitvector 'a -> integer -> integer -> list bitU -> bitvector 'a
-let bvupdate_aux is_inc start bs i j bs' =
-  let bits = update_aux is_inc start (List.map to_bitU (bitlistFromWord bs)) i j bs' in
-  wordFromBitlist (List.map of_bitU bits)
-  (*let iN = natFromInteger i in
-  let jN = natFromInteger j in
-  let startN = natFromInteger start in
-  let top = word_length bs - 1 in
-  let (hi,lo) = if is_inc then (top+startN-iN,top+startN-jN) else (top-startN+iN,top-startN+jN) in
-  word_update bs lo hi bs'*)
-
-val bvupdate : forall 'a 'b. Size 'a => bool -> integer -> bitvector 'a -> integer -> integer -> bitvector 'b -> bitvector 'a
-let bvupdate is_inc start bs i j bs' =
-  bvupdate_aux is_inc start bs i j (List.map to_bitU (bitlistFromWord bs'))
-
-val bvaccess : forall 'a. Size 'a => bool -> integer -> bitvector 'a -> integer -> bitU
-let bvaccess is_inc start bs n = bool_to_bitU (
-  let top = integerFromNat (word_length bs) - 1 in
-  if is_inc then getBit bs (natFromInteger (top + start - n))
-  else getBit bs (natFromInteger (top + n - start)))
-
-val bvupdate_pos : forall 'a. Size 'a => bool -> integer -> bitvector 'a -> integer -> bitU -> bitvector 'a
-let bvupdate_pos is_inc start v n b =
-  bvupdate_aux is_inc start v n n [b]
-
-let bitvector_access_inc (start, v, i) = bvaccess true start v i
-let bitvector_access_dec (start, v, i) = bvaccess false start v i
-let bitvector_update_pos_dec (start, v, i, b) = bvupdate_pos false start v i b
-let bitvector_update_subrange_dec (start, v, i, j, v') = bvupdate false start v i j v'
-
-val extract_only_bit : bitvector ty1 -> bitU
-let extract_only_bit elems =
-  let l = word_length elems in
-  if l = 1 then
-    bool_to_bitU (msb elems)
-  else if l = 0 then
-    failwith "extract_single_bit called for empty vector"
-  else
-    failwith "extract_single_bit called for vector with more bits"
-
-
-let norm_dec v = v (*reset_bitvector_start*)
-let adjust_start_index (start, v) = v (*set_bitvector_start (start, v)*)
-
-let cast_vec_bool v = bitU_to_bool (extract_only_bit v)
-let cast_bit_vec_basic (start, len, b) = vec_to_bvec (Vector [b] start false)
-let cast_boolvec_bitvec (Vector bs start inc) =
-  vec_to_bvec (Vector (List.map bool_to_bitU bs) start inc)
-let cast_vec_bl v = List.map bool_to_bitU (bitlistFromWord v)
-let cast_int_vec n = wordFromInteger n
-let cast_bl_vec (start, len, bs) = wordFromBitlist (List.map bitU_to_bool bs)
-let cast_bl_svec (start, len, bs) = cast_int_vec (bitlist_to_signed bs)
-
-let pp_bitu_vector (Vector elems start inc) =
-  let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in
-  "Vector [" ^ elems_pp ^ "] " ^ show start ^ " " ^ show inc
-
-
-let most_significant v =
-  if word_length v = 0 then
-    failwith "most_significant applied to empty vector"
-  else
-    bool_to_bitU (msb v)
-
-let bitwise_not_bitlist = List.map bitwise_not_bit
-
-let bitwise_not bs = lNot bs
-
-let bitwise_binop op (bsl, bsr) = (op bsl bsr)
-
-let bitwise_and x = bitwise_binop lAnd x
-let bitwise_or x = bitwise_binop lOr x
-let bitwise_xor x = bitwise_binop lXor x
-
-(*let unsigned bs : integer = unsignedIntegerFromWord bs*)
-let unsigned_big = unsigned
-
-let signed v : integer = signedIntegerFromWord v
-
-let hardware_mod (a: integer) (b:integer) : integer = 
- if a < 0 && b < 0
- then (abs a) mod (abs b)
- else if (a < 0 && b >= 0) 
- then (a mod b) - b
- else a mod b
-
-(* There are different possible answers for integer divide regarding
-rounding behaviour on negative operands. Positive operands always
-round down so derive the one we want (trucation towards zero) from
-that *)
-let hardware_quot (a:integer) (b:integer) : integer = 
-  let q = (abs a) / (abs b) in
-  if ((a<0) = (b<0)) then
-    q  (* same sign -- result positive *)
-  else
-    ~q (* different sign -- result negative *)
-
-let quot_signed = hardware_quot
-
-
-let signed_big = signed
-
-let to_num sign = if sign then signed else unsigned
-
-let max_64u = (integerPow 2 64) - 1
-let max_64  = (integerPow 2 63) - 1
-let min_64  = 0 - (integerPow 2 63)
-let max_32u = (4294967295 : integer)
-let max_32  = (2147483647 : integer)
-let min_32  = (0 - 2147483648 : integer)
-let max_8   = (127 : integer)
-let min_8   = (0 - 128 : integer)
-let max_5   = (31 : integer)
-let min_5   = (0 - 32 : integer)
-
-let get_max_representable_in sign (n : integer) : integer =
-  if (n = 64) then match sign with | true -> max_64 | false -> max_64u end
-  else if (n=32) then match sign with | true -> max_32 | false -> max_32u end
-  else if (n=8) then max_8
-  else if (n=5) then max_5
-  else match sign with | true -> integerPow 2 ((natFromInteger n) -1)
-                       | false -> integerPow 2 (natFromInteger n)
-       end
-
-let get_min_representable_in _ (n : integer) : integer =
-  if n = 64 then min_64
-  else if n = 32 then min_32
-  else if n = 8 then min_8
-  else if n = 5 then min_5
-  else 0 - (integerPow 2 (natFromInteger n))
-
-val to_bin_aux : natural -> list bitU
-let rec to_bin_aux x =
-  if x = 0 then []
-  else (if x mod 2 = 1 then B1 else B0) :: to_bin_aux (x / 2)
-let to_bin n = List.reverse (to_bin_aux n)
-
-val pad_zero : list bitU -> integer -> list bitU
-let rec pad_zero bits n =
-  if n = 0 then bits else pad_zero (B0 :: bits) (n -1)
-
-
-let rec add_one_bit_ignore_overflow_aux bits = match bits with
-  | [] -> []
-  | B0 :: bits -> B1 :: bits
-  | B1 :: bits -> B0 :: add_one_bit_ignore_overflow_aux bits
-  | BU :: _ -> failwith "add_one_bit_ignore_overflow: undefined bit"
-end
-
-let add_one_bit_ignore_overflow bits =
-  List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits))
-
-val to_norm_vec : forall 'a. Size 'a => integer -> bitvector 'a
-let to_norm_vec (n : integer) = wordFromInteger n
-(*
-  (* Bitvector length is determined by return type *)
-  let bits = wordFromInteger n in
-  let len = integerFromNat (word_length bits) in
-  let start = if is_inc then 0 else len - 1 in
-  (*if integerFromNat (word_length bits) = len then*)
-    Bitvector bits start is_inc
-  (*else
-    failwith "Vector length mismatch in to_vec"*)
-*)
-
-let to_vec_big = to_norm_vec
-
-let to_vec_inc (start, len, n) = to_norm_vec n
-let to_vec_norm_inc (len, n) = to_norm_vec n
-let to_vec_dec (start, len, n) = to_norm_vec n
-let to_vec_norm_dec (len, n) = to_norm_vec n
-
-(* TODO: Think about undefined bit(vector)s *)
-let to_vec_undef is_inc (len : integer) =
-  (* Bitvector *)
-  (failwith "undefined bitvector")
-  (* (if is_inc then 0 else len-1) is_inc *)
-
-let to_vec_inc_undef = to_vec_undef true
-let to_vec_dec_undef = to_vec_undef false
-
-let exts (start, len, vec) = to_norm_vec (signed vec)
-val extz : forall 'a 'b. Size 'a, Size 'b => (integer * integer * bitvector 'a) -> bitvector 'b
-let extz (start, len, vec) = to_norm_vec (unsigned vec)
-
-let exts_big (start, len, vec) = to_vec_big (signed_big vec)
-let extz_big (start, len, vec) = to_vec_big (unsigned_big vec)
-
-let quot = hardware_quot
-let modulo (l,r) = hardware_mod l r
-
-(* TODO: this, and the definitions that use it, currently require Size for
-   to_vec, which I'd rather avoid in favour of library versions; the
-   double-size results for multiplication may be a problem *)
-let arith_op_vec op sign (size : integer) l r =
-  let (l',r') = (to_num sign l, to_num sign r) in
-  let n = op l' r' in
-  to_norm_vec n
-
-
-(* add_vec
- * add_vec_signed
- * minus_vec
- * multiply_vec
- * multiply_vec_signed
- *)
-let add_VVV = arith_op_vec integerAdd false 1
-let addS_VVV = arith_op_vec integerAdd true 1
-let minus_VVV = arith_op_vec integerMinus false 1
-let mult_VVV = arith_op_vec integerMult false 2
-let multS_VVV = arith_op_vec integerMult true 2
-
-let mult_vec (l, r) = mult_VVV l r
-let mult_svec (l, r) = multS_VVV l r
-
-let add_vec (l, r) = add_VVV l r
-let sub_vec (l, r) = minus_VVV l r
-
-val arith_op_vec_range : forall 'a 'b. Size 'a, Size 'b => (integer -> integer -> integer) -> bool -> integer -> bitvector 'a -> integer -> bitvector 'b
-let arith_op_vec_range op sign size l r =
-  arith_op_vec op sign size l ((to_norm_vec r) : bitvector 'a)
-
-(* add_vec_range
- * add_vec_range_signed
- * minus_vec_range
- * mult_vec_range
- * mult_vec_range_signed
- *)
-let add_VIV = arith_op_vec_range integerAdd false 1
-let addS_VIV = arith_op_vec_range integerAdd true 1
-let minus_VIV = arith_op_vec_range integerMinus false 1
-let mult_VIV = arith_op_vec_range integerMult false 2
-let multS_VIV = arith_op_vec_range integerMult true 2
-
-let add_vec_int (l, r) = add_VIV l r
-let sub_vec_int (l, r) = minus_VIV l r
-
-val arith_op_range_vec : forall 'a 'b. Size 'a, Size 'b => (integer -> integer -> integer) -> bool -> integer -> integer -> bitvector 'a -> bitvector 'b
-let arith_op_range_vec op sign size l r =
-  arith_op_vec op sign size ((to_norm_vec l) : bitvector 'a) r
-
-(* add_range_vec
- * add_range_vec_signed
- * minus_range_vec
- * mult_range_vec
- * mult_range_vec_signed
- *)
-let add_IVV = arith_op_range_vec integerAdd false 1
-let addS_IVV = arith_op_range_vec integerAdd true 1
-let minus_IVV = arith_op_range_vec integerMinus false 1
-let mult_IVV = arith_op_range_vec integerMult false 2
-let multS_IVV = arith_op_range_vec integerMult true 2
-
-let arith_op_range_vec_range op sign l r = op l (to_num sign r)
-
-(* add_range_vec_range
- * add_range_vec_range_signed
- * minus_range_vec_range
- *)
-let add_IVI x = arith_op_range_vec_range integerAdd false x
-let addS_IVI x = arith_op_range_vec_range integerAdd true x
-let minus_IVI x = arith_op_range_vec_range integerMinus false x
-
-let arith_op_vec_range_range op sign l r = op (to_num sign l) r
-
-(* add_vec_range_range
- * add_vec_range_range_signed
- * minus_vec_range_range
- *)
-let add_VII x = arith_op_vec_range_range integerAdd false x
-let addS_VII x = arith_op_vec_range_range integerAdd true x
-let minus_VII x = arith_op_vec_range_range integerMinus false x
-
-
-
-let arith_op_vec_vec_range op sign l r =
-  let (l',r') = (to_num sign l,to_num sign r) in
-  op l' r'
-
-(* add_vec_vec_range
- * add_vec_vec_range_signed
- *)
-let add_VVI x = arith_op_vec_vec_range integerAdd false x
-let addS_VVI x = arith_op_vec_vec_range integerAdd true x
-
-let arith_op_vec_bit op sign (size : integer) l r =
-  let l' = to_num sign l in
-  let n = op l' (match r with | B1 -> (1 : integer) | _ -> 0 end) in
-  to_norm_vec n
-
-(* add_vec_bit
- * add_vec_bit_signed
- * minus_vec_bit_signed
- *)
-let add_VBV x = arith_op_vec_bit integerAdd false 1 x
-let addS_VBV x = arith_op_vec_bit integerAdd true 1 x
-let minus_VBV x = arith_op_vec_bit integerMinus true 1 x
-
-(* TODO: these can't be done directly in Lem because of the one_more size calculation
-val arith_op_overflow_vec : forall 'a 'b. Size 'a, Size 'b => (integer -> integer -> integer) -> bool -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b * bitU * bool
-let rec arith_op_overflow_vec op sign size (Bitvector _ _ is_inc as l) r =
-  let len = bvlength l in
-  let act_size = len * size in
-  let (l_sign,r_sign) = (to_num sign l,to_num sign r) in
-  let (l_unsign,r_unsign) = (to_num false l,to_num false r) in
-  let n = op l_sign r_sign in
-  let n_unsign = op l_unsign r_unsign in
-  let correct_size_num = to_vec_ord is_inc (act_size,n) in
-  let one_more_size_u = to_vec_ord is_inc (act_size + 1,n_unsign) in
-  let overflow =
-    if n <= get_max_representable_in sign len &&
-         n >= get_min_representable_in sign len
-    then B0 else B1 in
-  let c_out = most_significant one_more_size_u in
-  (correct_size_num,overflow,c_out)
-
-(* add_overflow_vec
- * add_overflow_vec_signed
- * minus_overflow_vec
- * minus_overflow_vec_signed
- * mult_overflow_vec
- * mult_overflow_vec_signed
- *)
-let addO_VVV = arith_op_overflow_vec integerAdd false 1
-let addSO_VVV = arith_op_overflow_vec integerAdd true 1
-let minusO_VVV = arith_op_overflow_vec integerMinus false 1
-let minusSO_VVV = arith_op_overflow_vec integerMinus true 1
-let multO_VVV = arith_op_overflow_vec integerMult false 2
-let multSO_VVV = arith_op_overflow_vec integerMult true 2
-
-val arith_op_overflow_vec_bit : forall 'a 'b. Size 'a, Size 'b => (integer -> integer -> integer) -> bool -> integer ->
-                                bitvector 'a -> bitU -> bitvector 'b * bitU * bool
-let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (size : integer)
-                                  (Bitvector _ _ is_inc as l) r_bit =
-  let act_size = bvlength l * size in
-  let l' = to_num sign l in
-  let l_u = to_num false l in
-  let (n,nu,changed) = match r_bit with
-    | B1 -> (op l' 1, op l_u 1, true)
-    | B0 -> (l',l_u,false)
-    | BU -> failwith "arith_op_overflow_vec_bit applied to undefined bit"
-    end in
-(*    | _ -> assert false *)
-  let correct_size_num = to_vec_ord is_inc (act_size,n) in
-  let one_larger = to_vec_ord is_inc (act_size + 1,nu) in
-  let overflow =
-    if changed
-    then
-      if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size
-      then B0 else B1
-    else B0 in
-  (correct_size_num,overflow,most_significant one_larger)
-
-(* add_overflow_vec_bit_signed
- * minus_overflow_vec_bit
- * minus_overflow_vec_bit_signed
- *)
-let addSO_VBV = arith_op_overflow_vec_bit integerAdd true 1
-let minusO_VBV = arith_op_overflow_vec_bit integerMinus false 1
-let minusSO_VBV = arith_op_overflow_vec_bit integerMinus true 1
-*)
-type shift = LL_shift | RR_shift | LLL_shift
-
-let shift_op_vec op (bs, (n : integer)) =
-  let n = natFromInteger n in
-  match op with
-  | LL_shift (*"<<"*) ->
-     shiftLeft bs n
-  | RR_shift (*">>"*) ->
-     shiftRight bs n
-  | LLL_shift (*"<<<"*) ->
-     rotateLeft n bs
-  end
-
-let bitwise_leftshift x = shift_op_vec LL_shift x (*"<<"*)
-let bitwise_rightshift x = shift_op_vec RR_shift x (*">>"*)
-let bitwise_rotate x = shift_op_vec LLL_shift x (*"<<<"*)
-
-let shiftl = bitwise_leftshift
-let shiftr = bitwise_rightshift
-
-let rec arith_op_no0 (op : integer -> integer -> integer) l r =
-  if r = 0
-  then Nothing
-  else Just (op l r)
-(* TODO
-let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size ((Bitvector _ start is_inc) as l) r =
-  let act_size = bvlength l * size in
-  let (l',r') = (to_num sign l,to_num sign r) in
-  let n = arith_op_no0 op l' r' in
-  let (representable,n') =
-    match n with
-    | Just n' ->
-      (n' <= get_max_representable_in sign act_size &&
-         n' >= get_min_representable_in sign act_size, n')
-    | _ -> (false,0)
-    end in
-  if representable
-  then to_vec_ord is_inc (act_size,n')
-  else Vector (List.replicate (natFromInteger act_size) BU) start is_inc
-
-let mod_VVV = arith_op_vec_no0 hardware_mod false 1
-let quot_VVV = arith_op_vec_no0 hardware_quot false 1
-let quotS_VVV = arith_op_vec_no0 hardware_quot true 1
-
-let arith_op_overflow_no0_vec op sign size ((Vector _ start is_inc) as l) r =
-  let rep_size = length r * size in
-  let act_size = length l * size in
-  let (l',r') = (to_num sign l,to_num sign r) in
-  let (l_u,r_u) = (to_num false l,to_num false r) in
-  let n = arith_op_no0 op l' r' in
-  let n_u = arith_op_no0 op l_u r_u in
-  let (representable,n',n_u') =
-    match (n, n_u) with
-    | (Just n',Just n_u') ->
-       ((n' <= get_max_representable_in sign rep_size &&
-           n' >= (get_min_representable_in sign rep_size)), n', n_u')
-    | _ -> (true,0,0)
-    end in
-  let (correct_size_num,one_more) =
-    if representable then
-      (to_vec_ord is_inc (act_size,n'),to_vec_ord is_inc (act_size + 1,n_u'))
-    else
-      (Vector (List.replicate (natFromInteger act_size) BU) start is_inc,
-       Vector (List.replicate (natFromInteger (act_size + 1)) BU) start is_inc) in
-  let overflow = if representable then B0 else B1 in
-  (correct_size_num,overflow,most_significant one_more)
-
-let quotO_VVV = arith_op_overflow_no0_vec hardware_quot false 1
-let quotSO_VVV = arith_op_overflow_no0_vec hardware_quot true 1
-
-let arith_op_vec_range_no0 op sign size (Vector _ _ is_inc as l) r =
-  arith_op_vec_no0 op sign size l (to_vec_ord is_inc (length l,r))
-
-let mod_VIV = arith_op_vec_range_no0 hardware_mod false 1
-*)
-
-let duplicate (bit, length) =
-  vec_to_bvec (Vector (repeat [bit] length) (length - 1) false)
-
-(* TODO: replace with better native versions *)
-let replicate_bits (v, count) =
-  let v = bvec_to_vec true 0 v in
-  vec_to_bvec (Vector (repeat (get_elems v) count) ((length v * count) - 1) false)
-
-let compare_op op (l,r) = (op l r)
-
-let lt = compare_op (<)
-let gt = compare_op (>)
-let lteq = compare_op (<=)
-let gteq = compare_op (>=)
-
-let compare_op_vec op sign (l,r) =
-  let (l',r') = (to_num sign l, to_num sign r) in
-  compare_op op (l',r')
-
-let lt_vec x = compare_op_vec (<) true x
-let gt_vec x = compare_op_vec (>) true x
-let lteq_vec x = compare_op_vec (<=) true x
-let gteq_vec x = compare_op_vec (>=) true x
-
-let lt_vec_signed x = compare_op_vec (<) true x
-let gt_vec_signed x = compare_op_vec (>) true x
-let lteq_vec_signed x = compare_op_vec (<=) true x
-let gteq_vec_signed x = compare_op_vec (>=) true x
-let lt_vec_unsigned x = compare_op_vec (<) false x
-let gt_vec_unsigned x = compare_op_vec (>) false x
-let lteq_vec_unsigned x = compare_op_vec (<=) false x
-let gteq_vec_unsigned x = compare_op_vec (>=) false x
-
-let lt_svec = lt_vec_signed
-
-let compare_op_vec_range op sign (l,r) =
-  compare_op op ((to_num sign l),r)
-
-let lt_vec_range x = compare_op_vec_range (<) true x
-let gt_vec_range x = compare_op_vec_range (>) true x
-let lteq_vec_range x = compare_op_vec_range (<=) true x
-let gteq_vec_range x = compare_op_vec_range (>=) true x
-
-let compare_op_range_vec op sign (l,r) =
-  compare_op op (l, (to_num sign r))
-
-let lt_range_vec x = compare_op_range_vec (<) true x
-let gt_range_vec x = compare_op_range_vec (>) true x
-let lteq_range_vec x = compare_op_range_vec (<=) true x
-let gteq_range_vec x = compare_op_range_vec (>=) true x
-
-val eq : forall 'a. Eq 'a => 'a * 'a -> bool
-let eq (l,r) = (l = r)
-let eq_range (l,r) = (l = r)
-
-val eq_vec : forall 'a. Size 'a => bitvector 'a * bitvector 'a -> bool
-let eq_vec (l,r) = eq (to_num false l, to_num false r)
-let eq_bit (l,r) = eq (l, r)
-let eq_vec_range (l,r) = eq (to_num false l,r)
-let eq_range_vec (l,r) = eq (l, to_num false r)
-(*let eq_vec_vec (l,r) = eq (to_num true l, to_num true r)*)
-
-let neq (l,r) = not (eq (l,r))
-let neq_bit (l,r) = not (eq_bit (l,r))
-let neq_range (l,r) = not (eq_range (l,r))
-let neq_vec (l,r) = not (eq_vec (l,r))
-(*let neq_vec_vec (l,r) = not (eq_vec_vec (l,r))*)
-let neq_vec_range (l,r) = not (eq_vec_range (l,r))
-let neq_range_vec (l,r) = not (eq_range_vec (l,r))
-
-
-val make_indexed_vector : forall 'a. list (integer * 'a) -> 'a -> integer -> integer -> bool -> vector 'a
-let make_indexed_vector entries default start length dir =
-  let length = natFromInteger length in
-  Vector (List.foldl replace (replicate length default) entries) start dir
-
-(*
-val make_bit_vector_undef : integer -> vector bitU
-let make_bitvector_undef length =
-  Vector (replicate (natFromInteger length) BU) 0 true
- *)
-
-(* let bitwise_not_range_bit n = bitwise_not (to_vec_ord defaultDir n) *)
-
-(* TODO *)
-val mask : forall 'a 'b. Size 'b => (integer * integer * bitvector 'a) -> bitvector 'b
-let mask (start, _, w) = (zeroExtend w)
-
-(* Register operations *)
-
-(*let update_reg_range reg i j reg_val new_val = bvupdate (reg.reg_is_inc) (reg.reg_start) reg_val i j new_val
-let update_reg_pos reg i reg_val bit = bvupdate_pos (reg.reg_is_inc) (reg.reg_start) reg_val i bit
-let update_reg_field_range regfield i j reg_val new_val =
-  let current_field_value = regfield.get_field reg_val in
-  let new_field_value = bvupdate (regfield.field_is_inc) (regfield.field_start) current_field_value i j new_val in
-  regfield.set_field reg_val new_field_value
-(*let write_reg_field_pos regfield i reg_val bit =
-  let current_field_value = regfield.get_field reg_val in
-  let new_field_value = bvupdate_pos (regfield.field_is_inc) (regfield.field_start) current_field_value i bit in
-  regfield.set_field reg_val new_field_value*)*)
+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 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 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