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

Use split_reverse_second instead of split and then reverse in queue

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-11 14:10:39 -07:00
parent 37498f9fb8
commit ed15a2df9b
3 changed files with 30 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/util/list.h
View file

@ -133,4 +133,12 @@ template<typename It> list<typename std::iterator_traits<It>::value_type> to_lis
}
return r;
}
/** \brief Return <tt>reverse(to_list(begin, end))</tt> */
template<typename It> list<typename std::iterator_traits<It>::value_type> reverse_to_list(It const & begin, It const & end) {
list<typename std::iterator_traits<It>::value_type> r;
for (auto it = begin; it != end; ++it)
r = cons(*it, r);
return r;
}
}

20
src/util/list_fn.h
View file

@ -60,6 +60,26 @@ std::pair<list<T>, list<T>> split(list<T> const & l) {
}
}
/**
\brief Return two lists \c l1 and \c l2 of approximately the same size s.t.
<tt>append(l1, reverse(l2)) == l</tt>
*/
template<typename T>
std::pair<list<T>, list<T>> split_reverse_second(list<T> const & l) {
if (is_nil(l)) {
return mk_pair(l, l);
} else if (is_nil(cdr(l))) {
return mk_pair(l, list<T>());
} else {
buffer<T> tmp;
to_buffer(l, tmp);
unsigned mid = tmp.size() / 2;
auto beg = tmp.begin();
lean_assert(beg + mid <= tmp.end());
return mk_pair(to_list(beg, beg + mid), reverse_to_list(beg+mid, tmp.end()));
}
}
/**
\brief Append two lists
*/

6
src/util/queue.h
View file

@ -45,8 +45,7 @@ public:
if (is_nil(cdr(q.m_rear))) {
return mk_pair(queue(), car(q.m_rear));
} else {
auto p = split(q.m_rear);
p.second = reverse(p.second);
auto p = split_reverse_second(q.m_rear);
return mk_pair(queue(cdr(p.second), p.first), car(p.second));
}
} else {
@ -66,8 +65,7 @@ public:
if (is_nil(cdr(q.m_front))) {
return mk_pair(queue(), car(q.m_front));
} else {
auto p = split(q.m_front);
p.second = reverse(p.second);
auto p = split_reverse_second(q.m_front);
return mk_pair(queue(p.first, cdr(p.second)), car(p.second));
}
} else {