diff --git a/src/tests/util/CMakeLists.txt b/src/tests/util/CMakeLists.txt index cd5960481f..299706af77 100644 --- a/src/tests/util/CMakeLists.txt +++ b/src/tests/util/CMakeLists.txt @@ -1,9 +1,6 @@ add_executable(name name.cpp $) target_link_libraries(name ${EXTRA_LIBS}) add_exec_test(name "name") -add_executable(sequence sequence.cpp $) -target_link_libraries(sequence ${EXTRA_LIBS}) -add_exec_test(sequence "sequence") add_executable(sexpr_tst sexpr.cpp $ $ $) target_link_libraries(sexpr_tst ${EXTRA_LIBS}) add_exec_test(sexpr "sexpr_tst") diff --git a/src/tests/util/sequence.cpp b/src/tests/util/sequence.cpp deleted file mode 100644 index 576a84347c..0000000000 --- a/src/tests/util/sequence.cpp +++ /dev/null @@ -1,41 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "util/sequence.h" -#include "util/test.h" -#include "util/init_module.h" -using namespace lean; - -namespace lean { -template class sequence; -} - -static void tst1() { - sequence l1; - lean_assert(!l1); - sequence l2(10); - lean_assert(l2); - lean_assert(is_eqp(l2, l1 + l2)); - lean_assert(is_eqp(l2, l2 + l1)); - lean_assert(!is_eqp(l2, l2 + l2)); - sequence l3(20); - sequence l4(5); - sequence r = l4 + (l2 + l2) + (l3 + l4) + sequence(3); - buffer b; - r.linearize(b); - for (auto v : b) { - std::cout << v << " "; - } - std::cout << "\n"; - lean_assert(b[0] == 5 && b[1] == 10 && b[2] == 10 && b[3] == 20 && b[4] == 5 && b[5] == 3); -} - -int main() { - initialize_util_module(); - tst1(); - finalize_util_module(); - return has_violations() ? 1 : 0; -} diff --git a/src/util/sequence.h b/src/util/sequence.h deleted file mode 100644 index 8e54fdc249..0000000000 --- a/src/util/sequence.h +++ /dev/null @@ -1,128 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "util/rc.h" -#include "util/debug.h" -#include "util/buffer.h" -#include "util/optional.h" -#include "util/list.h" - -namespace lean { -/** \brief Sequence datastructure with O(1) concatenation operation */ -template -class sequence { - struct cell { - bool m_join; - MK_LEAN_RC(); - void dealloc(); - cell(bool join):m_join(join), m_rc(1) {} - }; - - struct elem_cell : public cell { - T m_value; - elem_cell(T const & v):cell(false), m_value(v) {} - }; - - struct node { - cell * m_ptr; - node():m_ptr(nullptr) {} - explicit node(T const & v); - node(node const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); } - node(node && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; } - node(node const & f, node const & s); - ~node() { if (m_ptr) m_ptr->dec_ref(); } - node & operator=(node const & s) { LEAN_COPY_REF(s); } - node & operator=(node && s) { LEAN_MOVE_REF(s); } - cell * raw() const { return m_ptr; } - explicit operator bool() const { return m_ptr != nullptr; } - }; - - struct join_cell : public cell { - node m_first; - node m_second; - join_cell(node const & f, node const & s):cell(true), m_first(f), m_second(s) {} - }; - -private: - node m_node; -public: - sequence() {} - explicit sequence(T const & v):m_node(v) {} - sequence(sequence const & f, sequence const & s):m_node(f.m_node, s.m_node) {} - - /** \brief Return true iff it is not the empty/nil sequence. */ - explicit operator bool() const { return m_node.raw() != nullptr; } - - /** \brief Pointer equality. Return true iff \c s1 and \c s2 point to the same memory location. */ - friend bool is_eqp(sequence const & s1, sequence const & s2) { return s1.m_node.raw() == s2.m_node.raw(); } - - friend sequence operator+(sequence const & s1, sequence const & s2) { return sequence(s1, s2); } - friend sequence operator+(sequence const & s, T const & v) { return s + sequence(v); } - friend sequence operator+(T const & v, sequence const & s) { return sequence(v) + s; } - sequence & operator+=(T const & v) { *this = *this + v; return *this; } - sequence & operator+=(sequence const & s) { *this = *this + s; return *this; } - - template - bool all_of(F && f) const { - buffer todo; - if (m_node) todo.push_back(m_node.raw()); - while (!todo.empty()) { - cell const * c = todo.back(); - todo.pop_back(); - if (c->m_join) { - todo.push_back(static_cast(c)->m_second.raw()); - todo.push_back(static_cast(c)->m_first.raw()); - } else { - if (!f(static_cast(c)->m_value)) - return false; - } - } - return true; - } - - template - void for_each(F && f) const { all_of([&](T const & v) { f(v); return true; }); } - - /** \brief Store sequence elements in \c r */ - void linearize(buffer & r) const { for_each([&](T const & v) { r.push_back(v); }); } - - list to_list() const { - buffer tmp; - linearize(tmp); - return ::lean::to_list(tmp.begin(), tmp.end()); - } -}; - -template -void sequence::cell::dealloc() { - if (m_join) { - join_cell * c = static_cast(this); - delete c; - } else { - elem_cell * c = static_cast(this); - delete c; - } -} - -template -sequence::node::node(T const & v):m_ptr(new elem_cell(v)) {} - -template -sequence::node::node(node const & f, node const & s) { - if (f && s) { - m_ptr = new join_cell(f, s); - } else if (f) { - m_ptr = f.m_ptr; - m_ptr->inc_ref(); - } else if (s) { - m_ptr = s.m_ptr; - m_ptr->inc_ref(); - } else { - m_ptr = nullptr; - } -} -}