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

refactor(metavar): reorganize and simplify metavariables

Browse source 
- Use hierarchical names instead of unsigned integers to identify metavariables.
- Associate type with metavariable.
- Replace metavar_env with substitution.
- Rename meta_ctx --> local_ctx
- Rename meta_entry --> local_entry
- Disable old elaborator
- Rename unification_problems to unification_constraints
- Add metavar_generator
- Fix metavar unit tests
- Modify type checker to use metavar_generator
- Fix placeholder module

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-26 18:24:45 -07:00
parent 3387c300a0
commit 59914a36f3
31 changed files with 874 additions and 1728 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

889
src/frontends/lean/elaborator.cpp
View file

@ -53,882 +53,17 @@ expr const & get_choice(expr const & e, unsigned i) {
return arg(eq_rhs(e), i); return arg(eq_rhs(e), i);
} }
class elaborator::imp { elaborator::elaborator(frontend const & ) {}
// Information for producing error messages regarding application type mismatch during elaboration
struct app_mismatch_info {
expr m_app; // original application
context m_ctx; // context where application occurs
std::vector<expr> m_args; // arguments after processing
std::vector<expr> m_types; // inferred types of the arguments
app_mismatch_info(expr const & app, context const & ctx, unsigned sz, expr const * args, expr const * types):
m_app(app), m_ctx(ctx), m_args(args, args+sz), m_types(types, types+sz) {}
};
// Information for producing error messages regarding expected type mismatch during elaboration
struct expected_type_info {
expr m_expr; // original expression
expr m_processed_expr; // expression after processing
expr m_expected; // expected type
expr m_given; // inferred type of the processed expr.
context m_ctx;
expected_type_info(expr const & e, expr const & p, expr const & exp, expr const & given, context const & ctx):
m_expr(e), m_processed_expr(p), m_expected(exp), m_given(given), m_ctx(ctx) {}
};
enum class info_kind { AppMismatchInfo, ExpectedTypeInfo };
typedef std::pair<info_kind, unsigned> info_ref;
std::vector<app_mismatch_info> m_app_mismatch_info;
std::vector<expected_type_info> m_expected_type_info;
info_ref mk_app_mismatch_info(expr const & app, context const & ctx, unsigned sz, expr const * args, expr const * types) {
unsigned idx = m_app_mismatch_info.size();
m_app_mismatch_info.push_back(app_mismatch_info(app, ctx, sz, args, types));
return mk_pair(info_kind::AppMismatchInfo, idx);
}
info_ref mk_expected_type_info(expr const & e, expr const & p, expr const & exp, expr const & g, context const & ctx) {
unsigned idx = m_expected_type_info.size();
m_expected_type_info.push_back(expected_type_info(e, p, exp, g, ctx));
return mk_pair(info_kind::ExpectedTypeInfo, idx);
}
context get_context(info_ref const & r) const {
if (r.first == info_kind::AppMismatchInfo)
return m_app_mismatch_info[r.second].m_ctx;
else
return m_expected_type_info[r.second].m_ctx;
}
// unification constraint lhs == second
struct constraint {
expr m_lhs;
expr m_rhs;
context m_ctx;
info_ref m_info;
constraint(expr const & lhs, expr const & rhs, context const & ctx, info_ref const & r):
m_lhs(lhs), m_rhs(rhs), m_ctx(ctx), m_info(r) {}
constraint(expr const & lhs, expr const & rhs, constraint const & c):
m_lhs(lhs), m_rhs(rhs), m_ctx(c.m_ctx), m_info(c.m_info) {}
constraint(expr const & lhs, expr const & rhs, context const & ctx, constraint const & c):
m_lhs(lhs), m_rhs(rhs), m_ctx(ctx), m_info(c.m_info) {}
};
// information associated with the metavariable
struct metavar_info {
expr m_assignment;
expr m_type;
expr m_mvar;
context m_ctx;
bool m_mark; // for implementing occurs check
bool m_type_cnstr; // true when type constraint was already generated
metavar_info() {
m_mark = false;
m_type_cnstr = false;
}
};
typedef std::deque<constraint> constraint_queue;
typedef std::vector<metavar_info> metavars;
frontend const & m_frontend;
environment const & m_env;
name_set const * m_available_defs;
elaborator const * m_owner;
expr m_root;
constraint_queue m_constraints;
metavars m_metavars;
normalizer m_normalizer;
bool m_processing_root;
// The following mapping is used to store the relationship
// between elaborated expressions and non-elaborated expressions.
// We need that because a frontend may associate line number information
// with the original non-elaborated expressions.
expr_map<expr> m_trace;
volatile bool m_interrupted;
void add_trace(expr const & old_e, expr const & new_e) {
if (!is_eqp(old_e, new_e)) {
m_trace[new_e] = old_e;
}
}
expr mk_metavar(context const & ctx) {
unsigned midx = m_metavars.size();
expr r = ::lean::mk_metavar(midx);
m_metavars.push_back(metavar_info());
m_metavars[midx].m_mvar = r;
m_metavars[midx].m_ctx = ctx;
return r;
}
expr metavar_type(expr const & m) {
lean_assert(is_metavar(m));
unsigned midx = metavar_idx(m);
if (m_metavars[midx].m_type) {
return m_metavars[midx].m_type;
} else {
context ctx = m_metavars[midx].m_ctx;
expr t = mk_metavar(ctx);
m_metavars[midx].m_type = t;
return t;
}
}
expr lookup(context const & c, unsigned i) {
auto p = lookup_ext(c, i);
context_entry const & def = p.first;
context const & def_c = p.second;
lean_assert(c.size() > def_c.size());
return lift_free_vars(def.get_domain(), 0, c.size() - def_c.size());
}
expr check_pi(expr const & e, context const & ctx, expr const & s, context const & s_ctx) {
check_interrupted(m_interrupted);
if (is_pi(e)) {
return e;
} else {
expr r = head_reduce(e, m_env, ctx, m_available_defs);
if (!is_eqp(r, e)) {
return check_pi(r, ctx, s, s_ctx);
} else if (is_var(e)) {
try {
auto p = lookup_ext(ctx, var_idx(e));
context_entry const & entry = p.first;
context const & entry_ctx = p.second;
if (entry.get_body()) {
return lift_free_vars(check_pi(entry.get_body(), entry_ctx, s, s_ctx), 0, ctx.size() - entry_ctx.size());
}
} catch (exception&) {
// this can happen if we access a variable out of scope
throw function_expected_exception(m_env, s_ctx, s);
}
} else if (has_assigned_metavar(e)) {
return check_pi(instantiate(e), ctx, s, s_ctx);
} else if (is_metavar(e) && !has_meta_context(e)) {
// e is a unassigned metavariable that must be a Pi,
// then we can assign it to (Pi x : A, B x), where
// A and B are fresh metavariables
unsigned midx = metavar_idx(e);
expr A = mk_metavar(ctx);
name x("x");
context ctx2 = extend(ctx, x, A);
expr B = mk_metavar(ctx2);
expr type = mk_pi(x, A, B(Var(0)));
m_metavars[midx].m_assignment = type;
return type;
}
throw function_expected_exception(m_env, s_ctx, s);
}
}
level check_universe(expr const & e, context const & ctx, expr const & s, context const & s_ctx) {
check_interrupted(m_interrupted);
if (is_metavar(e)) {
// approx: assume it is level 0
return level();
} else if (is_type(e)) {
return ty_level(e);
} else if (e == Bool) {
return level();
} else {
expr r = head_reduce(e, m_env, ctx, m_available_defs);
if (!is_eqp(r, e)) {
return check_universe(r, ctx, s, s_ctx);
} else if (is_var(e)) {
try {
auto p = lookup_ext(ctx, var_idx(e));
context_entry const & entry = p.first;
context const & entry_ctx = p.second;
if (entry.get_body()) {
return check_universe(entry.get_body(), entry_ctx, s, s_ctx);
}
} catch (exception&) {
// this can happen if we access a variable out of scope
throw type_expected_exception(m_env, s_ctx, s);
}
} else if (has_assigned_metavar(e)) {
return check_universe(instantiate(e), ctx, s, s_ctx);
}
throw type_expected_exception(m_env, s_ctx, s);
}
}
bool is_convertible(expr const & t1, expr const & t2, context const & ctx) {
return m_normalizer.is_convertible(t1, t2, ctx);
}
void choose(buffer<expr> const & f_choices, buffer<expr> const & f_choice_types,
buffer<expr> & args, buffer<expr> & types,
context const & ctx, expr const & src) {
lean_assert(f_choices.size() == f_choice_types.size());
buffer<unsigned> good_choices;
unsigned best_num_coercions = std::numeric_limits<unsigned>::max();
unsigned num_choices = f_choices.size();
unsigned num_args = args.size();
// We consider two overloads ambiguous if they need the same number of coercions.
for (unsigned j = 0; j < num_choices; j++) {
expr f_t = f_choice_types[j];
unsigned num_coercions = 0; // number of coercions needed by current choice
try {
unsigned i = 1;
for (; i < num_args; i++) {
f_t = check_pi(f_t, ctx, src, ctx);
expr expected = abst_domain(f_t);
expr given = types[i];
if (!has_metavar(expected) && !has_metavar(given)) {
if (is_convertible(given, expected, ctx)) {
// compatible
} else if (m_frontend.get_coercion(given, expected, ctx)) {
// compatible if using coercion
num_coercions++;
} else {
break; // failed
}
}
f_t = ::lean::instantiate(abst_body(f_t), args[i]);
}
if (i == num_args) {
if (num_coercions < best_num_coercions) {
// found best choice
args[0] = f_choices[j];
types[0] = f_choice_types[j];
good_choices.clear();
best_num_coercions = num_coercions;
}
good_choices.push_back(j);
}
} catch (exception & ex) {
// candidate failed
// do nothing
}
}
if (good_choices.size() == 0) {
throw no_overload_exception(*m_owner, ctx, src, f_choices.size(), f_choices.data(), f_choice_types.data(),
args.size() - 1, args.data() + 1, types.data() + 1);
} else if (good_choices.size() == 1) {
// found overload
return;
} else {
buffer<expr> good_f_choices;
buffer<expr> good_f_choice_types;
for (unsigned j : good_choices) {
good_f_choices.push_back(f_choices[j]);
good_f_choice_types.push_back(f_choice_types[j]);
}
throw ambiguous_overload_exception(*m_owner, ctx, src, good_f_choices.size(), good_f_choices.data(), good_f_choice_types.data(),
args.size() - 1, args.data() + 1, types.data() + 1);
}
}
/**
\brief Traverse the expression \c e, and compute
1- A new expression that does not contain choice expressions,
coercions have been added when appropriate, and placeholders
have been replaced with metavariables.
2- The type of \c e.
It also populates m_constraints with a set of constraints that
need to be solved to infer the value of the metavariables.
*/
expr_pair process(expr const & e, context const & ctx) {
check_interrupted(m_interrupted);
switch (e.kind()) {
case expr_kind::MetaVar:
return expr_pair(e, metavar_type(e));
case expr_kind::Constant:
if (is_placeholder(e)) {
expr m = mk_metavar(ctx);
m_trace[m] = e;
return expr_pair(m, metavar_type(m));
} else {
return expr_pair(e, m_env.get_object(const_name(e)).get_type());
}
case expr_kind::Var:
return expr_pair(e, lookup(ctx, var_idx(e)));
case expr_kind::Type:
return expr_pair(e, mk_type(ty_level(e) + 1));
case expr_kind::Value:
return expr_pair(e, to_value(e).get_type());
case expr_kind::App: {
buffer<expr> args;
buffer<expr> types;
buffer<expr> f_choices;
buffer<expr> f_choice_types;
unsigned num = num_args(e);
unsigned i = 0;
bool modified = false;
expr const & f = arg(e, 0);
if (is_metavar(f)) {
throw invalid_placeholder_exception(*m_owner, ctx, e);
} else if (is_choice(f)) {
unsigned num_alts = get_num_choices(f);
for (unsigned j = 0; j < num_alts; j++) {
auto p = process(get_choice(f, j), ctx);
f_choices.push_back(p.first);
f_choice_types.push_back(p.second);
}
args.push_back(expr()); // placeholder
types.push_back(expr()); // placeholder
modified = true;
i++;
}
for (; i < num; i++) {
expr const & a_i = arg(e, i);
auto p = process(a_i, ctx);
if (!is_eqp(p.first, a_i))
modified = true;
args.push_back(p.first);
types.push_back(p.second);
}
if (!f_choices.empty()) {
// choose one of the functions (overloads) based on the types in types
choose(f_choices, f_choice_types, args, types, ctx, e);
}
expr f_t = types[0];
for (unsigned i = 1; i < num; i++) {
f_t = check_pi(f_t, ctx, e, ctx);
if (m_processing_root) {
expr expected = abst_domain(f_t);
expr given = types[i];
if (has_metavar(expected) || has_metavar(given)) {
info_ref r = mk_app_mismatch_info(e, ctx, args.size(), args.data(), types.data());
m_constraints.push_back(constraint(expected, given, ctx, r));
} else {
if (!is_convertible(given, expected, ctx)) {
expr coercion = m_frontend.get_coercion(given, expected, ctx);
if (coercion) {
modified = true;
args[i] = mk_app(coercion, args[i]);
} else {
throw app_type_mismatch_exception(m_env, ctx, e, types.size(), types.data());
}
}
}
}
f_t = ::lean::instantiate(abst_body(f_t), args[i]);
}
if (modified) {
expr new_e = mk_app(args.size(), args.data());
m_trace[new_e] = e;
return expr_pair(new_e, f_t);
} else {
return expr_pair(e, f_t);
}
}
case expr_kind::Eq: {
auto lhs_p = process(eq_lhs(e), ctx);
auto rhs_p = process(eq_rhs(e), ctx);
expr new_e = update_eq(e, lhs_p.first, rhs_p.first);
add_trace(e, new_e);
return expr_pair(new_e, mk_bool_type());
}
case expr_kind::Pi: {
auto d_p = process(abst_domain(e), ctx);
auto b_p = process(abst_body(e), extend(ctx, abst_name(e), d_p.first));
expr t = mk_type(max(check_universe(d_p.second, ctx, e, ctx), check_universe(b_p.second, ctx, e, ctx)));
expr new_e = update_pi(e, d_p.first, b_p.first);
add_trace(e, new_e);
return expr_pair(new_e, t);
}
case expr_kind::Lambda: {
auto d_p = process(abst_domain(e), ctx);
auto b_p = process(abst_body(e), extend(ctx, abst_name(e), d_p.first));
expr t = mk_pi(abst_name(e), d_p.first, b_p.second);
expr new_e = update_lambda(e, d_p.first, b_p.first);
add_trace(e, new_e);
return expr_pair(new_e, t);
}
case expr_kind::Let: {
expr_pair t_p;
if (let_type(e))
t_p = process(let_type(e), ctx);
auto v_p = process(let_value(e), ctx);
if (let_type(e)) {
expr const & expected = t_p.first;
expr const & given = v_p.second;
if (has_metavar(expected) || has_metavar(given)) {
info_ref r = mk_expected_type_info(let_value(e), v_p.first, expected, given, ctx);
m_constraints.push_back(constraint(expected, given, ctx, r));
} else {
if (!is_convertible(given, expected, ctx)) {
expr coercion = m_frontend.get_coercion(given, expected, ctx);
if (coercion) {
v_p.first = mk_app(coercion, v_p.first);
} else {
throw def_type_mismatch_exception(m_env, ctx, let_name(e), let_type(e), v_p.first, v_p.second);
}
}
}
}
auto b_p = process(let_body(e), extend(ctx, let_name(e), t_p.first ? t_p.first : v_p.second, v_p.first));
expr t = ::lean::instantiate(b_p.second, v_p.first);
expr new_e = update_let(e, t_p.first, v_p.first, b_p.first);
add_trace(e, new_e);
return expr_pair(new_e, t);
}}
lean_unreachable();
}
expr infer(expr const & e, context const & ctx) {
return process(e, ctx).second;
}
bool is_simple_ho_match(expr const & e1, context const & ctx) {
if (is_app(e1) && is_metavar(arg(e1, 0)) && is_var(arg(e1, 1), 0) && num_args(e1) == 2 && !empty(ctx)) {
return true;
} else {
return false;
}
}
void unify_simple_ho_match(expr const & e1, expr const & e2, constraint const & c) {
context const & ctx = c.m_ctx;
context_entry const & head = ::lean::lookup(ctx, 0);
m_constraints.push_back(constraint(arg(e1, 0), mk_lambda(head.get_name(),
lift_free_vars(head.get_domain(), 1, 1),
lift_free_vars(e2, 1, 1)), c));
}
struct cycle_detected {};
void occ_core(expr const & t) {
check_interrupted(m_interrupted);
auto proc = [&](expr const & e, unsigned) {
if (is_metavar(e)) {
unsigned midx = metavar_idx(e);
if (m_metavars[midx].m_mark)
throw cycle_detected();
if (m_metavars[midx].m_assignment) {
flet<bool> set(m_metavars[midx].m_mark, true);
occ_core(m_metavars[midx].m_assignment);
}
}
};
for_each_fn<decltype(proc)> visitor(proc);
visitor(t);
}
// occurs check
bool occ(expr const & t, unsigned midx) {
lean_assert(!m_metavars[midx].m_mark);
flet<bool> set(m_metavars[midx].m_mark, true);
try {
occ_core(t);
return true;
} catch (cycle_detected&) {
return false;
}
}
[[noreturn]] void throw_unification_exception(constraint const & c) {
// display(std::cout);
m_constraints.push_back(c);
info_ref const & r = c.m_info;
if (r.first == info_kind::AppMismatchInfo) {
app_mismatch_info & info = m_app_mismatch_info[r.second];
for (expr & arg : info.m_args)
arg = instantiate(arg);
for (expr & type : info.m_types)
type = instantiate(type);
throw unification_app_mismatch_exception(*m_owner, info.m_ctx, info.m_app, info.m_args, info.m_types);
} else {
expected_type_info & info = m_expected_type_info[r.second];
info.m_processed_expr = instantiate(info.m_processed_expr);
info.m_given = instantiate(info.m_given);
info.m_expected = instantiate(info.m_expected);
throw unification_type_mismatch_exception(*m_owner, info.m_ctx, info.m_expr, info.m_processed_expr,
info.m_expected, info.m_given);
}
}
void solve_mvar(expr const & m, expr const & t, constraint const & c) {
lean_assert(is_metavar(m) && !has_meta_context(m));
unsigned midx = metavar_idx(m);
if (m_metavars[midx].m_assignment) {
m_constraints.push_back(constraint(m_metavars[midx].m_assignment, t, c));
} else if (has_metavar(t, midx) || !occ(t, midx)) {
throw_unification_exception(c);
} else {
m_metavars[midx].m_assignment = t;
}
}
/**
\brief Temporary hack until we build the new elaborator.
*/
expr instantiate_metavar(expr const & e, unsigned midx, expr const & v) {
metavar_env menv;
while (!menv.contains(midx))
menv.mk_metavar();
menv.assign(midx, v);
return instantiate_metavars(e, menv);
}
/**
\brief Temporary hack until we build the new elaborator.
*/
bool is_lift(expr const & e, expr & c, unsigned & s, unsigned & n) {
if (!is_metavar(e) || !has_meta_context(e))
return false;
meta_ctx const & ctx = metavar_ctx(e);
meta_entry const & entry = head(ctx);
if (entry.is_lift()) {
c = ::lean::mk_metavar(metavar_idx(e), tail(ctx));
add_trace(e, c);
s = entry.s();
n = entry.n();
return true;
} else {
return false;
}
}
/**
\brief Temporary hack until we build the new elaborator.
*/
bool is_inst(expr const & e, expr & c, unsigned & s, expr & v) {
if (!is_metavar(e) || !has_meta_context(e))
return false;
meta_ctx const & ctx = metavar_ctx(e);
meta_entry const & entry = head(ctx);
if (entry.is_inst()) {
c = ::lean::mk_metavar(metavar_idx(e), tail(ctx));
add_trace(e, c);
s = entry.s();
v = entry.v();
return true;
} else {
return false;
}
}
bool solve_meta(expr const & e, expr const & t, constraint const & c) {
lean_assert(has_meta_context(e));
expr const & m = e;
unsigned midx = metavar_idx(m);
unsigned i, s, n;
expr v, a, b;
if (m_metavars[midx].m_assignment) {
expr s = instantiate_metavar(e, midx, m_metavars[midx].m_assignment);
m_constraints.push_back(constraint(s, t, c));
return true;
}
if (!has_metavar(t)) {
if (is_lift(e, a, s, n)) {
if (!has_free_var(t, s, s+n)) {
m_constraints.push_back(constraint(a, lower_free_vars(t, s+n, n), c));
return true;
} else {
// display(std::cout);
throw_unification_exception(c);
}
}
}
if (has_assigned_metavar(t)) {
m_constraints.push_back(constraint(e, instantiate(t), c));
return true;
}
if (is_inst(e, a, i, v) && is_lift(a, b, s, n) && !has_free_var(t, s, s+n)) {
// subst (lift b s n) i v == t
// t does not have free-variables in the range [s, s+n)
// Thus, if t has a free variables in [s, s+n), then the only possible solution is
// (lift b s n) == i
// v == t
m_constraints.push_back(constraint(a, mk_var(i), c));
m_constraints.push_back(constraint(v, t, c));
return true;
}
return false;
}
void solve_core() {
unsigned delayed = 0;
unsigned last_num_constraints = 0;
while (!m_constraints.empty()) {
check_interrupted(m_interrupted);
constraint c = m_constraints.front();
m_constraints.pop_front();
expr const & lhs = c.m_lhs;
expr const & rhs = c.m_rhs;
// std::cout << "Solving " << lhs << " === " << rhs << "\n";
if (lhs == rhs || (!has_metavar(lhs) && !has_metavar(rhs))) {
// do nothing
delayed = 0;
} else if (is_metavar(lhs) && !has_meta_context(lhs)) {
delayed = 0;
solve_mvar(lhs, rhs, c);
} else if (is_metavar(rhs) && !has_meta_context(rhs)) {
delayed = 0;
solve_mvar(rhs, lhs, c);
} else if (is_metavar(lhs) || is_metavar(rhs)) {
if (is_metavar(lhs) && solve_meta(lhs, rhs, c)) {
delayed = 0;
} else if (is_metavar(rhs) && solve_meta(rhs, lhs, c)) {
delayed = 0;
} else {
m_constraints.push_back(c);
if (delayed == 0) {
last_num_constraints = m_constraints.size();
delayed++;
} else if (delayed > last_num_constraints) {
throw_unification_exception(c);
} else {
delayed++;
}
}
} else if (is_type(lhs) && is_type(rhs)) {
// ignoring type universe levels. We let the kernel check that
delayed = 0;
} else if (is_abstraction(lhs) && is_abstraction(rhs)) {
delayed = 0;
m_constraints.push_back(constraint(abst_domain(lhs), abst_domain(rhs), c));
m_constraints.push_back(constraint(abst_body(lhs), abst_body(rhs), extend(c.m_ctx, abst_name(lhs), abst_domain(lhs)), c));
} else if (is_eq(lhs) && is_eq(rhs)) {
delayed = 0;
m_constraints.push_back(constraint(eq_lhs(lhs), eq_lhs(rhs), c));
m_constraints.push_back(constraint(eq_rhs(lhs), eq_rhs(rhs), c));
} else {
expr new_lhs = head_reduce(lhs, m_env, c.m_ctx, m_available_defs);
expr new_rhs = head_reduce(rhs, m_env, c.m_ctx, m_available_defs);
if (!is_eqp(lhs, new_lhs) || !is_eqp(rhs, new_rhs)) {
delayed = 0;
m_constraints.push_back(constraint(new_lhs, new_rhs, c));
} else if (is_app(new_lhs) && is_app(new_rhs) && num_args(new_lhs) == num_args(new_rhs)) {
delayed = 0;
unsigned num = num_args(new_lhs);
for (unsigned i = 0; i < num; i++) {
m_constraints.push_back(constraint(arg(new_lhs, i), arg(new_rhs, i), c));
}
} else if (is_simple_ho_match(new_lhs, c.m_ctx)) {
delayed = 0;
unify_simple_ho_match(new_lhs, new_rhs, c);
} else if (is_simple_ho_match(new_rhs, c.m_ctx)) {
delayed = 0;
unify_simple_ho_match(new_rhs, new_lhs, c);
} else if (has_assigned_metavar(new_lhs)) {
delayed = 0;
m_constraints.push_back(constraint(instantiate(new_lhs), new_rhs, c));
} else if (has_assigned_metavar(new_rhs)) {
delayed = 0;
m_constraints.push_back(constraint(new_lhs, instantiate(new_rhs), c));
} else {
m_constraints.push_back(c);
if (delayed == 0) {
last_num_constraints = m_constraints.size();
delayed++;
} else if (delayed > last_num_constraints) {
throw_unification_exception(c);
} else {
delayed++;
}
}
}
}
}
struct found_assigned {};
bool has_assigned_metavar(expr const & e) {
auto proc = [&](expr const & n, unsigned) {
if (is_metavar(n)) {
unsigned midx = metavar_idx(n);
if (m_metavars[midx].m_assignment)
throw found_assigned();
}
};
for_each_fn<decltype(proc)> visitor(proc);
try {
visitor(e);
return false;
} catch (found_assigned&) {
return true;
}
}
expr instantiate(expr const & e) {
auto proc = [&](expr const & n, unsigned) -> expr {
if (is_metavar(n)) {
expr const & m = n;
unsigned midx = metavar_idx(m);
if (m_metavars[midx].m_assignment) {
if (has_assigned_metavar(m_metavars[midx].m_assignment)) {
m_metavars[midx].m_assignment = instantiate(m_metavars[midx].m_assignment);
}
return instantiate_metavar(n, midx, m_metavars[midx].m_assignment);
}
}
return n;
};
auto tracer = [&](expr const & old_e, expr const & new_e) {
add_trace(old_e, new_e);
};
replace_fn<decltype(proc), decltype(tracer)> replacer(proc, tracer);
return replacer(e);
}
void solve() {
unsigned num_meta = m_metavars.size();
m_processing_root = false;
while (true) {
solve_core();
bool cont = false;
bool progress = false;
// unsigned unsolved_midx = 0;
for (unsigned midx = 0; midx < num_meta; midx++) {
if (m_metavars[midx].m_assignment) {
if (has_assigned_metavar(m_metavars[midx].m_assignment)) {
m_metavars[midx].m_assignment = instantiate(m_metavars[midx].m_assignment);
}
if (has_metavar(m_metavars[midx].m_assignment)) {
// unsolved_midx = midx;
cont = true; // must continue
} else {
if (m_metavars[midx].m_type && !m_metavars[midx].m_type_cnstr) {
context ctx = m_metavars[midx].m_ctx;
try {
expr t = infer(m_metavars[midx].m_assignment, ctx);
m_metavars[midx].m_type_cnstr = true;
info_ref r = mk_expected_type_info(m_metavars[midx].m_mvar, m_metavars[midx].m_assignment,
m_metavars[midx].m_type, t, ctx);
m_constraints.push_back(constraint(m_metavars[midx].m_type, t, ctx, r));
progress = true;
} catch (exception&) {
// std::cout << "Failed to infer type of: ?M" << midx << "\n"
// << m_metavars[midx].m_assignment << "\nAT\n" << m_metavars[midx].m_ctx << "\n";
expr null_given_type; // failed to infer given type.
throw unification_type_mismatch_exception(*m_owner, ctx, m_metavars[midx].m_mvar, m_metavars[midx].m_assignment,
instantiate(m_metavars[midx].m_type), null_given_type);
}
}
}
} else {
cont = true;
}
}
if (!cont)
return;
if (!progress)
return;
}
}
public:
imp(frontend const & fe, name_set const * defs):
m_frontend(fe),
m_env(fe.get_environment()),
m_available_defs(defs),
m_normalizer(m_env) {
m_interrupted = false;
m_owner = nullptr;
}
void clear() {
m_trace.clear();
m_normalizer.clear();
}
void set_interrupt(bool flag) {
m_interrupted = flag;
m_normalizer.set_interrupt(flag);
}
void display(std::ostream & out) {
for (unsigned i = 0; i < m_metavars.size(); i++) {
out << "#" << i << " ";
auto m = m_metavars[i];
if (m.m_assignment)
out << m.m_assignment;
else
out << "[unassigned]";
if (m.m_type)
out << ", type: " << m.m_type;
out << "\n";
}
for (auto c : m_constraints) {
out << c.m_lhs << " === " << c.m_rhs << "\n";
}
}
environment const & get_environment() const {
return m_env;
}
expr operator()(expr const & e, expr const & expected_type, elaborator const & elb) {
m_owner = &elb;
m_constraints.clear();
m_metavars.clear();
m_app_mismatch_info.clear();
m_expected_type_info.clear();
m_processing_root = true;
auto p = process(e, context());
m_root = p.first;
expr given_type = p.second;
if (expected_type) {
if (has_metavar(given_type)) {
info_ref r = mk_expected_type_info(e, m_root, expected_type, given_type, context());
m_constraints.push_back(constraint(expected_type, given_type, context(), r));
}
}
if (has_metavar(m_root)) {
solve();
expr r = instantiate(m_root);
if (has_metavar(r))
throw unsolved_placeholder_exception(elb, context(), m_root);
return r;
} else {
return m_root;
}
}
expr const & get_original(expr const & e) const {
expr const * r = &e;
while (true) {
auto it = m_trace.find(*r);
if (it == m_trace.end()) {
return *r;
} else {
r = &(it->second);
}
}
}
format pp(formatter & f, options const & o) const {
bool unicode = get_pp_unicode(o);
format r;
bool first = true;
for (auto c : m_constraints) {
if (first) first = false; else r += line();
r += group(format{f(c.m_lhs, o), space(), unicode ? g_unification_u_fmt : g_unification_fmt, line(), f(c.m_rhs, o)});
}
return r;
}
bool has_constraints() const { return !m_constraints.empty(); }
};
elaborator::elaborator(frontend const & fe):m_ptr(new imp(fe, nullptr)) {}
elaborator::~elaborator() {} elaborator::~elaborator() {}
expr elaborator::operator()(expr const & e) { return (*m_ptr)(e, expr(), *this); } expr elaborator::operator()(expr const & e) { return e; }
expr elaborator::operator()(expr const & e, expr const & expected_type) { return (*m_ptr)(e, expected_type, *this); } expr elaborator::operator()(expr const & e, expr const & /* expected_type */) { return e; }
expr const & elaborator::get_original(expr const & e) const { return m_ptr->get_original(e); } expr const & elaborator::get_original(expr const & e) const { return e; }
void elaborator::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); } void elaborator::set_interrupt(bool ) {}
void elaborator::clear() { m_ptr->clear(); } void elaborator::clear() {}
environment const & elaborator::get_environment() const { return m_ptr->get_environment(); } environment g_env;
void elaborator::display(std::ostream & out) const { m_ptr->display(out); } environment const & elaborator::get_environment() const { return g_env; }
format elaborator::pp(formatter & f, options const & o) const { return m_ptr->pp(f, o); } void elaborator::display(std::ostream & ) const {}
void elaborator::print(imp * ptr) { ptr->display(std::cout); } format elaborator::pp(formatter &, options const &) const { return format(); }
bool elaborator::has_constraints() const { return m_ptr->has_constraints(); } void elaborator::print(imp * ptr) { lean_assert(ptr); }
bool elaborator::has_constraints() const { return false; }
} }

