diff options
Diffstat (limited to 'src/process_file.ml')
| -rw-r--r-- | src/process_file.ml | 14 |
1 files changed, 5 insertions, 9 deletions
diff --git a/src/process_file.ml b/src/process_file.ml index 5eb9f1ee..0601bfab 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -92,23 +92,19 @@ let opt_new_typecheck = ref false let opt_just_check = ref false let opt_ddump_tc_ast = ref false let opt_dno_cast = ref false -let opt_mono_split = ref ([]:((string * int) * string) list) let check_ast (defs : unit Ast.defs) : Type_check.tannot Ast.defs * Type_check.Env.t = let ienv = if !opt_dno_cast then Type_check.Env.no_casts Type_check.initial_env else Type_check.initial_env in let ast, env = Type_check.check ienv defs in - let ast = match !opt_mono_split with - | [] -> ast - | l -> - let ast = Monomorphise.split_defs l ast in - let ienv = Type_check.Env.no_casts Type_check.initial_env in - let ast, _ = Type_check.check ienv ast in - ast - in let () = if !opt_ddump_tc_ast then Pretty_print.pp_defs stdout ast else () in let () = if !opt_just_check then exit 0 else () in (ast, env) +let monomorphise_ast locs ast = + let ast = Monomorphise.split_defs locs ast in + 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 |