feat(lazy_list): implement ML-like lazy lists
We will use lazy lists to represent the set of solutions produced by the elaborator. The elaborator plugins will also use lazy lists. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
58e2ec331c
commit
3c8dff9085
3 changed files with 149 additions and 0 deletions
|
@ -49,3 +49,6 @@ add_test(exception ${CMAKE_CURRENT_BINARY_DIR}/exception)
|
||||||
add_executable(bit_tricks bit_tricks.cpp)
|
add_executable(bit_tricks bit_tricks.cpp)
|
||||||
target_link_libraries(bit_tricks ${EXTRA_LIBS})
|
target_link_libraries(bit_tricks ${EXTRA_LIBS})
|
||||||
add_test(bit_tricks ${CMAKE_CURRENT_BINARY_DIR}/bit_tricks)
|
add_test(bit_tricks ${CMAKE_CURRENT_BINARY_DIR}/bit_tricks)
|
||||||
|
add_executable(lazy_list lazy_list.cpp)
|
||||||
|
target_link_libraries(lazy_list ${EXTRA_LIBS})
|
||||||
|
add_test(lazy_list ${CMAKE_CURRENT_BINARY_DIR}/lazy_list)
|
||||||
|
|
62
src/tests/util/lazy_list.cpp
Normal file
62
src/tests/util/lazy_list.cpp
Normal file
|
@ -0,0 +1,62 @@
|
||||||
|
/*
|
||||||
|
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
||||||
|
Released under Apache 2.0 license as described in the file LICENSE.
|
||||||
|
|
||||||
|
Author: Leonardo de Moura
|
||||||
|
*/
|
||||||
|
#include <iostream>
|
||||||
|
#include <utility>
|
||||||
|
#include "util/test.h"
|
||||||
|
#include "util/numerics/mpz.h"
|
||||||
|
#include "util/pair.h"
|
||||||
|
#include "util/lazy_list.h"
|
||||||
|
using namespace lean;
|
||||||
|
|
||||||
|
lazy_list<int> seq(int s) {
|
||||||
|
return lazy_list<int>(s, [=]() { return seq(s + 1); });
|
||||||
|
}
|
||||||
|
|
||||||
|
lazy_list<int> from(int begin, int step, int end) {
|
||||||
|
if (begin > end)
|
||||||
|
return lazy_list<int>();
|
||||||
|
else
|
||||||
|
return lazy_list<int>(begin, [=]() { return from(begin + step, step, end); });
|
||||||
|
}
|
||||||
|
|
||||||
|
lazy_list<mpz> fact_list_core(mpz i, mpz n) {
|
||||||
|
return lazy_list<mpz>(n, [=]() { return fact_list_core(i+1, n*(i+1)); });
|
||||||
|
}
|
||||||
|
|
||||||
|
lazy_list<mpz> fact_list() {
|
||||||
|
return fact_list_core(mpz(1), mpz(1));
|
||||||
|
}
|
||||||
|
|
||||||
|
template<typename T>
|
||||||
|
lazy_list<T> first(unsigned sz, lazy_list<T> l) {
|
||||||
|
if (sz == 0 || !l) {
|
||||||
|
return lazy_list<T>();
|
||||||
|
} else {
|
||||||
|
return lazy_list<T>(head(l), [=]() { return first(sz - 1, tail(l)); });
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
template<typename T1, typename T2>
|
||||||
|
lazy_list<std::pair<T1, T2>> zip(lazy_list<T1> const & l1, lazy_list<T2> const & l2) {
|
||||||
|
if (l1 && l2) {
|
||||||
|
return lazy_list<std::pair<T1, T2>>(mk_pair(head(l1), head(l2)), [=]() { return zip(tail(l1), tail(l2)); });
|
||||||
|
} else {
|
||||||
|
return lazy_list<std::pair<T1, T2>>();
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
int main() {
|
||||||
|
lazy_list<int> l(-10, from(10, 20, 100));
|
||||||
|
l = cons(-20, l);
|
||||||
|
for (auto c : l) {
|
||||||
|
std::cout << c << "\n";
|
||||||
|
}
|
||||||
|
for (auto c : first(30, zip(seq(1), fact_list()))) {
|
||||||
|
std::cout << c.first << " " << c.second << "\n";
|
||||||
|
}
|
||||||
|
return 0;
|
||||||
|
}
|
84
src/util/lazy_list.h
Normal file
84
src/util/lazy_list.h
Normal file
|
@ -0,0 +1,84 @@
|
||||||
|
/*
|
||||||
|
Copyright (c) 2013 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"
|
||||||
|
|
||||||
|
namespace lean {
|
||||||
|
/**
|
||||||
|
\brief ML-like lazy lists.
|
||||||
|
*/
|
||||||
|
template<typename T>
|
||||||
|
class lazy_list {
|
||||||
|
public:
|
||||||
|
class cell {
|
||||||
|
MK_LEAN_RC();
|
||||||
|
void dealloc() { delete this; }
|
||||||
|
T m_head;
|
||||||
|
public:
|
||||||
|
cell(T const & h):m_rc(0), m_head(h) {}
|
||||||
|
virtual ~cell() {}
|
||||||
|
T const & head() const { return m_head; }
|
||||||
|
virtual lazy_list tail() const { return lazy_list(); }
|
||||||
|
};
|
||||||
|
|
||||||
|
private:
|
||||||
|
class explicit_cell : public cell {
|
||||||
|
lazy_list m_tail;
|
||||||
|
public:
|
||||||
|
explicit_cell(T const & h, lazy_list const & l):cell(h), m_tail(l) {}
|
||||||
|
virtual ~explicit_cell() {}
|
||||||
|
virtual lazy_list tail() const { return m_tail; }
|
||||||
|
};
|
||||||
|
|
||||||
|
template<typename Tail>
|
||||||
|
class lazy_cell : public cell {
|
||||||
|
Tail m_tail;
|
||||||
|
public:
|
||||||
|
lazy_cell(T const & h, Tail const & t):cell(h), m_tail(t) {}
|
||||||
|
virtual ~lazy_cell() {}
|
||||||
|
virtual lazy_list tail() const { return m_tail(); }
|
||||||
|
};
|
||||||
|
|
||||||
|
cell * m_ptr;
|
||||||
|
public:
|
||||||
|
lazy_list():m_ptr(nullptr) {}
|
||||||
|
lazy_list(T const & h):m_ptr(new cell(h)) { m_ptr->inc_ref(); }
|
||||||
|
lazy_list(T const & h, lazy_list const & t):m_ptr(new explicit_cell(h, t)) { m_ptr->inc_ref(); }
|
||||||
|
template<typename F>
|
||||||
|
lazy_list(T const & h, F const & f):m_ptr(new lazy_cell<F>(h, f)) { m_ptr->inc_ref(); }
|
||||||
|
lazy_list(lazy_list const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
|
||||||
|
lazy_list(lazy_list&& s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
|
||||||
|
~lazy_list() { if (m_ptr) m_ptr->dec_ref(); }
|
||||||
|
|
||||||
|
lazy_list & operator=(lazy_list const & s) { LEAN_COPY_REF(list, s); }
|
||||||
|
lazy_list & operator=(lazy_list && s) { LEAN_MOVE_REF(list, s); }
|
||||||
|
|
||||||
|
operator bool() const { return m_ptr != nullptr; }
|
||||||
|
|
||||||
|
friend T const & head(lazy_list const & l) { lean_assert(l); return l.m_ptr->head(); }
|
||||||
|
friend lazy_list tail(lazy_list const & l) { lean_assert(l); return l.m_ptr->tail(); }
|
||||||
|
friend lazy_list cons(T const & h, lazy_list const & t) { return lazy_list(h, t); }
|
||||||
|
|
||||||
|
class iterator {
|
||||||
|
friend class lazy_list;
|
||||||
|
lazy_list m_it;
|
||||||
|
iterator(lazy_list const & it):m_it(it) {}
|
||||||
|
public:
|
||||||
|
iterator(iterator const & s):m_it(s.m_it) {}
|
||||||
|
iterator & operator++() { m_it = tail(m_it); return *this; }
|
||||||
|
iterator operator++(int) { iterator tmp(*this); operator++(); return tmp; }
|
||||||
|
bool operator==(iterator const & s) const { return m_it == s.m_it; }
|
||||||
|
bool operator!=(iterator const & s) const { return !operator==(s); }
|
||||||
|
T const & operator*() { lean_assert(m_it); return head(m_it); }
|
||||||
|
T const * operator->() { lean_assert(m_it); return &(head(m_it)); }
|
||||||
|
};
|
||||||
|
|
||||||
|
iterator begin() const { return iterator(*this); }
|
||||||
|
iterator end() const { return iterator(lazy_list()); }
|
||||||
|
};
|
||||||
|
}
|
Loading…
Reference in a new issue