michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/user_recursors): add get_num_minors

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-15 11:35:55 -08:00
parent ccdaa524f7
commit eae26cdfae
2 changed files with 11 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/library/user_recursors.cpp
View file

@ -22,6 +22,16 @@ bool recursor_info::is_minor(unsigned pos) const {
return true; return true;
} }
unsigned recursor_info::get_num_minors() const {
unsigned r = m_num_args;
lean_assert(r >= get_motive_pos());
r -= get_motive_pos();
lean_assert(m_major_pos >= get_first_index_pos());
lean_assert(r >= m_major_pos - get_first_index_pos() + 1);
r -= (m_major_pos - get_first_index_pos() + 1);
return r;
}
recursor_info::recursor_info(name const & r, name const & I, list<unsigned> const & univ_pos, recursor_info::recursor_info(name const & r, name const & I, list<unsigned> const & univ_pos,
bool dep_elim, unsigned num_args, unsigned major_pos, bool dep_elim, unsigned num_args, unsigned major_pos,
list<optional<unsigned>> const & params_pos, list<unsigned> const & indices_pos, list<optional<unsigned>> const & params_pos, list<unsigned> const & indices_pos,

2
src/library/user_recursors.h
View file

@ -42,13 +42,13 @@ public:
unsigned get_motive_pos() const { return get_num_params(); } unsigned get_motive_pos() const { return get_num_params(); }
unsigned get_first_index_pos() const { return m_major_pos - get_num_indices(); } unsigned get_first_index_pos() const { return m_major_pos - get_num_indices(); }
unsigned get_major_pos() const { return m_major_pos; } unsigned get_major_pos() const { return m_major_pos; }
/** \brief Return position of the recursor parameters in the major premise. */
list<optional<unsigned>> const & get_params_pos() const { return m_params_pos; } list<optional<unsigned>> const & get_params_pos() const { return m_params_pos; }
/** \brief Return position of the recursor indices in the major premise. */ /** \brief Return position of the recursor indices in the major premise. */
list<unsigned> const & get_indices_pos() const { return m_indices_pos; } list<unsigned> const & get_indices_pos() const { return m_indices_pos; }
list<bool> const & get_produce_motive() const { return m_produce_motive; } list<bool> const & get_produce_motive() const { return m_produce_motive; }
bool has_dep_elim() const { return m_dep_elim; } bool has_dep_elim() const { return m_dep_elim; }
bool is_minor(unsigned pos) const; bool is_minor(unsigned pos) const;
unsigned get_num_minors() const;
void write(serializer & s) const; void write(serializer & s) const;
static recursor_info read(deserializer & d); static recursor_info read(deserializer & d);