diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp index 0a95af03e0..355fc5d258 100644 --- a/src/kernel/normalizer.cpp +++ b/src/kernel/normalizer.cpp @@ -133,7 +133,10 @@ class normalizer::imp { }); } - /** \brief Return true iff the value_stack does affect the context of a metavariable */ + /** + \brief Return true iff the value_stack does not affect the context of a metavariable + See big comment at reify_closure. + */ bool is_identity_stack(value_stack const & s, unsigned k) { unsigned i = 0; for (auto e : s) { @@ -149,9 +152,9 @@ class normalizer::imp { expr const & e = c.get_expr(); context const & ctx = c.get_context(); value_stack const & s = c.get_stack(); - freset reset(m_cache); - flet set(m_ctx, ctx); if (is_abstraction(e)) { + freset reset(m_cache); + flet set(m_ctx, ctx); return update_abst(e, [&](expr const & d, expr const & b) { expr new_d = reify(normalize(d, s, k), k); m_cache.clear(); // make sure we do not reuse cached values from the previous call @@ -160,23 +163,58 @@ class normalizer::imp { }); } else { lean_assert(is_metavar(e)); - local_context lctx = metavar_lctx(e); - unsigned len_s = length(s); - unsigned len_ctx = ctx.size(); - lean_assert(k >= len_ctx); - expr r; - if (k > len_ctx + len_s) - r = add_lift(e, len_s, k - len_ctx - len_s); - else - r = e; - if (is_identity_stack(s, k)) { - return r; - } + // We use the following trick to reify a metavariable in the context of the value_stack s, and context ctx. + // Let v_0, ..., v_{n-1} be the values on the stack s. We assume v_0 is the top of the stack. + // Let v_i' be reify(v_i, k). Then, v_i' is the "value" of the free variable #i in the metavariable e. + // Let m be the size of the context ctx. Thus + // + // The metavariable e may contain free variables. + // Moreover, if we instantiate e with T[x_0, ..., x_{n-1}, x_n, ..., x_{n+m-1}] + // Then, in this occurrence of e, we must have + // + // T[v_0', ..., v_{n-1}', reify(#{m-1}, k), ..., reify(#0, k)] + // + // reify(#j, k) is the index of j-th variable in the context ctx. + // It is just the variable #{k - j - 1}. + // So, we get + // + // T[v_0', ..., v_{n-1}', #{k - m}, ..., #{k - 1}] + // + // Thus, we implement this operation as: + // + // instantiate(e, {#{k - 1}, ..., #{k - m}, v_{n-1}', ..., v_1', v_0'})) + // + // This operation is equivalent to R_{n+m} defined as + // R_0 = e + // R_1 = instantiate(R_0, v_0') + // ... + // R_n = instantiate(R_{n-1}, v_{n-1}') + // R_{n+1} = instantiate(R_n, #{k - m}) + // ... + // R_{n+m} = instantiate(R_{n+m-1}, #{k-1}) + // + // + // Finally, we also use the following optimization. + // If all v_i' are equal to #i and n + m == k, then we just return e, because + // + // T[#0, ..., #n-1, #{n + m - m}, ..., #{m + n - 1}] + // == + // T[#0, ..., #n-1, #n, ..., #{m + n - 1}] + // == + // e + // + unsigned n = length(s); + unsigned m = ctx.size(); + if (k == n + m && is_identity_stack(s, k)) + return e; buffer subst; for (auto v : s) subst.push_back(reify(v, k)); + for (unsigned i = m; i >= 1; i--) + subst.push_back(mk_var(k - i)); + lean_assert(subst.size() == n + m); std::reverse(subst.begin(), subst.end()); - return instantiate(r, subst.size(), subst.data()); + return instantiate(e, subst.size(), subst.data()); } } diff --git a/src/tests/kernel/normalizer.cpp b/src/tests/kernel/normalizer.cpp index edc2f2fac4..d53e8f8d9d 100644 --- a/src/tests/kernel/normalizer.cpp +++ b/src/tests/kernel/normalizer.cpp @@ -17,6 +17,7 @@ Author: Leonardo de Moura #include "kernel/kernel_exception.h" #include "kernel/printer.h" #include "kernel/metavar.h" +#include "kernel/free_vars.h" #include "library/deep_copy.h" #include "library/arith/int.h" #include "frontends/lean/frontend.h" @@ -312,8 +313,34 @@ static void tst10() { context ctx({{"x", Bool}, {"y", Bool}}); expr m = menv->mk_metavar(ctx); ctx = extend(ctx, "z", none_expr(), m); - std::cout << normalizer(env)(Var(0), ctx) << "\n"; - lean_assert_eq(normalizer(env)(Var(0), ctx), add_lift(m, 0, 1)); + expr N = normalizer(env)(Var(0), ctx); + expr f = Const("f"); + metavar_env menv_copy1 = menv.copy(); + lean_verify(menv_copy1->assign(m, f(Var(0)))); + lean_assert_eq(menv_copy1->instantiate_metavars(N), f(Var(1))); + metavar_env menv_copy2 = menv.copy(); + lean_verify(menv_copy2->assign(m, f(Var(1)))); + lean_assert_eq(menv_copy2->instantiate_metavars(N), f(Var(2))); +} + +static void tst11() { + environment env; + metavar_env menv; + context ctx({{"A", Type()}}); + expr m1 = menv->mk_metavar(extend(ctx, "x", Type())); + expr x = Const("x"); + expr e = Fun({x, Type()}, m1); + expr T = Fun({x, Type()}, lift_free_vars(e, 0, 1)(x)); + context ctx2 = extend(ctx, "C", Type()); + expr T1 = lift_free_vars(T, 0, 1); + expr N = normalizer(env)(T1, ctx2, menv); + std::cout << m1 << " context: " << menv->get_context(m1) << "\n"; + std::cout << T1 << " AT " << ctx2 << "\n==>\n" << N << "\n"; + lean_verify(menv->assign(m1, Var(1))); + std::cout << menv->instantiate_metavars(T1) << "\n"; + std::cout << menv->instantiate_metavars(N) << "\n"; + lean_assert_eq(normalizer(env)(menv->instantiate_metavars(T1), ctx2), + menv->instantiate_metavars(N)); } int main() { @@ -329,5 +356,6 @@ int main() { tst8(); tst9(); tst10(); + tst11(); return has_violations() ? 1 : 0; }