Add metavariable utilities. They will be used to refactor the elaborator.

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

src/library/CMakeLists.txt

@@ -1,3 +1,3 @@
 add_library(library basic_thms.cpp deep_copy.cpp max_sharing.cpp toplevel.cpp printer.cpp
-  formatter.cpp context_to_lambda.cpp state.cpp beta.cpp metavar_env.cpp elaborator.cpp)
+  formatter.cpp context_to_lambda.cpp state.cpp beta.cpp metavar.cpp metavar_env.cpp elaborator.cpp)
 target_link_libraries(library ${LEAN_LIBS})

src/library/metavar.cpp

@@ -0,0 +1,262 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "metavar.h"
+#include "replace.h"
+#include "for_each.h"
+
+namespace lean {
+static name g_metavar_prefix(name(name(name(0u), "library"), "metavar"));
+static name g_subst_prefix(name(name(name(0u), "library"), "subst"));
+static name g_lift_prefix(name(name(name(0u), "library"), "lift"));
+static name g_lower_prefix(name(name(name(0u), "library"), "lower"));
+
+expr mk_metavar(unsigned idx) {
+    return mk_constant(name(g_metavar_prefix, idx));
+}
+
+bool is_metavar(expr const & n) {
+    return is_constant(n) && !const_name(n).is_atomic() && const_name(n).get_prefix() == g_metavar_prefix;
+}
+
+unsigned metavar_idx(expr const & n) {
+    lean_assert(is_metavar(n));
+    return const_name(n).get_numeral();
+}
+
+struct found_metavar {};
+
+bool has_metavar(expr const & e) {
+    auto f = [](expr const & c, unsigned offset) {
+        if (is_metavar(c))
+            throw found_metavar();
+    };
+    try {
+        for_each_fn<decltype(f)> proc(f);
+        proc(e);
+        return false;
+    } catch (found_metavar) {
+        return true;
+    }
+}
+
+bool has_metavar(expr const & e, unsigned midx) {
+    auto f = [=](expr const & m, unsigned offset) {
+        if (is_metavar(m) && metavar_idx(m) == midx)
+            throw found_metavar();
+    };
+    try {
+        for_each_fn<decltype(f)> proc(f);
+        proc(e);
+        return false;
+    } catch (found_metavar) {
+        return true;
+    }
+}
+
+expr mk_subst_fn(unsigned idx) {
+    return mk_constant(name(g_subst_prefix, idx));
+}
+
+bool is_subst_fn(expr const & n) {
+    return is_constant(n) && !const_name(n).is_atomic() && const_name(n).get_prefix() == g_subst_prefix;
+}
+
+expr mk_subst(expr const & e, unsigned i, expr const & c) {
+    return mk_app(mk_subst_fn(i), e, c);
+}
+
+bool is_subst(expr const & e, unsigned & i, expr & c) {
+    if (is_app(e) && is_subst_fn(arg(e,0))) {
+        i = const_name(arg(e,0)).get_numeral();
+        c = arg(e,2);
+        return true;
+    } else {
+        return false;
+    }
+}
+
+bool is_subst(expr const & e) {
+    return is_app(e) && is_subst_fn(arg(e,0));
+}
+
+expr mk_lift_fn(unsigned s, unsigned n) {
+    return mk_constant(name(name(g_lift_prefix, s), n));
+}
+
+bool is_lift_fn(expr const & n) {
+    return
+        is_constant(n) &&
+        !const_name(n).is_atomic() &&
+        !const_name(n).get_prefix().is_atomic() &&
+        const_name(n).get_prefix().get_prefix() == g_lift_prefix;
+}
+
+expr mk_lift(expr const & e, unsigned s, unsigned n) {
+    return mk_app(mk_lift_fn(s, n), e);
+}
+
+bool is_lift(expr const & e, unsigned & s, unsigned & n) {
+    if (is_app(e) && is_lift_fn(arg(e,0))) {
+        name const & l = const_name(arg(e,0));
+        n = l.get_numeral();
+        s = l.get_prefix().get_numeral();
+        return true;
+    } else {
+        return false;
+    }
+}
+
+bool is_lift(expr const & e) {
+    return is_app(e) && is_lift_fn(arg(e,0));
+}
+
+expr mk_lower_fn(unsigned s, unsigned n) {
+    return mk_constant(name(name(g_lower_prefix, s), n));
+}
+
+bool is_lower_fn(expr const & n) {
+    return
+        is_constant(n) &&
+        !const_name(n).is_atomic() &&
+        !const_name(n).get_prefix().is_atomic() &&
+        const_name(n).get_prefix().get_prefix() == g_lower_prefix;
+}
+
+expr mk_lower(expr const & e, unsigned s, unsigned n) {
+    return mk_app(mk_lower_fn(s, n), e);
+}
+
+bool is_lower(expr const & e, unsigned & s, unsigned & n) {
+    if (is_app(e) && is_lower_fn(arg(e,0))) {
+        name const & l = const_name(arg(e,0));
+        n = l.get_numeral();
+        s = l.get_prefix().get_numeral();
+        return true;
+    } else {
+        return false;
+    }
+}
+
+bool is_lower(expr const & e) {
+    return is_app(e) && is_lower_fn(arg(e,0));
+}
+
+bool is_meta(expr const & e) {
+    return is_metavar(e) || is_subst(e) || is_lift(e) || is_lower(e);
+}
+
+expr lower_free_vars_mmv(expr const & e, unsigned s, unsigned n) {
+    if (n == 0)
+        return e;
+    lean_assert(s >= n);
+    auto f = [=](expr const & e, unsigned offset) -> expr {
+        if (is_var(e) && var_idx(e) >= s + offset) {
+            return mk_var(var_idx(e) - n);
+        } else if (is_meta(e)) {
+            return mk_lower(e, s + offset, n);
+        } else {
+            return e;
+        }
+    };
+    return replace_fn<decltype(f)>(f)(e);
+}
+
+expr lift_free_vars_mmv(expr const & e, unsigned s, unsigned n) {
+    if (n == 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) + n);
+        } else if (is_meta(e)) {
+            return mk_lift(e, s + offset, n);
+        } else {
+            return e;
+        }
+    };
+    return replace_fn<decltype(f)>(f)(e);
+}
+
+expr instantiate_free_var_mmv(expr const & e, unsigned i, expr const & c) {
+    auto f = [&](expr const & e, unsigned offset) -> expr {
+        if (is_var(e)) {
+            unsigned vidx = var_idx(e);
+            if (vidx == offset + i)
+                return lift_free_vars_mmv(c, 0, offset);
+            else if (vidx > offset + i)
+                return mk_var(vidx - 1);
+            else
+                return e;
+        } else if (is_meta(e)) {
+            return mk_lower(mk_subst(e, offset, lift_free_vars_mmv(c, 0, offset+1)), offset+1, 1);
+        } else {
+            return e;
+        }
+    };
+    return replace_fn<decltype(f)>(f)(e);
+}
+
+expr subst_mmv(expr const & e, unsigned i, expr const & c) {
+    auto f = [&](expr const & e, unsigned offset) -> expr {
+        if (is_var(e)) {
+            unsigned vidx = var_idx(e);
+            if (vidx == offset + i)
+                return lift_free_vars_mmv(c, 0, offset);
+            else
+                return e;
+        } else if (is_meta(e)) {
+            return mk_subst(e, offset, lift_free_vars_mmv(c, 0, offset));
+        } else {
+            return e;
+        }
+    };
+    return replace_fn<decltype(f)>(f)(e);
+}
+
+expr get_metavar(expr const & e) {
+    lean_assert(is_meta(e));
+    if (is_metavar(e)) {
+        return e;
+    } else {
+        return get_metavar(arg(e, 1));
+    }
+}
+
+expr instantiate_metavar_core(expr const & e, expr const & v) {
+    lean_assert(is_meta(e));
+    unsigned i, s, n;
+    expr c;
+    if (is_metavar(e)) {
+        return v;
+    } else if (is_subst(e, i, c)) {
+        return subst_mmv(instantiate_metavar_core(arg(e, 1), v), i, c);
+    } else if (is_lift(e, s, n)) {
+        return lift_free_vars_mmv(instantiate_metavar_core(arg(e, 1), v), s, n);
+    } else if (is_lower(e, s, n)) {
+        return lower_free_vars_mmv(instantiate_metavar_core(arg(e, 1), v), s, n);
+    } else {
+        lean_unreachable();
+        return e;
+    }
+}
+
+expr instantiate_metavar(expr const & e, unsigned midx, expr const & v) {
+    auto f = [=](expr const & e, unsigned offset) -> expr {
+        if (is_meta(e)) {
+            expr m = get_metavar(e);
+            lean_assert(is_metavar(m));
+            if (metavar_idx(m) == midx) {
+                return instantiate_metavar_core(e, v);
+            } else {
+                return e;
+            }
+        } else {
+            return e;
+        }
+    };
+    return replace_fn<decltype(f)>(f)(e);
+}
+}

