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

Add iterator for traversing local objects (i.e., ignores objects defined in ancestor environments)

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-15 09:29:42 -07:00
parent 2b7834c5fc
commit 013fa866fa
3 changed files with 85 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
src/kernel/environment.cpp
View file

@ -341,6 +341,26 @@ struct environment::imp {
}
}
unsigned get_num_objects(bool local) const {
if (local || !has_parent()) {
return m_objects.size();
} else {
return m_objects.size() + m_parent->get_num_objects(false);
}
}
object const & get_object(unsigned i, bool local) const {
if (local || !has_parent()) {
return *(m_objects[i]);
} else {
unsigned num_parent_objects = m_parent->get_num_objects(false);
if (i >= num_parent_objects)
return *(m_objects[i - num_parent_objects]);
else
return m_parent->get_object(i, false);
}
}
/** \brief Display universal variable constraints and objects stored in this environment and its parents. */
void display(std::ostream & out, environment const & env) const {
if (has_parent())
@ -468,12 +488,12 @@ named_object const * environment::get_object_ptr(name const & n) const {
return m_imp->get_object_ptr(n);
}
unsigned environment::get_num_objects() const {
return m_imp->m_objects.size();
unsigned environment::get_num_objects(bool local) const {
return m_imp->get_num_objects(local);
}
object const & environment::get_object(unsigned i) const {
return *(m_imp->m_objects[i]);
object const & environment::get_object(unsigned i, bool local) const {
return m_imp->get_object(i, local);
}
void environment::display(std::ostream & out) const {

45
src/kernel/environment.h
View file

@ -24,8 +24,8 @@ private:
void check_type(name const & n, expr const & t, expr const & v);
explicit environment(std::shared_ptr<imp> const & ptr);
explicit environment(imp * new_ptr);
unsigned get_num_objects() const;
object const & get_object(unsigned i) const;
unsigned get_num_objects(bool local) const;
object const & get_object(unsigned i, bool local) const;
public:
environment();
~environment();
@ -140,22 +140,49 @@ public:
class object_iterator {
environment const & m_env;
unsigned m_idx;
bool m_local;
friend class environment;
object_iterator(environment const & env, unsigned idx):m_env(env), m_idx(idx) {}
object_iterator(environment const & env, unsigned idx, bool local):m_env(env), m_idx(idx), m_local(local) {}
public:
object_iterator(object_iterator const & s):m_env(s.m_env), m_idx(s.m_idx) {}
object_iterator(object_iterator const & s):m_env(s.m_env), m_idx(s.m_idx), m_local(s.m_local) {}
object_iterator & operator++() { ++m_idx; return *this; }
object_iterator operator++(int) { object_iterator tmp(*this); operator++(); return tmp; }
bool operator==(object_iterator const & s) const { lean_assert(&m_env == &(s.m_env)); return m_idx == s.m_idx; }
bool operator!=(object_iterator const & s) const { return !operator==(s); }
object const & operator*() { return m_env.get_object(m_idx); }
object const & operator*() { return m_env.get_object(m_idx, m_local); }
};
/** \brief Return an iterator to the beginning of the sequence of objects stored in this environment */
object_iterator begin_objects() const { return object_iterator(*this, 0); }
/**
\brief Return an iterator to the beginning of the sequence of
objects stored in this environment.
/** \brief Return an iterator to the end of the sequence of objects stored in this environment */
object_iterator end_objects() const { return object_iterator(*this, get_num_objects()); }
\remark The objects in this environment and ancestor
environments are considered
*/
object_iterator begin_objects() const { return object_iterator(*this, 0, false); }
/**
\brief Return an iterator to the end of the sequence of
objects stored in this environment.
\remark The objects in this environment and ancestor
environments are considered
*/
object_iterator end_objects() const { return object_iterator(*this, get_num_objects(false), false); }
/**
\brief Return an iterator to the beginning of the sequence of
objects stored in this environment (objects in ancestor
environments are ingored).
*/
object_iterator begin_local_objects() const { return object_iterator(*this, 0, true); }
/**
\brief Return an iterator to the end of the sequence of
objects stored in this environment (objects in ancestor
environments are ingored).
*/
object_iterator end_local_objects() const { return object_iterator(*this, get_num_objects(true), true); }
// =======================================
/** \brief Display universal variable constraints and objects stored in this environment and its parents. */

25
src/tests/kernel/environment.cpp
View file

@ -168,6 +168,30 @@ static void tst7() {
std::cout << "Environment\n" << env;
}
static void tst8() {
environment env;
std::cout << "=======================\n";
env.add_var("a", Type());
env.add_var("b", Type());
environment env2 = env.mk_child();
env2.add_var("c", Type());
env2.add_var("d", Type());
env2.add_var("e", Type());
unsigned counter = 0;
std::for_each(env2.begin_local_objects(), env2.end_local_objects(), [&](object const & obj) { std::cout << obj.pp(env2) << "\n"; counter++; });
lean_assert(counter == 3);
std::cout << "=======================\n";
counter = 0;
std::for_each(env2.begin_objects(), env2.end_objects(), [&](object const & obj) { std::cout << obj.pp(env2) << "\n"; counter++; });
lean_assert(counter == 5);
environment env3 = env2.mk_child();
env3.add_var("f", Type() >> Type());
std::cout << "=======================\n";
counter = 0;
std::for_each(env3.begin_objects(), env3.end_objects(), [&](object const & obj) { std::cout << obj.pp(env3) << "\n"; counter++; });
lean_assert(counter == 6);
}
int main() {
enable_trace("is_convertible");
tst1();
@ -177,5 +201,6 @@ int main() {
tst5();
tst6();
tst7();
tst8();
return has_violations() ? 1 : 0;
}