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

feat(frontends/lean/elaborator): keep postponing delayed coercions until the type can be inferred

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-07 12:40:00 -07:00
parent fe448d47be
commit b956ce68d2
8 changed files with 150 additions and 58 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -502,7 +502,7 @@ public:
else
return choose(std::make_shared<class_elaborator>(*this, mvar, mvar_type, local_insts, insts, ctx, s, j));
};
add_cnstr(mk_choice_cnstr(m, choice_fn, true, j));
add_cnstr(mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::MaxDelayed), j));
}
return m;
}
@ -544,7 +544,7 @@ public:
return choose(std::make_shared<choice_expr_elaborator>(*this, mvar, e, ctx, s));
};
justification j = mk_justification("none of the overloads is applicable", some_expr(e));
add_cnstr(mk_choice_cnstr(m, fn, false, j));
add_cnstr(mk_choice_cnstr(m, fn, to_delay_factor(cnstr_group::Basic), j));
return m;
}
@ -609,6 +609,21 @@ public:
return a;
}
constraint mk_delayed_coercion_cnstr(expr const & m, expr const & a, expr const & a_type, justification const & j, unsigned delay_factor) {
auto choice_fn = [=](expr const & mvar, expr const & new_d_type, substitution const & /* s */, name_generator const & /* ngen */) {
// Remark: we want the coercions solved before we start discarding FlexFlex constraints. So, we use PreFlexFlex as a max cap
// for delaying coercions.
if (is_meta(new_d_type) && delay_factor < to_delay_factor(cnstr_group::PreFlexFlex)) {
// The type is still unknown, delay the constraint even more.
return lazy_list<constraints>(constraints(mk_delayed_coercion_cnstr(m, a, a_type, justification(), delay_factor+1)));
} else {
expr r = apply_coercion(a, a_type, new_d_type);
return lazy_list<constraints>(constraints(mk_eq_cnstr(mvar, r, justification())));
}
};
return mk_choice_cnstr(m, choice_fn, delay_factor, j);
}
/** \brief Given an application \c e, where the expected type is d_type, and the argument type is a_type,
create a "delayed coercion". The idea is to create a choice constraint and postpone the coercion
search. We do that whenever d_type or a_type is a metavar application, and d_type or a_type is a coercion source/target.
@ -616,12 +631,8 @@ public:
expr mk_delayed_coercion(expr const & e, expr const & d_type, expr const & a_type) {
expr a = app_arg(e);
expr m = mk_meta(some_expr(d_type), a.get_tag());
auto choice_fn = [=](expr const & mvar, expr const & new_d_type, substitution const & /* s */, name_generator const & /* ngen */) {
expr r = apply_coercion(a, a_type, new_d_type);
return lazy_list<constraints>(constraints(mk_eq_cnstr(mvar, r, justification())));
};
justification j = mk_app_justification(m_env, e, d_type, a_type);
add_cnstr(mk_choice_cnstr(m, choice_fn, false, j));
add_cnstr(mk_delayed_coercion_cnstr(m, a, a_type, j, to_delay_factor(cnstr_group::Basic)));
return update_app(e, app_fn(e), m);
}

18
src/kernel/constraint.cpp
View file

