From 7441db19749fb7fb9383b6361dfbd99547e53486 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Tue, 29 Sep 2020 16:23:40 +0100 Subject: Refactor: Change AST type from a union to a struct --- src/process_file.ml | 41 ++++++++++++++++++++--------------------- 1 file changed, 20 insertions(+), 21 deletions(-) (limited to 'src/process_file.ml') diff --git a/src/process_file.ml b/src/process_file.ml index 63ea49cc..b121c87c 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -267,7 +267,7 @@ let opt_dno_cast = ref false 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 ast in - let () = if !opt_ddump_tc_ast then Pretty_print_sail.pp_defs stdout ast else () 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) @@ -277,7 +277,7 @@ let load_files ?check:(check=false) options type_envs files = let t = Profile.start () in let ast = Parse_ast.Defs (List.map (fun f -> (f, parse_file f |> snd |> preprocess options)) 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 () = if !opt_ddump_initial_ast then Pretty_print_sail.pp_ast stdout ast else () in begin match !opt_reformat with | Some dir -> @@ -330,7 +330,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 @@ -358,7 +358,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 @@ -370,7 +370,7 @@ let output_lem filename libs type_env defs = (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) = @@ -378,7 +378,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 @@ -396,10 +396,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 @@ -408,45 +408,44 @@ 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_ast 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_ast_target tgt) -- cgit v1.2.3