michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(kernel/object): compact object serialization kind ids

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-29 19:19:24 -08:00
parent d0fdc3619b
commit dbd122301a
5 changed files with 12 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

BIN
src/builtin/basic.olean
View file

Binary file not shown.

BIN
src/builtin/cast.olean
View file

Binary file not shown.

4
src/frontends/lean/frontend.cpp
View file

@ -39,7 +39,7 @@ public:
virtual char const * keyword() const { return "MarkImplicit"; } virtual char const * keyword() const { return "MarkImplicit"; }
virtual void write(serializer & s) const { virtual void write(serializer & s) const {
unsigned sz = m_implicit.size(); unsigned sz = m_implicit.size();
s << "MarkImplicit" << m_obj_name << sz; s << "Imp" << m_obj_name << sz;
for (auto b : m_implicit) for (auto b : m_implicit)
s << b; s << b;
} }
@ -52,7 +52,7 @@ static void read_mark_implicit(environment const & env, io_state const &, deseri
implicit.push_back(d.read_bool()); implicit.push_back(d.read_bool());
mark_implicit_arguments(env, n, implicit.size(), implicit.data()); mark_implicit_arguments(env, n, implicit.size(), implicit.data());
} }
static object_cell::register_deserializer_fn mark_implicit_ds("MarkImplicit", read_mark_implicit); static object_cell::register_deserializer_fn mark_implicit_ds("Imp", read_mark_implicit);
static std::vector<bool> g_empty_vector; static std::vector<bool> g_empty_vector;
/** /**

4
src/kernel/environment.cpp
View file

@ -33,14 +33,14 @@ public:
set_opaque_command(name const & n, bool opaque):m_obj_name(n), m_opaque(opaque) {} set_opaque_command(name const & n, bool opaque):m_obj_name(n), m_opaque(opaque) {}
virtual ~set_opaque_command() {} virtual ~set_opaque_command() {}
virtual char const * keyword() const { return "SetOpaque"; } virtual char const * keyword() const { return "SetOpaque"; }
virtual void write(serializer & s) const { s << "SetOpaque" << m_obj_name << m_opaque; } virtual void write(serializer & s) const { s << "Opa" << m_obj_name << m_opaque; }
}; };
static void read_set_opaque(environment const & env, io_state const &, deserializer & d) { static void read_set_opaque(environment const & env, io_state const &, deserializer & d) {
name n = read_name(d); name n = read_name(d);
bool o = d.read_bool(); bool o = d.read_bool();
env->set_opaque(n, o); env->set_opaque(n, o);
} }
static object_cell::register_deserializer_fn set_opaque_ds("SetOpaque", read_set_opaque); static object_cell::register_deserializer_fn set_opaque_ds("Opa", read_set_opaque);
class import_command : public neutral_object_cell { class import_command : public neutral_object_cell {
std::string m_mod_name; std::string m_mod_name;

16
src/kernel/object.cpp
View file

@ -157,14 +157,14 @@ public:
axiom_object_cell(name const & n, expr const & t):postulate_object_cell(n, t) {} axiom_object_cell(name const & n, expr const & t):postulate_object_cell(n, t) {}
virtual char const * keyword() const { return "Axiom"; } virtual char const * keyword() const { return "Axiom"; }
virtual bool is_axiom() const { return true; } virtual bool is_axiom() const { return true; }
virtual void write(serializer & s) const { s << "Axiom" << get_name() << get_type(); } virtual void write(serializer & s) const { s << "Ax" << get_name() << get_type(); }
}; };
static void read_axiom(environment const & env, io_state const &, deserializer & d) { static void read_axiom(environment const & env, io_state const &, deserializer & d) {
name n = read_name(d); name n = read_name(d);
expr t = read_expr(d); expr t = read_expr(d);
env->add_axiom(n, t); env->add_axiom(n, t);
} }
static object_cell::register_deserializer_fn axiom_ds("Axiom", read_axiom); static object_cell::register_deserializer_fn axiom_ds("Ax", read_axiom);
/** /**
@ -175,14 +175,14 @@ public:
variable_decl_object_cell(name const & n, expr const & t):postulate_object_cell(n, t) {} variable_decl_object_cell(name const & n, expr const & t):postulate_object_cell(n, t) {}
virtual char const * keyword() const { return "Variable"; } virtual char const * keyword() const { return "Variable"; }
virtual bool is_var_decl() const { return true; } virtual bool is_var_decl() const { return true; }
virtual void write(serializer & s) const { s << "Variable" << get_name() << get_type(); } virtual void write(serializer & s) const { s << "Var" << get_name() << get_type(); }
}; };
static void read_variable(environment const & env, io_state const &, deserializer & d) { static void read_variable(environment const & env, io_state const &, deserializer & d) {
name n = read_name(d); name n = read_name(d);
expr t = read_expr(d); expr t = read_expr(d);
env->add_var(n, t); env->add_var(n, t);
} }
static object_cell::register_deserializer_fn var_decl_ds("Variable", read_variable); static object_cell::register_deserializer_fn var_decl_ds("Var", read_variable);
/** /**
\brief Base class for definitions: theorems and definitions. \brief Base class for definitions: theorems and definitions.
@ -202,7 +202,7 @@ public:
virtual expr get_value() const { return m_value; } virtual expr get_value() const { return m_value; }
virtual char const * keyword() const { return "Definition"; } virtual char const * keyword() const { return "Definition"; }
virtual unsigned get_weight() const { return m_weight; } virtual unsigned get_weight() const { return m_weight; }
virtual void write(serializer & s) const { s << "Definition" << get_name() << get_type() << get_value(); } virtual void write(serializer & s) const { s << "Def" << get_name() << get_type() << get_value(); }
}; };
static void read_definition(environment const & env, io_state const &, deserializer & d) { static void read_definition(environment const & env, io_state const &, deserializer & d) {
name n = read_name(d); name n = read_name(d);
@ -210,7 +210,7 @@ static void read_definition(environment const & env, io_state const &, deseriali
expr v = read_expr(d); expr v = read_expr(d);
env->add_definition(n, t, v); env->add_definition(n, t, v);
} }
static object_cell::register_deserializer_fn definition_ds("Definition", read_definition); static object_cell::register_deserializer_fn definition_ds("Def", read_definition);
/** /**
\brief Theorems \brief Theorems
@ -223,7 +223,7 @@ public:
} }
virtual char const * keyword() const { return "Theorem"; } virtual char const * keyword() const { return "Theorem"; }
virtual bool is_theorem() const { return true; } virtual bool is_theorem() const { return true; }
virtual void write(serializer & s) const { s << "Theorem" << get_name() << get_type() << get_value(); } virtual void write(serializer & s) const { s << "Th" << get_name() << get_type() << get_value(); }
}; };
static void read_theorem(environment const & env, io_state const &, deserializer & d) { static void read_theorem(environment const & env, io_state const &, deserializer & d) {
name n = read_name(d); name n = read_name(d);
@ -231,7 +231,7 @@ static void read_theorem(environment const & env, io_state const &, deserializer
expr v = read_expr(d); expr v = read_expr(d);
env->add_theorem(n, t, v); env->add_theorem(n, t, v);
} }
static object_cell::register_deserializer_fn theorem_ds("Theorem", read_theorem); static object_cell::register_deserializer_fn theorem_ds("Th", read_theorem);
object mk_uvar_decl(name const & n, level const & l) { return object(new uvar_declaration_object_cell(n, l)); } 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, unsigned weight) { return object(new definition_object_cell(n, t, v, 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)); }