fix(elaborator): add basic support for flex-flex pairs, add more tests, fix bug when enumerating different solutions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
80a507cf45
commit
019f64671b
2 changed files with 275 additions and 77 deletions
|
|
@ -143,6 +143,7 @@ class elaborator::imp {
|
|||
unsigned m_next_id;
|
||||
int m_quota;
|
||||
trace m_conflict;
|
||||
bool m_first;
|
||||
bool m_interrupted;
|
||||
|
||||
|
||||
|
|
@ -680,88 +681,98 @@ class elaborator::imp {
|
|||
}
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Auxiliary method for \c process_meta_app. Add new case-splits to new_cs
|
||||
*/
|
||||
void process_meta_app_core(std::unique_ptr<generic_case_split> & new_cs, expr const & a, expr const & b, bool is_lhs, unification_constraint const & c) {
|
||||
lean_assert(is_meta_app(a));
|
||||
context const & ctx = get_context(c);
|
||||
metavar_env & menv = m_state.m_menv;
|
||||
expr f_a = arg(a, 0);
|
||||
lean_assert(is_metavar(f_a));
|
||||
unsigned num_a = num_args(a);
|
||||
buffer<expr> arg_types;
|
||||
buffer<unification_constraint> ucs;
|
||||
for (unsigned i = 1; i < num_a; i++) {
|
||||
arg_types.push_back(m_type_inferer(arg(a, i), ctx, &menv, ucs));
|
||||
for (auto uc : ucs)
|
||||
push_front(uc);
|
||||
}
|
||||
// Add projections
|
||||
for (unsigned i = 1; i < num_a; i++) {
|
||||
// Assign f_a <- fun (x_1 : T_0) ... (x_{num_a-1} : T_{num_a-1}), x_i
|
||||
state new_state(m_state);
|
||||
trace new_assumption = mk_assumption();
|
||||
expr proj = mk_lambda(arg_types, mk_var(num_a - i - 1));
|
||||
expr new_a = arg(a, i);
|
||||
expr new_b = b;
|
||||
if (!is_lhs)
|
||||
swap(new_a, new_b);
|
||||
push_new_constraint(new_state.m_queue, is_eq(c), ctx, new_a, new_b, new_assumption);
|
||||
push_new_eq_constraint(new_state.m_queue, ctx, f_a, proj, new_assumption);
|
||||
new_cs->push_back(new_state, new_assumption);
|
||||
}
|
||||
// Add imitation
|
||||
state new_state(m_state);
|
||||
trace new_assumption = mk_assumption();
|
||||
expr imitation;
|
||||
if (is_app(b)) {
|
||||
// Imitation for applications
|
||||
expr f_b = arg(b, 0);
|
||||
unsigned num_b = num_args(b);
|
||||
// Assign f_a <- fun (x_1 : T_0) ... (x_{num_a-1} : T_{num_a-1}), f_b (h_1 x_1 ... x_{num_a-1}) ... (h_{num_b-1} x_1 ... x_{num_a-1})
|
||||
// New constraints (h_i a_1 ... a_{num_a-1}) == arg(b, i)
|
||||
buffer<expr> imitation_args; // arguments for the imitation
|
||||
imitation_args.push_back(f_b);
|
||||
for (unsigned i = 1; i < num_b; i++) {
|
||||
expr h_i = new_state.m_menv.mk_metavar(ctx);
|
||||
imitation_args.push_back(mk_app_vars(h_i, num_a - 1));
|
||||
push_new_eq_constraint(new_state.m_queue, ctx, update_app(a, 0, h_i), arg(b, i), new_assumption);
|
||||
}
|
||||
imitation = mk_lambda(arg_types, mk_app(imitation_args.size(), imitation_args.data()));
|
||||
} else if (is_eq(b)) {
|
||||
// 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})
|
||||
// New constraints (h_1 a_1 ... a_{num_a-1}) == eq_lhs(b)
|
||||
// (h_2 a_1 ... a_{num_a-1}) == eq_rhs(b)
|
||||
expr h_1 = new_state.m_menv.mk_metavar(ctx);
|
||||
expr h_2 = new_state.m_menv.mk_metavar(ctx);
|
||||
push_new_eq_constraint(new_state.m_queue, ctx, update_app(a, 0, h_1), eq_lhs(b), new_assumption);
|
||||
push_new_eq_constraint(new_state.m_queue, ctx, update_app(a, 0, h_2), eq_rhs(b), new_assumption);
|
||||
imitation = mk_lambda(arg_types, mk_eq(mk_app_vars(h_1, num_a - 1), mk_app_vars(h_2, num_a - 1)));
|
||||
} else if (is_abstraction(b)) {
|
||||
// Imitation for lambdas and Pis
|
||||
// Assign f_a <- fun (x_1 : T_0) ... (x_{num_a-1} : T_{num_a-1}),
|
||||
// fun (x_b : (?h_1 x_1 ... x_{num_a-1})), (?h_2 x_1 ... x_{num_a-1} x_b)
|
||||
// New constraints (h_1 a_1 ... a_{num_a-1}) == abst_domain(b)
|
||||
// (h_2 a_1 ... a_{num_a-1} x_b) == abst_body(b)
|
||||
expr h_1 = new_state.m_menv.mk_metavar(ctx);
|
||||
expr h_2 = new_state.m_menv.mk_metavar(ctx);
|
||||
push_new_eq_constraint(new_state.m_queue, ctx, update_app(a, 0, h_1), abst_domain(b), new_assumption);
|
||||
push_new_eq_constraint(new_state.m_queue, extend(ctx, abst_name(b), abst_domain(b)),
|
||||
mk_app(update_app(a, 0, h_2), Var(0)), abst_body(b), new_assumption);
|
||||
imitation = mk_lambda(arg_types, update_abstraction(b, mk_app_vars(h_1, num_a - 1), mk_app_vars(h_2, num_a)));
|
||||
} else {
|
||||
// "Dumb imitation" aka the constant function
|
||||
// Assign f_a <- fun (x_1 : T_0) ... (x_{num_a-1} : T_{num_a-1}), b
|
||||
imitation = mk_lambda(arg_types, lift_free_vars(b, 0, num_a - 1));
|
||||
}
|
||||
lean_assert(imitation);
|
||||
push_new_eq_constraint(new_state.m_queue, ctx, f_a, imitation, new_assumption);
|
||||
new_cs->push_back(new_state, new_assumption);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Process a constraint <tt>ctx |- a = b</tt> where \c a is of the form <tt>(?m ...)</tt>.
|
||||
We perform a "case split" using "projection" or "imitation". See Huet&Lang's paper on higher order matching
|
||||
for further details.
|
||||
*/
|
||||
bool process_meta_app(expr const & a, expr const & b, bool is_lhs, unification_constraint const & c) {
|
||||
if (is_meta_app(a) && !is_meta_app(b)) {
|
||||
context const & ctx = get_context(c);
|
||||
metavar_env & menv = m_state.m_menv;
|
||||
expr f_a = arg(a, 0);
|
||||
lean_assert(is_metavar(f_a));
|
||||
unsigned num_a = num_args(a);
|
||||
buffer<expr> arg_types;
|
||||
buffer<unification_constraint> ucs;
|
||||
for (unsigned i = 1; i < num_a; i++) {
|
||||
arg_types.push_back(m_type_inferer(arg(a, i), ctx, &menv, ucs));
|
||||
for (auto uc : ucs)
|
||||
push_front(uc);
|
||||
}
|
||||
bool process_meta_app(expr const & a, expr const & b, bool is_lhs, unification_constraint const & c, bool flex_flex = false) {
|
||||
if (is_meta_app(a) && (flex_flex || !is_meta_app(b))) {
|
||||
std::unique_ptr<generic_case_split> new_cs(new generic_case_split(c, m_state));
|
||||
// Add projections
|
||||
for (unsigned i = 1; i < num_a; i++) {
|
||||
// Assign f_a <- fun (x_1 : T_0) ... (x_{num_a-1} : T_{num_a-1}), x_i
|
||||
state new_state(m_state);
|
||||
trace new_assumption = mk_assumption();
|
||||
expr proj = mk_lambda(arg_types, mk_var(num_a - i - 1));
|
||||
expr new_a = arg(a, i);
|
||||
expr new_b = b;
|
||||
if (!is_lhs)
|
||||
swap(new_a, new_b);
|
||||
push_new_constraint(new_state.m_queue, is_eq(c), ctx, new_a, new_b, new_assumption);
|
||||
push_new_eq_constraint(new_state.m_queue, ctx, f_a, proj, new_assumption);
|
||||
new_cs->push_back(new_state, new_assumption);
|
||||
}
|
||||
// Add imitation
|
||||
state new_state(m_state);
|
||||
trace new_assumption = mk_assumption();
|
||||
expr imitation;
|
||||
if (is_app(b)) {
|
||||
// Imitation for applications
|
||||
expr f_b = arg(b, 0);
|
||||
unsigned num_b = num_args(b);
|
||||
// Assign f_a <- fun (x_1 : T_0) ... (x_{num_a-1} : T_{num_a-1}), f_b (h_1 x_1 ... x_{num_a-1}) ... (h_{num_b-1} x_1 ... x_{num_a-1})
|
||||
// New constraints (h_i a_1 ... a_{num_a-1}) == arg(b, i)
|
||||
buffer<expr> imitation_args; // arguments for the imitation
|
||||
imitation_args.push_back(f_b);
|
||||
for (unsigned i = 1; i < num_b; i++) {
|
||||
expr h_i = new_state.m_menv.mk_metavar(ctx);
|
||||
imitation_args.push_back(mk_app_vars(h_i, num_a - 1));
|
||||
push_new_eq_constraint(new_state.m_queue, ctx, update_app(a, 0, h_i), arg(b, i), new_assumption);
|
||||
}
|
||||
imitation = mk_lambda(arg_types, mk_app(imitation_args.size(), imitation_args.data()));
|
||||
} else if (is_eq(b)) {
|
||||
// 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})
|
||||
// New constraints (h_1 a_1 ... a_{num_a-1}) == eq_lhs(b)
|
||||
// (h_2 a_1 ... a_{num_a-1}) == eq_rhs(b)
|
||||
expr h_1 = new_state.m_menv.mk_metavar(ctx);
|
||||
expr h_2 = new_state.m_menv.mk_metavar(ctx);
|
||||
push_new_eq_constraint(new_state.m_queue, ctx, update_app(a, 0, h_1), eq_lhs(b), new_assumption);
|
||||
push_new_eq_constraint(new_state.m_queue, ctx, update_app(a, 0, h_2), eq_rhs(b), new_assumption);
|
||||
imitation = mk_lambda(arg_types, mk_eq(mk_app_vars(h_1, num_a - 1), mk_app_vars(h_2, num_a - 1)));
|
||||
} else if (is_abstraction(b)) {
|
||||
// Imitation for lambdas and Pis
|
||||
// Assign f_a <- fun (x_1 : T_0) ... (x_{num_a-1} : T_{num_a-1}),
|
||||
// fun (x_b : (?h_1 x_1 ... x_{num_a-1})), (?h_2 x_1 ... x_{num_a-1} x_b)
|
||||
// New constraints (h_1 a_1 ... a_{num_a-1}) == abst_domain(b)
|
||||
// (h_2 a_1 ... a_{num_a-1} x_b) == abst_body(b)
|
||||
expr h_1 = new_state.m_menv.mk_metavar(ctx);
|
||||
expr h_2 = new_state.m_menv.mk_metavar(ctx);
|
||||
push_new_eq_constraint(new_state.m_queue, ctx, update_app(a, 0, h_1), abst_domain(b), new_assumption);
|
||||
push_new_eq_constraint(new_state.m_queue, extend(ctx, abst_name(b), abst_domain(b)),
|
||||
mk_app(update_app(a, 0, h_2), Var(0)), abst_body(b), new_assumption);
|
||||
imitation = mk_lambda(arg_types, update_abstraction(b, mk_app_vars(h_1, num_a - 1), mk_app_vars(h_2, num_a)));
|
||||
} else {
|
||||
// "Dumb imitation" aka the constant function
|
||||
// Assign f_a <- fun (x_1 : T_0) ... (x_{num_a-1} : T_{num_a-1}), b
|
||||
imitation = mk_lambda(arg_types, lift_free_vars(b, 0, num_a - 1));
|
||||
}
|
||||
lean_assert(imitation);
|
||||
push_new_eq_constraint(new_state.m_queue, ctx, f_a, imitation, new_assumption);
|
||||
new_cs->push_back(new_state, new_assumption);
|
||||
process_meta_app_core(new_cs, a, b, is_lhs, c);
|
||||
if (flex_flex && is_meta_app(b))
|
||||
process_meta_app_core(new_cs, b, a, !is_lhs, c);
|
||||
bool r = new_cs->next(*this);
|
||||
lean_assert(r);
|
||||
m_case_splits.push_back(std::move(new_cs));
|
||||
|
|
@ -977,6 +988,8 @@ class elaborator::imp {
|
|||
// process very expensive cases
|
||||
if (process_lower(a, b, c))
|
||||
return true;
|
||||
if (process_meta_app(a, b, true, c, true))
|
||||
return true;
|
||||
}
|
||||
|
||||
// std::cout << "Postponed: "; display(std::cout, c);
|
||||
|
|
@ -1080,7 +1093,7 @@ public:
|
|||
m_next_id = 0;
|
||||
m_quota = 0;
|
||||
m_interrupted = false;
|
||||
|
||||
m_first = true;
|
||||
display(std::cout);
|
||||
}
|
||||
|
||||
|
|
@ -1094,6 +1107,12 @@ public:
|
|||
assumptions.push_back(cs->m_curr_assumption);
|
||||
m_conflict = trace(new next_solution_trace(assumptions.size(), assumptions.data()));
|
||||
resolve_conflict();
|
||||
} else if (m_first) {
|
||||
m_first = false;
|
||||
} else {
|
||||
// this is not the first run, and there are no case-splits
|
||||
m_conflict = trace(new next_solution_trace(0, nullptr));
|
||||
throw elaborator_exception(m_conflict);
|
||||
}
|
||||
reset_quota();
|
||||
while (true) {
|
||||
|
|
|
|||
|
|
@ -9,6 +9,7 @@ Author: Leonardo de Moura
|
|||
#include "kernel/type_checker.h"
|
||||
#include "kernel/abstract.h"
|
||||
#include "kernel/kernel_exception.h"
|
||||
#include "kernel/normalizer.h"
|
||||
#include "library/basic_thms.h"
|
||||
#include "library/reduce.h"
|
||||
#include "library/placeholder.h"
|
||||
|
|
@ -616,6 +617,178 @@ void tst19() {
|
|||
env);
|
||||
}
|
||||
|
||||
void tst20() {
|
||||
environment env;
|
||||
metavar_env menv;
|
||||
expr N = Const("N");
|
||||
expr M = Const("M");
|
||||
env.add_var("N", Type());
|
||||
env.add_var("M", Type());
|
||||
env.add_var("f", N >> (M >> M));
|
||||
env.add_var("a", N);
|
||||
env.add_var("b", M);
|
||||
expr f = Const("f");
|
||||
expr x = Const("x");
|
||||
expr a = Const("a");
|
||||
expr b = Const("b");
|
||||
expr m1 = menv.mk_metavar();
|
||||
expr l = m1(b, a);
|
||||
expr r = f(b, f(a, b));
|
||||
elaborator elb(env, menv, context(), l, r);
|
||||
while (true) {
|
||||
try {
|
||||
auto sol = elb.next();
|
||||
std::cout << m1 << " -> " << beta_reduce(sol.get_subst(m1)) << "\n";
|
||||
std::cout << beta_reduce(instantiate_metavars(l, sol)) << "\n";
|
||||
lean_assert(beta_reduce(instantiate_metavars(l, sol)) == r);
|
||||
std::cout << "--------------\n";
|
||||
} catch (elaborator_exception & ex) {
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void tst21() {
|
||||
environment env;
|
||||
import_all(env);
|
||||
metavar_env menv;
|
||||
expr N = Const("N");
|
||||
expr M = Const("M");
|
||||
env.add_var("N", Type());
|
||||
env.add_var("f", N >> (Bool >> N));
|
||||
env.add_var("a", N);
|
||||
env.add_var("b", N);
|
||||
expr f = Const("f");
|
||||
expr x = Const("x");
|
||||
expr a = Const("a");
|
||||
expr b = Const("b");
|
||||
expr m1 = menv.mk_metavar();
|
||||
expr l = m1(b, a);
|
||||
expr r = Fun({x, N}, f(x, Eq(a, b)));
|
||||
elaborator elb(env, menv, context(), l, r);
|
||||
while (true) {
|
||||
try {
|
||||
auto sol = elb.next();
|
||||
std::cout << m1 << " -> " << beta_reduce(sol.get_subst(m1)) << "\n";
|
||||
std::cout << beta_reduce(instantiate_metavars(l, sol)) << "\n";
|
||||
lean_assert(beta_reduce(instantiate_metavars(l, sol)) == r);
|
||||
std::cout << "--------------\n";
|
||||
} catch (elaborator_exception & ex) {
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void tst22() {
|
||||
environment env;
|
||||
import_all(env);
|
||||
metavar_env menv;
|
||||
expr N = Const("N");
|
||||
env.add_var("N", Type());
|
||||
env.add_var("f", N >> (Int >> N));
|
||||
env.add_var("a", N);
|
||||
env.add_var("b", N);
|
||||
expr m1 = menv.mk_metavar();
|
||||
expr m2 = menv.mk_metavar();
|
||||
expr m3 = menv.mk_metavar();
|
||||
expr t1 = menv.get_type(m1);
|
||||
expr t2 = menv.get_type(m2);
|
||||
expr f = Const("f");
|
||||
expr a = Const("a");
|
||||
expr b = Const("b");
|
||||
expr l = f(m1(a), iAdd(m3, iAdd(iVal(1), iVal(1))));
|
||||
expr r = f(m2(b), iAdd(iVal(1), iVal(2)));
|
||||
elaborator elb(env, menv, context(), l, r);
|
||||
while (true) {
|
||||
try {
|
||||
auto sol = elb.next();
|
||||
std::cout << m3 << " -> " << beta_reduce(sol.get_subst(m3)) << "\n";
|
||||
lean_assert(sol.get_subst(m3) == iVal(1));
|
||||
std::cout << beta_reduce(instantiate_metavars(l, sol)) << "\n";
|
||||
std::cout << beta_reduce(instantiate_metavars(r, sol)) << "\n";
|
||||
std::cout << "--------------\n";
|
||||
} catch (elaborator_exception & ex) {
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void tst23() {
|
||||
environment env;
|
||||
import_all(env);
|
||||
metavar_env menv;
|
||||
expr N = Const("N");
|
||||
env.add_var("N", Type());
|
||||
env.add_var("f", N >> (N >> N));
|
||||
expr x = Const("x");
|
||||
expr y = Const("y");
|
||||
expr f = Const("f");
|
||||
expr m1 = menv.mk_metavar();
|
||||
expr m2 = menv.mk_metavar();
|
||||
expr l = Fun({{x, N}, {y, N}}, Eq(y, f(x, m1)));
|
||||
expr r = Fun({{x, N}, {y, N}}, Eq(m2, f(m1, x)));
|
||||
elaborator elb(env, menv, context(), l, r);
|
||||
while (true) {
|
||||
try {
|
||||
auto sol = elb.next();
|
||||
std::cout << m1 << " -> " << beta_reduce(sol.get_subst(m1)) << "\n";
|
||||
std::cout << beta_reduce(instantiate_metavars(l, sol)) << "\n";
|
||||
lean_assert_eq(beta_reduce(instantiate_metavars(l, sol)),
|
||||
beta_reduce(instantiate_metavars(r, sol)));
|
||||
std::cout << "--------------\n";
|
||||
} catch (elaborator_exception & ex) {
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void tst24() {
|
||||
environment env;
|
||||
import_all(env);
|
||||
metavar_env menv;
|
||||
expr N = Const("N");
|
||||
env.add_var("N", Type());
|
||||
env.add_var("f", N >> (N >> N));
|
||||
expr f = Const("f");
|
||||
expr m1 = menv.mk_metavar();
|
||||
expr l = f(f(m1));
|
||||
expr r = f(m1);
|
||||
elaborator elb(env, menv, context(), l, r);
|
||||
try {
|
||||
elb.next();
|
||||
lean_unreachable();
|
||||
} catch (elaborator_exception & ex) {
|
||||
}
|
||||
}
|
||||
|
||||
void tst25() {
|
||||
environment env;
|
||||
import_all(env);
|
||||
metavar_env menv;
|
||||
expr N = Const("N");
|
||||
env.add_var("N", Type());
|
||||
env.add_var("f", N >> (N >> N));
|
||||
expr x = Const("x");
|
||||
expr y = Const("y");
|
||||
expr f = Const("f");
|
||||
expr m1 = menv.mk_metavar();
|
||||
expr l = Fun({x, N}, Fun({y, N}, f(m1, y))(x));
|
||||
expr r = Fun({x, N}, f(x, x));
|
||||
elaborator elb(env, menv, context(), l, r);
|
||||
while (true) {
|
||||
try {
|
||||
auto sol = elb.next();
|
||||
std::cout << m1 << " -> " << beta_reduce(sol.get_subst(m1)) << "\n";
|
||||
std::cout << beta_reduce(instantiate_metavars(l, sol)) << "\n";
|
||||
lean_assert_eq(beta_reduce(instantiate_metavars(l, sol)),
|
||||
beta_reduce(instantiate_metavars(r, sol)));
|
||||
std::cout << "--------------\n";
|
||||
} catch (elaborator_exception & ex) {
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
int main() {
|
||||
tst1();
|
||||
tst2();
|
||||
|
|
@ -636,6 +809,12 @@ int main() {
|
|||
tst17();
|
||||
tst18();
|
||||
tst19();
|
||||
tst20();
|
||||
tst21();
|
||||
tst22();
|
||||
tst23();
|
||||
tst24();
|
||||
tst25();
|
||||
return has_violations() ? 1 : 0;
|
||||
}
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue