From f19944cf0995a611e83ce8d74f2ddbe5a3eb885c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 23 Nov 2013 15:33:25 -0800 Subject: [PATCH] refactor(util/lazy_list): 'lazier' lazy_lists In the new implementation, even the head of the lazy list is computed on demand. Signed-off-by: Leonardo de Moura --- src/library/tactic/tactic.cpp | 69 ++++++++------ src/library/tactic/tactic.h | 25 +++++ src/tests/library/tactic/tactic.cpp | 21 ++--- src/tests/util/CMakeLists.txt | 3 + src/tests/util/lazy_list.cpp | 62 +++++++------ src/util/lazy_list.h | 82 ++++++---------- src/util/lazy_list_fn.h | 139 ++++++++++++++++++---------- src/util/optional.h | 5 + 8 files changed, 236 insertions(+), 170 deletions(-) diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp index ce466fa8d..d774f238b 100644 --- a/src/library/tactic/tactic.cpp +++ b/src/library/tactic/tactic.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include #include +#include "util/sstream.h" #include "util/interrupt.h" #include "util/lazy_list_fn.h" #include "library/tactic/tactic_exception.h" @@ -22,9 +23,10 @@ tactic & tactic::operator=(tactic && s) { expr tactic::solve(environment const & env, io_state const & io, proof_state const & s) { proof_state_seq r = operator()(env, io, s); - if (!r) + auto p = r.pull(); + if (!p) throw exception("tactic failed to solve input"); - proof_state final = head(r); + proof_state final = p->first; assignment a(final.get_menv()); proof_map m; return final.get_proof_builder()(m, env, a); @@ -37,7 +39,7 @@ expr tactic::solve(environment const & env, io_state const & io, context const & tactic id_tactic() { return mk_tactic([](environment const &, io_state const &, proof_state const & s) -> proof_state_seq { - return proof_state_seq(s); + return to_proof_state_seq(s); }); } @@ -52,10 +54,28 @@ tactic now_tactic() { if (!empty(s.get_goals())) return proof_state_seq(); else - return proof_state_seq(s); + return to_proof_state_seq(s); }); } +tactic trace_tactic(std::string const & msg) { + return mk_tactic([=](environment const &, io_state const & io, proof_state const & s) -> proof_state_seq { + return proof_state_seq([=]() { + io.get_diagnostic_channel() << msg << "\n"; + io.get_diagnostic_channel().get_stream().flush(); + return some(mk_pair(s, proof_state_seq())); + }); + }); +} + +tactic trace_tactic(sstream const & msg) { + return trace_tactic(msg.str()); +} + +tactic trace_tactic(char const * msg) { + return trace_tactic(std::string(msg)); +} + tactic assumption_tactic() { return mk_tactic([](environment const &, io_state const &, proof_state const & s) -> proof_state_seq { list> proofs; @@ -84,7 +104,7 @@ tactic assumption_tactic() { } return p(new_m, env, a); }); - return proof_state_seq(proof_state(s, new_goals, new_p)); + return to_proof_state_seq(proof_state(s, new_goals, new_p)); }); } @@ -102,14 +122,8 @@ tactic then(tactic t1, tactic t2) { tactic orelse(tactic t1, tactic t2) { return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq { tactic _t1(t1); - proof_state_seq r = _t1(env, io, s); - if (r) { - return r; - } else { - check_interrupted(); - tactic _t2(t2); - return _t2(env, io, s); - } + tactic _t2(t2); + return orelse(_t1(env, io, s), _t2(env, io, s)); }); } @@ -200,10 +214,7 @@ tactic par(tactic t1, tactic t2, unsigned check_ms) { th2.request_interrupt(); th1.join(); th2.join(); - if (r1) - return r1; - else - return r2; + return orelse(r1, r2); } catch (...) { th1.request_interrupt(); th2.request_interrupt(); @@ -218,10 +229,11 @@ tactic repeat(tactic t) { return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s1) -> proof_state_seq { tactic t1(t); proof_state_seq r = t1(env, io, s1); - if (!r) { - return proof_state_seq(s1); + auto p = r.pull(); + if (!p) { + return to_proof_state_seq(s1); } else { - return map_append(r, [=](proof_state const & s2) { + return map_append(to_proof_state_seq(p), [=](proof_state const & s2) { check_interrupted(); tactic t2 = repeat(t1); return t2(env, io, s2); @@ -233,13 +245,14 @@ tactic repeat(tactic t) { tactic repeat_at_most(tactic t, unsigned k) { return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s1) -> proof_state_seq { if (k == 0) - return proof_state_seq(s1); + return to_proof_state_seq(s1); tactic t1(t); proof_state_seq r = t1(env, io, s1); - if (!r) { - return proof_state_seq(s1); + auto p = r.pull(); + if (!p) { + return to_proof_state_seq(s1); } else { - return map_append(r, [=](proof_state const & s2) { + return map_append(to_proof_state_seq(p), [=](proof_state const & s2) { check_interrupted(); tactic t2 = repeat_at_most(t1, k - 1); return t2(env, io, s2); @@ -260,10 +273,10 @@ tactic force(tactic t) { tactic _t(t); proof_state_seq r = _t(env, io, s); buffer buf; - for (auto s2 : r) { - buf.push_back(s2); - check_interrupted(); - } + for_each(r, [&](proof_state const & s2) { + buf.push_back(s2); + check_interrupted(); + }); return to_lazy(to_list(buf.begin(), buf.end())); }); } diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h index 12288a2f1..f892a48ea 100644 --- a/src/library/tactic/tactic.h +++ b/src/library/tactic/tactic.h @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include #include #include +#include #include "util/lazy_list.h" #include "library/io_state.h" #include "library/tactic/proof_state.h" @@ -64,6 +65,19 @@ public: template tactic mk_tactic(F && f) { return tactic(new simple_tactic_cell(std::forward(f))); } +inline proof_state_seq to_proof_state_seq(proof_state const & s) { + return proof_state_seq([=]() { return some(mk_pair(s, proof_state_seq())); }); +} + +inline proof_state_seq to_proof_state_seq(proof_state_seq::maybe_pair const & p) { + lean_assert(p); + return proof_state_seq([=]() { return some(mk_pair(p->first, p->second)); }); +} + +inline proof_state_seq to_proof_state_seq(proof_state const & s, proof_state_seq const & t) { + return proof_state_seq([=]() { return some(mk_pair(s, t)); }); +} + /** \brief Return a "do nothing" tactic (aka skip). */ @@ -80,15 +94,25 @@ tactic now_tactic(); \brief Return a tactic that solves any goal of the form ..., H : A, ... |- A. */ tactic assumption_tactic(); +/** + \brief Return a tactic that just returns the input state, and display the given message in the diagnostic channel. +*/ +tactic trace_tactic(char const * msg); +class sstream; +tactic trace_tactic(sstream const & msg); +tactic trace_tactic(std::string const & msg); + /** \brief Return a tactic that performs \c t1 followed by \c t2. */ tactic then(tactic t1, tactic t2); +inline tactic operator<<(tactic t1, tactic t2) { return then(t1, t2); } /** \brief Return a tactic that applies \c t1, and if \c t1 returns the empty sequence of states, then applies \c t2. */ tactic orelse(tactic t1, tactic t2); +inline tactic operator||(tactic t1, tactic t2) { return orelse(t1, t2); } /** \brief Return a tactic that tries the tactic \c t for at most \c ms milliseconds. If the tactic does not terminate in \c ms milliseconds, then the empty @@ -106,6 +130,7 @@ tactic try_for(tactic t, unsigned ms, unsigned check_ms = 1); from tactic \c t2. */ tactic append(tactic t1, tactic t2); +inline tactic operator+(tactic t1, tactic t2) { return append(t1, t2); } /** \brief Execute both tactics and and combines their results. The results produced by tactics \c t1 and \c t2 are interleaved diff --git a/src/tests/library/tactic/tactic.cpp b/src/tests/library/tactic/tactic.cpp index b0757cdfd..028a4bb1f 100644 --- a/src/tests/library/tactic/tactic.cpp +++ b/src/tests/library/tactic/tactic.cpp @@ -25,17 +25,10 @@ tactic loop_tactic() { }); } -tactic msg_tactic(std::string msg) { - return mk_tactic([=](environment const &, io_state const &, proof_state const & s) -> proof_state_seq { - std::cout << msg << "\n"; - return proof_state_seq(s); - }); -} - tactic set_tactic(std::atomic * flag) { return mk_tactic([=](environment const &, io_state const &, proof_state const & s) -> proof_state_seq { *flag = true; - return proof_state_seq(s); + return to_proof_state_seq(s); }); } @@ -71,7 +64,7 @@ static void tst1() { check_failure(try_for(loop_tactic(), 100), env, io, ctx, q); std::cout << "proof 1: " << try_for(t, 10000).solve(env, io, s) << "\n"; check_failure(try_for(orelse(try_for(loop_tactic(), 10000), - msg_tactic(std::string("hello world"))), + trace_tactic(std::string("hello world"))), 100), env, io, ctx, q); std::atomic flag1(false); @@ -87,10 +80,16 @@ static void tst1() { std::cout << "proof 2: " << par(loop_tactic(), par(loop_tactic(), t)).solve(env, io, ctx, q) << "\n"; #endif - std::cout << "proof 2: " << orelse(then(repeat_at_most(append(msg_tactic("hello1"), msg_tactic("hello2")), 5), fail_tactic()), + std::cout << "proof 2: " << orelse(then(repeat_at_most(append(trace_tactic("hello1"), trace_tactic("hello2")), 5), fail_tactic()), t).solve(env, io, ctx, q) << "\n"; std::cout << "------------------\n"; - std::cout << "proof 2: " << force(take(then(repeat_at_most(interleave(id_tactic(), id_tactic()), 100), then(msg_tactic("foo"), t)), 5)).solve(env, io, ctx, q) << "\n"; + std::cout << "proof 2: " << ((trace_tactic("hello1.1") + trace_tactic("hello1.2") + trace_tactic("hello1.3") + trace_tactic("hello1.4")) << + (trace_tactic("hello2.1") + trace_tactic("hello2.2")) << + (trace_tactic("hello3.1") || trace_tactic("hello3.2")) << + assumption_tactic()).solve(env, io, ctx, q) << "\n"; + std::cout << "------------------\n"; + std::cout << "proof 2: " << force(take(repeat_at_most(interleave(id_tactic(), id_tactic()), 100) << trace_tactic("foo") << t, + 5)).solve(env, io, ctx, q) << "\n"; std::cout << "done\n"; } diff --git a/src/tests/util/CMakeLists.txt b/src/tests/util/CMakeLists.txt index b1f1697a1..c42485039 100644 --- a/src/tests/util/CMakeLists.txt +++ b/src/tests/util/CMakeLists.txt @@ -61,3 +61,6 @@ add_test(safe_arith ${CMAKE_CURRENT_BINARY_DIR}/safe_arith) add_executable(set set.cpp) target_link_libraries(set ${EXTRA_LIBS}) add_test(set ${CMAKE_CURRENT_BINARY_DIR}/set) +add_executable(optional optional.cpp) +target_link_libraries(optional ${EXTRA_LIBS}) +add_test(optional ${CMAKE_CURRENT_BINARY_DIR}/optional) diff --git a/src/tests/util/lazy_list.cpp b/src/tests/util/lazy_list.cpp index 2917819fb..489c67676 100644 --- a/src/tests/util/lazy_list.cpp +++ b/src/tests/util/lazy_list.cpp @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include #include #include "util/test.h" +#include "util/optional.h" #include "util/numerics/mpz.h" #include "util/pair.h" #include "util/lazy_list.h" @@ -15,18 +16,18 @@ Author: Leonardo de Moura using namespace lean; lazy_list seq(int s) { - return lazy_list(s, [=]() { return seq(s + 1); }); + return lazy_list([=]() { return some(mk_pair(s, seq(s + 1))); }); } lazy_list from(int begin, int step, int end) { if (begin > end) return lazy_list(); else - return lazy_list(begin, [=]() { return from(begin + step, step, end); }); + return lazy_list([=]() { return some(mk_pair(begin, from(begin + step, step, end))); }); } lazy_list fact_list_core(mpz i, mpz n) { - return lazy_list(n, [=]() { return fact_list_core(i+1, n*(i+1)); }); + return lazy_list([=]() { return some(mk_pair(n, fact_list_core(i+1, n*(i+1)))); }); } lazy_list fact_list() { @@ -51,36 +52,41 @@ lazy_list mk_simple3() { template void display(lazy_list const & l) { - for (auto v : l) { - std::cout << v << " "; - } + int buffer[20000]; + int i = 0; + for_each(l, [&](T const & v) { + std::cout << v << " "; + buffer[i] = i; + i++; + }); std::cout << "\n"; } -int main() { - lean_assert(head(lazy_list(10)) == 10); - lean_assert(!lazy_list()); - lean_assert(!tail(lazy_list(10))); - lazy_list l(-10, from(10, 20, 100)); - l = cons(-20, l); - lean_assert(head(l) == -20); - for (auto c : l) { - std::cout << c << "\n"; - } - int i = 1; - for (auto c : take(30, zip(seq(1), fact_list()))) { - lean_assert(c.first == i); - std::cout << c.first << " " << c.second << "\n"; - i++; - } +static void tst1() { + lazy_list l([]() { return some(mk_pair(10, lazy_list())); }); + lazy_list empty; + lean_assert(l.pull()->first == 10); + lean_assert(!empty.pull()); + lean_assert(!l.pull()->second.pull()); list l2{1, 2, 3}; - i = 1; - for (auto c : to_lazy(l2)) { - lean_assert(c == i); - i++; - } + int i = 1; + for_each(to_lazy(l2), [&](int c) { + std::cout << "c: " << c << ", i: " << i << "\n"; + lean_assert(c == i); + i++; + }); display(mk_simple1(4)); display(mk_simple2()); - display(take(12, mk_simple3())); + display(take(10, fact_list())); + display(take(20, mk_simple3())); + display(orelse(take(10, seq(1)), take(10, seq(100)))); + display(orelse(take(10, seq(1)), lazy_list())); + display(orelse(lazy_list(), take(10, seq(100)))); + display(orelse(take(0, seq(1)), take(10, seq(100)))); + display(orelse(filter(take(100, seq(1)), [](int i) { return i < 0; }), take(10, seq(1000)))); +} + +int main() { + tst1(); return 0; } diff --git a/src/util/lazy_list.h b/src/util/lazy_list.h index 2b0a1f44b..f77ce0183 100644 --- a/src/util/lazy_list.h +++ b/src/util/lazy_list.h @@ -5,8 +5,9 @@ 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/rc.h" +#include "util/optional.h" namespace lean { /** @@ -15,70 +16,45 @@ namespace lean { template class lazy_list { public: - class cell { + typedef optional> maybe_pair; // head and tail pair +private: + class cell_base { MK_LEAN_RC(); void dealloc() { delete this; } - T m_head; public: - cell(T const & h):m_rc(0), m_head(h) {} + cell_base():m_rc(0) {} + virtual ~cell_base() {} + virtual maybe_pair pull() const = 0; + }; + + template + class cell : public cell_base { + F m_f; + public: + cell(F && f):cell_base(), m_f(f) {} virtual ~cell() {} - T const & head() const { return m_head; } - virtual lazy_list tail() const { return lazy_list(); } + virtual maybe_pair pull() const { return m_f(); } }; -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 - 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; + cell_base * 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 - lazy_list(T const & h, F const & f):m_ptr(new lazy_cell(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(lazy_list && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; } + template explicit lazy_list(F && f):m_ptr(new cell(std::forward(f))) { m_ptr->inc_ref(); } ~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); } + lazy_list & operator=(lazy_list const & s) { LEAN_COPY_REF(lazy_list, s); } + lazy_list & operator=(lazy_list && s) { LEAN_MOVE_REF(lazy_list, s); } - operator bool() const { return m_ptr != nullptr; } + maybe_pair pull() const { + if (m_ptr) + return m_ptr->pull(); + else + return maybe_pair(); + } - 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()); } + friend T head(lazy_list const & l) { return l.pull()->first; } + friend lazy_list tail(lazy_list const & l) { return l.pull()->second; } }; } diff --git a/src/util/lazy_list_fn.h b/src/util/lazy_list_fn.h index f31639448..664adf6e1 100644 --- a/src/util/lazy_list_fn.h +++ b/src/util/lazy_list_fn.h @@ -10,78 +10,117 @@ Author: Leonardo de Moura #include "util/list.h" namespace lean { -template -lazy_list take(unsigned sz, lazy_list l) { - if (sz == 0 || !l) { - return lazy_list(); - } else { - return lazy_list(head(l), [=]() { return take(sz - 1, tail(l)); }); - } -} - -template -lazy_list> zip(lazy_list const & l1, lazy_list const & l2) { - if (l1 && l2) { - return lazy_list>(mk_pair(head(l1), head(l2)), [=]() { return zip(tail(l1), tail(l2)); }); - } else { - return lazy_list>(); +template +void for_each(lazy_list l, F && f) { + while (true) { + auto p = l.pull(); + if (p) { + f(p->first); + l = p->second; + } else { + break; + } } } template -lazy_list to_lazy(list const & l) { - if (l) - return lazy_list(head(l), [=]() { return to_lazy(tail(l)); }); - else +lazy_list take(unsigned sz, lazy_list const & l) { + if (sz == 0) { return lazy_list(); + } else { + return lazy_list([=]() { + auto p = l.pull(); + if (p) + return some(mk_pair(p->first, take(sz - 1, p->second))); + else + return p; + }); + } +} + +template +lazy_list to_lazy(list l) { + if (l) { + return lazy_list([=]() { + return some(mk_pair(head(l), to_lazy(tail(l)))); + }); + } else { + return lazy_list(); + } } template lazy_list append(lazy_list const & l1, lazy_list const & l2) { - if (!l1) - return l2; - else if (!l2) - return l1; - else - return lazy_list(head(l1), [=]() { return append(tail(l1), l2); }); + return lazy_list([=]() { + auto p = l1.pull(); + if (!p) + return l2.pull(); + else + return some(mk_pair(p->first, append(p->second, l2))); + }); } -template -lazy_list map(lazy_list const & l, F && f) { - if (!l) - return l; - else - return lazy_list(f(head(l)), [=]() { return map(tail(l), f); }); +template +lazy_list orelse(lazy_list const & l1, lazy_list const & l2) { + return lazy_list([=]() { + auto p = l1.pull(); + if (!p) + return l2.pull(); + else + return some(mk_pair(p->first, orelse(p->second, lazy_list()))); + }); } template lazy_list interleave(lazy_list const & l1, lazy_list const & l2) { - if (!l1) - return l2; - else if (!l2) - return l1; - else - return lazy_list(head(l1), [=]() { return interleave(l2, tail(l1)); }); + return lazy_list([=]() { + auto p = l1.pull(); + if (!p) + return l2.pull(); + else + return some(mk_pair(p->first, interleave(l2, p->second))); + }); +} + +template +lazy_list map(lazy_list const & l, F && f) { + return lazy_list([=]() { + auto p = l.pull(); + if (!p) + return p; + else + return some(mk_pair(f(p->first), map(p->second, f))); + }); } template -lazy_list filter(lazy_list const & l, P && p) { - if (!l) - return l; - else if (p(head(l))) - return lazy_list(head(l), [=]() { return filter(tail(l), p); }); - else - return filter(tail(l), p); +lazy_list filter(lazy_list const & l, P && pred) { + return lazy_list([=]() { + auto p = l.pull(); + if (!p) + return p; + else if (pred(p->first)) + return some(mk_pair(p->first, p->second)); + else + return filter(p->second, pred).pull(); + }); } template lazy_list map_append_aux(lazy_list const & h, lazy_list const & l, F && f) { - if (!l) - return h; - else if (h) - return lazy_list(head(h), [=]() { return map_append_aux(tail(h), l, f); }); - else - return map_append_aux(f(head(l)), tail(l), f); + return lazy_list([=]() { + auto p1 = h.pull(); + if (p1) { + return some(mk_pair(p1->first, map_append_aux(p1->second, l, f))); + } else { + auto p2 = l.pull(); + if (p2) { + return map_append_aux(f(p2->first), p2->second, f).pull(); + } else { + return typename lazy_list::maybe_pair(); + } + } + }); } template diff --git a/src/util/optional.h b/src/util/optional.h index d2e2fabc5..0c532ff76 100644 --- a/src/util/optional.h +++ b/src/util/optional.h @@ -96,4 +96,9 @@ public: return !o1.m_some || o1.m_value == o2.m_value; } }; + +template +optional some(T && t) { + return optional(std::forward(t)); +} }