@ -31,10 +31,10 @@ struct level_constraint_cell : public constraint_cell {
struct choice_constraint_cell : public constraint_cell {
expr m_expr;
choice_fn m_fn;
bool m_delayed;
choice_constraint_cell(expr const & e, choice_fn const & fn, bool delayed, justification const & j):
unsigned m_delay_factor;
choice_constraint_cell(expr const & e, choice_fn const & fn, unsigned delay_factor, justification const & j):
constraint_cell(constraint_kind::Choice, j),
m_expr(e), m_fn(fn), m_delayed(delayed) {}
m_expr(e), m_fn(fn), m_delay_factor(delay_factor) {}
};
void constraint_cell::dealloc() {
@ -63,9 +63,9 @@ constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const &
constraint mk_level_eq_cnstr(level const & lhs, level const & rhs, justification const & j) {
return constraint(new level_constraint_cell(lhs, rhs, j));
}
constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, bool delayed, justification const & j) {
constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, justification const & j) {
lean_assert(is_meta(m));
return constraint(new choice_constraint_cell(m, fn, delayed, j));
return constraint(new choice_constraint_cell(m, fn, delay_factor, j));
}
expr const & cnstr_lhs_expr(constraint const & c) { lean_assert(is_eq_cnstr(c)); return static_cast<eq_constraint_cell*>(c.raw())->m_lhs; }
@ -82,8 +82,8 @@ expr const & cnstr_expr(constraint const & c) { lean_assert(is_choice_cnstr(c));
choice_fn const & cnstr_choice_fn(constraint const & c) {
lean_assert(is_choice_cnstr(c)); return static_cast<choice_constraint_cell*>(c.raw())->m_fn;
}
bool cnstr_delayed(constraint const & c) {
lean_assert(is_choice_cnstr(c)); return static_cast<choice_constraint_cell*>(c.raw())->m_delayed;
unsigned cnstr_delay_factor(constraint const & c) {
lean_assert(is_choice_cnstr(c)); return static_cast<choice_constraint_cell*>(c.raw())->m_delay_factor;
}
constraint update_justification(constraint const & c, justification const & j) {
@ -93,7 +93,7 @@ constraint update_justification(constraint const & c, justification const & j) {
case constraint_kind::LevelEq:
return mk_level_eq_cnstr(cnstr_lhs_level(c), cnstr_rhs_level(c), j);
case constraint_kind::Choice:
return mk_choice_cnstr(cnstr_expr(c), cnstr_choice_fn(c), cnstr_delayed(c), j);
return mk_choice_cnstr(cnstr_expr(c), cnstr_choice_fn(c), cnstr_delay_factor(c), j);
}
lean_unreachable(); // LCOV_EXCL_LINE
}
@ -108,7 +108,7 @@ std::ostream & operator<<(std::ostream & out, constraint const & c) {
break;
case constraint_kind::Choice:
out << "choice ";
if (cnstr_delayed(c)) out << "[delayed] ";
if (cnstr_delay_factor(c) != 0) out << "[delayed:" << cnstr_delay_factor(c) << "] ";
out << cnstr_expr(c);
break;
}

8
src/kernel/constraint.h
View file

@ -67,7 +67,7 @@ public:
friend constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j);
friend constraint mk_level_eq_cnstr(level const & lhs, level const & rhs, justification const & j);
friend constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, bool delayed, justification const & j);
friend constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, justification const & j);
constraint_cell * raw() const { return m_ptr; }
};
@ -77,7 +77,7 @@ inline bool operator!=(constraint const & c1, constraint const & c2) { return !(
constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j);
constraint mk_level_eq_cnstr(level const & lhs, level const & rhs, justification const & j);
constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, bool delayed, justification const & j);
constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, justification const & j);
inline bool is_eq_cnstr(constraint const & c) { return c.kind() == constraint_kind::Eq; }
inline bool is_level_eq_cnstr(constraint const & c) { return c.kind() == constraint_kind::LevelEq; }
@ -97,8 +97,8 @@ level const & cnstr_rhs_level(constraint const & c);
expr const & cnstr_expr(constraint const & c);
/** \brief Return the choice_fn associated with a choice constraint. */
choice_fn const & cnstr_choice_fn(constraint const & c);
/** \brief Return true iff choice constraint must be delayed. */
bool cnstr_delayed(constraint const & c);
/** \brief Return the choice constraint delay factor */
unsigned cnstr_delay_factor(constraint const & c);
/** \brief Printer for debugging purposes */
std::ostream & operator<<(std::ostream & out, constraint const & c);

14
src/library/kernel_bindings.cpp
View file

