Refactor: Change AST type from a union to a struct

1 files changed, 20 insertions, 21 deletions

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)