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

feat(elaborator): only process upper bound constraints when the corresponding metavariable does not have lower bound and max constraints

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-10-23 12:50:31 -07:00
parent 172567a2fb
commit 8e1a75ce1c
2 changed files with 79 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -919,9 +919,19 @@ class elaborator::imp {
}
}
/**
\brief Return true iff c is a constraint of the form <tt>ctx |- a << ?m</tt>, where \c a is Type or Bool
*/
bool is_lower(unification_constraint const & c) {
return
is_convertible(c) &&
is_metavar(convertible_to(c)) &&
(convertible_from(c) == Bool || is_type(convertible_from(c)));
}
/** \brief Process constraint of the form <tt>ctx |- a << ?m</tt>, where \c a is Type or Bool */
bool process_lower(expr const & a, expr const & b, unification_constraint const & c) {
if (is_convertible(c) && is_metavar(b) && (a == Bool || is_type(a))) {
if (is_lower(c)) {
// Remark: in principle, there are infinite number of choices.
// We approximate and only consider the most useful ones.
trace new_tr(new destruct_trace(c));
@ -940,11 +950,53 @@ class elaborator::imp {
}
}
/**
\brief Return true if the current queue contains a constraint that satisfies the predicate p
*/
template<typename P>
bool has_constraint(P p) {
auto it = m_state.m_queue.begin();
auto end = m_state.m_queue.end();
for (; it != end; ++it) {
unification_constraint const & c = *it;
if (p(c))
return true;
}
return false;
}
/**
\brief Return true iff the current queue has a max constraint of the form <tt>ctx |- max(L1, L2) == a</tt>.
\pre is_metavar(a)
*/
bool has_max_constraint(expr const & a) {
lean_assert(is_metavar(a));
return has_constraint([&](unification_constraint const & c) { return is_max(c) && max_rhs(c) == a; });
}
/**
\brief Return true iff the current queue has a constraint that is a lower bound for \c a.
\pre is_metavar(a)
*/
bool has_lower(expr const & a) {
lean_assert(is_metavar(a));
return has_constraint([&](unification_constraint const & c) { return is_lower(c) && convertible_to(c) == a; });
}
/** \brief Process constraint of the form <tt>ctx |- ?m << b</tt>, where \c a is Type */
bool process_upper(expr const & a, expr const & b, unification_constraint const & c) {
if (is_convertible(c) && is_metavar(a) && is_type(b)) {
if (is_convertible(c) && is_metavar(a) && is_type(b) && !has_max_constraint(a) && !has_lower(a)) {
// Remark: in principle, there are infinite number of choices.
// We approximate and only consider the most useful ones.
//
// Remark: we only consider \c a if the queue does not have a constraint
// of the form ctx |- max(L1, L2) == a.
// If it does, we don't need to guess. We wait \c a to be assigned
// and just check if the upper bound is satisfied.
//
// Remark: we also give preference to lower bounds
trace new_tr(new destruct_trace(c));
unification_constraint new_c;
if (b == Type()) {
@ -1094,6 +1146,8 @@ class elaborator::imp {
}
if (m_quota < - static_cast<int>(m_state.m_queue.size())) {
// std::cout << "\n\nTRYING EXPENSIVE STEP...\n";
// display(std::cout);
// process very expensive cases
if (process_lower(a, b, c) ||
process_upper(a, b, c) ||
@ -1304,7 +1358,7 @@ public:
cnstr_queue & q = m_state.m_queue;
if (q.empty() || m_quota < - static_cast<int>(q.size()) - 10) {
name m = find_unassigned_metavar();
std::cout << "Queue is empty\n"; display(std::cout);
std::cout << "Queue is empty\n"; display(std::cout); std::cout << "\n\n";
if (m) {
// TODO(Leo)
// erase the following line, and implement interface with synthesizer

23
src/tests/library/elaborator/elaborator.cpp
View file

@ -305,6 +305,7 @@ static void unsolved(expr const & e, environment const & env) {
}
static void tst7() {
std::cout << "\nTST 7\n";
environment env;
import_all(env);
expr A = Const("A");
@ -325,6 +326,7 @@ static void tst7() {
}
static void tst8() {
std::cout << "\nTST 8\n";
environment env;
import_all(env);
expr a = Const("a");
@ -350,6 +352,7 @@ static void tst8() {
}
static void tst9() {
std::cout << "\nTST 9\n";
environment env;
import_all(env);
expr Nat = Const("N");
@ -381,6 +384,7 @@ static void tst9() {
}
static void tst10() {
std::cout << "\nTST 10\n";
environment env;
import_all(env);
expr Nat = Const("N");
@ -404,6 +408,7 @@ static void tst10() {
}
static void tst11() {
std::cout << "\nTST 11\n";
environment env;
import_all(env);
expr A = Const("A");
@ -421,6 +426,7 @@ static void tst11() {
}
static void tst12() {
std::cout << "\nTST 12\n";
environment env;
import_all(env);
expr lst = Const("list");
@ -441,6 +447,7 @@ static void tst12() {
}
static void tst13() {
std::cout << "\nTST 13\n";
environment env;
import_all(env);
expr B = Const("B");
@ -463,6 +470,7 @@ static void tst13() {
}
static void tst14() {
std::cout << "\nTST 14\n";
environment env;
import_all(env);
expr A = Const("A");
@ -503,6 +511,7 @@ static void tst14() {
}
static void tst15() {
std::cout << "\nTST 15\n";
environment env;
import_all(env);
expr A = Const("A");
@ -528,6 +537,7 @@ static void tst15() {
}
static void tst16() {
std::cout << "\nTST 16\n";
environment env;
import_all(env);
expr a = Const("a");
@ -565,6 +575,7 @@ static void tst16() {
}
void tst17() {
std::cout << "\nTST 17\n";
environment env;
import_all(env);
expr A = Const("A");
@ -579,6 +590,7 @@ void tst17() {
}
void tst18() {
std::cout << "\nTST 18\n";
environment env;
import_all(env);
expr A = Const("A");
@ -592,6 +604,7 @@ void tst18() {
}
void tst19() {
std::cout << "\nTST 19\n";
environment env;
import_all(env);
expr R = Const("R");
@ -618,6 +631,7 @@ void tst19() {
}
void tst20() {
std::cout << "\nTST 20\n";
environment env;
metavar_env menv;
expr N = Const("N");
@ -649,6 +663,7 @@ void tst20() {
}
void tst21() {
std::cout << "\nTST 21\n";
environment env;
import_all(env);
metavar_env menv;
@ -680,6 +695,7 @@ void tst21() {
}
void tst22() {
std::cout << "\nTST 22\n";
environment env;
import_all(env);
metavar_env menv;
@ -714,6 +730,7 @@ void tst22() {
}
void tst23() {
std::cout << "\nTST 23\n";
environment env;
import_all(env);
metavar_env menv;
@ -743,6 +760,7 @@ void tst23() {
}
void tst24() {
std::cout << "\nTST 24\n";
environment env;
import_all(env);
metavar_env menv;
@ -762,6 +780,7 @@ void tst24() {
}
void tst25() {
std::cout << "\nTST 25\n";
environment env;
import_all(env);
metavar_env menv;
@ -790,6 +809,7 @@ void tst25() {
}
void tst26() {
std::cout << "\nTST 26\n";
/*
Solve elaboration problem for
@ -818,12 +838,13 @@ void tst26() {
}
void tst27() {
std::cout << "\nTST 27\n";
/*
Solve elaboration problem for
g : Pi (A : Type U), A -> A
eq : Pi (A : Type U), A -> A -> Bool
a : Type 1
a : Type M
fun f : _, eq _ ((g _ f) a) a
*/
environment env;