From 2a6f3b8e42a4cb4cececb79a9011346b5b25ce80 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 22 Aug 2017 17:31:48 +0100
Subject: Add option to dump monomorphised ast before (re-)typechecking

---
 src/process_file.ml  | 3 +++
 src/process_file.mli | 1 +
 src/sail.ml          | 3 +++
 3 files changed, 7 insertions(+)

(limited to 'src')

diff --git a/src/process_file.ml b/src/process_file.ml
index 1c133ce8..f445f900 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -108,8 +108,11 @@ let check_ast (defs : unit Ast.defs) : Type_check.tannot Ast.defs * Type_check.E
   let () = if !opt_just_check then exit 0 else () in
   (ast, env)
 
+let opt_ddump_raw_mono_ast = ref false
+
 let monomorphise_ast locs ast =
   let ast = Monomorphise.split_defs locs ast in
+  let () = if !opt_ddump_raw_mono_ast then Pretty_print.pp_defs stdout ast else () in
   let ienv = Type_check.Env.no_casts Type_check.initial_env in
   Type_check.check ienv ast
 
diff --git a/src/process_file.mli b/src/process_file.mli
index cd867b0d..5bcd9e03 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -56,6 +56,7 @@ 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
+val opt_ddump_raw_mono_ast : bool ref
 
 type out_type =
   | Lem_ast_out
diff --git a/src/sail.ml b/src/sail.ml
index dbc0eff4..7f46293f 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -88,6 +88,9 @@ let options = Arg.align ([
       | [fname;line;var] -> opt_mono_split := ((fname,int_of_string line),var)::!opt_mono_split
       | _ -> raise (Arg.Bad (s ^ " not of form <filename>:<line>:<variable>"))),
       "<filename>:<line>:<variable> to case split for monomorphisation");
+  ( "-ddump_raw_mono_ast",
+    Arg.Set opt_ddump_raw_mono_ast,
+    " (debug) dump the monomorphised ast before type-checking");
   ( "-new_parser",
     Arg.Set Process_file.opt_new_parser,
     " (experimental) use new parser");
-- 
cgit v1.2.3