2 files changed, 12 insertions, 2 deletions
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 6d895a87..4018fd54 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -32,8 +32,8 @@ let inline (>>=) = bind
 val (>>) : forall 'b. M unit -> M 'b -> M 'b
 let inline (>>) m n = m >>= fun _ -> n
 
-val exit : forall 'a. string -> M 'a
-let exit s = Fail (Just s)
+val exit : forall 'a 'b. 'b -> M 'a
+let exit s = Fail Nothing
 
 val read_mem : end_flag -> bool -> read_kind -> vector bitU -> integer -> M (vector bitU)
 let read_mem endian dir rk addr sz =
@@ -93,6 +93,9 @@ let write_reg_field reg regfield v =
 let write_reg_bitfield reg regfield bit =
   write_reg_aux (extern_reg_field_whole reg regfield)
                 (Vector [bit] 0 (is_inc_of_reg reg))
+let write_reg_field_range reg regfield i j v =
+  write_reg_aux (extern_reg_field_slice reg regfield (natFromInteger i,natFromInteger j)) v
+
 
 
 val barrier : barrier_kind -> M unit
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 399cc218..2b270e65 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -267,6 +267,8 @@ let hardware_quot (a:integer) (b:integer) : integer =
   then (a/b) + 1
   else a/b
 
+let quot_signed = hardware_quot
+
 
 let signed_big = signed
 
@@ -588,6 +590,11 @@ let rec repeat xs n =
   if n = 0 then []
   else xs ++ repeat xs (n-1)
 
+(*
+let duplicate bit length =
+  Vector (repeat [bit] length) (if dir then 0 else length - 1) dir
+ *)
+
 let compare_op op (l,r) = bool_to_bit (op l r)
 
 let lt = compare_op (<)