diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast_util.ml | 15 | ||||
| -rw-r--r-- | src/ast_util.mli | 1 | ||||
| -rw-r--r-- | src/pretty_print_lem.ml | 40 | ||||
| -rw-r--r-- | src/pretty_print_lem_ast.ml | 1 | ||||
| -rw-r--r-- | src/rewriter.ml | 54 | ||||
| -rw-r--r-- | src/util.ml | 9 | ||||
| -rw-r--r-- | src/util.mli | 5 |
7 files changed, 93 insertions, 32 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index 5740a3c7..aef1a05d 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -392,6 +392,11 @@ and string_of_n_constraint = function | NC_aux (NC_true, _) -> "true" | NC_aux (NC_false, _) -> "false" +let string_of_annot = function + | Some (_, typ, eff) -> + "Some (_, " ^ string_of_typ typ ^ ", " ^ string_of_effect eff ^ ")" + | None -> "None" + let string_of_quant_item_aux = function | QI_id (KOpt_aux (KOpt_none kid, _)) -> string_of_kid kid | QI_id (KOpt_aux (KOpt_kind (k, kid), _)) -> string_of_kind k ^ " " ^ string_of_kid kid @@ -629,13 +634,17 @@ let rec is_vector_typ = function let typ_app_args_of = function | Typ_aux (Typ_app (Id_aux (Id c,_), targs), l) -> (c, List.map (fun (Typ_arg_aux (a,_)) -> a) targs, l) - | Typ_aux (_, l) -> raise (Reporting_basic.err_typ l "typ_app_args_of called on non-app type") + | Typ_aux (_, l) as typ -> + raise (Reporting_basic.err_typ l + ("typ_app_args_of called on non-app type " ^ string_of_typ typ)) let rec vector_typ_args_of typ = match typ_app_args_of typ with | ("vector", [Typ_arg_nexp start; Typ_arg_nexp len; Typ_arg_order ord; Typ_arg_typ etyp], _) -> - (start, len, ord, etyp) + (simplify_nexp start, simplify_nexp len, ord, etyp) | ("register", [Typ_arg_typ rtyp], _) -> vector_typ_args_of rtyp - | (_, _, l) -> raise (Reporting_basic.err_typ l "vector_typ_args_of called on non-vector type") + | (_, _, l) -> + raise (Reporting_basic.err_typ l + ("vector_typ_args_of called on non-vector type " ^ string_of_typ typ)) let is_order_inc = function | Ord_aux (Ord_inc, _) -> true diff --git a/src/ast_util.mli b/src/ast_util.mli index 6a150872..e6823ee9 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -146,6 +146,7 @@ val string_of_order : order -> string val string_of_nexp : nexp -> string val string_of_typ : typ -> string val string_of_typ_arg : typ_arg -> string +val string_of_annot : ('a * typ * effect) option -> string val string_of_n_constraint : n_constraint -> string val string_of_quant_item : quant_item -> string val string_of_typquant : typquant -> string diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 4e6b6615..5e0d39a0 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -58,7 +58,11 @@ let langlebar = string "<|" let ranglebar = string "|>" let anglebars = enclose langlebar ranglebar -let fix_id name = match name with +let is_number_char c = + c = '0' || c = '1' || c = '2' || c = '3' || c = '4' || c = '5' || + c = '6' || c = '7' || c = '8' || c = '9' + +let fix_id remove_tick name = match name with | "assert" | "lsl" | "lsr" @@ -76,22 +80,17 @@ let fix_id name = match name with | "EQ" | "integer" -> name ^ "'" - | _ -> name - -let is_number char = - char = '0' || char = '1' || char = '2' || char = '3' || char = '4' || char = '5' || - char = '6' || char = '7' || char = '8' || char = '9' + | _ -> + if name.[0] = '\'' then + let var = String.sub name 1 (String.length name - 1) in + if remove_tick then var else (var ^ "'") + else if is_number_char(name.[0]) then + ("v" ^ name ^ "'") + else name let doc_id_lem (Id_aux(i,_)) = match i with - | Id i -> - (* this not the right place to do this, just a workaround *) - if i.[0] = '\'' then - string ((String.sub i 1 (String.length i - 1)) ^ "'") - else if is_number(i.[0]) then - string ("v" ^ i ^ "'") - else - string (fix_id i) + | Id i -> string (fix_id false i) | DeIid x -> (* add an extra space through empty to avoid a closing-comment * token in case of x ending with star. *) @@ -102,7 +101,7 @@ let doc_id_lem_type (Id_aux(i,_)) = | Id("int") -> string "ii" | Id("nat") -> string "ii" | Id("option") -> string "maybe" - | Id i -> string (fix_id i) + | Id i -> string (fix_id false i) | DeIid x -> (* add an extra space through empty to avoid a closing-comment * token in case of x ending with star. *) @@ -115,12 +114,14 @@ let doc_id_lem_ctor (Id_aux(i,_)) = | Id("nat") -> string "integer" | Id("Some") -> string "Just" | Id("None") -> string "Nothing" - | Id i -> string (fix_id (String.capitalize i)) + | Id i -> string (fix_id false (String.capitalize i)) | DeIid x -> (* add an extra space through empty to avoid a closing-comment * token in case of x ending with star. *) separate space [colon; string (String.capitalize x); empty] +let doc_var_lem kid = string (fix_id true (string_of_kid kid)) + let effectful_set = List.exists (fun (BE_aux (eff,_)) -> @@ -230,6 +231,7 @@ let rec contains_t_pp_var (Typ_aux (t,a) as typ) = match t with | Typ_wild -> true | Typ_id _ -> false | Typ_var _ -> true + | Typ_exist _ -> true | Typ_fn (t1,t2,_) -> contains_t_pp_var t1 || contains_t_pp_var t2 | Typ_tup ts -> List.exists contains_t_pp_var ts | Typ_app (c,targs) -> @@ -321,6 +323,7 @@ let rec doc_pat_lem sequential mwords apat_needed (P_aux (p,(l,annot)) as pa) = begin match id with | Id_aux (Id "None",_) -> string "Nothing" (* workaround temporary issue *) | _ -> doc_id_lem id end + | P_var kid -> doc_var_lem kid | P_as(p,id) -> parens (separate space [doc_pat_lem sequential mwords true p; string "as"; doc_id_lem id]) | P_typ(typ,p) -> let doc_p = doc_pat_lem sequential mwords true p in @@ -697,7 +700,7 @@ let doc_exp_lem, doc_let_lem = let recordtyp = match annot with | Some (env, Typ_aux (Typ_id tid,_), _) when Env.is_record tid env -> tid - | _ -> raise (report l "cannot get record type") in + | _ -> 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 (semi_sp ^^ break 1) (doc_fexp sequential mwords early_ret recordtyp) fexps)) ^^ space) in @@ -707,7 +710,7 @@ let doc_exp_lem, doc_let_lem = let recordtyp = match eannot with | Some (env, Typ_aux (Typ_id tid,_), _) when Env.is_record tid env -> tid - | _ -> raise (report l "cannot get record type") in + | _ -> 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)) | E_vector exps -> let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in @@ -1011,6 +1014,7 @@ let doc_exp_lem, doc_let_lem = top_exp sequential mwords early_ret true e]) | LEXP_id id -> doc_id_lem id | LEXP_cast (typ,id) -> doc_id_lem id + | LEXP_tup lexps -> parens (separate_map comma_sp (doc_lexp_deref_lem sequential mwords early_ret) lexps) | _ -> raise (Reporting_basic.err_unreachable l ("doc_lexp_deref_lem: Shouldn't happen")) (* expose doc_exp_lem and doc_let *) diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml index c75c102f..5edf9d12 100644 --- a/src/pretty_print_lem_ast.ml +++ b/src/pretty_print_lem_ast.ml @@ -328,6 +328,7 @@ let rec pp_format_pat_lem (P_aux(p,(l,annot))) = | P_lit(lit) -> "(P_lit " ^ pp_format_lit_lem lit ^ ")" | P_wild -> "P_wild" | P_id(id) -> "(P_id " ^ pp_format_id_lem id ^ ")" + | P_var(kid) -> "(P_var " ^ pp_format_var_lem kid ^ ")" | P_as(pat,id) -> "(P_as " ^ pp_format_pat_lem pat ^ " " ^ pp_format_id_lem id ^ ")" | P_typ(typ,pat) -> "(P_typ " ^ pp_format_typ_lem typ ^ " " ^ pp_format_pat_lem pat ^ ")" | P_app(id,pats) -> "(P_app " ^ pp_format_id_lem id ^ " [" ^ diff --git a/src/rewriter.ml b/src/rewriter.ml index 3dc66b04..2b096609 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -2183,6 +2183,15 @@ let id_is_local_var id env = match Env.lookup_id id env with | Local _ -> true | _ -> false +let rec lexp_is_local (LEXP_aux (lexp, _)) env = match lexp with + | LEXP_memory _ -> false + | LEXP_id id + | LEXP_cast (_, id) -> id_is_local_var id env + | LEXP_tup lexps -> List.for_all (fun lexp -> lexp_is_local lexp env) lexps + | LEXP_vector (lexp,_) + | LEXP_vector_range (lexp,_,_) + | LEXP_field (lexp,_) -> lexp_is_local lexp env + let id_is_unbound id env = match Env.lookup_id id env with | Unbound -> true | _ -> false @@ -2203,6 +2212,13 @@ let lexp_is_effectful (LEXP_aux (_, (_, annot))) = match annot with let rec rewrite_local_lexp ((LEXP_aux(lexp,((l,_) as annot))) as le) = match lexp with | LEXP_id id | LEXP_cast (_, id) -> (le, E_aux (E_id id, annot), (fun exp -> exp)) + | LEXP_tup les -> + let get_id (LEXP_aux(lexp,((l,_) as annot)) as le) = match lexp with + | LEXP_id id | LEXP_cast (_, id) -> E_aux (E_id id, annot) + | _ -> + raise (Reporting_basic.err_unreachable l + ("Unsupported sub-lexp " ^ string_of_lexp le ^ " in tuple")) in + (le, E_aux (E_tuple (List.map get_id les), annot), (fun exp -> exp)) | LEXP_vector (lexp, e) -> let (lexp, access, rexp) = rewrite_local_lexp lexp in (lexp, E_aux (E_vector_access (access, e), annot), @@ -2233,7 +2249,7 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f let rec walker exps = match exps with | [] -> [] | (E_aux(E_assign(le,e), ((l, Some (env,typ,eff)) as annot)) as exp)::exps - when lexp_is_local_intro le env && not (lexp_is_effectful le)-> + when lexp_is_local_intro le env && not (lexp_is_effectful le) -> let (le', _, re') = rewrite_local_lexp le in let e' = re' (rewrite_base e) in let exps' = walker exps in @@ -2371,12 +2387,11 @@ let rewrite_defs_early_return = | _ -> exp in let e_block es = - (* let rec walker = function - | e :: es -> if is_return e then [e] else e :: walker es - | [] -> [] in - let es = walker es in *) match es with | [E_aux (e, _)] -> e + | _ :: _ when is_return (Util.last es) -> + let (E_aux (_, annot) as e) = Util.last es in + E_return (E_aux (E_block (Util.butlast es @ [get_return e]), annot)) | _ -> E_block es in let e_if (e1, e2, e3) = @@ -2404,14 +2419,19 @@ let rewrite_defs_early_return = | _ -> full_exp in let rewrite_funcl_early_return _ (FCL_aux (FCL_Funcl (id, pat, exp), a)) = - let exp = fold_exp - { id_exp_alg with e_block = e_block; e_if = e_if; e_case = e_case; - e_aux = e_aux } exp in + let exp = + exp + (* Pull early returns out as far as possible *) + |> fold_exp { id_exp_alg with e_block = e_block; e_if = e_if; e_case = e_case } + (* Remove singleton E_return *) + |> get_return + (* Fix effect annotations *) + |> fold_exp { id_exp_alg with e_aux = e_aux } in let a = match a with | (l, Some (env, typ, eff)) -> (l, Some (env, typ, union_effects eff (effect_of exp))) | _ -> a in - FCL_aux (FCL_Funcl (id, pat, get_return exp), a) in + FCL_aux (FCL_Funcl (id, pat, exp), a) in let rewrite_fun_early_return rewriters (FD_aux (FD_function (rec_opt, tannot_opt, effect_opt, funcls), a)) = @@ -2948,8 +2968,19 @@ let rewrite_defs_letbind_effects = let rewrite_defs_effectful_let_expressions = + let rec pat_of_local_lexp (LEXP_aux (lexp, ((l, _) as annot))) = match lexp with + | LEXP_id id -> P_aux (P_id id, annot) + | LEXP_cast (typ, id) -> P_aux (P_typ (typ, P_aux (P_id id, annot)), annot) + | LEXP_tup lexps -> P_aux (P_tup (List.map pat_of_local_lexp lexps), annot) + | _ -> raise (Reporting_basic.err_unreachable l "unexpected local lexp") in + let e_let (lb,body) = match lb with + | LB_aux (LB_val_implicit (P_aux (P_wild, _), E_aux (E_assign ((LEXP_aux (_, annot) as le), exp), _)), _) + when lexp_is_local le (env_of_annot annot) -> + (* Rewrite assignments to local variables into let bindings *) + let (lhs, _, rhs) = rewrite_local_lexp le in + E_let (LB_aux (LB_val_implicit (pat_of_local_lexp lhs, rhs exp), annot), body) | LB_aux (LB_val_explicit (_,pat,exp'),annot') | LB_aux (LB_val_implicit (pat,exp'),annot') -> if effectful exp' @@ -3261,7 +3292,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = "tail-position": check the definition nexp_term and where it is used. *) | _ -> exp -let replace_memwrite_e_assign exp = +let replace_memwrite_e_assign exp = let e_aux = fun (expaux,annot) -> match expaux with | E_assign (LEXP_aux (LEXP_memory (id,args),_),v) -> E_aux (E_app (id,args @ [v]),annot) @@ -3395,7 +3426,8 @@ let rewrite_defs_remove_e_assign = let recheck_defs defs = fst (check initial_env defs) let rewrite_defs_lem =[ - top_sort_defs; + (* top_sort_defs; *) + rewrite_trivial_sizeof; rewrite_sizeof; rewrite_defs_remove_vector_concat; rewrite_defs_remove_bitvector_pats; diff --git a/src/util.ml b/src/util.ml index c89cc1ef..335fd36f 100644 --- a/src/util.ml +++ b/src/util.ml @@ -86,6 +86,15 @@ (* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) (**************************************************************************) +let rec last = function + | [x] -> x + | _ :: xs -> last xs + | [] -> raise (Failure "last") + +let rec butlast = function + | [x] -> [] + | x :: xs -> x :: butlast xs + | [] -> [] module Duplicate(S : Set.S) = struct diff --git a/src/util.mli b/src/util.mli index f1182c61..11588de2 100644 --- a/src/util.mli +++ b/src/util.mli @@ -40,6 +40,11 @@ (* SUCH DAMAGE. *) (**************************************************************************) +(* Last element of a list *) +val last : 'a list -> 'a + +val butlast : 'a list -> 'a list + (** Mixed useful things *) module Duplicate(S : Set.S) : sig type dups = |