From 22bebbf242ad272fbc01d60f661f8168c1e5c5ff Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 28 Dec 2013 14:39:10 -0800 Subject: [PATCH] feat(kernel/object): serializer for kernel objects Signed-off-by: Leonardo de Moura --- src/frontends/lean/CMakeLists.txt | 2 +- src/frontends/lean/coercion.h | 1 + src/frontends/lean/environment_scope.cpp | 3 +- src/frontends/lean/frontend.cpp | 25 ++++++++ src/frontends/lean/operator_info.cpp | 30 +++++++++ src/frontends/lean/operator_info.h | 1 + src/kernel/environment.cpp | 25 +++++++- src/kernel/expr.cpp | 2 +- src/kernel/object.cpp | 82 ++++++++++++++++++++++-- src/kernel/object.h | 13 +++- src/tests/frontends/lean/frontend.cpp | 1 + 11 files changed, 174 insertions(+), 11 deletions(-) diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index 11295b144..7c9d2dd4b 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/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}) diff --git a/src/frontends/lean/coercion.h b/src/frontends/lean/coercion.h index 378c425a0..addd096c9 100644 --- a/src/frontends/lean/coercion.h +++ b/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; }; } diff --git a/src/frontends/lean/environment_scope.cpp b/src/frontends/lean/environment_scope.cpp index 9751a37bf..aec93e41e 100644 --- a/src/frontends/lean/environment_scope.cpp +++ b/src/frontends/lean/environment_scope.cpp @@ -85,6 +85,7 @@ static expr Fun(expr e, name_map & info_map, dependencies const & d } std::vector export_local_objects(environment const & env) { + // TODO(Leo): Revise using Parameters if (!env->has_parent()) return std::vector(); name_map info_map; @@ -110,7 +111,7 @@ std::vector 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)))); } diff --git a/src/frontends/lean/frontend.cpp b/src/frontends/lean/frontend.cpp index be61f630e..f16ca5057 100644 --- a/src/frontends/lean/frontend.cpp +++ b/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 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 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 g_empty_vector; /** \brief Environment extension object for the Lean default frontend. diff --git a/src/frontends/lean/operator_info.cpp b/src/frontends/lean/operator_info.cpp index 4d410ad2a..c8da18e1a 100644 --- a/src/frontends/lean/operator_info.cpp +++ b/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(m_op.get_fixity()) << m_op.get_precedence() << m_expr; +} +static void read_notation(environment const & env, io_state const & ios, deserializer & d) { + buffer parts; + unsigned num = d.read_unsigned(); + for (unsigned i = 0; i < num; i++) + parts.push_back(read_name(d)); + fixity fx = static_cast(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; diff --git a/src/frontends/lean/operator_info.h b/src/frontends/lean/operator_info.h index 7b3ade8ee..d73a44277 100644 --- a/src/frontends/lean/operator_info.h +++ b/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; }; } diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 97eb697b2..3abce2d35 100644 --- a/src/kernel/environment.cpp +++ b/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 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. */ diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 6590668f6..6a76ce0f4 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -208,7 +208,7 @@ expr_value::~expr_value() { } typedef std::unordered_map value_readers; static std::unique_ptr g_value_readers; -std::unordered_map & get_value_readers() { +value_readers & get_value_readers() { if (!g_value_readers) g_value_readers.reset(new value_readers()); return *(g_value_readers.get()); diff --git a/src/kernel/object.cpp b/src/kernel/object.cpp index 687bb22d7..81eb4627d 100644 --- a/src/kernel/object.cpp +++ b/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 #include "kernel/object.h" #include "kernel/environment.h" namespace lean { +typedef std::unordered_map object_readers; +static std::unique_ptr 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): - named_typed_object_cell(object_kind::Definition, n, t), m_value(v), m_opaque(opaque), m_weight(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_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)); } diff --git a/src/kernel/object.h b/src/kernel/object.h index 863438cf6..ec0d52fa3 100644 --- a/src/kernel/object.h +++ b/src/kernel/object.h @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #pragma once #include +#include #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 some_object(object && o) { return optional(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); diff --git a/src/tests/frontends/lean/frontend.cpp b/src/tests/frontends/lean/frontend.cpp index 4cf916370..83d49a552 100644 --- a/src/tests/frontends/lean/frontend.cpp +++ b/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() {