feat(util/name): serialization for hierarchical names

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

src/tests/util/serializer.cpp

@@ -14,6 +14,7 @@ Author: Leonardo de Moura
 #include "util/object_serializer.h"
 #include "util/debug.h"
 #include "util/list.h"
+#include "util/name.h"
 using namespace lean;
 
 template<typename T>
@@ -121,8 +122,30 @@ static void tst2() {
     lean_assert(is_eqp(new_l5, new_l3));
 }
 
+static void tst3() {
+    std::ostringstream out;
+    serializer s(out);
+    name n1{"foo", "bla"};
+    name n2(n1, 10);
+    name n3(n2, "tst");
+    name n4(n1, "hello");
+    name n5("simple");
+    s << n1 << n2 << n3 << n4 << n2 << n5;
+    std::istringstream in(out.str());
+    deserializer d(in);
+    name m1, m2, m3, m4, m5, m6;
+    d >> m1 >> m2 >> m3 >> m4 >> m5 >> m6;
+    lean_assert(n1 == m1);
+    lean_assert(n2 == m2);
+    lean_assert(n3 == m3);
+    lean_assert(n4 == m4);
+    lean_assert(n2 == m5);
+    lean_assert(n5 == m6);
+}
+
 int main() {
     tst1();
     tst2();
+    tst3();
     return has_violations() ? 1 : 0;
 }

src/util/name.cpp

@@ -18,6 +18,7 @@ Author: Leonardo de Moura
 #include "util/hash.h"
 #include "util/trace.h"
 #include "util/ascii.h"
+#include "util/object_serializer.h"
 
 namespace lean {
 constexpr char const * anonymous_str = "[anonymous]";
@@ -356,6 +357,71 @@ name operator+(name const & n1, name const & n2) {
     }
 }
 
+class name_serializer : public object_serializer<name, name::ptr_hash, name::ptr_eq> {
+    typedef object_serializer<name, name::ptr_hash, name::ptr_eq> super;
+public:
+    void write(name const & n) {
+        super::write(n, [&]() {
+                serializer & s = get_owner();
+                s.write_char(static_cast<char>(n.kind()));
+                if (n.is_anonymous())
+                    return;
+                if (n.is_atomic()) {
+                    s.write_bool(false);
+                } else {
+                    s.write_bool(true);
+                    write(n.get_prefix());
+                }
+                if (n.is_string()) {
+                    s.write_string(n.get_string());
+                } else {
+                    s.write_unsigned(n.get_numeral());
+                }
+            });
+    }
+};
+
+class name_deserializer : public object_deserializer<name> {
+    typedef object_deserializer<name> super;
+public:
+    name read() {
+        return super::read([&]() {
+                deserializer & d = get_owner();
+                auto k = static_cast<name_kind>(d.read_char());
+                if (k == name_kind::ANONYMOUS)
+                    return name();
+                name prefix;
+                if (d.read_bool())
+                    prefix = read();
+                if (k == name_kind::STRING) {
+                    return name(prefix, d.read_string().c_str());
+                } else {
+                    lean_assert(k == name_kind::NUMERAL);
+                    return name(prefix, d.read_unsigned());
+                }
+            });
+    }
+};
+
+struct name_sd {
+    unsigned m_serializer_extid;
+    unsigned m_deserializer_extid;
+    name_sd() {
+        m_serializer_extid   = serializer::register_extension([](){ return std::unique_ptr<serializer::extension>(new name_serializer()); });
+        m_deserializer_extid = deserializer::register_extension([](){ return std::unique_ptr<deserializer::extension>(new name_deserializer()); });
+    }
+};
+static name_sd g_name_sd;
+
+serializer & operator<<(serializer & s, name const & n) {
+    s.get_extension<name_serializer>(g_name_sd.m_serializer_extid).write(n);
+    return s;
+}
+
+name read_name(deserializer & d) {
+    return d.get_extension<name_deserializer>(g_name_sd.m_deserializer_extid).read();
+}
+
 DECL_UDATA(name)
 
 static int mk_name(lua_State * L) {

src/util/name.h

@@ -7,8 +7,10 @@ Author: Leonardo de Moura
 #pragma once
 #include <string>
 #include <iostream>
+#include <functional>
 #include <algorithm>
 #include "util/lua.h"
+#include "util/serializer.h"
 
 namespace lean {
 constexpr char const * lean_name_separator = "::";
@@ -117,12 +119,20 @@ public:
         else
             return cmp(a, b);
     }
+
+    struct ptr_hash { unsigned operator()(name const & n) const { return std::hash<imp*>()(n.m_ptr); } };
+    struct ptr_eq { bool operator()(name const & n1, name const & n2) const { return n1.m_ptr == n2.m_ptr; } };
 };
+
 struct name_hash { unsigned operator()(name const & n) const { return n.hash(); } };
 struct name_eq { bool operator()(name const & n1, name const & n2) const { return n1 == n2; } };
 struct name_cmp { int operator()(name const & n1, name const & n2) const { return cmp(n1, n2); } };
 struct name_quick_cmp { int operator()(name const & n1, name const & n2) const { return quick_cmp(n1, n2); } };
 
+serializer & operator<<(serializer & s, name const & n);
+name read_name(deserializer & d);
+inline deserializer & operator>>(deserializer & d, name & n) { n = read_name(d); return d; }
+
 UDATA_DEFS(name)
 name to_name_ext(lua_State * L, int idx);
 void open_name(lua_State * L);