From 0ef8ba2939275016010ea41b23955304179b7f4b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 27 Dec 2013 23:30:13 -0800 Subject: [PATCH] feat(kernel/level): serializer for level objects Signed-off-by: Leonardo de Moura --- src/kernel/level.cpp | 74 ++++++++++++++++++++++++++++++++++++++ src/kernel/level.h | 8 +++++ src/tests/kernel/level.cpp | 23 ++++++++++++ 3 files changed, 105 insertions(+) diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp index 0b67b5d11..efb5f4464 100644 --- a/src/kernel/level.cpp +++ b/src/kernel/level.cpp @@ -10,6 +10,7 @@ Author: Leonardo de Moura #include "util/rc.h" #include "util/debug.h" #include "util/hash.h" +#include "util/object_serializer.h" #include "kernel/level.h" namespace lean { @@ -257,5 +258,78 @@ level max(std::initializer_list const & l) { return *(l.begin()); return max_core(l.size(), l.begin()); } + + +class level_serializer : public object_serializer { + typedef object_serializer super; +public: + void write(level const & l) { + super::write(l, [&]() { + serializer & s = get_owner(); + auto k = kind(l); + s << static_cast(k); + switch (k) { + case level_kind::UVar: + s << uvar_name(l); + break; + case level_kind::Lift: + s << lift_offset(l); + write(lift_of(l)); + break; + case level_kind::Max: + s << max_size(l); + for (unsigned i = 0; i < max_size(l); i++) + write(max_level(l, i)); + break; + } + }); + } +}; + +class level_deserializer : public object_deserializer { + typedef object_deserializer super; +public: + level read() { + return super::read([&]() { + deserializer & d = get_owner(); + auto k = static_cast(d.read_char()); + switch (k) { + case level_kind::UVar: + return level(read_name(d)); + case level_kind::Lift: { + unsigned offset = d.read_unsigned(); + return read() + offset; + } + case level_kind::Max: { + buffer lvls; + unsigned num = d.read_unsigned(); + for (unsigned i = 0; i < num; i++) { + lvls.push_back(read()); + } + return max_core(lvls.size(), lvls.data()); + }} + lean_unreachable(); + }); + } +}; + +struct level_sd { + unsigned m_s_extid; + unsigned m_d_extid; + level_sd() { + m_s_extid = serializer::register_extension([](){ return std::unique_ptr(new level_serializer()); }); + m_d_extid = deserializer::register_extension([](){ return std::unique_ptr(new level_deserializer()); }); + } +}; +static level_sd g_level_sd; + +serializer & operator<<(serializer & s, level const & n) { + s.get_extension(g_level_sd.m_s_extid).write(n); + return s; +} + +level read_level(deserializer & d) { + return d.get_extension(g_level_sd.m_d_extid).read(); +} } void print(lean::level const & l) { std::cout << l << std::endl; } diff --git a/src/kernel/level.h b/src/kernel/level.h index 2df7402a2..6b9a7747a 100644 --- a/src/kernel/level.h +++ b/src/kernel/level.h @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #include #include "util/name.h" +#include "util/serializer.h" #include "util/sexpr/format.h" #include "util/sexpr/options.h" @@ -55,6 +56,9 @@ public: friend void swap(level & l1, level & l2) { std::swap(l1, l2); } friend std::ostream & operator<<(std::ostream & out, level const & l); + + struct ptr_hash { unsigned operator()(level const & n) const { return std::hash()(n.m_ptr); } }; + struct ptr_eq { bool operator()(level const & n1, level const & n2) const { return n1.m_ptr == n2.m_ptr; } }; }; level max(level const & l1, level const & l2); @@ -74,5 +78,9 @@ inline level const * max_end_levels(level const & l) { return max_begin_levels format pp(level const & l, bool unicode); /** \brief Pretty print the given level expression using the given configuration options. */ format pp(level const & l, options const & opts = options()); + +serializer & operator<<(serializer & s, level const & l); +level read_level(deserializer & d); +inline deserializer & operator>>(deserializer & d, level & l) { l = read_level(d); return d; } } void print(lean::level const & l); diff --git a/src/tests/kernel/level.cpp b/src/tests/kernel/level.cpp index 5b762da66..1edbad5df 100644 --- a/src/tests/kernel/level.cpp +++ b/src/tests/kernel/level.cpp @@ -11,6 +11,18 @@ Author: Leonardo de Moura #include "kernel/printer.h" using namespace lean; +static void check_serializer(level const & l) { + std::ostringstream out; + serializer s(out); + s << l << l; + std::istringstream in(out.str()); + deserializer d(in); + level l1, l2; + d >> l1 >> l2; + lean_assert(l == l1); + lean_assert(l == l2); +} + static void tst0() { environment env; lean_assert(env->begin_objects() == env->end_objects()); @@ -31,6 +43,10 @@ static void tst1() { level l2 = env->add_uvar("l2", l1 + 10); level l3 = env->add_uvar("l3", max(l2, l1 + 3)); level l4 = env->add_uvar("l4", max(l1 + 8, max(l2 + 2, l3 + 20))); + check_serializer(l1); + check_serializer(l2); + check_serializer(l3); + check_serializer(l4); std::cout << pp(max(l1 + 8, max(l2 + 2, l3 + 20))) << "\n"; std::cout << pp(level()) << "\n"; std::cout << pp(level()+1) << "\n"; @@ -55,6 +71,7 @@ static void tst3() { environment env; level l1 = env->add_uvar("l1", level()); level l2 = env->add_uvar("l2", l1 + ((1<<30) + 1024)); + check_serializer(l2); try { level l3 = env->add_uvar("l3", l2 + (1<<30)); lean_unreachable(); @@ -72,6 +89,12 @@ static void tst4() { level l4 = env->add_uvar("l4", l3 + 1); level l5 = env->add_uvar("l5", l3 + 1); level l6 = env->add_uvar("l6", max(l4, l5) + 1); + check_serializer(l1); + check_serializer(l2); + check_serializer(l3); + check_serializer(l4); + check_serializer(l5); + check_serializer(l6); lean_assert(!env->is_ge(l5 + 1, l6)); lean_assert(env->is_ge(l6, l5)); lean_assert(env->is_ge(l6, max({l1, l2, l3, l4, l5})));