feat(kernel/free_vars): improve has_free_vars function, it produces better results for expressions containing metavariables

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

src/kernel/free_vars.cpp

@@ -233,9 +233,10 @@ unsigned free_var_range(expr const & e, metavar_env const & menv) {
 */
 class has_free_var_in_range_fn {
 protected:
-    unsigned             m_low;
+    unsigned                           m_low;
-    unsigned             m_high;
+    unsigned                           m_high;
-    expr_cell_offset_set m_cached;
+    expr_cell_offset_set               m_cached;
+    std::unique_ptr<free_var_range_fn> m_range_fn;
 
     bool apply(optional<expr> const & e, unsigned offset) {
         return e && apply(*e, offset);
@@ -251,7 +252,10 @@ protected:
         case expr_kind::Type: case expr_kind::Value:
             return false;
         case expr_kind::MetaVar:
-            return true;
+            if (m_range_fn)
+                break; // it is not cheap
+            else
+                return true; // assume that any free variable can occur in the metavariable
         case expr_kind::Var:
             return var_idx(e) >= offset + m_low && var_idx(e) < offset + m_high;
         case expr_kind::App: case expr_kind::Eq: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let:
@@ -276,9 +280,20 @@ protected:
             lean_assert(const_type(e));
             result = apply(const_type(e), offset);
             break;
-        case expr_kind::Type: case expr_kind::Value: case expr_kind::Var: case expr_kind::MetaVar:
+        case expr_kind::Type: case expr_kind::Value: case expr_kind::Var:
             // easy cases were already handled
             lean_unreachable(); // LCOV_EXCL_LINE
+        case expr_kind::MetaVar: {
+            lean_assert(m_range_fn);
+            unsigned R = (*m_range_fn)(e);
+            if (R > 0) {
+                unsigned max_fvar_idx = R - 1;
+                result = max_fvar_idx >= offset + m_low;
+                // Remark: Variable #0 may occur in \c e.
+                // So, we don't have to check the upper bound offset + m_high;
+            }
+            break;
+        }
         case expr_kind::App:
             result = std::any_of(begin_args(e), end_args(e), [=](expr const & arg){ return apply(arg, offset); });
             break;
@@ -301,31 +316,27 @@ protected:
         return result;
     }
 public:
-    has_free_var_in_range_fn(unsigned low, unsigned high):
+    has_free_var_in_range_fn(unsigned low, unsigned high, metavar_env const * menv):
         m_low(low),
         m_high(high) {
         lean_assert(low < high);
+        if (menv)
+            m_range_fn.reset(new free_var_range_fn(*menv));
     }
     bool operator()(expr const & e) { return apply(e, 0); }
 };
 
-bool has_free_var(expr const & e, unsigned vidx) {
+bool has_free_var(expr const & e, unsigned low, unsigned high, metavar_env const * menv) {
-    return has_free_var_in_range_fn(vidx, vidx+1)(e);
+    return has_free_var_in_range_fn(low, high, menv)(e);
 }
 
-bool has_free_var(expr const & e, unsigned low, unsigned high) {
+expr lower_free_vars(expr const & e, unsigned s, unsigned d, metavar_env const * menv) {
-    return has_free_var_in_range_fn(low, high)(e);
-}
-
-expr lower_free_vars(expr const & e, unsigned s, unsigned d) {
     lean_assert(s >= d);
-    lean_assert(!has_free_var(e, s-d, s));
+    lean_assert(!has_free_var(e, s-d, s, menv));
     auto f = [=](expr const & e, unsigned offset) -> expr {
         if (is_var(e) && var_idx(e) >= s + offset) {
             lean_assert(var_idx(e) >= offset + d);
             return mk_var(var_idx(e) - d);
-        } else if (is_metavar(e)) {
-            lean_unreachable(); // LCOV_EXCL_LINE
         } else {
             return e;
         }

src/kernel/free_vars.h

@@ -36,26 +36,36 @@ class metavar_env;
 */
 unsigned free_var_range(expr const & e, metavar_env const & menv);
 
-/**
-    \brief Return true iff \c e contains the free variable <tt>(var i)</tt>.
-*/
-bool has_free_var(expr const & e, unsigned i);
-
 /**
     \brief Return true iff \c e constains a free variable <tt>(var i)</tt> s.t. \c i in <tt>[low, high)</tt>.
     \pre low < high
+
+    \remark If menv != nullptr, then we use \c free_var_range to compute the free variables that may
+    occur in a metavariable.
 */
-bool has_free_var(expr const & e, unsigned low, unsigned high);
+bool has_free_var(expr const & e, unsigned low, unsigned high, metavar_env const * menv = nullptr);
+inline bool has_free_var(expr const & e, unsigned low, unsigned high, metavar_env const & menv) {
+    return has_free_var(e, low, high, &menv);
+}
+/**
+    \brief Return true iff \c e contains the free variable <tt>(var i)</tt>.
+*/
+inline bool has_free_var(expr const & e, unsigned i, metavar_env const * menv = nullptr) {  return has_free_var(e, i, i+1, menv); }
 
 /**
-   \brief Lower the free variables >= s in \c e by d. That is, a free variable <tt>(var i)</tt> s.t.
+   \brief Lower the free variables >= s in \c e by \c d. That is, a free variable <tt>(var i)</tt> s.t.
    <tt>i >= s</tt> is mapped into <tt>(var i-d)</tt>.
 
-   \pre d > 0
+   \pre s >= d
-   \pre !has_free_var(e, 0, d)
+   \pre !has_free_var(e, s-d, d, menv)
+
+   \remark The parameter menv is only used for debugging purposes
 */
-expr lower_free_vars(expr const & e, unsigned s, unsigned d);
+expr lower_free_vars(expr const & e, unsigned s, unsigned d, metavar_env const * menv = nullptr);
-inline expr lower_free_vars(expr const & e, unsigned d) { return lower_free_vars(e, d, d); }
+inline expr lower_free_vars(expr const & e, unsigned s, unsigned d, metavar_env const & menv) {
+    return lower_free_vars(e, s, d, &menv);
+}
+inline expr lower_free_vars(expr const & e, unsigned d, metavar_env const * menv = nullptr) { return lower_free_vars(e, d, d, menv); }
 
 /**
    \brief Lift free variables >= s in \c e by d.

src/tests/kernel/free_vars.cpp

@@ -106,11 +106,44 @@ static void tst4() {
     lean_assert_eq(fn(mk_let("x", Var(2), Var(1), Var(4))), 4);
 }
 
+static void tst5() {
+    metavar_env menv;
+    expr m1 = menv.mk_metavar();
+    expr f = Const("f");
+    expr a = Const("a");
+    expr b = Const("b");
+    expr t = Const("t");
+    expr x = Const("x");
+    lean_assert(has_free_var(mk_lambda("x", t, f(Var(1))), 0,  menv));
+    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;
+    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));
+    lean_assert(!has_free_var(m2, 2, menv));
+    lean_assert(has_free_var(Fun({x, Bool}, m2), 0, menv));
+    lean_assert(!has_free_var(Fun({x, Bool}, m2), 1, menv));
+    lean_assert(has_free_var(Fun({x, Bool}, add_inst(add_lift(m2, 1, 3), 0, Var(0))), 0, menv));
+    lean_assert(has_free_var(Fun({x, Bool}, add_inst(add_lift(m2, 1, 1), 0, Var(0))), 0, menv));
+    lean_assert(!has_free_var(Fun({x, Bool}, add_inst(add_lift(m2, 1, 1), 0, Var(0))), 1, menv));
+    lean_assert(has_free_var(Fun({x, Bool}, add_inst(add_lift(m2, 1, 2), 0, Var(0))), 1, 3, menv));
+    lean_assert(!has_free_var(Fun({x, Bool}, add_inst(add_lift(m2, 1, 2), 0, Var(0))), 2, 5, menv));
+    lean_assert_eq(lower_free_vars(Fun({x, Bool}, add_inst(add_lift(m2, 1, 2), 0, Var(0))), 5, 3, menv),
+                   Fun({x, Bool}, add_inst(add_lift(m2, 1, 2), 0, Var(0))));
+    lean_assert_eq(lower_free_vars(Fun({x, Bool}, Var(6)(add_inst(add_lift(m2, 1, 2), 0, Var(0)))), 5, 3, menv),
+                   Fun({x, Bool}, Var(3)(add_inst(add_lift(m2, 1, 2), 0, Var(0)))));
+}
+
 int main() {
     save_stack_info();
     tst1();
     tst2();
     tst3();
     tst4();
+    tst5();
     return has_violations() ? 1 : 0;
 }