diff options
Diffstat (limited to 'src/process_file.ml')
| -rw-r--r-- | src/process_file.ml | 60 |
1 files changed, 33 insertions, 27 deletions
diff --git a/src/process_file.ml b/src/process_file.ml index a0245c8f..d67fba76 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -48,6 +48,7 @@ (* SUCH DAMAGE. *) (**************************************************************************) +open Ast_defs open PPrint open Pretty_print_common @@ -263,10 +264,10 @@ let opt_ddump_tc_ast = ref false let opt_ddump_rewrite_ast = ref None let opt_dno_cast = ref false -let check_ast (env : Type_check.Env.t) (defs : unit Ast.defs) : Type_check.tannot Ast.defs * Type_check.Env.t = +let check_ast (env : Type_check.Env.t) (ast : unit ast) : Type_check.tannot ast * Type_check.Env.t = let env = if !opt_dno_cast then Type_check.Env.no_casts env else env in - let ast, env = Type_error.check env defs in - let () = if !opt_ddump_tc_ast then Pretty_print_sail.pp_defs stdout ast else () in + let ast, env = Type_error.check env ast in + let () = if !opt_ddump_tc_ast then Pretty_print_sail.pp_ast stdout ast else () in let () = if !opt_just_check then exit 0 else () in (ast, env) @@ -274,9 +275,15 @@ let load_files ?check:(check=false) options type_envs files = if !opt_memo_z3 then Constraint.load_digests () else (); let t = Profile.start () in - let ast = Parse_ast.Defs (List.map (fun f -> (f, parse_file f |> snd |> preprocess options)) files) in + + let parsed_files = List.map (fun f -> (f, parse_file f)) files in + + let comments = List.map (fun (f, (comments, _)) -> (f, comments)) parsed_files in + let ast = Parse_ast.Defs (List.map (fun (f, (_, file_ast)) -> (f, preprocess options file_ast)) parsed_files) in let ast = Initial_check.process_ast ~generate:(not check) ast in - let () = if !opt_ddump_initial_ast then Pretty_print_sail.pp_defs stdout ast else () in + let ast = { ast with comments = comments } in + + let () = if !opt_ddump_initial_ast then Pretty_print_sail.pp_ast stdout ast else () in begin match !opt_reformat with | Some dir -> @@ -329,7 +336,7 @@ let close_output_with_check (o, temp_file_name, opt_dir, file_name) = let generated_line f = Printf.sprintf "Generated by Sail from %s." f -let output_lem filename libs type_env defs = +let output_lem filename libs type_env ast = let generated_line = generated_line filename in (* let seq_suffix = if !Pretty_print_lem.opt_sequential then "_sequential" else "" in *) let types_module = (filename ^ "_types") in @@ -357,7 +364,7 @@ let output_lem filename libs type_env defs = string (" " ^ String.capitalize_ascii filename); string "begin"; string ""; - State.generate_isa_lemmas !Pretty_print_lem.opt_mwords defs; + State.generate_isa_lemmas !Pretty_print_lem.opt_mwords ast.defs; string ""; string "end" ] ^^ hardline @@ -366,10 +373,10 @@ let output_lem filename libs type_env defs = open_output_with_check_unformatted !opt_lem_output_dir (filename ^ "_types" ^ ".lem") in let ((o,_,_,_) as ext_o) = open_output_with_check_unformatted !opt_lem_output_dir (filename ^ ".lem") in - (Pretty_print.pp_defs_lem + (Pretty_print.pp_ast_lem (ot, base_imports) (o, base_imports @ (String.capitalize_ascii types_module :: libs)) - type_env defs generated_line); + type_env ast generated_line); close_output_with_check ext_ot; close_output_with_check ext_o; let ((ol,_,_,_) as ext_ol) = @@ -377,7 +384,7 @@ let output_lem filename libs type_env defs = print ol isa_lemmas; close_output_with_check ext_ol -let output_coq opt_dir filename alt_modules alt_modules2 libs defs = +let output_coq opt_dir filename alt_modules alt_modules2 libs ast = let generated_line = generated_line filename in let types_module = (filename ^ "_types") in let base_imports_default = ["Sail.Base"; "Sail.Real"] in @@ -395,10 +402,10 @@ let output_coq opt_dir filename alt_modules alt_modules2 libs defs = open_output_with_check_unformatted opt_dir (filename ^ "_types" ^ ".v") in let ((o,_,_,_) as ext_o) = open_output_with_check_unformatted opt_dir (filename ^ ".v") in - (Pretty_print_coq.pp_defs_coq + (Pretty_print_coq.pp_ast_coq (ot, base_imports) (o, base_imports @ (types_module :: libs) @ alt_modules2) - defs generated_line) + ast generated_line) (alt_modules2 <> []); (* suppress MR and M defns if alt_modules2 present*) close_output_with_check ext_ot; close_output_with_check ext_o @@ -407,49 +414,48 @@ let rec iterate (f : int -> unit) (n : int) : unit = if n = 0 then () else (f n; iterate f (n - 1)) -let output1 libpath out_arg filename type_env defs = +let output1 libpath out_arg filename type_env ast = let f' = Filename.basename (Filename.chop_extension filename) in match out_arg with | Lem_out libs -> - output_lem f' libs type_env defs + output_lem f' libs type_env ast | Coq_out libs -> - output_coq !opt_coq_output_dir f' !opt_alt_modules_coq !opt_alt_modules2_coq libs defs + output_coq !opt_coq_output_dir f' !opt_alt_modules_coq !opt_alt_modules2_coq libs ast let output libpath out_arg files = List.iter - (fun (f, type_env, defs) -> - output1 libpath out_arg f type_env defs) + (fun (f, type_env, ast) -> + output1 libpath out_arg f type_env ast) files -let rewrite_step n total (defs, env) (name, rewriter) = +let rewrite_step n total (ast, env) (name, rewriter) = let t = Profile.start () in - let defs, env = rewriter env defs in + let ast, env = rewriter env ast in Profile.finish ("rewrite " ^ name) t; let _ = match !(opt_ddump_rewrite_ast) with | Some (f, i) -> begin 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 None filename in - Pretty_print_sail.pp_defs ot defs; + Pretty_print_sail.pp_ast ot ast; close_output_with_check ext_ot; opt_ddump_rewrite_ast := Some (f, i + 1) end | _ -> () in Util.progress "Rewrite " name n total; - defs, env + ast, env -let rewrite env rewriters defs = +let rewrite env rewriters ast = let total = List.length rewriters in - try snd (List.fold_left (fun (n, defsenv) rw -> n + 1, rewrite_step n total defsenv rw) (1, (defs, env)) rewriters) with + try snd (List.fold_left (fun (n, astenv) rw -> n + 1, rewrite_step n total astenv rw) (1, (ast, env)) rewriters) with | Type_check.Type_error (_, l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err)) -let rewrite_ast_initial env = rewrite env [("initial", fun env defs -> Rewriter.rewrite_defs defs, env)] +let rewrite_ast_initial env = rewrite env [("initial", fun env ast -> Rewriter.rewrite_ast ast, env)] -let rewrite_ast_target tgt env = rewrite env (Rewrites.rewrite_defs_target tgt) +let rewrite_ast_target tgt env = rewrite env (Rewrites.rewrite_ast_target tgt) -let rewrite_ast_check env = rewrite env Rewrites.rewrite_defs_check +let rewrite_ast_check env = rewrite env Rewrites.rewrite_ast_check let descatter type_envs ast = let ast = Scattered.descatter ast in |