2 files changed, 17 insertions, 12 deletions
diff --git a/mips/mips_extras.lem b/mips/mips_extras.lem
index f0f6a0c5..4e570a6f 100644
--- a/mips/mips_extras.lem
+++ b/mips/mips_extras.lem
@@ -1,10 +1,10 @@
 open import Pervasives
 open import Pervasives_extra
-open import Sail_instr_kinds
-open import Sail_values
-open import Sail_operators
-open import Prompt_monad
-open import Prompt
+open import Sail2_instr_kinds
+open import Sail2_values
+open import Sail2_operators
+open import Sail2_prompt_monad
+open import Sail2_prompt
 
 val MEMr             : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval 'b 'e
 val MEMr_reserve     : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval 'b 'e
@@ -80,9 +80,6 @@ let read_ram _ size _ addr = MEMr addr size
 let string_of_bits bs = string_of_bv (bits_of bs)
 let string_of_int = show
 
-let _sign_extend bits len = maybe_failwith (of_bits (exts_bv len bits))
-let _zero_extend bits len = maybe_failwith (of_bits (extz_bv len bits))
-
 let shift_bits_left v n =
   let r = Maybe.bind (unsigned n) (fun n -> of_bits (shiftl_bv v n)) in
   maybe_fail "shift_bits_left" r
@@ -121,3 +118,8 @@ let print_bits msg bs = prerr_endline (msg ^ (string_of_bits bs))
 val get_time_ns : unit -> integer
 let get_time_ns () = 0
 declare ocaml target_rep function get_time_ns = `(fun () -> Big_int.of_int (int_of_float (1e9 *. Unix.gettimeofday ())))`
+
+val cycle_count : unit -> unit
+let cycle_count _ = ()
+
+let inline eq_bit = eq
diff --git a/mips/prelude.sail b/mips/prelude.sail
index 1c1a38ce..76638c68 100644
--- a/mips/prelude.sail
+++ b/mips/prelude.sail
@@ -149,11 +149,14 @@ union exception = {
   Error_internal_error : unit
 }
 
-val sign_extend : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m)
-val zero_extend : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m)
+val mips_sign_extend : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m)
+val mips_zero_extend : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m)
 
-function sign_extend v = sail_sign_extend(v, sizeof('m))
-function zero_extend v = sail_zero_extend(v, sizeof('m))
+function mips_sign_extend v = sail_sign_extend(v, sizeof('m))
+function mips_zero_extend v = sail_zero_extend(v, sizeof('m))
+
+overload sign_extend = {mips_sign_extend}
+overload zero_extend = {mips_zero_extend}
 
 val zeros : forall 'n, 'n >= 0 . unit -> bits('n)
 function zeros() = replicate_bits (0b0,'n)