3 files changed, 33 insertions, 28 deletions
diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index 32d06caf..30c7325e 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -5,7 +5,7 @@ open import Sail_values
 
 (*** Bit vector operations *)
 
-let bvlength = length
+let bitvector_length = length
 
 let set_bitvector_start = set_vector_start
 let reset_bitvector_start = reset_vector_start
@@ -25,8 +25,10 @@ let vector_subrange_bl_dec = vector_subrange_bl
 
 let bitvector_access_inc = vector_access_inc
 let bitvector_access_dec = vector_access_dec
-let bitvector_update_pos_dec = update_pos
-let bitvector_update_subrange_dec = vector_update_dec
+let bitvector_update_pos_inc = vector_update_pos_inc
+let bitvector_update_pos_dec = vector_update_pos_dec
+let bitvector_update_subrange_inc = vector_update_subrange_inc
+let bitvector_update_subrange_dec = vector_update_subrange_dec
 
 let extract_only_bit = extract_only_element
 
@@ -197,18 +199,8 @@ let extz_bl (start, len, bits) = Vector bits start false
 let exts_bl (start, len, bits) = Vector bits start false
 
 
-let add (l,r) = integerAdd l r
-let add_signed (l,r) = integerAdd l r
-let sub (l,r) = integerMinus l r
-let mult (l,r) = integerMult l r
-let quotient (l,r) = integerDiv l r
-let modulo (l,r) = hardware_mod l r
 let quot = hardware_quot
-let power (l,r) = integerPow l r
-
-let add_int = add
-let sub_int = sub
-let mult_int = mult
+let modulo (l,r) = hardware_mod l r
 
 let arith_op_vec op sign (size : integer) (Vector _ _ is_inc as l) r =
   let (l',r') = (to_num sign l, to_num sign r) in
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index e0e66c3e..8fb158de 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -5,7 +5,7 @@ open import Sail_values
 
 (*** Bit vector operations *)
 
-let bvlength bs = integerFromNat (word_length bs)
+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) =
@@ -240,18 +240,8 @@ let extz_big (start, len, vec) = to_vec_big (unsigned_big vec)
 let extz_bl (start, len, bits) = vec_to_bvec (Vector bits (integerFromNat (List.length bits - 1)) false)
 let exts_bl (start, len, bits) = vec_to_bvec (Vector bits (integerFromNat (List.length bits - 1)) false)
 
-let add (l,r) = integerAdd l r
-let add_signed (l,r) = integerAdd l r
-let sub (l,r) = integerMinus l r
-let mult (l,r) = integerMult l r
-let quotient (l,r) = integerDiv l r
-let modulo (l,r) = hardware_mod l r
 let quot = hardware_quot
-let power (l,r) = integerPow l r
-
-let add_int = add
-let sub_int = sub
-let mult_int = mult
+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
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index b0de85e0..906b35a8 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -13,6 +13,26 @@ let pow m n = m ** (natFromInteger n)
 
 let pow2 n = pow 2 n
 
+let add_int (l,r) = integerAdd l r
+let add_signed (l,r) = integerAdd l r
+let sub_int (l,r) = integerMinus l r
+let mult_int (l,r) = integerMult l r
+let quotient_int (l,r) = integerDiv l r
+let quotient_nat (l,r) = natDiv l r
+let power_int_nat (l,r) = integerPow l r
+let power_int_int (l, r) = integerPow l (natFromInteger r)
+let negate_int i = integerNegate i
+let min_int (l, r) = integerMin l r
+let max_int (l, r) = integerMax l r
+
+let add_real (l, r) = realAdd l r
+let sub_real (l, r) = realMinus l r
+let mult_real (l, r) = realMult l r
+let div_real (l, r) = realDiv l r
+let negate_real r = realNegate r
+let abs_real r = realAbs r
+let power_real (b, e) = realPowInteger b e
+
 let bool_or (l, r) = (l || r)
 let bool_and (l, r) = (l && r)
 let bool_xor (l, r) = xor l r
@@ -226,8 +246,8 @@ val update : forall 'a. vector 'a -> integer -> integer -> vector 'a -> vector '
 let update (Vector bs start is_inc) i j (Vector bs' _ _) =
   Vector (update_aux is_inc start bs i j bs') start is_inc
 
-let vector_update_inc (start, v, i, j, v') = update v i j v'
-let vector_update_dec (start, v, i, j, v') = update v i j v'
+let vector_update_subrange_inc (start, v, i, j, v') = update v i j v'
+let vector_update_subrange_dec (start, v, i, j, v') = update v i j v'
 
 val access_aux : forall 'a. bool -> integer -> list 'a -> integer -> 'a
 let access_aux is_inc start xs n =
@@ -244,6 +264,9 @@ val update_pos : forall 'a. vector 'a -> integer -> 'a -> vector 'a
 let update_pos v n b =
   update v n n (Vector [b] 0 false)
 
+let vector_update_pos_inc (start, v, i, x) = update_pos v i x
+let vector_update_pos_dec (start, v, i, x) = update_pos v i x
+
 let extract_only_element (Vector elems _ _) = match elems with
   | [] -> failwith "extract_only_element called for empty vector"
   | [e] -> e