From dcf7cf00ff4d859745874129b6188a75bbcfa3c3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 6 Jul 2014 16:46:34 -0700 Subject: [PATCH] fix(*): bugs in the type checker, inductive datatypes, and unifier The bugs were indentified when performing the tiny change in the file tests/lean/run/group.lean --- src/kernel/inductive/inductive.cpp | 37 ++++++-- src/kernel/inductive/inductive.h | 4 + src/kernel/type_checker.cpp | 105 ++++++++++------------- src/kernel/type_checker.h | 26 +++++- src/library/inductive_unifier_plugin.cpp | 58 ++++++------- src/library/unifier.cpp | 63 +++----------- tests/lean/run/group.lean | 4 +- 7 files changed, 138 insertions(+), 159 deletions(-) diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp index 5a839bc7d..2c5dea150 100644 --- a/src/kernel/inductive/inductive.cpp +++ b/src/kernel/inductive/inductive.cpp @@ -765,9 +765,10 @@ optional inductive_normalizer_extension::operator()(expr const & e, extens return none_expr(); // it is not an eliminator buffer elim_args; get_app_args(e, elim_args); - if (elim_args.size() != it1->m_num_ACe + it1->m_num_indices + 1) - return none_expr(); // number of arguments does not match - expr intro_app = ctx.whnf(elim_args.back()); + unsigned major_idx = it1->m_num_ACe + it1->m_num_indices; + if (elim_args.size() < major_idx + 1) + return none_expr(); // major premise is missing + expr intro_app = ctx.whnf(elim_args[major_idx]); expr const & intro_fn = get_app_fn(intro_app); // Last argument must be a constant and an application of a constant. if (!is_constant(intro_fn)) @@ -800,11 +801,15 @@ optional inductive_normalizer_extension::operator()(expr const & e, extens std::reverse(ACebu.begin(), ACebu.end()); expr r = instantiate_univ_params(it2->m_comp_rhs_body, it1->m_level_names, const_levels(elim_fn)); r = instantiate(r, ACebu.size(), ACebu.data()); + if (elim_args.size() > major_idx + 1) { + unsigned num_args = elim_args.size() - major_idx - 1; + r = mk_app(r, num_args, elim_args.data() + major_idx + 1); + } return some_expr(r); } -// Return true if \c e is of the form (elim ... (?m ...)) -bool inductive_normalizer_extension::may_reduce_later(expr const & e, extension_context & ctx) const { +template +bool is_elim_meta_app_core(Ctx & ctx, expr const & e) { inductive_env_ext const & ext = get_extension(ctx.env()); expr const & elim_fn = get_app_fn(e); if (!is_constant(elim_fn)) @@ -814,12 +819,22 @@ bool inductive_normalizer_extension::may_reduce_later(expr const & e, extension_ return false; buffer elim_args; get_app_args(e, elim_args); - if (elim_args.size() != it1->m_num_ACe + it1->m_num_indices + 1) + unsigned major_idx = it1->m_num_ACe + it1->m_num_indices; + if (elim_args.size() < major_idx + 1) return false; - expr intro_app = ctx.whnf(elim_args.back()); + expr intro_app = ctx.whnf(elim_args[major_idx]); return is_meta(intro_app); } +bool is_elim_meta_app(type_checker & tc, expr const & e) { + return is_elim_meta_app_core(tc, e); +} + +// Return true if \c e is of the form (elim ... (?m ...)) +bool inductive_normalizer_extension::may_reduce_later(expr const & e, extension_context & ctx) const { + return is_elim_meta_app_core(ctx, e); +} + optional is_inductive_decl(environment const & env, name const & n) { inductive_env_ext const & ext = get_extension(env); if (auto it = ext.m_inductive_info.find(n)) @@ -843,5 +858,13 @@ optional is_elim_rule(environment const & env, name const & n) { else return optional(); } + +optional get_elim_major_idx(environment const & env, name const & n) { + inductive_env_ext const & ext = get_extension(env); + if (auto it = ext.m_elim_info.find(n)) + return optional(it->m_num_ACe + it->m_num_indices); + else + return optional(); +} } } diff --git a/src/kernel/inductive/inductive.h b/src/kernel/inductive/inductive.h index 11db07038..61e01f223 100644 --- a/src/kernel/inductive/inductive.h +++ b/src/kernel/inductive/inductive.h @@ -62,5 +62,9 @@ optional is_intro_rule(environment const & env, name const & n); s.t. \c n is an elimination rule of D. Otherwise, return none. */ optional is_elim_rule(environment const & env, name const & n); + +/** \brief Given the eliminator \c n, this function return the position of major premise */ +optional get_elim_major_idx(environment const & env, name const & n); +bool is_elim_meta_app(type_checker & tc, expr const & e); } } diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 48cf275ea..a9ff3c3f7 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -24,6 +24,37 @@ Author: Leonardo de Moura namespace lean { static name g_x_name("x"); +expr replace_range(expr const & type, expr const & new_range) { + if (is_pi(type)) + return update_binding(type, binding_domain(type), replace_range(binding_body(type), new_range)); + else + return new_range; +} + +/** \brief Return the "arity" of the given type. The arity is the number of nested pi-expressions. */ +static unsigned get_arity(expr type) { + unsigned r = 0; + while (is_pi(type)) { + type = binding_body(type); + r++; + } + return r; +} + +expr mk_aux_type_metavar_for(name_generator & ngen, expr const & t) { + expr new_type = replace_range(t, mk_sort(mk_meta_univ(ngen.next()))); + name n = ngen.next(); + return mk_metavar(n, new_type); +} + +expr mk_aux_metavar_for(name_generator & ngen, expr const & t) { + unsigned num = get_arity(t); + expr r = mk_app_vars(mk_aux_type_metavar_for(ngen, t), num); + expr new_type = replace_range(t, r); + name n = ngen.next(); + return mk_metavar(n, new_type); +} + type_checker::scope::scope(type_checker & tc): m_tc(tc), m_keep(false) { m_tc.push(); @@ -68,48 +99,6 @@ optional type_checker::next_cnstr() { } } -/** - \brief Given a metavariable application ((?m t_1) ... t_k) - Create a telescope with the types of t_1 ... t_k. - If t_i is a local constant, then we abstract the occurrences of t_i in the types of t_{i+1} ... t_k. - Return false if the telescope still contains local constants after the abstraction step. -*/ -bool type_checker::meta_to_telescope(expr const & e, buffer & telescope) { - lean_assert(is_meta(e)); - lean_assert(closed(e)); - buffer> locals; - return meta_to_telescope_core(e, telescope, locals); -} - -/** \brief Auxiliary method for meta_to_telescope */ -bool type_checker::meta_to_telescope_core(expr const & e, buffer & telescope, buffer> & locals) { - lean_assert(is_meta(e)); - if (is_app(e)) { - if (!meta_to_telescope_core(app_fn(e), telescope, locals)) - return false; - // infer type and abstract local constants - unsigned n = locals.size(); - expr t = replace(infer_type(app_arg(e)), - [&](expr const & e, unsigned offset) -> optional { - if (is_local(e)) { - for (unsigned i = 0; i < n; i++) { - if (locals[i] && is_eqp(*locals[i], e)) - return some_expr(mk_var(offset + n - i - 1)); - } - } - return none_expr(); - }); - if (has_local(t)) - return false; - telescope.push_back(t); - if (is_local(e)) - locals.push_back(some_expr(e)); - else - locals.push_back(none_expr()); - } - return true; -} - /** \brief Make sure \c e "is" a sort, and return the corresponding sort. If \c e is not a sort, then the whnf procedure is invoked. Then, there are @@ -150,25 +139,19 @@ expr type_checker::ensure_pi_core(expr e, expr const & s) { if (is_pi(e)) { return e; } else if (is_meta(e)) { - buffer telescope; - if (!meta_to_telescope(e, telescope)) { - environment env = m_env; - throw_kernel_exception(env, s, - [=](formatter const & fmt, options const & o) { return pp_function_expected(fmt, env, o, s); }); - } - expr ta = mk_sort(mk_meta_univ(m_gen.next())); - expr A = mk_metavar(m_gen.next(), mk_pi(telescope, ta)); - expr A_xs = mk_app_vars(A, telescope.size()); - telescope.push_back(A_xs); - expr tb = mk_sort(mk_meta_univ(m_gen.next())); - expr B = mk_metavar(m_gen.next(), mk_pi(telescope, tb)); - buffer args; - get_app_args(e, args); - expr A_args = mk_app(A, args.size(), args.data()); - args.push_back(Var(0)); - expr B_args = mk_app(B, args.size(), args.data()); - expr r = mk_pi(g_x_name, A_args, B_args); - justification j = mk_justification(s, + 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); + 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 42785478d..73e7eca42 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -16,6 +16,30 @@ Author: Leonardo de Moura #include "kernel/converter.h" namespace lean { + +/** \brief Given \c type of the form (Pi ctx, r), return (Pi ctx, new_range) */ +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] + return a new metavariable \c m1 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_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] + 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} + where \c u is a new universe metavariable. +*/ +expr mk_aux_metavar_for(name_generator & ngen, expr const & t); + /** \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. @@ -59,8 +83,6 @@ class type_checker { optional expand_macro(expr const & m); std::pair open_binding_body(expr const & e); void add_cnstr(constraint const & c); - bool meta_to_telescope(expr const & e, buffer & telescope); - bool meta_to_telescope_core(expr const & e, buffer & telescope, buffer> & locals); expr ensure_sort_core(expr e, expr const & s); expr ensure_pi_core(expr e, expr const & s); justification mk_macro_jst(expr const & e); diff --git a/src/library/inductive_unifier_plugin.cpp b/src/library/inductive_unifier_plugin.cpp index 10ad8cdf7..e74ee768c 100644 --- a/src/library/inductive_unifier_plugin.cpp +++ b/src/library/inductive_unifier_plugin.cpp @@ -11,36 +11,26 @@ Author: Leonardo de Moura namespace lean { class inductive_unifier_plugin_cell : public unifier_plugin_cell { - /** \brief Return true iff \c e is of the form (elim ... (?m ...)) */ - bool is_elim_meta_app(type_checker & tc, expr const & e) const { - if (!is_app(e)) - return false; - expr const & f = get_app_fn(e); - if (!is_constant(f)) - return false; - auto it_name = inductive::is_elim_rule(tc.env(), const_name(f)); - if (!it_name) - return false; - if (!is_meta(app_arg(e))) - return false; - if (is_pi(tc.whnf(tc.infer(e)))) - return false; - return true; - } - - /** \brief Return true iff the lhs or rhs of the constraint c is of the form (elim ... (?m ...)) */ + /** \brief Return true iff the lhs or rhs of the constraint c is of the form (elim ... (?m ...) ...) */ bool is_elim_meta_cnstr(type_checker & tc, constraint const & c) const { - return is_eq_cnstr(c) && (is_elim_meta_app(tc, cnstr_lhs_expr(c)) || is_elim_meta_app(tc, cnstr_rhs_expr(c))); + return is_eq_cnstr(c) && (inductive::is_elim_meta_app(tc, cnstr_lhs_expr(c)) || + inductive::is_elim_meta_app(tc, cnstr_rhs_expr(c))); } - /** \brief Return true iff \c e is of the form (?m ... (intro ...)) */ + /** \brief Return true iff \c e is of the form (?m ... (intro ...) ...) */ bool is_meta_intro_app(type_checker & tc, expr const & e) const { if (!is_app(e) || !is_meta(e)) return false; - expr arg = get_app_fn(app_arg(e)); - if (!is_constant(arg)) - return false; - return (bool) inductive::is_intro_rule(tc.env(), const_name(arg)); // NOLINT + buffer args; + get_app_args(e, args); + for (expr const & a : args) { + expr arg = get_app_fn(a); + if (!is_constant(arg)) + continue; + if (inductive::is_intro_rule(tc.env(), const_name(arg))) + return true; + } + return false; } /** \brief Return true iff the lhs or rhs of the constraint c is of the form (?m ... (intro ...)) */ @@ -50,21 +40,21 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell { /** \brief Given (elim args) =?= t, where elim is the eliminator/recursor for the inductive declaration \c decl, - and the last argument of args is of the form (?m ...), we create a case split where we try to assign (?m ...) + and the major premise is of the form (?m ...), we create a case split where we try to assign (?m ...) to the different constructors of decl. */ lazy_list add_elim_meta_cnstrs(type_checker & tc, name_generator ngen, inductive::inductive_decl const & decl, expr const & elim, buffer & args, expr const & t, justification const & j) const { lean_assert(is_constant(elim)); + environment const & env = tc.env(); levels elim_lvls = const_levels(elim); unsigned elim_num_lvls = length(elim_lvls); - unsigned num_args = args.size(); - expr meta = args[num_args - 1]; // save last argument, we will update it + unsigned major_idx = *inductive::get_elim_major_idx(env, const_name(elim)); + expr meta = args[major_idx]; // save this argument, we will update it lean_assert(is_meta(meta)); buffer margs; expr const & m = get_app_args(meta, margs); expr const & mtype = mlocal_type(m); - environment const & env = tc.env(); buffer alts; for (auto const & intro : inductive::inductive_decl_intros(decl)) { name const & intro_name = inductive::intro_rule_name(intro); @@ -83,10 +73,10 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell { hint = mk_app(hint, mk_app(mk_aux_metavar_for(ngen, mtype), margs)); intro_type = tc.whnf(binding_body(intro_type)); } - constraint c1 = mk_eq_cnstr(meta, hint, j); - args[num_args - 1] = hint; + constraint c1 = mk_eq_cnstr(meta, hint, j); + args[major_idx] = hint; expr reduce_elim = tc.whnf(mk_app(elim, args)); - constraint c2 = mk_eq_cnstr(reduce_elim, t, j); + constraint c2 = mk_eq_cnstr(reduce_elim, t, j); alts.push_back(constraints({c1, c2})); } return to_lazy(to_list(alts.begin(), alts.end())); @@ -94,7 +84,7 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell { lazy_list process_elim_meta_core(type_checker & tc, name_generator const & ngen, expr const & lhs, expr const & rhs, justification const & j) const { - lean_assert(is_elim_meta_app(tc, lhs)); + lean_assert(inductive::is_elim_meta_app(tc, lhs)); buffer args; expr const & elim = get_app_args(lhs, args); environment const & env = tc.env(); @@ -116,9 +106,9 @@ public: expr const & lhs = cnstr_lhs_expr(c); expr const & rhs = cnstr_rhs_expr(c); justification const & j = c.get_justification(); - if (is_elim_meta_app(tc, lhs)) + if (inductive::is_elim_meta_app(tc, lhs)) return process_elim_meta_core(tc, ngen, lhs, rhs, j); - else if (is_elim_meta_app(tc, rhs)) + else if (inductive::is_elim_meta_app(tc, rhs)) return process_elim_meta_core(tc, ngen, rhs, lhs, j); else return lazy_list(); diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index e8a2290b2..ccc9866c1 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -190,55 +190,6 @@ std::pair unify_simple(substitution const & s, const return mk_pair(unify_status::Unsupported, s); } - -/** \brief Given \c type of the form (Pi ctx, r), return (Pi ctx, new_range) */ -static expr replace_range(expr const & type, expr const & new_range) { - if (is_pi(type)) - return update_binding(type, binding_domain(type), replace_range(binding_body(type), new_range)); - else - return new_range; -} - -/** \brief Return the "arity" of the given type. The arity is the number of nested pi-expressions. */ -static unsigned get_arity(expr type) { - unsigned r = 0; - while (is_pi(type)) { - type = binding_body(type); - r++; - } - return r; -} - -/** - \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] - return a new metavariable \c m1 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_type_metavar_for(name_generator & ngen, expr const & t) { - expr new_type = replace_range(t, mk_sort(mk_meta_univ(ngen.next()))); - name n = ngen.next(); - return mk_metavar(n, new_type); -} - -/** - \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] - 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} - where \c u is a new universe metavariable. -*/ -expr mk_aux_metavar_for(name_generator & ngen, expr const & t) { - unsigned num = get_arity(t); - expr r = mk_app_vars(mk_aux_type_metavar_for(ngen, t), num); - expr new_type = replace_range(t, r); - name n = ngen.next(); - return mk_metavar(n, new_type); -} - static constraint g_dont_care_cnstr = mk_eq_cnstr(expr(), expr(), justification()); /** @@ -740,11 +691,15 @@ struct unifier_fn { } } + void pop_case_split() { + m_tc->pop(); + m_case_splits.pop_back(); + } + bool resolve_conflict() { lean_assert(in_conflict()); - // Remark: we must save the value of m_conflict because d->next(*this) may change it. - justification conflict = *m_conflict; while (!m_case_splits.empty()) { + justification conflict = *m_conflict; std::unique_ptr & d = m_case_splits.back(); if (depends_on(conflict, d->m_assumption_idx)) { d->m_failed_justifications = mk_composite1(d->m_failed_justifications, conflict); @@ -752,9 +707,9 @@ struct unifier_fn { reset_conflict(); return true; } + } else { + pop_case_split(); } - m_tc->pop(); - m_case_splits.pop_back(); } return false; } @@ -784,6 +739,7 @@ struct unifier_fn { } else { // update conflict update_conflict(mk_composite1(*m_conflict, cs.m_failed_justifications)); + pop_case_split(); return false; } } @@ -830,6 +786,7 @@ struct unifier_fn { } else { // update conflict update_conflict(mk_composite1(*m_conflict, cs.m_failed_justifications)); + pop_case_split(); return false; } } diff --git a/tests/lean/run/group.lean b/tests/lean/run/group.lean index 23eb74df6..aae2a0c93 100644 --- a/tests/lean/run/group.lean +++ b/tests/lean/run/group.lean @@ -29,8 +29,8 @@ definition group_to_struct [instance] (g : group) : group_struct (carrier g) check group_struct -definition mul {A : Type} {s : group_struct A} : A → A → A -:= group_struct_rec (λ mul one inv h1 h2 h3, mul) s +definition mul {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