4 files changed, 44 insertions, 45 deletions
diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index b94257f0..30c7325e 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -437,11 +437,6 @@ let arith_op_vec_range_no0 op sign size (Vector _ _ is_inc as l) r =
 
 let mod_VIV = arith_op_vec_range_no0 hardware_mod false 1
 
-val repeat : forall 'a. list 'a -> integer -> list 'a
-let rec repeat xs n =
-  if n = 0 then []
-  else xs ++ repeat xs (n-1)
-
 (* Assumes decreasing bit vectors *)
 let duplicate (bit, length) =
   Vector (repeat [bit] length) (length - 1) false
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index a1fc1fd7..8fb158de 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -118,9 +118,9 @@ let bitwise_not bs = lNot bs
 
 let bitwise_binop op (bsl, bsr) = (op bsl bsr)
 
-let bitwise_and = bitwise_binop lAnd
-let bitwise_or = bitwise_binop lOr
-let bitwise_xor = bitwise_binop lXor
+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
@@ -311,9 +311,9 @@ let arith_op_range_vec_range op sign l r = op l (to_num sign r)
  * add_range_vec_range_signed
  * minus_range_vec_range
  *)
-let add_IVI = arith_op_range_vec_range integerAdd false
-let addS_IVI = arith_op_range_vec_range integerAdd true
-let minus_IVI = arith_op_range_vec_range integerMinus false
+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
 
@@ -321,9 +321,9 @@ let arith_op_vec_range_range op sign l r = op (to_num sign l) r
  * add_vec_range_range_signed
  * minus_vec_range_range
  *)
-let add_VII = arith_op_vec_range_range integerAdd false
-let addS_VII = arith_op_vec_range_range integerAdd true
-let minus_VII = arith_op_vec_range_range integerMinus false
+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
 
 
 
@@ -334,8 +334,8 @@ let arith_op_vec_vec_range op sign l r =
 (* add_vec_vec_range
  * add_vec_vec_range_signed
  *)
-let add_VVI = arith_op_vec_vec_range integerAdd false
-let addS_VVI = arith_op_vec_vec_range integerAdd true
+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
@@ -346,9 +346,9 @@ let arith_op_vec_bit op sign (size : integer) l r =
  * add_vec_bit_signed
  * minus_vec_bit_signed
  *)
-let add_VBV = arith_op_vec_bit integerAdd false 1
-let addS_VBV = arith_op_vec_bit integerAdd true 1
-let minus_VBV = arith_op_vec_bit integerMinus true 1
+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
@@ -426,9 +426,9 @@ let shift_op_vec op (bs, (n : integer)) =
      rotateLeft n bs
   end
 
-let bitwise_leftshift = shift_op_vec LL_shift (*"<<"*)
-let bitwise_rightshift = shift_op_vec RR_shift (*">>"*)
-let bitwise_rotate = shift_op_vec LLL_shift (*"<<<"*)
+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
 
@@ -491,6 +491,11 @@ 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 (<)
@@ -502,37 +507,37 @@ 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 = compare_op_vec (<) true
-let gt_vec = compare_op_vec (>) true
-let lteq_vec = compare_op_vec (<=) true
-let gteq_vec = compare_op_vec (>=) true
+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 = compare_op_vec (<) true
-let gt_vec_signed = compare_op_vec (>) true
-let lteq_vec_signed = compare_op_vec (<=) true
-let gteq_vec_signed = compare_op_vec (>=) true
-let lt_vec_unsigned = compare_op_vec (<) false
-let gt_vec_unsigned = compare_op_vec (>) false
-let lteq_vec_unsigned = compare_op_vec (<=) false
-let gteq_vec_unsigned = compare_op_vec (>=) false
+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 = compare_op_vec_range (<) true
-let gt_vec_range = compare_op_vec_range (>) true
-let lteq_vec_range = compare_op_vec_range (<=) true
-let gteq_vec_range = compare_op_vec_range (>=) true
+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 = compare_op_range_vec (<) true
-let gt_range_vec = compare_op_range_vec (>) true
-let lteq_range_vec = compare_op_range_vec (<=) true
-let gteq_range_vec = compare_op_range_vec (>=) true
+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)
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 48d728bf..906b35a8 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -41,7 +41,7 @@ let list_append (l, r) = l ++ r
 
 val repeat : forall 'a. list 'a -> integer -> list 'a
 let rec repeat xs n =
-  if n = 0 then []
+  if n <= 0 then []
   else xs ++ repeat xs (n-1)
 
 let duplicate_to_list (bit, length) = repeat [bit] length
@@ -355,7 +355,6 @@ let vec_to_bvec (Vector elems start is_inc) =
 
 (*** Vector operations *)
 
-
 (* Bytes and addresses *)
 
 val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a)
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index dc30a17f..1b03c81e 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -212,7 +212,7 @@ val barrier : forall 'regs. barrier_kind -> M 'regs unit
 let barrier _ = return ()
 
 val footprint : forall 'regs. M 'regs unit
-let footprint = return ()
+let footprint s = return () s
 
 
 val foreachM_inc : forall 'regs 'vars 'e. (integer * integer * integer) -> 'vars ->