From ff73fb22fb20e30a21c8a833e90cb0b6657a9f63 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 15 Nov 2015 12:07:44 -0800 Subject: [PATCH] feat(library/user_recursors): store whether recursor is recursive or not --- src/frontends/lean/builtin_cmds.cpp | 2 ++ src/library/user_recursors.cpp | 30 +++++++++++++++++++++-------- src/library/user_recursors.h | 4 +++- tests/lean/run/user_recursor.lean | 16 +++++++++++++++ 4 files changed, 43 insertions(+), 9 deletions(-) create mode 100644 tests/lean/run/user_recursor.lean diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 0f30e9913..1e6db8747 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -301,6 +301,8 @@ static void print_recursor_info(parser & p) { out << "recursor information\n" << " num. parameters: " << info.get_num_params() << "\n" << " num. indices: " << info.get_num_indices() << "\n" + << " num. minors: " << info.get_num_minors() << "\n" + << " recursive: " << info.is_recursive() << "\n" << " universe param pos.: "; for (unsigned idx : info.get_universe_pos()) { if (idx == recursor_info::get_motive_univ_idx()) { diff --git a/src/library/user_recursors.cpp b/src/library/user_recursors.cpp index 559f5e283..e2536c730 100644 --- a/src/library/user_recursors.cpp +++ b/src/library/user_recursors.cpp @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include #include #include "util/sstream.h" +#include "kernel/find_fn.h" #include "kernel/inductive/inductive.h" #include "library/scoped_ext.h" #include "library/util.h" @@ -33,16 +34,16 @@ unsigned recursor_info::get_num_minors() const { } recursor_info::recursor_info(name const & r, name const & I, list const & univ_pos, - bool dep_elim, unsigned num_args, unsigned major_pos, + bool dep_elim, bool is_rec, unsigned num_args, unsigned major_pos, list> const & params_pos, list const & indices_pos, list const & produce_motive): - m_recursor(r), m_type_name(I), m_universe_pos(univ_pos), m_dep_elim(dep_elim), + m_recursor(r), m_type_name(I), m_universe_pos(univ_pos), m_dep_elim(dep_elim), m_recursive(is_rec), m_num_args(num_args), m_major_pos(major_pos), m_params_pos(params_pos), m_indices_pos(indices_pos), m_produce_motive(produce_motive) {} recursor_info::recursor_info() {} void recursor_info::write(serializer & s) const { - s << m_recursor << m_type_name << m_dep_elim << m_num_args << m_major_pos; + s << m_recursor << m_type_name << m_dep_elim << m_recursive << m_num_args << m_major_pos; write_list(s, m_universe_pos); write_list(s, m_params_pos); write_list(s, m_indices_pos); @@ -51,7 +52,7 @@ void recursor_info::write(serializer & s) const { recursor_info recursor_info::read(deserializer & d) { recursor_info info; - d >> info.m_recursor >> info.m_type_name >> info.m_dep_elim + d >> info.m_recursor >> info.m_type_name >> info.m_dep_elim >> info.m_recursive >> info.m_num_args >> info.m_major_pos; info.m_universe_pos = read_list(d); info.m_params_pos = read_list>(d); @@ -76,6 +77,7 @@ recursor_info mk_recursor_info(environment const & env, name const & r, optional list universe_pos = mk_list_range(0, num_univ_params); if (env.get(name(*I, "rec")).get_num_univ_params() != num_univ_params) universe_pos = cons(recursor_info::get_motive_univ_idx(), universe_pos); + bool is_rec = is_recursive_datatype(env, *I); unsigned major_pos = *inductive::get_elim_major_idx(env, r); unsigned num_indices = *inductive::get_num_indices(env, *I); unsigned num_params = *inductive::get_num_params(env, *I); @@ -87,7 +89,7 @@ recursor_info mk_recursor_info(environment const & env, name const & r, optional list> params_pos = map2>(mk_list_range(0, num_params), [](unsigned i) { return optional(i); }); list indices_pos = mk_list_range(num_params, num_params + num_indices); - return recursor_info(r, *I, universe_pos, inductive::has_dep_elim(env, *I), + return recursor_info(r, *I, universe_pos, inductive::has_dep_elim(env, *I), is_rec, num_args, major_pos, params_pos, indices_pos, produce_motive); } declaration d = env.get(r); @@ -237,11 +239,23 @@ recursor_info mk_recursor_info(environment const & env, name const & r, optional buffer produce_motive; unsigned nparams = params_pos.size(); unsigned nindices = indices_pos.size(); + bool is_rec = false; for (unsigned i = nparams+1; i < tele.size(); i++) { if (i < major_pos - nindices || i > major_pos) { // i is a minor premise - buffer tmp; - expr res = get_app_fn(to_telescope(tc, mlocal_type(tele[i]), tmp)); + buffer minor_args; + expr res = get_app_fn(to_telescope(tc, mlocal_type(tele[i]), minor_args)); + if (!is_rec) { + for (expr const & minor_arg : minor_args) { + lean_assert(is_local(minor_arg)); + if (find(mlocal_type(minor_arg), [&](expr const & e, unsigned) { + return is_local(e) && mlocal_name(C) == mlocal_name(e); + })) { + is_rec = true; + break; + } + } + } if (is_local(res) && mlocal_name(C) == mlocal_name(res)) { produce_motive.push_back(true); } else { @@ -250,7 +264,7 @@ recursor_info mk_recursor_info(environment const & env, name const & r, optional } } - return recursor_info(r, const_name(I), to_list(univ_param_pos), dep_elim, tele.size(), major_pos, + return recursor_info(r, const_name(I), to_list(univ_param_pos), dep_elim, is_rec, tele.size(), major_pos, to_list(params_pos), to_list(indices_pos), to_list(produce_motive)); } diff --git a/src/library/user_recursors.h b/src/library/user_recursors.h index 5b36b023d..d0e28b3d6 100644 --- a/src/library/user_recursors.h +++ b/src/library/user_recursors.h @@ -13,6 +13,7 @@ class recursor_info { name m_type_name; list m_universe_pos; // position of the recursor universe level parameters. bool m_dep_elim; + bool m_recursive; unsigned m_num_args; // total number of arguments unsigned m_major_pos; // if param is , then it should be resolved by type class resolution @@ -23,7 +24,7 @@ class recursor_info { public: recursor_info(name const & r, name const & I, list const & univ_pos, - bool dep_elim, unsigned num_args, unsigned major_pos, + bool dep_elim, bool is_rec, unsigned num_args, unsigned major_pos, list> const & params_pos, list const & indices_pos, list const & produce_motive); recursor_info(); @@ -47,6 +48,7 @@ public: list const & get_indices_pos() const { return m_indices_pos; } list const & get_produce_motive() const { return m_produce_motive; } bool has_dep_elim() const { return m_dep_elim; } + bool is_recursive() const { return m_recursive; } bool is_minor(unsigned pos) const; unsigned get_num_minors() const; diff --git a/tests/lean/run/user_recursor.lean b/tests/lean/run/user_recursor.lean new file mode 100644 index 000000000..ef6dab08f --- /dev/null +++ b/tests/lean/run/user_recursor.lean @@ -0,0 +1,16 @@ +import data.finset +check @and.rec + +definition and.rec2 [recursor 4] {p r : Prop} (H₁ : p → r) (H₂ : p ∧ p) : r := +and.rec_on H₂ (λ h₁ h₁, H₁ h₁) + +set_option pp.all true +check ∃ x : nat, x = x + +print [recursor] and.rec2 +print [recursor] or.rec +print [recursor] and.rec +print [recursor] nat.rec +print [recursor] finset.induction +print [recursor] list.rec +print [recursor] Exists.rec