diff options
Diffstat (limited to 'src/pretty_print_lem.ml')
| -rw-r--r-- | src/pretty_print_lem.ml | 19 |
1 files changed, 15 insertions, 4 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 5e0d39a0..e2c8c0ac 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -418,10 +418,21 @@ let doc_exp_lem, doc_let_lem = (align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^ parens (string "update_reg_field_bit" ^/^ field_ref ^/^ expY e2) ^/^ expY e))) | _ -> - liftR ((prefix 2 1) - (string "update_reg") - (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^ - parens (string "update_reg_bit" ^/^ expY e2) ^/^ expY e)) + (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" -> + (* Special case vectors of register references *) + let deref = + parens (separate space [ + string "access"; + expY (lexp_to_exp le); + expY e2 + ]) in + liftR ((prefix 2 1) (string "write_reg") (deref ^/^ expY e)) + | _ -> + liftR ((prefix 2 1) (string "update_reg") + (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^ + parens (string "update_reg_bit" ^/^ expY e2) ^/^ expY e))) ) (* | LEXP_field (le,id) when is_bit_typ t -> liftR ((prefix 2 1) |