michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/definitional/equations): bug when compiling in proof relevant kernels

Browse source
This commit is contained in:
Leonardo de Moura 2015-01-02 23:17:33 -08:00
parent 92b6c06a21
commit 21a9cd58a3
1 changed files with 12 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/library/definitional/equations.cpp
View file

@ -235,6 +235,7 @@ class equation_compiler_fn {
expr whnf(expr const & e) { return m_tc.whnf(e).first; } expr whnf(expr const & e) { return m_tc.whnf(e).first; }
expr infer_type(expr const & e) { return m_tc.infer(e).first; } expr infer_type(expr const & e) { return m_tc.infer(e).first; }
bool is_def_eq(expr const & e1, expr const & e2) { return m_tc.is_def_eq(e1, e2).first; } bool is_def_eq(expr const & e1, expr const & e2) { return m_tc.is_def_eq(e1, e2).first; }
bool is_proof_irrelevant() const { return m_tc.env().prop_proof_irrel(); }
optional<name> is_constructor(expr const & e) const { optional<name> is_constructor(expr const & e) const {
if (!is_constant(e)) if (!is_constant(e))
@ -325,6 +326,8 @@ class equation_compiler_fn {
} }
program(program const & p, list<optional<name>> const & new_s, list<eqn> const & new_e): program(program const & p, list<optional<name>> const & new_s, list<eqn> const & new_e):
program(p.m_fn, p.m_context, new_s, new_e, p.m_type) {} program(p.m_fn, p.m_context, new_s, new_e, p.m_type) {}
program(program const & p, list<expr> const & ctx):
program(p.m_fn, ctx, p.m_var_stack, p.m_eqns, p.m_type) {}
program() {} program() {}
expr const & get_var(name const & n) const { expr const & get_var(name const & n) const {
for (expr const & v : m_context) { for (expr const & v : m_context) {
@ -796,8 +799,15 @@ class equation_compiler_fn {
expr compile(program const & p) { expr compile(program const & p) {
buffer<expr> vars; buffer<expr> vars;
to_buffer(p.m_context, vars); to_buffer(p.m_context, vars);
expr r = compile_core(p); if (!is_proof_irrelevant()) {
return Fun(vars, r); // We have to include the global context because the proof relevant version
// uses the class-instance resolution, and must be able to "see" the complete
// context.
program new_p(p, append(to_list(m_global_context), p.m_context));
return Fun(vars, compile_core(new_p));
} else {
return Fun(vars, compile_core(p));
}
} }
/** \brief Return true iff \c e is one of the functions being defined */ /** \brief Return true iff \c e is one of the functions being defined */