more shallow embedding fixes

1 files changed, 12 insertions, 10 deletions

diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 6dea2e9b..b369fd21 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -35,16 +35,16 @@ let inline (>>) m n = m >>= fun _ -> n
 val exit : forall 'a. string -> M 'a
 let exit s = Fail (Just s)
 
-val read_memory : read_kind -> vector bitU -> integer -> M (vector bitU)
-let read_memory rk addr sz =
+val read_memory : bool -> read_kind -> vector bitU -> integer -> M (vector bitU)
+let read_memory dir rk addr sz =
   let addr = address_lifted_of_bitv addr in
   let sz = natFromInteger sz in
   let k memory_value =
-    let bitv = bitv_of_byte_lifteds memory_value in
+    let bitv = bitv_of_byte_lifteds dir memory_value in
     (Done bitv,Nothing) in
   Read_mem (rk,addr,sz) k
 
-val write_memory_ea : write_kind -> vector bitU -> integer  -> M unit
+val write_memory_ea : write_kind -> vector bitU -> integer -> M unit
 let write_memory_ea wk addr sz =
   let addr = address_lifted_of_bitv addr in
   let sz = natFromInteger sz in
@@ -63,7 +63,7 @@ let read_reg_range reg i j =
   let reg = Reg_slice (name_of_reg reg) (start_of_reg_nat reg) (dir_of_reg reg)
                       (if i<j then (i,j) else (j,i)) in
   let k register_value =
-    let v = bitvFromRegisterValue register_value in
+    let v = bitv_of_register_value register_value in
     (Done v,Nothing) in
   Read_reg reg k
 
@@ -76,7 +76,7 @@ let read_reg reg =
   let reg = Reg (name_of_reg reg) (start_of_reg_nat reg)
                 (size_of_reg_nat reg) (dir_of_reg reg) in
   let k register_value =
-    let v = bitvFromRegisterValue register_value in
+    let v = bitv_of_register_value register_value in
     (Done v,Nothing) in
   Read_reg reg k
 
@@ -87,7 +87,7 @@ let read_reg_field reg regfield =
   let reg = Reg_slice (name_of_reg reg) (start_of_reg_nat reg) (dir_of_reg reg)
                       (if i<j then (i,j) else (j,i)) in
   let k register_value =
-    let v = bitvFromRegisterValue register_value in
+    let v = bitv_of_register_value register_value in
     (Done v,Nothing) in
   Read_reg reg k
 
@@ -98,19 +98,21 @@ let read_reg_bitfield reg rbit =
 
 val write_reg_range : register -> integer -> integer -> vector bitU -> M unit
 let write_reg_range reg i j v =
-  let rv = registerValueFromBitv v reg in
   let (i,j) = (natFromInteger i,natFromInteger j) in
   let reg = Reg_slice (name_of_reg reg) (start_of_reg_nat reg) (dir_of_reg reg) (i,j) in
+  let rv = extern_reg_value reg v in
   Write_reg (reg,rv) (Done (),Nothing)
 
 val write_reg_bit : register -> integer -> bitU -> M unit
-let write_reg_bit reg i bit = write_reg_range reg i i (Vector [bit] 0 true)
+let write_reg_bit reg i bit =
+  write_reg_range reg i i (Vector [bit] 0 (is_inc_of_reg reg))
+  (* the zero start index shouldn't matter *)
 
 val write_reg : register -> vector bitU -> M unit
 let write_reg reg v =
-  let rv = registerValueFromBitv v reg in
   let reg = Reg (name_of_reg reg) (start_of_reg_nat reg)
                 (size_of_reg_nat reg) (dir_of_reg reg) in
+  let rv = extern_reg_value reg v in
   Write_reg (reg,rv) (Done (),Nothing)
 
 val write_reg_field : register -> register_field -> vector bitU -> M unit