feat(kernel): improve instantiate and lift_free_vars (use metavar_env to minimize the number of lift and inst local_entries needed)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/kernel/free_vars.cpp

@@ -344,14 +344,14 @@ expr lower_free_vars(expr const & e, unsigned s, unsigned d, metavar_env const *
     return replace_fn<decltype(f)>(f)(e);
 }
 
-expr lift_free_vars(expr const & e, unsigned s, unsigned d) {
+expr lift_free_vars(expr const & e, unsigned s, unsigned d, metavar_env const * menv) {
     if (d == 0)
         return e;
     auto f = [=](expr const & e, unsigned offset) -> expr {
         if (is_var(e) && var_idx(e) >= s + offset) {
             return mk_var(var_idx(e) + d);
         } else if (is_metavar(e)) {
-            return add_lift(e, s + offset, d);
+            return add_lift(e, s + offset, d, menv);
         } else {
             return e;
         }

src/kernel/free_vars.h

@@ -70,7 +70,12 @@ inline expr lower_free_vars(expr const & e, unsigned d, metavar_env const * menv
 
 /**
    \brief Lift free variables >= s in \c e by d.
+
+   \remark When the parameter menv != nullptr, this function will minimize the use
+   of the local entry lift in metavariables occurring in \c e.
 */
-expr lift_free_vars(expr const & e, unsigned s, unsigned d);
+expr lift_free_vars(expr const & e, unsigned s, unsigned d, metavar_env const * menv = nullptr);
-inline expr lift_free_vars(expr const & e, unsigned d) { return lift_free_vars(e, 0, d); }
+inline expr lift_free_vars(expr const & e, unsigned s, unsigned d, metavar_env const & menv) { return lift_free_vars(e, s, d, &menv); }
+inline expr lift_free_vars(expr const & e, unsigned d, metavar_env const * menv = nullptr) { return lift_free_vars(e, 0, d, menv); }
+inline expr lift_free_vars(expr const & e, unsigned d, metavar_env const & menv) { return lift_free_vars(e, 0, d, &menv); }
 }

src/kernel/instantiate.cpp

@@ -5,12 +5,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <algorithm>
+#include <limits>
 #include "kernel/free_vars.h"
 #include "kernel/replace_fn.h"
 #include "kernel/metavar.h"
+#include "kernel/instantiate.h"
 
 namespace lean {
-expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s) {
+expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s, metavar_env const * menv) {
     auto f = [=](expr const & m, unsigned offset) -> expr {
         if (is_var(m)) {
             unsigned vidx = var_idx(m);
@@ -25,7 +27,7 @@ expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s)
         } else if (is_metavar(m)) {
             expr r = m;
             for (unsigned i = 0; i < n; i++)
-                r = add_inst(r, offset + n - i - 1, s[i]);
+                r = add_inst(r, offset + n - i - 1, s[i], menv);
             return r;
         } else {
             return m;
@@ -34,18 +36,18 @@ expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s)
     return replace_fn<decltype(f)>(f)(a);
 }
 
-expr instantiate_with_closed(expr const & a, unsigned n, expr const * s) {
+expr instantiate_with_closed(expr const & a, unsigned n, expr const * s, metavar_env const * menv) {
-    lean_assert(std::all_of(s, s+n, closed));
+    lean_assert(std::all_of(s, s+n, [&](expr const & e) { return !has_free_var(e, 0, std::numeric_limits<unsigned>::max(), menv); }));
-    return instantiate_with_closed_relaxed(a, n, s);
+    return instantiate_with_closed_relaxed(a, n, s, menv);
 }
 
-expr instantiate(expr const & a, unsigned s, unsigned n, expr const * subst) {
+expr instantiate(expr const & a, unsigned s, unsigned n, expr const * subst, metavar_env const * menv) {
     auto f = [=](expr const & m, unsigned offset) -> expr {
         if (is_var(m)) {
             unsigned vidx = var_idx(m);
             if (vidx >= offset + s) {
                 if (vidx < offset + s + n)
-                    return lift_free_vars(subst[n - (vidx - s - offset) - 1], offset);
+                    return lift_free_vars(subst[n - (vidx - s - offset) - 1], offset, menv);
                 else
                     return mk_var(vidx - n);
             } else {
@@ -54,7 +56,7 @@ expr instantiate(expr const & a, unsigned s, unsigned n, expr const * subst) {
         } else if (is_metavar(m)) {
             expr r = m;
             for (unsigned i = 0; i < n; i++)
-                r = add_inst(r, offset + s + n - i - 1, lift_free_vars(subst[i], offset + n - i - 1));
+                r = add_inst(r, offset + s + n - i - 1, lift_free_vars(subst[i], offset + n - i - 1, menv), menv);
             return r;
         } else {
             return m;
@@ -62,18 +64,18 @@ expr instantiate(expr const & a, unsigned s, unsigned n, expr const * subst) {
     };
     return replace_fn<decltype(f)>(f)(a);
 }
-expr instantiate(expr const & e, unsigned n, expr const * s) {
+expr instantiate(expr const & e, unsigned n, expr const * s, metavar_env const * menv) {
-    return instantiate(e, 0, n, s);
+    return instantiate(e, 0, n, s, menv);
 }
-expr instantiate(expr const & e, unsigned i, expr const & s) {
+expr instantiate(expr const & e, unsigned i, expr const & s, metavar_env const * menv) {
-    return instantiate(e, i, 1, &s);
+    return instantiate(e, i, 1, &s, menv);
 }
 
 bool is_head_beta(expr const & t) {
     return is_app(t) && is_lambda(arg(t, 0));
 }
 
-expr apply_beta(expr f, unsigned num_args, expr const * args) {
+expr apply_beta(expr f, unsigned num_args, expr const * args, metavar_env const * menv) {
     lean_assert(is_lambda(f));
     unsigned m = 1;
     while (is_lambda(abst_body(f)) && m < num_args) {
@@ -81,7 +83,7 @@ expr apply_beta(expr f, unsigned num_args, expr const * args) {
         m++;
     }
     lean_assert(m <= num_args);
-    expr r = instantiate(abst_body(f), m, args);
+    expr r = instantiate(abst_body(f), m, args, menv);
     if (m == num_args) {
         return r;
     } else {
@@ -93,18 +95,18 @@ expr apply_beta(expr f, unsigned num_args, expr const * args) {
     }
 }
 
-expr head_beta_reduce(expr const & t) {
+expr head_beta_reduce(expr const & t, metavar_env const * menv) {
     if (!is_head_beta(t)) {
         return t;
     } else {
-        return apply_beta(arg(t, 0), num_args(t) - 1, &arg(t, 1));
+        return apply_beta(arg(t, 0), num_args(t) - 1, &arg(t, 1), menv);
     }
 }
 
-expr beta_reduce(expr t) {
+expr beta_reduce(expr t, metavar_env const * menv) {
     auto f = [=](expr const & m, unsigned) -> expr {
         if (is_head_beta(m))
-            return head_beta_reduce(m);
+            return head_beta_reduce(m, menv);
         else
             return m;
     };

src/kernel/instantiate.h

@@ -8,36 +8,76 @@ Author: Leonardo de Moura
 #include "kernel/expr.h"
 
 namespace lean {
+class metavar_env;
 /**
    \brief Replace the free variables with indices 0, ..., n-1 with s[n-1], ..., s[0] in e.
 
    \pre s[0], ..., s[n-1] must be closed expressions (i.e., no free variables).
+
+   \remark When the parameter menv != nullptr, this function will minimize the use
+   of the local entry inst in metavariables occurring in \c e.
 */
-expr instantiate_with_closed(expr const & e, unsigned n, expr const * s);
+expr instantiate_with_closed(expr const & e, unsigned n, expr const * s, metavar_env const * menv = nullptr);
+inline expr instantiate_with_closed(expr const & e, unsigned n, expr const * s, metavar_env const & menv) {
+    return instantiate_with_closed(e, n, s, &menv);
+}
 inline expr instantiate_with_closed(expr const & e, std::initializer_list<expr> const & l) {
     return instantiate_with_closed(e, l.size(), l.begin());
 }
-inline expr instantiate_with_closed(expr const & e, expr const & s) { return instantiate_with_closed(e, 1, &s); }
+inline expr instantiate_with_closed(expr const & e, expr const & s, metavar_env const * menv = nullptr) {
+    return instantiate_with_closed(e, 1, &s, menv);
+}
+inline expr instantiate_with_closed(expr const & e, expr const & s, metavar_env const & menv) {
+    return instantiate_with_closed(e, s, &menv);
+}
 /**
    \brief Similar to instantiate_with_closed, but does not use an assertion for
    testing whether arguments are close or not.
    This version is useful, for example, when we want to treat metavariables as closed terms.
 */
-expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s);
+expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s, metavar_env const * menv = nullptr);
+inline expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s, metavar_env const & menv) {
+    return instantiate_with_closed_relaxed(a, n, s, menv);
+}
 
 /**
    \brief Replace the free variables with indices 0, ..., n-1 with s[n-1], ..., s[0] in e.
+
+   \remark When the parameter menv != nullptr, this function will minimize the use
+   of the local entry inst in metavariables occurring in \c e.
 */
-expr instantiate(expr const & e, unsigned n, expr const * s);
+expr instantiate(expr const & e, unsigned n, expr const * s, metavar_env const * menv = nullptr);
-inline expr instantiate(expr const & e, std::initializer_list<expr> const & l) { return instantiate(e, l.size(), l.begin()); }
+inline expr instantiate(expr const & e, unsigned n, expr const * s, metavar_env const & menv) {
-inline expr instantiate(expr const & e, expr const & s) { return instantiate(e, 1, &s); }
+    return instantiate(e, n, s, &menv);
+}
+inline expr instantiate(expr const & e, std::initializer_list<expr> const & l) {
+    return instantiate(e, l.size(), l.begin());
+}
+inline expr instantiate(expr const & e, expr const & s, metavar_env const * menv = nullptr) {
+    return instantiate(e, 1, &s, menv);
+}
+inline expr instantiate(expr const & e, expr const & s, metavar_env const & menv) {
+    return instantiate(e, s, &menv);
+}
 /**
    \brief Replace free variable \c i with \c s in \c e.
 */
-expr instantiate(expr const & e, unsigned i, expr const & s);
+expr instantiate(expr const & e, unsigned i, expr const & s, metavar_env const * menv = nullptr);
-
+inline expr instantiate(expr const & e, unsigned i, expr const & s, metavar_env const & menv) {
-expr apply_beta(expr f, unsigned num_args, expr const * args);
+    return instantiate(e, i, s, &menv);
-bool is_head_beta(expr const & t);
+}
-expr head_beta_reduce(expr const & t);
+
-expr beta_reduce(expr t);
+expr apply_beta(expr f, unsigned num_args, expr const * args, metavar_env const * menv = nullptr);
+inline expr apply_beta(expr f, unsigned num_args, expr const * args, metavar_env const & menv) {
+    return apply_beta(f, num_args, args, &menv);
+}
+bool is_head_beta(expr const & t);
+expr head_beta_reduce(expr const & t, metavar_env const * menv = nullptr);
+inline expr head_beta_reduce(expr const & t, metavar_env const & menv) {
+    return head_beta_reduce(t, &menv);
+}
+expr beta_reduce(expr t, metavar_env const * menv = nullptr);
+inline expr beta_reduce(expr t, metavar_env const & menv) {
+    return beta_reduce(t, &menv);
+}
 }

src/kernel/metavar.cpp

@@ -330,7 +330,9 @@ local_context add_lift(local_context const & lctx, unsigned s, unsigned n) {
     return cons(mk_lift(s, n), lctx);
 }
 
-expr add_lift(expr const & m, unsigned s, unsigned n) {
+expr add_lift(expr const & m, unsigned s, unsigned n, metavar_env const * menv) {
+    if (menv && s >= free_var_range(m, *menv))
+        return m;
     return update_metavar(m, add_lift(metavar_lctx(m), s, n));
 }
 
@@ -352,7 +354,9 @@ local_context add_inst(local_context const & lctx, unsigned s, expr const & v) {
     return cons(mk_inst(s, v), lctx);
 }
 
-expr add_inst(expr const & m, unsigned s, expr const & v) {
+expr add_inst(expr const & m, unsigned s, expr const & v, metavar_env const * menv) {
+    if (menv && s >= free_var_range(m, *menv))
+        return m;
     return update_metavar(m, add_inst(metavar_lctx(m), s, v));
 }
 

src/kernel/metavar.h

@@ -180,15 +180,25 @@ local_context add_lift(local_context const & lctx, unsigned s, unsigned n);
    \brief Add a lift:s:n operation to the context of the given metavariable.
 
    \pre is_metavar(m)
+
+   \remark If menv != nullptr, then we use \c free_var_range to compute the free variables that may
+   occur in \c m. If s > the maximum free variable that occurs in \c m, then
+   we do not add a lift local entry to the local context.
 */
-expr add_lift(expr const & m, unsigned s, unsigned n);
+expr add_lift(expr const & m, unsigned s, unsigned n, metavar_env const * menv = nullptr);
+inline expr add_lift(expr const & m, unsigned s, unsigned n, metavar_env const & menv) { return add_lift(m, s, n, &menv); }
 
 /**
    \brief Add an inst:s:v operation to the context of the given metavariable.
 
    \pre is_metavar(m)
+
+   \remark If menv != nullptr, then we use \c free_var_range to compute the free variables that may
+   occur in \c m. If s > the maximum free variable that occurs in \c m, then
+   we do not add an inst local entry to the local context.
 */
-expr add_inst(expr const & m, unsigned s, expr const & v);
+expr add_inst(expr const & m, unsigned s, expr const & v, metavar_env const * menv = nullptr);
+inline expr add_inst(expr const & m, unsigned s, expr const & v, metavar_env const & menv) { return add_inst(m, s, v, &menv); }
 
 /**
    \brief Extend the local context \c lctx with the entry <tt>inst:s v</tt>

src/tests/kernel/free_vars.cpp

@@ -118,9 +118,7 @@ static void tst5() {
     lean_assert(!has_free_var(mk_lambda("x", t, f(Var(0))), 1, menv));
     lean_assert(!has_free_var(m1, 0, menv));
     lean_assert(!has_free_var(m1, 1, menv));
-    context ctx;
+    context ctx({{"x", Bool}, {"y", Bool}});
-    ctx = extend(ctx, name("x"), Bool);
-    ctx = extend(ctx, name("y"), Bool);
     expr m2 = menv.mk_metavar(ctx);
     lean_assert(has_free_var(m2, 0, menv));
     lean_assert(has_free_var(m2, 1, menv));
@@ -138,6 +136,19 @@ static void tst5() {
                    Fun({x, Bool}, Var(3)(add_inst(add_lift(m2, 1, 2), 0, Var(0)))));
 }
 
+static void tst6() {
+    metavar_env menv;
+    expr f  = Const("f");
+    expr m1 = menv.mk_metavar();
+    expr m2 = menv.mk_metavar(context({{"x", Bool}, {"y", Bool}}));
+    lean_assert(lift_free_vars(m1, 0, 1, menv) == m1);
+    lean_assert(lift_free_vars(m2, 0, 1, menv) != m2);
+    lean_assert(lift_free_vars(m2, 0, 1, menv) == add_lift(m2, 0, 1));
+    lean_assert(lift_free_vars(m1, 0, 1) == add_lift(m1, 0, 1));
+    lean_assert(lift_free_vars(f(m1), 0, 1, menv) == f(m1));
+    lean_assert(lift_free_vars(f(m2), 0, 1, menv) == f(add_lift(m2, 0, 1)));
+}
+
 int main() {
     save_stack_info();
     tst1();
@@ -145,5 +156,6 @@ int main() {
     tst3();
     tst4();
     tst5();
+    tst6();
     return has_violations() ? 1 : 0;
 }

src/tests/kernel/instantiate.cpp

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include "util/test.h"
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
+#include "kernel/metavar.h"
 using namespace lean;
 
 static void tst1() {
@@ -44,9 +45,54 @@ static void tst2() {
     lean_assert_eq(head_beta_reduce(F1), F1);
 }
 
+static void tst3() {
+    metavar_env menv;
+    expr f  = Const("f");
+    expr a  = Const("a");
+    expr T  = Const("T");
+    expr m1 = menv.mk_metavar();
+    expr m2 = menv.mk_metavar(context({{"x", T}, {"y", T}}));
+    lean_assert_eq(instantiate(f(m1, Var(0)), 0, a, menv), f(m1, a));
+    lean_assert_ne(instantiate(f(m1, Var(0)), 0, a, menv), instantiate(f(m1, Var(0)), 0, a));
+    lean_assert_ne(instantiate(f(m2, Var(0)), 0, a, menv), f(m2, a));
+    lean_assert_eq(instantiate(f(m2, Var(0)), 0, a, menv), f(add_inst(m2, 0, a), a));
+    expr x = Const("x");
+    lean_assert_eq(instantiate(Fun({x, T}, f(m1, Var(1), Var(0))), 0, f(Var(0)), menv),
+                   Fun({x, T}, f(m1, f(Var(1)), Var(0))));
+    lean_assert_eq(instantiate(Fun({x, T}, f(m2, Var(1), Var(0))), 0, f(Var(0)), menv),
+                   Fun({x, T}, f(add_inst(m2, 1, f(Var(1))), f(Var(1)), Var(0))));
+    lean_assert_eq(instantiate(Fun({x, T}, f(m2, Var(3), Var(0))), 2, f(Var(0)), menv),
+                   Fun({x, T}, f(m2, f(Var(1)), Var(0))));
+    lean_assert_eq(instantiate(Fun({x, T}, f(m1, Var(3), Var(0))), 2, f(Var(0)), menv),
+                   Fun({x, T}, f(m1, f(Var(1)), Var(0))));
+    lean_assert_eq(instantiate(Fun({x, T}, f(m2, Var(3), Var(0))), 1, f(Var(0)), menv),
+                   Fun({x, T}, f(m2, Var(2), Var(0))));
+    expr m3 = menv.mk_metavar(context({{"x", T}, {"y", T}, {"z", T}}));
+    lean_assert_eq(instantiate(Fun({x, T}, f(m3, Var(3), Var(0))), 1, f(Var(0)), menv),
+                   Fun({x, T}, f(add_inst(m3, 2, f(Var(1))), Var(2), Var(0))));
+}
+
+static void tst4() {
+    metavar_env menv;
+    expr T  = Const("T");
+    expr m1 = menv.mk_metavar();
+    expr m2 = menv.mk_metavar(context({{"x", T}, {"y", T}}));
+    expr f = Const("f");
+    expr g = Const("f");
+    expr x = Const("x");
+    expr a = Const("a");
+    expr F1 = Fun({x, T}, g(x, m1))(a);
+    expr F2 = Fun({x, T}, g(x, m2))(a);
+    lean_assert_eq(head_beta_reduce(F1, menv), g(a, m1));
+    lean_assert_eq(head_beta_reduce(F1), g(a, add_inst(m1, 0, a)));
+    lean_assert_eq(head_beta_reduce(F2, menv), g(a, add_inst(m2, 0, a)));
+}
+
 int main() {
     save_stack_info();
     tst1();
     tst2();
+    tst3();
+    tst4();
     return has_violations() ? 1 : 0;
 }

src/tests/kernel/metavar.cpp

@@ -18,6 +18,7 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 #include "kernel/printer.h"
 #include "kernel/kernel_exception.h"
+#include "kernel/builtin.h"
 #include "library/placeholder.h"
 #include "library/io_state.h"
 #include "library/arith/arith.h"
@@ -599,6 +600,27 @@ static void tst27() {
     std::cout << up << "\n";
 }
 
+static void tst28() {
+    metavar_env menv;
+    expr f = Const("f");
+    expr a = Const("a");
+    expr m1 = menv.mk_metavar();
+    lean_assert(add_inst(m1, 0, f(a), menv) == m1);
+    lean_assert(add_inst(m1, 1, f(a), menv) == m1);
+    lean_assert(add_lift(m1, 0, 2, menv) == m1);
+    lean_assert(add_lift(m1, 1, 2, menv) == m1);
+    expr m2 = menv.mk_metavar(context({{"x", Bool}, {"y", Bool}}));
+    lean_assert(add_inst(m2, 0, f(a), menv) != m2);
+    lean_assert(add_inst(m2, 0, f(a), menv) == add_inst(m2, 0, f(a)));
+    lean_assert(add_inst(m2, 1, f(a), menv) != m2);
+    lean_assert(add_inst(m2, 2, f(a), menv) == m2);
+    lean_assert(add_lift(m2, 0, 2, menv) != m2);
+    lean_assert(add_lift(m2, 0, 2, menv) == add_lift(m2, 0, 2));
+    lean_assert(add_lift(m2, 1, 2, menv) != m2);
+    lean_assert(add_lift(m2, 2, 2, menv) == m2);
+    lean_assert(add_lift(m2, 2, 2, menv) != add_lift(m2, 2, 2));
+}
+
 int main() {
     save_stack_info();
     tst1();
@@ -628,5 +650,6 @@ int main() {
     tst25();
     tst26();
     tst27();
+    tst28();
     return has_violations() ? 1 : 0;
 }