2014-01-13 01:45:24 +00:00
|
|
|
/*
|
|
|
|
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 "util/optional.h"
|
|
|
|
#include "util/buffer.h"
|
|
|
|
#include "kernel/free_vars.h"
|
|
|
|
#include "kernel/instantiate.h"
|
2014-01-16 10:05:09 +00:00
|
|
|
#include "kernel/kernel.h"
|
|
|
|
#include "library/equality.h"
|
2014-01-13 01:45:24 +00:00
|
|
|
#include "library/kernel_bindings.h"
|
2014-01-19 18:32:06 +00:00
|
|
|
#include "library/hop_match.h"
|
2014-01-13 01:45:24 +00:00
|
|
|
|
|
|
|
namespace lean {
|
|
|
|
|
|
|
|
class hop_match_fn {
|
|
|
|
buffer<optional<expr>> & m_subst;
|
|
|
|
buffer<expr> m_vars;
|
2014-01-19 18:32:06 +00:00
|
|
|
optional<ro_environment> m_env;
|
2014-01-13 01:45:24 +00:00
|
|
|
|
|
|
|
bool is_free_var(expr const & x, unsigned ctx_size) const {
|
|
|
|
return is_var(x) && var_idx(x) >= ctx_size;
|
|
|
|
}
|
|
|
|
|
|
|
|
bool is_locally_bound(expr const & x, unsigned ctx_size) const {
|
|
|
|
return is_var(x) && var_idx(x) < ctx_size;
|
|
|
|
}
|
|
|
|
|
|
|
|
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;
|
|
|
|
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();
|
2014-01-14 02:06:23 +00:00
|
|
|
m_subst[sz - vidx - 1] = t;
|
2014-01-13 01:45:24 +00:00
|
|
|
}
|
|
|
|
|
|
|
|
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))
|
|
|
|
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)
|
|
|
|
return none_expr();
|
|
|
|
else
|
|
|
|
return some_expr(r);
|
|
|
|
}
|
|
|
|
|
2014-01-14 22:37:28 +00:00
|
|
|
// 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 {
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2014-01-13 01:45:24 +00:00
|
|
|
/**
|
|
|
|
\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) {
|
2014-01-14 22:37:28 +00:00
|
|
|
if (is_simple_proj(t, ctx_size, vars)) {
|
|
|
|
return some_expr(lower_free_vars(arg(t, 0), ctx_size, ctx_size));
|
|
|
|
}
|
2014-01-13 01:45:24 +00:00
|
|
|
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);
|
|
|
|
}
|
|
|
|
|
2014-01-19 18:32:06 +00:00
|
|
|
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)
|
|
|
|
return true;
|
|
|
|
auto new_p = unfold_constant(p);
|
|
|
|
if (new_p)
|
|
|
|
return match_constant(*new_p, t);
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
|
2014-01-13 01:45:24 +00:00
|
|
|
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);
|
|
|
|
if (s) {
|
2014-01-14 22:37:28 +00:00
|
|
|
return lift_free_vars(*s, ctx_size) == t;
|
2014-01-13 01:45:24 +00:00
|
|
|
} else if (has_locally_bound_var(t, ctx_size)) {
|
|
|
|
return false;
|
|
|
|
} else {
|
2014-01-14 02:06:23 +00:00
|
|
|
assign(p, lower_free_vars(t, ctx_size, ctx_size), ctx_size);
|
2014-01-13 01:45:24 +00:00
|
|
|
return true;
|
|
|
|
}
|
2014-01-14 22:37:28 +00:00
|
|
|
} else if (is_app(p) && is_free_var(arg(p, 0), ctx_size) && args_are_distinct_locally_bound_vars(p, ctx_size, m_vars)) {
|
|
|
|
// higher-order pattern case
|
2014-01-13 01:45:24 +00:00
|
|
|
auto s = get_subst(arg(p, 0), ctx_size);
|
|
|
|
unsigned num = num_args(p);
|
|
|
|
if (s) {
|
|
|
|
expr f = lift_free_vars(*s, ctx_size);
|
|
|
|
expr new_p = apply_beta(f, num - 1, &(arg(p, 1)));
|
2014-01-14 22:37:28 +00:00
|
|
|
return new_p == t;
|
2014-01-13 01:45:24 +00:00
|
|
|
} else {
|
2014-01-14 22:37:28 +00:00
|
|
|
optional<expr> new_t = proj(t, ctx, ctx_size, m_vars);
|
|
|
|
if (new_t) {
|
|
|
|
assign(arg(p, 0), *new_t, ctx_size);
|
|
|
|
return true;
|
2014-01-13 01:45:24 +00:00
|
|
|
}
|
2014-01-14 22:37:28 +00:00
|
|
|
// fallback to the first-order case
|
2014-01-13 01:45:24 +00:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2014-01-14 22:37:28 +00:00
|
|
|
if (p == t && !has_free_var_ge(p, ctx_size)) {
|
2014-01-13 01:45:24 +00:00
|
|
|
return true;
|
2014-01-14 22:37:28 +00:00
|
|
|
}
|
2014-01-13 01:45:24 +00:00
|
|
|
|
2014-01-19 18:32:06 +00:00
|
|
|
if (m_env && is_constant(p)) {
|
|
|
|
return match_constant(p, t);
|
|
|
|
}
|
|
|
|
|
2014-01-16 10:05:09 +00:00
|
|
|
if (is_equality(p) && is_equality(t) && (!is_eq(p) || !is_eq(t))) {
|
2014-01-14 22:37:28 +00:00
|
|
|
// Remark: if p and t are homogeneous equality, then we handle as an application (in the else branch)
|
|
|
|
// We do that because we can get more information. For example, the pattern
|
|
|
|
// may be (eq #1 a b).
|
|
|
|
// This branch ignores the type.
|
2014-01-16 10:05:09 +00:00
|
|
|
expr_pair p1 = get_equality_args(p);
|
|
|
|
expr_pair p2 = get_equality_args(t);
|
2014-01-13 01:45:24 +00:00
|
|
|
return match(p1.first, p2.first, ctx, ctx_size) && match(p1.second, p2.second, ctx, ctx_size);
|
|
|
|
} else {
|
|
|
|
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) {
|
2014-01-14 22:37:28 +00:00
|
|
|
return match(arg(p, i1), mk_app(i2+1, begin_args(t)), ctx, ctx_size);
|
2014-01-13 01:45:24 +00:00
|
|
|
} else if (i2 == 0 && i1 > 0) {
|
2014-01-14 22:37:28 +00:00
|
|
|
return match(mk_app(i1+1, begin_args(p)), arg(t, i2), ctx, ctx_size);
|
2014-01-13 01:45:24 +00:00
|
|
|
} else {
|
|
|
|
if (!match(arg(p, i1), arg(t, i2), ctx, ctx_size))
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
}
|
|
|
|
return true;
|
|
|
|
}
|
|
|
|
case expr_kind::Lambda: case expr_kind::Pi:
|
|
|
|
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:
|
2014-01-19 18:32:06 +00:00
|
|
|
hop_match_fn(buffer<optional<expr>> & subst, optional<ro_environment> const & env):m_subst(subst), m_env(env) {}
|
2014-01-13 01:45:24 +00:00
|
|
|
|
|
|
|
bool operator()(expr const & p, expr const & t) {
|
|
|
|
return match(p, t, context(), 0);
|
|
|
|
}
|
|
|
|
};
|
|
|
|
|
2014-01-19 18:32:06 +00:00
|
|
|
bool hop_match(expr const & p, expr const & t, buffer<optional<expr>> & subst, optional<ro_environment> const & env) {
|
|
|
|
return hop_match_fn(subst, env)(p, t);
|
2014-01-13 01:45:24 +00:00
|
|
|
}
|
|
|
|
|
2014-01-19 18:32:06 +00:00
|
|
|
static int hop_match_core(lua_State * L, optional<ro_environment> const & env) {
|
2014-01-13 01:45:24 +00:00
|
|
|
int nargs = lua_gettop(L);
|
|
|
|
expr p = to_expr(L, 1);
|
|
|
|
expr t = to_expr(L, 2);
|
|
|
|
int k = 0;
|
2014-01-19 18:32:06 +00:00
|
|
|
if (nargs >= 4) {
|
|
|
|
k = luaL_checkinteger(L, 4);
|
2014-01-13 01:45:24 +00:00
|
|
|
if (k < 0)
|
2014-01-19 18:32:06 +00:00
|
|
|
throw exception("hop_match, arg #4 must be non-negative");
|
2014-01-13 01:45:24 +00:00
|
|
|
} else {
|
|
|
|
k = free_var_range(p);
|
|
|
|
}
|
|
|
|
buffer<optional<expr>> subst;
|
|
|
|
subst.resize(k);
|
2014-01-19 18:32:06 +00:00
|
|
|
if (hop_match(p, t, subst, env)) {
|
2014-01-13 01:45:24 +00:00
|
|
|
lua_newtable(L);
|
|
|
|
int i = 1;
|
|
|
|
for (auto s : subst) {
|
|
|
|
if (s) {
|
|
|
|
push_expr(L, *s);
|
|
|
|
} else {
|
2014-01-16 07:51:17 +00:00
|
|
|
lua_pushboolean(L, false);
|
2014-01-13 01:45:24 +00:00
|
|
|
}
|
|
|
|
lua_rawseti(L, -2, i);
|
|
|
|
i = i + 1;
|
|
|
|
}
|
|
|
|
} else {
|
|
|
|
lua_pushnil(L);
|
|
|
|
}
|
|
|
|
return 1;
|
|
|
|
}
|
|
|
|
|
2014-01-19 18:32:06 +00:00
|
|
|
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));
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2014-01-13 01:45:24 +00:00
|
|
|
void open_hop_match(lua_State * L) {
|
|
|
|
SET_GLOBAL_FUN(hop_match, "hop_match");
|
|
|
|
}
|
|
|
|
}
|