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

fix(library/compiler/compiler): assertion violations

Browse source
This commit is contained in:
Leonardo de Moura 2019-03-19 10:18:41 -07:00
parent e31e562c79
commit aa56578a29
2 changed files with 16 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/kernel/declaration.h
View file

@ -458,8 +458,13 @@ public:
names const & get_lparams() const { return to_constant_val().get_lparams(); }
unsigned get_num_lparams() const { return length(get_lparams()); }
expr const & get_type() const { return to_constant_val().get_type(); }
bool has_value() const { return is_theorem() || is_definition(); }
expr const & get_value() const { lean_assert(has_value()); return static_cast<expr const &>(cnstr_get_ref(to_val(), 1)); }
bool has_value(bool allow_opaque = false) const {
return is_theorem() || is_definition() || (allow_opaque && is_opaque());
}
expr const & get_value(bool allow_opaque = false) const {
lean_assert(has_value(allow_opaque));
return static_cast<expr const &>(cnstr_get_ref(to_val(), 1));
}
reducibility_hints const & get_hints() const;
axiom_val const & to_axiom_val() const { lean_assert(is_axiom()); return static_cast<axiom_val const &>(to_val()); }

13
src/library/compiler/compiler.cpp
View file

@ -42,8 +42,9 @@ static name get_real_name(name const & n) {
}
static comp_decls to_comp_decls(environment const & env, names const & cs) {
bool allow_opaque = true;
return map2<comp_decl>(cs, [&](name const & n) {
return comp_decl(get_real_name(n), env.get(n).get_value());
return comp_decl(get_real_name(n), env.get(n).get_value(allow_opaque));
});
}
@ -143,6 +144,10 @@ bool is_main_fn_type(expr const & type) {
}
}
static bool has_synthetic_sorry(constant_info const & cinfo) {
return cinfo.is_definition() && has_synthetic_sorry(cinfo.get_value());
}
environment compile(environment const & env, options const & opts, names cs) {
if (!is_codegen_enabled(opts))
return env;
@ -171,9 +176,9 @@ environment compile(environment const & env, options const & opts, names cs) {
for (name const & c : cs) {
lean_assert(!is_extern_constant(env, c));
if ((!env.get(c).is_definition() && !env.get(c).is_opaque()) || has_synthetic_sorry(env.get(c).get_value())) {
return env;
}
constant_info cinfo = env.get(c);
if (!cinfo.is_definition() && !cinfo.is_opaque()) return env;
if (has_synthetic_sorry(cinfo)) return env;
}
comp_decls ds = to_comp_decls(env, cs);