refactor(kernel): remove unnecessary files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
6baa59376c
commit
997f32378c
6 changed files with 1 additions and 1099 deletions
|
|
@ -3,11 +3,9 @@ for_each_fn.cpp occurs.cpp replace_fn.cpp free_vars.cpp abstract.cpp
|
||||||
instantiate.cpp context.cpp formatter.cpp max_sharing.cpp kernel_exception.cpp
|
instantiate.cpp context.cpp formatter.cpp max_sharing.cpp kernel_exception.cpp
|
||||||
object.cpp environment.cpp replace_visitor.cpp io_state.cpp
|
object.cpp environment.cpp replace_visitor.cpp io_state.cpp
|
||||||
normalizer.cpp
|
normalizer.cpp
|
||||||
# type_checker.cpp kernel.cpp metavar.cpp
|
# type_checker.cpp kernel.cpp
|
||||||
# justification.cpp unification_constraint.cpp
|
# justification.cpp unification_constraint.cpp
|
||||||
# type_checker_justification.cpp pos_info_provider.cpp
|
# type_checker_justification.cpp pos_info_provider.cpp
|
||||||
# update_expr.cpp
|
|
||||||
# universe_constraints.cpp
|
|
||||||
)
|
)
|
||||||
|
|
||||||
target_link_libraries(kernel ${LEAN_LIBS})
|
target_link_libraries(kernel ${LEAN_LIBS})
|
||||||
|
|
|
||||||
|
|
@ -1,503 +0,0 @@
|
||||||
/*
|
|
||||||
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 <utility>
|
|
||||||
#include <vector>
|
|
||||||
#include <limits>
|
|
||||||
#include <algorithm>
|
|
||||||
#include "util/exception.h"
|
|
||||||
#include "kernel/metavar.h"
|
|
||||||
#include "kernel/free_vars.h"
|
|
||||||
#include "kernel/instantiate.h"
|
|
||||||
#include "kernel/occurs.h"
|
|
||||||
#include "kernel/for_each_fn.h"
|
|
||||||
#include "kernel/find_fn.h"
|
|
||||||
|
|
||||||
namespace lean {
|
|
||||||
/**
|
|
||||||
\brief Assignment normalization justification. That is, when other assignments are applied to an existing assignment.
|
|
||||||
*/
|
|
||||||
class normalize_assignment_justification : public justification_cell {
|
|
||||||
context m_ctx;
|
|
||||||
expr m_expr;
|
|
||||||
std::vector<justification> m_jsts;
|
|
||||||
public:
|
|
||||||
normalize_assignment_justification(context const & ctx, expr const & e,
|
|
||||||
justification const & jst,
|
|
||||||
unsigned num_assignment_jsts, justification const * assignment_jsts):
|
|
||||||
m_ctx(ctx),
|
|
||||||
m_expr(e),
|
|
||||||
m_jsts(assignment_jsts, assignment_jsts + num_assignment_jsts) {
|
|
||||||
m_jsts.push_back(jst);
|
|
||||||
std::reverse(m_jsts.begin(), m_jsts.end());
|
|
||||||
}
|
|
||||||
|
|
||||||
virtual format pp_header(formatter const & fmt, options const & opts, optional<metavar_env> const & menv) const {
|
|
||||||
unsigned indent = get_pp_indent(opts);
|
|
||||||
format expr_fmt = fmt(instantiate_metavars(menv, m_ctx), instantiate_metavars(menv, m_expr), false, opts);
|
|
||||||
format r;
|
|
||||||
r += format("Normalize assignment");
|
|
||||||
r += nest(indent, compose(line(), expr_fmt));
|
|
||||||
return r;
|
|
||||||
}
|
|
||||||
|
|
||||||
virtual void get_children(buffer<justification_cell*> & r) const {
|
|
||||||
append(r, m_jsts);
|
|
||||||
}
|
|
||||||
|
|
||||||
virtual optional<expr> get_main_expr() const { return some_expr(m_expr); }
|
|
||||||
};
|
|
||||||
|
|
||||||
void metavar_env_cell::inc_timestamp() {
|
|
||||||
if (m_timestamp == std::numeric_limits<unsigned>::max()) {
|
|
||||||
// This should not happen in real examples. We add it just to be safe.
|
|
||||||
throw exception("metavar_env_cell timestamp overflow");
|
|
||||||
}
|
|
||||||
m_timestamp++;
|
|
||||||
}
|
|
||||||
|
|
||||||
metavar_env_cell::metavar_env_cell(name const & prefix):
|
|
||||||
m_name_generator(prefix),
|
|
||||||
m_beta_reduce_mv(true),
|
|
||||||
m_timestamp(1),
|
|
||||||
m_rc(0) {
|
|
||||||
}
|
|
||||||
|
|
||||||
static name g_default_name("M");
|
|
||||||
metavar_env_cell::metavar_env_cell():
|
|
||||||
metavar_env_cell(g_default_name) {
|
|
||||||
}
|
|
||||||
|
|
||||||
metavar_env_cell::metavar_env_cell(metavar_env_cell const & other):
|
|
||||||
m_name_generator(other.m_name_generator),
|
|
||||||
m_metavar_data(other.m_metavar_data),
|
|
||||||
m_beta_reduce_mv(other.m_beta_reduce_mv),
|
|
||||||
m_timestamp(1),
|
|
||||||
m_rc(0) {
|
|
||||||
}
|
|
||||||
|
|
||||||
expr metavar_env_cell::mk_metavar(context const & ctx, optional<expr> const & type) {
|
|
||||||
inc_timestamp();
|
|
||||||
name m = m_name_generator.next();
|
|
||||||
expr r = ::lean::mk_metavar(m);
|
|
||||||
m_metavar_data.insert(m, data(type, ctx));
|
|
||||||
return r;
|
|
||||||
}
|
|
||||||
|
|
||||||
context metavar_env_cell::get_context(expr const & m) const {
|
|
||||||
lean_assert(is_metavar(m));
|
|
||||||
lean_assert(!has_local_context(m));
|
|
||||||
return get_context(metavar_name(m));
|
|
||||||
}
|
|
||||||
|
|
||||||
context metavar_env_cell::get_context(name const & m) const {
|
|
||||||
auto it = m_metavar_data.find(m);
|
|
||||||
lean_assert(it);
|
|
||||||
return it->m_context;
|
|
||||||
}
|
|
||||||
|
|
||||||
expr metavar_env_cell::get_type(expr const & m) {
|
|
||||||
lean_assert(is_metavar(m));
|
|
||||||
expr t = get_type(metavar_name(m));
|
|
||||||
if (has_local_context(m)) {
|
|
||||||
if (is_metavar(t)) {
|
|
||||||
return update_metavar(t, append(metavar_lctx(m), metavar_lctx(t)));
|
|
||||||
} else {
|
|
||||||
return apply_local_context(t, metavar_lctx(m), metavar_env(this));
|
|
||||||
}
|
|
||||||
} else {
|
|
||||||
return t;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
expr metavar_env_cell::get_type(name const & m) {
|
|
||||||
auto it = m_metavar_data.find(m);
|
|
||||||
lean_assert(it);
|
|
||||||
if (it->m_type) {
|
|
||||||
return *(it->m_type);
|
|
||||||
} else {
|
|
||||||
expr t = mk_metavar(get_context(m));
|
|
||||||
it->m_type = t;
|
|
||||||
return t;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
bool metavar_env_cell::has_type(name const & m) const {
|
|
||||||
auto it = m_metavar_data.find(m);
|
|
||||||
lean_assert(it);
|
|
||||||
return static_cast<bool>(it->m_type);
|
|
||||||
}
|
|
||||||
|
|
||||||
bool metavar_env_cell::has_type(expr const & m) const {
|
|
||||||
lean_assert(is_metavar(m));
|
|
||||||
return has_type(metavar_name(m));
|
|
||||||
}
|
|
||||||
|
|
||||||
optional<justification> metavar_env_cell::get_justification(expr const & m) const {
|
|
||||||
lean_assert(is_metavar(m));
|
|
||||||
return get_justification(metavar_name(m));
|
|
||||||
}
|
|
||||||
|
|
||||||
optional<justification> metavar_env_cell::get_justification(name const & m) const {
|
|
||||||
auto r = get_subst_jst(m);
|
|
||||||
if (r)
|
|
||||||
return optional<justification>(r->second);
|
|
||||||
else
|
|
||||||
return optional<justification>();
|
|
||||||
}
|
|
||||||
|
|
||||||
bool metavar_env_cell::is_assigned(name const & m) const {
|
|
||||||
auto it = m_metavar_data.find(m);
|
|
||||||
return it && it->m_subst;
|
|
||||||
}
|
|
||||||
|
|
||||||
bool metavar_env_cell::is_assigned(expr const & m) const {
|
|
||||||
lean_assert(is_metavar(m));
|
|
||||||
return is_assigned(metavar_name(m));
|
|
||||||
}
|
|
||||||
|
|
||||||
bool metavar_env_cell::assign(name const & m, expr const & t, justification const & jst) {
|
|
||||||
lean_assert(!is_assigned(m));
|
|
||||||
inc_timestamp();
|
|
||||||
justification jst2 = jst;
|
|
||||||
buffer<justification> jsts;
|
|
||||||
expr t2 = instantiate_metavars(t, jsts);
|
|
||||||
if (!jsts.empty()) {
|
|
||||||
jst2 = justification(new normalize_assignment_justification(get_context(m), t, jst,
|
|
||||||
jsts.size(), jsts.data()));
|
|
||||||
}
|
|
||||||
unsigned ctx_size = get_context_size(m);
|
|
||||||
if (has_metavar(t2)) {
|
|
||||||
bool failed = false;
|
|
||||||
// Make sure the contexts of the metavariables occurring in \c t2 are
|
|
||||||
// not too big.
|
|
||||||
for_each(t2, [&](expr const & e, unsigned offset) {
|
|
||||||
if (is_metavar(e)) {
|
|
||||||
lean_assert(!is_assigned(e));
|
|
||||||
unsigned range = free_var_range(e, metavar_env(this));
|
|
||||||
if (range > ctx_size + offset) {
|
|
||||||
unsigned extra = range - ctx_size - offset;
|
|
||||||
auto it2 = m_metavar_data.find(metavar_name(e));
|
|
||||||
if (it2 == nullptr) {
|
|
||||||
failed = true;
|
|
||||||
} else {
|
|
||||||
unsigned e_ctx_size = it2->m_context.size();
|
|
||||||
if (e_ctx_size < extra) {
|
|
||||||
failed = true;
|
|
||||||
} else {
|
|
||||||
it2->m_context = it2->m_context.truncate(e_ctx_size - extra);
|
|
||||||
lean_assert_le(free_var_range(e, metavar_env(this)), ctx_size + offset);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
return true;
|
|
||||||
});
|
|
||||||
if (failed)
|
|
||||||
return false;
|
|
||||||
}
|
|
||||||
if (free_var_range(t2, metavar_env(this)) > ctx_size)
|
|
||||||
return false;
|
|
||||||
auto it = m_metavar_data.find(m);
|
|
||||||
lean_assert(it);
|
|
||||||
it->m_subst = t2;
|
|
||||||
it->m_justification = jst2;
|
|
||||||
return true;
|
|
||||||
}
|
|
||||||
|
|
||||||
bool metavar_env_cell::assign(name const & m, expr const & t) {
|
|
||||||
justification j;
|
|
||||||
return assign(m, t, j);
|
|
||||||
}
|
|
||||||
|
|
||||||
bool metavar_env_cell::assign(expr const & m, expr const & t, justification const & j) {
|
|
||||||
lean_assert(is_metavar(m));
|
|
||||||
lean_assert(!has_local_context(m));
|
|
||||||
return assign(metavar_name(m), t, j);
|
|
||||||
}
|
|
||||||
|
|
||||||
bool metavar_env_cell::assign(expr const & m, expr const & t) {
|
|
||||||
justification j;
|
|
||||||
return assign(m, t, j);
|
|
||||||
}
|
|
||||||
|
|
||||||
expr apply_local_context(expr const & a, local_context const & lctx, optional<ro_metavar_env> const & menv) {
|
|
||||||
if (lctx) {
|
|
||||||
if (is_metavar(a)) {
|
|
||||||
return mk_metavar(metavar_name(a), append(lctx, metavar_lctx(a)));
|
|
||||||
} else {
|
|
||||||
expr r = apply_local_context(a, tail(lctx), menv);
|
|
||||||
local_entry const & e = head(lctx);
|
|
||||||
if (e.is_lift()) {
|
|
||||||
return lift_free_vars(r, e.s(), e.n(), menv);
|
|
||||||
} else {
|
|
||||||
lean_assert(e.is_inst());
|
|
||||||
return instantiate(r, e.s(), e.v(), menv);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
} else {
|
|
||||||
return a;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
optional<std::pair<expr, justification>> metavar_env_cell::get_subst_jst(expr const & m) const {
|
|
||||||
lean_assert(is_metavar(m));
|
|
||||||
auto p = get_subst_jst(metavar_name(m));
|
|
||||||
if (p) {
|
|
||||||
expr r = p->first;
|
|
||||||
local_context const & lctx = metavar_lctx(m);
|
|
||||||
if (lctx)
|
|
||||||
r = apply_local_context(r, lctx, metavar_env(const_cast<metavar_env_cell*>(this)));
|
|
||||||
return some(mk_pair(r, p->second));
|
|
||||||
} else {
|
|
||||||
return p;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
optional<std::pair<expr, justification>> metavar_env_cell::get_subst_jst(name const & m) const {
|
|
||||||
auto it = const_cast<metavar_env_cell*>(this)->m_metavar_data.find(m);
|
|
||||||
if (it->m_subst) {
|
|
||||||
expr s = *(it->m_subst);
|
|
||||||
if (has_assigned_metavar(s)) {
|
|
||||||
buffer<justification> jsts;
|
|
||||||
expr new_subst = instantiate_metavars(s, jsts);
|
|
||||||
if (!jsts.empty()) {
|
|
||||||
justification new_jst(new normalize_assignment_justification(it->m_context, s, it->m_justification,
|
|
||||||
jsts.size(), jsts.data()));
|
|
||||||
it->m_justification = new_jst;
|
|
||||||
it->m_subst = new_subst;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
return optional<std::pair<expr, justification>>(std::pair<expr, justification>(*(it->m_subst), it->m_justification));
|
|
||||||
} else {
|
|
||||||
return optional<std::pair<expr, justification>>();
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
optional<expr> metavar_env_cell::get_subst(name const & m) const {
|
|
||||||
auto r = get_subst_jst(m);
|
|
||||||
if (r)
|
|
||||||
return some_expr(r->first);
|
|
||||||
else
|
|
||||||
return none_expr();
|
|
||||||
}
|
|
||||||
|
|
||||||
optional<expr> metavar_env_cell::get_subst(expr const & m) const {
|
|
||||||
auto r = get_subst_jst(m);
|
|
||||||
if (r)
|
|
||||||
return some_expr(r->first);
|
|
||||||
else
|
|
||||||
return none_expr();
|
|
||||||
}
|
|
||||||
|
|
||||||
bool metavar_env_cell::has_assigned_metavar(expr const & e) const {
|
|
||||||
if (!has_metavar(e)) {
|
|
||||||
return false;
|
|
||||||
} else {
|
|
||||||
bool result = false;
|
|
||||||
for_each(e, [&](expr const & n, unsigned) {
|
|
||||||
if (result)
|
|
||||||
return false;
|
|
||||||
if (!has_metavar(n))
|
|
||||||
return false;
|
|
||||||
if (is_metavar(n)) {
|
|
||||||
if (is_assigned(n)) {
|
|
||||||
result = true;
|
|
||||||
return false;
|
|
||||||
}
|
|
||||||
for (auto const & entry : metavar_lctx(n)) {
|
|
||||||
if (entry.is_inst() && has_assigned_metavar(entry.v())) {
|
|
||||||
result = true;
|
|
||||||
return false;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
return true;
|
|
||||||
});
|
|
||||||
return result;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
bool metavar_env_cell::has_metavar(expr const & e, expr const & m) const {
|
|
||||||
if (has_metavar(e)) {
|
|
||||||
lean_assert(is_metavar(m));
|
|
||||||
lean_assert(!is_assigned(m));
|
|
||||||
return static_cast<bool>(find(e, [&](expr const & m2) {
|
|
||||||
return
|
|
||||||
is_metavar(m2) &&
|
|
||||||
((metavar_name(m) == metavar_name(m2)) ||
|
|
||||||
(is_assigned(m2) && has_metavar(*get_subst(m2), m)));
|
|
||||||
}));
|
|
||||||
} else {
|
|
||||||
return false;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
class instantiate_metavars_proc : public replace_visitor {
|
|
||||||
protected:
|
|
||||||
metavar_env_cell const * m_menv;
|
|
||||||
buffer<justification> & m_jsts;
|
|
||||||
|
|
||||||
void push_back(justification const & jst) {
|
|
||||||
if (jst)
|
|
||||||
m_jsts.push_back(jst);
|
|
||||||
}
|
|
||||||
|
|
||||||
virtual expr visit_metavar(expr const & m, context const & ctx) {
|
|
||||||
local_context const & lctx = metavar_lctx(m);
|
|
||||||
if (is_metavar(m) && m_menv->is_assigned(m)) {
|
|
||||||
auto p = m_menv->get_subst_jst(m);
|
|
||||||
lean_assert(p);
|
|
||||||
expr r = p->first;
|
|
||||||
push_back(p->second);
|
|
||||||
if (m_menv->has_assigned_metavar(r)) {
|
|
||||||
return visit(r, ctx);
|
|
||||||
} else {
|
|
||||||
return r;
|
|
||||||
}
|
|
||||||
} else if (std::find_if(lctx.begin(), lctx.end(), [&](local_entry const & e) { return e.is_inst() && m_menv->has_assigned_metavar(e.v()); })
|
|
||||||
!= lctx.end()) {
|
|
||||||
// local context has assigned metavariables
|
|
||||||
buffer<local_entry> new_lctx;
|
|
||||||
for (auto const & e : lctx) {
|
|
||||||
if (e.is_inst())
|
|
||||||
new_lctx.push_back(mk_inst(e.s(), visit(e.v(), ctx)));
|
|
||||||
else
|
|
||||||
new_lctx.push_back(e);
|
|
||||||
}
|
|
||||||
return mk_metavar(metavar_name(m), to_list(new_lctx.begin(), new_lctx.end()));
|
|
||||||
} else {
|
|
||||||
return m;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
virtual expr visit_app(expr const & e, context const & ctx) {
|
|
||||||
expr const & f = arg(e, 0);
|
|
||||||
if (m_menv->beta_reduce_metavar_application() && is_metavar(f) && m_menv->is_assigned(f)) {
|
|
||||||
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 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:
|
|
||||||
instantiate_metavars_proc(metavar_env_cell const * menv, buffer<justification> & jsts):
|
|
||||||
m_menv(menv),
|
|
||||||
m_jsts(jsts) {
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
expr metavar_env_cell::instantiate_metavars(expr const & e, buffer<justification> & jsts) const {
|
|
||||||
if (!has_metavar(e)) {
|
|
||||||
return e;
|
|
||||||
} else {
|
|
||||||
expr r = instantiate_metavars_proc(this, jsts)(e);
|
|
||||||
lean_assert(!has_assigned_metavar(r));
|
|
||||||
return r;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
context metavar_env_cell::instantiate_metavars(context const & ctx) const {
|
|
||||||
buffer<context_entry> new_entries;
|
|
||||||
auto it = ctx.begin();
|
|
||||||
auto end = ctx.end();
|
|
||||||
for (; it != end; ++it) {
|
|
||||||
auto n = it->get_name();
|
|
||||||
auto d = it->get_domain();
|
|
||||||
auto b = it->get_body();
|
|
||||||
if (d && b)
|
|
||||||
new_entries.emplace_back(n, instantiate_metavars(*d), instantiate_metavars(*b));
|
|
||||||
else if (d)
|
|
||||||
new_entries.emplace_back(n, instantiate_metavars(*d));
|
|
||||||
else
|
|
||||||
new_entries.emplace_back(n, none_expr(), instantiate_metavars(*b));
|
|
||||||
}
|
|
||||||
return context(new_entries.size(), new_entries.data());
|
|
||||||
}
|
|
||||||
|
|
||||||
template<typename MEnv>
|
|
||||||
bool cached_metavar_env_tpl<MEnv>::update(optional<MEnv> const & menv) {
|
|
||||||
if (!menv) {
|
|
||||||
m_menv = optional<MEnv>();
|
|
||||||
if (m_timestamp != 0) {
|
|
||||||
m_timestamp = 0;
|
|
||||||
return true;
|
|
||||||
} else {
|
|
||||||
return false;
|
|
||||||
}
|
|
||||||
} else {
|
|
||||||
unsigned new_timestamp = (*menv)->get_timestamp();
|
|
||||||
if (m_menv != menv || m_timestamp != new_timestamp) {
|
|
||||||
m_menv = menv;
|
|
||||||
m_timestamp = new_timestamp;
|
|
||||||
return true;
|
|
||||||
} else {
|
|
||||||
return false;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
template class cached_metavar_env_tpl<metavar_env>;
|
|
||||||
template class cached_metavar_env_tpl<ro_metavar_env>;
|
|
||||||
|
|
||||||
local_context add_lift(local_context const & lctx, unsigned s, unsigned n) {
|
|
||||||
if (n == 0)
|
|
||||||
return lctx;
|
|
||||||
if (lctx) {
|
|
||||||
local_entry e = head(lctx);
|
|
||||||
// Simplification rule
|
|
||||||
// lift:s2:n2 lift:s1:n1 ---> lift:s1:n1+n2 when s1 <= s2 <= s1 + n1
|
|
||||||
if (e.is_lift() && e.s() <= s && s <= e.s() + e.n()) {
|
|
||||||
return add_lift(tail(lctx), e.s(), e.n() + n);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
return cons(mk_lift(s, n), lctx);
|
|
||||||
}
|
|
||||||
|
|
||||||
expr add_lift(expr const & m, unsigned s, unsigned n, optional<ro_metavar_env> const & menv) {
|
|
||||||
if (menv && s >= free_var_range(m, *menv))
|
|
||||||
return m;
|
|
||||||
return update_metavar(m, add_lift(metavar_lctx(m), s, n));
|
|
||||||
}
|
|
||||||
|
|
||||||
local_context add_inst(local_context const & lctx, unsigned s, expr const & v) {
|
|
||||||
if (lctx) {
|
|
||||||
local_entry e = head(lctx);
|
|
||||||
if (e.is_lift() && e.s() <= s && s < e.s() + e.n()) {
|
|
||||||
return add_lift(tail(lctx), e.s(), e.n() - 1);
|
|
||||||
}
|
|
||||||
// Simplifications such as
|
|
||||||
// inst:4 #6 lift:5:3 --> lift:4:2
|
|
||||||
// inst:3 #7 lift:4:5 --> lift:3:4
|
|
||||||
// General rule is:
|
|
||||||
// inst:(s-1) #(s+n-2) lift:s:n --> lift:s-1:n-1
|
|
||||||
if (e.is_lift() && is_var(v) && e.s() > 0 && s == e.s() - 1 && e.s() + e.n() > 2 && var_idx(v) == e.s() + e.n() - 2) {
|
|
||||||
return add_lift(tail(lctx), e.s() - 1, e.n() - 1);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
return cons(mk_inst(s, v), lctx);
|
|
||||||
}
|
|
||||||
|
|
||||||
expr add_inst(expr const & m, unsigned s, expr const & v, optional<ro_metavar_env> const & menv) {
|
|
||||||
if (menv && s >= free_var_range(m, *menv))
|
|
||||||
return m;
|
|
||||||
return update_metavar(m, add_inst(metavar_lctx(m), s, v));
|
|
||||||
}
|
|
||||||
|
|
||||||
bool has_local_context(expr const & m) {
|
|
||||||
return static_cast<bool>(metavar_lctx(m));
|
|
||||||
}
|
|
||||||
|
|
||||||
expr pop_meta_context(expr const & m) {
|
|
||||||
lean_assert(has_local_context(m));
|
|
||||||
return update_metavar(m, tail(metavar_lctx(m)));
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
@ -1,389 +0,0 @@
|
||||||
/*
|
|
||||||
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 <utility>
|
|
||||||
#include "util/rc.h"
|
|
||||||
#include "util/pair.h"
|
|
||||||
#include "util/splay_map.h"
|
|
||||||
#include "util/name_generator.h"
|
|
||||||
#include "kernel/expr.h"
|
|
||||||
#include "kernel/context.h"
|
|
||||||
#include "kernel/justification.h"
|
|
||||||
#include "kernel/replace_visitor.h"
|
|
||||||
|
|
||||||
namespace lean {
|
|
||||||
/**
|
|
||||||
\brief Metavar environment (cell). It is an auxiliary datastructure used for:
|
|
||||||
|
|
||||||
1- Creating metavariables.
|
|
||||||
2- Storing their types and the contexts where they were created.
|
|
||||||
3- Storing substitutions.
|
|
||||||
*/
|
|
||||||
class metavar_env_cell {
|
|
||||||
friend class metavar_env;
|
|
||||||
struct data {
|
|
||||||
optional<expr> m_subst; // substitution
|
|
||||||
optional<expr> m_type; // type of the metavariable
|
|
||||||
context m_context; // context where the metavariable was defined
|
|
||||||
justification m_justification; // justification for assigned metavariables.
|
|
||||||
data(optional<expr> const & t = none_expr(), context const & ctx = context()):m_type(t), m_context(ctx) {}
|
|
||||||
};
|
|
||||||
typedef splay_map<name, data, name_quick_cmp> name2data;
|
|
||||||
|
|
||||||
name_generator m_name_generator;
|
|
||||||
name2data m_metavar_data;
|
|
||||||
// If the following flag is true, then beta-reduction is automatically applied
|
|
||||||
// when we apply a substitution containing ?m <- fun (x : T), ...
|
|
||||||
// to an expression containing (?m a)
|
|
||||||
// The motivation is that higher order unification and matching produces a
|
|
||||||
// bunch of assignments of the form ?m <- fun (x : T), ...
|
|
||||||
bool m_beta_reduce_mv;
|
|
||||||
unsigned m_timestamp;
|
|
||||||
MK_LEAN_RC();
|
|
||||||
|
|
||||||
static bool has_metavar(expr const & e) { return ::lean::has_metavar(e); }
|
|
||||||
void dealloc() { delete this; }
|
|
||||||
void inc_timestamp();
|
|
||||||
public:
|
|
||||||
metavar_env_cell();
|
|
||||||
metavar_env_cell(name const & prefix);
|
|
||||||
metavar_env_cell(metavar_env_cell const & other);
|
|
||||||
|
|
||||||
bool beta_reduce_metavar_application() const { return m_beta_reduce_mv; }
|
|
||||||
void set_beta_reduce_metavar_application(bool f) { m_beta_reduce_mv = f; }
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief The timestamp is increased whenever this environment is
|
|
||||||
updated.
|
|
||||||
|
|
||||||
\remark The result is always greater than 0.
|
|
||||||
*/
|
|
||||||
unsigned get_timestamp() const { return m_timestamp; }
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Create a new metavariable in the given context and with the given type.
|
|
||||||
*/
|
|
||||||
expr mk_metavar(context const & ctx = context(), optional<expr> const & type = none_expr());
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Return the context where the given metavariable was created.
|
|
||||||
\pre is_metavar(m)
|
|
||||||
\pre !has_local_context(m)
|
|
||||||
*/
|
|
||||||
context get_context(expr const & m) const;
|
|
||||||
context get_context(name const & m) const;
|
|
||||||
|
|
||||||
unsigned get_context_size(expr const & m) const { return get_context(m).size(); }
|
|
||||||
unsigned get_context_size(name const & m) const { return get_context(m).size(); }
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Return the type of the given metavariable.
|
|
||||||
\pre is_metavar(m)
|
|
||||||
|
|
||||||
\remark If \c m does not have a type associated with it, then a new
|
|
||||||
metavariable is created to represent the type of \c m.
|
|
||||||
|
|
||||||
\remark If \c m has a local context, then the local context is applied.
|
|
||||||
*/
|
|
||||||
expr get_type(expr const & m);
|
|
||||||
expr get_type(name const & m);
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Return true iff \c m has a type associated with it.
|
|
||||||
\pre is_metavar(m)
|
|
||||||
*/
|
|
||||||
bool has_type(expr const & m) const;
|
|
||||||
bool has_type(name const & m) const;
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Return the substitution and justification for the given metavariable.
|
|
||||||
*/
|
|
||||||
optional<std::pair<expr, justification>> get_subst_jst(name const & m) const;
|
|
||||||
optional<std::pair<expr, justification>> get_subst_jst(expr const & m) const;
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Return the justification for an assigned metavariable.
|
|
||||||
\pre is_metavar(m)
|
|
||||||
*/
|
|
||||||
optional<justification> get_justification(expr const & m) const;
|
|
||||||
optional<justification> get_justification(name const & m) const;
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Return true iff the metavariable named \c m is assigned in this substitution.
|
|
||||||
*/
|
|
||||||
bool is_assigned(name const & m) const;
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Return true if the given metavariable is assigned in this
|
|
||||||
substitution.
|
|
||||||
|
|
||||||
\pre is_metavar(m)
|
|
||||||
*/
|
|
||||||
bool is_assigned(expr const & m) const;
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Assign metavariable named \c m.
|
|
||||||
|
|
||||||
\pre !is_assigned(m)
|
|
||||||
|
|
||||||
\remark The method returns false if the assignment cannot be performed
|
|
||||||
because \c t contain free variables that are not available in the context
|
|
||||||
associated with \c m.
|
|
||||||
*/
|
|
||||||
bool assign(name const & m, expr const & t, justification const & j);
|
|
||||||
bool assign(name const & m, expr const & t);
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Assign metavariable \c m to \c t.
|
|
||||||
|
|
||||||
\remark The method returns false if the assignment cannot be performed
|
|
||||||
because \c t contain free variables that are not available in the context
|
|
||||||
associated with \c m.
|
|
||||||
|
|
||||||
\pre is_metavar(m)
|
|
||||||
\pre !has_meta_context(m)
|
|
||||||
\pre !is_assigned(m)
|
|
||||||
*/
|
|
||||||
bool assign(expr const & m, expr const & t, justification const & j);
|
|
||||||
bool assign(expr const & m, expr const & t);
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Return the substitution associated with the given metavariable
|
|
||||||
in this substitution.
|
|
||||||
|
|
||||||
\pre is_metavar(m)
|
|
||||||
*/
|
|
||||||
optional<expr> get_subst(expr const & m) const;
|
|
||||||
optional<expr> get_subst(name const & m) const;
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Apply f to each substitution in the metavariable environment.
|
|
||||||
*/
|
|
||||||
template<typename F>
|
|
||||||
void for_each_subst(F f) const {
|
|
||||||
m_metavar_data.for_each([&](name const & k, data const & d) {
|
|
||||||
if (d.m_subst)
|
|
||||||
f(k, *(d.m_subst));
|
|
||||||
});
|
|
||||||
}
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Return true iff \c e has a metavariable that is assigned in \c menv.
|
|
||||||
*/
|
|
||||||
bool has_assigned_metavar(expr const & e) const;
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Return true iff \c e contains the metavariable \c m.
|
|
||||||
The substitutions in this metavar environment are taken into account.
|
|
||||||
|
|
||||||
\brief is_metavar(m)
|
|
||||||
*/
|
|
||||||
bool has_metavar(expr const & e, expr const & m) const;
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Instantiate the metavariables occurring in \c e with the substitutions
|
|
||||||
provided by \c menv. Store the justification of replace variables in jsts.
|
|
||||||
*/
|
|
||||||
expr instantiate_metavars(expr const & e, buffer<justification> & jsts) const;
|
|
||||||
inline expr instantiate_metavars(expr const & e) const {
|
|
||||||
buffer<justification> tmp;
|
|
||||||
return instantiate_metavars(e, tmp);
|
|
||||||
}
|
|
||||||
context instantiate_metavars(context const & ctx) const;
|
|
||||||
};
|
|
||||||
|
|
||||||
class ro_metavar_env;
|
|
||||||
/**
|
|
||||||
\brief Reference to metavariable environment (cell).
|
|
||||||
*/
|
|
||||||
class metavar_env {
|
|
||||||
friend class optional<metavar_env>;
|
|
||||||
friend class ro_metavar_env;
|
|
||||||
friend class metavar_env_cell;
|
|
||||||
metavar_env_cell * m_ptr;
|
|
||||||
explicit metavar_env(metavar_env_cell * ptr):m_ptr(ptr) { if (m_ptr) m_ptr->inc_ref(); }
|
|
||||||
public:
|
|
||||||
metavar_env():m_ptr(new metavar_env_cell()) { m_ptr->inc_ref(); }
|
|
||||||
metavar_env(name const & prefix):m_ptr(new metavar_env_cell(prefix)) { m_ptr->inc_ref(); }
|
|
||||||
metavar_env(metavar_env const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
|
|
||||||
metavar_env(metavar_env && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
|
|
||||||
~metavar_env() { if (m_ptr) m_ptr->dec_ref(); }
|
|
||||||
metavar_env & operator=(metavar_env const & s) { LEAN_COPY_REF(s); }
|
|
||||||
metavar_env & operator=(metavar_env && s) { LEAN_MOVE_REF(s); }
|
|
||||||
metavar_env_cell * operator->() const { return m_ptr; }
|
|
||||||
metavar_env_cell & operator*() const { return *m_ptr; }
|
|
||||||
metavar_env copy() const { return metavar_env(new metavar_env_cell(*m_ptr)); }
|
|
||||||
friend bool is_eqp(metavar_env const & menv1, metavar_env const & menv2) { return menv1.m_ptr == menv2.m_ptr; }
|
|
||||||
friend bool operator==(metavar_env const & menv1, metavar_env const & menv2) { return is_eqp(menv1, menv2); }
|
|
||||||
typedef metavar_env_cell * ptr;
|
|
||||||
};
|
|
||||||
|
|
||||||
SPECIALIZE_OPTIONAL_FOR_SMART_PTR(metavar_env)
|
|
||||||
inline optional<metavar_env> none_menv() { return optional<metavar_env>(); }
|
|
||||||
inline optional<metavar_env> some_menv(metavar_env const & e) { return optional<metavar_env>(e); }
|
|
||||||
inline optional<metavar_env> some_menv(metavar_env && e) { return optional<metavar_env>(std::forward<metavar_env>(e)); }
|
|
||||||
|
|
||||||
inline expr instantiate_metavars(optional<metavar_env> const & menv, expr const & e) {
|
|
||||||
if (menv)
|
|
||||||
return (*menv)->instantiate_metavars(e);
|
|
||||||
else
|
|
||||||
return e;
|
|
||||||
}
|
|
||||||
|
|
||||||
inline context instantiate_metavars(optional<metavar_env> const & menv, context const & ctx) {
|
|
||||||
if (menv)
|
|
||||||
return (*menv)->instantiate_metavars(ctx);
|
|
||||||
else
|
|
||||||
return ctx;
|
|
||||||
}
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Read-only reference to metavariable environment (cell).
|
|
||||||
*/
|
|
||||||
class ro_metavar_env {
|
|
||||||
friend class optional<ro_metavar_env>;
|
|
||||||
friend class metavar_env;
|
|
||||||
metavar_env_cell * m_ptr;
|
|
||||||
explicit ro_metavar_env(metavar_env_cell * ptr):m_ptr(ptr) { if (m_ptr) m_ptr->inc_ref(); }
|
|
||||||
friend class type_checker;
|
|
||||||
/*
|
|
||||||
\brief (Hack) The following two methods are used by the type_checker. Some methods
|
|
||||||
in the type checker only need read-only access when unification constraints are not
|
|
||||||
used. For these methods, we can relax the interface and accept a read-only metavariable
|
|
||||||
environment. However, the type checker internally uses the read-write version. So,
|
|
||||||
this constructor is a hack to workaround that.
|
|
||||||
*/
|
|
||||||
static optional<metavar_env> const & to_rw(optional<ro_metavar_env> const & menv) { return reinterpret_cast<optional<metavar_env> const &>(menv); }
|
|
||||||
metavar_env const & to_rw() const { return reinterpret_cast<metavar_env const&>(*this); }
|
|
||||||
public:
|
|
||||||
ro_metavar_env():m_ptr(new metavar_env_cell()) { m_ptr->inc_ref(); }
|
|
||||||
ro_metavar_env(metavar_env const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
|
|
||||||
ro_metavar_env(ro_metavar_env const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
|
|
||||||
ro_metavar_env(ro_metavar_env && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
|
|
||||||
~ro_metavar_env() { if (m_ptr) m_ptr->dec_ref(); }
|
|
||||||
ro_metavar_env & operator=(ro_metavar_env const & s) { LEAN_COPY_REF(s); }
|
|
||||||
ro_metavar_env & operator=(ro_metavar_env && s) { LEAN_MOVE_REF(s); }
|
|
||||||
metavar_env_cell const * operator->() const { return m_ptr; }
|
|
||||||
metavar_env_cell const & operator*() const { return *m_ptr; }
|
|
||||||
metavar_env copy() const { return metavar_env(new metavar_env_cell(*m_ptr)); }
|
|
||||||
friend bool is_eqp(ro_metavar_env const & menv1, ro_metavar_env const & menv2) { return menv1.m_ptr == menv2.m_ptr; }
|
|
||||||
friend bool operator==(ro_metavar_env const & menv1, ro_metavar_env const & menv2) { return is_eqp(menv1, menv2); }
|
|
||||||
typedef metavar_env_cell const * ptr;
|
|
||||||
};
|
|
||||||
|
|
||||||
SPECIALIZE_OPTIONAL_FOR_SMART_PTR(ro_metavar_env)
|
|
||||||
inline optional<ro_metavar_env> none_ro_menv() { return optional<ro_metavar_env>(); }
|
|
||||||
inline optional<ro_metavar_env> some_ro_menv(ro_metavar_env const & e) { return optional<ro_metavar_env>(e); }
|
|
||||||
inline optional<ro_metavar_env> some_ro_menv(ro_metavar_env && e) { return optional<ro_metavar_env>(std::forward<ro_metavar_env>(e)); }
|
|
||||||
inline optional<ro_metavar_env> const & to_ro_menv(optional<metavar_env> const & menv) { return reinterpret_cast<optional<ro_metavar_env> const &>(menv); }
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Template for creating a cached reference to a metavariable
|
|
||||||
environment + timestamp at the time of the caching. This object may
|
|
||||||
also cache optional references.
|
|
||||||
|
|
||||||
We use this template for cached_metavar_env and cached_ro_metavar_env
|
|
||||||
*/
|
|
||||||
template<typename MEnv>
|
|
||||||
class cached_metavar_env_tpl {
|
|
||||||
optional<MEnv> m_menv;
|
|
||||||
unsigned m_timestamp;
|
|
||||||
public:
|
|
||||||
cached_metavar_env_tpl():m_timestamp(0) {}
|
|
||||||
void clear() { m_menv = optional<MEnv>(); m_timestamp = 0; }
|
|
||||||
/**
|
|
||||||
\brief Updated the cached value with menv.
|
|
||||||
Return true if menv is different from the the cached metavar_env, or if
|
|
||||||
the timestamp is different.
|
|
||||||
*/
|
|
||||||
bool update(optional<MEnv> const & menv);
|
|
||||||
bool update(MEnv const & menv) { return update(optional<MEnv>(menv)); }
|
|
||||||
explicit operator bool() const { return static_cast<bool>(m_menv); }
|
|
||||||
optional<MEnv> const & to_some_menv() const { return m_menv; }
|
|
||||||
MEnv operator*() const { return *m_menv; }
|
|
||||||
typename MEnv::ptr operator->() const { lean_assert(m_menv); return (*m_menv).operator->(); }
|
|
||||||
};
|
|
||||||
|
|
||||||
class cached_metavar_env : public cached_metavar_env_tpl<metavar_env> {
|
|
||||||
public:
|
|
||||||
optional<ro_metavar_env> const & to_some_ro_menv() const { return to_ro_menv(to_some_menv()); }
|
|
||||||
};
|
|
||||||
|
|
||||||
typedef cached_metavar_env_tpl<ro_metavar_env> cached_ro_metavar_env;
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Apply the changes in \c lctx to \c a.
|
|
||||||
*/
|
|
||||||
expr apply_local_context(expr const & a, local_context const & lctx, optional<ro_metavar_env> const & menv);
|
|
||||||
inline expr apply_local_context(expr const & a, local_context const & lctx, ro_metavar_env const & menv) { return apply_local_context(a, lctx, some_ro_menv(menv)); }
|
|
||||||
inline expr apply_local_context(expr const & a, local_context const & lctx) { return apply_local_context(a, lctx, none_ro_menv()); }
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Extend the local context \c lctx with the entry <tt>lift:s:n</tt>
|
|
||||||
*/
|
|
||||||
local_context add_lift(local_context const & lctx, unsigned s, unsigned n);
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Add a lift:s:n operation to the context of the given metavariable.
|
|
||||||
|
|
||||||
\pre is_metavar(m)
|
|
||||||
|
|
||||||
\remark If menv is not none, then we use \c free_var_range to compute the free variables that may
|
|
||||||
occur in \c m. If s > the maximum free variable that occurs in \c m, then
|
|
||||||
we do not add a lift local entry to the local context.
|
|
||||||
*/
|
|
||||||
expr add_lift(expr const & m, unsigned s, unsigned n, optional<ro_metavar_env> const & menv);
|
|
||||||
inline expr add_lift(expr const & m, unsigned s, unsigned n) { return add_lift(m, s, n, none_ro_menv()); }
|
|
||||||
inline expr add_lift(expr const & m, unsigned s, unsigned n, ro_metavar_env const & menv) { return add_lift(m, s, n, some_ro_menv(menv)); }
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Extend the local context \c lctx with the entry <tt>inst:s v</tt>
|
|
||||||
*/
|
|
||||||
local_context add_inst(local_context const & lctx, unsigned s, expr const & v);
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Add an inst:s:v operation to the context of the given metavariable.
|
|
||||||
|
|
||||||
\pre is_metavar(m)
|
|
||||||
|
|
||||||
\remark If menv is not none, then we use \c free_var_range to compute the free variables that may
|
|
||||||
occur in \c m. If s > the maximum free variable that occurs in \c m, then
|
|
||||||
we do not add an inst local entry to the local context.
|
|
||||||
*/
|
|
||||||
expr add_inst(expr const & m, unsigned s, expr const & v, optional<ro_metavar_env> const & menv);
|
|
||||||
inline expr add_inst(expr const & m, unsigned s, expr const & v) { return add_inst(m, s, v, none_ro_menv()); }
|
|
||||||
inline expr add_inst(expr const & m, unsigned s, expr const & v, ro_metavar_env const & menv) { return add_inst(m, s, v, some_ro_menv(menv)); }
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Return true iff the given metavariable has a non-empty
|
|
||||||
local context associated with it.
|
|
||||||
|
|
||||||
\pre is_metavar(m)
|
|
||||||
*/
|
|
||||||
bool has_local_context(expr const & m);
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Return the same metavariable, but the head of the context is removed.
|
|
||||||
|
|
||||||
\pre is_metavar(m)
|
|
||||||
\pre has_meta_context(m)
|
|
||||||
*/
|
|
||||||
expr pop_meta_context(expr const & m);
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Return true iff \c e has a metavariable that is assigned in \c menv.
|
|
||||||
*/
|
|
||||||
bool has_assigned_metavar(expr const & e, ro_metavar_env const & menv);
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Return true iff \c e contains the metavariable \c m.
|
|
||||||
The substitutions in \c menv are taken into account.
|
|
||||||
|
|
||||||
\brief is_metavar(m)
|
|
||||||
*/
|
|
||||||
bool has_metavar(expr const & e, expr const & m, ro_metavar_env const & menv);
|
|
||||||
}
|
|
||||||
|
|
@ -1,97 +0,0 @@
|
||||||
/*
|
|
||||||
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 <utility>
|
|
||||||
#include <vector>
|
|
||||||
#include "util/safe_arith.h"
|
|
||||||
#include "util/pair.h"
|
|
||||||
#include "util/buffer.h"
|
|
||||||
#include "kernel/universe_constraints.h"
|
|
||||||
|
|
||||||
namespace lean {
|
|
||||||
optional<int> universe_constraints::get_distance(name const & n1, name const & n2) const {
|
|
||||||
auto it = m_distances.find(mk_pair(n1, n2));
|
|
||||||
if (it != m_distances.end())
|
|
||||||
return optional<int>(it->second);
|
|
||||||
else
|
|
||||||
return optional<int>();
|
|
||||||
}
|
|
||||||
|
|
||||||
void universe_constraints::add_var(name const & n) {
|
|
||||||
lean_assert(!get_distance(n, n));
|
|
||||||
m_distances[mk_pair(n, n)] = 0;
|
|
||||||
m_outgoing_edges[n].emplace_back(n, 0);
|
|
||||||
m_incoming_edges[n].emplace_back(n, 0);
|
|
||||||
}
|
|
||||||
|
|
||||||
bool universe_constraints::contains(name const & n) const {
|
|
||||||
return static_cast<bool>(get_distance(n, n));
|
|
||||||
}
|
|
||||||
|
|
||||||
bool universe_constraints::is_implied(name const & n1, name const & n2, int k) const {
|
|
||||||
auto d = get_distance(n1, n2);
|
|
||||||
return d && *d >= k;
|
|
||||||
}
|
|
||||||
|
|
||||||
bool universe_constraints::is_consistent(name const & n1, name const & n2, int k) const {
|
|
||||||
// we just check if n2 >= n1 - k + 1 is not implied
|
|
||||||
return !is_implied(n2, n1, safe_add(safe_sub(0, k), 1));
|
|
||||||
}
|
|
||||||
|
|
||||||
bool universe_constraints::overflows(name const & n1, name const & n2, int k) const {
|
|
||||||
try {
|
|
||||||
auto it1 = m_incoming_edges.find(n1);
|
|
||||||
if (it1 != m_incoming_edges.end()) {
|
|
||||||
for (auto const & in : it1->second)
|
|
||||||
safe_add(in.second, k);
|
|
||||||
}
|
|
||||||
auto it2 = m_outgoing_edges.find(n2);
|
|
||||||
if (it2 != m_outgoing_edges.end()) {
|
|
||||||
for (auto const & out : it2->second)
|
|
||||||
safe_add(out.second, k);
|
|
||||||
}
|
|
||||||
return false;
|
|
||||||
} catch (...) {
|
|
||||||
return true;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Add the pair (n, k) to entries if it does not contain an entry (n, k').
|
|
||||||
Otherwise, replace entry (n, k') with (n, k).
|
|
||||||
*/
|
|
||||||
static void updt_entry(std::vector<std::pair<name, int>> & entries, name const & n, int k) {
|
|
||||||
auto it = std::find_if(entries.begin(), entries.end(), [&](std::pair<name, int> const & p) { return p.first == n; });
|
|
||||||
if (it == entries.end())
|
|
||||||
entries.emplace_back(n, k);
|
|
||||||
else
|
|
||||||
it->second = k;
|
|
||||||
}
|
|
||||||
|
|
||||||
void universe_constraints::add_constraint(name const & n1, name const & n2, int k) {
|
|
||||||
lean_assert(contains(n1));
|
|
||||||
lean_assert(contains(n2));
|
|
||||||
lean_assert(is_consistent(n1, n2, k));
|
|
||||||
if (is_implied(n1, n2, k))
|
|
||||||
return; // redundant
|
|
||||||
buffer<std::tuple<name, name, int>> to_add;
|
|
||||||
for (auto const & in : m_incoming_edges[n1])
|
|
||||||
to_add.emplace_back(in.first, n2, safe_add(in.second, k));
|
|
||||||
for (auto const & out : m_outgoing_edges[n2])
|
|
||||||
to_add.emplace_back(n1, out.first, safe_add(out.second, k));
|
|
||||||
for (auto const & e : to_add) {
|
|
||||||
name const & from = std::get<0>(e);
|
|
||||||
name const & to = std::get<1>(e);
|
|
||||||
int new_k = std::get<2>(e);
|
|
||||||
auto old_k = get_distance(from, to);
|
|
||||||
if (!old_k || new_k > *old_k) {
|
|
||||||
updt_entry(m_outgoing_edges[from], to, new_k);
|
|
||||||
updt_entry(m_incoming_edges[to], from, new_k);
|
|
||||||
m_distances[mk_pair(from, to)] = new_k;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
@ -1,73 +0,0 @@
|
||||||
/*
|
|
||||||
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 <unordered_map>
|
|
||||||
#include <utility>
|
|
||||||
#include <functional>
|
|
||||||
#include <vector>
|
|
||||||
#include "util/name.h"
|
|
||||||
#include "util/hash.h"
|
|
||||||
#include "util/name_map.h"
|
|
||||||
#include "util/optional.h"
|
|
||||||
|
|
||||||
namespace lean {
|
|
||||||
/**
|
|
||||||
\brief Store the set of universe constraints.
|
|
||||||
|
|
||||||
It is based on Floyd-Warshall all-pairs shortest path algorithm.
|
|
||||||
*/
|
|
||||||
class universe_constraints {
|
|
||||||
typedef std::pair<name, int> edge;
|
|
||||||
typedef std::vector<edge> edges;
|
|
||||||
typedef name_map<edges> node_to_edges;
|
|
||||||
typedef std::pair<name, name> name_pair;
|
|
||||||
struct name_pair_hash_fn {
|
|
||||||
unsigned operator()(name_pair const & p) const { return hash(p.first.hash(), p.second.hash()); }
|
|
||||||
};
|
|
||||||
typedef std::unordered_map<name_pair, int, name_pair_hash_fn, std::equal_to<name_pair>> distances;
|
|
||||||
node_to_edges m_incoming_edges;
|
|
||||||
node_to_edges m_outgoing_edges;
|
|
||||||
distances m_distances;
|
|
||||||
public:
|
|
||||||
/**
|
|
||||||
\brief Add a new variable.
|
|
||||||
|
|
||||||
\pre The variables does not exist in this set of constraints.
|
|
||||||
*/
|
|
||||||
void add_var(name const & n);
|
|
||||||
/**
|
|
||||||
\brief Return true iff this set of constraints contains the variable n.
|
|
||||||
That is, it was added using add_var.
|
|
||||||
*/
|
|
||||||
bool contains(name const & n) const;
|
|
||||||
/** \brief Return true iff n1 >= n2 + k is implied by this set of constraints. */
|
|
||||||
bool is_implied(name const & n1, name const & n2, int k) const;
|
|
||||||
/** \brief Return true iff n1 < n2 + k is not implied by this set of constraints. */
|
|
||||||
bool is_consistent(name const & n1, name const & n2, int k) const;
|
|
||||||
/**
|
|
||||||
\brief Return true iff the constraint n1 >= n2 + k produces an integer overflow when added
|
|
||||||
to the set of constraints.
|
|
||||||
*/
|
|
||||||
bool overflows(name const & n1, name const & n2, int k) const;
|
|
||||||
/**
|
|
||||||
\brief Add new constraint n1 >= n2 + k.
|
|
||||||
|
|
||||||
\pre is_consistent(n1, n2, k)
|
|
||||||
\pre contains(n1)
|
|
||||||
\pre contains(n2)
|
|
||||||
*/
|
|
||||||
void add_constraint(name const & n1, name const & n2, int k);
|
|
||||||
/**
|
|
||||||
\brief Return the "distance" between n1 and n2.
|
|
||||||
That is, the best k s.t. n1 >= n2 + k is implied by this set of constraints
|
|
||||||
but n1 >= n2 + k + i is not for any i > 0.
|
|
||||||
|
|
||||||
If there is no such k, then return none.
|
|
||||||
*/
|
|
||||||
optional<int> get_distance(name const & n1, name const & n2) const;
|
|
||||||
};
|
|
||||||
}
|
|
||||||
|
|
@ -1,34 +0,0 @@
|
||||||
/*
|
|
||||||
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 "kernel/expr.h"
|
|
||||||
|
|
||||||
namespace lean {
|
|
||||||
/**
|
|
||||||
\brief Base class for values that have a hierarchical attached to it.
|
|
||||||
*/
|
|
||||||
class named_value : public value {
|
|
||||||
name m_name;
|
|
||||||
public:
|
|
||||||
named_value(name const & n):m_name(n) {}
|
|
||||||
virtual ~named_value() {}
|
|
||||||
virtual name get_name() const { return m_name; }
|
|
||||||
virtual bool is_atomic_pp(bool /* unicode */, bool /* coercion */) const { return true; } // NOLINT
|
|
||||||
};
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Base class for values that have a hierarchical name and a type
|
|
||||||
attached to it.
|
|
||||||
*/
|
|
||||||
class const_value : public named_value {
|
|
||||||
expr m_type;
|
|
||||||
public:
|
|
||||||
const_value(name const & n, expr const & t):named_value(n), m_type(t) {}
|
|
||||||
virtual ~const_value() {}
|
|
||||||
virtual expr get_type() const { return m_type; }
|
|
||||||
};
|
|
||||||
}
|
|
||||||
Loading…
Reference in a new issue