From 70041bf43f52a030493c1286f9cf6ceb2e9dfecb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 30 Sep 2018 09:48:37 -0700 Subject: [PATCH] feat(library/compiler/vm_compiler): add option `codegen` --- src/library/compiler/vm_compiler.cpp | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/library/compiler/vm_compiler.cpp b/src/library/compiler/vm_compiler.cpp index 0975c9adac..5308fa3edd 100644 --- a/src/library/compiler/vm_compiler.cpp +++ b/src/library/compiler/vm_compiler.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include "runtime/sstream.h" #include "util/fresh_name.h" +#include "util/sexpr/option_declarations.h" #include "kernel/instantiate.h" #include "library/sorry.h" #include "library/noncomputable.h" @@ -365,7 +366,11 @@ static environment vm_compile(environment const & env, buffer const & return new_env; } -environment vm_compile(environment const & env, options const &, buffer const & ds, bool optimize_bytecode) { +static name * g_codegen = nullptr; + +environment vm_compile(environment const & env, options const & opts, buffer const & ds, bool optimize_bytecode) { + if (!opts.get_bool(*g_codegen, true)) + return env; for (constant_info const & info : ds) { if (!info.is_definition() || is_noncomputable(env, info.get_name()) || is_vm_builtin_function(info.get_name())) return env; @@ -386,9 +391,12 @@ void initialize_vm_compiler() { register_name_generator_prefix(*g_vm_compiler_fresh); register_trace_class({"compiler", "optimize_bytecode"}); register_trace_class({"compiler", "code_gen"}); + g_codegen = new name("codegen"); + register_bool_option(*g_codegen, true, "(compiler) enable/disable code generation"); } void finalize_vm_compiler() { + delete g_codegen; delete g_vm_compiler_fresh; } }