From 2c6d4d2225035eef958880f982be05c145e2fa53 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 29 Oct 2013 02:11:06 -0700 Subject: [PATCH] fix(kernel/normalizer): do not apply substitutions in the normalizer It is incorrect to apply substitutions during normalization. The problem is that we do not have support for tracking justifications in the normalizer. So, substitutions were being silently applied during normalization. Thus, the correctness of the conflict resolution in the elaboration was being affected. Signed-off-by: Leonardo de Moura --- src/kernel/normalizer.cpp | 35 ++------- src/kernel/normalizer.h | 5 +- src/kernel/type_checker.cpp | 2 +- src/library/elaborator/elaborator.cpp | 2 +- src/library/type_inferer.cpp | 2 +- tests/lean/elab1.lean.expected.out | 105 ++++++++++++++++---------- 6 files changed, 78 insertions(+), 73 deletions(-) diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp index ae84649cf5..240e3b861d 100644 --- a/src/kernel/normalizer.cpp +++ b/src/kernel/normalizer.cpp @@ -71,8 +71,6 @@ class normalizer::imp { environment const & m_env; context m_ctx; - metavar_env const * m_menv; - unsigned m_menv_timestamp; cache m_cache; unsigned m_max_depth; unsigned m_depth; @@ -193,11 +191,7 @@ class normalizer::imp { svalue r; switch (a.kind()) { case expr_kind::MetaVar: - if (m_menv && m_menv->is_assigned(a)) { - r = normalize(m_menv->get_subst(a), s, k); - } else { - r = svalue(updt_metavar(a, s, k)); - } + r = svalue(updt_metavar(a, s, k)); break; case expr_kind::Var: r = lookup(s, var_idx(a)); @@ -295,38 +289,21 @@ class normalizer::imp { } } - void set_menv(metavar_env const * menv) { - if (m_menv == menv) { - // Check whether m_menv has been updated since the last time the normalizer has been invoked - if (m_menv && m_menv->get_timestamp() > m_menv_timestamp) { - m_menv_timestamp = m_menv->get_timestamp(); - m_cache.clear(); - } - } else { - m_menv = menv; - m_cache.clear(); - m_menv_timestamp = m_menv ? m_menv->get_timestamp() : 0; - } - } - public: imp(environment const & env, unsigned max_depth): m_env(env) { m_interrupted = false; m_max_depth = max_depth; m_depth = 0; - m_menv = nullptr; - m_menv_timestamp = 0; } - expr operator()(expr const & e, context const & ctx, metavar_env const * menv) { + expr operator()(expr const & e, context const & ctx) { set_ctx(ctx); - set_menv(menv); unsigned k = m_ctx.size(); return reify(normalize(e, value_stack(), k), k); } - void clear() { m_ctx = context(); m_cache.clear(); m_menv = nullptr; m_menv_timestamp = 0; } + void clear() { m_ctx = context(); m_cache.clear(); } void set_interrupt(bool flag) { m_interrupted = flag; } }; @@ -334,12 +311,12 @@ normalizer::normalizer(environment const & env, unsigned max_depth):m_ptr(new im normalizer::normalizer(environment const & env):normalizer(env, std::numeric_limits::max()) {} normalizer::normalizer(environment const & env, options const & opts):normalizer(env, get_normalizer_max_depth(opts)) {} normalizer::~normalizer() {} -expr normalizer::operator()(expr const & e, context const & ctx, metavar_env const * menv) { return (*m_ptr)(e, ctx, menv); } +expr normalizer::operator()(expr const & e, context const & ctx) { return (*m_ptr)(e, ctx); } void normalizer::clear() { m_ptr->clear(); } void normalizer::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); } -expr normalize(expr const & e, environment const & env, context const & ctx, metavar_env const * menv) { - return normalizer(env)(e, ctx, menv); +expr normalize(expr const & e, environment const & env, context const & ctx) { + return normalizer(env)(e, ctx); } } diff --git a/src/kernel/normalizer.h b/src/kernel/normalizer.h index 0f612668a7..bb76ae9bab 100644 --- a/src/kernel/normalizer.h +++ b/src/kernel/normalizer.h @@ -13,7 +13,6 @@ Author: Leonardo de Moura namespace lean { class environment; class options; -class metavar_env; /** \brief Functional object for normalizing expressions */ class normalizer { class imp; @@ -24,7 +23,7 @@ public: normalizer(environment const & env, options const & opts); ~normalizer(); - expr operator()(expr const & e, context const & ctx = context(), metavar_env const * menv = nullptr); + expr operator()(expr const & e, context const & ctx = context()); void clear(); @@ -33,5 +32,5 @@ public: void reset_interrupt() { set_interrupt(false); } }; /** \brief Normalize \c e using the environment \c env and context \c ctx */ -expr normalize(expr const & e, environment const & env, context const & ctx = context(), metavar_env const * menv = nullptr); +expr normalize(expr const & e, environment const & env, context const & ctx = context()); } diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 97ad116aa9..d379a9cc6e 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -32,7 +32,7 @@ class type_checker::imp { volatile bool m_interrupted; expr normalize(expr const & e, context const & ctx) { - return m_normalizer(e, ctx, m_menv); + return m_normalizer(e, ctx); } expr lookup(context const & c, unsigned i) { diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index 11f1ca64c4..6bb58ea21b 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -504,7 +504,7 @@ class elaborator::imp { } expr normalize(context const & ctx, expr const & a) { - return m_normalizer(a, ctx, &(m_state.m_menv)); + return m_normalizer(a, ctx); } void process_app(context const & ctx, expr & a) { diff --git a/src/library/type_inferer.cpp b/src/library/type_inferer.cpp index 6c3953e795..0ada71aa3e 100644 --- a/src/library/type_inferer.cpp +++ b/src/library/type_inferer.cpp @@ -32,7 +32,7 @@ class type_inferer::imp { volatile bool m_interrupted; expr normalize(expr const & e, context const & ctx) { - return m_normalizer(e, ctx, m_menv); + return m_normalizer(e, ctx); } expr check_type(expr const & e, expr const & s, context const & ctx) { diff --git a/tests/lean/elab1.lean.expected.out b/tests/lean/elab1.lean.expected.out index dbdbf4af0f..b4b6fde460 100644 --- a/tests/lean/elab1.lean.expected.out +++ b/tests/lean/elab1.lean.expected.out @@ -138,9 +138,9 @@ A : Type, B : Type, a : ?M3::0, b : ?M3::1, C : Type ⊢ ?M3::0[lift:0:3] ≺ C Error (line: 20, pos: 28) unexpected metavariable occurrence Failed to solve ⊢ b ≈ a - Destruct/Decompose - ⊢ b = b ≺ a = ?M3::3 - Normalize + Substitution + ⊢ b ≈ ?M3::2 + Destruct/Decompose ⊢ b = b ≺ ?M3::2 = ?M3::3 (line: 22: pos: 22) Type of argument 6 must be convertible to the expected type in the application of Trans::explicit @@ -151,6 +151,19 @@ Failed to solve ?M3::3 Refl a Refl b + Assignment + ⊢ a ≈ ?M3::2 + Destruct/Decompose + ⊢ a = a ≺ ?M3::1 = ?M3::2 + (line: 22: pos: 22) Type of argument 5 must be convertible to the expected type in the application of + Trans::explicit + with arguments: + ?M3::0 + ?M3::1 + ?M3::2 + ?M3::3 + Refl a + Refl b Failed to solve ⊢ (?M3::0 ≈ Type) ⊕ (?M3::0 ≈ Type 1) ⊕ (?M3::0 ≈ Type 2) ⊕ (?M3::0 ≈ Type M) ⊕ (?M3::0 ≈ Type U) Destruct/Decompose @@ -560,51 +573,67 @@ a : Bool, b : Bool, H : ?M3::2, H_na : ?M3::7 ⊢ a ≺ if Bool (if Bool a b ⊤ a : Bool, b : Bool, H : ?M3::2, H_na : ?M3::7 ⊢ a ≈ ?M3::8 Destruct/Decompose a : Bool, b : Bool, H : ?M3::2, H_na : ?M3::7 ⊢ if Bool a b ⊤ ≈ if Bool ?M3::8 ?M3::9 ⊤ - Destruct/Decompose - a : Bool, - b : Bool, - H : ?M3::2, - H_na : ?M3::7 ⊢ - if Bool (if Bool a b ⊤) a ⊤ ≺ if Bool (if Bool ?M3::8 ?M3::9 ⊤) ?M3::11 ⊤ - Normalize - a : Bool, - b : Bool, - H : ?M3::2, - H_na : ?M3::7 ⊢ - (a ⇒ b) ⇒ a ≺ if Bool ?M3::10 ?M3::11 ⊤ - Substitution + Normalize + a : Bool, b : Bool, H : ?M3::2, H_na : ?M3::7 ⊢ if Bool a b ⊤ ≈ ?M3::8 ⇒ ?M3::9 + Substitution + a : Bool, b : Bool, H : ?M3::2, H_na : ?M3::7 ⊢ if Bool a b ⊤ ≈ ?M3::10 + Destruct/Decompose a : Bool, b : Bool, H : ?M3::2, H_na : ?M3::7 ⊢ - ?M3::2[lift:0:2] ≺ if Bool ?M3::10 ?M3::11 ⊤ + if Bool (if Bool a b ⊤) a ⊤ ≺ if Bool ?M3::10 ?M3::11 ⊤ Normalize a : Bool, b : Bool, H : ?M3::2, H_na : ?M3::7 ⊢ - ?M3::2[lift:0:2] ≺ ?M3::10 ⇒ ?M3::11 - (line: 29: pos: 48) Type of argument 3 must be convertible to the expected type in the application of - MT::explicit + (a ⇒ b) ⇒ a ≺ if Bool ?M3::10 ?M3::11 ⊤ + Substitution + a : Bool, + b : Bool, + H : ?M3::2, + H_na : ?M3::7 ⊢ + ?M3::2[lift:0:2] ≺ if Bool ?M3::10 ?M3::11 ⊤ + Normalize + a : Bool, + b : Bool, + H : ?M3::2, + H_na : ?M3::7 ⊢ + ?M3::2[lift:0:2] ≺ ?M3::10 ⇒ ?M3::11 + (line: 29: pos: 48) Type of argument 3 must be convertible to the expected type in the application of + MT::explicit + with arguments: + ?M3::10 + ?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)) + Assignment + a : Bool, b : Bool, H : ?M3::2, H_na : ?M3::7 ⊢ ?M3::10 ≈ ?M3::8 ⇒ ?M3::9 + Destruct/Decompose + a : Bool, b : Bool, H : ?M3::2, H_na : ?M3::7 ⊢ ¬ ?M3::10 ≺ ¬ (?M3::8 ⇒ ?M3::9) + (line: 29: pos: 40) Type of argument 3 must be convertible to the expected type in the application of + NotImp1::explicit with arguments: - ?M3::10 - ?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)) + ?M3::8 + ?M3::9 + MT H H_na Assignment a : Bool, b : Bool, H : ?M3::2 ⊢ if Bool (if Bool a b ⊤) a ⊤ ≺ ?M3::5 Normalize