8
src/frontends/lean/pp.cpp
View file

@ -201,7 +201,7 @@ class pp_fn {
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Value: case expr_kind::Type: case expr_kind::Var: case expr_kind::Constant: case expr_kind::Value: case expr_kind::Type:
return true; return true;
case expr_kind::MetaVar: case expr_kind::MetaVar:
return !metavar_ctx(e); return !metavar_lctx(e);
case expr_kind::App: case expr_kind::App:
if (!m_coercion && is_coercion(e)) if (!m_coercion && is_coercion(e))
return is_atomic(arg(e, 1)); return is_atomic(arg(e, 1));
@ -1022,12 +1022,12 @@ class pp_fn {
} }
result pp_metavar(expr const & a, unsigned depth) { result pp_metavar(expr const & a, unsigned depth) {
format mv_fmt = compose(format("?M"), format(metavar_idx(a))); format mv_fmt = compose(format("?M"), format(metavar_name(a)));
if (metavar_ctx(a)) { if (metavar_lctx(a)) {
format ctx_fmt; format ctx_fmt;
bool first = true; bool first = true;
unsigned r_weight = 1; unsigned r_weight = 1;
for (meta_entry const & e : metavar_ctx(a)) { for (local_entry const & e : metavar_lctx(a)) {
format e_fmt; format e_fmt;
if (e.is_lift()) { if (e.is_lift()) {
e_fmt = format{g_lift_fmt, colon(), format(e.s()), colon(), format(e.n())}; e_fmt = format{g_lift_fmt, colon(), format(e.s()), colon(), format(e.n())};

34
src/kernel/expr.cpp
View file

@ -11,11 +11,20 @@ Author: Leonardo de Moura
#include "kernel/expr.h" #include "kernel/expr.h"
#include "kernel/free_vars.h" #include "kernel/free_vars.h"
#include "kernel/expr_eq.h" #include "kernel/expr_eq.h"
#include "kernel/metavar.h"
namespace lean { namespace lean {
meta_entry::meta_entry(unsigned s, unsigned n):m_kind(meta_entry_kind::Lift), m_s(s), m_n(n) {} local_entry::local_entry(unsigned s, unsigned n):m_kind(local_entry_kind::Lift), m_s(s), m_n(n) {}
meta_entry::meta_entry(unsigned s, expr const & v):m_kind(meta_entry_kind::Inst), m_s(s), m_v(v) {} local_entry::local_entry(unsigned s, expr const & v):m_kind(local_entry_kind::Inst), m_s(s), m_v(v) {}
meta_entry::~meta_entry() {} local_entry::~local_entry() {}
bool local_entry::operator==(local_entry const & e) const {
if (m_kind != e.m_kind || m_s != e.m_s)
return false;
if (is_inst())
return m_v == e.m_v;
else
return m_n == e.m_n;
}
unsigned hash_args(unsigned size, expr const * args) { unsigned hash_args(unsigned size, expr const * args) {
return hash(size, [&args](unsigned i){ return args[i].hash(); }); return hash(size, [&args](unsigned i){ return args[i].hash(); });
@ -128,10 +137,21 @@ expr_value::expr_value(value & v):
expr_value::~expr_value() { expr_value::~expr_value() {
m_val.dec_ref(); m_val.dec_ref();
} }
expr_metavar::expr_metavar(unsigned i, meta_ctx const & c): expr_metavar::expr_metavar(name const & n, expr const & t, local_context const & lctx):
expr_cell(expr_kind::MetaVar, i, true), expr_cell(expr_kind::MetaVar, n.hash(), true),
m_midx(i), m_ctx(c) {} m_name(n), m_type(t), m_lctx(lctx) {}
expr_metavar::~expr_metavar() {} expr_metavar::~expr_metavar() {}
expr expr_metavar::get_type() const {
if (m_type && get_lctx()) {
if (is_metavar(m_type)) {
return update_metavar(m_type, append(get_lctx(), metavar_lctx(m_type)));
} else {
return apply_local_context(m_type, get_lctx());
}
} else {
return m_type;
}
}
void expr_cell::dealloc() { void expr_cell::dealloc() {
switch (kind()) { switch (kind()) {
@ -172,7 +192,7 @@ expr copy(expr const & a) {
case expr_kind::Lambda: return mk_lambda(abst_name(a), abst_domain(a), abst_body(a)); case expr_kind::Lambda: return mk_lambda(abst_name(a), abst_domain(a), abst_body(a));
case expr_kind::Pi: return mk_pi(abst_name(a), abst_domain(a), abst_body(a)); case expr_kind::Pi: return mk_pi(abst_name(a), abst_domain(a), abst_body(a));
case expr_kind::Let: return mk_let(let_name(a), let_type(a), let_value(a), let_body(a)); case expr_kind::Let: return mk_let(let_name(a), let_type(a), let_value(a), let_body(a));
case expr_kind::MetaVar: return mk_metavar(metavar_idx(a), metavar_ctx(a)); case expr_kind::MetaVar: return mk_metavar(metavar_name(a), metavar_raw_type(a), metavar_lctx(a));
} }
lean_unreachable(); lean_unreachable();
} }

110
src/kernel/expr.h
View file

@ -31,12 +31,12 @@ class value;
| Type universe | Type universe
| Eq expr expr (heterogeneous equality) | Eq expr expr (heterogeneous equality)
| Let name expr expr expr | Let name expr expr expr
| Metavar idx meta_ctx | Metavar name expr? local_context (the expression is the type of the metavariable)
meta_ctx ::= [meta_entry] local_context ::= [local_entry]
meta_entry ::= lift idx idx local_entry ::= lift idx idx
| inst idx expr | inst idx expr
TODO(Leo): match expressions. TODO(Leo): match expressions.
@ -47,12 +47,12 @@ The main API is divided in the following sections
- Miscellaneous - Miscellaneous
======================================= */ ======================================= */
enum class expr_kind { Var, Constant, Value, App, Lambda, Pi, Type, Eq, Let, MetaVar }; enum class expr_kind { Var, Constant, Value, App, Lambda, Pi, Type, Eq, Let, MetaVar };
class meta_entry; class local_entry;
/** /**
\brief A metavariable context is just a list of meta_entries. \brief A metavariable local context is just a list of local_entries.
\see meta_entry \see local_entry
*/ */
typedef list<meta_entry> meta_ctx; typedef list<local_entry> local_context;
/** /**
\brief Base class used to represent expressions. \brief Base class used to represent expressions.
@ -121,7 +121,7 @@ public:
friend expr mk_pi(name const & n, expr const & t, expr const & e); friend expr mk_pi(name const & n, expr const & t, expr const & e);
friend expr mk_type(level const & l); friend expr mk_type(level const & l);
friend expr mk_let(name const & n, expr const & t, expr const & v, expr const & e); friend expr mk_let(name const & n, expr const & t, expr const & v, expr const & e);
friend expr mk_metavar(unsigned idx, meta_ctx const & ctx); friend expr mk_metavar(name const & n, expr const & t, local_context const & ctx);
friend bool is_eqp(expr const & a, expr const & b) { return a.m_ptr == b.m_ptr; } friend bool is_eqp(expr const & a, expr const & b) { return a.m_ptr == b.m_ptr; }
@ -254,9 +254,9 @@ public:
value const & get_value() const { return m_val; } value const & get_value() const { return m_val; }
}; };
/** /**
\see meta_entry \see local_entry
*/ */
enum class meta_entry_kind { Lift, Inst }; enum class local_entry_kind { Lift, Inst };
/** /**
\brief An entry in a metavariable context. \brief An entry in a metavariable context.
It represents objects of the form: It represents objects of the form:
@ -288,36 +288,42 @@ enum class meta_entry_kind { Lift, Inst };
f a (g #3) f a (g #3)
</code> </code>
*/ */
class meta_entry { class local_entry {
meta_entry_kind m_kind; local_entry_kind m_kind;
unsigned m_s; unsigned m_s;
unsigned m_n; unsigned m_n;
expr m_v; expr m_v;
meta_entry(unsigned s, unsigned n); local_entry(unsigned s, unsigned n);
meta_entry(unsigned s, expr const & v); local_entry(unsigned s, expr const & v);
public: public:
~meta_entry(); ~local_entry();
friend meta_entry mk_lift(unsigned s, unsigned n); friend local_entry mk_lift(unsigned s, unsigned n);
friend meta_entry mk_inst(unsigned s, expr const & v); friend local_entry mk_inst(unsigned s, expr const & v);
meta_entry_kind kind() const { return m_kind; } local_entry_kind kind() const { return m_kind; }
bool is_inst() const { return kind() == meta_entry_kind::Inst; } bool is_inst() const { return kind() == local_entry_kind::Inst; }
bool is_lift() const { return kind() == meta_entry_kind::Lift; } bool is_lift() const { return kind() == local_entry_kind::Lift; }
unsigned s() const { return m_s; } unsigned s() const { return m_s; }
unsigned n() const { lean_assert(is_lift()); return m_n; } unsigned n() const { lean_assert(is_lift()); return m_n; }
bool operator==(local_entry const & e) const;
bool operator!=(local_entry const & e) const { return !operator==(e); }
expr const & v() const { lean_assert(is_inst()); return m_v; } expr const & v() const { lean_assert(is_inst()); return m_v; }
}; };
inline meta_entry mk_lift(unsigned s, unsigned n) { return meta_entry(s, n); } inline local_entry mk_lift(unsigned s, unsigned n) { return local_entry(s, n); }
inline meta_entry mk_inst(unsigned s, expr const & v) { return meta_entry(s, v); } inline local_entry mk_inst(unsigned s, expr const & v) { return local_entry(s, v); }
/** \brief Metavariables */ /** \brief Metavariables */
class expr_metavar : public expr_cell { class expr_metavar : public expr_cell {
unsigned m_midx; name m_name;
meta_ctx m_ctx; expr m_type;
local_context m_lctx;
public: public:
expr_metavar(unsigned i, meta_ctx const & c); expr_metavar(name const & n, expr const & t, local_context const & lctx);
~expr_metavar(); ~expr_metavar();
unsigned get_midx() const { return m_midx; } name const & get_name() const { return m_name; }
meta_ctx const & get_ctx() const { return m_ctx; } expr const & get_raw_type() const { return m_type; }
/* \brief Return the type of the metavariable modulo the associated local context */
expr get_type() const;
local_context const & get_lctx() const { return m_lctx; }
}; };
// ======================================= // =======================================
@ -374,7 +380,9 @@ inline expr mk_type(level const & l) { return expr(new expr_type(l)); }
expr mk_type(); expr mk_type();
inline expr Type(level const & l) { return mk_type(l); } inline expr Type(level const & l) { return mk_type(l); }
inline expr Type() { return mk_type(); } inline expr Type() { return mk_type(); }
inline expr mk_metavar(unsigned idx, meta_ctx const & ctx = meta_ctx()) { return expr(new expr_metavar(idx, ctx)); } inline expr mk_metavar(name const & n, expr const & t = expr(), local_context const & ctx = local_context()) {
return expr(new expr_metavar(n, t, ctx));
}
inline expr expr::operator()(expr const & a1) const { return mk_app({*this, a1}); } inline expr expr::operator()(expr const & a1) const { return mk_app({*this, a1}); }
inline expr expr::operator()(expr const & a1, expr const & a2) const { return mk_app({*this, a1, a2}); } inline expr expr::operator()(expr const & a1, expr const & a2) const { return mk_app({*this, a1, a2}); }
@ -432,8 +440,10 @@ inline name const & let_name(expr_cell * e) { return to_let(e)->get
inline expr const & let_value(expr_cell * e) { return to_let(e)->get_value(); } inline expr const & let_value(expr_cell * e) { return to_let(e)->get_value(); }
inline expr const & let_type(expr_cell * e) { return to_let(e)->get_type(); } inline expr const & let_type(expr_cell * e) { return to_let(e)->get_type(); }
inline expr const & let_body(expr_cell * e) { return to_let(e)->get_body(); } inline expr const & let_body(expr_cell * e) { return to_let(e)->get_body(); }
inline unsigned metavar_idx(expr_cell * e) { return to_metavar(e)->get_midx(); } inline name const & metavar_name(expr_cell * e) { return to_metavar(e)->get_name(); }
inline meta_ctx const & metavar_ctx(expr_cell * e) { return to_metavar(e)->get_ctx(); } inline expr const & metavar_raw_type(expr_cell * e) { return to_metavar(e)->get_raw_type(); }
inline expr metavar_type(expr_cell * e) { return to_metavar(e)->get_type(); }
inline local_context const & metavar_lctx(expr_cell * e) { return to_metavar(e)->get_lctx(); }
/** \brief Return the reference counter of the given expression. */ /** \brief Return the reference counter of the given expression. */
inline unsigned get_rc(expr const & e) { return e.raw()->get_rc(); } inline unsigned get_rc(expr const & e) { return e.raw()->get_rc(); }
@ -463,8 +473,10 @@ inline name const & let_name(expr const & e) { return to_let(e)->ge
inline expr const & let_type(expr const & e) { return to_let(e)->get_type(); } inline expr const & let_type(expr const & e) { return to_let(e)->get_type(); }
inline expr const & let_value(expr const & e) { return to_let(e)->get_value(); } inline expr const & let_value(expr const & e) { return to_let(e)->get_value(); }
inline expr const & let_body(expr const & e) { return to_let(e)->get_body(); } inline expr const & let_body(expr const & e) { return to_let(e)->get_body(); }
inline unsigned metavar_idx(expr const & e) { return to_metavar(e)->get_midx(); } inline name const & metavar_name(expr const & e) { return to_metavar(e)->get_name(); }
inline meta_ctx const & metavar_ctx(expr const & e) { return to_metavar(e)->get_ctx(); } inline expr const & metavar_raw_type(expr const & e) { return to_metavar(e)->get_raw_type(); }
inline expr metavar_type(expr const & e) { return to_metavar(e)->get_type(); }
inline local_context const & metavar_lctx(expr const & e) { return to_metavar(e)->get_lctx(); }
inline bool has_metavar(expr const & e) { return e.has_metavar(); } inline bool has_metavar(expr const & e) { return e.has_metavar(); }
// ======================================= // =======================================
@ -582,14 +594,11 @@ template<typename F> expr update_eq(expr const & e, F f) {
else else
return e; return e;
} }
template<typename F> expr update_metavar(expr const & e, unsigned i, F f) { template<typename F> expr update_metavar(expr const & e, name const & n, expr const & t, F f) {
static_assert(std::is_same<typename std::result_of<F(meta_entry const &)>::type, buffer<local_entry> new_entries;
meta_entry>::value, bool modified = (n != metavar_name(e) || t != metavar_raw_type(e));
"update_metavar: return type of f(meta_entry) is not meta_entry"); for (local_entry const & me : metavar_lctx(e)) {
buffer<meta_entry> new_entries; local_entry new_me = f(me);
bool modified = (i != metavar_idx(e));
for (meta_entry const & me : metavar_ctx(e)) {
meta_entry new_me = f(me);
if (new_me.kind() != me.kind() || new_me.s() != me.s()) { if (new_me.kind() != me.kind() || new_me.s() != me.s()) {
modified = true; modified = true;
} else if (new_me.is_inst()) { } else if (new_me.is_inst()) {
@ -601,15 +610,18 @@ template<typename F> expr update_metavar(expr const & e, unsigned i, F f) {
new_entries.push_back(new_me); new_entries.push_back(new_me);
} }
if (modified) if (modified)
return mk_metavar(i, to_list(new_entries.begin(), new_entries.end())); return mk_metavar(n, t, to_list(new_entries.begin(), new_entries.end()));
else else
return e; return e;
} }
template<typename F> expr update_metavar(expr const & e, F f) { template<typename F> expr update_metavar(expr const & e, F f) {
static_assert(std::is_same<typename std::result_of<F(meta_entry const &)>::type, return update_metavar(e, metavar_name(e), metavar_raw_type(e), f);
meta_entry>::value, }
"update_metavar: return type of f(meta_entry) is not meta_entry"); inline expr update_metavar(expr const & e, local_context const & lctx) {
return update_metavar(e, metavar_idx(e), f); if (metavar_lctx(e) != lctx)
return mk_metavar(metavar_name(e), metavar_raw_type(e), lctx);
else
return e;
} }
// ======================================= // =======================================

6
src/kernel/expr_eq.h
View file

@ -58,8 +58,10 @@ class expr_eq_fn {
case expr_kind::Value: return to_value(a) == to_value(b); case expr_kind::Value: return to_value(a) == to_value(b);
case expr_kind::Let: return apply(let_type(a), let_type(b)) && apply(let_value(a), let_value(b)) && apply(let_body(a), let_body(b)); case expr_kind::Let: return apply(let_type(a), let_type(b)) && apply(let_value(a), let_value(b)) && apply(let_body(a), let_body(b));
case expr_kind::MetaVar: case expr_kind::MetaVar:
return metavar_idx(a) == metavar_idx(b) && return
compare(metavar_ctx(a), metavar_ctx(b), [&](meta_entry const & e1, meta_entry const & e2) { metavar_name(a) == metavar_name(b) &&
metavar_raw_type(a) == metavar_raw_type(b) &&
compare(metavar_lctx(a), metavar_lctx(b), [&](local_entry const & e1, local_entry const & e2) {
if (e1.kind() != e2.kind() || e1.s() != e2.s()) if (e1.kind() != e2.kind() || e1.s() != e2.s())
return false; return false;
if (e1.is_inst()) if (e1.is_inst())

275
src/kernel/metavar.cpp
View file

@ -14,7 +14,7 @@ Author: Leonardo de Moura
#include "kernel/for_each.h" #include "kernel/for_each.h"
namespace lean { namespace lean {
void metavar_env::inc_timestamp() { void substitution::inc_timestamp() {
if (m_timestamp == std::numeric_limits<unsigned>::max()) { if (m_timestamp == std::numeric_limits<unsigned>::max()) {
// This should not happen in real examples. We add it just to be safe. // This should not happen in real examples. We add it just to be safe.
throw exception("metavar_env timestamp overflow"); throw exception("metavar_env timestamp overflow");
@ -22,117 +22,100 @@ void metavar_env::inc_timestamp() {
m_timestamp++; m_timestamp++;
} }
metavar_env::metavar_env():m_timestamp(0) {} substitution::substitution():
m_size(0),
m_timestamp(0) {
}
expr metavar_env::mk_metavar(expr const & type, context const & ctx) { bool substitution::operator==(substitution const & s) const {
if (size() != s.size())
return false;
// TODO(Leo)
return true;
}
bool substitution::is_assigned(name const & m) const {
return const_cast<substitution*>(this)->m_subst.splay_find(m);
}
bool substitution::is_assigned(expr const & m) const {
return is_assigned(metavar_name(m));
}
void substitution::assign(name const & m, expr const & t) {
lean_assert(!is_assigned(m));
m_subst.insert(m, t);
inc_timestamp(); inc_timestamp();
unsigned midx = m_env.size(); m_size++;
m_env.push_back(data(type, ctx));
return ::lean::mk_metavar(midx);
} }
expr metavar_env::mk_metavar(context const & ctx) { void substitution::assign(expr const & m, expr const & t) {
return mk_metavar(expr(), ctx); lean_assert(is_metavar(m));
lean_assert(!has_local_context(m));
assign(metavar_name(m), t);
} }
bool metavar_env::contains(unsigned midx) const { expr apply_local_context(expr const & a, local_context const & lctx) {
return midx < m_env.size(); if (lctx) {
} expr r = apply_local_context(a, tail(lctx));
local_entry const & e = head(lctx);
bool metavar_env::is_assigned(unsigned midx) const {
return m_env[midx].m_subst;
}
expr metavar_env::get_subst_core(unsigned midx) const {
return m_env[midx].m_subst;
}
expr metavar_env::get_subst(unsigned midx) const {
expr r = m_env[midx].m_subst;
if (r && has_assigned_metavar(r, *this)) {
r = instantiate_metavars(r, *this);
expr t = m_env[midx].m_type;
context ctx = m_env[midx].m_ctx;
const_cast<metavar_env*>(this)->m_env[midx] = data(r, t, ctx);
return r;
} else {
return r;
}
}
expr metavar_env::get_type(unsigned midx, unification_problems & up) {
data d = m_env[midx];
expr t = d.m_type;
if (t) {
return t;
} else {
t = mk_metavar();
expr s = d.m_subst;
m_env[midx] = data(s, t, d.m_ctx);
if (s)
up.add_type_of_eq(d.m_ctx, s, t);
else
up.add_type_of_eq(d.m_ctx, ::lean::mk_metavar(midx), t);
return t;
}
}
expr metavar_env::get_type(unsigned midx) const {
return m_env[midx].m_type;
}
void metavar_env::assign(unsigned midx, expr const & v) {
inc_timestamp();
lean_assert(!is_assigned(midx));
data const & d = m_env[midx];
m_env[midx] = data(v, d.m_type, d.m_ctx);
}
context const & metavar_env::get_context(unsigned midx) const {
return m_env[midx].m_ctx;
}
expr instantiate(expr const & s, meta_ctx const & ctx, metavar_env const & env) {
if (ctx) {
expr r = instantiate(s, tail(ctx), env);
meta_entry const & e = head(ctx);
if (e.is_lift()) { if (e.is_lift()) {
return lift_free_vars(r, e.s(), e.n()); return lift_free_vars(r, e.s(), e.n());
} else { } else {
lean_assert(e.is_inst()); lean_assert(e.is_inst());
return ::lean::instantiate(r, e.s(), instantiate_metavars(e.v(), env)); return instantiate(r, e.s(), e.v());
} }
} else { } else {
return s; return a;
} }
} }
expr metavar_env::get_subst(expr const & m) const { expr substitution::get_subst(expr const & m) const {
expr s = get_subst(metavar_idx(m)); lean_assert(is_metavar(m));
if (s) name2expr::entry const * e = const_cast<substitution*>(this)->m_subst.splay_find(metavar_name(m));
return instantiate(s, metavar_ctx(m), *this); if (e) {
else expr r = e->second;
return s; if (has_assigned_metavar(r, *this)) {
r = instantiate_metavars(r, *this);
const_cast<substitution*>(this)->m_subst.insert(metavar_name(m), r);
}
local_context const & lctx = metavar_lctx(m);
if (lctx) {
r = apply_local_context(r, lctx);
if (has_assigned_metavar(r, *this))
r = instantiate_metavars(r, *this);
}
return r;
} else {
return expr();
}
} }
expr metavar_env::get_type(expr const & m, unification_problems & up) { static name g_unique_name = name::mk_internal_unique_name();
expr s = get_type(metavar_idx(m), up);
return instantiate(s, metavar_ctx(m), *this); metavar_generator::metavar_generator(name const & prefix):
m_gen(prefix) {
} }
void metavar_env::assign(expr const & m, expr const & t) { metavar_generator::metavar_generator():
lean_assert(!metavar_ctx(m)); m_gen(g_unique_name) {
assign(metavar_idx(m), t);
} }
expr instantiate_metavars(expr const & e, metavar_env const & env) { expr metavar_generator::mk(expr const & t) {
return mk_metavar(m_gen.next(), t, local_context());
}
expr metavar_generator::mk() {
return mk(mk(expr()));
}
expr instantiate_metavars(expr const & e, substitution const & s) {
if (!has_metavar(e)) { if (!has_metavar(e)) {
return e; return e;
} else { } else {
auto f = [=](expr const & m, unsigned) -> expr { auto f = [=](expr const & m, unsigned) -> expr {
if (is_metavar(m) && env.contains(m)) { if (is_metavar(m) && s.is_assigned(m)) {
expr s = env.get_subst(m); return s.get_subst(m);
return s ? s : m;
} else { } else {
return m; return m;
} }
@ -141,62 +124,13 @@ expr instantiate_metavars(expr const & e, metavar_env const & env) {
} }
} }
meta_ctx add_lift(meta_ctx const & ctx, unsigned s, unsigned n) {
if (n == 0) {
return ctx;
} else if (ctx) {
meta_entry e = head(ctx);
// Simplification rule
// lift:(s1+n1):n2 lift:s1:n1 ---> lift:s1:n1+n2
if (e.is_lift() && s == e.s() + e.n()) {
return add_lift(tail(ctx), e.s(), e.n() + n);
}
}
return cons(mk_lift(s, n), ctx);
}
expr add_lift(expr const & m, unsigned s, unsigned n) {
return mk_metavar(metavar_idx(m), add_lift(metavar_ctx(m), s, n));
}
meta_ctx add_inst(meta_ctx const & ctx, unsigned s, expr const & v) {
if (ctx) {
meta_entry e = head(ctx);
if (e.is_lift() && e.s() <= s && s < e.s() + e.n()) {
return add_lift(tail(ctx), 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(ctx), e.s() - 1, e.n() - 1);
}
}
return cons(mk_inst(s, v), ctx);
}
expr add_inst(expr const & m, unsigned s, expr const & v) {
return mk_metavar(metavar_idx(m), add_inst(metavar_ctx(m), s, v));
}
bool has_meta_context(expr const & m) {
return metavar_ctx(m);
}
expr pop_meta_context(expr const & m) {
lean_assert(has_meta_context(m));
return mk_metavar(metavar_idx(m), tail(metavar_ctx(m)));
}
struct found_assigned {}; struct found_assigned {};
bool has_assigned_metavar(expr const & e, metavar_env const & menv) { bool has_assigned_metavar(expr const & e, substitution const & s) {
if (!has_metavar(e)) { if (!has_metavar(e)) {
return false; return false;
} else { } else {
auto proc = [&](expr const & n, unsigned) { auto proc = [&](expr const & n, unsigned) {
if (is_metavar(n) && menv.contains(n) && menv.is_assigned(n)) if (is_metavar(n) && s.is_assigned(n))
throw found_assigned(); throw found_assigned();
}; };
for_each_fn<decltype(proc)> visitor(proc); for_each_fn<decltype(proc)> visitor(proc);
@ -209,21 +143,70 @@ bool has_assigned_metavar(expr const & e, metavar_env const & menv) {
} }
} }
local_context add_lift(local_context const & lctx, unsigned s, unsigned n) {
if (n == 0) {
return lctx;
} else if (lctx) {
local_entry e = head(lctx);
// Simplification rule
// lift:(s1+n1):n2 lift:s1:n1 ---> lift:s1:n1+n2
if (e.is_lift() && 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) {
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) {
return update_metavar(m, add_inst(metavar_lctx(m), s, v));
}
bool has_local_context(expr const & m) {
return metavar_lctx(m);
}
expr pop_meta_context(expr const & m) {
lean_assert(has_local_context(m));
return update_metavar(m, tail(metavar_lctx(m)));
}
/** /**
\brief Auxiliary exception used to sign that a metavariable was \brief Auxiliary exception used to sign that a metavariable was
found in an expression. found in an expression.
*/ */
struct found_metavar {}; struct found_metavar {};
bool has_metavar(expr const & e, unsigned midx, metavar_env const & menv) { bool has_metavar(expr const & e, expr const & m, substitution const & s) {
auto f = [&](expr const & m, unsigned) { lean_assert(is_metavar(m));
if (is_metavar(m)) { lean_assert(!s.is_assigned(m));
unsigned midx2 = metavar_idx(m); auto f = [&](expr const & m2, unsigned) {
if (midx2 == midx) if (is_metavar(m2)) {
if (metavar_name(m) == metavar_name(m2))
throw found_metavar(); throw found_metavar();
if (menv.contains(midx2) && if (s.is_assigned(m2) &&
menv.is_assigned(midx2) && has_metavar(s.get_subst(m2), m, s))
has_metavar(menv.get_subst(midx2), midx, menv))
throw found_metavar(); throw found_metavar();
} }
}; };

264
src/kernel/metavar.h
View file

@ -6,186 +6,131 @@ Author: Leonardo de Moura
*/ */
#pragma once #pragma once
#include "util/pair.h" #include "util/pair.h"
#include "util/pvector.h" #include "util/splay_map.h"
#include "util/name_generator.h"
#include "kernel/expr.h" #include "kernel/expr.h"
#include "kernel/context.h" #include "kernel/context.h"
namespace lean { namespace lean {
/** /**
\brief Set of unification problems that need to be solved. \brief Metavariable substitution. It is essentially a mapping from
It store two kinds of problems: metavariables to expressions.
1. <tt>ctx |- lhs == rhs</tt>
2. <tt>ctx |- typeof(n) == t</tt>
3. <tt>ctx |- t1 is_convertible_to t2</tt>
*/ */
class unification_problems { class substitution {
public: typedef splay_map<name, expr, name_cmp> name2expr;
virtual ~unification_problems() {} name2expr m_subst;
/** unsigned m_size;
\brief Add a new unification problem of the form <tt>ctx |- lhs == rhs</tt> unsigned m_timestamp;
*/
virtual void add_eq(context const & ctx, expr const & lhs, expr const & rhs) = 0;
/**
\brief Add a new unification problem of the form <tt>ctx |- typeof(n) == t</tt>
*/
virtual void add_type_of_eq(context const & ctx, expr const & n, expr const & t) = 0;
/**
\brief Add a new problem of the form <tt>ctx |- t1 is_convertible_to t2</tt>
\remark <tt>ctx |- t1 == t2</tt> implies <tt>ctx |- t1 is_convertible_to t2</tt>
*/
virtual void add_is_convertible(context const & ctx, expr const & t1, expr const & t2) = 0;
};
/**
\brief Metavariable environment. It is essentially a mapping
from metavariables to assignments and types.
*/
class metavar_env {
struct data {
expr m_subst;
expr m_type;
context m_ctx;
data(expr const & t, context const & ctx):m_type(t), m_ctx(ctx) {}
data(expr const & s, expr const & t, context const & ctx):m_subst(s), m_type(t), m_ctx(ctx) {}
};
pvector<data> m_env;
unsigned m_timestamp;
void inc_timestamp(); void inc_timestamp();
public: public:
metavar_env(); substitution();
/** /**
\brief The timestamp is increased whenever the environment is updated by \brief The timestamp is increased whenever the substitution is updated by
\c mk_metavar or \c assign. \c mk_metavar or \c assign.
*/ */
unsigned get_timestamp() const { return m_timestamp; } unsigned get_timestamp() const { return m_timestamp; }
/** /**
\brief Return the number of metavariables in this metavar_env. \brief Return the number of assigned metavariables in this substitution.
*/ */
unsigned size() const { return m_env.size(); } unsigned size() const { return m_size; }
/** /**
\brief Create new metavariable in this environment. \brief Return true iff the metavariable named \c m is assigned in this substitution.
*/ */
expr mk_metavar(context const & ctx = context()); bool is_assigned(name const & m) const;
/** /**
\brief Create a new metavariable with the given type and context. \brief Return true if the given metavariable is assigned in this
*/ substitution.
expr mk_metavar(expr const & type, context const & ctx = context());
/**
\brief Return true if this environment contains a metavariable
with id \c midx. That is, it has an entry of the form
<tt>midx -> (s, t)</tt>.
*/
bool contains(unsigned midx) const;
/**
\brief Return true if the metavariable with id \c midx is assigned in
this environment.
\pre contains(midx)
*/
bool is_assigned(unsigned midx) const;
/**
\brief Return the substitution associated with the metavariable with id \c midx
in this environment.
If the metavariable is not assigned in this environment, then it returns the null
expression.
\pre contains(midx)
*/
expr get_subst(unsigned midx) const;
expr get_subst_core(unsigned midx) const;
/**
\brief Return the type of the metavariable with id \c midx in this environment.
\remark A new metavariable may be created to represent the type of the input
metavariable. When this happens, a new unification problem of the form
<tt>typeof(m) = t</tt> is added to \c up, where \c m is the metavariable
with id \c midx, and \c t is the result of this method.
\pre contains(midx)
*/
expr get_type(unsigned midx, unification_problems & up);
/**
\brief Return type of the metavariable with id \c midx in this environment.
If the metavariable is not associated with any type, then return the null expression.
*/
expr get_type(unsigned midx) const;
/**
\brief Assign the metavariable with id \c midx to the term \c t.
\pre !is_assigned(midx)
*/
void assign(unsigned midx, expr const & t);
/**
\brief Return the context associated with a metavariable.
*/
context const & get_context(unsigned midx) const;
/**
\brief Return true if this environment contains the given metavariable
\pre is_metavar(m) \pre is_metavar(m)
*/ */
bool contains(expr const & m) const { return contains(metavar_idx(m)); } bool is_assigned(expr const & m) const;
/** /**
\pre contains(m) \brief Assign metavariable named \c m.
\pre !is_assigned(m)
*/ */
bool is_assigned(expr const & m) const { return is_assigned(metavar_idx(m)); } void assign(name const & m, expr const & t);
/** /**
\brief Return the substitution associated with the metavariable \c m. \brief Assign metavariable \c m to \c t.
If \c m has a context ctx associated with it, then the substitution is
'moved' to ctx.
\pre contains(m) \pre is_metavar(m)
*/ \pre !has_meta_context(m)
expr get_subst(expr const & m) const;
/**
\brief Return the type of the given metavariable.
If \c m has a context ctx associated with it, then the type is
'moved' to ctx.
\pre contains(m)
*/
expr get_type(expr const & m, unification_problems & up);
/**
\brief Assign the metavariable \c m to \c t.
The metavariable must not have a context associated with it.
\pre contains(m)
\pre !metavar_ctx(m)
\pre !is_assigned(m) \pre !is_assigned(m)
*/ */
void assign(expr const & m, expr const & t); void assign(expr const & m, expr const & t);
/**
\brief Return the substitution associated with the given metavariable
in this substitution.
If the metavariable is not assigned in this substitution, then it returns the null
expression.
\pre is_metavar(m)
*/
expr get_subst(expr const & m) const;
bool operator==(substitution const & s) const;
bool operator!=(substitution const & s) const { return !operator==(s); }
/**
\brief Apply f to each entry in this substitution.
*/
template<typename F>
void for_each(F f) const { m_subst.for_each(f); }
// TODO(Leo) metavar
expr mk_metavar(context const & = context()) { return expr(); }
}; };
expr instantiate(expr const & s, meta_ctx const & ctx, metavar_env const & env); /**
\brief Metavar generator.
*/
class metavar_generator {
name_generator m_gen;
public:
metavar_generator(name const & prefix);
metavar_generator();
/**
\brief Return the prefix used to create metavariables in this generator.
*/
name const & prefix() const { return m_gen.prefix(); }
/**
\brief Create a metavariable with the given type.
*/
expr mk(expr const & t);
/**
\brief Create a metavariable where the type is another
metavariable. The type of the type is a null expression.
*/
expr mk();
};
/**
\brief Apply the changes in \c lctx to \c a.
*/
expr apply_local_context(expr const & a, local_context const & lctx);
/** /**
\brief Instantiate the metavariables occurring in \c e with the substitutions \brief Instantiate the metavariables occurring in \c e with the substitutions
provided by \c env. provided by \c s.
*/ */
expr instantiate_metavars(expr const & e, metavar_env const & env); expr instantiate_metavars(expr const & e, substitution const & s);
/** /**
\brief Extend the context \c ctx with the entry <tt>lift:s:n</tt> \brief Extend the local context \c lctx with the entry <tt>lift:s:n</tt>
*/ */
meta_ctx add_lift(meta_ctx const & ctx, unsigned s, unsigned n); 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. \brief Add a lift:s:n operation to the context of the given metavariable.
@ -202,17 +147,17 @@ expr add_lift(expr const & m, unsigned s, unsigned n);
expr add_inst(expr const & m, unsigned s, expr const & v); expr add_inst(expr const & m, unsigned s, expr const & v);
/** /**
\brief Extend the context \c ctx with the entry <tt>inst:s v</tt> \brief Extend the local context \c lctx with the entry <tt>inst:s v</tt>
*/ */
meta_ctx add_inst(meta_ctx const & ctx, unsigned s, expr const & v); local_context add_inst(local_context const & lctx, unsigned s, expr const & v);
/** /**
\brief Return true iff the given metavariable has a non-empty \brief Return true iff the given metavariable has a non-empty
context associated with it. local context associated with it.
\pre is_metavar(m) \pre is_metavar(m)
*/ */
bool has_meta_context(expr const & m); bool has_local_context(expr const & m);
/** /**
\brief Return the same metavariable, but the head of the context is removed. \brief Return the same metavariable, but the head of the context is removed.
@ -223,16 +168,37 @@ bool has_meta_context(expr const & m);
expr pop_meta_context(expr const & m); expr pop_meta_context(expr const & m);
/** /**
\brief Return true iff \c e has a metavariable that is assigned in menv. \brief Return true iff \c e has a metavariable that is assigned in \c s.
*/ */
bool has_assigned_metavar(expr const & e, metavar_env const & menv); bool has_assigned_metavar(expr const & e, substitution const & s);
/** /**
\brief Return true iff \c e contains the metavariable with index \c midx. \brief Return true iff \c e contains the metavariable \c m.
The substitutions in \c menv are taken into account. The substitutions in \c s are taken into account.
\brief is_metavar(m)
*/ */
bool has_metavar(expr const & e, unsigned midx, metavar_env const & menv = metavar_env()); bool has_metavar(expr const & e, expr const & m, substitution const & s = substitution());
inline bool has_metavar(expr const & e, expr const & m, metavar_env const & menv = metavar_env()) {
return has_metavar(e, metavar_idx(m), menv);
} /**
\brief Set of unification constraints that need to be solved.
It store two kinds of problems:
1. <tt>ctx |- lhs == rhs</tt>
2. <tt>ctx |- n : t</tt>
*/
class unification_constraints {
public:
virtual ~unification_constraints() {}
/**
\brief Add a new unification problem of the form <tt>ctx |- lhs == rhs</tt>
It means that rhs is convertible to lhs.
If rhs and lhs are not types, then this is just equality (modulo normalization).
*/
virtual void add(context const & ctx, expr const & lhs, expr const & rhs) = 0;
/**
\brief Add a new unification problem of the form <tt>ctx |- n : t</tt>
*/
virtual void add_type_of(context const & ctx, expr const & n, expr const & t) = 0;
};
} }

89
src/kernel/normalizer.cpp
View file

@ -69,14 +69,14 @@ value_stack extend(value_stack const & s, svalue const & v) { return cons(v, s);
class normalizer::imp { class normalizer::imp {
typedef scoped_map<expr, svalue, expr_hash, expr_eqp> cache; typedef scoped_map<expr, svalue, expr_hash, expr_eqp> cache;
environment const & m_env; environment const & m_env;
context m_ctx; context m_ctx;
metavar_env const * m_menv; substitution const * m_subst;
unsigned m_menv_timestamp; unsigned m_subst_timestamp;
cache m_cache; cache m_cache;
unsigned m_max_depth; unsigned m_max_depth;
unsigned m_depth; unsigned m_depth;
volatile bool m_interrupted; volatile bool m_interrupted;
/** /**
\brief Auxiliary object for saving the current context. \brief Auxiliary object for saving the current context.
@ -161,14 +161,13 @@ class normalizer::imp {
lean_assert(is_metavar(m)); lean_assert(is_metavar(m));
if (is_identity_stack(s, k)) if (is_identity_stack(s, k))
return m; // nothing to be done return m; // nothing to be done
meta_ctx mctx = metavar_ctx(m); local_context lctx = metavar_lctx(m);
unsigned midx = metavar_idx(m); unsigned len_s = length(s);
unsigned len_s = length(s); unsigned len_ctx = m_ctx.size();
unsigned len_ctx = m_ctx.size();
lean_assert(k >= len_ctx); lean_assert(k >= len_ctx);
if (k > len_ctx) if (k > len_ctx)
mctx = add_lift(mctx, len_s, k - len_ctx); lctx = add_lift(lctx, len_s, k - len_ctx);
expr r = mk_metavar(midx, mctx); expr r = update_metavar(m, lctx);
buffer<expr> subst; buffer<expr> subst;
for (auto e : s) { for (auto e : s) {
subst.push_back(reify(e, k)); subst.push_back(reify(e, k));
@ -194,8 +193,8 @@ class normalizer::imp {
svalue r; svalue r;
switch (a.kind()) { switch (a.kind()) {
case expr_kind::MetaVar: case expr_kind::MetaVar:
if (m_menv && m_menv->contains(a) && m_menv->is_assigned(a)) { if (m_subst && m_subst->is_assigned(a)) {
r = normalize(m_menv->get_subst(a), s, k); r = normalize(m_subst->get_subst(a), s, k);
} else { } else {
r = svalue(updt_metavar(a, s, k)); r = svalue(updt_metavar(a, s, k));
} }
@ -323,63 +322,63 @@ class normalizer::imp {
} }
} }
void set_menv(metavar_env const * menv) { void set_subst(substitution const * subst) {
if (m_menv == menv) { if (m_subst == subst) {
// Check whether m_menv has been updated since the last time the normalizer has been invoked // Check whether m_subst has been updated since the last time the normalizer has been invoked
if (m_menv && m_menv->get_timestamp() > m_menv_timestamp) { if (m_subst && m_subst->get_timestamp() > m_subst_timestamp) {
m_menv_timestamp = m_menv->get_timestamp(); m_subst_timestamp = m_subst->get_timestamp();
m_cache.clear(); m_cache.clear();
} }
} else { } else {
m_menv = menv; m_subst = subst;
m_cache.clear(); m_cache.clear();
m_menv_timestamp = m_menv ? m_menv->get_timestamp() : 0; m_subst_timestamp = m_subst ? m_subst->get_timestamp() : 0;
} }
} }
public: public:
imp(environment const & env, unsigned max_depth): imp(environment const & env, unsigned max_depth):
m_env(env) { m_env(env) {
m_interrupted = false; m_interrupted = false;
m_max_depth = max_depth; m_max_depth = max_depth;
m_depth = 0; m_depth = 0;
m_menv = nullptr; m_subst = nullptr;
m_menv_timestamp = 0; m_subst_timestamp = 0;
} }
expr operator()(expr const & e, context const & ctx, metavar_env const * menv) { expr operator()(expr const & e, context const & ctx, substitution const * subst) {
set_ctx(ctx); set_ctx(ctx);
set_menv(menv); set_subst(subst);
unsigned k = m_ctx.size(); unsigned k = m_ctx.size();
return reify(normalize(e, value_stack(), k), k); return reify(normalize(e, value_stack(), k), k);
} }
bool is_convertible(expr const & given, expr const & expected, context const & ctx, bool is_convertible(expr const & given, expr const & expected, context const & ctx,
metavar_env * menv, unification_problems * up) { substitution * subst, unification_constraints * uc) {
if (is_convertible_core(given, expected)) if (is_convertible_core(given, expected))
return true; return true;
expr new_given = given; expr new_given = given;
expr new_expected = expected; expr new_expected = expected;
if (has_metavar(new_given) || has_metavar(new_expected)) { if (has_metavar(new_given) || has_metavar(new_expected)) {
if (!menv) if (!subst)
return false; return false;
new_given = instantiate_metavars(new_given, *menv); new_given = instantiate_metavars(new_given, *subst);
new_expected = instantiate_metavars(new_expected, *menv); new_expected = instantiate_metavars(new_expected, *subst);
if (is_convertible_core(new_given, new_expected)) if (is_convertible_core(new_given, new_expected))
return true; return true;
if (has_metavar(new_given) || has_metavar(new_expected)) { if (has_metavar(new_given) || has_metavar(new_expected)) {
// Very conservative approach, just postpone the problem. // Very conservative approach, just postpone the problem.
// We may also try to normalize new_given and new_expected even if // We may also try to normalize new_given and new_expected even if
// they contain metavariables. // they contain metavariables.
if (up) { if (uc) {
up->add_is_convertible(ctx, new_given, new_expected); uc->add(ctx, new_expected, new_given);
return true; return true;
} else { } else {
return false; return false;
} }
} }
} }
set_menv(menv); set_subst(subst);
set_ctx(ctx); set_ctx(ctx);
unsigned k = m_ctx.size(); unsigned k = m_ctx.size();
new_given = reify(normalize(new_given, value_stack(), k), k); new_given = reify(normalize(new_given, value_stack(), k), k);
@ -387,7 +386,7 @@ public:
return is_convertible_core(new_given, new_expected); return is_convertible_core(new_given, new_expected);
} }
void clear() { m_ctx = context(); m_cache.clear(); m_menv = nullptr; m_menv_timestamp = 0; } void clear() { m_ctx = context(); m_cache.clear(); m_subst = nullptr; m_subst_timestamp = 0; }
void set_interrupt(bool flag) { m_interrupted = flag; } void set_interrupt(bool flag) { m_interrupted = flag; }
}; };
@ -395,20 +394,20 @@ normalizer::normalizer(environment const & env, unsigned max_depth):m_ptr(new im
normalizer::normalizer(environment const & env):normalizer(env, std::numeric_limits<unsigned>::max()) {} normalizer::normalizer(environment const & env):normalizer(env, std::numeric_limits<unsigned>::max()) {}
normalizer::normalizer(environment const & env, options const & opts):normalizer(env, get_normalizer_max_depth(opts)) {} normalizer::normalizer(environment const & env, options const & opts):normalizer(env, get_normalizer_max_depth(opts)) {}
normalizer::~normalizer() {} normalizer::~normalizer() {}
expr normalizer::operator()(expr const & e, context const & ctx, metavar_env const * menv) { return (*m_ptr)(e, ctx, menv); } expr normalizer::operator()(expr const & e, context const & ctx, substitution const * subst) { return (*m_ptr)(e, ctx, subst); }
bool normalizer::is_convertible(expr const & t1, expr const & t2, context const & ctx, bool normalizer::is_convertible(expr const & t1, expr const & t2, context const & ctx,
metavar_env * menv, unification_problems * up) { substitution * subst, unification_constraints * uc) {
return m_ptr->is_convertible(t1, t2, ctx, menv, up); return m_ptr->is_convertible(t1, t2, ctx, subst, uc);
} }
void normalizer::clear() { m_ptr->clear(); } void normalizer::clear() { m_ptr->clear(); }
void normalizer::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); } void normalizer::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); }
expr normalize(expr const & e, environment const & env, context const & ctx, metavar_env const * menv) { expr normalize(expr const & e, environment const & env, context const & ctx, substitution const * subst) {
return normalizer(env)(e, ctx, menv); return normalizer(env)(e, ctx, subst);
} }
bool is_convertible(expr const & given, expr const & expected, environment const & env, context const & ctx, bool is_convertible(expr const & given, expr const & expected, environment const & env, context const & ctx,
metavar_env * menv, unification_problems * up) { substitution * subst, unification_constraints * uc) {
return normalizer(env).is_convertible(given, expected, ctx, menv, up); return normalizer(env).is_convertible(given, expected, ctx, subst, uc);
} }
} }

12
src/kernel/normalizer.h
View file

@ -13,8 +13,8 @@ Author: Leonardo de Moura
namespace lean { namespace lean {
class environment; class environment;
class options; class options;
class metavar_env; class substitution;
class unification_problems; class unification_constraints;
/** \brief Functional object for normalizing expressions */ /** \brief Functional object for normalizing expressions */
class normalizer { class normalizer {
class imp; class imp;
@ -25,9 +25,9 @@ public:
normalizer(environment const & env, options const & opts); normalizer(environment const & env, options const & opts);
~normalizer(); ~normalizer();
expr operator()(expr const & e, context const & ctx = context(), metavar_env const * menv = nullptr); expr operator()(expr const & e, context const & ctx = context(), substitution const * subst = nullptr);
bool is_convertible(expr const & t1, expr const & t2, context const & ctx = context(), bool is_convertible(expr const & t1, expr const & t2, context const & ctx = context(),
metavar_env * menv = nullptr, unification_problems * up = nullptr); substitution * menv = nullptr, unification_constraints * uc = nullptr);
void clear(); void clear();
@ -36,7 +36,7 @@ public:
void reset_interrupt() { set_interrupt(false); } void reset_interrupt() { set_interrupt(false); }
}; };
/** \brief Normalize \c e using the environment \c env and context \c ctx */ /** \brief Normalize \c e using the environment \c env and context \c ctx */
expr normalize(expr const & e, environment const & env, context const & ctx = context(), metavar_env const * menv = nullptr); expr normalize(expr const & e, environment const & env, context const & ctx = context(), substitution const * subst = nullptr);
bool is_convertible(expr const & t1, expr const & t2, environment const & env, context const & ctx = context(), bool is_convertible(expr const & t1, expr const & t2, environment const & env, context const & ctx = context(),
metavar_env * menv = nullptr, unification_problems * up = nullptr); substitution * subst = nullptr, unification_constraints * uc = nullptr);
} }

108
src/kernel/type_checker.cpp
View file

@ -21,14 +21,16 @@ static name g_x_name("x");
class type_checker::imp { class type_checker::imp {
typedef scoped_map<expr, expr, expr_hash, expr_eqp> cache; typedef scoped_map<expr, expr, expr_hash, expr_eqp> cache;
environment const & m_env; environment const & m_env;
cache m_cache; cache m_cache;
normalizer m_normalizer; normalizer m_normalizer;
context m_ctx; context m_ctx;
metavar_env * m_menv; substitution * m_subst;
unsigned m_menv_timestamp; unsigned m_subst_timestamp;
unification_problems * m_up; metavar_generator * m_mgen;
volatile bool m_interrupted; unification_constraints * m_uc;
volatile bool m_interrupted;
expr lookup(context const & c, unsigned i) { expr lookup(context const & c, unsigned i) {
auto p = lookup_ext(c, i); auto p = lookup_ext(c, i);
@ -44,17 +46,17 @@ class type_checker::imp {
expr r = m_normalizer(e, ctx); expr r = m_normalizer(e, ctx);
if (is_pi(r)) if (is_pi(r))
return r; return r;
if (has_metavar(r) && m_menv && m_up) { if (has_metavar(r) && m_subst && m_uc && m_mgen) {
// Create two fresh variables A and B, // Create two fresh variables A and B,
// and assign r == (Pi(x : A), B x) // and assign r == (Pi(x : A), B x)
expr A = m_menv->mk_metavar(ctx); expr A = m_mgen->mk();
expr B = m_menv->mk_metavar(ctx); expr B = m_mgen->mk();
expr p = mk_pi(g_x_name, A, B(Var(0))); expr p = mk_pi(g_x_name, A, B(Var(0)));
if (is_metavar(r) && !has_meta_context(r)) { if (is_metavar(r) && !has_local_context(r)) {
// cheap case // cheap case
m_menv->assign(r, p); m_subst->assign(r, p);
} else { } else {
m_up->add_eq(ctx, r, p); m_uc->add(ctx, r, p);
} }
return p; return p;
} }
@ -67,18 +69,18 @@ class type_checker::imp {
return ty_level(u); return ty_level(u);
if (u == Bool) if (u == Bool)
return level(); return level();
if (has_metavar(u) && m_menv && m_up) { if (has_metavar(u) && m_subst && m_uc) {
// Remark: in the current implementation we don't have level constraints and variables // Remark: in the current implementation we don't have level constraints and variables
// in the unification problem set. So, we assume the metavariable is in level 0. // in the unification problem set. So, we assume the metavariable is in level 0.
// This is a crude approximation that works most of the time. // This is a crude approximation that works most of the time.
// A better solution is consists in creating a fresh universe level k and // A better solution is consists in creating a fresh universe level k and
// associate the constraint that u == Type k. // associate the constraint that u == Type k.
// Later the constraint must be solved in the elaborator. // Later the constraint must be solved in the elaborator.
if (is_metavar(u) && !has_meta_context(u)) { if (is_metavar(u) && !has_local_context(u)) {
// cheap case // cheap case
m_menv->assign(u, Type()); m_subst->assign(u, Type());
} else { } else {
m_up->add_eq(ctx, u, Type()); m_uc->add(ctx, u, Type());
} }
return level(); return level();
} }
@ -98,11 +100,10 @@ class type_checker::imp {
expr r; expr r;
switch (e.kind()) { switch (e.kind()) {
case expr_kind::MetaVar: case expr_kind::MetaVar:
if (m_menv && m_up) { r = metavar_type(e);
return m_menv->get_type(e, *m_up); if (!r)
} else { throw kernel_exception(m_env, "metavariable does not have a type associated with it");
throw kernel_exception(m_env, "unexpected metavariable occurrence"); break;
}
case expr_kind::Constant: case expr_kind::Constant:
r = m_env.get_object(const_name(e)).get_type(); r = m_env.get_object(const_name(e)).get_type();
break; break;
@ -200,7 +201,7 @@ class type_checker::imp {
} }
bool is_convertible_core(expr const & t1, expr const & t2, context const & ctx) { bool is_convertible_core(expr const & t1, expr const & t2, context const & ctx) {
return m_normalizer.is_convertible(t1, t2, ctx, m_menv, m_up); return m_normalizer.is_convertible(t1, t2, ctx, m_subst, m_uc);
} }
void set_ctx(context const & ctx) { void set_ctx(context const & ctx) {
@ -210,17 +211,17 @@ class type_checker::imp {
} }
} }
void set_menv(metavar_env * menv) { void set_subst(substitution * subst) {
if (m_menv == menv) { if (m_subst == subst) {
// Check whether m_menv has been updated since the last time the normalizer has been invoked // Check whether m_subst has been updated since the last time the normalizer has been invoked
if (m_menv && m_menv->get_timestamp() > m_menv_timestamp) { if (m_subst && m_subst->get_timestamp() > m_subst_timestamp) {
clear(); clear();
m_menv_timestamp = m_menv->get_timestamp(); m_subst_timestamp = m_subst->get_timestamp();
} }
} else { } else {
clear(); clear();
m_menv = menv; m_subst = subst;
m_menv_timestamp = m_menv ? m_menv->get_timestamp() : 0; m_subst_timestamp = m_subst ? m_subst->get_timestamp() : 0;
} }
} }
@ -228,30 +229,33 @@ public:
imp(environment const & env): imp(environment const & env):
m_env(env), m_env(env),
m_normalizer(env) { m_normalizer(env) {
m_menv = nullptr; m_subst = nullptr;
m_menv_timestamp = 0; m_subst_timestamp = 0;
m_up = nullptr; m_mgen = nullptr;
m_interrupted = false; m_uc = nullptr;
m_interrupted = false;
} }
level infer_universe(expr const & t, context const & ctx, metavar_env * menv, unification_problems * up) { level infer_universe(expr const & t, context const & ctx, substitution * subst, metavar_generator * mgen, unification_constraints * uc) {
set_ctx(ctx); set_ctx(ctx);
set_menv(menv); set_subst(subst);
flet<unification_problems*> set(m_up, up); flet<unification_constraints*> set_uc(m_uc, uc);
flet<metavar_generator*> set_mgen(m_mgen, mgen);
return infer_universe_core(t, ctx); return infer_universe_core(t, ctx);
} }
expr infer_type(expr const & e, context const & ctx, metavar_env * menv, unification_problems * up) { expr infer_type(expr const & e, context const & ctx, substitution * subst, metavar_generator * mgen, unification_constraints * uc) {
set_ctx(ctx); set_ctx(ctx);
set_menv(menv); set_subst(subst);
flet<unification_problems*> set(m_up, up); flet<unification_constraints*> set_uc(m_uc, uc);
flet<metavar_generator*> set_mgen(m_mgen, mgen);
return infer_type_core(e, ctx); return infer_type_core(e, ctx);
} }
bool is_convertible(expr const & t1, expr const & t2, context const & ctx, metavar_env * menv, unification_problems * up) { bool is_convertible(expr const & t1, expr const & t2, context const & ctx, substitution * subst, unification_constraints * uc) {
set_ctx(ctx); set_ctx(ctx);
set_menv(menv); set_subst(subst);
flet<unification_problems*> set(m_up, up); flet<unification_constraints*> set_uc(m_uc, uc);
return is_convertible_core(t1, t2, ctx); return is_convertible_core(t1, t2, ctx);
} }
@ -264,8 +268,8 @@ public:
m_cache.clear(); m_cache.clear();
m_normalizer.clear(); m_normalizer.clear();
m_ctx = context(); m_ctx = context();
m_menv = nullptr; m_subst = nullptr;
m_menv_timestamp = 0; m_subst_timestamp = 0;
} }
normalizer & get_normalizer() { normalizer & get_normalizer() {
@ -275,16 +279,16 @@ public:
type_checker::type_checker(environment const & env):m_ptr(new imp(env)) {} type_checker::type_checker(environment const & env):m_ptr(new imp(env)) {}
type_checker::~type_checker() {} type_checker::~type_checker() {}
expr type_checker::infer_type(expr const & e, context const & ctx, metavar_env * menv, unification_problems * up) { expr type_checker::infer_type(expr const & e, context const & ctx, substitution * subst, metavar_generator * mgen, unification_constraints * uc) {
return m_ptr->infer_type(e, ctx, menv, up); return m_ptr->infer_type(e, ctx, subst, mgen, uc);
} }
level type_checker::infer_universe(expr const & e, context const & ctx, metavar_env * menv, unification_problems * up) { level type_checker::infer_universe(expr const & e, context const & ctx, substitution * subst, metavar_generator * mgen, unification_constraints * uc) {
return m_ptr->infer_universe(e, ctx, menv, up); return m_ptr->infer_universe(e, ctx, subst, mgen, uc);
} }
void type_checker::clear() { m_ptr->clear(); } void type_checker::clear() { m_ptr->clear(); }
void type_checker::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); } void type_checker::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); }
bool type_checker::is_convertible(expr const & t1, expr const & t2, context const & ctx, metavar_env * menv, unification_problems * up) { bool type_checker::is_convertible(expr const & t1, expr const & t2, context const & ctx, substitution * subst, unification_constraints * uc) {
return m_ptr->is_convertible(t1, t2, ctx, menv, up); return m_ptr->is_convertible(t1, t2, ctx, subst, uc);
} }
normalizer & type_checker::get_normalizer() { return m_ptr->get_normalizer(); } normalizer & type_checker::get_normalizer() { return m_ptr->get_normalizer(); }

35
src/kernel/type_checker.h
View file

@ -12,8 +12,9 @@ Author: Leonardo de Moura
namespace lean { namespace lean {
class environment; class environment;
class normalizer; class normalizer;
class metavar_env; class substitution;
class unification_problems; class metavar_generator;
class unification_constraints;
/** /**
\brief Lean Type Checker. It can also be used to infer types, universes and check whether a \brief Lean Type Checker. It can also be used to infer types, universes and check whether a
type \c A is convertible to a type \c B. type \c A is convertible to a type \c B.
@ -25,19 +26,31 @@ public:
type_checker(environment const & env); type_checker(environment const & env);
~type_checker(); ~type_checker();
expr infer_type(expr const & e, context const & ctx = context(), expr infer_type(expr const & e,
metavar_env * menv = nullptr, unification_problems * up = nullptr); context const & ctx = context(),
substitution * subst = nullptr,
metavar_generator * mgen = nullptr,
unification_constraints * uc = nullptr);
level infer_universe(expr const & e, context const & ctx = context(), level infer_universe(expr const & e,
metavar_env * menv = nullptr, unification_problems * up = nullptr); context const & ctx = context(),
substitution * subst = nullptr,
metavar_generator * mgen = nullptr,
unification_constraints * uc = nullptr);
void check(expr const & e, context const & ctx = context(), void check(expr const & e,
metavar_env * menv = nullptr, unification_problems * up = nullptr) { context const & ctx = context(),
infer_type(e, ctx, menv, up); substitution * subst = nullptr,
metavar_generator * mgen = nullptr,
unification_constraints * uc = nullptr) {
infer_type(e, ctx, subst, mgen, uc);
} }
bool is_convertible(expr const & t1, expr const & t2, context const & ctx = context(), bool is_convertible(expr const & t1,
metavar_env * menv = nullptr, unification_problems * up = nullptr); expr const & t2,
context const & ctx = context(),
substitution * subst = nullptr,
unification_constraints * uc = nullptr);
void clear(); void clear();

2
src/library/deep_copy.cpp
View file

@ -38,7 +38,7 @@ class deep_copy_fn {
case expr_kind::Pi: r = mk_pi(abst_name(a), apply(abst_domain(a)), apply(abst_body(a))); break; case expr_kind::Pi: r = mk_pi(abst_name(a), apply(abst_domain(a)), apply(abst_body(a))); break;
case expr_kind::Let: r = mk_let(let_name(a), apply(let_type(a)), apply(let_value(a)), apply(let_body(a))); break; case expr_kind::Let: r = mk_let(let_name(a), apply(let_type(a)), apply(let_value(a)), apply(let_body(a))); break;
case expr_kind::MetaVar: case expr_kind::MetaVar:
r = update_metavar(a, [&](meta_entry const & e) -> meta_entry { r = update_metavar(a, [&](local_entry const & e) -> local_entry {
if (e.is_inst()) if (e.is_inst())
return mk_inst(e.s(), apply(e.v())); return mk_inst(e.s(), apply(e.v()));
else else

12
src/library/expr_lt.cpp
View file

@ -52,13 +52,13 @@ bool is_lt(expr const & a, expr const & b, bool use_hash) {
return is_lt(let_body(a), let_body(b), use_hash); return is_lt(let_body(a), let_body(b), use_hash);
} }
case expr_kind::MetaVar: case expr_kind::MetaVar:
if (metavar_idx(a) != metavar_idx(b)) { if (metavar_name(a) != metavar_name(b)) {
return metavar_idx(a) < metavar_idx(b); return metavar_name(a) < metavar_name(b);
} else { } else {
auto it1 = metavar_ctx(a).begin(); auto it1 = metavar_lctx(a).begin();
auto it2 = metavar_ctx(b).begin(); auto it2 = metavar_lctx(b).begin();
auto end1 = metavar_ctx(a).end(); auto end1 = metavar_lctx(a).end();
auto end2 = metavar_ctx(b).end(); auto end2 = metavar_lctx(b).end();
for (; it1 != end1 && it2 != end2; ++it1, ++it2) { for (; it1 != end1 && it2 != end2; ++it1, ++it2) {
if (it1->kind() != it2->kind()) { if (it1->kind() != it2->kind()) {
return it1->kind() < it2->kind(); return it1->kind() < it2->kind();

152
src/library/ho_unifier.cpp
View file

@ -71,11 +71,11 @@ class ho_unifier::imp {
typedef std::tuple<context, expr, expr> constraint; typedef std::tuple<context, expr, expr> constraint;
typedef pdeque<constraint> cqueue; // constraint queue typedef pdeque<constraint> cqueue; // constraint queue
struct state { struct state {
unsigned m_id; unsigned m_id;
metavar_env m_subst; substitution m_subst;
cqueue m_queue; cqueue m_queue;
state(unsigned id, metavar_env const & menv, cqueue const & q): state(unsigned id, substitution const & subst, cqueue const & q):
m_id(id), m_subst(menv), m_queue(q) {} m_id(id), m_subst(subst), m_queue(q) {}
}; };
typedef std::vector<state> state_stack; typedef std::vector<state> state_stack;
@ -93,10 +93,10 @@ class ho_unifier::imp {
bool m_use_normalizer; bool m_use_normalizer;
bool m_use_beta; bool m_use_beta;
static metavar_env & subst_of(state & s) { return s.m_subst; } static substitution & subst_of(state & s) { return s.m_subst; }
static cqueue & queue_of(state & s) { return s.m_queue; } static cqueue & queue_of(state & s) { return s.m_queue; }
state mk_state(metavar_env const & s, cqueue const & q) { state mk_state(substitution const & s, cqueue const & q) {
unsigned id = m_next_state_id; unsigned id = m_next_state_id;
m_next_state_id++; m_next_state_id++;
return state(id, s, q); return state(id, s, q);
@ -127,11 +127,11 @@ class ho_unifier::imp {
m_delayed++; m_delayed++;
} }
void init(context const & ctx, expr const & l, expr const & r, metavar_env const & menv) { void init(context const & ctx, expr const & l, expr const & r, substitution const & subst) {
m_next_state_id = 0; m_next_state_id = 0;
m_used_aux_vars = false; m_used_aux_vars = false;
m_state_stack.clear(); m_state_stack.clear();
m_state_stack.push_back(mk_state(menv, cqueue())); m_state_stack.push_back(mk_state(subst, cqueue()));
add_constraint(ctx, l, r); add_constraint(ctx, l, r);
} }
@ -142,19 +142,18 @@ class ho_unifier::imp {
\remark \c ini_s is the initial substitution set. \c s is an extension of \c ini_s \remark \c ini_s is the initial substitution set. \c s is an extension of \c ini_s
*/ */
bool contains_solution(list<result> const & r, metavar_env const & s, residue const & rs, metavar_env const & ini_s) { bool contains_solution(list<result> const & r, substitution const & s, residue const & rs, substitution const & ini_s) {
return return
empty(rs) && empty(rs) &&
std::any_of(r.begin(), r.end(), [&](result const & prev) { std::any_of(r.begin(), r.end(), [&](result const & prev) {
if (!empty(prev.second)) if (!empty(prev.second))
return false; return false;
metavar_env const & prev_s = prev.first; // TODO(Leo) metavar
// Remark, prev_s and s are extensions of ini_s // substitution const & prev_s = prev.first;
for (unsigned i = 0; i < ini_s.size(); i++) { // if (s != prev_s)
if (!ini_s.is_assigned(i) && prev_s.get_subst(i) != s.get_subst(i)) // return false;
return false; // return true;
} return false;
return true;
}); });
} }
@ -163,7 +162,8 @@ class ho_unifier::imp {
\remark \c ini_s is the initial substitution set. \c s is an extension of \c ini_s \remark \c ini_s is the initial substitution set. \c s is an extension of \c ini_s
*/ */
metavar_env cleanup_subst(metavar_env const & s, metavar_env const & ini_s) { substitution cleanup_subst(substitution const & s, substitution const & ini_s) {
#if 0 // TODO(Leo) metavar
metavar_env new_s; metavar_env new_s;
for (unsigned i = 0; i < ini_s.size(); i++) { for (unsigned i = 0; i < ini_s.size(); i++) {
new_s.mk_metavar(s.get_type(i), s.get_context(i)); new_s.mk_metavar(s.get_type(i), s.get_context(i));
@ -178,6 +178,9 @@ class ho_unifier::imp {
} }
} }
return new_s; return new_s;
#else
return s;
#endif
} }
/** /**
@ -187,7 +190,7 @@ class ho_unifier::imp {
\remark \c ini_s is the initial substitution set. \c s is an extension of \c ini_s \remark \c ini_s is the initial substitution set. \c s is an extension of \c ini_s
*/ */
list<result> save_result(list<result> const & r, metavar_env s, residue const & rs, metavar_env const & ini_s) { list<result> save_result(list<result> const & r, substitution s, residue const & rs, substitution const & ini_s) {
if (empty(rs) && m_used_aux_vars) { if (empty(rs) && m_used_aux_vars) {
// We only do the cleanup when we don't have a residue. // We only do the cleanup when we don't have a residue.
// If we have a residue, we can only remove auxiliary metavariables that do not occur in rs // If we have a residue, we can only remove auxiliary metavariables that do not occur in rs
@ -210,12 +213,12 @@ class ho_unifier::imp {
4- \c a is an application of the form <tt>(?m ...)</tt> where ?m is an assigned metavariable. 4- \c a is an application of the form <tt>(?m ...)</tt> where ?m is an assigned metavariable.
*/ */
enum status { Solved, Failed, Continue }; enum status { Solved, Failed, Continue };
status process_metavar(expr & a, expr & b, metavar_env & s) { status process_metavar(expr & a, expr & b, substitution & s) {
if (is_metavar(a)) { if (is_metavar(a)) {
if (s.is_assigned(a)) { if (s.is_assigned(a)) {
// Case 1 // Case 1
a = s.get_subst(a); a = s.get_subst(a);
} else if (!has_meta_context(a)) { } else if (!has_local_context(a)) {
// Case 2 // Case 2
if (has_metavar(b, a, s)) { if (has_metavar(b, a, s)) {
return Failed; return Failed;
@ -225,7 +228,7 @@ class ho_unifier::imp {
return Solved; return Solved;
} }
} else { } else {
meta_entry const & me = head(metavar_ctx(a)); local_entry const & me = head(metavar_lctx(a));
if (me.is_lift() && !has_free_var(b, me.s(), me.s() + me.n())) { if (me.is_lift() && !has_free_var(b, me.s(), me.s() + me.n())) {
// Case 3 // Case 3
b = lower_free_vars(b, me.s() + me.n(), me.n()); b = lower_free_vars(b, me.s() + me.n(), me.n());
@ -316,12 +319,12 @@ class ho_unifier::imp {
/** \brief Return true iff \c a is a metavariable and has a meta context. */ /** \brief Return true iff \c a is a metavariable and has a meta context. */
bool is_metavar_with_context(expr const & a) { bool is_metavar_with_context(expr const & a) {
return is_metavar(a) && has_meta_context(a); return is_metavar(a) && has_local_context(a);
} }
/** \brief Return true if \c a is of the form <tt>(?m[...] ...)</tt> */ /** \brief Return true if \c a is of the form <tt>(?m[...] ...)</tt> */
bool is_meta_app_with_context(expr const & a) { bool is_meta_app_with_context(expr const & a) {
return is_meta_app(a) && has_meta_context(arg(a, 0)); return is_meta_app(a) && has_local_context(arg(a, 0));
} }
/** /**
@ -334,13 +337,12 @@ class ho_unifier::imp {
One possible workaround it o make sure that every metavariable has an associated type One possible workaround it o make sure that every metavariable has an associated type
before invoking ho_unifier. before invoking ho_unifier.
*/ */
class unification_problems_wrapper : public unification_problems { class unification_constraints_wrapper : public unification_constraints {
bool m_failed; bool m_failed;
public: public:
unification_problems_wrapper():m_failed(false) {} unification_constraints_wrapper():m_failed(false) {}
virtual void add_eq(context const &, expr const &, expr const &) { m_failed = true; } virtual void add(context const &, expr const &, expr const &) { m_failed = true; }
virtual void add_type_of_eq(context const &, expr const &, expr const &) { m_failed = true; } virtual void add_type_of(context const &, expr const &, expr const &) { m_failed = true; }
virtual void add_is_convertible(context const &, expr const &, expr const &) { m_failed = true; }
bool failed() const { return m_failed; } bool failed() const { return m_failed; }
}; };
@ -382,24 +384,24 @@ class ho_unifier::imp {
*/ */
bool process_meta_app(context const & ctx, expr const & a, expr const & b) { bool process_meta_app(context const & ctx, expr const & a, expr const & b) {
lean_assert(is_meta_app(a)); lean_assert(is_meta_app(a));
lean_assert(!has_meta_context(arg(a, 0))); lean_assert(!has_local_context(arg(a, 0)));
lean_assert(!is_meta_app(b)); lean_assert(!is_meta_app(b));
m_used_aux_vars = true; m_used_aux_vars = true;
expr f_a = arg(a, 0); expr f_a = arg(a, 0);
lean_assert(is_metavar(f_a)); lean_assert(is_metavar(f_a));
state top_state = m_state_stack.back(); state top_state = m_state_stack.back();
cqueue q = queue_of(top_state); cqueue q = queue_of(top_state);
metavar_env s = subst_of(top_state); substitution s = subst_of(top_state);
unsigned midx = metavar_idx(f_a); name const & mname = metavar_name(f_a);
unsigned num_a = num_args(a); unsigned num_a = num_args(a);
unification_problems_wrapper upw; unification_constraints_wrapper ucw;
buffer<expr> arg_types; buffer<expr> arg_types;
for (unsigned i = 1; i < num_a; i++) { for (unsigned i = 1; i < num_a; i++) {
arg_types.push_back(m_type_infer(arg(a, i), ctx, &s, &upw)); arg_types.push_back(m_type_infer(arg(a, i), ctx, &s, &ucw));
} }
// Clear m_type_infer cache since we don't want a reference to s inside of m_type_infer // Clear m_type_infer cache since we don't want a reference to s inside of m_type_infer
m_type_infer.clear(); m_type_infer.clear();
if (upw.failed()) if (ucw.failed())
return false; return false;
m_state_stack.pop_back(); m_state_stack.pop_back();
// Add projections // Add projections
@ -407,14 +409,14 @@ class ho_unifier::imp {
// Assign f_a <- fun (x_1 : T_0) ... (x_{num_a-1} : T_{num_a-1}), x_i // Assign f_a <- fun (x_1 : T_0) ... (x_{num_a-1} : T_{num_a-1}), x_i
cqueue new_q = q; cqueue new_q = q;
new_q.push_front(constraint(ctx, arg(a, i), b)); new_q.push_front(constraint(ctx, arg(a, i), b));
metavar_env new_s = s; substitution new_s = s;
expr proj = mk_lambda(arg_types, mk_var(num_a - i - 1)); expr proj = mk_lambda(arg_types, mk_var(num_a - i - 1));
new_s.assign(midx, proj); new_s.assign(mname, proj);
m_state_stack.push_back(mk_state(new_s, new_q)); m_state_stack.push_back(mk_state(new_s, new_q));
} }
// Add imitation // Add imitation
metavar_env new_s = s; substitution new_s = s;
cqueue new_q = q; cqueue new_q = q;
if (is_app(b)) { if (is_app(b)) {
// Imitation for applications // Imitation for applications
expr f_b = arg(b, 0); expr f_b = arg(b, 0);
@ -429,7 +431,7 @@ class ho_unifier::imp {
new_q.push_front(constraint(ctx, update_app(a, 0, h_i), arg(b, i))); new_q.push_front(constraint(ctx, update_app(a, 0, h_i), arg(b, i)));
} }
expr imitation = mk_lambda(arg_types, mk_app(imitation_args.size(), imitation_args.data())); expr imitation = mk_lambda(arg_types, mk_app(imitation_args.size(), imitation_args.data()));
new_s.assign(midx, imitation); new_s.assign(mname, imitation);
} else if (is_eq(b)) { } else if (is_eq(b)) {
// Imitation for equality // Imitation for equality
// Assign f_a <- fun (x_1 : T_0) ... (x_{num_a-1} : T_{num_a-1}), (h_1 x_1 ... x_{num_a-1}) = (h_2 x_1 ... x_{num_a-1}) // Assign f_a <- fun (x_1 : T_0) ... (x_{num_a-1} : T_{num_a-1}), (h_1 x_1 ... x_{num_a-1}) = (h_2 x_1 ... x_{num_a-1})
@ -438,7 +440,7 @@ class ho_unifier::imp {
expr h_1 = new_s.mk_metavar(ctx); expr h_1 = new_s.mk_metavar(ctx);
expr h_2 = new_s.mk_metavar(ctx); expr h_2 = new_s.mk_metavar(ctx);
expr imitation = mk_lambda(arg_types, mk_eq(mk_app_vars(h_1, num_a - 1), mk_app_vars(h_2, num_a - 1))); expr imitation = mk_lambda(arg_types, mk_eq(mk_app_vars(h_1, num_a - 1), mk_app_vars(h_2, num_a - 1)));
new_s.assign(midx, imitation); new_s.assign(mname, imitation);
new_q.push_front(constraint(ctx, update_app(a, 0, h_1), eq_lhs(b))); new_q.push_front(constraint(ctx, update_app(a, 0, h_1), eq_lhs(b)));
new_q.push_front(constraint(ctx, update_app(a, 0, h_2), eq_rhs(b))); new_q.push_front(constraint(ctx, update_app(a, 0, h_2), eq_rhs(b)));
} else if (is_abstraction(b)) { } else if (is_abstraction(b)) {
@ -450,14 +452,14 @@ class ho_unifier::imp {
expr h_1 = new_s.mk_metavar(ctx); expr h_1 = new_s.mk_metavar(ctx);
expr h_2 = new_s.mk_metavar(ctx); expr h_2 = new_s.mk_metavar(ctx);
expr imitation = mk_lambda(arg_types, update_abstraction(b, mk_app_vars(h_1, num_a - 1), mk_app_vars(h_2, num_a))); expr imitation = mk_lambda(arg_types, update_abstraction(b, mk_app_vars(h_1, num_a - 1), mk_app_vars(h_2, num_a)));
new_s.assign(midx, imitation); new_s.assign(mname, imitation);
new_q.push_front(constraint(ctx, update_app(a, 0, h_1), abst_domain(b))); new_q.push_front(constraint(ctx, update_app(a, 0, h_1), abst_domain(b)));
new_q.push_front(constraint(extend(ctx, abst_name(b), abst_domain(b)), mk_app(update_app(a, 0, h_2), Var(0)), abst_body(b))); new_q.push_front(constraint(extend(ctx, abst_name(b), abst_domain(b)), mk_app(update_app(a, 0, h_2), Var(0)), abst_body(b)));
} else { } else {
// "Dumb imitation" aka the constant function // "Dumb imitation" aka the constant function
// Assign f_a <- fun (x_1 : T_0) ... (x_{num_a-1} : T_{num_a-1}), b // Assign f_a <- fun (x_1 : T_0) ... (x_{num_a-1} : T_{num_a-1}), b
expr imitation = mk_lambda(arg_types, lift_free_vars(b, 0, num_a - 1)); expr imitation = mk_lambda(arg_types, lift_free_vars(b, 0, num_a - 1));
new_s.assign(midx, imitation); new_s.assign(mname, imitation);
} }
m_state_stack.push_back(mk_state(new_s, new_q)); m_state_stack.push_back(mk_state(new_s, new_q));
reset_delayed(); reset_delayed();
@ -466,7 +468,7 @@ class ho_unifier::imp {
/** \brief Return true if \c a is of the form ?m[inst:i t, ...] */ /** \brief Return true if \c a is of the form ?m[inst:i t, ...] */
bool is_metavar_inst(expr const & a) const { bool is_metavar_inst(expr const & a) const {
return is_metavar(a) && has_meta_context(a) && head(metavar_ctx(a)).is_inst(); return is_metavar(a) && has_local_context(a) && head(metavar_lctx(a)).is_inst();
} }
/** /**
@ -479,50 +481,50 @@ class ho_unifier::imp {
lean_assert(is_metavar_inst(a)); lean_assert(is_metavar_inst(a));
lean_assert(!is_metavar_inst(b)); lean_assert(!is_metavar_inst(b));
lean_assert(!is_meta_app(b)); lean_assert(!is_meta_app(b));
m_used_aux_vars = true; m_used_aux_vars = true;
meta_ctx mctx = metavar_ctx(a); local_context lctx = metavar_lctx(a);
unsigned midx = metavar_idx(a); name const & mname = metavar_name(a);
unsigned i = head(mctx).s(); unsigned i = head(lctx).s();
expr t = head(mctx).v(); expr t = head(lctx).v();
state top_state = m_state_stack.back(); state top_state = m_state_stack.back();
cqueue q = queue_of(top_state); cqueue q = queue_of(top_state);
metavar_env s = subst_of(top_state); substitution s = subst_of(top_state);
m_state_stack.pop_back(); m_state_stack.pop_back();
{ {
// Case 1 // Case 1
metavar_env new_s = s; substitution new_s = s;
new_s.assign(midx, mk_var(i)); new_s.assign(mname, mk_var(i));
cqueue new_q = q; cqueue new_q = q;
new_q.push_front(constraint(ctx, t, b)); new_q.push_front(constraint(ctx, t, b));
m_state_stack.push_back(mk_state(new_s, new_q)); m_state_stack.push_back(mk_state(new_s, new_q));
} }
{ {
// Case 2 // Case 2
metavar_env new_s = s; substitution new_s = s;
cqueue new_q = q; cqueue new_q = q;
if (is_app(b)) { if (is_app(b)) {
// Imitation for applications b == f(s_1, ..., s_k) // Imitation for applications b == f(s_1, ..., s_k)
// midx <- f(?h_1, ..., ?h_k) // mname <- f(?h_1, ..., ?h_k)
expr f_b = arg(b, 0); expr f_b = arg(b, 0);
unsigned num_b = num_args(b); unsigned num_b = num_args(b);
buffer<expr> imitation; buffer<expr> imitation;
imitation.push_back(f_b); imitation.push_back(f_b);
for (unsigned i = 1; i < num_b; i++) for (unsigned i = 1; i < num_b; i++)
imitation.push_back(new_s.mk_metavar(ctx)); imitation.push_back(new_s.mk_metavar(ctx));
new_s.assign(midx, mk_app(imitation.size(), imitation.data())); new_s.assign(mname, mk_app(imitation.size(), imitation.data()));
} else if (is_eq(b)) { } else if (is_eq(b)) {
// Imitation for equality b == Eq(s1, s2) // Imitation for equality b == Eq(s1, s2)
// midx <- Eq(?h_1, ?h_2) // mname <- Eq(?h_1, ?h_2)
expr h_1 = new_s.mk_metavar(ctx); expr h_1 = new_s.mk_metavar(ctx);
expr h_2 = new_s.mk_metavar(ctx); expr h_2 = new_s.mk_metavar(ctx);
new_s.assign(midx, mk_eq(h_1, h_2)); new_s.assign(mname, mk_eq(h_1, h_2));
} else if (is_abstraction(b)) { } else if (is_abstraction(b)) {
// Lambdas and Pis // Lambdas and Pis
// Imitation for Lambdas and Pis, b == Fun(x:T) B // Imitation for Lambdas and Pis, b == Fun(x:T) B
// midx <- Fun (x:?h_1) ?h_2 x) // mname <- Fun (x:?h_1) ?h_2 x)
expr h_1 = new_s.mk_metavar(ctx); expr h_1 = new_s.mk_metavar(ctx);
expr h_2 = new_s.mk_metavar(ctx); expr h_2 = new_s.mk_metavar(ctx);
new_s.assign(midx, update_abstraction(b, h_1, mk_app(h_2, Var(0)))); new_s.assign(mname, update_abstraction(b, h_1, mk_app(h_2, Var(0))));
} else { } else {
new_q.push_front(constraint(ctx, pop_meta_context(a), lift_free_vars(b, i, 1))); new_q.push_front(constraint(ctx, pop_meta_context(a), lift_free_vars(b, i, 1)));
} }
@ -535,7 +537,7 @@ class ho_unifier::imp {
\brief Process the constraint \c c. Return true if the constraint was processed or postponed, and false \brief Process the constraint \c c. Return true if the constraint was processed or postponed, and false
if it failed to solve the constraint. if it failed to solve the constraint.
*/ */
bool process(constraint const & c, metavar_env & s) { bool process(constraint const & c, substitution & s) {
context ctx = std::get<0>(c); context ctx = std::get<0>(c);
expr const & old_a = std::get<1>(c); expr const & old_a = std::get<1>(c);
expr const & old_b = std::get<2>(c); expr const & old_b = std::get<2>(c);
@ -660,8 +662,8 @@ public:
m_use_beta = get_ho_unifier_use_beta(opts); m_use_beta = get_ho_unifier_use_beta(opts);
} }
list<result> unify(context const & ctx, expr const & a, expr const & b, metavar_env const & menv) { list<result> unify(context const & ctx, expr const & a, expr const & b, substitution const & subst) {
init(ctx, a, b, menv); init(ctx, a, b, subst);
list<result> r; list<result> r;
unsigned num_solutions = 0; unsigned num_solutions = 0;
while (!m_state_stack.empty()) { while (!m_state_stack.empty()) {
@ -673,7 +675,7 @@ public:
unsigned cq_size = cq.size(); unsigned cq_size = cq.size();
if (cq.empty()) { if (cq.empty()) {
// no constraints left to be solved // no constraints left to be solved
r = save_result(r, subst_of(top_state), residue(), menv); r = save_result(r, subst_of(top_state), residue(), subst);
num_solutions++; num_solutions++;
m_state_stack.pop_back(); m_state_stack.pop_back();
} else { } else {
@ -692,7 +694,7 @@ public:
residue rs; residue rs;
for (auto c : cq) for (auto c : cq)
rs = cons(c, rs); rs = cons(c, rs);
r = save_result(r, subst_of(top_state), rs, menv); r = save_result(r, subst_of(top_state), rs, subst);
num_solutions++; num_solutions++;
reset_delayed(); reset_delayed();
m_state_stack.pop_back(); m_state_stack.pop_back();
@ -712,7 +714,7 @@ public:
ho_unifier::ho_unifier(environment const & env, options const & opts):m_ptr(new imp(env, opts)) {} ho_unifier::ho_unifier(environment const & env, options const & opts):m_ptr(new imp(env, opts)) {}
ho_unifier::~ho_unifier() {} ho_unifier::~ho_unifier() {}
void ho_unifier::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); } void ho_unifier::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); }
list<ho_unifier::result> ho_unifier::operator()(context const & ctx, expr const & l, expr const & r, metavar_env const & menv) { list<ho_unifier::result> ho_unifier::operator()(context const & ctx, expr const & l, expr const & r, substitution const & subst) {
return m_ptr->unify(ctx, l, r, menv); return m_ptr->unify(ctx, l, r, subst);
} }
} }

4
src/library/ho_unifier.h
View file

@ -21,7 +21,7 @@ public:
~ho_unifier(); ~ho_unifier();
typedef list<std::tuple<context, expr, expr>> residue; typedef list<std::tuple<context, expr, expr>> residue;
typedef std::pair<metavar_env, residue> result; typedef std::pair<substitution, residue> result;
/** /**
\brief Try to unify \c l and \c r in the context \c ctx using the input substitution \c menv. \brief Try to unify \c l and \c r in the context \c ctx using the input substitution \c menv.
@ -34,7 +34,7 @@ public:
Each pair is a possible solution. The resultant \c metavar_env may contain new metavariables. Each pair is a possible solution. The resultant \c metavar_env may contain new metavariables.
The empty list represents failure. The empty list represents failure.
*/ */
list<result> operator()(context const & ctx, expr const & l, expr const & r, metavar_env const & menv); list<result> operator()(context const & ctx, expr const & l, expr const & r, substitution const & menv);
void set_interrupt(bool flag); void set_interrupt(bool flag);
void interrupt() { set_interrupt(true); } void interrupt() { set_interrupt(true); }

65
src/library/light_checker.cpp
View file

@ -20,14 +20,15 @@ namespace lean {
class light_checker::imp { class light_checker::imp {
typedef scoped_map<expr, expr, expr_hash, expr_eqp> cache; typedef scoped_map<expr, expr, expr_hash, expr_eqp> cache;
environment m_env; environment m_env;
context m_ctx; context m_ctx;
metavar_env * m_menv; substitution * m_subst;
unsigned m_menv_timestamp; unsigned m_subst_timestamp;
unification_problems * m_up; unification_constraints * m_uc;
normalizer m_normalizer; normalizer m_normalizer;
cache m_cache; cache m_cache;
volatile bool m_interrupted; volatile bool m_interrupted;
level infer_universe(expr const & t, context const & ctx) { level infer_universe(expr const & t, context const & ctx) {
expr u = m_normalizer(infer_type(t, ctx), ctx); expr u = m_normalizer(infer_type(t, ctx), ctx);
@ -59,29 +60,29 @@ class light_checker::imp {
return instantiate(t, num_args(e)-1, &arg(e, 1)); return instantiate(t, num_args(e)-1, &arg(e, 1));
} }
void set_menv(metavar_env * menv) { void set_subst(substitution * subst) {
if (m_menv == menv) { if (m_subst == subst) {
// Check whether m_menv has been updated since the last time the normalizer has been invoked // Check whether m_subst has been updated since the last time the normalizer has been invoked
if (m_menv && m_menv->get_timestamp() > m_menv_timestamp) { if (m_subst && m_subst->get_timestamp() > m_subst_timestamp) {
m_menv_timestamp = m_menv->get_timestamp(); m_subst_timestamp = m_subst->get_timestamp();
m_cache.clear(); m_cache.clear();
} }
} else { } else {
m_menv = menv; m_subst = subst;
m_cache.clear(); m_cache.clear();
m_menv_timestamp = m_menv ? m_menv->get_timestamp() : 0; m_subst_timestamp = m_subst ? m_subst->get_timestamp() : 0;
} }
} }
expr infer_type(expr const & e, context const & ctx) { expr infer_type(expr const & e, context const & ctx) {
// cheap cases, we do not cache results // cheap cases, we do not cache results
switch (e.kind()) { switch (e.kind()) {
case expr_kind::MetaVar: case expr_kind::MetaVar: {
if (m_menv && m_up) { expr r = metavar_type(e);
return m_menv->get_type(e, *m_up); if (!r)
} else { throw kernel_exception(m_env, "metavariable does not have a type associated with it");
throw kernel_exception(m_env, "unexpected metavariable occurrence"); return r;
} }
case expr_kind::Constant: { case expr_kind::Constant: {
object const & obj = m_env.get_object(const_name(e)); object const & obj = m_env.get_object(const_name(e));
if (obj.has_type()) if (obj.has_type())
@ -176,16 +177,16 @@ public:
imp(environment const & env): imp(environment const & env):
m_env(env), m_env(env),
m_normalizer(env) { m_normalizer(env) {
m_interrupted = false; m_interrupted = false;
m_menv = nullptr; m_subst = nullptr;
m_menv_timestamp = 0; m_subst_timestamp = 0;
m_up = nullptr; m_uc = nullptr;
} }
expr operator()(expr const & e, context const & ctx, metavar_env * menv, unification_problems * up) { expr operator()(expr const & e, context const & ctx, substitution * subst, unification_constraints * uc) {
set_ctx(ctx); set_ctx(ctx);
set_menv(menv); set_subst(subst);
flet<unification_problems*> set(m_up, up); flet<unification_constraints*> set(m_uc, uc);
return infer_type(e, ctx); return infer_type(e, ctx);
} }
@ -198,14 +199,14 @@ public:
m_cache.clear(); m_cache.clear();
m_normalizer.clear(); m_normalizer.clear();
m_ctx = context(); m_ctx = context();
m_menv = nullptr; m_subst = nullptr;
m_menv_timestamp = 0; m_subst_timestamp = 0;
} }
}; };
light_checker::light_checker(environment const & env):m_ptr(new imp(env)) {} light_checker::light_checker(environment const & env):m_ptr(new imp(env)) {}
light_checker::~light_checker() {} light_checker::~light_checker() {}
expr light_checker::operator()(expr const & e, context const & ctx, metavar_env * menv, unification_problems * up) { expr light_checker::operator()(expr const & e, context const & ctx, substitution * subst, unification_constraints * uc) {
return m_ptr->operator()(e, ctx, menv, up); return m_ptr->operator()(e, ctx, subst, uc);
} }
void light_checker::clear() { m_ptr->clear(); } void light_checker::clear() { m_ptr->clear(); }
void light_checker::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); } void light_checker::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); }

6
src/library/light_checker.h
View file

@ -11,8 +11,8 @@ Author: Leonardo de Moura
namespace lean { namespace lean {
class environment; class environment;
class metavar_env; class substitution;
class unification_problems; class unification_constraints;
/** /**
\brief Functional object for "quickly" inferring the type of expressions. \brief Functional object for "quickly" inferring the type of expressions.
It does not check whether the input expression is type correct or not. It does not check whether the input expression is type correct or not.
@ -30,7 +30,7 @@ public:
light_checker(environment const & env); light_checker(environment const & env);
~light_checker(); ~light_checker();
expr operator()(expr const & e, context const & ctx = context(), metavar_env * menv = nullptr, unification_problems * up = nullptr); expr operator()(expr const & e, context const & ctx = context(), substitution * subst = nullptr, unification_constraints * uc = nullptr);
void clear(); void clear();

2
src/library/max_sharing.cpp
View file

@ -63,7 +63,7 @@ struct max_sharing_fn::imp {
return r; return r;
} }
case expr_kind::MetaVar: { case expr_kind::MetaVar: {
expr r = update_metavar(a, [=](meta_entry const & e) -> meta_entry { expr r = update_metavar(a, [=](local_entry const & e) -> local_entry {
if (e.is_inst()) if (e.is_inst())
return mk_inst(e.s(), apply(e.v())); return mk_inst(e.s(), apply(e.v()));
else else

9
src/library/placeholder.cpp
View file

@ -9,7 +9,6 @@ Author: Leonardo de Moura
#include "kernel/expr_maps.h" #include "kernel/expr_maps.h"
#include "kernel/replace.h" #include "kernel/replace.h"
#include "library/placeholder.h" #include "library/placeholder.h"
#include "library/replace_using_ctx.h"
namespace lean { namespace lean {
static name g_placeholder_name("_"); static name g_placeholder_name("_");
@ -25,10 +24,10 @@ bool has_placeholder(expr const & e) {
return occurs(mk_placholder(), e); return occurs(mk_placholder(), e);
} }
expr replace_placeholders_with_metavars(expr const & e, metavar_env & menv, expr_map<expr> * trace) { expr replace_placeholders_with_metavars(expr const & e, metavar_generator & mgen, expr_map<expr> * trace) {
auto f = [&](expr const & e, context const & ctx, unsigned) -> expr { auto f = [&](expr const & e, unsigned) -> expr {
if (is_placeholder(e)) { if (is_placeholder(e)) {
return menv.mk_metavar(ctx); return mgen.mk();
} else { } else {
return e; return e;
} }
@ -37,6 +36,6 @@ expr replace_placeholders_with_metavars(expr const & e, metavar_env & menv, expr
if (trace) if (trace)
(*trace)[t] = s; (*trace)[t] = s;
}; };
return replace_using_ctx_fn<decltype(f), decltype(p)>(f, p)(e); return replace_fn<decltype(f), decltype(p)>(f, p)(e);
} }
} }

7
src/library/placeholder.h
View file

@ -9,7 +9,8 @@ Author: Leonardo de Moura
#include "kernel/expr_maps.h" #include "kernel/expr_maps.h"
namespace lean { namespace lean {
class metavar_env; class substitution;
class metavar_generator;
/** /**
\brief Return a new placeholder expression. To be able to track location, \brief Return a new placeholder expression. To be able to track location,
a new constant for each placeholder. a new constant for each placeholder.
@ -27,9 +28,9 @@ bool is_placeholder(expr const & e);
bool has_placeholder(expr const & e); bool has_placeholder(expr const & e);
/** /**
\brief Replace the placeholders in \c e with fresh metavariables from menv. \brief Replace the placeholders in \c e with fresh metavariables from \c mgen.
if \c trace is not null, then for each new expression \c t created based on if \c trace is not null, then for each new expression \c t created based on
\c s, we store <tt>(*trace)[t] = s</tt>. We say this is traceability information. \c s, we store <tt>(*trace)[t] = s</tt>. We say this is traceability information.
*/ */
expr replace_placeholders_with_metavars(expr const & e, metavar_env & menv, expr_map<expr> * trace = nullptr); expr replace_placeholders_with_metavars(expr const & e, metavar_generator & mgen, expr_map<expr> * trace = nullptr);
} }

6
src/library/printer.cpp
View file

@ -76,11 +76,11 @@ struct print_expr_fn {
} }
void print_metavar(expr const & a, context const &) { void print_metavar(expr const & a, context const &) {
out() << "?M" << metavar_idx(a); out() << "?M" << metavar_name(a);
if (metavar_ctx(a)) { if (metavar_lctx(a)) {
out() << "["; out() << "[";
bool first = true; bool first = true;
for (meta_entry const & e : metavar_ctx(a)) { for (local_entry const & e : metavar_lctx(a)) {
if (first) first = false; else out() << ", "; if (first) first = false; else out() << ", ";
if (e.is_lift()) { if (e.is_lift()) {
out() << "lift:" << e.s() << ":" << e.n(); out() << "lift:" << e.s() << ":" << e.n();

6
src/tests/kernel/CMakeLists.txt
View file

@ -28,6 +28,6 @@ add_test(environment ${CMAKE_CURRENT_BINARY_DIR}/environment)
add_executable(occurs occurs.cpp) add_executable(occurs occurs.cpp)
target_link_libraries(occurs ${EXTRA_LIBS}) target_link_libraries(occurs ${EXTRA_LIBS})
add_test(occurs ${CMAKE_CURRENT_BINARY_DIR}/occurs) add_test(occurs ${CMAKE_CURRENT_BINARY_DIR}/occurs)
add_executable(metavar_kernel metavar.cpp) add_executable(metavar metavar.cpp)
target_link_libraries(metavar_kernel ${EXTRA_LIBS}) target_link_libraries(metavar ${EXTRA_LIBS})
add_test(metavar_kernel ${CMAKE_CURRENT_BINARY_DIR}/metavar_kernel) add_test(metavar ${CMAKE_CURRENT_BINARY_DIR}/metavar)

2
src/tests/kernel/expr.cpp
View file

@ -347,7 +347,7 @@ void tst15() {
expr f = Const("f"); expr f = Const("f");
expr x = Var(0); expr x = Var(0);
expr a = Const("a"); expr a = Const("a");
expr m = mk_metavar(0); expr m = mk_metavar("m");
lean_assert(has_metavar(m)); lean_assert(has_metavar(m));
lean_assert(has_metavar(f(m))); lean_assert(has_metavar(f(m)));
lean_assert(!has_metavar(f(a))); lean_assert(!has_metavar(f(a)));

378
src/tests/kernel/metavar.cpp
View file

@ -20,126 +20,112 @@ Author: Leonardo de Moura
#include "library/placeholder.h" #include "library/placeholder.h"
using namespace lean; using namespace lean;
class unification_problems_dbg : public unification_problems { class unification_constraints_dbg : public unification_constraints {
typedef std::tuple<context, expr, expr> constraint; typedef std::tuple<context, expr, expr> constraint;
typedef std::vector<constraint> constraints; typedef std::vector<constraint> constraints;
constraints m_eqs; constraints m_eqs;
constraints m_type_of_eqs; constraints m_type_of_eqs;
constraints m_is_convertible_cnstrs;
public: public:
unification_problems_dbg() {} unification_constraints_dbg() {}
virtual ~unification_problems_dbg() {} virtual ~unification_constraints_dbg() {}
virtual void add_eq(context const & ctx, expr const & lhs, expr const & rhs) { m_eqs.push_back(constraint(ctx, lhs, rhs)); } virtual void add(context const & ctx, expr const & lhs, expr const & rhs) { m_eqs.push_back(constraint(ctx, lhs, rhs)); }
virtual void add_type_of_eq(context const & ctx, expr const & n, expr const & t) { m_type_of_eqs.push_back(constraint(ctx, n, t)); } virtual void add_type_of(context const & ctx, expr const & n, expr const & t) { m_type_of_eqs.push_back(constraint(ctx, n, t)); }
virtual void add_is_convertible(context const & ctx, expr const & t1, expr const & t2) { m_is_convertible_cnstrs.push_back(constraint(ctx, t1, t2)); }
constraints const & eqs() const { return m_eqs; } constraints const & eqs() const { return m_eqs; }
constraints const & type_of_eqs() const { return m_type_of_eqs; } constraints const & type_of_eqs() const { return m_type_of_eqs; }
constraints const & is_convertible_cnstrs() const { return m_is_convertible_cnstrs; } friend std::ostream & operator<<(std::ostream & out, unification_constraints_dbg const & uc) {
friend std::ostream & operator<<(std::ostream & out, unification_problems_dbg const & up) { for (auto c : uc.m_eqs)
for (auto c : up.m_eqs)
std::cout << std::get<0>(c) << " |- " << std::get<1>(c) << " == " << std::get<2>(c) << "\n"; std::cout << std::get<0>(c) << " |- " << std::get<1>(c) << " == " << std::get<2>(c) << "\n";
for (auto c : up.m_type_of_eqs) for (auto c : uc.m_type_of_eqs)
std::cout << std::get<0>(c) << " |- " << std::get<1>(c) << " : " << std::get<2>(c) << "\n"; std::cout << std::get<0>(c) << " |- " << std::get<1>(c) << " : " << std::get<2>(c) << "\n";
for (auto c : up.m_is_convertible_cnstrs)
std::cout << std::get<0>(c) << " |- " << std::get<1>(c) << " == " << std::get<2>(c) << "\n";
return out; return out;
} }
}; };
std::ostream & operator<<(std::ostream & out, metavar_env const & env) { std::ostream & operator<<(std::ostream & out, substitution const & env) {
bool first = true; bool first = true;
for (unsigned i = 0; i < env.size(); i++) { env.for_each([&](name const & n, expr const & v) {
if (env.is_assigned(i)) {
if (first) first = false; else out << "\n"; if (first) first = false; else out << "\n";
out << "?M" << i << " <- " << env.get_subst(i); out << "?M" << n << " <- " << v;
} });
}
return out; return out;
} }
static void tst1() { static void tst1() {
unification_problems_dbg u; substitution subst;
metavar_env menv; metavar_generator gen;
expr m1 = menv.mk_metavar(); expr m1 = gen.mk();
lean_assert(!menv.is_assigned(m1)); lean_assert(!subst.is_assigned(m1));
lean_assert(menv.contains(m1)); expr t1 = metavar_type(m1);
lean_assert(!menv.contains(2));
expr t1 = menv.get_type(m1, u);
lean_assert(is_metavar(t1)); lean_assert(is_metavar(t1));
lean_assert(menv.contains(t1)); lean_assert(is_eqp(metavar_type(m1), t1));
lean_assert(is_eqp(menv.get_type(m1, u), t1)); lean_assert(is_eqp(metavar_type(m1), t1));
lean_assert(is_eqp(menv.get_type(m1, u), t1)); lean_assert(!subst.is_assigned(m1));
lean_assert(!menv.is_assigned(m1)); expr m2 = gen.mk();
expr m2 = menv.mk_metavar(); lean_assert(!subst.is_assigned(m1));
lean_assert(!menv.is_assigned(m1)); expr t2 = metavar_type(m2);
lean_assert(menv.contains(m1));
expr t2 = menv.get_type(m2, u);
lean_assert(is_metavar(m2)); lean_assert(is_metavar(m2));
lean_assert(menv.contains(m2));
lean_assert(!is_eqp(t1, t2)); lean_assert(!is_eqp(t1, t2));
lean_assert(t1 != t2); lean_assert(t1 != t2);
lean_assert(u.eqs().empty());
lean_assert(u.type_of_eqs().size() == 2);
for (auto p : u.type_of_eqs()) {
std::cout << "typeof(" << std::get<1>(p) << ") == " << std::get<2>(p) << "\n";
}
expr f = Const("f"); expr f = Const("f");
expr a = Const("a"); expr a = Const("a");
menv.assign(m1, f(a)); subst.assign(m1, f(a));
lean_assert(menv.is_assigned(m1)); lean_assert(subst.is_assigned(m1));
lean_assert(!menv.is_assigned(m2)); lean_assert(!subst.is_assigned(m2));
lean_assert(menv.get_subst(m1) == f(a)); lean_assert(subst.get_subst(m1) == f(a));
} }
static void tst2() { static void tst2() {
metavar_env menv; substitution subst;
metavar_generator gen;
expr f = Const("f"); expr f = Const("f");
expr g = Const("g"); expr g = Const("g");
expr h = Const("h"); expr h = Const("h");
expr a = Const("a"); expr a = Const("a");
expr m1 = menv.mk_metavar(); expr m1 = gen.mk();
expr m2 = menv.mk_metavar(); expr m2 = gen.mk();
// move m1 to a different context, and store new metavariable + context in m11 // move m1 to a different context, and store new metavariable + context in m11
std::cout << "---------------------\n"; std::cout << "---------------------\n";
expr m11 = add_inst(m1, 0, f(a, m2)); expr m11 = add_inst(m1, 0, f(a, m2));
std::cout << m11 << "\n"; std::cout << m11 << "\n";
menv.assign(m1, f(Var(0))); subst.assign(m1, f(Var(0)));
std::cout << instantiate_metavars(m11, menv) << "\n"; std::cout << instantiate_metavars(m11, subst) << "\n";
menv.assign(m2, g(a, Var(1))); subst.assign(m2, g(a, Var(1)));
std::cout << instantiate_metavars(h(m11), menv) << "\n"; std::cout << instantiate_metavars(h(m11), subst) << "\n";
lean_assert(instantiate_metavars(h(m11), menv) == h(f(f(a, g(a, Var(1)))))); lean_assert(instantiate_metavars(h(m11), subst) == h(f(f(a, g(a, Var(1))))));
} }
static void tst3() { static void tst3() {
metavar_env menv; substitution subst;
metavar_generator gen;
expr f = Const("f"); expr f = Const("f");
expr g = Const("g"); expr g = Const("g");
expr h = Const("h"); expr h = Const("h");
expr a = Const("a"); expr a = Const("a");
expr x = Const("x"); expr x = Const("x");
expr T = Const("T"); expr T = Const("T");
expr m1 = menv.mk_metavar(); expr m1 = gen.mk();
expr F = Fun({x, T}, f(m1, x)); expr F = Fun({x, T}, f(m1, x));
menv.assign(m1, h(Var(0), Var(2))); subst.assign(m1, h(Var(0), Var(2)));
std::cout << instantiate(abst_body(F), g(a)) << "\n"; std::cout << instantiate(abst_body(F), g(a)) << "\n";
std::cout << instantiate_metavars(instantiate(abst_body(F), g(a)), menv) << "\n"; std::cout << instantiate_metavars(instantiate(abst_body(F), g(a)), subst) << "\n";
lean_assert(instantiate_metavars(instantiate(abst_body(F), g(a)), menv) == f(h(g(a), Var(1)), g(a))); lean_assert(instantiate_metavars(instantiate(abst_body(F), g(a)), subst) == f(h(g(a), Var(1)), g(a)));
std::cout << instantiate(instantiate_metavars(abst_body(F), menv), g(a)) << "\n"; std::cout << instantiate(instantiate_metavars(abst_body(F), subst), g(a)) << "\n";
lean_assert(instantiate(instantiate_metavars(abst_body(F), menv), g(a)) == lean_assert(instantiate(instantiate_metavars(abst_body(F), subst), g(a)) ==
instantiate_metavars(instantiate(abst_body(F), g(a)), menv)); instantiate_metavars(instantiate(abst_body(F), g(a)), subst));
} }
static void tst4() { static void tst4() {
metavar_env menv; substitution subst;
metavar_generator gen;
expr f = Const("f"); expr f = Const("f");
expr g = Const("g"); expr g = Const("g");
expr h = Const("h"); expr h = Const("h");
expr a = Const("a"); expr a = Const("a");
expr m1 = menv.mk_metavar(); expr m1 = gen.mk();
expr F = f(m1, Var(2)); expr F = f(m1, Var(2));
menv.assign(m1, h(Var(1))); subst.assign(m1, h(Var(1)));
std::cout << instantiate(F, {g(Var(0)), h(a)}) << "\n"; std::cout << instantiate(F, {g(Var(0)), h(a)}) << "\n";
std::cout << instantiate_metavars(instantiate(F, {g(Var(0)), h(a)}), menv) << "\n"; std::cout << instantiate_metavars(instantiate(F, {g(Var(0)), h(a)}), subst) << "\n";
} }
static void tst5() { static void tst5() {
@ -154,17 +140,18 @@ static void tst6() {
expr a = Const("a"); expr a = Const("a");
expr g = Const("g"); expr g = Const("g");
expr h = Const("h"); expr h = Const("h");
metavar_env menv; substitution subst;
expr m1 = menv.mk_metavar(); metavar_generator gen;
expr m2 = menv.mk_metavar(); expr m1 = gen.mk();
expr m2 = gen.mk();
expr t = f(Var(0), Fun({x, N}, f(Var(1), x, Fun({y, N}, f(Var(2), x, y))))); expr t = f(Var(0), Fun({x, N}, f(Var(1), x, Fun({y, N}, f(Var(2), x, y)))));
expr r = instantiate(t, g(m1, m2)); expr r = instantiate(t, g(m1, m2));
std::cout << r << std::endl; std::cout << r << std::endl;
menv.assign(1, Var(2)); subst.assign(m2, Var(2));
r = instantiate_metavars(r, menv); r = instantiate_metavars(r, subst);
std::cout << r << std::endl; std::cout << r << std::endl;
menv.assign(0, h(Var(3))); subst.assign(m1, h(Var(3)));
r = instantiate_metavars(r, menv); r = instantiate_metavars(r, subst);
std::cout << r << std::endl; std::cout << r << std::endl;
lean_assert(r == f(g(h(Var(3)), Var(2)), Fun({x, N}, f(g(h(Var(4)), Var(3)), x, Fun({y, N}, f(g(h(Var(5)), Var(4)), x, y)))))); lean_assert(r == f(g(h(Var(3)), Var(2)), Fun({x, N}, f(g(h(Var(4)), Var(3)), x, Fun({y, N}, f(g(h(Var(5)), Var(4)), x, y))))));
} }
@ -173,12 +160,13 @@ static void tst7() {
expr f = Const("f"); expr f = Const("f");
expr g = Const("g"); expr g = Const("g");
expr a = Const("a"); expr a = Const("a");
metavar_env menv; substitution subst;
expr m1 = menv.mk_metavar(); metavar_generator gen;
expr m1 = gen.mk();
expr t = f(m1, Var(0)); expr t = f(m1, Var(0));
expr r = instantiate(t, a); expr r = instantiate(t, a);
menv.assign(0, g(Var(0))); subst.assign(m1, g(Var(0)));
r = instantiate_metavars(r, menv); r = instantiate_metavars(r, subst);
std::cout << r << std::endl; std::cout << r << std::endl;
lean_assert(r == f(g(a), a)); lean_assert(r == f(g(a), a));
} }
@ -187,12 +175,13 @@ static void tst8() {
expr f = Const("f"); expr f = Const("f");
expr g = Const("g"); expr g = Const("g");
expr a = Const("a"); expr a = Const("a");
metavar_env menv; substitution subst;
expr m1 = menv.mk_metavar(); metavar_generator gen;
expr m1 = gen.mk();
expr t = f(m1, Var(0), Var(2)); expr t = f(m1, Var(0), Var(2));
expr r = instantiate(t, a); expr r = instantiate(t, a);
menv.assign(0, g(Var(0), Var(1))); subst.assign(m1, g(Var(0), Var(1)));
r = instantiate_metavars(r, menv); r = instantiate_metavars(r, subst);
std::cout << r << std::endl; std::cout << r << std::endl;
lean_assert(r == f(g(a, Var(0)), a, Var(1))); lean_assert(r == f(g(a, Var(0)), a, Var(1)));
} }
@ -201,15 +190,16 @@ static void tst9() {
expr f = Const("f"); expr f = Const("f");
expr g = Const("g"); expr g = Const("g");
expr a = Const("a"); expr a = Const("a");
metavar_env menv; substitution subst;
expr m1 = menv.mk_metavar(); metavar_generator gen;
expr m1 = gen.mk();
expr t = f(m1, Var(1), Var(2)); expr t = f(m1, Var(1), Var(2));
expr r = lift_free_vars(t, 1, 2); expr r = lift_free_vars(t, 1, 2);
std::cout << r << std::endl; std::cout << r << std::endl;
r = instantiate(r, a); r = instantiate(r, a);
std::cout << r << std::endl; std::cout << r << std::endl;
menv.assign(0, g(Var(0), Var(1))); subst.assign(m1, g(Var(0), Var(1)));
r = instantiate_metavars(r, menv); r = instantiate_metavars(r, subst);
std::cout << r << std::endl; std::cout << r << std::endl;
lean_assert(r == f(g(a, Var(2)), Var(2), Var(3))); lean_assert(r == f(g(a, Var(2)), Var(2), Var(3)));
} }
@ -222,36 +212,39 @@ static void tst10() {
expr a = Const("a"); expr a = Const("a");
expr g = Const("g"); expr g = Const("g");
expr h = Const("h"); expr h = Const("h");
metavar_env menv; substitution subst;
expr m1 = menv.mk_metavar(); metavar_generator gen;
expr m2 = menv.mk_metavar(); expr m1 = gen.mk();
expr m2 = gen.mk();
expr t = f(Var(0), Fun({x, N}, f(Var(1), Var(2), x, Fun({y, N}, f(Var(2), x, y))))); expr t = f(Var(0), Fun({x, N}, f(Var(1), Var(2), x, Fun({y, N}, f(Var(2), x, y)))));
expr r = instantiate(t, g(m1)); expr r = instantiate(t, g(m1));
std::cout << r << std::endl; std::cout << r << std::endl;
r = instantiate(r, h(m2)); r = instantiate(r, h(m2));
std::cout << r << std::endl; std::cout << r << std::endl;
menv.assign(0, f(Var(0))); subst.assign(m1, f(Var(0)));
menv.assign(1, Var(2)); subst.assign(m2, Var(2));
r = instantiate_metavars(r, menv); r = instantiate_metavars(r, subst);
std::cout << r << std::endl; std::cout << r << std::endl;
lean_assert(r == f(g(f(h(Var(2)))), Fun({x, N}, f(g(f(h(Var(3)))), h(Var(3)), x, Fun({y, N}, f(g(f(h(Var(4)))), x, y)))))); lean_assert(r == f(g(f(h(Var(2)))), Fun({x, N}, f(g(f(h(Var(3)))), h(Var(3)), x, Fun({y, N}, f(g(f(h(Var(4)))), x, y))))));
} }
static void tst11() { static void tst11() {
metavar_env menv; substitution subst;
unsigned t1 = menv.get_timestamp(); unsigned t1 = subst.get_timestamp();
expr m = menv.mk_metavar(); metavar_generator gen;
unsigned t2 = menv.get_timestamp(); expr m = gen.mk();
lean_assert(t2 > t1); unsigned t2 = subst.get_timestamp();
lean_assert(!menv.is_assigned(m)); lean_assert(t2 == t1);
lean_assert(menv.get_timestamp() == t2); lean_assert(!subst.is_assigned(m));
menv.assign(m, Const("a")); lean_assert(subst.get_timestamp() == t2);
lean_assert(menv.get_timestamp() > t2); subst.assign(m, Const("a"));
lean_assert(subst.get_timestamp() > t2);
} }
static void tst12() { static void tst12() {
metavar_env menv; substitution subst;
expr m = menv.mk_metavar(); metavar_generator gen;
expr m = gen.mk();
expr f = Const("f"); expr f = Const("f");
std::cout << instantiate(f(m), {Var(0), Var(1)}) << "\n"; std::cout << instantiate(f(m), {Var(0), Var(1)}) << "\n";
std::cout << instantiate(f(m), {Var(1), Var(0)}) << "\n"; std::cout << instantiate(f(m), {Var(1), Var(0)}) << "\n";
@ -259,8 +252,9 @@ static void tst12() {
static void tst13() { static void tst13() {
environment env; environment env;
metavar_env menv; substitution subst;
expr m = menv.mk_metavar(); metavar_generator gen;
expr m = gen.mk();
env.add_var("N", Type()); env.add_var("N", Type());
expr N = Const("N"); expr N = Const("N");
env.add_var("f", N >> N); env.add_var("f", N >> N);
@ -271,17 +265,18 @@ static void tst13() {
expr F = Fun({x, N}, f(m))(a); expr F = Fun({x, N}, f(m))(a);
normalizer norm(env); normalizer norm(env);
std::cout << norm(F) << "\n"; std::cout << norm(F) << "\n";
menv.assign(0, Var(0)); subst.assign(m, Var(0));
std::cout << norm(instantiate_metavars(F, menv)) << "\n"; std::cout << norm(instantiate_metavars(F, subst)) << "\n";
lean_assert(norm(instantiate_metavars(F, menv)) == lean_assert(norm(instantiate_metavars(F, subst)) ==
instantiate_metavars(norm(F), menv)); instantiate_metavars(norm(F), subst));
} }
static void tst14() { static void tst14() {
environment env; environment env;
metavar_env menv; substitution subst;
expr m1 = menv.mk_metavar(); metavar_generator gen;
expr m2 = menv.mk_metavar(); expr m1 = gen.mk();
expr m2 = gen.mk();
expr N = Const("N"); expr N = Const("N");
expr f = Const("f"); expr f = Const("f");
expr h = Const("h"); expr h = Const("h");
@ -292,17 +287,17 @@ static void tst14() {
env.add_var("h", Pi({N, Type()}, N >> (N >> N))); env.add_var("h", Pi({N, Type()}, N >> (N >> N)));
expr F1 = Fun({{N, Type()}, {a, N}, {f, N >> N}}, expr F1 = Fun({{N, Type()}, {a, N}, {f, N >> N}},
(Fun({{x, N}, {y, N}}, Eq(f(m1), y)))(a)); (Fun({{x, N}, {y, N}}, Eq(f(m1), y)))(a));
metavar_env menv2 = menv; substitution subst2 = subst;
menv2.assign(0, h(Var(4), Var(1), Var(3))); subst2.assign(m1, h(Var(4), Var(1), Var(3)));
normalizer norm(env); normalizer norm(env);
env.add_var("M", Type()); env.add_var("M", Type());
expr M = Const("M"); expr M = Const("M");
std::cout << norm(F1) << "\n"; std::cout << norm(F1) << "\n";
std::cout << instantiate_metavars(norm(F1), menv2) << "\n"; std::cout << instantiate_metavars(norm(F1), subst2) << "\n";
std::cout << instantiate_metavars(F1, menv2) << "\n"; std::cout << instantiate_metavars(F1, subst2) << "\n";
std::cout << norm(instantiate_metavars(F1, menv2)) << "\n"; std::cout << norm(instantiate_metavars(F1, subst2)) << "\n";
lean_assert(instantiate_metavars(norm(F1), menv2) == lean_assert(instantiate_metavars(norm(F1), subst2) ==
norm(instantiate_metavars(F1, menv2))); norm(instantiate_metavars(F1, subst2)));
expr F2 = (Fun({{N, Type()}, {f, N >> N}, {a, N}, {b, N}}, expr F2 = (Fun({{N, Type()}, {f, N >> N}, {a, N}, {b, N}},
(Fun({{x, N}, {y, N}}, Eq(f(m1), y)))(a, m2)))(M); (Fun({{x, N}, {y, N}}, Eq(f(m1), y)))(a, m2)))(M);
std::cout << norm(F2) << "\n"; std::cout << norm(F2) << "\n";
@ -313,9 +308,10 @@ static void tst14() {
static void tst15() { static void tst15() {
environment env; environment env;
metavar_env menv; substitution subst;
normalizer norm(env); normalizer norm(env);
expr m1 = menv.mk_metavar(); metavar_generator gen;
expr m1 = gen.mk();
expr f = Const("f"); expr f = Const("f");
expr x = Const("x"); expr x = Const("x");
expr y = Const("y"); expr y = Const("y");
@ -324,21 +320,22 @@ static void tst15() {
env.add_var("N", Type()); env.add_var("N", Type());
env.add_var("f", Type() >> Type()); env.add_var("f", Type() >> Type());
expr F = Fun({z, Type()}, Fun({{x, Type()}, {y, Type()}}, f(m1))(N, N)); expr F = Fun({z, Type()}, Fun({{x, Type()}, {y, Type()}}, f(m1))(N, N));
menv.assign(0, Var(2)); subst.assign(m1, Var(2));
std::cout << norm(F) << "\n"; std::cout << norm(F) << "\n";
std::cout << instantiate_metavars(norm(F), menv) << "\n"; std::cout << instantiate_metavars(norm(F), subst) << "\n";
std::cout << norm(instantiate_metavars(F, menv)) << "\n"; std::cout << norm(instantiate_metavars(F, subst)) << "\n";
lean_assert(instantiate_metavars(norm(F), menv) == lean_assert(instantiate_metavars(norm(F), subst) ==
norm(instantiate_metavars(F, menv))); norm(instantiate_metavars(F, subst)));
} }
static void tst16() { static void tst16() {
environment env; environment env;
metavar_env menv; substitution subst;
normalizer norm(env); normalizer norm(env);
context ctx; context ctx;
ctx = extend(ctx, "w", Type()); ctx = extend(ctx, "w", Type());
expr m1 = menv.mk_metavar(); metavar_generator gen;
expr m1 = gen.mk();
expr f = Const("f"); expr f = Const("f");
expr x = Const("x"); expr x = Const("x");
expr y = Const("y"); expr y = Const("y");
@ -346,22 +343,23 @@ static void tst16() {
expr N = Const("N"); expr N = Const("N");
env.add_var("N", Type()); env.add_var("N", Type());
expr F = Fun({z, Type()}, Fun({{x, Type()}, {y, Type()}}, m1)(N, N)); expr F = Fun({z, Type()}, Fun({{x, Type()}, {y, Type()}}, m1)(N, N));
menv.assign(0, Var(3)); subst.assign(m1, Var(3));
std::cout << norm(F, ctx) << "\n"; std::cout << norm(F, ctx) << "\n";
std::cout << instantiate_metavars(norm(F, ctx), menv) << "\n"; std::cout << instantiate_metavars(norm(F, ctx), subst) << "\n";
std::cout << norm(instantiate_metavars(F, menv), ctx) << "\n"; std::cout << norm(instantiate_metavars(F, subst), ctx) << "\n";
} }
static void tst17() { static void tst17() {
environment env; environment env;
metavar_env menv; substitution subst;
normalizer norm(env); normalizer norm(env);
context ctx; context ctx;
ctx = extend(ctx, "w1", Type()); ctx = extend(ctx, "w1", Type());
ctx = extend(ctx, "w2", Type()); ctx = extend(ctx, "w2", Type());
ctx = extend(ctx, "w3", Type()); ctx = extend(ctx, "w3", Type());
ctx = extend(ctx, "w4", Type()); ctx = extend(ctx, "w4", Type());
expr m1 = menv.mk_metavar(); metavar_generator gen;
expr m1 = gen.mk();
expr f = Const("f"); expr f = Const("f");
expr x = Const("x"); expr x = Const("x");
expr y = Const("y"); expr y = Const("y");
@ -369,32 +367,33 @@ static void tst17() {
expr N = Const("N"); expr N = Const("N");
env.add_var("N", Type()); env.add_var("N", Type());
expr F = Fun({z, Type()}, Fun({{x, Type()}, {y, Type()}}, m1)(N, N)); expr F = Fun({z, Type()}, Fun({{x, Type()}, {y, Type()}}, m1)(N, N));
metavar_env menv2 = menv; substitution subst2 = subst;
menv.assign(0, Var(3)); subst.assign(m1, Var(3));
std::cout << norm(F, ctx) << "\n"; std::cout << norm(F, ctx) << "\n";
std::cout << instantiate_metavars(norm(F, ctx), menv) << "\n"; std::cout << instantiate_metavars(norm(F, ctx), subst) << "\n";
std::cout << norm(instantiate_metavars(F, menv), ctx) << "\n"; std::cout << norm(instantiate_metavars(F, subst), ctx) << "\n";
F = Fun({z, Type()}, Fun({{x, Type()}, {y, Type()}, {x, Type()}, {y, Type()}, {x, Type()}}, m1)(N, N, N, N, N)); F = Fun({z, Type()}, Fun({{x, Type()}, {y, Type()}, {x, Type()}, {y, Type()}, {x, Type()}}, m1)(N, N, N, N, N));
lean_assert(instantiate_metavars(norm(F, ctx), menv) == lean_assert(instantiate_metavars(norm(F, ctx), subst) ==
norm(instantiate_metavars(F, menv), ctx)); norm(instantiate_metavars(F, subst), ctx));
std::cout << "----------------------\n"; std::cout << "----------------------\n";
menv2.assign(0, Var(8)); subst2.assign(m1, Var(8));
std::cout << norm(F, ctx) << "\n"; std::cout << norm(F, ctx) << "\n";
std::cout << instantiate_metavars(norm(F, ctx), menv2) << "\n"; std::cout << instantiate_metavars(norm(F, ctx), subst2) << "\n";
std::cout << norm(instantiate_metavars(F, menv2), ctx) << "\n"; std::cout << norm(instantiate_metavars(F, subst2), ctx) << "\n";
lean_assert(instantiate_metavars(norm(F, ctx), menv2) == lean_assert(instantiate_metavars(norm(F, ctx), subst2) ==
norm(instantiate_metavars(F, menv2), ctx)); norm(instantiate_metavars(F, subst2), ctx));
} }
static void tst18() { static void tst18() {
environment env; environment env;
metavar_env menv; substitution subst;
normalizer norm(env); normalizer norm(env);
context ctx; context ctx;
ctx = extend(ctx, "w1", Type()); ctx = extend(ctx, "w1", Type());
ctx = extend(ctx, "w2", Type()); ctx = extend(ctx, "w2", Type());
expr m1 = menv.mk_metavar(); metavar_generator gen;
expr m2 = menv.mk_metavar(); expr m1 = gen.mk();
expr m2 = gen.mk();
expr f = Const("f"); expr f = Const("f");
expr g = Const("g"); expr g = Const("g");
expr h = Const("h"); expr h = Const("h");
@ -409,25 +408,26 @@ static void tst18() {
env.add_var("h", N >> (N >> N)); env.add_var("h", N >> (N >> N));
expr F = Fun({z, Type()}, Fun({{f, N >> N}, {y, Type()}}, m1)(Fun({x, N}, g(z, x, m2)), N)); expr F = Fun({z, Type()}, Fun({{f, N >> N}, {y, Type()}}, m1)(Fun({x, N}, g(z, x, m2)), N));
std::cout << norm(F, ctx) << "\n"; std::cout << norm(F, ctx) << "\n";
metavar_env menv2 = menv; substitution subst2 = subst;
menv2.assign(0, Var(1)); subst2.assign(m1, Var(1));
menv2.assign(1, h(Var(2), Var(1))); subst2.assign(m2, h(Var(2), Var(1)));
std::cout << instantiate_metavars(norm(F, ctx), menv2) << "\n"; std::cout << instantiate_metavars(norm(F, ctx), subst2) << "\n";
std::cout << instantiate_metavars(F, menv2) << "\n"; std::cout << instantiate_metavars(F, subst2) << "\n";
lean_assert(instantiate_metavars(norm(F, ctx), menv2) == lean_assert(instantiate_metavars(norm(F, ctx), subst2) ==
norm(instantiate_metavars(F, menv2), ctx)); norm(instantiate_metavars(F, subst2), ctx));
lean_assert(instantiate_metavars(norm(F, ctx), menv2) == lean_assert(instantiate_metavars(norm(F, ctx), subst2) ==
Fun({{z, Type()}, {x, N}}, g(z, x, h(Var(2), z)))); Fun({{z, Type()}, {x, N}}, g(z, x, h(Var(2), z))));
} }
static void tst19() { static void tst19() {
environment env; environment env;
metavar_env menv; substitution subst;
normalizer norm(env); normalizer norm(env);
context ctx; context ctx;
ctx = extend(ctx, "w1", Type()); ctx = extend(ctx, "w1", Type());
ctx = extend(ctx, "w2", Type()); ctx = extend(ctx, "w2", Type());
expr m1 = menv.mk_metavar(); metavar_generator gen;
expr m1 = gen.mk();
expr x = Const("x"); expr x = Const("x");
expr y = Const("y"); expr y = Const("y");
expr N = Const("N"); expr N = Const("N");
@ -440,12 +440,13 @@ static void tst19() {
static void tst20() { static void tst20() {
environment env; environment env;
metavar_env menv; substitution subst;
normalizer norm(env); normalizer norm(env);
context ctx; context ctx;
ctx = extend(ctx, "w1", Type()); ctx = extend(ctx, "w1", Type());
ctx = extend(ctx, "w2", Type()); ctx = extend(ctx, "w2", Type());
expr m1 = menv.mk_metavar(); metavar_generator gen;
expr m1 = gen.mk();
expr x = Const("x"); expr x = Const("x");
expr y = Const("y"); expr y = Const("y");
expr z = Const("z"); expr z = Const("z");
@ -461,38 +462,37 @@ static void tst20() {
} }
static void tst21() { static void tst21() {
metavar_env menv; substitution subst;
expr m1 = menv.mk_metavar(); metavar_generator gen;
lean_assert(add_lift(add_lift(m1, 0, 1), 1, 1) == expr m1 = gen.mk();
add_lift(m1, 0, 2)); expr l = add_lift(add_lift(m1, 0, 1), 1, 1);
lean_assert(add_lift(add_lift(m1, 1, 2), 3, 4) == expr r = add_lift(m1, 0, 2);
add_lift(m1, 1, 6)); std::cout << metavar_type(l) << " " << metavar_type(r) << "\n";
lean_assert(add_lift(add_lift(m1, 1, 3), 3, 4) != lean_assert_eq(l, r);
add_lift(m1, 1, 7)); lean_assert_eq(add_lift(add_lift(m1, 1, 2), 3, 4),
add_lift(m1, 1, 6));
lean_assert_ne(add_lift(add_lift(m1, 1, 3), 3, 4),
add_lift(m1, 1, 7));
} }
#define _ mk_placholder() #define _ mk_placholder()
static void tst22() { static void tst22() {
metavar_env menv; substitution subst;
metavar_generator mgen;
expr f = Const("f"); expr f = Const("f");
expr x = Const("x"); expr x = Const("x");
expr N = Const("N"); expr N = Const("N");
expr F = f(Fun({x, N}, f(_, x)), _); expr F = f(Fun({x, N}, f(_, x)), _);
std::cout << F << "\n"; std::cout << F << "\n";
std::cout << replace_placeholders_with_metavars(F, menv) << "\n"; std::cout << replace_placeholders_with_metavars(F, mgen) << "\n";
lean_assert(menv.contains(0));
lean_assert(menv.contains(1));
lean_assert(!menv.contains(2));
lean_assert(menv.get_context(0).size() == 1);
lean_assert(lookup(menv.get_context(0), 0).get_domain() == N);
lean_assert(menv.get_context(1).size() == 0);
} }
static void tst23() { static void tst23() {
environment env; environment env;
metavar_env menv; substitution subst;
unification_problems_dbg up; unification_constraints_dbg up;
metavar_generator mgen;
type_checker checker(env); type_checker checker(env);
expr N = Const("N"); expr N = Const("N");
expr f = Const("f"); expr f = Const("f");
@ -502,28 +502,30 @@ static void tst23() {
env.add_var("a", N); env.add_var("a", N);
expr x = Const("x"); expr x = Const("x");
expr F0 = f(Fun({x, N}, f(_, x))(a), _); expr F0 = f(Fun({x, N}, f(_, x))(a), _);
expr F1 = replace_placeholders_with_metavars(F0, menv); expr F1 = replace_placeholders_with_metavars(F0, mgen);
std::cout << F1 << "\n"; std::cout << F1 << "\n";
std::cout << checker.infer_type(F1, context(), &menv, &up) << "\n"; std::cout << checker.infer_type(F1, context(), &subst, &mgen, &up) << "\n";
std::cout << up << "\n"; std::cout << up << "\n";
} }
static void tst24() { static void tst24() {
metavar_env menv; substitution subst;
expr m1 = menv.mk_metavar(); metavar_generator gen;
expr m2 = menv.mk_metavar(); expr m1 = gen.mk();
expr m2 = gen.mk();
expr f = Const("f"); expr f = Const("f");
expr a = Const("a"); expr a = Const("a");
menv.assign(m1, f(m2)); subst.assign(m1, f(m2));
menv.assign(m2, a); subst.assign(m2, a);
lean_assert(instantiate_metavars(f(m1), menv) == f(f(a))); lean_assert(instantiate_metavars(f(m1), subst) == f(f(a)));
std::cout << instantiate_metavars(f(m1), menv) << "\n"; std::cout << instantiate_metavars(f(m1), subst) << "\n";
} }
static void tst25() { static void tst25() {
environment env; environment env;
metavar_env menv; substitution subst;
unification_problems_dbg up; unification_constraints_dbg up;
metavar_generator gen;
type_checker checker(env); type_checker checker(env);
expr N = Const("N"); expr N = Const("N");
expr a = Const("a"); expr a = Const("a");
@ -531,10 +533,10 @@ static void tst25() {
env.add_var("N", Type()); env.add_var("N", Type());
env.add_var("a", N); env.add_var("a", N);
env.add_var("b", N); env.add_var("b", N);
expr m = menv.mk_metavar(); expr m = gen.mk();
expr F = m(a, b); expr F = m(a, b);
std::cout << checker.infer_type(F, context(), &menv, &up) << "\n"; std::cout << checker.infer_type(F, context(), &subst, &gen, &up) << "\n";
std::cout << menv << "\n"; std::cout << subst << "\n";
std::cout << up << "\n"; std::cout << up << "\n";
} }

4
src/tests/library/deep_copy.cpp
View file

@ -16,8 +16,8 @@ static void tst1() {
expr x = Var(0); expr x = Var(0);
expr t = Type(); expr t = Type();
expr z = Const("z"); expr z = Const("z");
meta_ctx ctx{mk_lift(0, 1), mk_inst(0, a)}; local_context lctx{mk_lift(0, 1), mk_inst(0, a)};
expr m = mk_metavar(0, ctx); expr m = mk_metavar("a", expr(), lctx);
expr F = mk_let("z", Type(), Type(level()+1), mk_pi("y", t, mk_lambda("x", t, f(f(f(x, a), Const("10")), Eq(x, m))))); expr F = mk_let("z", Type(), Type(level()+1), mk_pi("y", t, mk_lambda("x", t, f(f(f(x, a), Const("10")), Eq(x, m)))));
expr G = deep_copy(F); expr G = deep_copy(F);
lean_assert(F == G); lean_assert(F == G);

22
src/tests/library/expr_lt.cpp
View file

@ -65,17 +65,17 @@ static void tst1() {
lt(mk_pi("x", Int, Int), mk_pi("y", Real, Bool), true); lt(mk_pi("x", Int, Int), mk_pi("y", Real, Bool), true);
lt(mk_pi("x", Int, Int), mk_pi("y", Int, Real), true); lt(mk_pi("x", Int, Int), mk_pi("y", Int, Real), true);
lt(mk_pi("x", Int, Int), mk_pi("y", Int, Int), false); lt(mk_pi("x", Int, Int), mk_pi("y", Int, Int), false);
meta_ctx ctx1{mk_lift(0, 1), mk_inst(0, Const("a"))}; local_context lctx1{mk_lift(0, 1), mk_inst(0, Const("a"))};
meta_ctx ctx2{mk_lift(0, 1), mk_inst(0, Const("b"))}; local_context lctx2{mk_lift(0, 1), mk_inst(0, Const("b"))};
meta_ctx ctx3{mk_lift(3, 1), mk_inst(0, Const("a"))}; local_context lctx3{mk_lift(3, 1), mk_inst(0, Const("a"))};
meta_ctx ctx4{mk_lift(0, 1), mk_inst(0, Const("a")), mk_inst(0, Const("b"))}; local_context lctx4{mk_lift(0, 1), mk_inst(0, Const("a")), mk_inst(0, Const("b"))};
meta_ctx ctx5{mk_inst(0, Const("a")), mk_inst(0, Const("a"))}; local_context lctx5{mk_inst(0, Const("a")), mk_inst(0, Const("a"))};
lt(mk_metavar(0, ctx1), mk_metavar(1, ctx1), true); lt(mk_metavar("a", expr(), lctx1), mk_metavar("b", expr(), lctx1), true);
lt(mk_metavar(0, ctx1), mk_metavar(0, ctx2), true); lt(mk_metavar("a", expr(), lctx1), mk_metavar("a", expr(), lctx2), true);
lt(mk_metavar(0, ctx1), mk_metavar(0, ctx3), true); lt(mk_metavar("a", expr(), lctx1), mk_metavar("a", expr(), lctx3), true);
lt(mk_metavar(0, ctx1), mk_metavar(0, ctx4), true); lt(mk_metavar("a", expr(), lctx1), mk_metavar("a", expr(), lctx4), true);
lt(mk_metavar(0, ctx1), mk_metavar(0, ctx5), true); lt(mk_metavar("a", expr(), lctx1), mk_metavar("a", expr(), lctx5), true);
lt(mk_metavar(0, ctx1), mk_metavar(0, ctx1), false); lt(mk_metavar("a", expr(), lctx1), mk_metavar("a", expr(), lctx1), false);
} }
int main() { int main() {

72
src/tests/library/ho_unifier.cpp
View file

@ -16,7 +16,7 @@ using namespace lean;
void tst1() { void tst1() {
environment env; environment env;
metavar_env menv; substitution subst;
ho_unifier unify(env); ho_unifier unify(env);
expr N = Const("N"); expr N = Const("N");
expr M = Const("M"); expr M = Const("M");
@ -29,10 +29,10 @@ void tst1() {
expr x = Const("x"); expr x = Const("x");
expr a = Const("a"); expr a = Const("a");
expr b = Const("b"); expr b = Const("b");
expr m1 = menv.mk_metavar(); expr m1 = subst.mk_metavar();
expr l = m1(b, a); expr l = m1(b, a);
expr r = f(b, f(a, b)); expr r = f(b, f(a, b));
for (auto sol : unify(context(), l, r, menv)) { for (auto sol : unify(context(), l, r, subst)) {
std::cout << m1 << " -> " << beta_reduce(sol.first.get_subst(m1)) << "\n"; std::cout << m1 << " -> " << beta_reduce(sol.first.get_subst(m1)) << "\n";
std::cout << beta_reduce(instantiate_metavars(l, sol.first)) << "\n"; std::cout << beta_reduce(instantiate_metavars(l, sol.first)) << "\n";
lean_assert(beta_reduce(instantiate_metavars(l, sol.first)) == r); lean_assert(beta_reduce(instantiate_metavars(l, sol.first)) == r);
@ -43,7 +43,7 @@ void tst1() {
void tst2() { void tst2() {
environment env; environment env;
import_basic(env); import_basic(env);
metavar_env menv; substitution subst;
ho_unifier unify(env); ho_unifier unify(env);
expr N = Const("N"); expr N = Const("N");
expr M = Const("M"); expr M = Const("M");
@ -55,10 +55,10 @@ void tst2() {
expr x = Const("x"); expr x = Const("x");
expr a = Const("a"); expr a = Const("a");
expr b = Const("b"); expr b = Const("b");
expr m1 = menv.mk_metavar(); expr m1 = subst.mk_metavar();
expr l = m1(b, a); expr l = m1(b, a);
expr r = Fun({x, N}, f(x, Eq(a, b))); expr r = Fun({x, N}, f(x, Eq(a, b)));
for (auto sol : unify(context(), l, r, menv)) { for (auto sol : unify(context(), l, r, subst)) {
std::cout << m1 << " -> " << beta_reduce(sol.first.get_subst(m1)) << "\n"; std::cout << m1 << " -> " << beta_reduce(sol.first.get_subst(m1)) << "\n";
std::cout << beta_reduce(instantiate_metavars(l, sol.first)) << "\n"; std::cout << beta_reduce(instantiate_metavars(l, sol.first)) << "\n";
lean_assert(beta_reduce(instantiate_metavars(l, sol.first)) == r); lean_assert(beta_reduce(instantiate_metavars(l, sol.first)) == r);
@ -70,24 +70,24 @@ void tst3() {
environment env; environment env;
import_basic(env); import_basic(env);
import_arith(env); import_arith(env);
metavar_env menv; substitution subst;
ho_unifier unify(env); ho_unifier unify(env);
expr N = Const("N"); expr N = Const("N");
env.add_var("N", Type()); env.add_var("N", Type());
env.add_var("f", N >> (Int >> N)); env.add_var("f", N >> (Int >> N));
env.add_var("a", N); env.add_var("a", N);
env.add_var("b", N); env.add_var("b", N);
expr m1 = menv.mk_metavar(); expr m1 = subst.mk_metavar();
expr m2 = menv.mk_metavar(); expr m2 = subst.mk_metavar();
expr m3 = menv.mk_metavar(); expr m3 = subst.mk_metavar();
expr t1 = menv.get_type(m1); expr t1 = metavar_type(m1);
expr t2 = menv.get_type(m2); expr t2 = metavar_type(m2);
expr f = Const("f"); expr f = Const("f");
expr a = Const("a"); expr a = Const("a");
expr b = Const("b"); expr b = Const("b");
expr l = f(m1(a), iAdd(m3, iAdd(iVal(1), iVal(1)))); expr l = f(m1(a), iAdd(m3, iAdd(iVal(1), iVal(1))));
expr r = f(m2(b), iAdd(iVal(1), iVal(2))); expr r = f(m2(b), iAdd(iVal(1), iVal(2)));
for (auto sol : unify(context(), l, r, menv)) { for (auto sol : unify(context(), l, r, subst)) {
std::cout << m3 << " -> " << sol.first.get_subst(m3) << "\n"; std::cout << m3 << " -> " << sol.first.get_subst(m3) << "\n";
lean_assert(sol.first.get_subst(m3) == iVal(1)); lean_assert(sol.first.get_subst(m3) == iVal(1));
lean_assert(length(sol.second) == 1); lean_assert(length(sol.second) == 1);
@ -99,19 +99,19 @@ void tst3() {
void tst4() { void tst4() {
environment env; environment env;
metavar_env menv; substitution subst;
ho_unifier unify(env); ho_unifier unify(env);
expr N = Const("N"); expr N = Const("N");
env.add_var("N", Type()); env.add_var("N", Type());
env.add_var("f", N >> (N >> N)); env.add_var("f", N >> (N >> N));
expr x = Const("x"); expr x = Const("x");
expr y = Const("y"); expr y = Const("y");
expr f = Const("f"); expr f = Const("f");
expr m1 = menv.mk_metavar(); expr m1 = subst.mk_metavar();
expr m2 = menv.mk_metavar(); expr m2 = subst.mk_metavar();
expr l = Fun({{x, N}, {y, N}}, Eq(y, f(x, m1))); expr l = Fun({{x, N}, {y, N}}, Eq(y, f(x, m1)));
expr r = Fun({{x, N}, {y, N}}, Eq(m2, f(m1, x))); expr r = Fun({{x, N}, {y, N}}, Eq(m2, f(m1, x)));
auto sols = unify(context(), l, r, menv); auto sols = unify(context(), l, r, subst);
lean_assert(length(sols) == 1); lean_assert(length(sols) == 1);
for (auto sol : sols) { for (auto sol : sols) {
std::cout << m1 << " -> " << sol.first.get_subst(m1) << "\n"; std::cout << m1 << " -> " << sol.first.get_subst(m1) << "\n";
@ -124,33 +124,33 @@ void tst4() {
void tst5() { void tst5() {
environment env; environment env;
metavar_env menv; substitution subst;
ho_unifier unify(env); ho_unifier unify(env);
expr N = Const("N"); expr N = Const("N");
env.add_var("N", Type()); env.add_var("N", Type());
env.add_var("f", N >> (N >> N)); env.add_var("f", N >> (N >> N));
expr f = Const("f"); expr f = Const("f");
expr m1 = menv.mk_metavar(); expr m1 = subst.mk_metavar();
expr l = f(f(m1)); expr l = f(f(m1));
expr r = f(m1); expr r = f(m1);
auto sols = unify(context(), l, r, menv); auto sols = unify(context(), l, r, subst);
lean_assert(length(sols) == 0); lean_assert(length(sols) == 0);
} }
void tst6() { void tst6() {
environment env; environment env;
metavar_env menv; substitution subst;
ho_unifier unify(env); ho_unifier unify(env);
expr N = Const("N"); expr N = Const("N");
env.add_var("N", Type()); env.add_var("N", Type());
env.add_var("f", N >> (N >> N)); env.add_var("f", N >> (N >> N));
expr x = Const("x"); expr x = Const("x");
expr y = Const("y"); expr y = Const("y");
expr f = Const("f"); expr f = Const("f");
expr m1 = menv.mk_metavar(); expr m1 = subst.mk_metavar();
expr l = Fun({x, N}, Fun({y, N}, f(m1, y))(x)); expr l = Fun({x, N}, Fun({y, N}, f(m1, y))(x));
expr r = Fun({x, N}, f(x, x)); expr r = Fun({x, N}, f(x, x));
auto sols = unify(context(), l, r, menv); auto sols = unify(context(), l, r, subst);
lean_assert(length(sols) == 2); lean_assert(length(sols) == 2);
for (auto sol : sols) { for (auto sol : sols) {
std::cout << m1 << " -> " << sol.first.get_subst(m1) << "\n"; std::cout << m1 << " -> " << sol.first.get_subst(m1) << "\n";

6
src/tests/library/max_sharing.cpp
View file

@ -29,9 +29,9 @@ static void tst1() {
std::cout << F2 << "\n"; std::cout << F2 << "\n";
lean_assert(is_eqp(arg(F2, 1), arg(F2, 2))); lean_assert(is_eqp(arg(F2, 1), arg(F2, 2)));
max_fn.clear(); max_fn.clear();
meta_ctx ctx{mk_lift(1, 1), mk_inst(0, a1)}; local_context lctx{mk_lift(1, 1), mk_inst(0, a1)};
expr m1 = mk_metavar(0, ctx); expr m1 = mk_metavar("m1", expr(), lctx);
expr m2 = mk_metavar(0, ctx); expr m2 = mk_metavar("m1", expr(), lctx);
F1 = f(m1, m2); F1 = f(m1, m2);
lean_assert(!is_eqp(arg(F1, 1), arg(F1, 2))); lean_assert(!is_eqp(arg(F1, 1), arg(F1, 2)));
F2 = max_fn(F1); F2 = max_fn(F1);

14
src/tests/library/rewriter/fo_match.cpp
View file

@ -8,6 +8,7 @@ Author: Soonho Kong
#include "util/trace.h" #include "util/trace.h"
#include "kernel/abstract.h" #include "kernel/abstract.h"
#include "kernel/expr.h" #include "kernel/expr.h"
#include "kernel/metavar.h"
#include "library/all/all.h" #include "library/all/all.h"
#include "library/arith/arith.h" #include "library/arith/arith.h"
#include "library/arith/nat.h" #include "library/arith/nat.h"
@ -398,8 +399,9 @@ static void match_eq_tst3() {
static void match_metavar_tst1() { static void match_metavar_tst1() {
cout << "--- match_metavar_tst1() ---" << endl; cout << "--- match_metavar_tst1() ---" << endl;
expr m1 = mk_metavar(0); metavar_generator gen;
expr m2 = mk_metavar(1); expr m1 = gen.mk();
expr m2 = gen.mk();
expr f = Const("f"); expr f = Const("f");
subst_map s; subst_map s;
bool result = test_match(m1, m1, 0, s); bool result = test_match(m1, m1, 0, s);
@ -409,8 +411,9 @@ static void match_metavar_tst1() {
static void match_metavar_tst2() { static void match_metavar_tst2() {
cout << "--- match_metavar_tst2() ---" << endl; cout << "--- match_metavar_tst2() ---" << endl;
expr m1 = mk_metavar(0); metavar_generator gen;
expr m2 = mk_metavar(1); expr m1 = gen.mk();
expr m2 = gen.mk();
expr f = Const("f"); expr f = Const("f");
subst_map s; subst_map s;
bool result = test_match(m1, m2, 0, s); bool result = test_match(m1, m2, 0, s);
@ -420,7 +423,8 @@ static void match_metavar_tst2() {
static void match_metavar_tst3() { static void match_metavar_tst3() {
cout << "--- match_metavar_tst3() ---" << endl; cout << "--- match_metavar_tst3() ---" << endl;
expr m1 = mk_metavar(0); metavar_generator gen;
expr m1 = gen.mk();
expr f = Const("f"); expr f = Const("f");
subst_map s; subst_map s;
bool result = test_match(m1, f, 0, s); bool result = test_match(m1, f, 0, s);

1
src/util/name.h
View file

@ -96,4 +96,5 @@ public:
}; };
struct name_hash { unsigned operator()(name const & n) const { return n.hash(); } }; struct name_hash { unsigned operator()(name const & n) const { return n.hash(); } };
struct name_eq { bool operator()(name const & n1, name const & n2) const { return n1 == n2; } }; struct name_eq { bool operator()(name const & n1, name const & n2) const { return n1 == n2; } };
struct name_cmp { int operator()(name const & n1, name const & n2) const { return cmp(n1, n2); } };
} }

2
src/util/splay_map.h
View file

@ -15,7 +15,9 @@ namespace lean {
*/ */
template<typename K, typename T, typename CMP> template<typename K, typename T, typename CMP>
class splay_map : public CMP { class splay_map : public CMP {
public:
typedef std::pair<K, T> entry; typedef std::pair<K, T> entry;
private:
struct entry_cmp : public CMP { struct entry_cmp : public CMP {
entry_cmp(CMP const & c):CMP(c) {} entry_cmp(CMP const & c):CMP(c) {}
int operator()(entry const & e1, entry const & e2) const { return CMP::operator()(e1.first, e2.first); } int operator()(entry const & e1, entry const & e2) const { return CMP::operator()(e1.first, e2.first); }