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

feat(util/list): improved filter that reuses list cells

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-14 20:15:37 -08:00
parent bdbf85405a
commit 1b1032eb99
2 changed files with 21 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/tests/util/list.cpp
View file

@ -209,6 +209,15 @@ static void tst16() {
lean_assert_eq(map(list<int>(), [](int i) { return i + 10; }), list<int>());
}
static void tst17() {
list<int> l({1, 2, 3, 4});
lean_assert(is_eqp(filter(l, [](int v) { return v < 10; }), l));
list<int> l2(filter(l, [](int v) { return v != 1; }));
lean_assert(is_eqp(tail(l), l2));
list<int> l3(filter(l, [](int v) { return v != 2; }));
lean_assert(is_eqp(tail(tail(l)), tail(l2)));
}
int main() {
tst1();
tst2();
@ -226,5 +235,6 @@ int main() {
tst14();
tst15();
tst16();
tst17();
return has_violations() ? 1 : 0;
}

16
src/util/list_fn.h
View file

@ -158,7 +158,7 @@ list<T> map(list<T> const & l, F && f) {
/**
\brief Filter/Remove elements from the list
that satisfy the given predicate.
that do not satisfy the given predicate.
*/
template<typename T, typename P>
list<T> filter(list<T> const & l, P && p) {
@ -168,13 +168,19 @@ list<T> filter(list<T> const & l, P && p) {
buffer<typename list<T>::cell*> tmp;
to_buffer(l, tmp);
unsigned i = tmp.size();
list<T> r;
while (i > 0) {
--i;
if (p(tmp[i]->head()))
r = cons(tmp[i]->head(), r);
if (!p(tmp[i]->head())) {
list<T> r = tmp[i]->tail();
while (i > 0) {
--i;
if (p(tmp[i]->head()))
r = cons(tmp[i]->head(), r);
}
return r;
}
}
return r;
return l; // not element was removed
}
}