michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library): add idx_metavar module

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-08 15:52:50 -07:00
parent 1c5c79fbc1
commit d6a483fe84
12 changed files with 126 additions and 91 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/CMakeLists.txt
View file

@ -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})

4
src/library/app_builder.cpp
View file

@ -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);
}

56
src/library/idx_metavar.cpp Normal file
View file

@ -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();
}
}

32
src/library/idx_metavar.h Normal file
View file

@ -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();
}

6
src/library/init_module.cpp
View file

@ -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();

67
src/library/match.cpp
View file

@ -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<expr> * 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<expr> 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<optional<level>> & lsubst, buffer<optional<expr>> & 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<unsigned, unsigned> 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");
}
}

24
src/library/match.h
View file

@ -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<expr> 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<level> 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.

6
src/library/tactic/rewrite_tactic.cpp
View file

@ -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

2
tests/lean/run/match1.lean
View file

@ -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))
*)

2
tests/lean/run/match2.lean
View file

@ -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)

8
tests/lua/hop1.lua
View file

@ -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)))))

8
tests/lua/hop2.lua
View file

@ -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)))