Add debugging option to dump AST after rewriting steps

5 files changed, 43 insertions, 23 deletions

diff --git a/src/process_file.ml b/src/process_file.ml
index c9a4f178..95562969 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -93,6 +93,7 @@ let load_file order env f =
 let opt_new_typecheck = ref false
 let opt_just_check = ref false
 let opt_ddump_tc_ast = ref false
+let opt_ddump_rewrite_ast = ref None
 let opt_dno_cast = ref false
 
 let check_ast (defs : unit Ast.defs) : Type_check.tannot Ast.defs * Type_check.Env.t =
@@ -107,10 +108,6 @@ let monomorphise_ast locs ast =
   let ienv = Type_check.Env.no_casts Type_check.initial_env in
   Type_check.check ienv ast
 
-let rewrite_ast (defs: Type_check.tannot Ast.defs) = Rewriter.rewrite_defs defs
-let rewrite_ast_lem (defs: Type_check.tannot Ast.defs) = Rewriter.rewrite_defs_lem defs
-let rewrite_ast_ocaml (defs: Type_check.tannot Ast.defs) = Rewriter.rewrite_defs_ocaml defs
-
 let open_output_with_check file_name =
   let (temp_file_name, o) = Filename.open_temp_file "ll_temp" "" in
   let o' = Format.formatter_of_out_channel o in
@@ -230,3 +227,20 @@ let output libpath out_arg files =
     (fun (f, defs) ->
        output1 libpath out_arg f defs)
     files
+
+let rewrite_step defs 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];
+        opt_ddump_rewrite_ast := Some (f, i + 1)
+      end
+    | _ -> () in
+  defs
+
+let rewrite rewriters defs = List.fold_left rewrite_step defs rewriters
+
+let rewrite_ast = rewrite [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/process_file.mli b/src/process_file.mli
index 9907b743..d0dae469 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -54,6 +54,7 @@ val load_file : Ast.order -> Type_check.Env.t -> string -> Type_check.tannot Ast
 val opt_new_typecheck : bool ref
 val opt_just_check : bool ref
 val opt_ddump_tc_ast : bool ref
+val opt_ddump_rewrite_ast : ((string * int) option) ref
 val opt_dno_cast : bool ref
 
 type out_type =
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 8cf682bf..b1f54c5f 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -2136,12 +2136,13 @@ let rewrite_defs_separate_numbs defs = rewrite_defs_base
      rewrite_def = rewrite_def;
      rewrite_defs = rewrite_defs_base} defs*)
 
-let rewrite_defs_ocaml =
-  top_sort_defs >>
-  rewrite_defs_remove_vector_concat >>
-  rewrite_sizeof >>
-  rewrite_defs_exp_lift_assign (* >>
+let rewrite_defs_ocaml = [
+  top_sort_defs;
+  rewrite_defs_remove_vector_concat;
+  rewrite_sizeof;
+  rewrite_defs_exp_lift_assign (* ;
   rewrite_defs_separate_numbs *)
+  ]
 
 let rewrite_defs_remove_blocks =
   let letbind_wild v body =
@@ -2969,17 +2970,18 @@ let rewrite_defs_remove_e_assign =
     }
 
 
-let rewrite_defs_lem =
-  top_sort_defs >>
-  rewrite_sizeof >>
-  rewrite_defs_remove_vector_concat >>
-  rewrite_defs_remove_bitvector_pats >>
-  rewrite_defs_guarded_pats >>
-  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 >>
+let rewrite_defs_lem =[
+  top_sort_defs;
+  rewrite_sizeof;
+  rewrite_defs_remove_vector_concat;
+  rewrite_defs_remove_bitvector_pats;
+  rewrite_defs_guarded_pats;
+  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
+  ]
   
diff --git a/src/rewriter.mli b/src/rewriter.mli
index 473456f6..9c91b55b 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 (*Perform rewrites to exclude AST nodes not supported for ocaml out*)
-val rewrite_defs_lem : tannot defs -> tannot defs (*Perform rewrites to exclude AST nodes not supported for lem out*)
+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*)
 
 (* the type of interpretations of pattern-matching expressions *)
 type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
diff --git a/src/sail.ml b/src/sail.ml
index c7c14a67..b08272cd 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -97,6 +97,9 @@ let options = Arg.align ([
   ( "-ddump_tc_ast",
     Arg.Set opt_ddump_tc_ast,
     " (debug) dump the typechecked ast to stdout");
+  ( "-ddump_rewrite_ast",
+    Arg.String (fun l -> opt_ddump_rewrite_ast := Some (l, 0)),
+    " <prefix> (debug) dump the ast after each rewriting step to <prefix>_<i>.lem");
   ( "-dtc_verbose",
     Arg.Int (fun verbosity -> Type_check.opt_tc_debug := verbosity),
     " (debug) verbose typechecker output: 0 is silent");