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