From 2cf9ca9345cac94c7da0022fd4ddbf19a5856694 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 29 Aug 2013 09:46:28 -0700 Subject: [PATCH] Add metavariable utilities. They will be used to refactor the elaborator. Signed-off-by: Leonardo de Moura --- src/library/CMakeLists.txt | 2 +- src/library/metavar.cpp | 262 +++++++++++++++++++++++++++++++ src/library/metavar.h | 118 ++++++++++++++ src/library/metavar_env.cpp | 46 ------ src/library/metavar_env.h | 13 +- src/library/printer.cpp | 25 ++- src/tests/library/CMakeLists.txt | 3 + src/tests/library/metavar.cpp | 103 ++++++++++++ 8 files changed, 508 insertions(+), 64 deletions(-) create mode 100644 src/library/metavar.cpp create mode 100644 src/library/metavar.h create mode 100644 src/tests/library/metavar.cpp diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index b12c8f000..57ce4b0d6 100644 --- a/src/library/CMakeLists.txt +++ b/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}) diff --git a/src/library/metavar.cpp b/src/library/metavar.cpp new file mode 100644 index 000000000..e5b947780 --- /dev/null +++ b/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 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 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(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(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(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(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(f)(e); +} +} diff --git a/src/library/metavar.h b/src/library/metavar.h new file mode 100644 index 000000000..4c0470dc3 --- /dev/null +++ b/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 idx >= + s. + + 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 idx > i 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 idx >= s. + + 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); +} + diff --git a/src/library/metavar_env.cpp b/src/library/metavar_env.cpp index d2491a19c..c84e766d3 100644 --- a/src/library/metavar_env.cpp +++ b/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 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 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), diff --git a/src/library/metavar_env.h b/src/library/metavar_env.h index 3e1d9319f..8e40cade8 100644 --- a/src/library/metavar_env.h +++ b/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 diff --git a/src/library/printer.cpp b/src/library/printer.cpp index c25f7a26a..793de9ed9 100644 --- a/src/library/printer.cpp +++ b/src/library/printer.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include #include "printer.h" +#include "metavar.h" #include "environment.h" #include "exception.h" @@ -54,10 +55,20 @@ struct print_expr_fn { } void print_app(expr const & a, context const & c) { - print_child(arg(a, 0), c); - for (unsigned i = 1; i < num_args(a); i++) { - out() << " "; - print_child(arg(a, i), 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); + } } } @@ -78,7 +89,11 @@ struct print_expr_fn { } break; case expr_kind::Constant: - out() << const_name(a); + if (is_metavar(a)) { + out() << "?M:" << metavar_idx(a); + } else { + out() << const_name(a); + } break; case expr_kind::App: print_app(a, c); diff --git a/src/tests/library/CMakeLists.txt b/src/tests/library/CMakeLists.txt index 2c99c3253..41349525d 100644 --- a/src/tests/library/CMakeLists.txt +++ b/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) diff --git a/src/tests/library/metavar.cpp b/src/tests/library/metavar.cpp new file mode 100644 index 000000000..15f2f4b3e --- /dev/null +++ b/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; +} + +