shallow embedding progress

1 files changed, 35 insertions, 65 deletions

diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index b369fd21..18868b4a 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -35,93 +35,63 @@ let inline (>>) m n = m >>= fun _ -> n
 val exit : forall 'a. string -> M 'a
 let exit s = Fail (Just s)
 
-val read_memory : bool -> read_kind -> vector bitU -> integer -> M (vector bitU)
-let read_memory dir rk addr sz =
+val read_mem : end_flag -> bool -> read_kind -> vector bitU -> integer -> M (vector bitU)
+let read_mem endian 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 dir memory_value in
+    let bitv = intern_mem_value endian 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
-let write_memory_ea wk addr sz =
+val write_mem_ea : write_kind -> vector bitU -> integer -> M unit
+let write_mem_ea wk addr sz =
   let addr = address_lifted_of_bitv addr in
   let sz = natFromInteger sz in
   Write_ea (wk,addr,sz) (Done (),Nothing)
 
-val write_memory_val : vector bitU -> M bool
-let write_memory_val v =
-  let v = byte_lifteds_of_bitv v in
+val write_mem_val : end_flag -> vector bitU -> M bool
+let write_mem_val endian v =
+  let v = extern_mem_value endian v in
   let k successful = (return successful,Nothing) in
   Write_memv v k
 
-
-val read_reg_range : register -> integer -> integer -> M (vector bitU)
-let read_reg_range reg i j =
-  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)
-                      (if i<j then (i,j) else (j,i)) in
-  let k register_value =
-    let v = bitv_of_register_value register_value in
+val read_reg_aux : reg_name -> M (vector bitU)
+let read_reg_aux reg = 
+  let k reg_value =
+    let v = intern_reg_value reg_value in
     (Done v,Nothing) in
   Read_reg reg k
 
-val read_reg_bit : register -> integer -> M bitU
-let read_reg_bit reg i =
-  read_reg_range reg i i >>= fun v -> return (access v i)
-
-val read_reg : register -> M (vector bitU)
 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 = bitv_of_register_value register_value in
-    (Done v,Nothing) in
-  Read_reg reg k
-
-
-val read_reg_field : register -> register_field -> M (vector bitU)
+  read_reg_aux (extern_reg_whole reg)
+let read_reg_range reg i j =
+  read_reg_aux (extern_reg_slice reg (i,j))
+let read_reg_bit reg i =
+  read_reg_aux (extern_reg_slice reg (i,i)) >>= fun v ->
+  return (extract_only_bit v)
 let read_reg_field reg regfield =
-  let (i,j) = register_field_indices_nat reg regfield in
-  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 = bitv_of_register_value register_value in
-    (Done v,Nothing) in
-  Read_reg reg k
-
-val read_reg_bitfield : register -> register_field -> M bitU
-let read_reg_bitfield reg rbit =
-  read_reg_bit reg (fst (register_field_indices reg rbit))
+  read_reg_aux (extern_reg_field_whole reg regfield)
+let read_reg_bitfield reg regfield =
+  read_reg_aux (extern_reg_field_whole reg regfield) >>= fun v ->
+  return (extract_only_bit v)
 
+val write_reg_aux : reg_name -> vector bitU -> M unit
+let write_reg_aux reg_name v =
+  let regval = extern_reg_value reg_name v in
+  Write_reg (reg_name,regval) (Done (), Nothing)
 
-val write_reg_range : register -> integer -> integer -> vector bitU -> M unit
+let write_reg reg v =
+  write_reg_aux (extern_reg_whole reg) v
 let write_reg_range reg i j v =
-  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
+  write_reg_aux (extern_reg_slice reg (i,j)) v
 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 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
-let write_reg_field reg regfield =
-  uncurry (write_reg_range reg) (register_field_indices reg regfield)
-
-val write_reg_bitfield : register -> register_field -> bitU -> M unit
-let write_reg_bitfield reg rbit =
-  write_reg_bit reg (fst (register_field_indices reg rbit))
+  write_reg_aux (extern_reg_slice reg (i,i)) (Vector [bit] i (is_inc_of_reg reg))
+let write_reg_field reg regfield v =
+  write_reg_aux (extern_reg_field_whole reg regfield) v
+let write_reg_bitfield reg regfield bit =
+  write_reg_aux (extern_reg_field_whole reg regfield)
+                (Vector [bit] 0 (is_inc_of_reg reg))
 
 
 val barrier : barrier_kind -> M unit