@ -1513,13 +1513,13 @@ static int mk_choice_cnstr(lua_State * L) {
expr m = to_expr(L, 1);
choice_fn fn = to_choice_fn(L, 2);
if (nargs == 2)
return push_constraint(L, mk_choice_cnstr(m, fn, false, justification()));
return push_constraint(L, mk_choice_cnstr(m, fn, 0, justification()));
else if (nargs == 3 && is_justification(L, 3))
return push_constraint(L, mk_choice_cnstr(m, fn, false, to_justification(L, 3)));
return push_constraint(L, mk_choice_cnstr(m, fn, 0, to_justification(L, 3)));
else if (nargs == 3)
return push_constraint(L, mk_choice_cnstr(m, fn, lua_toboolean(L, 3), justification()));
return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), justification()));
else
return push_constraint(L, mk_choice_cnstr(m, fn, lua_toboolean(L, 3), to_justification(L, 4)));
return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), to_justification(L, 4)));
}
static int constraint_expr(lua_State * L) {
@ -1530,10 +1530,10 @@ static int constraint_expr(lua_State * L) {
throw exception("arg #1 must be a choice constraint");
}
static int constraint_delayed(lua_State * L) {
static int constraint_delay_factor(lua_State * L) {
constraint const & c = to_constraint(L, 1);
if (is_choice_cnstr(c))
return push_boolean(L, cnstr_delayed(c));
return push_integer(L, cnstr_delay_factor(c));
else
throw exception("arg #1 must be a choice constraint");
}
@ -1550,7 +1550,7 @@ static const struct luaL_Reg constraint_m[] = {
{"rhs", safe_function<constraint_rhs>},
{"justification", safe_function<constraint_jst>},
{"expr", safe_function<constraint_expr>},
{"delayed", safe_function<constraint_delayed>},
{"delay_factor", safe_function<constraint_delay_factor>},
{0, 0}
};

45
src/library/unifier.cpp
View file

@ -191,37 +191,23 @@ std::pair<unify_status, substitution> unify_simple(substitution const & s, const
}
static constraint g_dont_care_cnstr = mk_eq_cnstr(expr(), expr(), justification());
/**
The unifier divides the constraints in 6 groups: Simple, Basic, FlexRigid, Reduction, FlexFlex, DelayedChoice
1) Simple: constraints that never create case-splits. Example: pattern matching constraints (?M l_1 ... l_n) =?= t.
The are not even inserted in the constraint priority queue.
2) Basic: contains user choice constraints used to model coercions and overloaded constraints, and constraints
that cannot be solved, and the unification plugin must be invoked.
3) FlexRigid constraints (?M t_1 ... t_n) =?= t, where t_n is not an introduction application
4) PluginDelayed: contraints delayed by the unifier_plugin. Examples: (elim ... (?m ...)) and (?m ... (intro ...)),
where elim is an eliminator/recursor and intro is an introduction/constructor.
This constraints are delayed because after ?m is assigned we may be able to reduce them.
5) FlexFlex: (?m1 ...) =?= (?m2 ...) we don't try to solve this constraint, we delay them and hope the other
ones instantiate ?m1 or ?m2. If this kind of constraint is the next to be processed in the queue, then
we simply discard it.
6) DelayedChoice: delayed choice constraints, they are used to model features such as class-instance
They are really term synthesizers. We use the unifier just to exploit the non-chronological backtracking
infrastructure
*/
enum class cnstr_group { Basic = 0, FlexRigid, PluginDelayed, FlexFlex, DelayedChoice };
static unsigned g_group_size = 1u << 28;
static unsigned g_cnstr_group_first_index[5] = { 0, g_group_size, 2*g_group_size, 3*g_group_size, 4*g_group_size};
static unsigned g_group_size = 1u << 29;
static unsigned g_cnstr_group_first_index[6] = { 0, g_group_size, 2*g_group_size, 3*g_group_size, 4*g_group_size, 5*g_group_size};
static unsigned get_group_first_index(cnstr_group g) {
return g_cnstr_group_first_index[static_cast<unsigned>(g)];
}
/** \brief Convert choice constraint delay factor to cnstr_group */
cnstr_group get_choice_cnstr_group(constraint const & c) {
lean_assert(is_choice_cnstr(c));
unsigned f = cnstr_delay_factor(c);
if (f > static_cast<unsigned>(cnstr_group::MaxDelayed)) {
return cnstr_group::MaxDelayed;
} else {
return static_cast<cnstr_group>(f);
}
}
/** \brief Auxiliary functional object for implementing simultaneous higher-order unification */
struct unifier_fn {
typedef std::pair<constraint, unsigned> cnstr; // constraint + idx
@ -638,10 +624,7 @@ struct unifier_fn {
switch (c.kind()) {
case constraint_kind::Choice:
// Choice constraints are never considered easy.
if (cnstr_delayed(c))
add_cnstr(c, nullptr, nullptr, cnstr_group::DelayedChoice);
else
add_cnstr(c, nullptr, nullptr, cnstr_group::Basic);
add_cnstr(c, nullptr, nullptr, get_choice_cnstr_group(c));
return true;
case constraint_kind::Eq:
return process_eq_constraint(c);

28
src/library/unifier.h
View file

@ -45,6 +45,34 @@ lazy_list<substitution> unify(environment const & env, expr const & lhs, expr co
lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, substitution const & s,
options const & o);
/**
The unifier divides the constraints in 6 groups: Simple, Basic, FlexRigid, PluginDelayed, PreFlexFlex, FlexFlex, MaxDelayed
1) Simple: constraints that never create case-splits. Example: pattern matching constraints (?M l_1 ... l_n) =?= t.
The are not even inserted in the constraint priority queue.
2) Basic: contains user choice constraints used to model coercions and overloaded constraints, and constraints
that cannot be solved, and the unification plugin must be invoked.
3) FlexRigid constraints (?M t_1 ... t_n) =?= t, where t_n is not an introduction application
4) PluginDelayed: contraints delayed by the unifier_plugin. Examples: (elim ... (?m ...)) and (?m ... (intro ...)),
where elim is an eliminator/recursor and intro is an introduction/constructor.
This constraints are delayed because after ?m is assigned we may be able to reduce them.
5) PreFlexFlex: this group is for constraints we want solved before we start discarding FlexFlex constraints.
6) FlexFlex: (?m1 ...) =?= (?m2 ...) we don't try to solve this constraint, we delay them and hope the other
ones instantiate ?m1 or ?m2. If this kind of constraint is the next to be processed in the queue, then
we simply discard it.
7) MaxDelayed: for delayed choice constraints, they are used to model features such as class-instance
They are really term synthesizers. We use the unifier just to exploit the non-chronological backtracking
infrastructure
*/
enum class cnstr_group { Basic = 0, FlexRigid, PluginDelayed, PreFlexFlex, FlexFlex, MaxDelayed };
inline unsigned to_delay_factor(cnstr_group g) { return static_cast<unsigned>(g); }
class unifier_exception : public exception {
justification m_jst;
substitution m_subst;

47
tests/lean/run/alias1.lean Normal file
View file

@ -0,0 +1,47 @@
import logic
namespace N1
variable num : Type.{1}
variable foo : num → num → num
end
namespace N2
variable val : Type.{1}
variable foo : val → val → val
end
using N1
using N2
variables a b : num
variables x y : val
check foo a b
check foo x y
variable f : num → val
coercion f
check foo a x
check foo x y
check foo x a
check foo a b
theorem T1 : foo a b = N1.foo a b
:= refl _
definition aux1 := foo a b -- System elaborated it to N2.foo (f a) (f b)
theorem T2 : aux1 = N2.foo (f a) (f b)
:= refl _
using N1
definition aux2 := foo a b -- Now N1 is in the beginning of the queue again, and this is elaborated to N1.foo a b
check aux2
theorem T3 : aux2 = N1.foo a b
:= refl aux2
check foo a b
theorem T4 : foo a b = N1.foo a b
:= refl _

23
tests/lean/run/alias2.lean Normal file
View file

@ -0,0 +1,23 @@
import logic
namespace N1
variable num : Type.{1}
variable foo : num → num → num
end
namespace N2
variable val : Type.{1}
variable foo : val → val → val
end
using N2
using N1
variables a b : num
variable f : num → val
coercion f
definition aux2 := foo a b
check aux2
theorem T3 : aux2 = N1.foo a b
:= refl _