feat(library/hop_match): port higher-order (pattern) matcher to Lean 0.2, we still have to implement support for universe levels
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
2dca68e645
commit
552be37d48
7 changed files with 174 additions and 343 deletions
|
|
@ -6,7 +6,7 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
|
|||
update_declaration.cpp choice.cpp scoped_ext.cpp locals.cpp
|
||||
standard_kernel.cpp hott_kernel.cpp
|
||||
unifier.cpp unifier_plugin.cpp inductive_unifier_plugin.cpp
|
||||
explicit.cpp num.cpp string.cpp opaque_hints.cpp head_map.cpp)
|
||||
# hop_match.cpp)
|
||||
explicit.cpp num.cpp string.cpp opaque_hints.cpp head_map.cpp
|
||||
hop_match.cpp)
|
||||
|
||||
target_link_libraries(library ${LEAN_LIBS})
|
||||
|
|
|
|||
|
|
@ -1,373 +1,187 @@
|
|||
/*
|
||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
||||
Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include "util/optional.h"
|
||||
#include "util/buffer.h"
|
||||
#include "kernel/free_vars.h"
|
||||
#include "kernel/abstract.h"
|
||||
#include "kernel/instantiate.h"
|
||||
#include "kernel/kernel.h"
|
||||
#include "kernel/for_each_fn.h"
|
||||
#include "kernel/replace_visitor.h"
|
||||
#include "library/equality.h"
|
||||
#include "library/kernel_bindings.h"
|
||||
#include "library/locals.h"
|
||||
#include "library/hop_match.h"
|
||||
|
||||
namespace lean {
|
||||
|
||||
class hop_match_fn {
|
||||
buffer<optional<expr>> & m_subst;
|
||||
buffer<expr> m_vars;
|
||||
optional<ro_environment> m_env;
|
||||
optional<ro_metavar_env> m_menv;
|
||||
name_map<name> * m_name_subst;
|
||||
buffer<optional<expr>> & m_subst;
|
||||
name_generator m_ngen;
|
||||
name_map<name> * m_name_subst;
|
||||
hop_matcher_plugin const * m_plugin;
|
||||
|
||||
bool is_free_var(expr const & x, unsigned ctx_size) const {
|
||||
return is_var(x) && var_idx(x) >= ctx_size;
|
||||
void assign(expr const & p, expr const & t) {
|
||||
lean_assert(var_idx(p) < m_subst.size());
|
||||
unsigned vidx = var_idx(p);
|
||||
unsigned sz = m_subst.size();
|
||||
m_subst[sz - vidx - 1] = t;
|
||||
}
|
||||
|
||||
bool is_locally_bound(expr const & x, unsigned ctx_size) const {
|
||||
return is_var(x) && var_idx(x) < ctx_size;
|
||||
}
|
||||
|
||||
expr lift_free_vars(expr const & e, unsigned d) const { return ::lean::lift_free_vars(e, d, m_menv); }
|
||||
expr lower_free_vars(expr const & e, unsigned s, unsigned d) const { return ::lean::lower_free_vars(e, s, d, m_menv); }
|
||||
bool has_free_var(expr const & e, unsigned i) const { return ::lean::has_free_var(e, i, m_menv); }
|
||||
bool has_free_var(expr const & e, unsigned low, unsigned high) const { return ::lean::has_free_var(e, low, high, m_menv); }
|
||||
expr apply_beta(expr f, unsigned num_args, expr const * args) const { return ::lean::apply_beta(f, num_args, args, m_menv); }
|
||||
bool has_free_var_ge(expr const & e, unsigned low) const { return ::lean::has_free_var_ge(e, low, m_menv); }
|
||||
|
||||
optional<expr> get_subst(expr const & x, unsigned ctx_size) const {
|
||||
lean_assert(is_free_var(x, ctx_size));
|
||||
unsigned vidx = var_idx(x) - ctx_size;
|
||||
optional<expr> get_subst(expr const & x) const {
|
||||
unsigned vidx = var_idx(x);
|
||||
unsigned sz = m_subst.size();
|
||||
if (vidx >= sz)
|
||||
throw exception("ill-formed higher-order matching problem");
|
||||
return m_subst[sz - vidx - 1];
|
||||
}
|
||||
|
||||
bool has_locally_bound_var(expr const & t, unsigned ctx_size) const {
|
||||
return has_free_var(t, 0, ctx_size);
|
||||
}
|
||||
|
||||
void assign(expr const & p, expr const & t, unsigned ctx_size) {
|
||||
lean_assert(is_free_var(p, ctx_size));
|
||||
lean_assert(!get_subst(p, ctx_size));
|
||||
unsigned vidx = var_idx(p) - ctx_size;
|
||||
unsigned sz = m_subst.size();
|
||||
m_subst[sz - vidx - 1] = t;
|
||||
}
|
||||
|
||||
bool args_are_distinct_locally_bound_vars(expr const & p, unsigned ctx_size, buffer<expr> & vars) {
|
||||
lean_assert(is_app(p));
|
||||
vars.clear();
|
||||
unsigned num = num_args(p);
|
||||
for (unsigned i = 1; i < num; i++) {
|
||||
expr const & v = arg(p, i);
|
||||
if (!is_locally_bound(v, ctx_size))
|
||||
bool args_are_distinct_locals(buffer<expr> const & args) {
|
||||
for (auto it = args.begin(); it != args.end(); it++) {
|
||||
if (!is_local(*it) || contains_local(*it, args.begin(), it))
|
||||
return false;
|
||||
if (std::find(vars.begin(), vars.end(), v) != vars.end())
|
||||
return false;
|
||||
vars.push_back(v);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Return t' when all locally bound variables in \c t occur in vars at positions [0, vars_size).
|
||||
The locally bound variables occurring in \c t are replaced using the following mapping:
|
||||
|
||||
vars[vars_size - 1] ==> #0
|
||||
...
|
||||
vars[0] ==> #vars_size - 1
|
||||
|
||||
None is returned if \c t contains a locally bound variable that does not occur in \c vars.
|
||||
Remark: vars_size <= vars.size()
|
||||
*/
|
||||
optional<expr> proj_core(expr const & t, unsigned ctx_size, buffer<expr> const & vars, unsigned vars_size) {
|
||||
bool failed = false;
|
||||
expr r = replace(t, [&](expr const & e, unsigned offset) -> expr {
|
||||
if (is_var(e)) {
|
||||
unsigned vidx = var_idx(e);
|
||||
if (vidx < offset)
|
||||
return e;
|
||||
vidx -= offset;
|
||||
if (vidx < ctx_size) {
|
||||
// e is locally bound
|
||||
for (unsigned i = 0; i < vars_size; i++) {
|
||||
if (var_idx(vars[i]) == vidx)
|
||||
return mk_var(offset + vars_size - i - 1);
|
||||
}
|
||||
failed = true;
|
||||
return e;
|
||||
} else if (ctx_size != vars_size) {
|
||||
return mk_var(offset + vidx - ctx_size + vars_size);
|
||||
} else {
|
||||
return e;
|
||||
}
|
||||
} else {
|
||||
return e;
|
||||
}
|
||||
});
|
||||
if (failed)
|
||||
optional<expr> proj(expr const & t, buffer<expr> const & args) {
|
||||
expr r = Fun(args, t);
|
||||
if (has_local(r))
|
||||
return none_expr();
|
||||
else
|
||||
return some_expr(r);
|
||||
}
|
||||
|
||||
// We say \c t has a simple projection when it is of the form (f v1 ... vn)
|
||||
// where f does no contain locally bound variables, and v1 ... vn are exactly the variables in vars.
|
||||
// In this case, the proj procedure can return f instead of (fun xn .... x1, f x1 ... xn)
|
||||
bool is_simple_proj(expr const & t, unsigned ctx_size, buffer<expr> const & vars) {
|
||||
if (is_app(t) && !has_locally_bound_var(arg(t, 0), ctx_size) && num_args(t) == vars.size() + 1) {
|
||||
for (unsigned i = 0; i < vars.size(); i++)
|
||||
if (arg(t, i+1) != vars[i])
|
||||
return false;
|
||||
return true;
|
||||
} else {
|
||||
bool match_plugin(expr const & p, expr const & t) {
|
||||
if (!m_plugin)
|
||||
return false;
|
||||
}
|
||||
return (*m_plugin)(p, t, m_subst, m_ngen.mk_child());
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Return <tt>(fun (x1 ... xn) t')</tt> if all locally bound variables in \c t occur in vars.
|
||||
\c n is the size of \c vars.
|
||||
None is returned if \c t contains a locally bound variable that does not occur in \c vars.
|
||||
*/
|
||||
optional<expr> proj(expr const & t, context const & ctx, unsigned ctx_size, buffer<expr> const & vars) {
|
||||
if (is_simple_proj(t, ctx_size, vars)) {
|
||||
return some_expr(lower_free_vars(arg(t, 0), ctx_size, ctx_size));
|
||||
bool match_binding(expr p, expr t) {
|
||||
lean_assert(is_binding(p) && is_binding(t));
|
||||
buffer<expr> ls;
|
||||
expr_kind k = p.kind();
|
||||
while (p.kind() == k && t.kind() == k) {
|
||||
if (m_name_subst)
|
||||
(*m_name_subst)[binding_name(p)] = binding_name(t);
|
||||
expr p_d = instantiate_rev(binding_domain(p), ls.size(), ls.data());
|
||||
expr t_d = instantiate_rev(binding_domain(t), ls.size(), ls.data());
|
||||
if (!match(p_d, t_d))
|
||||
return false;
|
||||
expr l = mk_local(m_ngen.next(), binding_name(t), t_d, binding_info(t));
|
||||
ls.push_back(l);
|
||||
p = binding_body(p);
|
||||
t = binding_body(t);
|
||||
}
|
||||
optional<expr> t_prime = proj_core(t, ctx_size, vars, vars.size());
|
||||
if (!t_prime)
|
||||
return none_expr();
|
||||
expr r = *t_prime;
|
||||
unsigned i = vars.size();
|
||||
while (i > 0) {
|
||||
--i;
|
||||
unsigned vidx = var_idx(vars[i]);
|
||||
auto p = lookup_ext(ctx, vidx);
|
||||
context_entry const & entry = p.first;
|
||||
context entry_ctx = p.second;
|
||||
if (!entry.get_domain())
|
||||
return none_expr();
|
||||
expr d = *entry.get_domain();
|
||||
optional<expr> new_d = proj_core(d, entry_ctx.size(), vars, i);
|
||||
if (!new_d)
|
||||
return none_expr();
|
||||
r = mk_lambda(entry.get_name(), *new_d, r);
|
||||
}
|
||||
return some_expr(r);
|
||||
if (p.kind() == k || t.kind() == k)
|
||||
return false;
|
||||
p = instantiate_rev(p, ls.size(), ls.data());
|
||||
t = instantiate_rev(t, ls.size(), ls.data());
|
||||
return match(p, t);
|
||||
}
|
||||
|
||||
optional<expr> unfold_constant(expr const & c) {
|
||||
if (is_constant(c)) {
|
||||
auto obj = (*m_env)->find_object(const_name(c));
|
||||
if (obj && (obj->is_definition() || obj->is_builtin()))
|
||||
return some_expr(obj->get_value());
|
||||
}
|
||||
return none_expr();
|
||||
}
|
||||
|
||||
bool match_constant(expr const & p, expr const & t) {
|
||||
if (p == t)
|
||||
bool match_macro(expr const & p, expr const & t) {
|
||||
if (macro_def(p) == macro_def(t) && macro_num_args(p) == macro_num_args(t)) {
|
||||
for (unsigned i = 0; i < macro_num_args(p); i++) {
|
||||
if (!match(macro_arg(p, i), macro_arg(t, i)))
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
auto new_p = unfold_constant(p);
|
||||
if (new_p)
|
||||
return match_constant(*new_p, t);
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Return true iff all free variables in the pattern \c p are assigned.
|
||||
*/
|
||||
bool all_free_vars_are_assigned(expr const & p, unsigned ctx_size) const {
|
||||
bool result = true;
|
||||
for_each(p, [&](expr const & v, unsigned offset) {
|
||||
if (!result)
|
||||
return false;
|
||||
if (is_var(v) && this->is_free_var(v, ctx_size + offset) && !get_subst(v, ctx_size + offset)) {
|
||||
result = false;
|
||||
}
|
||||
return true;
|
||||
});
|
||||
return result;
|
||||
bool match_app(expr const & p, expr const & t) {
|
||||
return match_core(app_fn(p), app_fn(t)) && match(app_arg(p), app_arg(t));
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Auxiliary functional object for instantiating the free variables in a pattern.
|
||||
*/
|
||||
class instantiate_free_vars_proc : public replace_visitor {
|
||||
protected:
|
||||
hop_match_fn & m_ref;
|
||||
unsigned m_ctx_size;
|
||||
|
||||
virtual expr visit_var(expr const & x, context const & ctx) {
|
||||
unsigned real_ctx_sz = ctx.size() + m_ctx_size;
|
||||
if (m_ref.is_free_var(x, real_ctx_sz)) {
|
||||
optional<expr> r = m_ref.get_subst(x, real_ctx_sz);
|
||||
lean_assert(r);
|
||||
return m_ref.lift_free_vars(*r, real_ctx_sz);
|
||||
} else {
|
||||
return x;
|
||||
}
|
||||
bool match_core(expr const & p, expr const & t) {
|
||||
if (p.kind() != t.kind())
|
||||
return match_plugin(p, t);
|
||||
switch (p.kind()) {
|
||||
case expr_kind::Local: case expr_kind::Meta:
|
||||
return mlocal_name(p) == mlocal_name(t);
|
||||
case expr_kind::Var:
|
||||
lean_unreachable(); // LCOV_EXCL_LINE
|
||||
case expr_kind::Constant:
|
||||
// TODO(Leo): universe levels
|
||||
return const_name(p) == const_name(t);
|
||||
case expr_kind::Sort:
|
||||
// TODO(Leo): universe levels
|
||||
return true;
|
||||
case expr_kind::Lambda: case expr_kind::Pi:
|
||||
return match_binding(p, t) || match_plugin(p, t);
|
||||
case expr_kind::Macro:
|
||||
return match_macro(p, t) || match_plugin(p, t);
|
||||
case expr_kind::App:
|
||||
return match_app(p, t) || match_plugin(p, t);
|
||||
}
|
||||
lean_unreachable(); // LCOV_EXCL_LINE
|
||||
}
|
||||
|
||||
virtual expr visit_app(expr const & e, context const & ctx) {
|
||||
unsigned real_ctx_sz = ctx.size() + m_ctx_size;
|
||||
expr const & f = arg(e, 0);
|
||||
if (is_var(f) && m_ref.is_free_var(f, real_ctx_sz)) {
|
||||
buffer<expr> new_args;
|
||||
for (unsigned i = 0; i < num_args(e); i++)
|
||||
new_args.push_back(visit(arg(e, i), ctx));
|
||||
if (is_lambda(new_args[0]))
|
||||
return m_ref.apply_beta(new_args[0], new_args.size() - 1, new_args.data() + 1);
|
||||
else
|
||||
return mk_app(new_args);
|
||||
} else {
|
||||
return replace_visitor::visit_app(e, ctx);
|
||||
}
|
||||
}
|
||||
public:
|
||||
hop_match_fn(buffer<optional<expr>> & subst, name_generator const & ngen, name_map<name> * name_subst, hop_matcher_plugin const * plugin):
|
||||
m_subst(subst), m_ngen(ngen), m_name_subst(name_subst), m_plugin(plugin) {}
|
||||
|
||||
public:
|
||||
instantiate_free_vars_proc(hop_match_fn & fn, unsigned ctx_size):
|
||||
m_ref(fn), m_ctx_size(ctx_size) {
|
||||
}
|
||||
};
|
||||
|
||||
bool match(expr const & p, expr const & t, context const & ctx, unsigned ctx_size) {
|
||||
lean_assert(ctx.size() == ctx_size);
|
||||
if (is_free_var(p, ctx_size)) {
|
||||
auto s = get_subst(p, ctx_size);
|
||||
bool match(expr const & p, expr const & t) {
|
||||
if (is_var(p)) {
|
||||
auto s = get_subst(p);
|
||||
if (s) {
|
||||
return lift_free_vars(*s, ctx_size) == t;
|
||||
} else if (has_locally_bound_var(t, ctx_size)) {
|
||||
return match_core(*s, t);
|
||||
} else if (has_local(t)) {
|
||||
return false;
|
||||
} else {
|
||||
assign(p, lower_free_vars(t, ctx_size, ctx_size), ctx_size);
|
||||
assign(p, t);
|
||||
return true;
|
||||
}
|
||||
} else if (is_app(p) && is_free_var(arg(p, 0), ctx_size)) {
|
||||
if (args_are_distinct_locally_bound_vars(p, ctx_size, m_vars)) {
|
||||
} else if (is_app(p)) {
|
||||
buffer<expr> args;
|
||||
expr const & f = get_app_rev_args(p, args);
|
||||
if (is_var(f)) {
|
||||
// higher-order pattern case
|
||||
auto s = get_subst(arg(p, 0), ctx_size);
|
||||
unsigned num = num_args(p);
|
||||
auto s = get_subst(f);
|
||||
if (s) {
|
||||
expr f = lift_free_vars(*s, ctx_size);
|
||||
expr new_p = apply_beta(f, num - 1, &(arg(p, 1)));
|
||||
return new_p == t;
|
||||
} else {
|
||||
optional<expr> new_t = proj(t, ctx, ctx_size, m_vars);
|
||||
expr new_p = apply_beta(*s, args.size(), args.data());
|
||||
return match_core(new_p, t);
|
||||
}
|
||||
if (args_are_distinct_locals(args)) {
|
||||
optional<expr> new_t = proj(t, args);
|
||||
if (new_t) {
|
||||
assign(arg(p, 0), *new_t, ctx_size);
|
||||
assign(f, *new_t);
|
||||
return true;
|
||||
}
|
||||
}
|
||||
} else if (all_free_vars_are_assigned(p, ctx_size)) {
|
||||
instantiate_free_vars_proc proc(*this, ctx_size);
|
||||
expr new_p = proc(p);
|
||||
return new_p == t;
|
||||
}
|
||||
// fallback to the first-order case
|
||||
}
|
||||
|
||||
if (p == t && !has_free_var_ge(p, ctx_size)) {
|
||||
return true;
|
||||
}
|
||||
|
||||
if (m_env && is_constant(p)) {
|
||||
return match_constant(p, t);
|
||||
}
|
||||
|
||||
if (p.kind() != t.kind())
|
||||
return false;
|
||||
switch (p.kind()) {
|
||||
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type:
|
||||
case expr_kind::Value: case expr_kind::MetaVar:
|
||||
return false;
|
||||
case expr_kind::App: {
|
||||
unsigned i1 = num_args(p);
|
||||
unsigned i2 = num_args(t);
|
||||
while (i1 > 0 && i2 > 0) {
|
||||
--i1;
|
||||
--i2;
|
||||
if (i1 == 0 && i2 > 0) {
|
||||
return match(arg(p, i1), mk_app(i2+1, begin_args(t)), ctx, ctx_size);
|
||||
} else if (i2 == 0 && i1 > 0) {
|
||||
return match(mk_app(i1+1, begin_args(p)), arg(t, i2), ctx, ctx_size);
|
||||
} else {
|
||||
if (!match(arg(p, i1), arg(t, i2), ctx, ctx_size))
|
||||
return false;
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
case expr_kind::Proj:
|
||||
return proj_first(p) == proj_first(t) && match(proj_arg(p), proj_arg(t), ctx, ctx_size);
|
||||
case expr_kind::HEq:
|
||||
return
|
||||
match(heq_lhs(p), heq_lhs(t), ctx, ctx_size) &&
|
||||
match(heq_rhs(p), heq_rhs(t), ctx, ctx_size);
|
||||
case expr_kind::Pair:
|
||||
return
|
||||
match(pair_first(p), pair_first(t), ctx, ctx_size) &&
|
||||
match(pair_second(p), pair_second(t), ctx, ctx_size) &&
|
||||
match(pair_type(p), pair_type(t), ctx, ctx_size);
|
||||
case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma:
|
||||
if (m_name_subst)
|
||||
(*m_name_subst)[abst_name(p)] = abst_name(t);
|
||||
return
|
||||
match(abst_domain(p), abst_domain(t), ctx, ctx_size) &&
|
||||
match(abst_body(p), abst_body(t), extend(ctx, abst_name(t), abst_domain(t)), ctx_size+1);
|
||||
case expr_kind::Let:
|
||||
// TODO(Leo)
|
||||
return false;
|
||||
}
|
||||
lean_unreachable();
|
||||
}
|
||||
public:
|
||||
hop_match_fn(buffer<optional<expr>> & subst, optional<ro_environment> const & env,
|
||||
optional<ro_metavar_env> const & menv, name_map<name> * name_subst):
|
||||
m_subst(subst), m_env(env), m_menv(menv), m_name_subst(name_subst) {}
|
||||
|
||||
bool operator()(expr const & p, expr const & t) {
|
||||
return match(p, t, context(), 0);
|
||||
return match_core(p, t);
|
||||
}
|
||||
};
|
||||
|
||||
bool hop_match(expr const & p, expr const & t, buffer<optional<expr>> & subst, optional<ro_environment> const & env,
|
||||
optional<ro_metavar_env> const & menv, name_map<name> * name_subst) {
|
||||
return hop_match_fn(subst, env, menv, name_subst)(p, t);
|
||||
static name g_tmp_prefix = name::mk_internal_unique_name();
|
||||
bool hop_match(expr const & p, expr const & t, buffer<optional<expr>> & subst, name const * prefix,
|
||||
name_map<name> * name_subst, hop_matcher_plugin const * plugin) {
|
||||
lean_assert(closed(t));
|
||||
if (prefix)
|
||||
return hop_match_fn(subst, name_generator(*prefix), name_subst, plugin).match(p, t);
|
||||
else
|
||||
return hop_match_fn(subst, name_generator(g_tmp_prefix), name_subst, plugin).match(p, t);
|
||||
}
|
||||
|
||||
static int hop_match_core(lua_State * L, optional<ro_environment> const & env) {
|
||||
int nargs = lua_gettop(L);
|
||||
expr p = to_expr(L, 1);
|
||||
expr t = to_expr(L, 2);
|
||||
int k = 0;
|
||||
optional<ro_metavar_env> menv;
|
||||
if (nargs >= 4 && !lua_isnil(L, 4))
|
||||
menv = to_metavar_env(L, 4);
|
||||
if (nargs >= 5) {
|
||||
k = luaL_checkinteger(L, 5);
|
||||
if (k < 0)
|
||||
throw exception("hop_match, arg #4 must be non-negative");
|
||||
} else {
|
||||
k = free_var_range(p);
|
||||
}
|
||||
static int hop_match(lua_State * L) {
|
||||
expr p = to_expr(L, 1);
|
||||
expr t = to_expr(L, 2);
|
||||
if (!closed(t))
|
||||
throw exception("higher-order pattern matching failure, input term must not contain free variables");
|
||||
unsigned k = get_free_var_range(p);
|
||||
buffer<optional<expr>> subst;
|
||||
subst.resize(k);
|
||||
if (hop_match(p, t, subst, env, menv)) {
|
||||
if (hop_match(p, t, subst, nullptr, nullptr, nullptr)) {
|
||||
lua_newtable(L);
|
||||
int i = 1;
|
||||
for (auto s : subst) {
|
||||
if (s) {
|
||||
if (s)
|
||||
push_expr(L, *s);
|
||||
} else {
|
||||
else
|
||||
lua_pushboolean(L, false);
|
||||
}
|
||||
lua_rawseti(L, -2, i);
|
||||
i = i + 1;
|
||||
}
|
||||
|
|
@ -377,22 +191,7 @@ static int hop_match_core(lua_State * L, optional<ro_environment> const & env) {
|
|||
return 1;
|
||||
}
|
||||
|
||||
static int hop_match(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
if (nargs >= 3) {
|
||||
if (!lua_isnil(L, 3)) {
|
||||
ro_shared_environment env(L, 3);
|
||||
return hop_match_core(L, optional<ro_environment>(env));
|
||||
} else {
|
||||
return hop_match_core(L, optional<ro_environment>());
|
||||
}
|
||||
} else {
|
||||
ro_shared_environment env(L);
|
||||
return hop_match_core(L, optional<ro_environment>(env));
|
||||
}
|
||||
}
|
||||
|
||||
void open_hop_match(lua_State * L) {
|
||||
SET_GLOBAL_FUN(hop_match, "hop_match");
|
||||
SET_GLOBAL_FUN(hop_match, "match");
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,44 +1,51 @@
|
|||
/*
|
||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
||||
Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include <functional>
|
||||
#include "util/lua.h"
|
||||
#include "util/optional.h"
|
||||
#include "util/buffer.h"
|
||||
#include "util/name_map.h"
|
||||
#include "kernel/expr.h"
|
||||
#include "kernel/environment.h"
|
||||
|
||||
namespace lean {
|
||||
/** \brief Callback for extending the higher-order pattern matching procedure.
|
||||
It is invoked before the matcher fails.
|
||||
|
||||
plugin(p, t, s) must return true iff for updated substitution s', s'(p) is definitionally equal to t.
|
||||
*/
|
||||
typedef std::function<bool(expr const &, expr const &, buffer<optional<expr>> &, name_generator const &)> hop_matcher_plugin; // NOLINT
|
||||
|
||||
/**
|
||||
\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.
|
||||
The substitution is stored in \c subst. Note that, this procedure treats free-variables as placholders
|
||||
instead of meta-variables.
|
||||
|
||||
\c subst is an assignment for the free variables occurring in \c p.
|
||||
|
||||
The free variables occurring in \c t are treated as constants.
|
||||
|
||||
We say non-free variables occurring in \c p and \c t are "locally bound".
|
||||
\pre \c t must not contain free variables. If it does, they must be replaced with local constants
|
||||
before invoking this functions.
|
||||
|
||||
\c p is a higher-order pattern when in all applications in \c p
|
||||
1- A free variable is not the function OR
|
||||
2- A free variable is the function, but all other arguments are distinct locally bound variables.
|
||||
2- A free variable is the function, but all other arguments are distinct local constants.
|
||||
|
||||
\pre \c subst must be big enough to store all free variables occurring in subst
|
||||
|
||||
If an environment is provided, then a constant \c c matches a term \c t if
|
||||
\c c is definitionally equal to \c t.
|
||||
|
||||
If a metavariable environment is provided, then it is provided to lift/lower
|
||||
free variables procedures to be able to minimize the size of the local context.
|
||||
If prefix is provided, then it is used for creating unique names.
|
||||
|
||||
If name_subst is different from nullptr, then the procedure stores in name_subst
|
||||
a mapping for binder names. It maps the binder names used in the pattern \c p into
|
||||
the binder names used in \c t.
|
||||
|
||||
If the plugin is provided, then it is invoked before a failure.
|
||||
*/
|
||||
bool hop_match(expr const & p, expr const & t, buffer<optional<expr>> & subst,
|
||||
optional<ro_environment> const & env = optional<ro_environment>(),
|
||||
optional<ro_metavar_env> const & menv = optional<ro_metavar_env>(),
|
||||
name_map<name> * name_subst = nullptr);
|
||||
bool hop_match(expr const & p, expr const & t, buffer<optional<expr>> & subst, name const * prefix = nullptr,
|
||||
name_map<name> * name_subst = nullptr, hop_matcher_plugin const * plugin = nullptr);
|
||||
void open_hop_match(lua_State * L);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -12,4 +12,14 @@ namespace lean {
|
|||
name_set collect_univ_params(expr const & e, name_set const & ls = name_set());
|
||||
void collect_locals(expr const & e, expr_struct_set & ls);
|
||||
level_param_names to_level_param_names(name_set const & ls);
|
||||
|
||||
/** \brief Return true iff \c [begin_locals, end_locals) contains \c local */
|
||||
template<typename It> bool contains_local(expr const & local, It const & begin_locals, It const & end_locals) {
|
||||
return std::any_of(begin_locals, end_locals, [&](expr const & l) { return mlocal_name(local) == mlocal_name(l); });
|
||||
}
|
||||
|
||||
/** \brief Return true iff \c locals contains \c local */
|
||||
inline bool contains_local(expr const & local, buffer<expr> const & locals) {
|
||||
return contains_local(local, locals.begin(), locals.end());
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -16,7 +16,7 @@ Author: Leonardo de Moura
|
|||
#include "library/explicit.h"
|
||||
#include "library/unifier.h"
|
||||
#include "library/scoped_ext.h"
|
||||
// #include "library/hop_match.h"
|
||||
#include "library/hop_match.h"
|
||||
|
||||
namespace lean {
|
||||
inline void open_core_module(lua_State * L) {
|
||||
|
|
@ -30,7 +30,7 @@ inline void open_core_module(lua_State * L) {
|
|||
open_scoped_ext(L);
|
||||
open_unifier(L);
|
||||
open_explicit(L);
|
||||
// open_hop_match(L);
|
||||
open_hop_match(L);
|
||||
}
|
||||
inline void register_core_module() {
|
||||
script_state::register_module(open_core_module);
|
||||
|
|
|
|||
|
|
@ -19,6 +19,7 @@ Author: Leonardo de Moura
|
|||
#include "kernel/kernel_exception.h"
|
||||
#include "kernel/error_msgs.h"
|
||||
#include "library/occurs.h"
|
||||
#include "library/locals.h"
|
||||
#include "library/unifier.h"
|
||||
#include "library/opaque_hints.h"
|
||||
#include "library/unifier_plugin.h"
|
||||
|
|
@ -32,16 +33,6 @@ static name g_unifier_expensive {"unifier", "expensive"};
|
|||
RegisterBoolOption(g_unifier_expensive, LEAN_DEFAULT_UNIFIER_EXPENSIVE, "(unifier) enable/disable expensive (and more complete) procedure");
|
||||
bool get_unifier_expensive(options const & opts) { return opts.get_bool(g_unifier_expensive, LEAN_DEFAULT_UNIFIER_EXPENSIVE); }
|
||||
|
||||
/** \brief Return true iff \c [begin_locals, end_locals) contains \c local */
|
||||
template<typename It> bool contains_local(expr const & local, It const & begin_locals, It const & end_locals) {
|
||||
return std::any_of(begin_locals, end_locals, [&](expr const & l) { return mlocal_name(local) == mlocal_name(l); });
|
||||
}
|
||||
|
||||
/** \brief Return true iff \c locals contains \c local */
|
||||
bool contains_local(expr const & local, buffer<expr> const & locals) {
|
||||
return contains_local(local, locals.begin(), locals.end());
|
||||
}
|
||||
|
||||
// If \c e is a metavariable ?m or a term of the form (?m l_1 ... l_n) where
|
||||
// l_1 ... l_n are distinct local variables, then return ?m, and store l_1 ... l_n in args.
|
||||
// Otherwise return none.
|
||||
|
|
|
|||
24
tests/lua/hop1.lua
Normal file
24
tests/lua/hop1.lua
Normal file
|
|
@ -0,0 +1,24 @@
|
|||
function tst_match(p, t)
|
||||
local r = match(p, t)
|
||||
assert(r)
|
||||
print("--------------")
|
||||
for i = 1, #r do
|
||||
print(" #" .. i .. " := " .. tostring(r[i]))
|
||||
end
|
||||
end
|
||||
|
||||
local env = environment()
|
||||
local N = Const("N")
|
||||
local f = Const("f")
|
||||
local a = Const("a")
|
||||
local b = Const("b")
|
||||
local x = Local("x", N)
|
||||
local y = Local("y", N)
|
||||
tst_match(f(Var(0), Var(0)), f(a, a))
|
||||
tst_match(f(Var(0), Var(1)), f(a, b))
|
||||
tst_match(Var(0)(x, y), f(x, f(x, y)))
|
||||
assert(not match(Var(0)(x, x), f(x, f(x, y))))
|
||||
assert(not match(Var(0)(x), f(x, y)))
|
||||
tst_match(Pi(x, y, Var(2)(x)), Pi(x, y, f(f(x))))
|
||||
tst_match(Fun(x, y, Var(2)(x)), Fun(x, y, f(f(x))))
|
||||
assert(match(Pi(x, Var(2)(x)), Pi(x, y, f(f(x)))))
|
||||
Loading…
Reference in a new issue