From 0e015974caed382fd19d9fb27b2fb18663e1e99b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 28 Jun 2014 11:18:22 -0700 Subject: [PATCH] fix(library/unifier): bug in process_flex_rigid, also cleanup the code and break it into different cases Signed-off-by: Leonardo de Moura --- library/standard/logic.lean | 4 +- src/frontends/lean/elaborator.cpp | 1 - src/library/unifier.cpp | 237 ++++++++++++++++++++++-------- 3 files changed, 178 insertions(+), 64 deletions(-) diff --git a/library/standard/logic.lean b/library/standard/logic.lean index 6fb790d0c..020e5ee7c 100644 --- a/library/standard/logic.lean +++ b/library/standard/logic.lean @@ -70,8 +70,8 @@ theorem trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c theorem symm {A : Type} {a b : A} (H : a = b) : b = a := subst H (refl a) --- theorem congr1 {A B : Type} {f g : A → B} (H : f = g) (a : A) : f a = g a --- := subst H (refl (f a)) -- TODO: check unifier does not work in this case +theorem congr1 {A B : Type} {f g : A → B} (H : f = g) (a : A) : f a = g a +:= subst H (refl (f a)) theorem congr2 {A B : Type} {a b : A} (f : A → B) (H : a = b) : f a = f b := subst H (refl (f a)) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index a5c228728..7cc5d4fe7 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -601,7 +601,6 @@ public: return pp_def_type_mismatch(fmt, env, o, n, r_t, r_v_type); }); } - auto p = solve().pull(); lean_assert(p); substitution s = p->first; diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index a1f34a73c..f781898e4 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -870,16 +870,138 @@ struct unifier_fn { return is_eq_cnstr(c) && is_meta(cnstr_lhs_expr(c)) && is_meta(cnstr_rhs_expr(c)); } - /** \brief Process a flex rigid constraint */ - bool process_flex_rigid(expr const & lhs, expr const & rhs, justification const & j) { - lean_assert(is_meta(lhs)); + /** + \brief Given + m := a metavariable ?m + margs := [a_1 ... a_k] + rhs := (g b_1 ... b_n) + Then create the constraints + (?m_1 a_1 ... a_k) =?= b_1 + ... + (?m_n a_1 ... a_k) =?= b_n + ?m =?= fun (x_1 ... x_k), f (?m_1 x_1 ... x_k) ... (?m_n x_1 ... x_k) + + Remark: The term f is: + - g (if g is a constant), OR + - variable (if g is a local constant equal to a_i) + */ + constraints mk_flex_rigid_app_cnstrs(expr const & m, buffer const & margs, + expr const & f, expr const & rhs, justification const & j) { + lean_assert(is_metavar(m)); + lean_assert(is_app(rhs)); + lean_assert(is_constant(f) || is_var(f)); + buffer cs; + expr const & mtype = mlocal_type(m); + buffer rargs; + get_app_args(rhs, rargs); + buffer sargs; + for (expr const & rarg : rargs) { + expr maux = mk_aux_metavar_for(mtype); + cs.push_back(mk_eq_cnstr(mk_app(maux, margs), rarg, j)); + sargs.push_back(mk_app_vars(maux, margs.size())); + } + expr v = mk_app(f, sargs); + v = mk_lambda_for(mtype, v); + cs.push_back(mk_eq_cnstr(m, v, j)); + return to_list(cs.begin(), cs.end()); + } + + /** + \brief Given + m := a metavariable ?m + margs := [a_1 ... a_k] + rhs := (fun/Pi (y : A), B y) + Then create the constraints + (?m_1 a_1 ... a_k) =?= A + (?m_2 a_1 ... a_k l) =?= B l + ?m =?= fun (x_1 ... x_k), fun/Pi (y : ?m_1 x_1 ... x_k), ?m_2 x_1 ... x_k y + where l is a fresh local constant. + */ + constraints mk_bindings_imitation(expr const & m, buffer const & margs, expr const & rhs, justification const & j) { + lean_assert(is_metavar(m)); + lean_assert(is_binding(rhs)); + expr const & mtype = mlocal_type(m); + expr maux1 = mk_aux_metavar_for(mtype); + buffer cs; + cs.push_back(mk_eq_cnstr(mk_app(maux1, margs), binding_domain(rhs), j)); + expr dontcare; + expr tmp_pi = mk_pi(binding_name(rhs), mk_app_vars(maux1, margs.size()), dontcare); // trick for "extending" the context + expr mtype2 = replace_range(mtype, tmp_pi); // trick for "extending" the context + expr maux2 = mk_aux_metavar_for(mtype2); + expr new_local = mk_local(m_ngen.next(), binding_name(rhs), binding_domain(rhs)); + cs.push_back(mk_eq_cnstr(mk_app(mk_app(maux2, margs), new_local), instantiate(binding_body(rhs), new_local), j)); + expr v = update_binding(rhs, mk_app_vars(maux1, margs.size()), mk_app_vars(maux2, margs.size() + 1)); + v = mk_lambda_for(mtype, v); + cs.push_back(mk_eq_cnstr(m, v, j)); + return to_list(cs.begin(), cs.end()); + } + + /** + \brief Given + m := a metavariable ?m + rhs := sort, constant + Then solve (?m a_1 ... a_k) =?= rhs, by returning the constraint + ?m =?= fun (x1 ... x_k), rhs + */ + constraints mk_simple_imitation(expr const & m, expr const & rhs, justification const & j) { + lean_assert(is_metavar(m)); + lean_assert(is_sort(rhs) || is_constant(rhs)); + expr const & mtype = mlocal_type(m); + expr v = mk_lambda_for(mtype, rhs); + return constraints(mk_eq_cnstr(m, v, j)); + } + + /** + \brief Given + m := a metavariable ?m + margs := [a_1 ... a_k] + rhs := M(b_1 ... b_n) where M is a macro with arguments b_1 ... b_n + Then create the constraints + (?m_1 a_1 ... a_k) =?= b_1 + ... + (?m_n a_1 ... a_k) =?= b_n + ?m =?= fun (x_1 ... x_k), M((?m_1 x_1 ... x_k) ... (?m_n x_1 ... x_k)) + */ + constraints mk_macro_imitation(expr const & m, buffer const & margs, expr const & rhs, justification const & j) { + lean_assert(is_metavar(m)); + lean_assert(is_macro(rhs)); + expr const & mtype = mlocal_type(m); + buffer cs; + // create an auxiliary metavariable for each macro argument + buffer sargs; + for (unsigned i = 0; i < macro_num_args(rhs); i++) { + expr maux = mk_aux_metavar_for(mtype); + cs.push_back(mk_eq_cnstr(mk_app(maux, margs), macro_arg(rhs, i), j)); + sargs.push_back(mk_app_vars(maux, margs.size())); + } + expr v = mk_macro(macro_def(rhs), sargs.size(), sargs.data()); + v = mk_lambda_for(mtype, v); + cs.push_back(mk_eq_cnstr(m, v, j)); + return to_list(cs.begin(), cs.end()); + } + + /** + Given, + m := a metavariable ?m + margs := [a_1 ... a_k] + We say a unification problem (?m a_1 ... a_k) =?= rhs uses "simple projections" IF + rhs is NOT an application. + + If rhs is a local constant and a_i == rhs, then we add the constraint + ?m =?= fun x_1 ... x_k, x_i + to alts as a possible solution when a_i is the same local constant. + + If rhs is not a local constant, then for each a_i that is NOT a local constant, we add the constraints + ?m =?= fun x_1 ... x_k, x_i + a_i =?= rhs + to alts as a possible solution when a_i is the same local constant. + */ + void add_simple_projections(expr const & m, buffer const & margs, expr const & rhs, justification const & j, + buffer & alts) { + lean_assert(is_metavar(m)); lean_assert(!is_meta(rhs)); - buffer margs; - expr m = get_app_args(lhs, margs); - expr mtype = mlocal_type(m); - buffer alts; - lean_assert(!is_var(rhs)); // rhs can't be a free variable (this is an invariant of the approach we are using). - // Add Projections to alts + lean_assert(!is_app(rhs)); + expr const & mtype = mlocal_type(m); unsigned vidx = margs.size() - 1; for (expr const & marg : margs) { if (!is_local(marg) && !is_local(rhs)) { @@ -894,59 +1016,52 @@ struct unifier_fn { } vidx--; } - // Add Imitation to alts - buffer cs; - bool imitate = true; - if (is_app(rhs)) { - buffer rargs; - expr f = get_app_args(rhs, rargs); - // create an auxiliary metavariable for each rhs argument - buffer sargs; - for (expr const & rarg : rargs) { - expr maux = mk_aux_metavar_for(mtype); - cs.push_back(mk_eq_cnstr(mk_app(maux, margs), rarg, j)); - sargs.push_back(mk_app_vars(maux, margs.size())); + } + + /** \brief Process a flex rigid constraint */ + bool process_flex_rigid(expr const & lhs, expr const & rhs, justification const & j) { + lean_assert(is_meta(lhs)); + lean_assert(!is_meta(rhs)); + buffer margs; + expr m = get_app_args(lhs, margs); + for (expr & marg : margs) + marg = m_tc.whnf(marg); + buffer alts; + switch (rhs.kind()) { + case expr_kind::Var: case expr_kind::Meta: + lean_unreachable(); // LCOV_EXCL_LINE + case expr_kind::Local: + add_simple_projections(m, margs, rhs, j, alts); + break; + case expr_kind::Sort: case expr_kind::Constant: + add_simple_projections(m, margs, rhs, j, alts); + alts.push_back(mk_simple_imitation(m, rhs, j)); + break; + case expr_kind::Pi: case expr_kind::Lambda: + add_simple_projections(m, margs, rhs, j, alts); + alts.push_back(mk_bindings_imitation(m, margs, rhs, j)); + break; + case expr_kind::Macro: + add_simple_projections(m, margs, rhs, j, alts); + alts.push_back(mk_macro_imitation(m, margs, rhs, j)); + break; + case expr_kind::App: { + expr const & f = get_app_fn(rhs); + lean_assert(is_constant(f) || is_local(f)); + if (is_local(f)) { + unsigned vidx = margs.size() - 1; + for (expr const & marg : margs) { + if (is_local(marg) && mlocal_name(marg) == mlocal_name(f)) + alts.push_back(mk_flex_rigid_app_cnstrs(m, margs, mk_var(vidx), rhs, j)); + vidx--; + } + } else if (is_constant(f)) { + alts.push_back(mk_flex_rigid_app_cnstrs(m, margs, f, rhs, j)); + } else { + lean_unreachable(); // LCOV_EXCL_LINE } - f = abstract_locals(f, margs.size(), margs.data()); - if (!has_local(f)) { - expr v = mk_app(f, sargs); - v = mk_lambda_for(mtype, v); - cs.push_back(mk_eq_cnstr(m, v, j)); - } - } else if (is_binding(rhs)) { - expr maux1 = mk_aux_metavar_for(mtype); - cs.push_back(mk_eq_cnstr(mk_app(maux1, margs), binding_domain(rhs), j)); - expr dontcare; - expr tmp_pi = mk_pi(binding_name(rhs), mk_app_vars(maux1, margs.size()), dontcare); // trick for "extending" the context - expr mtype2 = replace_range(mtype, tmp_pi); // trick for "extending" the context - expr maux2 = mk_aux_metavar_for(mtype2); - expr new_local = mk_local(m_ngen.next(), binding_name(rhs), binding_domain(rhs)); - cs.push_back(mk_eq_cnstr(mk_app(mk_app(maux2, margs), new_local), instantiate(binding_body(rhs), new_local), j)); - expr v = update_binding(rhs, mk_app_vars(maux1, margs.size()), mk_app_vars(maux2, margs.size() + 1)); - v = mk_lambda_for(mtype, v); - cs.push_back(mk_eq_cnstr(m, v, j)); - } else if (is_sort(rhs) || is_constant(rhs)) { - expr v = mk_lambda_for(mtype, rhs); - cs.push_back(mk_eq_cnstr(m, v, j)); - } else if (is_local(rhs)) { - // We don't imitate when the right-hand-side is a local constant. - // The term (fun (ctx), local) is not well-formed. - imitate = false; - } else { - lean_assert(is_macro(rhs)); - // create an auxiliary metavariable for each macro argument - buffer sargs; - for (unsigned i = 0; i < macro_num_args(rhs); i++) { - expr maux = mk_aux_metavar_for(mtype); - cs.push_back(mk_eq_cnstr(mk_app(maux, margs), macro_arg(rhs, i), j)); - sargs.push_back(mk_app_vars(maux, margs.size())); - } - expr v = mk_macro(macro_def(rhs), sargs.size(), sargs.data()); - v = mk_lambda_for(mtype, v); - cs.push_back(mk_eq_cnstr(m, v, j)); - } - if (imitate) - alts.push_back(to_list(cs.begin(), cs.end())); + break; + }} if (alts.empty()) { set_conflict(j);