From 7c8daf8974f5c04bb0dfec257b8aaf976c8d2e66 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 29 Oct 2013 02:39:52 -0700 Subject: [PATCH] fix(kernel/metavar): make sure the justification and substitution are always matching each other Signed-off-by: Leonardo de Moura --- src/kernel/metavar.cpp | 38 ++++++++++++++-------- src/kernel/metavar.h | 9 +++++ src/library/elaborator/elaborator.cpp | 23 +++++-------- tests/lean/elab1.lean.expected.out | 47 ++++++++++++++++++--------- 4 files changed, 74 insertions(+), 43 deletions(-) diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp index 0e795bf88a..5803dbbedc 100644 --- a/src/kernel/metavar.cpp +++ b/src/kernel/metavar.cpp @@ -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(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 metavar_env::get_subst_jst(expr const & m) const { lean_assert(is_metavar(m)); - auto it = const_cast(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 metavar_env::get_subst_jst(name const & m) const { + auto it = const_cast(this)->m_metavar_data.splay_find(m); if (it->m_subst) { if (has_assigned_metavar(it->m_subst, *this)) { buffer 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 { diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h index a2a9696d2b..0bcaadf4f5 100644 --- a/src/kernel/metavar.h +++ b/src/kernel/metavar.h @@ -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 get_subst_jst(name const & m) const; + std::pair get_subst_jst(expr const & m) const; + /** \brief Return the justification for an assigned metavariable. \pre is_metavar(m) diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index 6bb58ea21b..90549c2056 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -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 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); diff --git a/tests/lean/elab1.lean.expected.out b/tests/lean/elab1.lean.expected.out index b4b6fde460..0ced617cff 100644 --- a/tests/lean/elab1.lean.expected.out +++ b/tests/lean/elab1.lean.expected.out @@ -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