src/library/metavar.h

@@ -0,0 +1,118 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "expr.h"
+
+namespace lean {
+/**
+    \brief Create a new metavariable with index \c idx.
+*/
+expr mk_metavar(unsigned idx);
+
+/**
+    \brief Return true iff \c n is a metavariable.
+*/
+bool is_metavar(expr const & n);
+
+/**
+    \brief Return the index of the given metavariable.
+    \pre is_metavar(n);
+*/
+unsigned metavar_idx(expr const & n);
+
+/**
+    \brief Return true iff the given expression contains a
+    metavariable
+*/
+bool has_metavar(expr const & e);
+
+/**
+    \brief Return true iff \c e contains a metavariable with index
+    \c midx
+*/
+bool has_metavar(expr const & e, unsigned midx);
+
+/**
+   \brief Version of lift_free_vars for expressions containing
+   metavariables. It will return a new expression such that the
+   index idx of free variables is increased by \c n when <tt>idx >=
+   s</tt>.
+
+   The suffix mmv stands for "modulo metavariables".
+*/
+expr lift_free_vars_mmv(expr const & e, unsigned s, unsigned n);
+
+/**
+   \brief Version of instantiate for expressions containing
+   metavariables. It will return a new expression such that the free
+   variables with index \c i are replaced with the expression \c v.
+   Moreover, the index \c idx of the free variables with <tt>idx > i</tt> is
+   lowered by 1.
+
+   The suffix mmv stands for "modulo metavariables".
+*/
+expr instantiate_free_var_mmv(expr const & e, unsigned i, expr const & v);
+
+/**
+   \brief Version of lower_free_vars for expressions containing
+   metavariables. It will return a new expression such that the
+   index \c idx of free variables is lowered by \c n when <tt>idx >= s</tt>.
+
+   The suffix mmv stands for "modulo metavariables".
+*/
+expr lower_free_vars_mmv(expr const & e, unsigned s, unsigned n);
+
+/**
+   \brief Instantiate the metavariable with index \c midx in \c e with
+   the expression \c v.
+*/
+expr instantiate_metavar(expr const & e, unsigned midx, expr const & v);
+
+/**
+   \brief Return true iff \c e is a delayed substitution expression
+   of the form (subst:i c v). The meaning of the expression is
+   substitute free variable \c i in \c c with expression \c v.
+*/
+bool is_subst(expr const & e, unsigned & i, expr & v);
+
+/**
+    \brief Return true iff \c e is a delayed substitution expression.
+*/
+bool is_subst(expr const & e);
+
+/**
+    \brief Return true iff \c e is a delayed lift expression of the
+    form (lift:s:n c). The meaning of the expression is lift the free
+    variables >= \c s by \c n in \c c.
+*/
+bool is_lift(expr const & e, unsigned & s, unsigned & n);
+
+/**
+    \brief Return true iff \c e is a delayed lift expression.
+*/
+bool is_lift(expr const & e);
+
+/**
+    \brief Return true iff \c e is a delayed lower expression of the
+    form (lower:s:n c). The meaning of the expression is lower the free
+    variables >= \c s by \c n in \c c.
+*/
+bool is_lower(expr const & e, unsigned & s, unsigned & n);
+
+/**
+    \brief Return true iff \c e is a delayed lower expression.
+*/
+bool is_lower(expr const & e);
+
+/**
+    \brief Return true iff \c e is a meta-variable, or a delayed
+    instantiation expression, or a delayed lift expression, or a
+    delayed lower expression.
+*/
+bool is_meta(expr const & e);
+}
+

