diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_lem.ml | 4 | ||||
| -rw-r--r-- | src/pretty_print_sail.ml | 20 | ||||
| -rw-r--r-- | src/process_file.ml | 10 | ||||
| -rw-r--r-- | src/rewriter.ml | 77 | ||||
| -rw-r--r-- | src/rewriter.mli | 4 |
5 files changed, 73 insertions, 42 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index b97845fd..c74cceb9 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -1516,7 +1516,9 @@ let doc_dec_lem sequential (DEC_aux (reg, ((l, _) as annot))) = let doc_spec_lem mwords (VS_aux (valspec,annot)) = empty -let rec doc_def_lem sequential mwords def = match def with +let rec doc_def_lem sequential mwords def = + (* let _ = Pretty_print_sail.pp_defs stderr (Defs [def]) in *) + match def with | DEF_spec v_spec -> (doc_spec_lem mwords v_spec,empty) | DEF_overload _ -> (empty,empty) | DEF_type t_def -> (group (doc_typdef_lem sequential mwords t_def) ^/^ hardline,empty) diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index 0f8e482a..d346c801 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -177,7 +177,8 @@ let doc_exp, doc_let = and starstar_exp ((E_aux(e,_)) as expr) = match e with | E_app_infix(l,(Id_aux(Id "**",_) as op),r) -> doc_op (doc_id op) (starstar_exp l) (app_exp r) - | E_if _ | E_for _ | E_loop _ | E_let _ -> right_atomic_exp expr + | E_if _ | E_for _ | E_loop _ | E_let _ + | E_internal_let _ | E_internal_plet _ -> right_atomic_exp expr | _ -> app_exp expr and right_atomic_exp ((E_aux(e,_)) as expr) = match e with (* Special case: omit "else ()" when the else branch is empty. *) @@ -208,6 +209,18 @@ let doc_exp, doc_let = )) ^/^ exp exp4 | E_let(leb,e) -> doc_op (string "in") (let_exp leb) (exp e) + | E_internal_let (lexp, exp1, exp2) -> + let le = + prefix 2 1 + (separate space [string "internal_let"; doc_lexp lexp; equals]) + (exp exp1) in + doc_op (string "in") le (exp exp2) + | E_internal_plet (pat, exp1, exp2) -> + let le = + prefix 2 1 + (separate space [string "internal_plet"; doc_pat pat; equals]) + (exp exp1) in + doc_op (string "in") le (exp exp2) | _ -> group (parens (exp expr)) and app_exp ((E_aux(e,_)) as expr) = match e with | E_app(f,args) -> @@ -303,6 +316,7 @@ let doc_exp, doc_let = | E_app (_, _)|E_vector_access (_, _)|E_vector_subrange (_, _, _) | E_cons (_, _)|E_field (_, _)|E_assign (_, _) | E_if _ | E_for _ | E_loop _ | E_let _ + | E_internal_let _ | E_internal_plet _ | E_vector_append _ | E_app_infix (_, (* for every app_infix operator caught at a higher precedence, @@ -346,8 +360,8 @@ let doc_exp, doc_let = | E_internal_exp_user _ -> raise (Reporting_basic.err_unreachable Unknown ("internal_exp_user not rewritten away")) | E_internal_cast ((_, Overload (_, _,_ )), _) | E_internal_exp _ -> assert false *) - | E_internal_let (lexp, exp1, exp2) -> - separate space [string "internal let"; doc_lexp lexp; equals; exp exp1; string "in"; exp exp2] + | E_internal_return exp1 -> + separate space [string "internal_return"; exp exp1] | _ -> failwith ("Cannot print: " ^ Ast_util.string_of_exp expr) and let_exp (LB_aux(lb,_)) = match lb with | LB_val(pat,e) -> diff --git a/src/process_file.ml b/src/process_file.ml index f176f198..8d23fcd2 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -234,12 +234,16 @@ let output libpath out_arg files = output1 libpath out_arg f defs) files -let rewrite_step defs rewriter = +let rewrite_step defs (name,rewriter) = let defs = rewriter defs in let _ = match !(opt_ddump_rewrite_ast) with | Some (f, i) -> begin - output "" Lem_ast_out [f ^ "_rewrite_" ^ string_of_int i ^ ".sail",defs]; + let filename = f ^ "_rewrite_" ^ string_of_int i ^ "_" ^ name ^ ".sail" in + output "" Lem_ast_out [filename, defs]; + let ((ot,_, _) as ext_ot) = open_output_with_check_unformatted filename in + Pretty_print_sail.pp_defs ot defs; + close_output_with_check ext_ot; opt_ddump_rewrite_ast := Some (f, i + 1) end | _ -> () in @@ -251,6 +255,6 @@ let rewrite rewriters defs = prerr_endline (Type_check.string_of_type_error err); exit 1 -let rewrite_ast = rewrite [Rewriter.rewrite_defs] +let rewrite_ast = rewrite [("initial", Rewriter.rewrite_defs)] let rewrite_ast_lem = rewrite Rewriter.rewrite_defs_lem let rewrite_ast_ocaml = rewrite Rewriter.rewrite_defs_ocaml diff --git a/src/rewriter.ml b/src/rewriter.ml index 82ebaec5..93aed0e1 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -1114,7 +1114,10 @@ let rewrite_sizeof (Defs defs) = if Bindings.mem f param_map then (* Retrieve instantiation of the type variables of the called function for the given parameters in the original environment *) - let inst = instantiation_of orig_exp in + let inst = + try instantiation_of orig_exp with + | Type_error (l, err) -> + raise (Reporting_basic.err_typ l (string_of_type_error err)) in (* Rewrite the inst using orig_kid so that each type variable has it's original name rather than a mangled typechecker name *) let inst = KBindings.fold (fun kid uvar b -> KBindings.add (orig_kid kid) uvar b) inst KBindings.empty in @@ -1125,7 +1128,9 @@ let rewrite_sizeof (Defs defs) = match uvar with | Some (U_nexp nexp) -> let sizeof = E_aux (E_sizeof nexp, (l, Some (env, atom_typ nexp, no_effect))) in - rewrite_trivial_sizeof_exp sizeof + (try rewrite_trivial_sizeof_exp sizeof with + | Type_error (l, err) -> + raise (Reporting_basic.err_typ l (string_of_type_error err))) (* If the type variable is Not_found then it was probably introduced by a P_var pattern, so it likely exists as a variable in scope. It can't be an existential because the assert rules that out. *) @@ -2532,12 +2537,17 @@ let rewrite_tuple_assignments defs = let env = env_of_annot annot in match e_aux with | E_assign (LEXP_aux (LEXP_tup lexps, _), exp) -> + (* let _ = Pretty_print_common.print stderr (Pretty_print_sail.doc_exp (E_aux (e_aux, annot))) in *) let (_, ids) = List.fold_left (fun (n, ids) _ -> (n + 1, ids @ [mk_id ("tup__" ^ string_of_int n)])) (0, []) lexps in let block_assign i lexp = mk_exp (E_assign (strip_lexp lexp, mk_exp (E_id (mk_id ("tup__" ^ string_of_int i))))) in let block = mk_exp (E_block (List.mapi block_assign lexps)) in let letbind = mk_letbind (mk_pat (P_tup (List.map (fun id -> mk_pat (P_id id)) ids))) (strip_exp exp) in let let_exp = mk_exp (E_let (letbind, block)) in - check_exp env let_exp unit_typ + begin + try check_exp env let_exp unit_typ with + | Type_error (l, err) -> + raise (Reporting_basic.err_typ l (string_of_type_error err)) + end | _ -> E_aux (e_aux, annot) in let assign_exp = { @@ -2868,7 +2878,9 @@ 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 + let rewrite_def rewriters def = + (* let _ = Pretty_print_sail.pp_defs stderr (Defs [def]) in *) + match def with | DEF_val (LB_aux (lb, annot)) -> let rewrap lb = DEF_val (LB_aux (lb, annot)) in begin @@ -3356,36 +3368,35 @@ let rewrite_defs_remove_e_assign = let recheck_defs defs = fst (check initial_env defs) -let rewrite_defs_lem =[ - top_sort_defs; - rewrite_trivial_sizeof; - rewrite_sizeof; - rewrite_defs_remove_vector_concat; - rewrite_defs_remove_bitvector_pats; - rewrite_defs_guarded_pats; - (* recheck_defs; *) - rewrite_defs_early_return; - rewrite_defs_exp_lift_assign; - rewrite_defs_remove_blocks; - rewrite_defs_letbind_effects; - rewrite_defs_remove_e_assign; - rewrite_defs_effectful_let_expressions; - rewrite_defs_remove_superfluous_letbinds; - rewrite_defs_remove_superfluous_returns +let rewrite_defs_lem = [ + ("top_sort_defs", top_sort_defs); + ("trivial_sizeof", rewrite_trivial_sizeof); + ("sizeof", rewrite_sizeof); + ("remove_vector_concat", rewrite_defs_remove_vector_concat); + ("remove_bitvector_pats", rewrite_defs_remove_bitvector_pats); + ("guarded_pats", rewrite_defs_guarded_pats); + (* ("recheck_defs", recheck_defs); *) + ("early_return", rewrite_defs_early_return); + ("exp_lift_assign", rewrite_defs_exp_lift_assign); + ("remove_blocks", rewrite_defs_remove_blocks); + ("letbind_effects", rewrite_defs_letbind_effects); + ("remove_e_assign", rewrite_defs_remove_e_assign); + ("effectful_let_expressions", rewrite_defs_effectful_let_expressions); + ("remove_superfluous_letbinds", rewrite_defs_remove_superfluous_letbinds); + ("remove_superfluous_returns", rewrite_defs_remove_superfluous_returns) ] let rewrite_defs_ocaml = [ - (* top_sort_defs; *) - rewrite_undefined; - rewrite_tuple_assignments; - rewrite_simple_assignments; - rewrite_defs_remove_vector_concat; - rewrite_constraint; - rewrite_trivial_sizeof; - rewrite_sizeof; - rewrite_simple_types; - rewrite_overload_cast; - rewrite_defs_exp_lift_assign; - (* rewrite_defs_exp_lift_assign *) - (* rewrite_defs_separate_numbs *) + (* ("top_sort_defs", top_sort_defs); *) + ("undefined", rewrite_undefined); + ("tuple_assignments", rewrite_tuple_assignments); + ("simple_assignments", rewrite_simple_assignments); + ("remove_vector_concat", rewrite_defs_remove_vector_concat); + ("constraint", rewrite_constraint); + ("trivial_sizeof", rewrite_trivial_sizeof); + ("sizeof", rewrite_sizeof); + ("simple_types", rewrite_simple_types); + ("overload_cast", rewrite_overload_cast); + ("exp_lift_assign", rewrite_defs_exp_lift_assign); + (* ("separate_numbs", rewrite_defs_separate_numbs) *) ] diff --git a/src/rewriter.mli b/src/rewriter.mli index 4b667793..1c3e8fae 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -56,8 +56,8 @@ type 'a rewriters = { rewrite_exp : 'a rewriters -> 'a exp -> 'a exp; val rewrite_exp : tannot rewriters -> tannot exp -> tannot exp val rewrite_defs : tannot defs -> tannot defs -val rewrite_defs_ocaml : (tannot defs -> tannot defs) list (*Perform rewrites to exclude AST nodes not supported for ocaml out*) -val rewrite_defs_lem : (tannot defs -> tannot defs) list (*Perform rewrites to exclude AST nodes not supported for lem out*) +val rewrite_defs_ocaml : (string * (tannot defs -> tannot defs)) list (*Perform rewrites to exclude AST nodes not supported for ocaml out*) +val rewrite_defs_lem : (string * (tannot defs -> tannot defs)) list (*Perform rewrites to exclude AST nodes not supported for lem out*) (* the type of interpretations of pattern-matching expressions *) type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg = |