3 files changed, 16 insertions, 9 deletions
diff --git a/src/gen_lib/power_extras.lem b/src/gen_lib/power_extras.lem
index 8515a406..2883c810 100644
--- a/src/gen_lib/power_extras.lem
+++ b/src/gen_lib/power_extras.lem
@@ -36,7 +36,7 @@ let EIEIO_Sync () = return ()
 
 let recalculate_dependency () = return ()
 
-let trap () = ()
+let trap () = exit ()
 (* this needs to change, but for that we'd have to make the type checker know about trap 
  * as an effect *)
 
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index ace65b3b..fa2afe23 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -434,18 +434,25 @@ let eq (l,r) = bool_to_bit (l = r)
 let eq_vec_range (l,r) = eq (to_num false l,r)
 let eq_range_vec (l,r) = eq (l, to_num false r)
 let eq_vec_vec (l,r) = eq (to_num true l, to_num true r)
-
-let neq (l,r) = bitwise_not_bit (eq (l,r))
+(*
+let neq (l,r) = bitwise_not_bit (eq (l,r)) *)
 let neq_vec (l,r) = bitwise_not_bit (eq_vec_vec (l,r))
 let neq_vec_range (l,r) = bitwise_not_bit (eq_vec_range (l,r))
 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
 let make_indexed_vector_reg entries default start length =
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index b5b0c37f..983d14c6 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -130,23 +130,23 @@ let rec foreach_dec (i,stop,by) vars body =
   else ((),vars)
 
 
-val foreachState_inc : forall 's 'e 'vars. (integer * integer * integer) -> 'vars ->
+val foreachM_inc : forall 's 'e 'vars. (integer * integer * integer) -> 'vars ->
                   (integer -> 'vars -> State 's 'e (unit * 'vars)) -> State 's 'e (unit * 'vars)
-let rec foreachState_inc (i,stop,by) vars body = 
+let rec foreachM_inc (i,stop,by) vars body = 
   if i <= stop
   then
     body i vars >>= fun (_,vars) ->
-    foreachState_inc (i + by,stop,by) vars body
+    foreachM_inc (i + by,stop,by) vars body
   else return ((),vars)
 
 
-val foreachState_dec : forall 's 'e 'vars. (integer * integer * integer) -> 'vars ->
+val foreachM_dec : forall 's 'e 'vars. (integer * integer * integer) -> 'vars ->
                   (integer -> 'vars -> State 's 'e (unit * 'vars)) -> State 's 'e (unit * 'vars)
-let rec foreachState_dec (i,stop,by) vars body = 
+let rec foreachM_dec (i,stop,by) vars body = 
   if i >= stop
   then
     body i vars >>= fun (_,vars) ->
-    foreachState_dec (i - by,stop,by) vars body
+    foreachM_dec (i - by,stop,by) vars body
   else return ((),vars)
 
 val read_reg_field : forall 'e. register -> register_field -> State state 'e (vector bit)