From 5b1491bdbda75ceb06c6028a4de2d6f574fabd7f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 19 May 2015 12:24:46 -0700 Subject: [PATCH] feat(library/user_recursors): store number of arguments expected by recursor --- src/library/user_recursors.cpp | 16 +++++++++------- src/library/user_recursors.h | 4 +++- 2 files changed, 12 insertions(+), 8 deletions(-) diff --git a/src/library/user_recursors.cpp b/src/library/user_recursors.cpp index 9b8195efb5..bb189bf624 100644 --- a/src/library/user_recursors.cpp +++ b/src/library/user_recursors.cpp @@ -23,10 +23,10 @@ bool recursor_info::is_minor(unsigned pos) const { } recursor_info::recursor_info(name const & r, name const & I, optional const & motive_univ_pos, - bool dep_elim, unsigned major_pos, list const & params_pos, + bool dep_elim, unsigned num_args, unsigned major_pos, list const & params_pos, list const & indices_pos): m_recursor(r), m_type_name(I), m_motive_univ_pos(motive_univ_pos), m_dep_elim(dep_elim), - m_major_pos(major_pos), m_params_pos(params_pos), m_indices_pos(indices_pos) {} + m_num_args(num_args), m_major_pos(major_pos), m_params_pos(params_pos), m_indices_pos(indices_pos) {} recursor_info::recursor_info() {} void recursor_info::write(serializer & s) const { @@ -61,11 +61,13 @@ recursor_info mk_recursor_info(environment const & env, name const & r, optional motive_univ_pos = 0; unsigned major_pos = *inductive::get_elim_major_idx(env, r); unsigned num_indices = *inductive::get_num_indices(env, *I); - unsigned num_parms = *inductive::get_num_params(env, *I); - list params_pos = mk_list_range(0, num_parms); - list indices_pos = mk_list_range(num_parms, num_parms + num_indices); + unsigned num_params = *inductive::get_num_params(env, *I); + unsigned num_minors = *inductive::get_num_minor_premises(env, *I); + unsigned num_args = num_params + 1 /* motive */ + num_minors + num_indices + 1 /* major */; + list params_pos = mk_list_range(0, num_params); + list indices_pos = mk_list_range(num_params, num_params + num_indices); return recursor_info(r, *I, motive_univ_pos, inductive::has_dep_elim(env, *I), - major_pos, params_pos, indices_pos); + num_args, major_pos, params_pos, indices_pos); } declaration d = env.get(r); type_checker tc(env); @@ -196,7 +198,7 @@ recursor_info mk_recursor_info(environment const & env, name const & r, optional lean_assert(*C_univ_pos < length(d.get_univ_params())); } - return recursor_info(r, const_name(I), C_univ_pos, dep_elim, major_pos, + return recursor_info(r, const_name(I), C_univ_pos, dep_elim, tele.size(), major_pos, to_list(params_pos), to_list(indices_pos)); } diff --git a/src/library/user_recursors.h b/src/library/user_recursors.h index b4a6978711..b32520eab2 100644 --- a/src/library/user_recursors.h +++ b/src/library/user_recursors.h @@ -13,6 +13,7 @@ class recursor_info { name m_type_name; optional m_motive_univ_pos; // if none, then recursor can only eliminate to Prop bool m_dep_elim; + unsigned m_num_args; // total number of arguments unsigned m_major_pos; list m_params_pos; // position of the recursor parameters in the major premise list m_indices_pos; // position of the recursor indices in the major premise @@ -21,13 +22,14 @@ public: recursor_info(name const & r, name const & I, optional const & motive_univ_pos, bool dep_elim, - unsigned major_pos, + unsigned num_args, unsigned major_pos, list const & params_pos, list const & indices_pos); recursor_info(); name const & get_name() const { return m_recursor; } name const & get_type_name() const { return m_type_name; } + unsigned get_num_args() const { return m_num_args; } unsigned get_num_params() const { return length(m_params_pos); } unsigned get_num_indices() const { return length(m_indices_pos); } unsigned get_motive_pos() const { return get_num_params(); }