Initial rewrite to move complex nexps in fn sigs into constraints

(for monomorphisation, off for now because the analysis needs extended).
Also tighten up orig_nexp, make Lem backend replace # in type variables.

1 files changed, 2 insertions, 0 deletions

diff --git a/src/process_file.ml b/src/process_file.ml
index ffd61fae..e9d04c5b 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -190,6 +190,7 @@ let opt_ddump_raw_mono_ast = ref false
 let opt_dmono_analysis = ref 0
 let opt_auto_mono = ref false
 let opt_mono_rewrites = ref false
+let opt_mono_complex_nexps = ref false
 let opt_dall_split_errors = ref false
 let opt_dmono_continue = ref false
 
@@ -199,6 +200,7 @@ let monomorphise_ast locs type_env ast =
     auto = !opt_auto_mono;
     debug_analysis = !opt_dmono_analysis;
     rewrites = !opt_mono_rewrites;
+    rewrite_toplevel_nexps = !opt_mono_complex_nexps;
     rewrite_size_parameters = !Pretty_print_lem.opt_mwords;
     all_split_errors = !opt_dall_split_errors;
     continue_anyway = !opt_dmono_continue;