From dbd122301a900e7a540b05a66226f6bd43dfcd5e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 29 Dec 2013 19:19:24 -0800 Subject: [PATCH] feat(kernel/object): compact object serialization kind ids Signed-off-by: Leonardo de Moura --- src/builtin/basic.olean | Bin 24779 -> 23900 bytes src/builtin/cast.olean | Bin 1205 -> 1143 bytes src/frontends/lean/frontend.cpp | 4 ++-- src/kernel/environment.cpp | 4 ++-- src/kernel/object.cpp | 16 ++++++++-------- 5 files changed, 12 insertions(+), 12 deletions(-) diff --git a/src/builtin/basic.olean b/src/builtin/basic.olean index 4ccb80be958e50779ed6b98ce03b8a44ee5689a6..2c11b4847cc4f49230c4ac0f7cdff7bc07fa0cd4 100644 GIT binary patch delta 1616 zcmZ8hZ)j6j6wgW0MAJr7yZ%|4w7QDh+I49ZR%<3pOj25G7imhNewe+=HM}!{N>}SZekAqg= zPb4uSjN`etGuZ=tzbDYQae9l?9^^C&XL0qNjgypYh>~R;DxqV9K6PC6NDED7Dx9Dz zer$XkLpy5mVfj9BBn7%yXt7iK9g)idBtn{)G1WF(>e};2exuIsSKcMzB@&+9 zvP$SIp%<&>>!sCK>#W|?vK;mcKX&f9JdpHjDP>(XgC%%g!g#&*0kv&WqT*m-O&!ar zLs`QV|E)Vkomw;HmbCwvYLVNlWBe`sX@1zdb8W*X9e;1PqCu3w_ zgAX@to1xMChg{h5wlbhmddzWSvSs)Cqp2jGbktyVQ&OG@EJb^~&~$}BTM=Z*?Q>97 zEE|-U3|ae*iBh0uUEs!xL9?7w*vbPmr|gyHa%wBI@Q^WgY@p@y66`0qx^)%g8DTev z3zcFo`QmU$ZmIaQ$I^-@PjWn+N+vQUkl!QxmoBbVElX=nr=_9})4FhbnRq)`h5s6` z8#{Zf=x$$i3h$WSH=5~GQW;F|*^c4eKVw73jB$;{^d3}#4fsdLJI2)&)A4Yy5nBUx z%wk!DsK{Q}ta&db0?yAA=n*?k&taQ{^~o^Xxo>Fb#*)$^ND zJsC#HWS51>Nh}E{bruXWcVh?&ye=LHs zjzK|`(&L}fqDz!kgh>QR_WYwD$R6}Z5m7-!^+)G!=Wh4hpM$}Vb3ga{`<~zVo!@;u zghq!^cf66~IX@@x$Kq#)!-7cII2c0#4MG~u>%~t^R=gN>$uJ&3LO4#=j)dcJ?N~S- z(6xu-H2v{tg`}qqJ52F-OkZuObosWIx3o5MTR1@4E9GY>5nArj(Z2C&$80>Q+`0^BFi*R z9n1z*xui~7CHP4r=Si8x@@d@&%3ft;#ZS{WpiH1U$UxF=N(8P@DGg+*!AoGS{#Glsh$PP;N zfk4uolH24@@_T6L8)N88%1d~ZzgQiq=CwW--%f{A0=B2>ajgAO8gTHBycxXzvW2hq zL%;&kF%|-8S0G|gBI4><{RkvOW>qrLnBF!4mY~KCXB2C}twwf&vA0?r&oslXMRN%l zxr^eztlkNrJQnKD`2o)h6%a^qUgEWRPPA8DQ$)wJ)8nshb+vVPq~qYEFNCLEgVS2ZdQO4Hd?T_bfC`*al!^n3cbOH7c=z&DoVBErPP8*i`e;;Cu$$`KDsa-A zIHqunF1{{2qow4|Wq)bZvAi#m(80U0E8mWLmzi-{(dCF$@<6g;$F^cRnZ*;u^W_xx z9NARuvm+-q?3BziNl+SROIPfZYcN=HP7XJ&+$4v$Rs~R;@=Y?cw&LLu8*VD=2DcmC zWV^*&-akRN+*WnV!!>Uwpzf=vI~6B&v|x2LPieu#InFpewDFm>vAVuY2ch3A)Z1`T S3m~nYKnShm-K)4}kLEusl)SS5 diff --git a/src/builtin/cast.olean b/src/builtin/cast.olean index 380e07a788b46e6406e3d32d8a6d806ebdf67b28..d706e903236878806cfad7098228c5dc22a141f7 100644 GIT binary patch delta 110 zcmdnW`JH2e(nNJ%LC@R*1{h#sWOS^UII$2e$Oe=F3vQNYjAs;vspSR=voHdIW5wjT YOsnAHk_hq5Y0SEe%s>s3=d*|b0CQv$+yDRo delta 188 zcmey)v6XXz5^H8+QcmhbC0|+J#G-7^+=86UHj6eW3baDyPDoiz!C~7tvGV3z(AR9C} HkwpvuO?xn7 diff --git a/src/frontends/lean/frontend.cpp b/src/frontends/lean/frontend.cpp index 1e6c3bf3ca..24cf908b26 100644 --- a/src/frontends/lean/frontend.cpp +++ b/src/frontends/lean/frontend.cpp @@ -39,7 +39,7 @@ public: virtual char const * keyword() const { return "MarkImplicit"; } virtual void write(serializer & s) const { unsigned sz = m_implicit.size(); - s << "MarkImplicit" << m_obj_name << sz; + s << "Imp" << m_obj_name << sz; for (auto b : m_implicit) s << b; } @@ -52,7 +52,7 @@ static void read_mark_implicit(environment const & env, io_state const &, deseri 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 object_cell::register_deserializer_fn mark_implicit_ds("Imp", read_mark_implicit); static std::vector g_empty_vector; /** diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index fe346455f9..e7d51f9c8d 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -33,14 +33,14 @@ 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; } + 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) { 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 object_cell::register_deserializer_fn set_opaque_ds("Opa", read_set_opaque); class import_command : public neutral_object_cell { std::string m_mod_name; diff --git a/src/kernel/object.cpp b/src/kernel/object.cpp index 83ce8a2993..816517439e 100644 --- a/src/kernel/object.cpp +++ b/src/kernel/object.cpp @@ -157,14 +157,14 @@ 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(); } + virtual void write(serializer & s) const { s << "Ax" << 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); +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) {} 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(); } + virtual void write(serializer & s) const { s << "Var" << 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); +static object_cell::register_deserializer_fn var_decl_ds("Var", read_variable); /** \brief Base class for definitions: theorems and definitions. @@ -202,7 +202,7 @@ 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(); } + 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) { 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); 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 @@ -223,7 +223,7 @@ public: } 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(); } + 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) { 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); 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_definition(name const & n, expr const & t, expr const & v, unsigned weight) { return object(new definition_object_cell(n, t, v, weight)); }