diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_lem.ml | 23 | ||||
| -rw-r--r-- | src/rewriter.ml | 15 |
2 files changed, 30 insertions, 8 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index e2c8c0ac..1bfb19aa 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -530,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 *) @@ -709,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 @@ -717,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)) diff --git a/src/rewriter.ml b/src/rewriter.ml index d6a6aa2f..62ea6be7 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -2220,8 +2220,9 @@ let rec rewrite_local_lexp ((LEXP_aux(lexp,((l,_) as annot))) as le) = (lhs, (fun exp -> rhs (E_aux (E_vector_update_subrange (lexp_to_exp lexp, e1, e2, exp), annot)))) | LEXP_field (lexp, id) -> let (lhs, rhs) = rewrite_local_lexp lexp in + let (LEXP_aux (_, recannot)) = lexp in let field_update exp = FES_aux (FES_Fexps ([FE_aux (FE_Fexp (id, exp), annot)], false), annot) in - (lhs, (fun exp -> rhs (E_aux (E_record_update (lexp_to_exp lexp, field_update exp), annot)))) + (lhs, (fun exp -> rhs (E_aux (E_record_update (lexp_to_exp lexp, field_update exp), recannot)))) | _ -> raise (Reporting_basic.err_unreachable l ("Unsupported lexp: " ^ string_of_lexp le)) (*Expects to be called after rewrite_defs; thus the following should not appear: @@ -2946,6 +2947,18 @@ let rewrite_defs_letbind_effects = let _ = reset_fresh_name_counter () in FCL_aux (FCL_Funcl (id,pat,n_exp_term newreturn exp),annot) in FD_aux (FD_function(recopt,tannotopt,effectopt,List.map rewrite_funcl funcls),fdannot) in + let rewrite_def rewriters = function + | DEF_val (LB_aux (lb, annot)) -> + let rewrap lb = DEF_val (LB_aux (lb, annot)) in + begin + match lb with + | LB_val_implicit (pat, exp) -> + rewrap (LB_val_implicit (pat, n_exp_term (effectful exp) exp)) + | LB_val_explicit (ts, pat, exp) -> + rewrap (LB_val_explicit (ts, pat, n_exp_term (effectful exp) exp)) + end + | DEF_fundef fdef -> DEF_fundef (rewrite_fun rewriters fdef) + | d -> d in rewrite_defs_base {rewrite_exp = rewrite_exp ; rewrite_pat = rewrite_pat |