3 files changed, 33 insertions, 2 deletions
diff --git a/src/gen_lib/power_extras.lem b/src/gen_lib/power_extras.lem
index 2883c810..b43c6403 100644
--- a/src/gen_lib/power_extras.lem
+++ b/src/gen_lib/power_extras.lem
@@ -26,6 +26,9 @@ let rec countLeadingZeros (Interp.V_tuple v) = ((match v with
 let MEMr (addr,l) = read_memory (unsigned addr) l
 let MEMr_reserve (addr,l) = read_memory (unsigned addr) l
 
+let MEMw_EA (addr,l) = write_writeEA (unsigned addr) l
+let MEMw_EA_conditional (addr,l) = write_writeEA (unsigned addr) l
+                                        
 let MEMw (addr,l,value) = write_memory (unsigned addr) l value
 let MEMw_conditional (addr,l,value) = write_memory (unsigned addr) l value >> return true
 
@@ -41,6 +44,6 @@ let trap () = exit ()
  * as an effect *)
 
 val countLeadingZeroes : vector bit * integer -> integer
-let countLeadingZeroes (V bits _ _ ,n)  = 
+let countLeadingZeroes (Vector bits _ _ ,n)  = 
   let (_,bits) = List.splitAt (natFromInteger n) bits in
   integerFromNat (List.length (takeWhile ((=) O) bits))
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 1382fd1d..738a0b20 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -1,4 +1,4 @@
-open import Pervasives_extra
+open import Pervasves_extra
 open import Vector
 open import Arch
 
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 0f6aa5ee..3914bdef 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -23,6 +23,8 @@ let bitwise_not_bit = function
   end
 
 let (~) = bitwise_not_bit
+
+val pow : integer -> integer -> integer
 let pow m n = m ** (natFromInteger n)
 
 
@@ -496,3 +498,29 @@ let bitwise_not_range_bit n = bitwise_not (to_vec defaultDir n)
 let mask (n,Vector bits start dir) =
   let current_size = List.length bits in
   Vector (drop (current_size - (natFromInteger n)) bits) (if dir then 0 else (n-1)) dir
+
+
+
+
+(* this is for a temporary workaround int/nat/integer/natural issues*)
+
+class (subInteger 'a)
+  val toInteger : 'a -> integer
+end
+
+
+instance (subInteger integer)
+  let toInteger = id
+end
+
+instance (subInteger int)
+  let toInteger = integerFromInt
+end
+
+instance (subInteger nat)
+  let toInteger = integerFromNat
+end
+
+instance (subInteger natural)
+  let toInteger = integerFromNatural
+end