From f4592da87f509b431cfc366075199eaeea0a0c36 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 21 Oct 2013 16:45:14 -0700 Subject: [PATCH] feat(elaborator): solve more unification constraints, add more tests Signed-off-by: Leonardo de Moura --- src/library/elaborator/elaborator.cpp | 145 +++++++++++-- src/library/elaborator/elaborator_trace.cpp | 33 ++- src/library/elaborator/elaborator_trace.h | 17 ++ src/tests/library/elaborator/elaborator.cpp | 212 ++++++++++++++++++++ 4 files changed, 393 insertions(+), 14 deletions(-) diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index 7c4b621b2..e74c1e48d 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -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 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 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 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(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 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 & 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(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(); diff --git a/src/library/elaborator/elaborator_trace.cpp b/src/library/elaborator/elaborator_trace.cpp index b327b2779..6fa753c8a 100644 --- a/src/library/elaborator/elaborator_trace.cpp +++ b/src/library/elaborator/elaborator_trace.cpp @@ -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 & 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 & r) const { + push_back(r, m_trace); +} + // ------------------------- // Synthesis trace objects // ------------------------- diff --git a/src/library/elaborator/elaborator_trace.h b/src/library/elaborator/elaborator_trace.h index ab8e65a9e..c24921f1f 100644 --- a/src/library/elaborator/elaborator_trace.h +++ b/src/library/elaborator/elaborator_trace.h @@ -130,6 +130,23 @@ public: virtual void get_children(buffer & r) const; }; +/** + \brief Trace object used to justify a typeof(m) == t 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 & r) const; +}; + /** \brief Base class for synthesis_failure_trace and synthesized_assignment_trace */ diff --git a/src/tests/library/elaborator/elaborator.cpp b/src/tests/library/elaborator/elaborator.cpp index 2cca32767..4ad8658f5 100644 --- a/src/tests/library/elaborator/elaborator.cpp +++ b/src/tests/library/elaborator/elaborator.cpp @@ -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 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 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 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 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 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; }