feat(metavar): automatically apply beta-reduction when instantiating metavariable applications (i.e., expressions of the form (?m a)), when the metavariable is a lambda

This feature is useful for problems that require higher-order matching and/or unification.

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

src/kernel/metavar.cpp

@@ -8,7 +8,6 @@ Author: Leonardo de Moura
 #include <algorithm>
 #include "util/exception.h"
 #include "kernel/metavar.h"
-#include "kernel/replace.h"
 #include "kernel/free_vars.h"
 #include "kernel/instantiate.h"
 #include "kernel/occurs.h"
@@ -20,8 +19,9 @@ void swap(substitution & s1, substitution & s2) {
     std::swap(s1.m_size, s2.m_size);
 }
 
-substitution::substitution():
+substitution::substitution(bool beta_reduce_mv):
-    m_size(0) {
+    m_size(0),
+    m_beta_reduce_mv(beta_reduce_mv) {
 }
 
 bool substitution::is_assigned(name const & m) const {
@@ -225,18 +225,41 @@ name metavar_env::find_unassigned_metavar() const {
     return r;
 }
 
+
+void instantiate_metavars_proc::instantiated_metavar(expr const &) {
+}
+
+expr instantiate_metavars_proc::visit_metavar(expr const & m, context const &) {
+    if (is_metavar(m) && m_subst.is_assigned(m)) {
+        instantiated_metavar(m);
+        return m_subst.get_subst(m);
+    } else {
+        return m;
+    }
+}
+
+expr instantiate_metavars_proc::visit_app(expr const & e, context const & ctx) {
+    if (m_subst.beta_reduce_metavar_application() && is_metavar(arg(e, 0)) && m_subst.is_assigned(arg(e, 0))) {
+        instantiated_metavar(arg(e, 0));
+        expr new_f = m_subst.get_subst(arg(e, 0));
+        if (is_lambda(new_f)) {
+            buffer<expr> new_args;
+            for (unsigned i = 1; i < num_args(e); i++)
+                new_args.push_back(visit(arg(e, i), ctx));
+            return apply_beta(new_f, new_args.size(), new_args.data());
+        }
+    }
+    return replace_visitor::visit_app(e, ctx);
+}
+
+instantiate_metavars_proc::instantiate_metavars_proc(substitution const & s):m_subst(s) {
+}
+
 expr instantiate_metavars(expr const & e, substitution const & s) {
     if (!has_metavar(e)) {
         return e;
     } else {
-        auto f = [=](expr const & m, unsigned) -> expr {
+        return instantiate_metavars_proc(s)(e);
-            if (is_metavar(m) && s.is_assigned(m)) {
-                return s.get_subst(m);
-            } else {
-                return m;
-            }
-        };
-        return replace_fn<decltype(f)>(f)(e);
     }
 }
 

src/kernel/metavar.h

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "kernel/expr.h"
 #include "kernel/context.h"
 #include "kernel/justification.h"
+#include "kernel/replace_visitor.h"
 
 namespace lean {
 /**
@@ -21,8 +22,17 @@ class substitution {
     typedef splay_map<name, expr, name_cmp> name2expr;
     name2expr m_subst;
     unsigned  m_size;
+    // If the following flag is true, then beta-reduction is automatically applied
+    // when we apply a substitution containing ?m <- fun (x : T), ...
+    // to an expression containing (?m a)
+    // The motivation is that higher order unification and matching produces a
+    // bunch of assignments of the form ?m <- fun (x : T), ...
+    bool      m_beta_reduce_mv;
 public:
-    substitution();
+    substitution(bool beta_reduce_mv = true);
+
+    bool beta_reduce_metavar_application() const { return m_beta_reduce_mv; }
+    void set_beta_reduce_metavar_application(bool f) { m_beta_reduce_mv = f; }
 
     friend void swap(substitution & s1, substitution & s2);
 
@@ -216,6 +226,18 @@ void swap(metavar_env & a, metavar_env & b);
 */
 expr apply_local_context(expr const & a, local_context const & lctx);
 
+class instantiate_metavars_proc : public replace_visitor {
+protected:
+    substitution const & m_subst;
+    virtual expr visit_metavar(expr const & m, context const &);
+    virtual expr visit_app(expr const & e, context const & ctx);
+    // The following method is invoked whenever the visitor instantiates
+    // a metavariable \c m
+    virtual void instantiated_metavar(expr const & m);
+public:
+    instantiate_metavars_proc(substitution const & s);
+};
+
 /**
    \brief Instantiate the metavariables occurring in \c e with the substitutions
    provided by \c s.

src/library/elaborator/elaborator.cpp

@@ -438,7 +438,10 @@ class elaborator::imp {
         if (is_app(a) && is_metavar(arg(a, 0)) && is_assigned(arg(a, 0))) {
             // Case 4
             justification new_jst(new substitution_justification(c, get_mvar_justification(arg(a, 0))));
-            expr new_a = update_app(a, 0, get_mvar_subst(arg(a, 0)));
+            expr new_f = get_mvar_subst(arg(a, 0));
+            expr new_a = update_app(a, 0, new_f);
+            if (m_state.m_menv.get_substitutions().beta_reduce_metavar_application())
+                new_a = head_beta_reduce(new_a);
             push_updated_constraint(c, is_lhs, new_a, new_jst);
             return Processed;
         }
@@ -453,24 +456,27 @@ class elaborator::imp {
         }
     }
 
+    class instantiate_metavars_tracking_justifications_proc : public instantiate_metavars_proc {
+        metavar_env &           m_menv;
+        buffer<justification> & m_jsts;
+    protected:
+        virtual void instantiated_metavar(expr const & m) {
+            justification t = m_menv.get_justification(m);
+            if (t)
+                m_jsts.push_back(t);
+        }
+    public:
+        instantiate_metavars_tracking_justifications_proc(metavar_env & menv, buffer<justification> & js):
+            instantiate_metavars_proc(menv.get_substitutions()), m_menv(menv), m_jsts(js) {}
+    };
+
     /**
        \brief Instantiate the assigned metavariables in \c a, and store the justifications
        in \c jsts.
     */
     expr instantiate_metavars(expr const & a, buffer<justification> & jsts) {
         lean_assert(has_assigned_metavar(a));
-        metavar_env & menv = m_state.m_menv;
+        return instantiate_metavars_tracking_justifications_proc(m_state.m_menv, jsts)(a);
-        auto f = [&](expr const & m, unsigned) -> expr {
-            if (is_metavar(m) && menv.is_assigned(m)) {
-                justification t = menv.get_justification(m);
-                if (t)
-                    jsts.push_back(t);
-                return menv.get_subst(m);
-            } else {
-                return m;
-            }
-        };
-        return replace_fn<decltype(f)>(f)(a);
     }
 
     /**

src/tests/library/elaborator/elaborator.cpp

@@ -263,7 +263,7 @@ static void tst6() {
     ucs.push_back(mk_eq_constraint(context(), expected, given, justification()));
     elaborator elb(env, menv, ucs.size(), ucs.data());
     substitution s = elb.next();
-    std::cout << beta_reduce(instantiate_metavars(V, s)) << "\n";
+    std::cout << instantiate_metavars(V, s) << "\n";
 }
 
 #define _ mk_placholder()
@@ -276,7 +276,7 @@ static expr elaborate(expr const & e, environment const & env) {
     checker.infer_type(e2, context(), &menv, ucs);
     elaborator elb(env, menv, ucs.size(), ucs.data());
     substitution s = elb.next();
-    return beta_reduce(instantiate_metavars(e2, s));
+    return instantiate_metavars(e2, s);
 }
 
 // Check elaborator success
@@ -652,9 +652,9 @@ void tst20() {
     while (true) {
         try {
             auto sol = elb.next();
-            std::cout << m1 << " -> " << beta_reduce(sol.get_subst(m1)) << "\n";
+            std::cout << m1 << " -> " << sol.get_subst(m1) << "\n";
-            std::cout << beta_reduce(instantiate_metavars(l, sol)) << "\n";
+            std::cout << instantiate_metavars(l, sol) << "\n";
-            lean_assert(beta_reduce(instantiate_metavars(l, sol)) == r);
+            lean_assert(instantiate_metavars(l, sol) == r);
             std::cout << "--------------\n";
         } catch (elaborator_exception & ex) {
             break;
@@ -684,9 +684,9 @@ void tst21() {
     while (true) {
         try {
             auto sol = elb.next();
-            std::cout << m1 << " -> " << beta_reduce(sol.get_subst(m1)) << "\n";
+            std::cout << m1 << " -> " << sol.get_subst(m1) << "\n";
-            std::cout << beta_reduce(instantiate_metavars(l, sol)) << "\n";
+            std::cout << instantiate_metavars(l, sol) << "\n";
-            lean_assert(beta_reduce(instantiate_metavars(l, sol)) == r);
+            lean_assert(instantiate_metavars(l, sol) == r);
             std::cout << "--------------\n";
         } catch (elaborator_exception & ex) {
             break;
@@ -718,10 +718,10 @@ void tst22() {
     while (true) {
         try {
             auto sol = elb.next();
-            std::cout << m3 << " -> " << beta_reduce(sol.get_subst(m3)) << "\n";
+            std::cout << m3 << " -> " << sol.get_subst(m3) << "\n";
             lean_assert(sol.get_subst(m3) == iVal(1));
-            std::cout << beta_reduce(instantiate_metavars(l, sol)) << "\n";
+            std::cout << instantiate_metavars(l, sol) << "\n";
-            std::cout << beta_reduce(instantiate_metavars(r, sol)) << "\n";
+            std::cout << instantiate_metavars(r, sol) << "\n";
             std::cout << "--------------\n";
         } catch (elaborator_exception & ex) {
             break;
@@ -748,10 +748,10 @@ void tst23() {
     while (true) {
         try {
             auto sol = elb.next();
-            std::cout << m1 << " -> " << beta_reduce(sol.get_subst(m1)) << "\n";
+            std::cout << m1 << " -> " << sol.get_subst(m1) << "\n";
-            std::cout << beta_reduce(instantiate_metavars(l, sol)) << "\n";
+            std::cout << instantiate_metavars(l, sol) << "\n";
-            lean_assert_eq(beta_reduce(instantiate_metavars(l, sol)),
+            lean_assert_eq(instantiate_metavars(l, sol),
-                           beta_reduce(instantiate_metavars(r, sol)));
+                           instantiate_metavars(r, sol));
             std::cout << "--------------\n";
         } catch (elaborator_exception & ex) {
             break;
@@ -797,8 +797,8 @@ void tst25() {
     while (true) {
         try {
             auto sol = elb.next();
-            std::cout << m1 << " -> " << beta_reduce(sol.get_subst(m1)) << "\n";
+            std::cout << m1 << " -> " << sol.get_subst(m1) << "\n";
-            std::cout << beta_reduce(instantiate_metavars(l, sol)) << "\n";
+            std::cout << instantiate_metavars(l, sol) << "\n";
             lean_assert_eq(beta_reduce(instantiate_metavars(l, sol)),
                            beta_reduce(instantiate_metavars(r, sol)));
             std::cout << "--------------\n";
@@ -868,8 +868,8 @@ void tst27() {
     std::cout << checker.infer_type(F, context(), &menv, ucs) << "\n";
     elaborator elb(env, menv, ucs.size(), ucs.data());
     substitution s = elb.next();
-    std::cout << beta_reduce(instantiate_metavars(F, s)) << "\n";
+    std::cout << instantiate_metavars(F, s) << "\n";
-    lean_assert_eq(beta_reduce(instantiate_metavars(F, s)),
+    lean_assert_eq(instantiate_metavars(F, s),
                    Fun({f, TypeM >> TypeM}, eq(TypeM, g(TypeM >> TypeM, f)(a), a)));
 }