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

feat(elaborator): solve more unification constraints, add more tests

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-10-21 16:45:14 -07:00
parent c3e87f106f
commit f4592da87f
4 changed files with 393 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -12,6 +12,7 @@ Author: Leonardo de Moura
#include "kernel/free_vars.h"
#include "kernel/normalizer.h"
#include "kernel/instantiate.h"
#include "kernel/replace.h"
#include "kernel/builtin.h"
#include "library/type_inferer.h"
#include "library/update_expr.h"
@ -165,6 +166,11 @@ class elaborator::imp {
m_state.m_queue.push_front(c);
}
/** \brief Add given constraint to the end of the current constraint queue */
void push_back(unification_constraint const & c) {
m_state.m_queue.push_back(c);
}
/** \brief Return true iff \c m is an assigned metavariable in the current state */
bool is_assigned(expr const & m) const {
lean_assert(is_metavar(m));
@ -199,6 +205,14 @@ class elaborator::imp {
return ::lean::has_metavar(e, m, m_state.m_menv.get_substitutions());
}
/**
\brief Return true iff \c e contains an assigned metavariable in
the current state.
*/
bool has_assigned_metavar(expr const & e) const {
return ::lean::has_assigned_metavar(e, m_state.m_menv.get_substitutions());
}
/**
\brief Return a unassigned metavariable in the current state.
Return the anonymous name if the state does not contain unassigned metavariables.
@ -291,12 +305,17 @@ class elaborator::imp {
/**
\brief Assign \c v to \c m with justification \c tr in the current state.
*/
void assign(expr const & m, expr const & v, trace const & tr) {
void assign(expr const & m, expr const & v, context const & ctx, trace const & tr) {
lean_assert(is_metavar(m));
metavar_env & menv = m_state.m_menv;
m_state.m_menv.assign(m, v, tr);
if (menv.has_type(m)) {
buffer<unification_constraint> ucs;
expr tv = m_type_inferer(v, ctx, &menv, ucs);
for (auto c : ucs)
push_front(c);
trace new_trace(new typeof_mvar_trace(ctx, m, menv.get_type(m), tv, tr));
push_front(mk_eq_constraint(ctx, menv.get_type(m), tv, new_trace));
}
}
@ -342,7 +361,7 @@ class elaborator::imp {
m_conflict = trace(new unification_failure_trace(c));
return Failed;
} else if (allow_assignment) {
assign(a, b, trace(new assignment_trace(c)));
assign(a, b, get_context(c), trace(new assignment_trace(c)));
reset_quota();
return Processed;
}
@ -350,7 +369,7 @@ class elaborator::imp {
local_entry const & me = head(metavar_lctx(a));
if (me.is_lift() && !has_free_var(b, me.s(), me.s() + me.n())) {
// Case 3
trace new_tr(new substitution_trace(c, get_mvar_trace(a)));
trace new_tr(new normalize_trace(c));
expr new_a = pop_meta_context(a);
expr new_b = lower_free_vars(b, me.s() + me.n(), me.n());
if (!is_lhs)
@ -371,6 +390,48 @@ class elaborator::imp {
return Continue;
}
trace mk_subst_trace(unification_constraint const & c, buffer<trace> const & subst_traces) {
if (subst_traces.size() == 1) {
return trace(new substitution_trace(c, subst_traces[0]));
} else {
return trace(new multi_substitution_trace(c, subst_traces.size(), subst_traces.data()));
}
}
/**
\brief Return true iff \c a contains instantiated variables. If this is the case,
then constraint \c c is updated with a new \c a s.t. all metavariables of \c a
are instantiated.
\remark if \c is_lhs is true, then we are considering the left-hand-side of the constraint \c c.
*/
bool instantiate_metavars(bool is_lhs, expr const & a, unification_constraint const & c) {
lean_assert(is_eq(c) || is_convertible(c));
lean_assert(!is_eq(c) || !is_lhs || is_eqp(eq_lhs(c), a));
lean_assert(!is_eq(c) || is_lhs || is_eqp(eq_rhs(c), a));
lean_assert(!is_convertible(c) || !is_lhs || is_eqp(convertible_from(c), a));
lean_assert(!is_convertible(c) || is_lhs || is_eqp(convertible_to(c), a));
if (has_assigned_metavar(a)) {
metavar_env & menv = m_state.m_menv;
buffer<trace> traces;
auto f = [&](expr const & m, unsigned) -> expr {
if (is_metavar(m) && menv.is_assigned(m)) {
trace t = menv.get_trace(m);
if (t)
traces.push_back(t);
return menv.get_subst(m);
} else {
return m;
}
};
expr new_a = replace_fn<decltype(f)>(f)(a);
trace new_tr = mk_subst_trace(c, traces);
push_updated_constraint(c, is_lhs, new_a, new_tr);
return true;
} else {
return false;
}
}
/** \brief Unfold let-expression */
void process_let(expr & a) {
@ -512,6 +573,41 @@ class elaborator::imp {
}
}
/** \brief Return true iff the variable with id \c vidx has a body/definition in the context \c ctx. */
static bool has_body(context const & ctx, unsigned vidx) {
try {
context_entry const & e = lookup(ctx, vidx);
if (e.get_body())
return true;
} catch (exception&) {
}
return false;
}
/**
\brief Return true iff ctx |- a == b is a "simple" higher-order matching constraint. By simple, we mean
a constraint of the form
ctx |- (?m x) == c
The constraint is solved by assigning ?m to (fun (x : T), c).
*/
bool process_simple_ho_match(context const & ctx, expr const & a, expr const & b, bool is_lhs, unification_constraint const & c) {
// Solve constraint of the form
// ctx |- (?m x) == c
// using imitation
if (is_eq(c) && is_meta_app(a) && is_var(arg(a, 1)) && !has_body(ctx, var_idx(arg(a, 1))) && closed(b)) {
expr m = arg(a, 0);
expr t = lookup(ctx, var_idx(arg(a, 1))).get_domain();
trace new_trace(new destruct_trace(c));
expr s = mk_lambda(g_x_name, t, b);
if (!is_lhs)
swap(m, s);
push_front(mk_eq_constraint(ctx, m, s, new_trace));
return true;
} else {
return false;
}
}
bool process_eq_convertible(context const & ctx, expr const & a, expr const & b, unification_constraint const & c) {
bool eq = is_eq(c);
if (a == b) {
@ -532,10 +628,19 @@ class elaborator::imp {
r = process_metavar(c, b, a, false, !is_type(a) && !is_meta(a) && a != Bool);
if (r != Continue) { return r == Processed; }
if (process_simple_ho_match(ctx, a, b, true, c) ||
process_simple_ho_match(ctx, b, a, false, c))
return true;
if (a.kind() == b.kind()) {
switch (a.kind()) {
case expr_kind::Constant: case expr_kind::Var: case expr_kind::Value:
return a == b;
if (a == b) {
return true;
} else {
m_conflict = trace(new unification_failure_trace(c));
return false;
}
case expr_kind::Type:
if ((!eq && m_env.is_ge(ty_level(b), ty_level(a))) || (eq && a == b)) {
return true;
@ -586,10 +691,18 @@ class elaborator::imp {
}
}
if (!is_meta(a) && !is_meta(b) && a.kind() != b.kind())
if (!is_meta(a) && !is_meta(b) && a.kind() != b.kind()) {
m_conflict = trace(new unification_failure_trace(c));
return false;
}
if (instantiate_metavars(true, a, c) ||
instantiate_metavars(false, b, c)) {
return true;
}
std::cout << "Postponed: "; display(std::cout, c);
push_back(c);
return true;
}
@ -600,15 +713,24 @@ class elaborator::imp {
return true;
}
bool process_choice(unification_constraint const &) {
// TODO(Leo)
return true;
bool process_choice(unification_constraint const & c) {
std::unique_ptr<case_split> new_cs(new choice_case_split(c, m_state));
bool r = new_cs->next(*this);
lean_assert(r);
m_case_splits.push_back(std::move(new_cs));
return r;
}
void resolve_conflict() {
lean_assert(m_conflict);
std::cout << "Resolve conflict, num case_splits: " << m_case_splits.size() << "\n";
formatter fmt = mk_simple_formatter();
std::cout << m_conflict.pp(fmt, options(), nullptr, true) << "\n";
while (!m_case_splits.empty()) {
std::unique_ptr<case_split> & d = m_case_splits.back();
std::cout << "Assumption " << d->m_curr_assumption.pp(fmt, options(), nullptr, true) << "\n";
if (depends_on(m_conflict, d->m_curr_assumption)) {
d->m_failed_traces.push_back(m_conflict);
if (d->next(*this)) {
@ -630,7 +752,6 @@ class elaborator::imp {
s.m_curr_assumption = mk_assumption();
m_state = s.m_prev_state;
push_front(mk_eq_constraint(get_context(choice), choice_mvar(choice), choice_ith(choice, idx), s.m_curr_assumption));
s.m_idx++;
return true;
} else {
m_conflict = trace(new unification_failure_by_cases_trace(choice, s.m_failed_traces.size(), s.m_failed_traces.data()));
@ -710,7 +831,7 @@ public:
while (true) {
check_interrupted(m_interrupted);
cnstr_queue & q = m_state.m_queue;
if (q.empty()) {
if (q.empty() || m_quota < -static_cast<int>(q.size())) {
name m = find_unassigned_metavar();
std::cout << "Queue is empty\n"; display(std::cout);
if (m) {
@ -722,7 +843,7 @@ public:
}
} else {
unification_constraint c = q.front();
std::cout << "Processing "; display(std::cout, c);
std::cout << "Processing, quota: " << m_quota << " "; display(std::cout, c);
q.pop_front();
if (!process(c)) {
resolve_conflict();

33
src/library/elaborator/elaborator_trace.cpp
View file

@ -48,9 +48,8 @@ expr const & propagation_trace::get_main_expr() const {
}
format propagation_trace::pp_header(formatter const & fmt, options const & opts) const {
format r;
unsigned indent = get_pp_indent(opts);
r += format(get_prop_name());
r += nest(indent, compose(line(), get_constraint().pp(fmt, opts, nullptr, false)));
r += compose(line(), get_constraint().pp(fmt, opts, nullptr, false));
return r;
}
@ -93,6 +92,36 @@ void multi_substitution_trace::get_children(buffer<trace_cell*> & r) const {
append(r, m_assignment_traces);
}
// -------------------------
// typeof metavar trace
// -------------------------
typeof_mvar_trace::typeof_mvar_trace(context const & ctx, expr const & m, expr const & tm, expr const & t, trace const & tr):
m_context(ctx),
m_mvar(m),
m_typeof_mvar(tm),
m_type(t),
m_trace(tr) {
}
typeof_mvar_trace::~typeof_mvar_trace() {
}
format typeof_mvar_trace::pp_header(formatter const & fmt, options const & opts) const {
format r;
unsigned indent = get_pp_indent(opts);
r += format("Propagate type,");
{
format body;
body += fmt(m_context, m_mvar, false, opts);
body += space();
body += colon();
body += nest(indent, compose(line(), fmt(m_context, m_typeof_mvar, false, opts)));
r += nest(indent, compose(line(), body));
}
return group(r);
}
void typeof_mvar_trace::get_children(buffer<trace_cell*> & r) const {
push_back(r, m_trace);
}
// -------------------------
// Synthesis trace objects
// -------------------------

17
src/library/elaborator/elaborator_trace.h
View file

@ -130,6 +130,23 @@ public:
virtual void get_children(buffer<trace_cell*> & r) const;
};
/**
\brief Trace object used to justify a <tt>typeof(m) == t</tt> constraint generated when
we assign a metavariable \c m.
*/
class typeof_mvar_trace : public trace_cell {
context m_context;
expr m_mvar;
expr m_typeof_mvar;
expr m_type;
trace m_trace;
public:
typeof_mvar_trace(context const & ctx, expr const & m, expr const & mt, expr const & t, trace const & tr);
virtual ~typeof_mvar_trace();
virtual format pp_header(formatter const &, options const &) const;
virtual void get_children(buffer<trace_cell*> & r) const;
};
/**
\brief Base class for synthesis_failure_trace and synthesized_assignment_trace
*/

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

@ -53,8 +53,220 @@ static void tst1() {
substitution s = elb.next();
}
static void tst2() {
/*
Solve elaboration problem for
g : Pi (A : Type), A -> A
a : Int
Axiom H : g _ a <= 0
The following elaboration problem is created
?m1 (g ?m2 (?m3 a)) (?m4 a)
?m1 in { Nat::Le, Int::Le, Real::Le }
?m3 in { Id, int2real }
?m4 in { Id, nat2int, nat2real }
*/
environment env;
import_all(env);
metavar_env menv;
buffer<unification_constraint> ucs;
type_checker checker(env);
expr A = Const("A");
expr g = Const("g");
env.add_var("g", Pi({A, Type()}, A >> A));
expr a = Const("a");
env.add_var("a", Int);
expr m1 = menv.mk_metavar();
expr m2 = menv.mk_metavar();
expr m3 = menv.mk_metavar();
expr m4 = menv.mk_metavar();
expr int_id = Fun({a, Int}, a);
expr nat_id = Fun({a, Nat}, a);
expr F = m1(g(m2, m3(a)), m4(nVal(0)));
std::cout << F << "\n";
std::cout << checker.infer_type(F, context(), &menv, ucs) << "\n";
ucs.push_back(mk_choice_constraint(context(), m1, { mk_nat_le_fn(), mk_int_le_fn(), mk_real_le_fn() }, trace()));
ucs.push_back(mk_choice_constraint(context(), m3, { int_id, mk_int_to_real_fn() }, trace()));
ucs.push_back(mk_choice_constraint(context(), m4, { nat_id, mk_nat_to_int_fn(), mk_nat_to_real_fn() }, trace()));
elaborator elb(env, menv, ucs.size(), ucs.data());
substitution s = elb.next();
}
static void tst3() {
/*
Solve elaboration problem for
a : Int
(fun x, (f x) > 10) a
The following elaboration problem is created
(fun x : ?m1, ?m2 (f ?m3 x) (?m4 10)) (?m5 a)
?m2 in { Nat::Le, Int::Le, Real::Le }
?m4 in { Id, nat2int, nat2real }
?m5 in { Id, int2real }
*/
environment env;
import_all(env);
metavar_env menv;
buffer<unification_constraint> ucs;
type_checker checker(env);
expr A = Const("A");
expr f = Const("f");
env.add_var("f", Pi({A, Type()}, A >> A));
expr a = Const("a");
env.add_var("a", Int);
expr m1 = menv.mk_metavar();
expr m2 = menv.mk_metavar();
expr m3 = menv.mk_metavar();
expr m4 = menv.mk_metavar();
expr m5 = menv.mk_metavar();
expr int_id = Fun({a, Int}, a);
expr nat_id = Fun({a, Nat}, a);
expr x = Const("x");
expr F = Fun({x, m1}, m2(f(m3, x), m4(nVal(10))))(m5(a));
std::cout << F << "\n";
std::cout << checker.infer_type(F, context(), &menv, ucs) << "\n";
ucs.push_back(mk_choice_constraint(context(), m2, { mk_nat_le_fn(), mk_int_le_fn(), mk_real_le_fn() }, trace()));
ucs.push_back(mk_choice_constraint(context(), m4, { nat_id, mk_nat_to_int_fn(), mk_nat_to_real_fn() }, trace()));
ucs.push_back(mk_choice_constraint(context(), m5, { int_id, mk_int_to_real_fn() }, trace()));
elaborator elb(env, menv, ucs.size(), ucs.data());
substitution s = elb.next();
}
static void tst4() {
/*
Variable f {A : Type} (a : A) : A
Variable a : Int
Variable b : Real
(fun x y, (f x) > (f y)) a b
The following elaboration problem is created
(fun (x : ?m1) (y : ?m2), ?m3 (f ?m4 x) (f ?m5 y)) (?m6 a) b
?m3 in { Nat::Le, Int::Le, Real::Le }
?m6 in { Id, int2real }
*/
environment env;
import_all(env);
metavar_env menv;
buffer<unification_constraint> ucs;
type_checker checker(env);
expr A = Const("A");
expr f = Const("f");
env.add_var("f", Pi({A, Type()}, A >> A));
expr a = Const("a");
expr b = Const("b");
env.add_var("a", Int);
env.add_var("b", Real);
expr m1 = menv.mk_metavar();
expr m2 = menv.mk_metavar();
expr m3 = menv.mk_metavar();
expr m4 = menv.mk_metavar();
expr m5 = menv.mk_metavar();
expr m6 = menv.mk_metavar();
expr x = Const("x");
expr y = Const("y");
expr int_id = Fun({a, Int}, a);
expr F = Fun({{x, m1}, {y, m2}}, m3(f(m4, x), f(m5, y)))(m6(a), b);
std::cout << F << "\n";
std::cout << checker.infer_type(F, context(), &menv, ucs) << "\n";
ucs.push_back(mk_choice_constraint(context(), m3, { mk_nat_le_fn(), mk_int_le_fn(), mk_real_le_fn() }, trace()));
ucs.push_back(mk_choice_constraint(context(), m6, { int_id, mk_int_to_real_fn() }, trace()));
elaborator elb(env, menv, ucs.size(), ucs.data());
substitution s = elb.next();
}
static void tst5() {
/*
Variable f {A : Type} (a b : A) : Bool
Variable a : Int
Variable b : Real
(fun x y, f x y) a b
The following elaboration problem is created
(fun (x : ?m1) (y : ?m2), (f ?m3 x y)) (?m4 a) b
?m4 in { Id, int2real }
*/
environment env;
import_all(env);
metavar_env menv;
buffer<unification_constraint> ucs;
type_checker checker(env);
expr A = Const("A");
expr f = Const("f");
env.add_var("f", Pi({A, Type()}, A >> (A >> A)));
expr a = Const("a");
expr b = Const("b");
env.add_var("a", Int);
env.add_var("b", Real);
expr m1 = menv.mk_metavar();
expr m2 = menv.mk_metavar();
expr m3 = menv.mk_metavar();
expr m4 = menv.mk_metavar();
expr x = Const("x");
expr y = Const("y");
expr int_id = Fun({a, Int}, a);
expr F = Fun({{x, m1}, {y, m2}}, f(m3, x, y))(m4(a), b);
std::cout << F << "\n";
std::cout << checker.infer_type(F, context(), &menv, ucs) << "\n";
ucs.push_back(mk_choice_constraint(context(), m4, { int_id, mk_int_to_real_fn() }, trace()));
elaborator elb(env, menv, ucs.size(), ucs.data());
substitution s = elb.next();
}
static void tst6() {
/*
Subst : Π (A : Type U) (a b : A) (P : A → Bool), (P a) → (a = b) → (P b)
f : Int -> Int -> Int
a : Int
b : Int
H1 : (f a (f a b)) == a
H2 : a = b
Theorem T : (f a (f b b)) == a := Subst _ _ _ _ H1 H2
*/
environment env;
import_all(env);
metavar_env menv;
buffer<unification_constraint> ucs;
type_checker checker(env);
expr f = Const("f");
expr a = Const("a");
expr b = Const("b");
expr H1 = Const("H1");
expr H2 = Const("H2");
expr m1 = menv.mk_metavar();
expr m2 = menv.mk_metavar();
expr m3 = menv.mk_metavar();
expr m4 = menv.mk_metavar();
env.add_var("f", Int >> (Int >> Int));
env.add_var("a", Int);
env.add_var("b", Int);
env.add_axiom("H1", Eq(f(a, f(a, b)), a));
env.add_axiom("H2", Eq(a, b));
expr V = Subst(m1, m2, m3, m4, H1, H2);
expr expected = Eq(f(a, f(b, b)), a);
expr given = checker.infer_type(V, context(), &menv, ucs);
ucs.push_back(mk_eq_constraint(context(), expected, given, trace()));
elaborator elb(env, menv, ucs.size(), ucs.data());
substitution s = elb.next();
}
int main() {
tst1();
tst2();
tst3();
tst4();
tst5();
tst6();
return has_violations() ? 1 : 0;
}