Add head_reduce_mmv (reduction function modulo metavariables)

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

src/library/metavar.cpp

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include "metavar.h"
 #include "replace.h"
 #include "for_each.h"
+#include "environment.h"
 
 namespace lean {
 static name g_metavar_prefix(name(name(name(0u), "library"), "metavar"));
@@ -259,4 +260,38 @@ expr instantiate_metavar(expr const & e, unsigned midx, expr const & v) {
     };
     return replace_fn<decltype(f)>(f)(e);
 }
+
+expr head_reduce_mmv(expr const & e, environment const & env, name_set const * defs) {
+    if (is_app(e) && is_lambda(arg(e, 0))) {
+        expr r = arg(e,0);
+        unsigned num = num_args(e);
+        unsigned i = 1;
+        while (i < num) {
+            r = instantiate_free_var_mmv(abst_body(r), 0, arg(e,i));
+            i = i + 1;
+            if (!is_lambda(r))
+                break;
+        }
+        if (i == num) {
+            return r;
+        } else {
+            buffer<expr> args;
+            args.push_back(r);
+            for (; i < num; i++)
+                args.push_back(arg(e,i));
+            return mk_app(args.size(), args.data());
+        }
+    } else if (is_let(e)) {
+        return instantiate_free_var_mmv(let_body(e), 0, let_value(e));
+    } else if (is_constant(e)) {
+        name const & n = const_name(e);
+        if (defs == nullptr || defs->find(n) != defs->end()) {
+            object const & obj = env.find_object(n);
+            if (obj && obj.is_definition() && !obj.is_opaque())
+                return obj.get_value();
+        }
+    }
+    return e;
+}
+
 }

src/library/metavar.h

@@ -6,6 +6,8 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "expr.h"
+#include "environment.h"
+#include "name_set.h"
 
 namespace lean {
 /**
@@ -72,6 +74,18 @@ expr lower_free_vars_mmv(expr const & e, unsigned s, unsigned n);
 */
 expr instantiate_metavar(expr const & e, unsigned midx, expr const & v);
 
+/**
+   \brief Try to reduce the head of the given expression.
+   The following reductions are tried:
+   1- Beta reduction
+   2- Constant unfolding (if constant is defined in env, and defs ==
+   nullptr or it contains constant).
+   3- Let expansion
+
+   \remark The expression \c e may contain metavariables.
+*/
+expr head_reduce_mmv(expr const & e, environment const & env, name_set const * defs = nullptr);
+
 /**
    \brief Return true iff \c e is a delayed substitution expression
    of the form (subst:i c v). The meaning of the expression is

src/tests/library/metavar.cpp

@@ -91,12 +91,29 @@ static void tst5() {
     lean_assert(r == f(g(f(h(Var(2)))), Fun({x, N}, f(g(f(h(Var(3)))), h(Var(3)), x, Fun({y, N}, f(g(f(h(Var(4)))), x, y))))));
 }
 
+static void tst6() {
+    environment env;
+    expr N  = Const("N");
+    expr f  = Const("f");
+    expr a  = Const("a");
+    expr x  = Const("x");
+    expr m1 = mk_metavar(1);
+    expr t  = mk_app(Fun({x,N}, m1), a);
+    expr s1 = instantiate_metavar(head_reduce_mmv(t, env), 1, Var(0));
+    expr s2 = head_reduce_mmv(instantiate_metavar(t, 1, Var(0)), env);
+    std::cout << instantiate_metavar(t, 1, Var(0)) << "\n";
+    std::cout << s1 << "\n";
+    std::cout << s2 << "\n";
+    lean_assert(s1 == s2);
+}
+
 int main() {
     tst1();
     tst2();
     tst3();
     tst4();
     tst5();
+    tst6();
     return has_violations() ? 1 : 0;
 }