From 48b28ad75c62e3eee4b1a5e522f79df87ff8f6a5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 6 Jul 2014 21:36:23 -0700 Subject: [PATCH] fix(library/unifier): missing test in flex_rigid Signed-off-by: Leonardo de Moura --- src/kernel/type_checker.cpp | 29 ++++--- src/kernel/type_checker.h | 21 +++-- src/library/unifier.cpp | 152 ++++++++++++++++++++++++++---------- tests/lean/run/group.lean | 2 +- tests/lean/run/group2.lean | 60 ++++++++++++++ 5 files changed, 202 insertions(+), 62 deletions(-) create mode 100644 tests/lean/run/group2.lean diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index a9ff3c3f7..12a959c55 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -55,6 +55,22 @@ expr mk_aux_metavar_for(name_generator & ngen, expr const & t) { return mk_metavar(n, new_type); } +expr mk_pi_for(name_generator & ngen, expr const & meta) { + lean_assert(is_meta(meta)); + buffer margs; + expr const & m = get_app_args(meta, margs); + expr const & mtype = mlocal_type(m); + expr maux1 = mk_aux_type_metavar_for(ngen, mtype); + expr dontcare; + expr tmp_pi = mk_pi(ngen.next(), 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_type_metavar_for(ngen, mtype2); + expr A = mk_app(maux1, margs); + margs.push_back(Var(0)); + expr B = mk_app(maux2, margs); + return mk_pi(ngen.next(), A, B); +} + type_checker::scope::scope(type_checker & tc): m_tc(tc), m_keep(false) { m_tc.push(); @@ -139,18 +155,7 @@ expr type_checker::ensure_pi_core(expr e, expr const & s) { if (is_pi(e)) { return e; } else if (is_meta(e)) { - buffer margs; - expr const & m = get_app_args(e, margs); - expr const & mtype = mlocal_type(m); - expr maux1 = mk_aux_type_metavar_for(m_gen, mtype); - expr dontcare; - expr tmp_pi = mk_pi(g_x_name, 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_type_metavar_for(m_gen, mtype2); - expr A = mk_app(maux1, margs); - margs.push_back(Var(0)); - expr B = mk_app(maux2, margs); - expr r = mk_pi(g_x_name, A, B); + expr r = mk_pi_for(m_gen, e); justification j = mk_justification(s, [=](formatter const & fmt, options const & o, substitution const & subst) { return pp_function_expected(fmt, m_env, o, subst.instantiate(s)); diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index 73e7eca42..33433815c 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -22,24 +22,33 @@ expr replace_range(expr const & type, expr const & new_range); /** \brief Given a type \c t of the form - Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), B[x_1, ..., x_n] + Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), B[x_1, ..., x_n] return a new metavariable \c m1 with type - Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{u} + Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{u} where \c u is a new universe metavariable. */ expr mk_aux_type_metavar_for(name_generator & ngen, expr const & t); /** \brief Given a type \c t of the form - Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), B[x_1, ..., x_n] + Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), B[x_1, ..., x_n] return a new metavariable \c m1 with type - Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), (m2 x_1 ... x_n) - where \c m2 is a new metavariable with type - Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{u} + Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), (?m2 x_1 ... x_n) + where \c ?m2 is a new metavariable with type + Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{u} where \c u is a new universe metavariable. */ expr mk_aux_metavar_for(name_generator & ngen, expr const & t); +/** + \brief Given a meta (?m t_1 ... t_n) where ?m has type + Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), B[x_1, ..., x_n] + return a Pi term + Pi (x : ?m1 t_1 ... t_n), (?m2 t_1 ... t_n x) + where ?m1 and ?m2 are fresh metavariables +*/ +expr mk_pi_for(name_generator & ngen, expr const & meta); + /** \brief Lean Type Checker. It can also be used to infer types, check whether a type \c A is convertible to a type \c B, etc. diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index ccc9866c1..eb572ed1e 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -353,18 +353,8 @@ struct unifier_fn { void update_conflict(justification const & j) { m_conflict = j; } void reset_conflict() { m_conflict = optional(); lean_assert(!in_conflict()); } - /** - \brief Given t - Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), B[x_1, ..., x_n] - return - fun (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), v - */ - expr mk_lambda_for(expr const & t, expr const & v) { - if (is_pi(t)) { - return mk_lambda(binding_name(t), binding_domain(t), mk_lambda_for(binding_body(t), v), binding_info(t)); - } else { - return v; - } + expr mk_local_for(expr const & b) { + return mk_local(m_ngen.next(), binding_name(b), binding_domain(b), binding_info(b)); } /** @@ -852,6 +842,62 @@ struct unifier_fn { return is_eq_cnstr(c) && is_meta(cnstr_lhs_expr(c)) && is_meta(cnstr_rhs_expr(c)); } + + /** + \brief Given t + Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), B[x_1, ..., x_n] + return + fun (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), v[x_1, ... x_n] + + \remark v has free variables. + */ + expr mk_lambda_for(expr const & t, expr const & v) { + if (is_pi(t)) { + return mk_lambda(binding_name(t), binding_domain(t), mk_lambda_for(binding_body(t), v), binding_info(t)); + } else { + return v; + } + } + + /** \see ensure_sufficient_args */ + optional ensure_sufficient_args_core(expr mtype, unsigned i, buffer const & margs) { + if (i == margs.size()) + return some_expr(mtype); + mtype = m_tc->ensure_pi(mtype); + if (!m_tc->is_def_eq(binding_domain(mtype), m_tc->infer(margs[i]))) + return none_expr(); + expr local = mk_local_for(mtype); + expr body = instantiate(binding_body(mtype), local); + auto new_body = ensure_sufficient_args_core(body, i+1, margs); + if (!new_body) + return none_expr(); + return some_expr(Pi(local, *new_body)); + } + + /** + \brief Make sure mtype is a Pi of size at least margs.size(). + If it is not, we use ensure_pi and (potentially) add new constaints to enforce it. + */ + optional ensure_sufficient_args(expr const & mtype, buffer const & margs, buffer & cs, justification const & j) { + expr t = mtype; + unsigned num = 0; + while (is_pi(t)) { + num++; + t = binding_body(t); + } + if (num == margs.size()) + return some_expr(mtype);; + lean_assert(!m_tc->next_cnstr()); // make sure there are no pending constraints + // We must create a scope to make sure no constraints "leak" into the current state. + type_checker::scope scope(*m_tc); + auto new_mtype = ensure_sufficient_args_core(mtype, 0, margs); + if (!new_mtype) + return none_expr(); + while (auto c = m_tc->next_cnstr()) + cs.push_back(update_justification(*c, mk_composite1(c->get_justification(), j))); + return new_mtype; + } + /** \brief Given m := a metavariable ?m @@ -867,13 +913,16 @@ struct unifier_fn { - 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) { + void mk_flex_rigid_app_cnstrs(expr const & m, buffer const & margs, expr const & f, expr const & rhs, justification const & j, + buffer & alts) { 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); + expr mtype = mlocal_type(m); + auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j); + if (!new_mtype) return; + mtype = *new_mtype; buffer rargs; get_app_args(rhs, rargs); buffer sargs; @@ -885,7 +934,7 @@ struct unifier_fn { 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()); + alts.push_back(to_list(cs.begin(), cs.end())); } /** @@ -899,23 +948,27 @@ struct unifier_fn { ?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) { + void mk_bindings_imitation(expr const & m, buffer const & margs, expr const & rhs, justification const & j, + buffer & alts) { lean_assert(is_metavar(m)); lean_assert(is_binding(rhs)); - expr const & mtype = mlocal_type(m); - expr maux1 = mk_aux_metavar_for(m_ngen, mtype); buffer cs; + expr mtype = mlocal_type(m); + auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j); + if (!new_mtype) return; + mtype = *new_mtype; + expr maux1 = mk_aux_metavar_for(m_ngen, 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(m_ngen, mtype2); - expr new_local = mk_local(m_ngen.next(), binding_name(rhs), binding_domain(rhs), binding_info(rhs)); + expr new_local = mk_local_for(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()); + alts.push_back(to_list(cs.begin(), cs.end())); } /** @@ -925,12 +978,13 @@ struct unifier_fn { 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) { + void mk_simple_imitation(expr const & m, expr const & rhs, justification const & j, buffer & alts) { 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)); + buffer cs; + cs.push_back(mk_eq_cnstr(m, mk_lambda_for(mtype, rhs), j)); + alts.push_back(to_list(cs.begin(), cs.end())); } /** @@ -944,11 +998,15 @@ struct unifier_fn { (?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) { + void mk_macro_imitation(expr const & m, buffer const & margs, expr const & rhs, justification const & j, + buffer & alts) { lean_assert(is_metavar(m)); lean_assert(is_macro(rhs)); - expr const & mtype = mlocal_type(m); buffer cs; + expr mtype = mlocal_type(m); + auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j); + if (!new_mtype) return; + mtype = *new_mtype; // create an auxiliary metavariable for each macro argument buffer sargs; for (unsigned i = 0; i < macro_num_args(rhs); i++) { @@ -959,7 +1017,7 @@ struct unifier_fn { 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()); + alts.push_back(to_list(cs.begin(), cs.end())); } /** @@ -979,7 +1037,7 @@ struct unifier_fn { to alts as a possible solution when a_i is the same local constant or a metavariable application */ - void add_simple_projections(expr const & m, buffer const & margs, expr const & rhs, justification const & j, + void mk_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)); @@ -991,13 +1049,21 @@ struct unifier_fn { expr const & marg = margs[i]; if ((!is_local(marg) && !is_local(rhs)) || (is_meta(marg) && is_local(rhs))) { // if rhs is not local, then we only add projections for the nonlocal arguments of lhs - constraint c1 = mk_eq_cnstr(marg, rhs, j); - constraint c2 = mk_eq_cnstr(m, mk_lambda_for(mtype, mk_var(vidx)), j); - alts.push_back(constraints({c1, c2})); + buffer cs; + if (auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j)) { + cs.push_back(mk_eq_cnstr(marg, rhs, j)); + expr v = mk_lambda_for(*new_mtype, mk_var(vidx)); + cs.push_back(mk_eq_cnstr(m, v, j)); + alts.push_back(to_list(cs.begin(), cs.end())); + } } else if (is_local(marg) && is_local(rhs) && mlocal_name(marg) == mlocal_name(rhs)) { // if the argument is local, and rhs is equal to it, then we also add a projection - constraint c1 = mk_eq_cnstr(m, mk_lambda_for(mtype, mk_var(vidx)), j); - alts.push_back(constraints(c1)); + buffer cs; + if (auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j)) { + expr v = mk_lambda_for(*new_mtype, mk_var(vidx)); + cs.push_back(mk_eq_cnstr(m, v, j)); + alts.push_back(to_list(cs.begin(), cs.end())); + } } } } @@ -1015,19 +1081,19 @@ struct unifier_fn { 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); + mk_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)); + mk_simple_projections(m, margs, rhs, j, alts); + mk_simple_imitation(m, rhs, j, alts); 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)); + mk_simple_projections(m, margs, rhs, j, alts); + mk_bindings_imitation(m, margs, rhs, j, alts); break; case expr_kind::Macro: - add_simple_projections(m, margs, rhs, j, alts); - alts.push_back(mk_macro_imitation(m, margs, rhs, j)); + mk_simple_projections(m, margs, rhs, j, alts); + mk_macro_imitation(m, margs, rhs, j, alts); break; case expr_kind::App: { expr const & f = get_app_fn(rhs); @@ -1039,11 +1105,11 @@ struct unifier_fn { --i; expr const & marg = margs[i]; 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)); + mk_flex_rigid_app_cnstrs(m, margs, mk_var(vidx), rhs, j, alts); } } else if (is_constant(f)) { - add_simple_projections(m, margs, rhs, j, alts); - alts.push_back(mk_flex_rigid_app_cnstrs(m, margs, f, rhs, j)); + mk_simple_projections(m, margs, rhs, j, alts); + mk_flex_rigid_app_cnstrs(m, margs, f, rhs, j, alts); } else { lean_unreachable(); // LCOV_EXCL_LINE } diff --git a/tests/lean/run/group.lean b/tests/lean/run/group.lean index aae2a0c93..404cc807d 100644 --- a/tests/lean/run/group.lean +++ b/tests/lean/run/group.lean @@ -29,7 +29,7 @@ definition group_to_struct [instance] (g : group) : group_struct (carrier g) check group_struct -definition mul {A : Type} {s : group_struct A} (a b : A) : A +definition mul [inline] {A : Type} {s : group_struct A} (a b : A) : A := group_struct_rec (λ mul one inv h1 h2 h3, mul) s a b infixl `*`:75 := mul diff --git a/tests/lean/run/group2.lean b/tests/lean/run/group2.lean new file mode 100644 index 000000000..3263cb041 --- /dev/null +++ b/tests/lean/run/group2.lean @@ -0,0 +1,60 @@ +import standard +using num + +section + parameter {A : Type} + parameter f : A → A → A + parameter one : A + parameter inv : A → A + infixl `*`:75 := f + postfix `^-1`:100 := inv + definition is_assoc := ∀ a b c, (a*b)*c = a*b*c + definition is_id := ∀ a, a*one = a + definition is_inv := ∀ a, a*a^-1 = one +end + +inductive group_struct (A : Type) : Type := +| mk_group_struct : Π (mul : A → A → A) (one : A) (inv : A → A), is_assoc mul → is_id mul one → is_inv mul one inv → group_struct A + +class group_struct + +inductive group : Type := +| mk_group : Π (A : Type), group_struct A → group + +definition carrier (g : group) : Type +:= group_rec (λ c s, c) g + +definition group_to_struct [instance] (g : group) : group_struct (carrier g) +:= group_rec (λ (A : Type) (s : group_struct A), s) g + +check group_struct + +definition mul [inline] {A : Type} {s : group_struct A} (a b : A) : A +:= group_struct_rec (λ mul one inv h1 h2 h3, mul) s a b + +infixl `*`:75 := mul + +section + variable G1 : group + variable G2 : group + variables a b c : (carrier G2) + variables d e : (carrier G1) + check a * b * b + check d * e +end + +variable pos_real : Type.{1} +variable rmul : pos_real → pos_real → pos_real +variable rone : pos_real +variable rinv : pos_real → pos_real +axiom H1 : is_assoc rmul +axiom H2 : is_id rmul rone +axiom H3 : is_inv rmul rone rinv + +definition real_group_struct [inline] [instance] : group_struct pos_real +:= mk_group_struct rmul rone rinv H1 H2 H3 + +variables x y : pos_real +check x * y +theorem T (a b : pos_real): (rmul a b) = a*b +:= refl (rmul a b)