src/library/metavar_env.cpp

@@ -17,52 +17,6 @@ Author: Leonardo de Moura
 #include "flet.h"
 
 namespace lean {
-static name g_metavar_prefix(name(name(name(0u), "library"), "metavar"));
-
-expr mk_metavar(unsigned idx) {
-    return mk_constant(name(g_metavar_prefix, idx));
-}
-
-bool is_metavar(expr const & n) {
-    return is_constant(n) && !const_name(n).is_atomic() && const_name(n).get_prefix() == g_metavar_prefix;
-}
-
-unsigned metavar_idx(expr const & n) {
-    lean_assert(is_metavar(n));
-    return const_name(n).get_numeral();
-}
-
-struct found_metavar {};
-
-bool has_metavar(expr const & e) {
-    auto f = [](expr const & c, unsigned offset) {
-        if (is_metavar(c))
-            throw found_metavar();
-    };
-    try {
-        for_each_fn<decltype(f)> proc(f);
-        proc(e);
-        return false;
-    } catch (found_metavar) {
-        return true;
-    }
-}
-
-/** \brief Return true iff \c e contains a metavariable with index midx */
-bool has_metavar(expr const & e, unsigned midx) {
-    auto f = [=](expr const & m, unsigned offset) {
-        if (is_metavar(m) && metavar_idx(m) == midx)
-            throw found_metavar();
-    };
-    try {
-        for_each_fn<decltype(f)> proc(f);
-        proc(e);
-        return false;
-    } catch (found_metavar) {
-        return true;
-    }
-}
-
 metavar_env::cell::cell(expr const & e, unsigned ctx_size, unsigned find):
     m_expr(e),
     m_ctx_size(ctx_size),

src/library/metavar_env.h

@@ -9,20 +9,9 @@ Author: Leonardo de Moura
 #include "environment.h"
 #include "context.h"
 #include "name_set.h"
+#include "metavar.h"
 
 namespace lean {
-/** \brief Create a metavariable with the given index */
-expr mk_metavar(unsigned idx);
-
-/** \brief Return true iff the given expression is a metavariable */
-bool is_metavar(expr const & n);
-
-/** \brief Return the index of the given metavariable */
-unsigned metavar_idx(expr const & n);
-
-/** \brief Return true iff the given expression contains a metavariable */
-bool has_metavar(expr const & e);
-
 /**
    \brief Metavariable environment. It is used for solving
    unification constraints generated by expression elaborator

src/library/printer.cpp

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include <algorithm>
 #include "printer.h"
+#include "metavar.h"
 #include "environment.h"
 #include "exception.h"
 
@@ -54,12 +55,22 @@ struct print_expr_fn {
     }
 
     void print_app(expr const & a, context const & c) {
+        unsigned i, s, n;
+        expr v;
+        if (is_lower(a, s, n)) {
+            out() << "lower:" << s << ":" << n << " "; print_child(arg(a, 1), c);
+        } else if (is_lift(a, s, n)) {
+            out() << "lift:" << s << ":" << n << " "; print_child(arg(a, 1), c);
+        } else if (is_subst(a, i, v)) {
+            out() << "subst:" << i << " "; print_child(arg(a, 1), c); out() << " "; print_child(v, context());
+        } else {
             print_child(arg(a, 0), c);
             for (unsigned i = 1; i < num_args(a); i++) {
                 out() << " ";
                 print_child(arg(a, i), c);
             }
         }
+    }
 
     void print_arrow_body(expr const & a, context const & c) {
         if (is_atomic(a) || is_arrow(a))
@@ -78,7 +89,11 @@ struct print_expr_fn {
             }
             break;
         case expr_kind::Constant:
+            if (is_metavar(a)) {
+                out() << "?M:" << metavar_idx(a);
+            } else {
                 out() << const_name(a);
+            }
             break;
         case expr_kind::App:
             print_app(a, c);

src/tests/library/CMakeLists.txt

@@ -4,3 +4,6 @@ add_test(implicit_args ${CMAKE_CURRENT_BINARY_DIR}/implicit_args)
 add_executable(beta beta.cpp)
 target_link_libraries(beta ${EXTRA_LIBS})
 add_test(beta ${CMAKE_CURRENT_BINARY_DIR}/beta)
+add_executable(metavar metavar.cpp)
+target_link_libraries(metavar ${EXTRA_LIBS})
+add_test(metavar ${CMAKE_CURRENT_BINARY_DIR}/metavar)

src/tests/library/metavar.cpp

@@ -0,0 +1,103 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "test.h"
+#include "metavar.h"
+#include "abstract.h"
+#include "printer.h"
+using namespace lean;
+
+static void tst1() {
+    expr N  = Const("N");
+    expr f  = Const("f");
+    expr x  = Const("x");
+    expr y  = Const("y");
+    expr a  = Const("a");
+    expr g  = Const("g");
+    expr h  = Const("h");
+    expr m1 = mk_metavar(1);
+    expr m2 = mk_metavar(2);
+    expr t = f(Var(0), Fun({x, N}, f(Var(1), x, Fun({y, N}, f(Var(2), x, y)))));
+    expr r = instantiate_free_var_mmv(t, 0, g(m1, m2));
+    std::cout << r << std::endl;
+    r = instantiate_metavar(r, 2, Var(2));
+    std::cout << r << std::endl;
+    r = instantiate_metavar(r, 1, h(Var(3)));
+    std::cout << r << std::endl;
+    lean_assert(r == f(g(h(Var(3)), Var(2)), Fun({x, N}, f(g(h(Var(4)), Var(3)), x, Fun({y, N}, f(g(h(Var(5)), Var(4)), x, y))))));
+}
+
+static void tst2() {
+    expr f  = Const("f");
+    expr g  = Const("g");
+    expr a  = Const("a");
+    expr m1 = mk_metavar(1);
+    expr t  = f(m1, Var(0));
+    expr r = instantiate_free_var_mmv(t, 0, a);
+    r = instantiate_metavar(r, 1, g(Var(0)));
+    std::cout << r << std::endl;
+    lean_assert(r == f(g(a), a));
+}
+
+static void tst3() {
+    expr f  = Const("f");
+    expr g  = Const("g");
+    expr a  = Const("a");
+    expr m1 = mk_metavar(1);
+    expr t  = f(m1, Var(0), Var(2));
+    expr r = instantiate_free_var_mmv(t, 0, a);
+    r = instantiate_metavar(r, 1, g(Var(0), Var(1)));
+    std::cout << r << std::endl;
+    lean_assert(r == f(g(a,Var(0)), a, Var(1)));
+}
+
+static void tst4() {
+    expr f  = Const("f");
+    expr g  = Const("g");
+    expr a  = Const("a");
+    expr m1 = mk_metavar(1);
+    expr t  = f(m1, Var(1), Var(2));
+    expr r  = lift_free_vars_mmv(t, 1, 2);
+    std::cout << r << std::endl;
+    r = instantiate_free_var_mmv(r, 0, a);
+    std::cout << r << std::endl;
+    r = instantiate_metavar(r, 1, g(Var(0), Var(1)));
+    std::cout << r << std::endl;
+    lean_assert(r == f(g(a,Var(2)), Var(2), Var(3)));
+}
+
+static void tst5() {
+    expr N  = Const("N");
+    expr f  = Const("f");
+    expr x  = Const("x");
+    expr y  = Const("y");
+    expr a  = Const("a");
+    expr g  = Const("g");
+    expr h  = Const("h");
+    expr m1 = mk_metavar(1);
+    expr m2 = mk_metavar(2);
+    expr t = f(Var(0), Fun({x, N}, f(Var(1), Var(2), x, Fun({y, N}, f(Var(2), x, y)))));
+    expr r = instantiate_free_var_mmv(t, 0, g(m1));
+    std::cout << r << std::endl;
+    r = instantiate_free_var_mmv(r, 0, h(m2));
+    std::cout << r << std::endl;
+    r = instantiate_metavar(r, 1, f(Var(0)));
+    std::cout << r << std::endl;
+    r = instantiate_metavar(r, 2, Var(2));
+    std::cout << r << std::endl;
+    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))))));
+}
+
+int main() {
+    tst1();
+    tst2();
+    tst3();
+    tst4();
+    tst5();
+    return has_violations() ? 1 : 0;
+}
+
+