[Git][monnier/typer][gambit-compiler-pp] Move simplification behind a flag.
Simon Génier pushed to branch gambit-compiler-pp at Stefan / Typer Commits: e322bbe1 by Simon Génier at 2022-08-26T19:01:42-04:00 Move simplification behind a flag. - - - - - 2 changed files: - src/elab.ml - typer.ml Changes: ===================================== src/elab.ml ===================================== @@ -69,6 +69,7 @@ let parsing_internals = ref false let btl_folder = try Sys.getenv "TYPER_BUILTINS" with Not_found -> "./btl" +let optimize = ref false let fatal ?print_action ?loc fmt = Log.log_fatal ~section:"ELAB" ?print_action ?loc fmt @@ -1997,10 +1998,16 @@ let process_file let pretokens = prelex source in let tokens = lex Grammar.default_stt pretokens in let ldecls, ectx' = lexp_p_decls [] tokens ectx in - let _, ldecls' = - List.fold_left_map Simpl.simpl_ldecls Subst.identity ldecls + let simpl_ldecls = + if !optimize + then + let _, ldecls = + List.fold_left_map Simpl.simpl_ldecls Subst.identity ldecls + in + ldecls + else ldecls in - List.iter backend#process_decls ldecls'; + List.iter backend#process_decls simpl_ldecls; ectx' with | Sys_error _ ===================================== typer.ml ===================================== @@ -45,6 +45,10 @@ let arg_defs = ("-Vmacro-expansion", Arg.Set Elab.macro_tracing_enabled, "Trace macro expansion"); + + ("-O", + Arg.Set Elab.optimize, + "Enable a simplification phase"); ] let parse_args argv usage = View it on GitLab: https://gitlab.com/monnier/typer/-/commit/e322bbe1fddd61f45c9a410cb1661d29cf... -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/e322bbe1fddd61f45c9a410cb1661d29cf... You're receiving this email because of your account on gitlab.com.
Afficher les réponses par date
participants (1)
-
Simon Génier (@ilovemonoids)