feat(kernel/level): serializer for level objects

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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<level> const & l) {
         return *(l.begin());
     return max_core(l.size(), l.begin());
 }
+
+
+class level_serializer : public object_serializer<level, level::ptr_hash, level::ptr_eq> {
+    typedef object_serializer<level, level::ptr_hash, level::ptr_eq> super;
+public:
+    void write(level const & l) {
+        super::write(l, [&]() {
+                serializer & s = get_owner();
+                auto k = kind(l);
+                s << static_cast<char>(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<level> {
+    typedef object_deserializer<level> super;
+public:
+    level read() {
+        return super::read([&]() {
+                deserializer & d = get_owner();
+                auto k = static_cast<level_kind>(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<level> 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<serializer::extension>(new level_serializer()); });
+        m_d_extid = deserializer::register_extension([](){ return std::unique_ptr<deserializer::extension>(new level_deserializer()); });
+    }
+};
+static level_sd g_level_sd;
+
+serializer & operator<<(serializer & s, level const & n) {
+    s.get_extension<level_serializer>(g_level_sd.m_s_extid).write(n);
+    return s;
+}
+
+level read_level(deserializer & d) {
+    return d.get_extension<level_deserializer>(g_level_sd.m_d_extid).read();
+}
 }
 void print(lean::level const & l) { std::cout << l << std::endl; }

src/kernel/level.h

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <iostream>
 #include <algorithm>
 #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<level_cell*>()(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);

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})));