feat(kernel/object): serializer for kernel objects

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

src/frontends/lean/CMakeLists.txt

@@ -1,3 +1,3 @@
 add_library(lean_frontend frontend.cpp operator_info.cpp scanner.cpp parser.cpp pp.cpp
-  notation.cpp frontend_elaborator.cpp register_module.cpp environment_scope.cpp)
+  notation.cpp frontend_elaborator.cpp register_module.cpp environment_scope.cpp coercion.cpp)
 target_link_libraries(lean_frontend ${LEAN_LIBS})

src/frontends/lean/coercion.h

@@ -19,5 +19,6 @@ public:
     virtual ~coercion_declaration() {}
     virtual char const * keyword() const { return "Coercion"; }
     expr const & get_coercion() const { return m_coercion; }
+    virtual void write(serializer & s) const;
 };
 }

src/frontends/lean/environment_scope.cpp

@@ -85,6 +85,7 @@ static expr Fun(expr e, name_map<object_info> & info_map, dependencies const & d
 }
 
 std::vector<object> export_local_objects(environment const & env) {
+    // TODO(Leo): Revise using Parameters
     if (!env->has_parent())
         return std::vector<object>();
     name_map<object_info> info_map;
@@ -110,7 +111,7 @@ std::vector<object> export_local_objects(environment const & env) {
             auto new_deps = mk_dependencies(info_map, dep_set);
             new_type = Pi(new_type, info_map, new_deps);
             new_val  = Fun(new_val, info_map, new_deps);
-            auto new_obj  = obj.is_theorem() ? mk_theorem(obj.get_name(), new_type, new_val) : mk_definition(obj.get_name(), new_type, new_val, obj.is_opaque(), obj.get_weight());
+            auto new_obj  = obj.is_theorem() ? mk_theorem(obj.get_name(), new_type, new_val) : mk_definition(obj.get_name(), new_type, new_val, obj.get_weight());
             new_objects.push_back(new_obj);
             info_map.insert(mk_pair(obj.get_name(), object_info(new_obj, pos, new_deps, mk_ref(new_obj, new_deps))));
         }

src/frontends/lean/frontend.cpp

@@ -28,6 +28,31 @@ Author: Leonardo de Moura
 #include "frontends/lean/pp.h"
 
 namespace lean {
+class mark_implicit_command : public neutral_object_cell {
+    name              m_obj_name;
+    std::vector<bool> m_implicit;
+public:
+    mark_implicit_command(name const & n, unsigned sz, bool const * implicit):
+        m_obj_name(n), m_implicit(implicit, implicit+sz) {}
+    virtual ~mark_implicit_command() {}
+    virtual char const * keyword() const { return "MarkImplicit"; }
+    virtual void write(serializer & s) const {
+        unsigned sz = m_implicit.size();
+        s << "MarkImplicit" << m_obj_name << sz;
+        for (auto b : m_implicit)
+            s << b;
+    }
+};
+static void read_mark_implicit(environment const & env, io_state const &, deserializer & d) {
+    name n = read_name(d);
+    buffer<bool> implicit;
+    unsigned num = d.read_unsigned();
+    for (unsigned i = 0; i < num; i++)
+        implicit.push_back(d.read_bool());
+    mark_implicit_arguments(env, n, implicit.size(), implicit.data());
+}
+static object_cell::register_deserializer_fn mark_implicit_ds("MarkImplicit", read_mark_implicit);
+
 static std::vector<bool> g_empty_vector;
 /**
    \brief Environment extension object for the Lean default frontend.

src/frontends/lean/operator_info.cpp

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include "util/rc.h"
 #include "frontends/lean/operator_info.h"
+#include "frontends/lean/frontend.h"
 
 namespace lean {
 /** \brief Actual implementation of operator_info */
@@ -179,6 +180,35 @@ char const * notation_declaration::keyword() const {
     return to_string(m_op.get_fixity());
 }
 
+void notation_declaration::write(serializer & s) const {
+    auto parts = m_op.get_op_name_parts();
+    s << "Notation" << length(parts);
+    for (auto n : parts)
+        s << n;
+    s << static_cast<char>(m_op.get_fixity()) << m_op.get_precedence() << m_expr;
+}
+static void read_notation(environment const & env, io_state const & ios, deserializer & d) {
+    buffer<name> parts;
+    unsigned num = d.read_unsigned();
+    for (unsigned i = 0; i < num; i++)
+        parts.push_back(read_name(d));
+    fixity fx = static_cast<fixity>(d.read_char());
+    unsigned p = d.read_unsigned();
+    expr e = read_expr(d);
+    switch (fx) {
+    case fixity::Infix:   lean_assert(parts.size() == 1); add_infix(env, ios, parts[0], p, e); return;
+    case fixity::Infixl:  lean_assert(parts.size() == 1); add_infixl(env, ios, parts[0], p, e); return;
+    case fixity::Infixr:  lean_assert(parts.size() == 1); add_infixr(env, ios, parts[0], p, e); return;
+    case fixity::Prefix:  lean_assert(parts.size() == 1); add_prefix(env, ios, parts[0], p, e); return;
+    case fixity::Postfix: lean_assert(parts.size() == 1); add_postfix(env, ios, parts[0], p, e); return;
+    case fixity::Mixfixl: add_mixfixl(env, ios, parts.size(), parts.data(), p, e); return;
+    case fixity::Mixfixr: add_mixfixr(env, ios, parts.size(), parts.data(), p, e); return;
+    case fixity::Mixfixc: add_mixfixc(env, ios, parts.size(), parts.data(), p, e); return;
+    case fixity::Mixfixo: add_mixfixo(env, ios, parts.size(), parts.data(), p, e); return;
+    }
+}
+static object_cell::register_deserializer_fn notation_ds("Notation", read_notation);
+
 std::ostream & operator<<(std::ostream & out, operator_info const & o) {
     out << pp(o);
     return out;

src/frontends/lean/operator_info.h

@@ -126,5 +126,6 @@ public:
     virtual char const * keyword() const;
     operator_info get_op() const { return m_op; }
     expr const & get_expr() const { return m_expr; }
+    virtual void write(serializer & s) const;
 };
 }

src/kernel/environment.cpp

@@ -21,6 +21,22 @@ Author: Leonardo de Moura
 #include "kernel/normalizer.h"
 
 namespace lean {
+class set_opaque_command : public neutral_object_cell {
+    name m_obj_name;
+    bool m_opaque;
+public:
+    set_opaque_command(name const & n, bool opaque):m_obj_name(n), m_opaque(opaque) {}
+    virtual ~set_opaque_command() {}
+    virtual char const * keyword() const { return "SetOpaque"; }
+    virtual void write(serializer & s) const { s << "SetOpaque" << m_obj_name << m_opaque; }
+};
+static void read_set_opaque(environment const & env, io_state const &, deserializer & d) {
+    name n = read_name(d);
+    bool o = d.read_bool();
+    env->set_opaque(n, o);
+}
+static object_cell::register_deserializer_fn set_opaque_ds("SetOpaque", read_set_opaque);
+
 static name g_builtin_module("builtin_module");
 class extension_factory {
     std::vector<environment_cell::mk_extension> m_makers;
@@ -323,7 +339,9 @@ void environment_cell::add_definition(name const & n, expr const & t, expr const
     check_no_cached_type(v);
     check_new_definition(n, t, v);
     unsigned w = get_max_weight(v) + 1;
-    register_named_object(mk_definition(n, t, v, opaque, w));
+    register_named_object(mk_definition(n, t, v, w));
+    if (opaque)
+        set_opaque(n, opaque);
 }
 
 /**
@@ -335,7 +353,9 @@ void environment_cell::add_definition(name const & n, expr const & v, bool opaqu
     check_name(n);
     expr v_t = m_type_checker->check(v);
     unsigned w = get_max_weight(v) + 1;
-    register_named_object(mk_definition(n, v_t, v, opaque, w));
+    register_named_object(mk_definition(n, v_t, v, w));
+    if (opaque)
+        set_opaque(n, opaque);
 }
 
 /** \brief Add new theorem. */
@@ -351,6 +371,7 @@ void environment_cell::set_opaque(name const & n, bool opaque) {
     if (!obj || !obj->is_definition())
         throw kernel_exception(env(), sstream() << "set_opaque failed, '" << n << "' is not a definition");
     obj->set_opaque(opaque);
+    add_neutral_object(new set_opaque_command(n, opaque));
 }
 
 /** \brief Add new axiom. */

src/kernel/expr.cpp

@@ -208,7 +208,7 @@ expr_value::~expr_value() {
 }
 typedef std::unordered_map<std::string, value::reader> value_readers;
 static std::unique_ptr<value_readers> g_value_readers;
-std::unordered_map<std::string, value::reader> & get_value_readers() {
+value_readers & get_value_readers() {
     if (!g_value_readers)
         g_value_readers.reset(new value_readers());
     return *(g_value_readers.get());

src/kernel/object.cpp

@@ -4,10 +4,32 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <string>
 #include "kernel/object.h"
 #include "kernel/environment.h"
 
 namespace lean {
+typedef std::unordered_map<std::string, object_cell::reader> object_readers;
+static std::unique_ptr<object_readers> g_object_readers;
+object_readers & get_object_readers() {
+    if (!g_object_readers)
+        g_object_readers.reset(new object_readers());
+    return *(g_object_readers.get());
+}
+
+void object_cell::register_deserializer(std::string const & k, reader rd) {
+    object_readers & readers = get_object_readers();
+    lean_assert(readers.find(k) == readers.end());
+    readers[k] = rd;
+}
+static void read_object(environment const & env, io_state const & ios, deserializer & d) {
+    auto k  = d.read_string();
+    object_readers & readers = get_object_readers();
+    auto it = readers.find(k);
+    lean_assert(it != readers.end());
+    it->second(env, ios, d);
+}
+
 neutral_object_cell::neutral_object_cell():object_cell(object_kind::Neutral) {}
 
 /**
@@ -38,7 +60,14 @@ public:
     virtual bool has_cnstr_level() const  { return true; }
     virtual level get_cnstr_level() const { return m_level; }
     virtual char const * keyword() const  { return "Universe"; }
+    virtual void write(serializer & s) const { s << "Universe" << get_name() << m_level; }
 };
+static void read_uvar_decl(environment const & env, io_state const &, deserializer & d) {
+    name n    = read_name(d);
+    level lvl = read_level(d);
+    env->add_uvar(n, lvl);
+}
+static object_cell::register_deserializer_fn uvar_ds("Universe", read_uvar_decl);
 
 /**
    \brief Builtin object.
@@ -60,7 +89,14 @@ public:
     virtual expr get_value() const       { return m_value; }
     virtual char const * keyword() const { return "Builtin"; }
     virtual bool is_builtin() const      { return true; }
+    virtual void write(serializer & s) const { s << "Builtin" << m_value; }
 };
+static void read_builtin(environment const & env, io_state const &, deserializer & d) {
+    expr v      = read_expr(d);
+    env->add_builtin(v);
+}
+static object_cell::register_deserializer_fn builtin_ds("Builtin", read_builtin);
+
 
 /**
    \brief Base class for capturing a set of builtin objects such as
@@ -84,7 +120,12 @@ public:
     virtual bool is_builtin_set() const { return true; }
     virtual bool in_builtin_set(expr const & v) const { return is_value(v) && typeid(to_value(v)) == typeid(to_value(m_representative)); }
     virtual char const * keyword() const { return "BuiltinSet"; }
+    virtual void write(serializer & s) const { s << "BuiltinSet" << m_representative; }
 };
+static void read_builtin_set(environment const & env, io_state const &, deserializer & d) {
+    env->add_builtin_set(read_expr(d));
+}
+static object_cell::register_deserializer_fn builtin_set_ds("BuiltinSet", read_builtin_set);
 
 /**
    \brief Named (and typed) kernel objects.
@@ -117,7 +158,15 @@ public:
     axiom_object_cell(name const & n, expr const & t):postulate_object_cell(n, t) {}
     virtual char const * keyword() const { return "Axiom"; }
     virtual bool is_axiom() const { return true; }
+    virtual void write(serializer & s) const { s << "Axiom" << get_name() << get_type(); }
 };
+static void read_axiom(environment const & env, io_state const &, deserializer & d) {
+    name n    = read_name(d);
+    expr t    = read_expr(d);
+    env->add_axiom(n, t);
+}
+static object_cell::register_deserializer_fn axiom_ds("Axiom", read_axiom);
+
 
 /**
    \brief Variable (aka constant) declaration
@@ -127,7 +176,14 @@ public:
     variable_decl_object_cell(name const & n, expr const & t):postulate_object_cell(n, t) {}
     virtual char const * keyword() const { return "Variable"; }
     virtual bool is_var_decl() const { return true; }
+    virtual void write(serializer & s) const { s << "Variable" << get_name() << get_type(); }
 };
+static void read_variable(environment const & env, io_state const &, deserializer & d) {
+    name n    = read_name(d);
+    expr t    = read_expr(d);
+    env->add_var(n, t);
+}
+static object_cell::register_deserializer_fn var_decl_ds("Variable", read_variable);
 
 /**
    \brief Base class for definitions: theorems and definitions.
@@ -137,8 +193,8 @@ class definition_object_cell : public named_typed_object_cell {
     bool     m_opaque;
     unsigned m_weight;
 public:
-    definition_object_cell(name const & n, expr const & t, expr const & v, bool opaque, unsigned weight):
+    definition_object_cell(name const & n, expr const & t, expr const & v, unsigned weight):
-        named_typed_object_cell(object_kind::Definition, n, t), m_value(v), m_opaque(opaque), m_weight(weight) {}
+        named_typed_object_cell(object_kind::Definition, n, t), m_value(v), m_weight(weight) {}
     virtual ~definition_object_cell() {}
 
     virtual bool is_definition() const   { return true; }
@@ -147,7 +203,15 @@ public:
     virtual expr get_value() const       { return m_value; }
     virtual char const * keyword() const { return "Definition"; }
     virtual unsigned get_weight() const  { return m_weight; }
+    virtual void write(serializer & s) const { s << "Definition" << get_name() << get_type() << get_value(); }
 };
+static void read_definition(environment const & env, io_state const &, deserializer & d) {
+    name n    = read_name(d);
+    expr t    = read_expr(d);
+    expr v    = read_expr(d);
+    env->add_definition(n, t, v);
+}
+static object_cell::register_deserializer_fn definition_ds("Definition", read_definition);
 
 /**
    \brief Theorems
@@ -155,13 +219,23 @@ public:
 class theorem_object_cell : public definition_object_cell {
 public:
     theorem_object_cell(name const & n, expr const & t, expr const & v):
-        definition_object_cell(n, t, v, true, 0) {}
+        definition_object_cell(n, t, v, 0) {
+        set_opaque(true);
+    }
     virtual char const * keyword() const { return "Theorem"; }
     virtual bool is_theorem() const { return true; }
+    virtual void write(serializer & s) const { s << "Theorem" << get_name() << get_type() << get_value(); }
 };
+static void read_theorem(environment const & env, io_state const &, deserializer & d) {
+    name n    = read_name(d);
+    expr t    = read_expr(d);
+    expr v    = read_expr(d);
+    env->add_theorem(n, t, v);
+}
+static object_cell::register_deserializer_fn theorem_ds("Theorem", read_theorem);
 
 object mk_uvar_decl(name const & n, level const & l) { return object(new uvar_declaration_object_cell(n, l)); }
-object mk_definition(name const & n, expr const & t, expr const & v, bool opaque, unsigned weight) { return object(new definition_object_cell(n, t, v, opaque, weight)); }
+object mk_definition(name const & n, expr const & t, expr const & v, unsigned weight) { return object(new definition_object_cell(n, t, v, weight)); }
 object mk_theorem(name const & n, expr const & t, expr const & v) { return object(new theorem_object_cell(n, t, v)); }
 object mk_axiom(name const & n, expr const & t) { return object(new axiom_object_cell(n, t)); }
 object mk_var_decl(name const & n, expr const & t) { return object(new variable_decl_object_cell(n, t)); }

src/kernel/object.h

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <algorithm>
+#include <string>
 #include "util/rc.h"
 #include "kernel/expr.h"
 /*
@@ -15,6 +16,7 @@ Author: Leonardo de Moura
   frontend may need to create new objects for bookkeeping.
 */
 namespace lean {
+class io_state;
 class object;
 enum class object_kind { UVarDeclaration, Definition, Postulate, Builtin, BuiltinSet, Neutral };
 
@@ -69,6 +71,13 @@ public:
     virtual bool in_builtin_set(expr const &) const { return false; }
 
     virtual unsigned get_weight() const { return 0; }
+
+    virtual void write(serializer & ) const = 0;
+    typedef void (*reader)(environment const & env, io_state const & ios, deserializer & d);
+    static void register_deserializer(std::string const & k, reader rd);
+    struct register_deserializer_fn {
+        register_deserializer_fn(std::string const & k, reader rd) { register_deserializer(k, rd); }
+    };
 };
 
 /**
@@ -103,7 +112,7 @@ public:
     object_kind kind() const { return m_ptr->kind(); }
 
     friend object mk_uvar_decl(name const & n, level const & l);
-    friend object mk_definition(name const & n, expr const & t, expr const & v, bool opaque, unsigned weight);
+    friend object mk_definition(name const & n, expr const & t, expr const & v, unsigned weight);
     friend object mk_theorem(name const & n, expr const & t, expr const & v);
     friend object mk_axiom(name const & n, expr const & t);
     friend object mk_var_decl(name const & n, expr const & t);
@@ -140,7 +149,7 @@ inline optional<object> some_object(object && o) { return optional<object>(std::
 object mk_uvar_decl(name const & n, level const & l);
 object mk_builtin(expr const & v);
 object mk_builtin_set(expr const & r);
-object mk_definition(name const & n, expr const & t, expr const & v, bool opaque, unsigned weight);
+object mk_definition(name const & n, expr const & t, expr const & v, unsigned weight);
 object mk_theorem(name const & n, expr const & t, expr const & v);
 object mk_axiom(name const & n, expr const & t);
 object mk_var_decl(name const & n, expr const & t);

src/tests/frontends/lean/frontend.cpp

@@ -97,6 +97,7 @@ public:
     alien_cell() {}
     unsigned & get_data(unsigned i) { return m_data[i]; }
     virtual char const * keyword() const { return "alien"; }
+    virtual void write(serializer & ) const { lean_unreachable(); } // LCOV_EXCL_LINE
 };
 
 static void tst6() {