3 files changed, 16 insertions, 18 deletions

diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 72effa2f..dd97541f 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -31,12 +31,12 @@ let inline (>>) m n = m >>= fun _ -> n
 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 =
+val read_mem : bool -> read_kind -> vector bitU -> integer -> M (vector bitU)
+let read_mem dir rk addr sz =
   let addr = address_lifted_of_bitv addr in
   let sz = natFromInteger sz in
   let k memory_value =
-    let bitv = internal_mem_value endian dir memory_value in
+    let bitv = internal_mem_value dir memory_value in
     (Done bitv,Nothing) in
   Read_mem (rk,addr,sz) k
 
@@ -46,9 +46,9 @@ let write_mem_ea wk addr sz =
   let sz = natFromInteger sz in
   Write_ea (wk,addr,sz) (Done (),Nothing)
 
-val write_mem_val : end_flag -> vector bitU -> M bool
-let write_mem_val endian v =
-  let v = external_mem_value endian v in
+val write_mem_val : vector bitU -> M bool
+let write_mem_val v =
+  let v = external_mem_value v in
   let k successful = (return successful,Nothing) in
   Write_memv v k
 
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 4771bcd7..e0d60dee 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -849,13 +849,11 @@ let external_reg_field_slice reg rfield (i,j) =
               (external_slice dir start (m,n))
               (external_slice dir start (i,j))
 
-let external_mem_value endian v =
-  let bytes = byte_lifteds_of_bitv v in 
-  if endian = E_big_endian then bytes else List.reverse bytes
+let external_mem_value v =
+  byte_lifteds_of_bitv v $> List.reverse
 
-let internal_mem_value endian direction bytes = 
-  let v = if endian = E_big_endian then bytes else List.reverse bytes in
-  bitv_of_byte_lifteds direction v
+let internal_mem_value direction bytes =
+  List.reverse bytes $> bitv_of_byte_lifteds direction
 
 
 
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 02fe8094..0dfd10d7 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -45,12 +45,12 @@ let set_reg state reg bitv =
   <| state with regstate = Map.insert reg bitv state.regstate |>
 
 
-val read_mem : end_flag -> bool -> read_kind -> vector bitU -> integer -> M (vector bitU)
-let read_mem endian dir read_kind addr sz state =
+val read_mem : bool -> read_kind -> vector bitU -> integer -> M (vector bitU)
+let read_mem dir read_kind addr sz state =
   let addr = integer_of_address (address_of_bitv addr) in
   let addrs = range addr (addr+sz-1) in
   let memory_value = List.map (fun addr -> Map_extra.find addr state.memstate) addrs in
-  let value = Sail_values.internal_mem_value endian dir memory_value in
+  let value = Sail_values.internal_mem_value dir memory_value in
   let is_exclusive = match read_kind with
     | Sail_impl_base.Read_plain -> false
     | Sail_impl_base.Read_tag -> failwith "Read_tag not implemented"
@@ -73,13 +73,13 @@ let write_mem_ea write_kind addr sz state =
   let addr = integer_of_address (address_of_bitv addr) in
   [(Left (), <| state with write_ea = Just (write_kind,addr,sz) |>)]
 
-val write_mem_val : end_flag -> vector bitU -> M bool
-let write_mem_val endian v state =
+val write_mem_val : vector bitU -> M bool
+let write_mem_val v state =
   let (write_kind,addr,sz) = match state.write_ea with
     | Nothing -> failwith "write ea has not been announced yet"
     | Just write_ea -> write_ea end in
   let addrs = range addr (addr+sz-1) in
-  let v = external_mem_value endian v in
+  let v = external_mem_value v in
   let addresses_with_value = List.zip addrs v in
   let memstate = List.foldl (fun mem (addr,v) -> Map.insert addr v mem)
                             state.memstate addresses_with_value in