diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/gen_lib/sail_values.ml | 7 | ||||
| -rw-r--r-- | src/pretty_print_ocaml.ml | 7 |
2 files changed, 10 insertions, 4 deletions
diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml index 19aa4709..aa3141ed 100644 --- a/src/gen_lib/sail_values.ml +++ b/src/gen_lib/sail_values.ml @@ -201,6 +201,13 @@ let set_vector_subrange_bit_big v n m new_v = set_vector_subrange_bit_int v (int_of_big_int n) (int_of_big_int m) new_v let set_vector_subrange_bit = set_vector_subrange_bit_int +let set_register_bit_int reg n v = + match reg with + | Vregister(array,start,inc,fields) -> + (!array).(if inc then (n - start) else (start - n)) <- v + | _ -> failwith "set_register_bit of non-register" +let set_register_bit_big reg n v = set_register_bit_int reg (int_of_big_int n) v +let set_register_bit = set_register_bit_big let set_register_field_v reg field new_v = match reg with diff --git a/src/pretty_print_ocaml.ml b/src/pretty_print_ocaml.ml index 5df8691e..2d9dc888 100644 --- a/src/pretty_print_ocaml.ml +++ b/src/pretty_print_ocaml.ml @@ -479,10 +479,9 @@ let doc_exp_ocaml, doc_let_ocaml = | _ -> (false,false) in match lexp with | LEXP_vector(v,e) -> - if is_bit then - doc_op (string "<-") (group (parens (string "get_barray" ^^ space ^^ doc_lexp_ocaml false v)) ^^ - dot ^^ parens ((string "int_of_big_int") ^^ space ^^ (exp e))) (exp e_new_v) - else (* XXX Check whether vector of reg? *) + if is_bit then (* XXX check whether register or not?? *) + parens ((string "set_register_bit" ^^ space ^^ doc_lexp_ocaml false v ^^ space ^^ exp e ^^ space ^^ exp e_new_v)) + else (* XXX Check whether vector of reg? XXX Does not work for decreasing vector. *) parens ((string "set_register") ^^ space ^^ ((group (parens ((string "get_varray") ^^ space ^^ doc_lexp_ocaml false v)) ^^ dot ^^ parens ((string "int_of_big_int") ^^ space ^^ (exp e))) ^^ space ^^ (exp e_new_v))) |