3 files changed, 18 insertions, 12 deletions
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 3efdd163..6fa406b8 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -136,6 +136,9 @@ let return a = Done a
 val (>>=) : forall 'a 'b. M 'a -> ('a -> M 'b) -> M 'b
 val (>>>) : forall 'a 'b 'c. ('a -> M 'b) -> ('b -> M 'c) -> ('a -> M 'c)
 
+val (>>) : forall 'b. M unit -> (unit -> M 'b) -> M 'b
+let (>>) m n = m >>= fun _ -> n
+
 let rec (>>=) m f = match m with
   | Done a -> f a
   | Read_mem rk addr sz rs k ->        Read_mem rk addr sz rs        (fun v -> (k v) >>= f)
@@ -153,8 +156,6 @@ let rec (>>=) m f = match m with
 val exit : forall 'a 'e. 'e -> M 'a
 let exit _ = Escape
 
-let (>>) m n = m >>= fun _ -> n
-
 val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a)
 let rec byte_chunks n list = match (n,list) with
   | (0,_) -> []
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index fa2afe23..c78a6cdf 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -69,6 +69,8 @@ let unsigned (V bs _ _ as v) : integer =
     fst (List.foldl
            (fun (acc,exp) b -> (acc + (if b = I then integerPow 2 exp else 0),exp +1)) (0,0) bs)
 
+let unsigned_big = unsigned
+        
 let signed v : integer =
   match most_significant v with
   | I -> 0 - (1 + (unsigned (bitwise_not v)))
@@ -76,6 +78,8 @@ let signed v : integer =
   | _ -> failwith "signed applied to vector with undefined bits"
   end
 
+let signed_big = signed
+
 let to_num sign = if sign then signed else unsigned
   
 let max_64u = (integerPow 2 64) - 1
@@ -137,6 +141,8 @@ let to_vec is_inc ((len : integer),(n : integer)) =
     let (V bs start is_inc) = bitwise_not (V abs_bs start is_inc) in
     V (add_one_bit bs false (len-1)) start is_inc
 
+let to_vec_big = to_vec
+      
 let to_vec_inc = to_vec true
 let to_vec_dec = to_vec false
 
@@ -146,6 +152,13 @@ let to_vec_undef is_inc (len : integer) =
 let to_vec_inc_undef = to_vec_undef true
 let to_vec_dec_undef = to_vec_undef false
 
+let get_dir (V _ _ ord) = ord
+                                    
+let exts (len, vec) = to_vec (get_dir vec) (len,signed vec)
+let extz (len, vec) = to_vec (get_dir vec) (len,unsigned vec)
+
+let exts_big (len, vec) = to_vec_big (get_dir vec) (len, signed_big vec)
+let extz_big (len, vec) = to_vec_big (get_dir vec) (len, unsigned_big vec)
 
 let add = integerAdd
 let add_signed = integerAdd
@@ -444,14 +457,6 @@ let neq_range_vec (l,r) = bitwise_not_bit (eq_range_vec (l,r))
 (* temporarily *)
 val neq : forall 'a 'b. 'a * 'b -> bit
 let neq _ = O
-                                          
-
-let EXTS (v1,(V _ _ is_inc as v)) =
-  to_vec is_inc (v1,signed v)
-
-let EXTZ = EXTS
-
-let exts = EXTS 
 
 val make_indexed_vector_reg : list (integer * register) -> maybe register -> integer -> integer ->
                               vector register
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 983d14c6..610bcc7d 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -30,12 +30,12 @@ let bind m f s = match m s with
   | (Right error,s') -> (Right error,s')
   end
 
-val exit : forall 's 'e. 'e -> State 's 'e unit
+val exit : forall 's 'e 'a. 'e -> State 's 'e 'a
 let exit e s = (Right e,s)
 
 let (>>=) = bind
 
-val (>>): forall 's 'e 'a 'b. State 's 'e 'a -> State 's 'e 'b -> State 's 'e 'b
+val (>>): forall 's 'e 'b. State 's 'e unit -> State 's 'e 'b -> State 's 'e 'b
 let (>>) m n = m >>= fun _ -> n
 
 val read_writeEA : forall 'e. unit -> State state 'e (integer * integer)