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

feat(kernel/metavar): is instantiate_metavars, we are also instantiating assigned metavariables that occur in the local context of unassinged ones.

Browse source 
This modification improves the effectiveness of the process_metavar_inst procedure in the Lean elaborator.

For example, suppose we have the constraint

   ctx |- ?M1[inst:0 ?M2] == a

If ?M1 and ?M2 are unassigned, then we have to consider the two possible solutions:

        ?M1 == a
    or
        ?M1 == #0 and ?M2 == a

On the other hand, if ?M2 is assigned to b, then we can ignore the second case.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-02 16:08:32 -08:00
parent ecc5d1bc3a
commit 9620b00e24
4 changed files with 70 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
src/kernel/metavar.cpp
View file

@ -303,9 +303,17 @@ bool metavar_env_cell::has_assigned_metavar(expr const & e) const {
return false;
if (!has_metavar(n))
return false;
if (is_metavar(n) && is_assigned(n)) {
result = true;
return false;
if (is_metavar(n)) {
if (is_assigned(n)) {
result = true;
return false;
}
for (auto const & entry : metavar_lctx(n)) {
if (entry.is_inst() && has_assigned_metavar(entry.v())) {
result = true;
return false;
}
}
}
return true;
});
@ -339,6 +347,7 @@ protected:
}
virtual expr visit_metavar(expr const & m, context const & ctx) {
local_context const & lctx = metavar_lctx(m);
if (is_metavar(m) && m_menv->is_assigned(m)) {
auto p = m_menv->get_subst_jst(m);
lean_assert(p);
@ -349,6 +358,17 @@ protected:
} else {
return r;
}
} else if (std::find_if(lctx.begin(), lctx.end(), [&](local_entry const & e) { return e.is_inst() && m_menv->has_assigned_metavar(e.v()); })
!= lctx.end()) {
// local context has assigned metavariables
buffer<local_entry> new_lctx;
for (auto const & e : lctx) {
if (e.is_inst())
new_lctx.push_back(mk_inst(e.s(), visit(e.v(), ctx)));
else
new_lctx.push_back(e);
}
return mk_metavar(metavar_name(m), to_list(new_lctx.begin(), new_lctx.end()));
} else {
return m;
}

44
src/library/elaborator/elaborator.cpp
View file

@ -183,15 +183,23 @@ class elaborator::imp {
push_active(c);
}
void collect_mvars(expr const & e, name_set & r) {
for_each(e, [&](expr const & m, unsigned) {
if (is_metavar(m) && !r.contains(metavar_name(m))) {
r.insert(metavar_name(m));
for (auto const & entry : metavar_lctx(m)) {
if (entry.is_inst())
collect_mvars(entry.v(), r);
}
}
return true;
});
}
/** \brief Collect metavars in \c c */
name_list collect_mvars(unification_constraint const & c) {
buffer<name> r;
auto f = [&](expr const & m, unsigned) {
if (is_metavar(m))
r.push_back(metavar_name(m));
return true;
};
for_each_fn<decltype(f)> proc(f);
name_set s;
auto proc = [&](expr const & e) { return collect_mvars(e, s); };
switch (c.kind()) {
case unification_constraint_kind::Eq:
proc(eq_lhs(c)); proc(eq_rhs(c)); break;
@ -203,10 +211,7 @@ class elaborator::imp {
lean_unreachable(); // we never delay Choice
break;
}
std::sort(r.begin(), r.end(), name_quick_cmp());
auto new_end = std::unique(r.begin(), r.end());
r.resize(r.size() + r.end() - new_end);
return to_list(r.begin(), r.end());
return s.fold([](name const & n, name_list const & l) { return cons(n, l); }, name_list());
}
/** \brief Add given constraint to the delayed list */
@ -1074,10 +1079,23 @@ class elaborator::imp {
/**
\brief Process a constraint <tt>ctx |- a == b</tt> where \c a is of the form <tt>?m[(inst:i t), ...]</tt>.
We perform a "case split",
Case 1) ?m[...] == #i and t == b
Case 1) ?m[...] == #i and t == b (for constants, variables, values and Type)
Case 2) imitate b
*/
bool process_metavar_inst(expr const & a, expr const & b, bool is_lhs, unification_constraint const & c) {
// This method is miss some cases. In particular the local context of \c a contains metavariables.
//
// (f#2 #1) == ?M2[i:1 ?M1]
//
// A possible solution for this constraint is:
// ?M2 == #1
// ?M1 == f#2 #1
//
// TODO(Leo): consider the following alternative design: We do NOT use approximations, since it is quite
// hard to understand what happened when they do not work. Instead, we rely on user provided plugins
// for handling the nasty cases.
//
// TODO(Leo): another possible design is to inform the user where approximation was used.
if (is_metavar_inst(a) && (is_eq(c) || (is_lhs && !is_actual_upper(b)) || (!is_lhs && !is_actual_lower(b)))) {
lean_assert(!is_assigned(a));
if (is_constant(b) || is_type(b) || is_value(b) || is_var(b)) {
@ -1085,7 +1103,7 @@ class elaborator::imp {
buffer<expr> solutions;
collect_metavar_solutions(lctx, b, solutions);
lean_assert(solutions.size() >= 1);
bool keep_c = local_context_has_metavar(lctx);
bool keep_c = local_context_has_metavar(metavar_lctx(a));
expr m = mk_metavar(metavar_name(a));
context ctx_m = m_state.m_menv->get_context(m);
if (solutions.size() == 1) {

8
tests/lean/bad9.lean Normal file
View file

@ -0,0 +1,8 @@
SetOption pp::implicit true.
SetOption pp::colors false.
Variable N : Type.
Check
fun (a : N) (f : N -> N) (H : f a == a),
let calc1 : f a == a := SubstP (fun x : N, f a == _) (Refl (f a)) H
in calc1.

8
tests/lean/bad9.lean.expected.out Normal file
View file

@ -0,0 +1,8 @@
Set: pp::colors
Set: pp::unicode
Set: lean::pp::implicit
Set: pp::colors
Assumed: N
λ (a : N) (f : N → N) (H : f a == a),
let calc1 : f a == a := @SubstP N (f a) a (λ x : N, f a == x) (@Refl N (f a)) H in calc1 :
Π (a : N) (f : N → N), f a == a → f a == a