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

fix(kernel/metavar): make sure the justification and substitution are always matching each other

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-10-29 02:39:52 -07:00
parent 2c6d4d2225
commit 7c8daf8974
4 changed files with 74 additions and 43 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

38
src/kernel/metavar.cpp
View file

@ -141,9 +141,7 @@ justification metavar_env::get_justification(expr const & m) const {
}
justification metavar_env::get_justification(name const & m) const {
auto it = const_cast<metavar_env*>(this)->m_metavar_data.splay_find(m);
lean_assert(it);
return it->m_justification;
return get_subst_jst(m).second;
}
bool metavar_env::is_assigned(name const & m) const {
@ -191,9 +189,22 @@ expr apply_local_context(expr const & a, local_context const & lctx) {
}
}
expr metavar_env::get_subst(expr const & m) const {
std::pair<expr, justification> metavar_env::get_subst_jst(expr const & m) const {
lean_assert(is_metavar(m));
auto it = const_cast<metavar_env*>(this)->m_metavar_data.splay_find(metavar_name(m));
auto p = get_subst_jst(metavar_name(m));
expr r = p.first;
if (p.first) {
local_context const & lctx = metavar_lctx(m);
if (lctx)
r = apply_local_context(r, lctx);
return mk_pair(r, p.second);
} else {
return p;
}
}
std::pair<expr, justification> metavar_env::get_subst_jst(name const & m) const {
auto it = const_cast<metavar_env*>(this)->m_metavar_data.splay_find(m);
if (it->m_subst) {
if (has_assigned_metavar(it->m_subst, *this)) {
buffer<justification> jsts;
@ -204,16 +215,16 @@ expr metavar_env::get_subst(expr const & m) const {
it->m_subst = new_subst;
}
}
local_context const & lctx = metavar_lctx(m);
expr r = it->m_subst;
if (lctx)
r = apply_local_context(r, lctx);
return r;
return mk_pair(it->m_subst, it->m_justification);
} else {
return expr();
return mk_pair(expr(), justification());
}
}
expr metavar_env::get_subst(expr const & m) const {
return get_subst_jst(m).first;
}
class instantiate_metavars_proc : public replace_visitor {
protected:
metavar_env const & m_menv;
@ -226,8 +237,9 @@ protected:
virtual expr visit_metavar(expr const & m, context const & ctx) {
if (is_metavar(m) && m_menv.is_assigned(m)) {
push_back(m_menv.get_justification(m));
expr r = m_menv.get_subst(m);
auto p = m_menv.get_subst_jst(m);
expr r = p.first;
push_back(p.second);
if (has_assigned_metavar(r, m_menv)) {
return visit(r, ctx);
} else {

9
src/kernel/metavar.h
View file

@ -91,6 +91,15 @@ public:
bool has_type(expr const & m) const;
bool has_type(name const & m) const;
/**
\brief Return the substitution and justification for the given metavariable.
If the metavariable is not assigned in this substitution, then it returns the null
expression.
*/
std::pair<expr, justification> get_subst_jst(name const & m) const;
std::pair<expr, justification> get_subst_jst(expr const & m) const;
/**
\brief Return the justification for an assigned metavariable.
\pre is_metavar(m)

23
src/library/elaborator/elaborator.cpp
View file

@ -184,18 +184,11 @@ class elaborator::imp {
return m_state.m_menv.is_assigned(m);
}
/** \brief Return the substitution for an assigned metavariable */
expr get_mvar_subst(expr const & m) const {
/** \brief Return the substitution (and justification) for an assigned metavariable */
std::pair<expr, justification> get_subst_jst(expr const & m) const {
lean_assert(is_metavar(m));
lean_assert(is_assigned(m));
return m_state.m_menv.get_subst(m);
}
/** \brief Return the justification/justification for an assigned metavariable */
justification get_mvar_justification(expr const & m) const {
lean_assert(is_metavar(m));
lean_assert(is_assigned(m));
return m_state.m_menv.get_justification(m);
return m_state.m_menv.get_subst_jst(m);
}
/** \brief Return the type of an metavariable */
@ -396,8 +389,9 @@ class elaborator::imp {
if (is_metavar(a)) {
if (is_assigned(a)) {
// Case 1
justification new_jst(new substitution_justification(c, get_mvar_justification(a)));
push_updated_constraint(c, is_lhs, get_mvar_subst(a), new_jst);
auto s_j = get_subst_jst(a);
justification new_jst(new substitution_justification(c, s_j.second));
push_updated_constraint(c, is_lhs, s_j.first, new_jst);
return Processed;
} else if (!has_local_context(a)) {
// Case 2
@ -433,8 +427,9 @@ class elaborator::imp {
if (is_app(a) && is_metavar(arg(a, 0)) && is_assigned(arg(a, 0))) {
// Case 4
justification new_jst(new substitution_justification(c, get_mvar_justification(arg(a, 0))));
expr new_f = get_mvar_subst(arg(a, 0));
auto s_j = get_subst_jst(arg(a, 0));
justification new_jst(new substitution_justification(c, s_j.second));
expr new_f = s_j.first;
expr new_a = update_app(a, 0, new_f);
if (m_state.m_menv.beta_reduce_metavar_application())
new_a = head_beta_reduce(new_a);

47
tests/lean/elab1.lean.expected.out
View file

@ -608,22 +608,37 @@ a : Bool, b : Bool, H : ?M3::2, H_na : ?M3::7 ⊢ a ≺ if Bool (if Bool a b ⊤
?M3::11
H
H_na
Assignment
a : Bool, b : Bool ⊢ ?M3::2 ≈ ?M3::0
Destruct/Decompose
a : Bool,
b : Bool ⊢
Π H : ?M3::2, ?M3::5 ≺ Π _ : ?M3::0, ?M3::1[lift:0:1]
(line: 27: pos: 4) Type of argument 3 must be convertible to the expected type in the application of
Discharge::explicit
with arguments:
?M3::0
?M3::1
λ H : ?M3::2,
DisjCases
(EM a)
(λ H_a : ?M3::6, H)
(λ H_na : ?M3::7, NotImp1 (MT H H_na))
Normalize assignment
?M3::0
Assignment
a : Bool, b : Bool ⊢ ?M3::2 ≈ ?M3::0
Destruct/Decompose
a : Bool,
b : Bool ⊢
Π H : ?M3::2, ?M3::5 ≺ Π _ : ?M3::0, ?M3::1[lift:0:1]
(line: 27: pos: 4) Type of argument 3 must be convertible to the expected type in the application of
Discharge::explicit
with arguments:
?M3::0
?M3::1
λ H : ?M3::2,
DisjCases
(EM a)
(λ H_a : ?M3::6, H)
(λ H_na : ?M3::7, NotImp1 (MT H H_na))
Assignment
a : Bool, b : Bool ⊢ ?M3::0 ≈ (a ⇒ b) ⇒ a
Destruct/Decompose
a : Bool, b : Bool ⊢ ?M3::0 ⇒ ?M3::1 ≺ ((a ⇒ b) ⇒ a) ⇒ a
Destruct/Decompose
a : Bool ⊢
Π b : Bool, ?M3::0 ⇒ ?M3::1 ≺
Π b : Bool, ((a ⇒ b) ⇒ a) ⇒ a
Destruct/Decompose
⊢
Π a b : Bool, ?M3::0 ⇒ ?M3::1 ≺
Π a b : Bool, ((a ⇒ b) ⇒ a) ⇒ a
(line: 26: pos: 16) Type of definition 'pierce' must be convertible to expected type.
Assignment
a : Bool, b : Bool, H : ?M3::2, H_na : ?M3::7 ⊢ ?M3::10 ≈ ?M3::8 ⇒ ?M3::9
Destruct/Decompose