diff options
| author | Peter Sewell | 2017-04-06 14:16:49 +0100 |
|---|---|---|
| committer | Peter Sewell | 2017-04-06 14:16:49 +0100 |
| commit | 401f914c9e0ef6a3ac3f1d4e8668afe2ff8c7cff (patch) | |
| tree | 9066ca58852d1894dc507f977112777d5d6edafc /src/pretty_print_ocaml.ml | |
| parent | 3b3af5555654f21f338b38e3adeb62760e5e72ff (diff) | |
| parent | d716893e137a41638b449162dc8b5c682eb7f4d4 (diff) | |
Merge branch 'master' of bitbucket.org:Peter_Sewell/sail
Diffstat (limited to 'src/pretty_print_ocaml.ml')
| -rw-r--r-- | src/pretty_print_ocaml.ml | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/src/pretty_print_ocaml.ml b/src/pretty_print_ocaml.ml index 47aacf0c..5df8691e 100644 --- a/src/pretty_print_ocaml.ml +++ b/src/pretty_print_ocaml.ml @@ -479,10 +479,13 @@ let doc_exp_ocaml, doc_let_ocaml = | _ -> (false,false) in match lexp with | LEXP_vector(v,e) -> - doc_op (string "<-") - (group (parens ((string (if is_bit then "get_barray" else "get_varray")) ^^ space ^^ doc_lexp_ocaml false v)) ^^ - dot ^^ parens ((string "int_of_big_int") ^^ space ^^ (exp e))) - (exp e_new_v) + 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? *) + 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))) | LEXP_vector_range(v,e1,e2) -> parens ((string (if is_bitv then "set_vector_subrange_bit" else "set_vector_subrange_vec")) ^^ space ^^ doc_lexp_ocaml false v ^^ space ^^ exp e1 ^^ space ^^ exp e2 ^^ space ^^ exp e_new_v) |