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

Simplify the elaborator

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-27 20:39:38 -07:00
parent 8dacd97801
commit cdab19b88c
5 changed files with 149 additions and 491 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/frontends/lean/lean_parser.cpp
View file

@ -116,7 +116,6 @@ class parser::imp {
bool m_found_errors; bool m_found_errors;
local_decls m_local_decls; local_decls m_local_decls;
unsigned m_num_local_decls; unsigned m_num_local_decls;
context m_context;
builtins m_builtins; builtins m_builtins;
expr_pos_info m_expr_pos_info; expr_pos_info m_expr_pos_info;
pos_info m_last_cmd_pos; pos_info m_last_cmd_pos;
@ -143,16 +142,13 @@ class parser::imp {
imp & m_fn; imp & m_fn;
local_decls::mk_scope m_scope; local_decls::mk_scope m_scope;
unsigned m_old_num_local_decls; unsigned m_old_num_local_decls;
context m_old_context;
mk_scope(imp & fn): mk_scope(imp & fn):
m_fn(fn), m_fn(fn),
m_scope(fn.m_local_decls), m_scope(fn.m_local_decls),
m_old_num_local_decls(fn.m_num_local_decls), m_old_num_local_decls(fn.m_num_local_decls) {
m_old_context(fn.m_context) {
} }
~mk_scope() { ~mk_scope() {
m_fn.m_num_local_decls = m_old_num_local_decls; m_fn.m_num_local_decls = m_old_num_local_decls;
m_fn.m_context = m_old_context;
} }
}; };
@ -661,7 +657,7 @@ class parser::imp {
auto p = pos(); auto p = pos();
next(); next();
mk_scope scope(*this); mk_scope scope(*this);
register_binding(g_unused, expr()); register_binding(g_unused);
// The -1 is a trick to get right associativity in Pratt's parsers // The -1 is a trick to get right associativity in Pratt's parsers
expr right = parse_expr(g_arrow_precedence-1); expr right = parse_expr(g_arrow_precedence-1);
return save(mk_arrow(left, right), p); return save(mk_arrow(left, right), p);
@ -688,12 +684,8 @@ class parser::imp {
} }
/** \brief Register the name \c n as a local declaration. */ /** \brief Register the name \c n as a local declaration. */
void register_binding(name const & n, expr const & type, expr const & val = expr()) { void register_binding(name const & n) {
unsigned lvl = m_num_local_decls; unsigned lvl = m_num_local_decls;
if (val)
m_context = extend(m_context, n, expr(), val);
else
m_context = extend(m_context, n, type);
m_local_decls.insert(n, lvl); m_local_decls.insert(n, lvl);
m_num_local_decls++; m_num_local_decls++;
lean_assert(m_local_decls.find(n)->second == lvl); lean_assert(m_local_decls.find(n)->second == lvl);
@ -710,7 +702,7 @@ class parser::imp {
unsigned sz = result.size(); unsigned sz = result.size();
result.resize(sz + names.size()); result.resize(sz + names.size());
expr type = parse_expr(); expr type = parse_expr();
for (std::pair<pos_info, name> const & n : names) register_binding(n.second, type); for (std::pair<pos_info, name> const & n : names) register_binding(n.second);
unsigned i = names.size(); unsigned i = names.size();
while (i > 0) { while (i > 0) {
--i; --i;
@ -834,7 +826,7 @@ class parser::imp {
name id = check_identifier_next("invalid let expression, identifier expected"); name id = check_identifier_next("invalid let expression, identifier expected");
check_assign_next("invalid let expression, ':=' expected"); check_assign_next("invalid let expression, ':=' expected");
expr val = parse_expr(); expr val = parse_expr();
register_binding(id, expr(), val); register_binding(id);
bindings.push_back(std::make_tuple(p, id, val)); bindings.push_back(std::make_tuple(p, id, val));
if (curr_is_in()) { if (curr_is_in()) {
next(); next();
@ -881,7 +873,7 @@ class parser::imp {
/** \brief Create a fresh metavariable. */ /** \brief Create a fresh metavariable. */
expr mk_metavar() { expr mk_metavar() {
return m_elaborator.mk_metavar(m_context); return m_elaborator.mk_metavar(m_num_local_decls);
} }
/** \brief Parse \c _ a hole that must be filled by the elaborator. */ /** \brief Parse \c _ a hole that must be filled by the elaborator. */

2
src/library/elaborator.h
View file

@ -30,7 +30,7 @@ public:
metavar_env & menv() { return m_metaenv; } metavar_env & menv() { return m_metaenv; }
void clear() { m_metaenv.clear(); } void clear() { m_metaenv.clear(); }
expr mk_metavar(context const & ctx) { return m_metaenv.mk_metavar(ctx); } expr mk_metavar(unsigned ctx_sz) { return m_metaenv.mk_metavar(ctx_sz); }
void set_interrupt(bool flag) { m_metaenv.set_interrupt(flag); } void set_interrupt(bool flag) { m_metaenv.set_interrupt(flag); }
void interrupt() { set_interrupt(true); } void interrupt() { set_interrupt(true); }

288
src/library/metavar_env.cpp
View file

@ -48,9 +48,24 @@ bool has_metavar(expr const & e) {
} }
} }
metavar_env::cell::cell(expr const & e, context const & ctx, unsigned find): /** \brief Return true iff \c e contains a metavariable with index midx */
bool has_metavar(expr const & e, unsigned midx) {
auto f = [=](expr const & m, unsigned offset) {
if (is_metavar(m) && metavar_idx(m) == midx)
throw found_metavar();
};
try {
for_each_fn<decltype(f)> proc(f);
proc(e);
return false;
} catch (found_metavar) {
return true;
}
}
metavar_env::cell::cell(expr const & e, unsigned ctx_size, unsigned find):
m_expr(e), m_expr(e),
m_context(ctx), m_ctx_size(ctx_size),
m_find(find), m_find(find),
m_rank(0), m_rank(0),
m_state(state::Unprocessed) { m_state(state::Unprocessed) {
@ -100,85 +115,6 @@ unsigned metavar_env::new_rank(unsigned r1, unsigned r2) {
else return std::max(r1, r2); else return std::max(r1, r2);
} }
/**
\brief Assign m <- s, where s is a term.
\pre s contains only unassigned metavariables.
The contexts of the unassigned metavariables occurring in s are
shortened to the length of the context associated with m.
The assignment is valid if:
1) \c s does contain free variables outside of the context
associated with m.
2) \c s does not contain m.
3) The context of every metavariable in s is unifiable with the
context of m.
*/
void metavar_env::assign_term(expr const & m, expr s, context const & ctx) {
lean_assert(is_metavar(m));
lean_assert(!is_assigned(m));
lean_assert(!is_metavar(s));
cell & mc = root_cell(m);
unsigned len_mc = length(mc.m_context);
unsigned len_ctx = length(ctx);
if (len_ctx < len_mc) {
// mc is used in a context with len_mc variables,
// but s free variables are references to a smaller context.
// So, we must lift s free variables.
s = lift_free_vars(s, len_mc - len_ctx);
} else if (len_ctx > len_mc) {
// s must only contain free variables that are available in mc.m_context
if (has_free_var(s, 0, len_ctx - len_mc))
failed_to_unify();
s = lower_free_vars(s, len_ctx - len_mc);
}
unsigned fv_range = 0;
auto proc = [&](expr const & n, unsigned offset) {
if (is_var(n)) {
unsigned vidx = var_idx(n);
if (vidx >= offset) {
unsigned fv_idx = vidx - offset;
fv_range = std::max(fv_range, fv_idx+1);
}
} else if (is_metavar(n)) {
// Remark: before performing an assignment, we
// instantiate all assigned metavariables in s.
lean_assert(!is_assigned(n));
cell & nc = root_cell(n);
if (mc.m_find == nc.m_find)
failed_to_unify(); // cycle detected
unsigned len_nc = length(nc.m_context);
// make sure nc is not bigger than mc
while (len_nc > len_mc) { nc.m_context = cdr(nc.m_context); len_nc--; }
// Remark: By property 2 of metavariable contexts, we
// know that m can't occur in the reduced
// nc.m_context.
//
// Property 2: If a metavariable ?m1 occurs in context ctx2 of
// metavariable ?m2, then context ctx1 of ?m1 must be a prefix of ctx2.
//
// make sure nc that prefix of mc
unify_ctx_prefix(nc.m_context, mc.m_context);
fv_range = std::max(fv_range, len_nc);
}
};
for_each_fn<decltype(proc)> visitor(proc);
visitor(s);
if (fv_range > length(mc.m_context)) {
// s has a free variable that is not in the context of mc
failed_to_unify();
}
mc.m_expr = s;
}
[[noreturn]] void metavar_env::failed_to_unify() { [[noreturn]] void metavar_env::failed_to_unify() {
throw exception("failed to unify"); throw exception("failed to unify");
} }
@ -199,11 +135,11 @@ metavar_env::metavar_env(environment const & env, name_set const * available_def
metavar_env::metavar_env(environment const & env):metavar_env(env, nullptr) { metavar_env::metavar_env(environment const & env):metavar_env(env, nullptr) {
} }
expr metavar_env::mk_metavar(context const & ctx) { expr metavar_env::mk_metavar(unsigned ctx_sz) {
m_modified = true; m_modified = true;
unsigned vidx = m_cells.size(); unsigned vidx = m_cells.size();
expr m = ::lean::mk_metavar(vidx); expr m = ::lean::mk_metavar(vidx);
m_cells.push_back(cell(m, ctx, vidx)); m_cells.push_back(cell(m, ctx_sz, vidx));
return m; return m;
} }
@ -217,20 +153,34 @@ expr metavar_env::root_at(expr const & e, unsigned ctx_size) const {
if (is_metavar(c.m_expr)) { if (is_metavar(c.m_expr)) {
return c.m_expr; return c.m_expr;
} else { } else {
unsigned len_c = length(c.m_context); lean_assert(c.m_ctx_size <= ctx_size);
lean_assert(len_c <= ctx_size); return lift_free_vars(c.m_expr, ctx_size - c.m_ctx_size);
if (len_c < ctx_size) {
return lift_free_vars(c.m_expr, ctx_size - len_c);
} else {
return c.m_expr;
}
} }
} else { } else {
return e; return e;
} }
} }
void metavar_env::assign(expr const & m, expr const & s, context const & ctx) { /**
\brief Make sure that the metavariables in \c s can only access
ctx_size free variables.
\pre s does not contain assigned metavariables.
*/
void metavar_env::reduce_metavars_ctx_size(expr const & s, unsigned ctx_size) {
auto proc = [&](expr const & m, unsigned offset) {
if (is_metavar(m)) {
lean_assert(!is_assigned(m));
cell & mc = root_cell(m);
if (mc.m_ctx_size > ctx_size + offset)
mc.m_ctx_size = ctx_size + offset;
}
};
for_each_fn<decltype(proc)> visitor(proc);
visitor(s);
}
void metavar_env::assign(expr const & m, expr const & s, unsigned ctx_size) {
lean_assert(is_metavar(m)); lean_assert(is_metavar(m));
lean_assert(!is_assigned(m)); lean_assert(!is_assigned(m));
if (m == s) if (m == s)
@ -239,14 +189,15 @@ void metavar_env::assign(expr const & m, expr const & s, context const & ctx) {
cell & mc = root_cell(m); cell & mc = root_cell(m);
lean_assert(is_metavar(mc.m_expr)); lean_assert(is_metavar(mc.m_expr));
lean_assert(metavar_idx(mc.m_expr) == mc.m_find); lean_assert(metavar_idx(mc.m_expr) == mc.m_find);
expr _s = instantiate_metavars(s, length(ctx)); expr _s = instantiate_metavars(s, ctx_size);
if (is_metavar(_s)) { if (is_metavar(_s)) {
// both are unassigned meta-variables... // both are unassigned meta-variables...
lean_assert(!is_assigned(_s)); lean_assert(!is_assigned(_s));
cell & sc = root_cell(_s); cell & sc = root_cell(_s);
lean_assert(is_metavar(sc.m_expr)); lean_assert(is_metavar(sc.m_expr));
ensure_same_length(mc.m_context, sc.m_context); unsigned new_ctx_sz = std::min(mc.m_ctx_size, sc.m_ctx_size);
unify_ctx_entries(mc.m_context, sc.m_context); mc.m_ctx_size = new_ctx_sz;
sc.m_ctx_size = new_ctx_sz;
if (mc.m_rank > sc.m_rank) { if (mc.m_rank > sc.m_rank) {
// we want to make mc the root of the equivalence class. // we want to make mc the root of the equivalence class.
mc.m_rank = new_rank(mc.m_rank, sc.m_rank); mc.m_rank = new_rank(mc.m_rank, sc.m_rank);
@ -257,9 +208,26 @@ void metavar_env::assign(expr const & m, expr const & s, context const & ctx) {
mc.m_find = sc.m_find; mc.m_find = sc.m_find;
} }
} else { } else {
assign_term(m, _s, ctx); lean_assert(!is_metavar(_s));
if (has_metavar(_s, mc.m_find)) {
failed_to_unify();
}
reduce_metavars_ctx_size(_s, mc.m_ctx_size);
if (ctx_size < mc.m_ctx_size) {
// mc is used in a context with more free variables.
// but s free variables are references to a smaller context.
// So, we must lift _s free variables.
_s = lift_free_vars(_s, mc.m_ctx_size - ctx_size);
} else if (ctx_size > mc.m_ctx_size) {
// _s must only contain free variables that are available
// in the context of mc
if (has_free_var(_s, 0, ctx_size - mc.m_ctx_size)) {
failed_to_unify();
}
_s = lower_free_vars(_s, ctx_size - mc.m_ctx_size);
}
mc.m_expr = _s;
} }
lean_assert(check_invariant());
} }
expr metavar_env::instantiate_metavars(expr const & e, unsigned outer_offset) { expr metavar_env::instantiate_metavars(expr const & e, unsigned outer_offset) {
@ -272,20 +240,16 @@ expr metavar_env::instantiate_metavars(expr const & e, unsigned outer_offset) {
return rc.m_expr; return rc.m_expr;
} else { } else {
switch (rc.m_state) { switch (rc.m_state) {
case state::Unprocessed: { case state::Unprocessed:
rc.m_state = state::Processing; rc.m_state = state::Processing;
unsigned rc_len = length(rc.m_context); rc.m_expr = instantiate_metavars(rc.m_expr, rc.m_ctx_size);
rc.m_expr = instantiate_metavars(rc.m_expr, rc_len);
rc.m_state = state::Processed; rc.m_state = state::Processed;
lean_assert(rc_len <= offset + outer_offset); lean_assert(rc.m_ctx_size <= offset + outer_offset);
return lift_free_vars(rc.m_expr, offset + outer_offset - rc_len); return lift_free_vars(rc.m_expr, offset + outer_offset - rc.m_ctx_size);
}
case state::Processing: throw exception("cycle detected"); case state::Processing: throw exception("cycle detected");
case state::Processed: { case state::Processed:
unsigned rc_len = length(rc.m_context); lean_assert(rc.m_ctx_size <= offset + outer_offset);
lean_assert(rc_len <= offset + outer_offset); return lift_free_vars(rc.m_expr, offset + outer_offset - rc.m_ctx_size);
return lift_free_vars(rc.m_expr, offset + outer_offset - rc_len);
}
} }
} }
} }
@ -316,73 +280,6 @@ expr const & metavar_env::get_definition(expr const & e) {
return m_env.find_object(const_name(e)).get_value(); return m_env.find_object(const_name(e)).get_value();
} }
/**
\brief Ensure both contexts have the same length
*/
void metavar_env::ensure_same_length(context & ctx1, context & ctx2) {
if (is_eqp(ctx1, ctx2)) {
return;
} else {
unsigned len1 = length(ctx1);
unsigned len2 = length(ctx2);
unsigned new_len = std::min(len1, len2);
while (len1 > new_len) { ctx1 = cdr(ctx1); --len1; }
while (len2 > new_len) { ctx2 = cdr(ctx2); --len2; }
}
}
/**
\brief Check if ctx1 is a prefix of ctx2. That is,
1- length(ctx1) <= length(ctx2)
2- Every entry in ctxt1 is unifiable with the corresponding
entry in ctx2.
*/
void metavar_env::unify_ctx_prefix(context const & ctx1, context const & ctx2) {
if (is_eqp(ctx1, ctx2)) {
return;
} else {
unsigned len1 = length(ctx1);
unsigned len2 = length(ctx2);
if (len1 > len2)
failed_to_unify();
context _ctx2 = ctx2;
while (len2 > len1) { _ctx2 = cdr(_ctx2); --len2; }
unify_ctx_entries(ctx1, _ctx2);
}
}
/**
\brief Unify the context entries of the given contexts.
\pre length(ctx1) == length(ctx2)
*/
void metavar_env::unify_ctx_entries(context const & ctx1, context const & ctx2) {
lean_assert(length(ctx1) == length(ctx2));
auto it1 = ctx1.begin();
auto end1 = ctx1.end();
auto it2 = ctx2.begin();
for (; it1 != end1; ++it1, ++it2) {
context_entry const & e1 = *it1;
context_entry const & e2 = *it2;
if ((e1.get_domain()) && (e2.get_domain())) {
unify(e1.get_domain(), e2.get_domain());
} else if (!(e1.get_domain()) && !(e2.get_domain())) {
// do nothing
} else {
failed_to_unify();
}
if ((e1.get_body()) && (e2.get_body())) {
unify(e1.get_body(), e2.get_body());
} else if (!(e1.get_body()) && !(e2.get_body())) {
// do nothing
} else {
failed_to_unify();
}
}
}
// Little hack for matching (?m #0) with t // Little hack for matching (?m #0) with t
// TODO: implement some support for higher order unification. // TODO: implement some support for higher order unification.
bool metavar_env::is_simple_ho_match(expr const & e1, expr const & e2, context const & ctx) { bool metavar_env::is_simple_ho_match(expr const & e1, expr const & e2, context const & ctx) {
@ -395,15 +292,15 @@ bool metavar_env::is_simple_ho_match(expr const & e1, expr const & e2, context c
// Little hack for matching (?m #0) with t // Little hack for matching (?m #0) with t
// TODO: implement some support for higher order unification. // TODO: implement some support for higher order unification.
void metavar_env::unify_simple_ho_match(expr const & e1, expr const & e2, context const & ctx) { void metavar_env::unify_simple_ho_match(expr const & e1, expr const & e2, unsigned ctx_size, context const & ctx) {
unify(arg(e1,0), mk_lambda(car(ctx).get_name(), car(ctx).get_domain(), e2), ctx); unify(arg(e1,0), mk_lambda(car(ctx).get_name(), car(ctx).get_domain(), e2), ctx_size, ctx);
} }
/** /**
\brief Auxiliary function for unifying expressions \c e1 and \brief Auxiliary function for unifying expressions \c e1 and
\c e2 when none of them are metavariables. \c e2 when none of them are metavariables.
*/ */
void metavar_env::unify_core(expr const & e1, expr const & e2, context const & ctx) { void metavar_env::unify_core(expr const & e1, expr const & e2, unsigned ctx_size, context const & ctx) {
check_interrupted(m_interrupted); check_interrupted(m_interrupted);
lean_assert(!is_metavar(e1)); lean_assert(!is_metavar(e1));
lean_assert(!is_metavar(e2)); lean_assert(!is_metavar(e2));
@ -412,51 +309,51 @@ void metavar_env::unify_core(expr const & e1, expr const & e2, context const & c
} else if (is_type(e1) && is_type(e2)) { } else if (is_type(e1) && is_type(e2)) {
return; // ignoring type universe levels. We let the kernel check that return; // ignoring type universe levels. We let the kernel check that
} else if (is_abstraction(e1) && is_abstraction(e2)) { } else if (is_abstraction(e1) && is_abstraction(e2)) {
unify(abst_domain(e1), abst_domain(e2), ctx); unify(abst_domain(e1), abst_domain(e2), ctx_size, ctx);
unify(abst_body(e1), abst_body(e2), extend(ctx, abst_name(e1), abst_domain(e1))); unify(abst_body(e1), abst_body(e2), ctx_size+1, extend(ctx, abst_name(e1), abst_domain(e1)));
} else if (is_eq(e1) && is_eq(e2)) { } else if (is_eq(e1) && is_eq(e2)) {
unify(eq_lhs(e1), eq_lhs(e2), ctx); unify(eq_lhs(e1), eq_lhs(e2), ctx_size, ctx);
unify(eq_rhs(e1), eq_rhs(e2), ctx); unify(eq_rhs(e1), eq_rhs(e2), ctx_size, ctx);
} else { } else {
expr r1 = head_reduce(e1, m_env, m_available_definitions); expr r1 = head_reduce(e1, m_env, m_available_definitions);
expr r2 = head_reduce(e2, m_env, m_available_definitions); expr r2 = head_reduce(e2, m_env, m_available_definitions);
if (!is_eqp(e1, r1) || !is_eqp(e2, r2)) { if (!is_eqp(e1, r1) || !is_eqp(e2, r2)) {
return unify(r1, r2, ctx); return unify(r1, r2, ctx_size, ctx);
} else if (is_app(e1) && is_app(e2) && num_args(e1) == num_args(e2)) { } else if (is_app(e1) && is_app(e2) && num_args(e1) == num_args(e2)) {
unsigned num = num_args(e1); unsigned num = num_args(e1);
for (unsigned i = 0; i < num; i++) { for (unsigned i = 0; i < num; i++) {
unify(arg(e1, i), arg(e2, i), ctx); unify(arg(e1, i), arg(e2, i), ctx_size, ctx);
} }
} else if (is_simple_ho_match(e1, e2, ctx)) { } else if (is_simple_ho_match(e1, e2, ctx)) {
unify_simple_ho_match(e1, e2, ctx); unify_simple_ho_match(e1, e2, ctx_size, ctx);
} else if (is_simple_ho_match(e2, e1, ctx)) { } else if (is_simple_ho_match(e2, e1, ctx)) {
unify_simple_ho_match(e2, e1, ctx); unify_simple_ho_match(e2, e1, ctx_size, ctx);
} else { } else {
failed_to_unify(); failed_to_unify();
} }
} }
} }
void metavar_env::unify(expr const & e1, expr const & e2, context const & ctx) { void metavar_env::unify(expr const & e1, expr const & e2, unsigned ctx_size, context const & ctx) {
lean_assert(ctx_size == length(ctx));
flet<unsigned> l(m_depth, m_depth+1); flet<unsigned> l(m_depth, m_depth+1);
if (m_depth > m_max_depth) if (m_depth > m_max_depth)
throw exception("unifier maximum recursion depth exceeded"); throw exception("unifier maximum recursion depth exceeded");
expr const & r1 = root_at(e1, ctx); expr const & r1 = root_at(e1, ctx_size);
expr const & r2 = root_at(e2, ctx); expr const & r2 = root_at(e2, ctx_size);
if (is_metavar(r1)) { if (is_metavar(r1)) {
assign(r1, r2, ctx); assign(r1, r2, ctx_size);
} else { } else {
if (is_metavar(r2)) { if (is_metavar(r2)) {
assign(r2, r1, ctx); assign(r2, r1, ctx_size);
} else { } else {
unify_core(r1, r2, ctx); unify_core(r1, r2, ctx_size, ctx);
} }
} }
} }
context const & metavar_env::get_context(expr const & m) { void metavar_env::unify(expr const & e1, expr const & e2, context const & ctx) {
lean_assert(is_metavar(m)); unify(e1, e2, length(ctx), ctx);
return root_cell(m).m_context;
} }
void metavar_env::set_interrupt(bool flag) { void metavar_env::set_interrupt(bool flag) {
@ -477,8 +374,7 @@ void metavar_env::display(std::ostream & out) const {
out << c.m_expr; out << c.m_expr;
else else
out << "[unassigned]"; out << "[unassigned]";
if (c.m_context) out << ", ctx_sz: " << c.m_ctx_size;
out << ", " << c.m_context;
out << "\n"; out << "\n";
} }
} }

67
src/library/metavar_env.h
View file

@ -33,25 +33,11 @@ class metavar_env {
enum class state { Unprocessed, Processing, Processed }; enum class state { Unprocessed, Processing, Processed };
struct cell { struct cell {
expr m_expr; expr m_expr;
context m_context; unsigned m_ctx_size; // size of the context where the metavariable is defined
unsigned m_find; unsigned m_find;
unsigned m_rank; unsigned m_rank;
state m_state; state m_state;
cell(expr const & e, context const & ctx, unsigned find); cell(expr const & e, unsigned ctx_size, unsigned find);
/*
Basic properties for metavariable contexts:
1) A metavariable does not occur in its own context.
2) If a metavariable ?m1 occurs in context ctx2 of
metavariable ?m2, then context ctx1 of ?m1 must be a prefix of ctx2.
This is by construction.
Here is an example:
(fun (A : Type) (?m1 : A) (?m2 : B), C)
The context of ?m1 is [A : Type]
The context of ?m2 is [A : Type, ?m1 : A]
Remark: these conditions are not enforced by this module.
*/
}; };
environment const & m_env; environment const & m_env;
std::vector<cell> m_cells; std::vector<cell> m_cells;
@ -70,22 +56,20 @@ class metavar_env {
cell & root_cell(expr const & m); cell & root_cell(expr const & m);
cell const & root_cell(expr const & m) const; cell const & root_cell(expr const & m) const;
unsigned new_rank(unsigned r1, unsigned r2); unsigned new_rank(unsigned r1, unsigned r2);
void assign_term(expr const & m, expr s, context const & ctx);
[[noreturn]] void failed_to_unify(); [[noreturn]] void failed_to_unify();
void ensure_same_length(context & ctx1, context & ctx2);
void unify_ctx_prefix(context const & ctx1, context const & ctx2);
void unify_ctx_entries(context const & ctx1, context const & ctx2);
bool is_simple_ho_match(expr const & e1, expr const & e2, context const & ctx); bool is_simple_ho_match(expr const & e1, expr const & e2, context const & ctx);
void unify_simple_ho_match(expr const & e1, expr const & e2, context const & ctx); void unify_simple_ho_match(expr const & e1, expr const & e2, unsigned ctx_size, context const & ctx);
void unify_core(expr const & e1, expr const & e2, context const & ctx); void unify_core(expr const & e1, expr const & e2, unsigned ctx_size, context const & ctx);
void reduce_metavars_ctx_size(expr const & s, unsigned ctx_size);
void unify(expr const & e1, expr const & e2, unsigned ctx_size, context const & ctx);
public: public:
metavar_env(environment const & env, name_set const * available_defs, unsigned max_depth); metavar_env(environment const & env, name_set const * available_defs, unsigned max_depth);
metavar_env(environment const & env, name_set const * available_defs); metavar_env(environment const & env, name_set const * available_defs);
metavar_env(environment const & env); metavar_env(environment const & env);
/** \brief Create a new meta-variable with the given context. */ /** \brief Create a new meta-variable for a context of size ctx_sz. */
expr mk_metavar(context const & ctx = context()); expr mk_metavar(unsigned ctx_sz = 0);
/** /**
\brief Return true iff the given metavariable representative is \brief Return true iff the given metavariable representative is
@ -102,28 +86,30 @@ public:
If the the metavariable was defined in smaller context, we lift the If the the metavariable was defined in smaller context, we lift the
free variables to match the size of the given context. free variables to match the size of the given context.
*/ */
expr root_at(expr const & m, context const & ctx) const { return root_at(m, length(ctx)); }
/**
\brief Similar to the previous function, but the context is given.
*/
expr root_at(expr const & m, unsigned ctx_size) const; expr root_at(expr const & m, unsigned ctx_size) const;
expr root_at(expr const & m, context const & ctx) const {
/** return root_at(m, length(ctx));
\brief If the given expression is a metavariable, then return the root }
of the equivalence class. Otherwise, return itself.
*/
// expr const & root(expr const & e) const
/** /**
\brief Assign m <- s \brief Assign m <- s
\remark s is a term that occurs in a context of size \c
ctx_size. We need this information to adjust \c s to the
metavariable \c m, since \c m maybe was created in context of
different size, or was unified with another metavariable
created in a smaller context.
\pre is_metavar(m)
*/ */
void assign(expr const & m, expr const & s, context const & ctx = context()); void assign(expr const & m, expr const & s, unsigned ctx_size);
/** /**
\brief Replace the metavariables occurring in \c e with the \brief Replace the metavariables occurring in \c e with the
substitutions in this metaenvironment. substitutions in this metaenvironment.
*/ */
expr instantiate_metavars(expr const & e, unsigned outer_offset = 0); expr instantiate_metavars(expr const & e, unsigned ctx_size = 0);
/** /**
\brief Return true iff the given expression is an available \brief Return true iff the given expression is an available
@ -145,14 +131,6 @@ public:
*/ */
void unify(expr const & e1, expr const & e2, context const & ctx = context()); void unify(expr const & e1, expr const & e2, context const & ctx = context());
/**
\brief Return the context associated with the given
meta-variable.
\pre is_metavar(m)
*/
context const & get_context(expr const & m);
/** /**
\brief Clear/Reset the state. \brief Clear/Reset the state.
*/ */
@ -164,7 +142,6 @@ public:
void set_interrupt(bool flag); void set_interrupt(bool flag);
void display(std::ostream & out) const; void display(std::ostream & out) const;
bool check_invariant() const; bool check_invariant() const;
}; };
} }

263
src/tests/library/implicit_args.cpp
View file

@ -44,7 +44,7 @@ static expr replace(expr const & e, context const & ctx, metavar_env & menv) {
switch (e.kind()) { switch (e.kind()) {
case expr_kind::Constant: case expr_kind::Constant:
if (is_placeholder(e)) { if (is_placeholder(e)) {
return menv.mk_metavar(ctx); return menv.mk_metavar(length(ctx));
} else { } else {
return e; return e;
} }
@ -85,221 +85,6 @@ expr elaborate(expr const & e, environment const & env) {
return elb(new_e); return elb(new_e);
} }
static void tst1() {
expr m1 = mk_metavar(0);
expr m2 = mk_metavar(1);
expr a = Const("a");
expr f = Const("f");
lean_assert(is_metavar(m1));
lean_assert(!is_metavar(a));
lean_assert(metavar_idx(m1) == 0);
lean_assert(metavar_idx(m2) == 1);
lean_assert(m1 != m2);
lean_assert(a != m1);
std::cout << m1 << " " << m2 << "\n";
lean_assert(has_metavar(m1));
lean_assert(has_metavar(f(f(f(m1)))));
lean_assert(!has_metavar(f(f(a))));
}
static void tst2() {
environment env;
metavar_env u(env);
expr m1 = u.mk_metavar();
expr m2 = u.mk_metavar();
expr m3 = u.mk_metavar();
lean_assert(!u.is_assigned(m1));
lean_assert(!u.is_assigned(m2));
lean_assert(!u.is_assigned(m3));
expr f = Const("f");
expr t1 = f(m1, m2);
expr t2 = f(m1, m1);
lean_assert(t1 != t2);
// m1 <- m2
u.assign(m1, m2);
std::cout << u << "\n";
lean_assert(u.root_at(m2, 0) == m2);
lean_assert(u.root_at(m1, 0) == m2);
expr a = Const("a");
expr b = Const("b");
expr g = Const("g");
expr t3 = f(a, m1);
expr t4 = f(m2, a);
expr t5 = f(a, a);
lean_assert(t3 != t4);
lean_assert(t4 != t5);
u.assign(m2, a);
u.assign(m3, b);
std::cout << u << "\n";
expr m4 = u.mk_metavar();
std::cout << u << "\n";
u.assign(m4, m1);
std::cout << u << "\n";
expr m5 = u.mk_metavar();
expr m6 = u.mk_metavar();
u.assign(m5, m6);
metavar_env u2(u);
u.assign(m5, m3);
std::cout << u << "\n";
u2.assign(m5, m2);
std::cout << u2 << "\n";
}
static void tst3() {
environment env;
metavar_env uenv(env);
expr m1 = uenv.mk_metavar();
expr f = Const("f");
expr a = Const("a");
expr b = Const("b");
expr g = Const("g");
expr m2 = uenv.mk_metavar();
uenv.assign(m2, f(m1, a));
uenv.assign(m1, b);
std::cout << uenv.instantiate_metavars(g(m2,b)) << "\n";
lean_assert(uenv.instantiate_metavars(g(m2,b)) == g(f(b,a), b));
lean_assert(uenv.instantiate_metavars(g(m2,f(a,m1))) == g(f(b,a),f(a,b)));
expr m3 = uenv.mk_metavar();
expr m4 = uenv.mk_metavar();
uenv.assign(m3, f(m4));
try {
uenv.assign(m4, f(m3));
lean_unreachable();
} catch (exception) {
}
}
static void tst4() {
environment env;
metavar_env uenv(env);
expr m1 = uenv.mk_metavar();
expr m2 = uenv.mk_metavar();
uenv.assign(m1, m2);
expr f = Const("f");
expr a = Const("a");
expr t = uenv.instantiate_metavars(f(m1,f(a, m1)));
std::cout << t << "\n";
lean_assert(t == f(m2, f(a, m2)));
}
static void tst5() {
environment env;
env.add_var("A", Type());
env.add_var("B", Type());
expr A = Const("A");
expr B = Const("B");
env.add_definition("F", Type(), A >> B);
env.add_definition("G", Type(), B >> B);
metavar_env uenv(env);
expr m1 = uenv.mk_metavar();
expr m2 = uenv.mk_metavar();
expr m3 = uenv.mk_metavar();
expr m4 = uenv.mk_metavar();
expr F = Const("F");
expr G = Const("G");
expr f = Const("f");
expr g = Const("g");
expr a = Const("a");
expr b = Const("b");
expr x = Const("x");
expr Id = Fun({x, A}, x);
expr t1 = f(m1, g(a, F));
expr t2 = f(g(a, b), Id(g(m2, m3 >> m4)));
metavar_env uenv2(uenv);
uenv2.unify(t1, t2);
std::cout << uenv2 << "\n";
lean_assert(uenv2.root_at(m1,0) == g(a, b));
lean_assert(uenv2.root_at(m2,0) == a);
lean_assert(uenv2.root_at(m3,0) == A);
lean_assert(uenv2.root_at(m4,0) == B);
lean_assert(uenv2.instantiate_metavars(t1) == f(g(a, b), g(a, F)));
lean_assert(uenv2.instantiate_metavars(t2) == f(g(a, b), Id(g(a, A >> B))));
metavar_env uenv3(uenv);
expr t3 = f(m1, m1 >> m1);
expr t4 = f(m2 >> m2, m3);
uenv3.unify(t3, t4);
std::cout << uenv3 << "\n";
uenv3.unify(m1, G);
std::cout << uenv3 << "\n";
std::cout << uenv3.instantiate_metavars(t3) << "\n";
}
static void tst6() {
environment env;
env.add_var("A", Type());
expr A = Const("A");
expr f = Const("f");
expr g = Const("g");
expr a = Const("a");
expr b = Const("b");
context ctx1;
ctx1 = extend(extend(ctx1, "x", A >> A), "y", A);
metavar_env uenv(env);
expr m1 = uenv.mk_metavar();
expr m2 = uenv.mk_metavar(ctx1);
context ctx2;
ctx2 = extend(ctx2, "x", m1);
expr m3 = uenv.mk_metavar(ctx2);
metavar_env uenv2(uenv);
expr t1 = f(m2, m3);
expr t2 = f(g(m3), Var(0));
std::cout << "----------------\n";
std::cout << uenv << "\n";
uenv.unify(t1, t2, ctx2);
std::cout << uenv << "\n";
std::cout << uenv.instantiate_metavars(t1,2) << "\n";
std::cout << uenv.instantiate_metavars(t2,1) << "\n";
lean_assert(uenv.instantiate_metavars(t1,2) == lift_free_vars(uenv.instantiate_metavars(t2,1),1));
lean_assert(uenv.instantiate_metavars(t2,1) == f(g(Var(0)),Var(0)));
lean_assert(uenv.instantiate_metavars(m1) == A >> A);
expr t3 = f(m2);
expr t4 = f(m3);
uenv2.unify(t3, t4);
std::cout << "----------------\n";
std::cout << uenv2 << "\n";
lean_assert(uenv2.instantiate_metavars(m1) == A >> A);
lean_assert(length(uenv2.get_context(m2)) == length(uenv2.get_context(m3)));
}
static void tst7() {
environment env;
env.add_var("A", Type());
env.add_var("B", Type());
expr A = Const("A");
expr B = Const("B");
env.add_definition("F", Type(), A >> B);
env.add_definition("G", Type(), B >> B);
name_set S;
S.insert("G");
metavar_env uenv(env, &S);
expr m1 = uenv.mk_metavar();
expr m2 = uenv.mk_metavar();
expr m3 = uenv.mk_metavar();
expr m4 = uenv.mk_metavar();
expr F = Const("F");
expr G = Const("G");
expr f = Const("f");
expr g = Const("g");
expr a = Const("a");
expr b = Const("b");
expr x = Const("x");
expr Id = Fun({x, A}, x);
expr t1 = f(m1, g(a, F));
expr t2 = f(g(a, b), Id(g(m2, m3 >> m4)));
metavar_env uenv2(uenv);
try {
uenv2.unify(t1, t2);
lean_unreachable();
} catch (exception) {
// It failed because "F" is not in the set of
// available definitions.
}
S.insert("F");
uenv.unify(t1, t2);
std::cout << uenv.instantiate_metavars(t1) << "\n";
std::cout << uenv.instantiate_metavars(t2) << "\n";
}
// Check elaborator success // Check elaborator success
static void success(expr const & e, expr const & expected, environment const & env) { static void success(expr const & e, expr const & expected, environment const & env) {
std::cout << "\n" << e << "\n------>\n" << elaborate(e, env) << "\n"; std::cout << "\n" << e << "\n------>\n" << elaborate(e, env) << "\n";
@ -322,7 +107,7 @@ static void unsolved(expr const & e, environment const & env) {
lean_assert(has_metavar(elaborate(e, env))); lean_assert(has_metavar(elaborate(e, env)));
} }
static void tst8() { static void tst1() {
environment env; environment env;
expr A = Const("A"); expr A = Const("A");
expr B = Const("B"); expr B = Const("B");
@ -342,7 +127,7 @@ static void tst8() {
success(F(_,_,Fun({a, Nat},a)), F(Nat,Nat,Fun({a,Nat},a)), env); success(F(_,_,Fun({a, Nat},a)), F(Nat,Nat,Fun({a,Nat},a)), env);
} }
static void tst9() { static void tst2() {
environment env = mk_toplevel(); environment env = mk_toplevel();
expr a = Const("a"); expr a = Const("a");
expr b = Const("b"); expr b = Const("b");
@ -367,7 +152,7 @@ static void tst9() {
env); env);
} }
static void tst10() { static void tst3() {
environment env = mk_toplevel(); environment env = mk_toplevel();
expr Nat = Const("Nat"); expr Nat = Const("Nat");
env.add_var("Nat", Type()); env.add_var("Nat", Type());
@ -398,7 +183,7 @@ static void tst10() {
success(Refl(_,a), Refl(Nat,a), env); success(Refl(_,a), Refl(Nat,a), env);
} }
static void tst11() { static void tst4() {
environment env; environment env;
expr Nat = Const("Nat"); expr Nat = Const("Nat");
env.add_var("Nat", Type()); env.add_var("Nat", Type());
@ -421,7 +206,7 @@ static void tst11() {
Fun({{A,Type()},{x,Nat},{y,R >> Nat},{z,R >> Nat}}, Eq(f(x, y), f(x, z))), env); Fun({{A,Type()},{x,Nat},{y,R >> Nat},{z,R >> Nat}}, Eq(f(x, y), f(x, z))), env);
} }
static void tst12() { static void tst5() {
environment env; environment env;
expr A = Const("A"); expr A = Const("A");
expr B = Const("B"); expr B = Const("B");
@ -438,7 +223,7 @@ static void tst12() {
Fun({{a,Nat},{b,Nat}},g(f(Nat,a,b))), env); Fun({{a,Nat},{b,Nat}},g(f(Nat,a,b))), env);
} }
static void tst13() { static void tst6() {
environment env; environment env;
expr lst = Const("list"); expr lst = Const("list");
expr nil = Const("nil"); expr nil = Const("nil");
@ -458,7 +243,7 @@ static void tst13() {
Fun({a,N>>N}, f(cons(N>>N, a, cons(N>>N, a, nil(N>>N))))), env); Fun({a,N>>N}, f(cons(N>>N, a, cons(N>>N, a, nil(N>>N))))), env);
} }
static void tst14() { static void tst7() {
environment env; environment env;
expr x = Const("x"); expr x = Const("x");
expr _ = mk_placholder(); expr _ = mk_placholder();
@ -466,7 +251,7 @@ static void tst14() {
fails(omega, env); fails(omega, env);
} }
static void tst15() { static void tst8() {
environment env; environment env;
expr B = Const("B"); expr B = Const("B");
expr A = Const("A"); expr A = Const("A");
@ -474,13 +259,13 @@ static void tst15() {
expr f = Const("f"); expr f = Const("f");
expr _ = mk_placholder(); expr _ = mk_placholder();
env.add_var("f", Pi({B, Type()}, B >> B)); env.add_var("f", Pi({B, Type()}, B >> B));
success(Fun({{A,Type()}, {B,Type()}, {x,_}}, f(B, x)),
Fun({{A,Type()}, {B,Type()}, {x,B}}, f(B, x)), env);
fails(Fun({{x,_}, {A,Type()}}, f(A, x)), env); fails(Fun({{x,_}, {A,Type()}}, f(A, x)), env);
success(Fun({{A,Type()}, {x,_}}, f(A, x)), success(Fun({{A,Type()}, {x,_}}, f(A, x)),
Fun({{A,Type()}, {x,A}}, f(A, x)), env); Fun({{A,Type()}, {x,A}}, f(A, x)), env);
success(Fun({{A,Type()}, {B,Type()}, {x,_}}, f(A, x)), success(Fun({{A,Type()}, {B,Type()}, {x,_}}, f(A, x)),
Fun({{A,Type()}, {B,Type()}, {x,A}}, f(A, x)), env); Fun({{A,Type()}, {B,Type()}, {x,A}}, f(A, x)), env);
success(Fun({{A,Type()}, {B,Type()}, {x,_}}, f(B, x)),
Fun({{A,Type()}, {B,Type()}, {x,B}}, f(B, x)), env);
success(Fun({{A,Type()}, {B,Type()}, {x,_}}, Eq(f(B, x), f(_,x))), success(Fun({{A,Type()}, {B,Type()}, {x,_}}, Eq(f(B, x), f(_,x))),
Fun({{A,Type()}, {B,Type()}, {x,B}}, Eq(f(B, x), f(B,x))), env); Fun({{A,Type()}, {B,Type()}, {x,B}}, Eq(f(B, x), f(B,x))), env);
success(Fun({{A,Type()}, {B,_}, {x,_}}, Eq(f(B, x), f(_,x))), success(Fun({{A,Type()}, {B,_}, {x,_}}, Eq(f(B, x), f(_,x))),
@ -488,7 +273,7 @@ static void tst15() {
unsolved(Fun({{A,_}, {B,_}, {x,_}}, Eq(f(B, x), f(_,x))), env); unsolved(Fun({{A,_}, {B,_}, {x,_}}, Eq(f(B, x), f(_,x))), env);
} }
static void tst16() { static void tst9() {
environment env = mk_toplevel(); environment env = mk_toplevel();
expr A = Const("A"); expr A = Const("A");
expr B = Const("B"); expr B = Const("B");
@ -528,7 +313,7 @@ static void tst16() {
Fun({{x,N},{y,Bool}}, True))), env); Fun({{x,N},{y,Bool}}, True))), env);
} }
static void tst17() { static void tst10() {
environment env = mk_toplevel(); environment env = mk_toplevel();
expr A = Const("A"); expr A = Const("A");
expr B = Const("B"); expr B = Const("B");
@ -554,7 +339,7 @@ static void tst17() {
} }
static void tst18() { static void tst11() {
environment env = mk_toplevel(); environment env = mk_toplevel();
expr a = Const("a"); expr a = Const("a");
expr b = Const("b"); expr b = Const("b");
@ -590,6 +375,20 @@ static void tst18() {
env2); env2);
} }
void tst12() {
environment env;
expr A = Const("A");
expr B = Const("B");
expr a = Const("a");
expr b = Const("b");
expr eq = Const("eq");
expr _ = mk_placholder();
env.add_var("eq", Pi({A, Type(level()+1)}, A >> (A >> Bool)));
success(eq(_, Fun({{A, Type()}, {a, _}}, a), Fun({{B, Type()}, {b, B}}, b)),
eq(Pi({A, Type()}, A >> A), Fun({{A, Type()}, {a, A}}, a), Fun({{B, Type()}, {b, B}}, b)),
env);
}
int main() { int main() {
tst1(); tst1();
tst2(); tst2();
@ -603,11 +402,5 @@ int main() {
tst10(); tst10();
tst11(); tst11();
tst12(); tst12();
tst13();
tst14();
tst15();
tst16();
tst17();
tst18();
return has_violations() ? 1 : 0; return has_violations() ? 1 : 0;
} }