max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(compiler/vm_compiler): only compile computable non-builtin definitions

Browse source
This commit is contained in:
Gabriel Ebner 2017-01-04 19:48:01 +01:00 • committed by Leonardo de Moura
parent 96398500b6
commit 9435762643
3 changed files with 13 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/frontends/lean/definition_cmds.cpp
View file

@ -319,13 +319,10 @@ static void check_noncomputable(bool ignore_noncomputable, environment const & e
}
}
static environment compile_decl(parser & p, environment const & env, def_cmd_kind kind, bool is_noncomputable,
static environment compile_decl(parser & p, environment const & env,
name const & c_name, name const & c_real_name, pos_info const & pos) {
if (is_noncomputable || kind == Theorem || kind == Example || is_vm_builtin_function(c_real_name))
return env;
try {
declaration d = env.get(c_real_name);
return vm_compile(env, d);
return vm_compile(env, env.get(c_real_name));
} catch (exception & ex) {
if (p.found_errors())
return env;
@ -379,7 +376,7 @@ declare_definition(parser & p, environment const & env, def_cmd_kind kind, buffe
}
new_env = attrs.apply(new_env, p.ios(), c_real_name);
new_env = compile_decl(p, new_env, kind, modifiers.m_is_noncomputable, c_name, c_real_name, pos);
new_env = compile_decl(p, new_env, c_name, c_real_name, pos);
if (doc_string) {
new_env = add_doc_string(new_env, c_real_name, *doc_string);
}

5
src/library/compiler/vm_compiler.cpp
View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "library/noncomputable.h"
#include "util/fresh_name.h"
#include "util/sstream.h"
#include "kernel/instantiate.h"
@ -399,7 +400,9 @@ static environment vm_compile(environment const & env, buffer<procedure> const &
}
environment vm_compile(environment const & env, declaration const & d) {
if (!d.is_definition()) return env;
if (!d.is_definition() || d.is_theorem() || is_noncomputable(env, d.get_name()) || is_vm_builtin_function(d.get_name()))
return env;
buffer<procedure> procs;
preprocess(env, d, procs);
return vm_compile(env, procs);

15
src/library/equations_compiler/util.cpp
View file

@ -292,15 +292,12 @@ pair<environment, expr> mk_aux_definition(environment const & env, options const
} catch (exception & ex) {
throw_mk_aux_definition_error(lctx, c, new_type, new_value, ex);
}
if (!header.m_is_lemma && !header.m_is_noncomputable) {
try {
declaration d = new_env.get(new_c);
new_env = vm_compile(new_env, d);
} catch (exception & ex) {
if (!header.m_prev_errors) {
throw nested_exception(sstream() << "equation compiler failed to generate bytecode for "
<< "auxiliary declaration '" << c << "'", ex);
}
try {
new_env = vm_compile(new_env, new_env.get(new_c));
} catch (exception & ex) {
if (!header.m_prev_errors) {
throw nested_exception(sstream() << "equation compiler failed to generate bytecode for "
<< "auxiliary declaration '" << c << "'", ex);
}
}
return mk_pair(new_env, r);