From d6a483fe84468ff4cd62e399027c8774b2689d3a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 8 Jun 2015 15:52:50 -0700 Subject: [PATCH] feat(library): add idx_metavar module --- src/library/CMakeLists.txt | 2 +- src/library/app_builder.cpp | 4 +- src/library/idx_metavar.cpp | 56 ++++++++++++++++++++++ src/library/idx_metavar.h | 32 +++++++++++++ src/library/init_module.cpp | 6 +-- src/library/match.cpp | 67 ++++++--------------------- src/library/match.h | 24 +++------- src/library/tactic/rewrite_tactic.cpp | 6 +-- tests/lean/run/match1.lean | 2 +- tests/lean/run/match2.lean | 2 +- tests/lua/hop1.lua | 8 ++-- tests/lua/hop2.lua | 8 ++-- 12 files changed, 126 insertions(+), 91 deletions(-) create mode 100644 src/library/idx_metavar.cpp create mode 100644 src/library/idx_metavar.h diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index bb6347d17..8b6690f4d 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -14,6 +14,6 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp local_context.cpp choice_iterator.cpp pp_options.cpp unfold_macros.cpp app_builder.cpp projection.cpp abbreviation.cpp relation_manager.cpp export.cpp user_recursors.cpp - class_instance_synth.cpp) + class_instance_synth.cpp idx_metavar.cpp) target_link_libraries(library ${LEAN_LIBS}) diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp index a34e52194..dc6105882 100644 --- a/src/library/app_builder.cpp +++ b/src/library/app_builder.cpp @@ -66,7 +66,7 @@ struct app_builder::imp { // Make sure m_levels contains at least nlvls metavariable universe levels void ensure_levels(unsigned nlvls) { while (m_levels.size() <= nlvls) { - level new_lvl = mk_idx_meta_univ(m_levels.size() - 1); + level new_lvl = mk_idx_metauniv(m_levels.size() - 1); levels new_lvls = append(m_levels.back(), levels(new_lvl)); m_levels.push_back(new_lvls); } @@ -110,7 +110,7 @@ struct app_builder::imp { domain_types.push_back(binding_domain(type)); // TODO(Leo): perhaps, we should cache the result of this while-loop. // The result of this computation can be reused in future calls. - expr meta = mk_idx_meta(idx, binding_domain(type)); + expr meta = mk_idx_metavar(idx, binding_domain(type)); idx++; type = instantiate(binding_body(type), meta); } diff --git a/src/library/idx_metavar.cpp b/src/library/idx_metavar.cpp new file mode 100644 index 000000000..b5989ef89 --- /dev/null +++ b/src/library/idx_metavar.cpp @@ -0,0 +1,56 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "util/interrupt.h" +#include "library/idx_metavar.h" + +#ifndef LEAN_INSTANTIATE_METAIDX_CACHE_CAPACITY +#define LEAN_INSTANTIATE_METAIDX_CACHE_CAPACITY 1024*8 +#endif + +namespace lean { +static name * g_tmp_prefix = nullptr; + +void initialize_idx_metavar() { + g_tmp_prefix = new name(name::mk_internal_unique_name()); +} + +void finalize_idx_metavar() { + delete g_tmp_prefix; +} + +level mk_idx_metauniv(unsigned i) { + return mk_meta_univ(name(*g_tmp_prefix, i)); +} + +expr mk_idx_metavar(unsigned i, expr const & type) { + return mk_metavar(name(*g_tmp_prefix, i), type); +} + +bool is_idx_metauniv(level const & l) { + if (!is_meta(l)) + return false; + name const & n = meta_id(l); + return !n.is_atomic() && n.is_numeral() && n.get_prefix() == *g_tmp_prefix; +} + +unsigned to_meta_idx(level const & l) { + lean_assert(is_idx_meta_univ(l)); + return meta_id(l).get_numeral(); +} + +bool is_idx_metavar(expr const & e) { + if (!is_metavar(e)) + return false; + name const & n = mlocal_name(e); + return !n.is_atomic() && n.is_numeral() && n.get_prefix() == *g_tmp_prefix; +} + +unsigned to_meta_idx(expr const & e) { + lean_assert(is_idx_meta(e)); + return mlocal_name(e).get_numeral(); +} +} diff --git a/src/library/idx_metavar.h b/src/library/idx_metavar.h new file mode 100644 index 000000000..87e6881b3 --- /dev/null +++ b/src/library/idx_metavar.h @@ -0,0 +1,32 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "kernel/expr.h" +namespace lean { +/** \brief Create a universe level metavariable that can be used as a placeholder in #match. + + \remark The index \c i is encoded in the hierarchical name, and can be quickly accessed. + In the match procedure the substitution is also efficiently represented as an array (aka buffer). +*/ +level mk_idx_metauniv(unsigned i); +/** \brief Return true iff \c l is a metauniverse created using \c mk_idx_metauniv */ +bool is_idx_metauniv(level const & l); +unsigned to_meta_idx(level const & l); + +/** \brief Create a special metavariable that can be used as a placeholder in #match. + + \remark The index \c i is encoded in the hierarchical name, and can be quickly accessed. + In the match procedure the substitution is also efficiently represented as an array (aka buffer). +*/ +expr mk_idx_metavar(unsigned i, expr const & type); +/** \brief Return true iff \c l is a metavariable created using \c mk_idx_metavar */ +bool is_idx_metavar(expr const & l); +unsigned to_meta_idx(expr const & e); + +void initialize_idx_metavar(); +void finalize_idx_metavar(); +} diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index dc0ac2cb4..64bc38346 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -26,7 +26,7 @@ Author: Leonardo de Moura #include "library/unifier_plugin.h" #include "library/io_state.h" #include "library/kernel_bindings.h" -#include "library/match.h" +#include "library/idx_metavar.h" #include "library/sorry.h" #include "library/placeholder.h" #include "library/print.h" @@ -46,7 +46,7 @@ void initialize_library_module() { initialize_fingerprint(); initialize_print(); initialize_placeholder(); - initialize_match(); + initialize_idx_metavar(); initialize_kernel_bindings(); initialize_io_state(); initialize_unifier(); @@ -110,7 +110,7 @@ void finalize_library_module() { finalize_unifier(); finalize_io_state(); finalize_kernel_bindings(); - finalize_match(); + finalize_idx_metavar(); finalize_placeholder(); finalize_print(); finalize_fingerprint(); diff --git a/src/library/match.cpp b/src/library/match.cpp index 85567159d..33940312b 100644 --- a/src/library/match.cpp +++ b/src/library/match.cpp @@ -13,50 +13,9 @@ Author: Leonardo de Moura #include "library/kernel_bindings.h" #include "library/locals.h" #include "library/match.h" +#include "library/idx_metavar.h" namespace lean { -static name * g_tmp_prefix = nullptr; - -void initialize_match() { - g_tmp_prefix = new name(name::mk_internal_unique_name()); -} - -void finalize_match() { - delete g_tmp_prefix; -} - -level mk_idx_meta_univ(unsigned i) { - return mk_meta_univ(name(*g_tmp_prefix, i)); -} - -expr mk_idx_meta(unsigned i, expr const & type) { - return mk_metavar(name(*g_tmp_prefix, i), type); -} - -bool is_idx_meta_univ(level const & l) { - if (!is_meta(l)) - return false; - name const & n = meta_id(l); - return !n.is_atomic() && n.is_numeral() && n.get_prefix() == *g_tmp_prefix; -} - -unsigned to_meta_idx(level const & l) { - lean_assert(is_idx_meta_univ(l)); - return meta_id(l).get_numeral(); -} - -bool is_idx_meta(expr const & e) { - if (!is_metavar(e)) - return false; - name const & n = mlocal_name(e); - return !n.is_atomic() && n.is_numeral() && n.get_prefix() == *g_tmp_prefix; -} - -unsigned to_meta_idx(expr const & e) { - lean_assert(is_idx_meta(e)); - return mlocal_name(e).get_numeral(); -} - class match_fn : public match_context { unsigned m_esubst_sz; optional * m_esubst; @@ -280,7 +239,7 @@ class match_fn : public match_context { } bool match_level(level const & p, level const & l) { - if (is_idx_meta_univ(p)) { + if (is_idx_metauniv(p)) { auto s = _get_subst(p); if (s) { return match_level_core(*s, l); @@ -370,7 +329,7 @@ class match_fn : public match_context { } bool _match(expr const & p, expr const & t) { - if (is_idx_meta(p)) { + if (is_idx_metavar(p)) { auto s = _get_subst(p); if (s) { return match_core(*s, t); @@ -381,7 +340,7 @@ class match_fn : public match_context { } else if (is_app(p)) { buffer args; expr const & f = get_app_rev_args(p, args); - if (is_idx_meta(f)) { + if (is_idx_metavar(f)) { // higher-order pattern case auto s = _get_subst(f); if (s) { @@ -426,7 +385,7 @@ bool match(expr const & p, expr const & t, name_subst, plugin, assigned).match(p, t); else return match_fn(lsubst_sz, lsubst, esubst_sz, esubst, - name_generator(*g_tmp_prefix), name_subst, plugin, assigned).match(p, t); + name_generator(), name_subst, plugin, assigned).match(p, t); } bool match(expr const & p, expr const & t, buffer> & lsubst, buffer> & esubst, @@ -449,7 +408,7 @@ bool whnf_match_plugin::on_failure(expr const & p, expr const & t, match_context static unsigned updt_idx_meta_univ_range(level const & l, unsigned r) { for_each(l, [&](level const & l) { if (!has_meta(l)) return false; - if (is_idx_meta_univ(l)) { + if (is_idx_metauniv(l)) { unsigned new_r = to_meta_idx(l) + 1; if (new_r > r) r = new_r; @@ -471,7 +430,7 @@ static pair get_idx_meta_univ_ranges(expr const & e) { rlvl = updt_idx_meta_univ_range(l, rlvl); if (is_sort(e)) rlvl = updt_idx_meta_univ_range(sort_level(e), rlvl); - if (is_idx_meta(e)) + if (is_idx_metavar(e)) rexp = std::max(to_meta_idx(e) + 1, rexp); return true; }); @@ -542,12 +501,12 @@ static int match(lua_State * L) { return 2; } -static int mk_idx_meta_univ(lua_State * L) { - return push_level(L, mk_idx_meta_univ(luaL_checkinteger(L, 1))); +static int mk_idx_metauniv(lua_State * L) { + return push_level(L, mk_idx_metauniv(luaL_checkinteger(L, 1))); } -static int mk_idx_meta(lua_State * L) { - return push_expr(L, mk_idx_meta(luaL_checkinteger(L, 1), to_expr(L, 2))); +static int mk_idx_metavar(lua_State * L) { + return push_expr(L, mk_idx_metavar(luaL_checkinteger(L, 1), to_expr(L, 2))); } void open_match(lua_State * L) { @@ -558,8 +517,8 @@ void open_match(lua_State * L) { SET_GLOBAL_FUN(mk_whnf_match_plugin, "whnf_match_plugin"); SET_GLOBAL_FUN(match_plugin_ref_pred, "is_match_plugin"); - SET_GLOBAL_FUN(mk_idx_meta_univ, "mk_idx_meta_univ"); - SET_GLOBAL_FUN(mk_idx_meta, "mk_idx_meta"); + SET_GLOBAL_FUN(mk_idx_metauniv, "mk_idx_metauniv"); + SET_GLOBAL_FUN(mk_idx_metavar, "mk_idx_metavar"); SET_GLOBAL_FUN(match, "match"); } } diff --git a/src/library/match.h b/src/library/match.h index b17d68072..b917723f8 100644 --- a/src/library/match.h +++ b/src/library/match.h @@ -13,22 +13,9 @@ Author: Leonardo de Moura #include "util/name_map.h" #include "kernel/expr.h" #include "kernel/environment.h" +#include "library/idx_metavar.h" namespace lean { -/** \brief Create a universe level metavariable that can be used as a placeholder in #match. - - \remark The index \c i is encoded in the hierarchical name, and can be quickly accessed. - In the match procedure the substitution is also efficiently represented as an array (aka buffer). -*/ -level mk_idx_meta_univ(unsigned i); - -/** \brief Create a special metavariable that can be used as a placeholder in #match. - - \remark The index \c i is encoded in the hierarchical name, and can be quickly accessed. - In the match procedure the substitution is also efficiently represented as an array (aka buffer). -*/ -expr mk_idx_meta(unsigned i, expr const & type); - /** \brief Context for match_plugins. */ class match_context { public: @@ -36,14 +23,15 @@ public: virtual name mk_name() = 0; /** \brief Given a variable \c x, return its assignment (if available) */ virtual optional get_subst(expr const & x) const = 0; - /** \brief Given a universe level meta-variable \c x (created using #mk_idx_meta_univ), return its assignment (if available) */ + /** \brief Given a universe level meta-variable \c x (created using #mk_idx_metauniv), + return its assignment (if available) */ virtual optional get_subst(level const & x) const = 0; /** \brief Assign the variable \c x to \c e \pre \c x is not assigned */ virtual void assign(expr const & x, expr const & e) = 0; /** \brief Assign the variable \c x to \c l - \pre \c x is not assigned, \c x was created using #mk_idx_meta_univ. + \pre \c x is not assigned, \c x was created using #mk_idx_metauniv. */ virtual void assign(level const & x, level const & l) = 0; virtual bool match(expr const & p, expr const & t) = 0; @@ -59,7 +47,7 @@ public: virtual ~match_plugin() {} /** \brief The following method is invoked before the matcher tries to process \c p and \c t. The method is only invoked when \c p and \c t have the same kind, - \c p is not a special metavariable created using \c mk_idx_meta, and + \c p is not a special metavariable created using \c mk_idx_metavar, and \c p and \c t are not structurally identical. The result should be: @@ -87,7 +75,7 @@ public: /** \brief Matching for higher-order patterns. Return true iff \c t matches the higher-order pattern \c p. The substitution is stored in \c subst. Note that, this procedure treats "special" meta-variables - (created using #mk_idx_meta_univ and #mk_idx_meta) as placeholders. The substitution of these + (created using #mk_idx_metauniv and #mk_idx_metavar) as placeholders. The substitution of these metavariable can be quickly accessed using an index stored in them. The parameters \c esubst and \c lsubst store the substitutions for them. There are just buffers. diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp index 7f2e35dff..99902b532 100644 --- a/src/library/tactic/rewrite_tactic.cpp +++ b/src/library/tactic/rewrite_tactic.cpp @@ -885,7 +885,7 @@ class rewrite_fn { return some_level(*it); } else { unsigned next_idx = m_lsubst.size(); - level r = mk_idx_meta_univ(next_idx); + level r = mk_idx_metauniv(next_idx); m_lsubst.push_back(none_level()); lmap.insert(meta_id(l), r); return some_level(r); @@ -908,7 +908,7 @@ class rewrite_fn { return some_expr(e); // done } else if (is_lambda(e)) { unsigned next_idx = m_esubst.size(); - expr r = mk_idx_meta(next_idx, m_tc->infer(e).first); + expr r = mk_idx_metavar(next_idx, m_tc->infer(e).first); m_esubst.push_back(none_expr()); return some_expr(r); } else if (is_meta(e)) { @@ -916,7 +916,7 @@ class rewrite_fn { return some_expr(*it); } else { unsigned next_idx = m_esubst.size(); - expr r = mk_idx_meta(next_idx, m_tc->infer(e).first); + expr r = mk_idx_metavar(next_idx, m_tc->infer(e).first); m_esubst.push_back(none_expr()); if (no_meta_args(e)) emap.insert(e, r); // cache only if arguments of e are not metavariables diff --git a/tests/lean/run/match1.lean b/tests/lean/run/match1.lean index ef91357f4..e1b8298ed 100644 --- a/tests/lean/run/match1.lean +++ b/tests/lean/run/match1.lean @@ -25,6 +25,6 @@ local f = Const("f") local two1 = Const("two1") local two2 = Const("two2") local succ = Const({"nat", "succ"}) -local V0 = mk_idx_meta(0, nat) +local V0 = mk_idx_metavar(0, nat) tst_match(f(succ(V0), two1), f(two2, two2)) *) diff --git a/tests/lean/run/match2.lean b/tests/lean/run/match2.lean index 508767041..6569da0d9 100644 --- a/tests/lean/run/match2.lean +++ b/tests/lean/run/match2.lean @@ -27,7 +27,7 @@ local f = Const("f") local g = Const("g") local a = Const("a") local b = Const("b") -local x = mk_idx_meta(0, nat) +local x = mk_idx_metavar(0, nat) local p = g(x, f(x, a)) local t = g(a, f(b, a)) tst_match(p, t) diff --git a/tests/lua/hop1.lua b/tests/lua/hop1.lua index 31c0042bd..427e59102 100644 --- a/tests/lua/hop1.lua +++ b/tests/lua/hop1.lua @@ -14,15 +14,15 @@ local a = Const("a") local b = Const("b") local x = Local("x", N) local y = Local("y", N) -local V0 = mk_idx_meta(0, N) -local V1 = mk_idx_meta(1, N) +local V0 = mk_idx_metavar(0, N) +local V1 = mk_idx_metavar(1, N) tst_match(f(V0, V0), f(a, a)) tst_match(f(V0, V1), f(a, b)) -local F0 = mk_idx_meta(0, Pi(x, y, N)) +local F0 = mk_idx_metavar(0, Pi(x, y, N)) tst_match(F0(x, y), f(x, f(x, y))) assert(not match(F0(x, x), f(x, f(x, y)))) assert(not match(F0(x), f(x, y))) -local F0 = mk_idx_meta(0, Pi(x, N)) +local F0 = mk_idx_metavar(0, Pi(x, N)) tst_match(Pi(x, y, F0(x)), Pi(x, y, f(f(x)))) tst_match(Fun(x, y, F0(x)), Fun(x, y, f(f(x)))) assert(match(Pi(x, F0(x)), Pi(x, y, f(f(x))))) diff --git a/tests/lua/hop2.lua b/tests/lua/hop2.lua index c1f561890..e55eb9b6d 100644 --- a/tests/lua/hop2.lua +++ b/tests/lua/hop2.lua @@ -21,12 +21,12 @@ local u2 = mk_global_univ("u2") local z = level() local f = Const("f", {u1, z}) local f2 = Const("f", {u1, u1+1}) -local fp = Const("f", {mk_idx_meta_univ(0), mk_idx_meta_univ(1)}) -local V0 = mk_idx_meta(0, N) -local V1 = mk_idx_meta(1, N) +local fp = Const("f", {mk_idx_metauniv(0), mk_idx_metauniv(1)}) +local V0 = mk_idx_metavar(0, N) +local V1 = mk_idx_metavar(1, N) tst_match(fp(V0, V0), f(a, a)) tst_match(fp(V0, V1), f2(a, b)) -local F0 = mk_idx_meta(0, Pi(x, y, N)) +local F0 = mk_idx_metavar(0, Pi(x, y, N)) tst_match(F0(x, y), f(x, f(x, y))) assert(not match(F0(x, x), f(x, f(x, y)))) assert(not match(F0(x), f(x, y)))