feat(util/sexpr): serialization for sexpr

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

src/tests/util/sexpr.cpp

@@ -211,6 +211,32 @@ static void tst9() {
     }
 }
 
+static sexpr mk_shared(unsigned n) {
+    sexpr f("f");
+    sexpr a(10);
+    sexpr b(true);
+    sexpr r(f, sexpr({a, b, sexpr(name({"foo", "bla"})), sexpr(mpz("10")), sexpr(mpq(1, 3))}));
+    for (unsigned i = 0; i < n; i++) {
+        r = sexpr(f, sexpr(r, r));
+    }
+    return r;
+}
+
+static void tst10() {
+    sexpr r = mk_shared(20);
+    std::ostringstream out;
+    serializer s(out);
+    s << r << r;
+    std::cout << "Stream Size: " << out.str().size() << "\n";
+    std::istringstream in(out.str());
+    deserializer d(in);
+    sexpr r2, r3;
+    d >> r2 >> r3;
+    lean_assert(is_eqp(head(tail(r2)), tail(tail(r2))));
+    lean_assert(is_eqp(r2, r3));
+    lean_assert(r == r2);
+}
+
 int main() {
     save_stack_info();
     tst1();
@@ -222,5 +248,6 @@ int main() {
     tst7();
     tst8();
     tst9();
+    tst10();
     return has_violations() ? 1 : 0;
 }

src/util/sexpr/sexpr.cpp

@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "util/name.h"
 #include "util/escaped.h"
 #include "util/buffer.h"
+#include "util/object_serializer.h"
 #include "util/numerics/mpz.h"
 #include "util/numerics/mpq.h"
 #include "util/sexpr/sexpr.h"
@@ -291,6 +292,77 @@ bool operator==(sexpr const & a, name const & b) { return is_name(a) && to_name(
 bool operator==(sexpr const & a, mpz const & b) { return is_mpz(a) && to_mpz(a) == b; }
 bool operator==(sexpr const & a, mpq const & b) { return is_mpq(a) && to_mpq(a) == b; }
 
+class sexpr_serializer : public object_serializer<sexpr, sexpr::ptr_hash, sexpr::ptr_eq> {
+    typedef object_serializer<sexpr, sexpr::ptr_hash, sexpr::ptr_eq> super;
+public:
+    void write(sexpr const & a) {
+        super::write(a, [&]() {
+                serializer & s = get_owner();
+                auto k = a.kind();
+                s << static_cast<char>(k);
+                switch (k) {
+                case sexpr_kind::Nil:                                  break;
+                case sexpr_kind::String: s << to_string(a);            break;
+                case sexpr_kind::Bool:   s << to_bool(a);              break;
+                case sexpr_kind::Int:    s << to_int(a);               break;
+                case sexpr_kind::Double: s << to_double(a);            break;
+                case sexpr_kind::Name:   s << to_name(a);              break;
+                case sexpr_kind::MPZ:    s << to_mpz(a);               break;
+                case sexpr_kind::MPQ:    s << to_mpq(a);               break;
+                case sexpr_kind::Cons:   write(car(a)); write(cdr(a)); break;
+                }
+            });
+    }
+};
+
+class sexpr_deserializer : public object_deserializer<sexpr> {
+    typedef object_deserializer<sexpr> super;
+public:
+    sexpr read() {
+        return super::read([&]() {
+                deserializer & d = get_owner();
+                auto k = static_cast<sexpr_kind>(d.read_char());
+                switch (k) {
+                case sexpr_kind::Nil:    return sexpr();
+                case sexpr_kind::String: return sexpr(d.read_string());
+                case sexpr_kind::Bool:   return sexpr(d.read_bool());
+                case sexpr_kind::Int:    return sexpr(d.read_int());
+                case sexpr_kind::Double: return sexpr(d.read_double());
+                case sexpr_kind::Name:   return sexpr(read_name(d));
+                case sexpr_kind::MPZ:    return sexpr(read_mpz(d));
+                case sexpr_kind::MPQ:    return sexpr(read_mpq(d));
+                case sexpr_kind::Cons:   {
+                    sexpr h = read();
+                    sexpr t = read();
+                    return sexpr(h, t);
+                }}
+                lean_unreachable();
+            });
+    }
+};
+
+struct sexpr_sd {
+    unsigned m_s_extid;
+    unsigned m_d_extid;
+    sexpr_sd() {
+        m_s_extid = serializer::register_extension([](){ return std::unique_ptr<serializer::extension>(new sexpr_serializer()); });
+        m_d_extid = deserializer::register_extension([](){ return std::unique_ptr<deserializer::extension>(new sexpr_deserializer()); });
+    }
+};
+static sexpr_sd g_sexpr_sd;
+
+serializer & operator<<(serializer & s, sexpr const & n) {
+    s.get_extension<sexpr_serializer>(g_sexpr_sd.m_s_extid).write(n);
+    return s;
+}
+
+sexpr read_sexpr(deserializer & d) {
+    return d.get_extension<sexpr_deserializer>(g_sexpr_sd.m_d_extid).read();
+}
+
+serializer & operator<<(serializer & s, sexpr const & a);
+sexpr read_sexpr(deserializer & d);
+
 DECL_UDATA(sexpr)
 
 static int sexpr_tostring(lua_State * L) {

src/util/sexpr/sexpr.h

@@ -8,7 +8,9 @@ Author: Leonardo de Moura
 #include <iostream>
 #include <string>
 #include <algorithm>
+#include <functional>
 #include "util/lua.h"
+#include "util/serializer.h"
 
 namespace lean {
 class name;
@@ -87,6 +89,9 @@ public:
     /** \brief Pointer equality */
     friend bool is_eqp(sexpr const & a, sexpr const & b) { return a.m_ptr == b.m_ptr; }
 
+    struct ptr_hash { unsigned operator()(sexpr const & a) const { return std::hash<sexpr_cell*>()(a.m_ptr); } };
+    struct ptr_eq { unsigned operator()(sexpr const & a1, sexpr const & a2) const { return is_eqp(a1, a2); } };
+
     friend std::ostream & operator<<(std::ostream & out, sexpr const & s);
 };
 
@@ -159,6 +164,10 @@ inline bool operator>(sexpr const & a, sexpr const & b) { return cmp(a, b) > 0;
 inline bool operator<=(sexpr const & a, sexpr const & b) { return cmp(a, b) <= 0; }
 inline bool operator>=(sexpr const & a, sexpr const & b) { return cmp(a, b) >= 0; }
 
+serializer & operator<<(serializer & s, sexpr const & a);
+sexpr read_sexpr(deserializer & d);
+inline deserializer & operator>>(deserializer & d, sexpr & a) { a = read_sexpr(d); return d; }
+
 UDATA_DEFS(sexpr)
 void open_sexpr(lua_State * L);
 }