lem gen_lib: update read/write functions to take (dummy) addrsize argument as in other places

1 files changed, 7 insertions, 7 deletions

diff --git a/src/gen_lib/sail2_prompt_monad.lem b/src/gen_lib/sail2_prompt_monad.lem
index e0ac09f6..28c0a27e 100644
--- a/src/gen_lib/sail2_prompt_monad.lem
+++ b/src/gen_lib/sail2_prompt_monad.lem
@@ -170,8 +170,8 @@ let read_mem_bytes rk addr sz =
     (maybe_fail "nat_of_bv" (nat_of_bv addr))
     (fun addr -> Read_mem rk addr (nat_of_int sz) return)
 
-val read_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv 'b 'e
-let read_mem rk addr sz =
+val read_mem : forall 'rv 'a 'b 'e 'addrsize. Bitvector 'a, Bitvector 'b => read_kind -> 'addrsize -> 'a -> integer -> monad 'rv 'b 'e
+let read_mem rk addr_sz addr sz =
   bind
     (read_mem_bytes rk addr sz)
     (fun bytes ->
@@ -185,15 +185,15 @@ let excl_result () =
   let k successful = (return successful) in
   Excl_res k
 
-val write_mem_ea : forall 'rv 'a 'e. Bitvector 'a => write_kind -> 'a -> integer -> monad 'rv unit 'e
-let write_mem_ea wk addr sz =
+val write_mem_ea : forall 'rv 'a 'e 'addrsize. Bitvector 'a => write_kind -> 'addrsize -> 'a -> integer -> monad 'rv unit 'e
+let write_mem_ea wk addr_size addr sz =
   bind
     (maybe_fail "nat_of_bv" (nat_of_bv addr))
     (fun addr -> Write_ea wk addr (nat_of_int sz) (Done ()))
 
-val write_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b =>
-  write_kind -> 'a -> integer -> 'b -> monad 'rv bool 'e
-let write_mem wk addr sz v =
+val write_mem : forall 'rv 'a 'b 'e 'addrsize. Bitvector 'a, Bitvector 'b =>
+  write_kind -> 'addrsize -> 'a -> integer -> 'b -> monad 'rv bool 'e
+let write_mem wk addr_size addr sz v =
   match (mem_bytes_of_bits v, nat_of_bv addr) with
     | (Just v, Just addr) ->
        Write_mem wk addr (nat_of_int sz) v return