Merge branch 'experiments' into mono-experiments

1 files changed, 31 insertions, 11 deletions

diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 5e0d39a0..1bfb19aa 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)
@@ -519,14 +530,19 @@ let doc_exp_lem, doc_let_lem =
             if contains_bitvector_typ t && not (contains_t_pp_var t)
             then (align epp ^^ (doc_tannot_lem sequential mwords (effectful eff) t), true)
             else (epp, aexp_needed) in
-          if aexp_needed then parens (align taepp) else taepp
+          if aexp_needed then parens (align taepp) else taepp*)
        | Id_aux (Id "length",_) ->
+          (* Another temporary hack: The sizeof rewriting introduces calls to
+             "length", and the disambiguation between the length function on
+             bitvectors and vectors of other element types should be done by
+             the type checker, but type checking after rewriting steps is
+             currently broken. *)
           let [arg] = args in
           let targ = typ_of arg in
-          let call = if is_bitvector_typ targ then "bvlength" else "length" in
+          let call = if mwords && is_bitvector_typ targ then "bvlength" else "length" in
           let epp = separate space [string call;expY arg] in
           if aexp_needed then parens (align epp) else epp
-       | Id_aux (Id "bool_not", _) ->
+       (*)| Id_aux (Id "bool_not", _) ->
           let [a] = args in
           let epp = align (string "~" ^^ expY a) in
           if aexp_needed then parens (align epp) else epp *)
@@ -698,7 +714,9 @@ let doc_exp_lem, doc_let_lem =
         | _ -> parens (separate_map comma expN exps))
     | E_record(FES_aux(FES_Fexps(fexps,_),_)) ->
        let recordtyp = match annot with
-         | Some (env, Typ_aux (Typ_id tid,_), _) when Env.is_record tid env ->
+         | Some (env, Typ_aux (Typ_id tid,_), _)
+         | Some (env, Typ_aux (Typ_app (tid, _), _), _)
+           when Env.is_record tid env ->
            tid
          | _ ->  raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in
        let epp = anglebars (space ^^ (align (separate_map
@@ -706,9 +724,11 @@ let doc_exp_lem, doc_let_lem =
                                           (doc_fexp sequential mwords early_ret recordtyp) fexps)) ^^ space) in
        if aexp_needed then parens epp else epp
     | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) ->
-       let (E_aux (_, (_, eannot))) = e in
-       let recordtyp = match eannot with
-         | Some (env, Typ_aux (Typ_id tid,_), _) when Env.is_record tid env ->
+       (* let (E_aux (_, (_, eannot))) = e in *)
+       let recordtyp = match annot with
+         | Some (env, Typ_aux (Typ_id tid,_), _)
+         | Some (env, Typ_aux (Typ_app (tid, _), _), _)
+           when Env.is_record tid env ->
            tid
          | _ ->  raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in
        anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp sequential mwords early_ret recordtyp) fexps))