Merge remote-tracking branch 'origin/experiments' into interactive

1 files changed, 3 insertions, 4 deletions

diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index 826ea98f..83746c0b 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -40,6 +40,9 @@ let cast_bit_vec_basic (start, len, b) = Vector (repeat [b] len) start false
 let cast_boolvec_bitvec (Vector bs start inc) =
   Vector (List.map bool_to_bitU bs) start inc
 let cast_vec_bl (Vector bs start inc) = bs
+let cast_bl_vec (start, len, bs) = Vector (extz_bl (len, bs)) start false
+let cast_bl_svec (start, len, bs) = Vector (bits_of_int (len, bitlist_to_signed bs)) start false
+let cast_int_vec n = of_bits (int_to_bin n)
 
 let pp_bitu_vector (Vector elems start inc) =
   let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in
@@ -150,10 +153,6 @@ let extz (start, len, vec) = set_vector_start (start, to_norm_vec (get_dir vec)
 let exts_big (start, len, vec) = set_vector_start (start, to_vec_big (get_dir vec) (len, signed_big vec))
 let extz_big (start, len, vec) = set_vector_start (start, to_vec_big (get_dir vec) (len, unsigned_big vec))
 
-(* TODO *)
-let extz_bl (start, len, bits) = Vector bits start false
-let exts_bl (start, len, bits) = Vector bits start false
-
 
 let quot = hardware_quot
 let modulo (l,r) = hardware_mod l r