Support vector registers (other than bitvectors)

3 files changed, 19 insertions, 6 deletions

diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 0de76624..f5ac8fc5 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -133,6 +133,7 @@ let write_reg_range reg i j v =
 let write_reg_pos reg i v =
   let iN = natFromInteger i in
   write_reg_aux (external_reg_slice reg (iN,iN)) [v]
+let write_reg_bit = write_reg_pos
 let write_reg_field reg regfield v =
   write_reg_aux (external_reg_field_whole reg regfield.field_name) v
 (*let write_reg_field_bit reg regfield bit =
@@ -142,6 +143,7 @@ let write_reg_field_range reg regfield i j v =
   write_reg_aux (external_reg_field_slice reg regfield.field_name (natFromInteger i,natFromInteger j)) v
 let write_reg_field_pos reg regfield i v =
   write_reg_field_range reg regfield i i [v]
+let write_reg_field_bit = write_reg_field_pos
 
 
 
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 2f835d56..dc30a17f 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -184,21 +184,30 @@ val update_reg_range : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => registe
 let update_reg_range reg i j reg_val new_val = set_bits (reg.reg_is_inc) (reg.reg_start) reg_val i j (bits_of new_val)
 let write_reg_range reg i j = update_reg reg (update_reg_range reg i j)
 
-let update_reg_pos reg i reg_val bit = set_bit (reg.reg_is_inc) (reg.reg_start) reg_val i (to_bitU bit)
+let update_reg_pos reg i reg_val x = update_pos reg_val i x
 let write_reg_pos reg i = update_reg reg (update_reg_pos reg i)
 
+let update_reg_bit reg i reg_val bit = set_bit (reg.reg_is_inc) (reg.reg_start) reg_val i (to_bitU bit)
+let write_reg_bit reg i = update_reg reg (update_reg_bit reg i)
+
 let update_reg_field_range regfield i j reg_val new_val =
   let current_field_value = regfield.get_field reg_val in
   let new_field_value = set_bits (regfield.field_is_inc) (regfield.field_start) current_field_value i j (bits_of new_val) in
   regfield.set_field reg_val new_field_value
 let write_reg_field_range reg regfield i j = update_reg reg (update_reg_field_range regfield i j)
 
-let update_reg_field_pos regfield i reg_val bit =
+let update_reg_field_pos regfield i reg_val x =
   let current_field_value = regfield.get_field reg_val in
-  let new_field_value = set_bit (regfield.field_is_inc) (regfield.field_start) current_field_value i (to_bitU bit) in
+  let new_field_value = update_pos current_field_value i x in
   regfield.set_field reg_val new_field_value
 let write_reg_field_pos reg regfield i = update_reg reg (update_reg_field_pos regfield i)
 
+let update_reg_field_bit regfield i reg_val bit =
+  let current_field_value = regfield.get_field reg_val in
+  let new_field_value = set_bit (regfield.field_is_inc) (regfield.field_start) current_field_value i (to_bitU bit) in
+  regfield.set_field reg_val new_field_value
+let write_reg_field_bit reg regfield i = update_reg reg (update_reg_field_bit regfield i)
+
 val barrier : forall 'regs. barrier_kind -> M 'regs unit
 let barrier _ = return ()
 
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index fdb65386..f6fec143 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -418,11 +418,12 @@ let doc_exp_lem, doc_let_lem =
                    doc_id_lem (typ_id_of (typ_of_annot lannot)) ^^
                    underscore ^^
                    doc_id_lem id in
+                 let call = if is_bitvector_typ (Env.base_typ_of (env_of full_exp) (typ_of_annot fannot)) then "write_reg_field_bit" else "write_reg_field_pos" in
                  liftR ((prefix 2 1)
-                   (string "write_reg_field_pos")
+                   (string call)
                    (align (doc_lexp_deref_lem sequential mwords early_ret le ^/^
                      field_ref ^/^ expY e2 ^/^ expY e)))
-            | _ ->
+            | LEXP_aux (_, lannot) ->
                (match le with
                  | LEXP_aux (_, (_, Some (_, Typ_aux (Typ_app (vector, [_; _; _; Typ_arg_aux (Typ_arg_typ etyp, _)]), _), _)))
                    when is_reftyp etyp && string_of_id vector = "vector" ->
@@ -436,7 +437,8 @@ let doc_exp_lem, doc_let_lem =
                    liftR ((prefix 2 1) (string "write_reg") (deref ^/^ expY e))
                  | _ ->
                    let deref = doc_lexp_deref_lem sequential mwords early_ret le in
-                   liftR ((prefix 2 1) (string "write_reg_pos")
+                   let call = if is_bitvector_typ (Env.base_typ_of (env_of full_exp) (typ_of_annot lannot)) then "write_reg_bit" else "write_reg_pos" in
+                   liftR ((prefix 2 1) (string call)
                    (deref ^/^ expY e2 ^/^ expY e)))
            )
         (* | LEXP_field (le,id) when is_bit_typ t ->