From f986963a95cf1bbf5516e1e8a8d8a56f546d8760 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 17 Feb 2014 21:32:24 -0800 Subject: [PATCH] refactor(kernel): serializer and deserializer Signed-off-by: Leonardo de Moura --- src/kernel/CMakeLists.txt | 8 +-- src/kernel/expr.cpp | 135 ++++++++++++++++++++----------------- src/kernel/max_sharing.cpp | 40 ++++------- 3 files changed, 88 insertions(+), 95 deletions(-) diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt index 361b617b2..4f8ef15aa 100644 --- a/src/kernel/CMakeLists.txt +++ b/src/kernel/CMakeLists.txt @@ -1,11 +1,11 @@ add_library(kernel level.cpp diff_cnstrs.cpp expr.cpp expr_eq_fn.cpp for_each_fn.cpp occurs.cpp replace_fn.cpp free_vars.cpp abstract.cpp -instantiate.cpp context.cpp formatter.cpp -# normalizer.cpp context.cpp level.cpp object.cpp environment.cpp -# type_checker.cpp kernel.cpp occurs.cpp metavar.cpp +instantiate.cpp context.cpp formatter.cpp max_sharing.cpp +# normalizer.cpp object.cpp environment.cpp +# type_checker.cpp kernel.cpp metavar.cpp # justification.cpp unification_constraint.cpp kernel_exception.cpp # type_checker_justification.cpp pos_info_provider.cpp -# replace_visitor.cpp update_expr.cpp io_state.cpp max_sharing.cpp +# replace_visitor.cpp update_expr.cpp io_state.cpp # universe_constraints.cpp ) diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index a47d499a8..b94940751 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -16,7 +16,7 @@ Author: Leonardo de Moura #include "kernel/expr.h" #include "kernel/expr_eq_fn.h" #include "kernel/free_vars.h" -// #include "kernel/max_sharing.h" +#include "kernel/max_sharing.h" namespace lean { static expr g_dummy(mk_var(0)); @@ -384,7 +384,21 @@ expr copy(expr const & a) { lean_unreachable(); // LCOV_EXCL_LINE } -#if 0 +serializer & operator<<(serializer & s, levels const & ls) { + s << length(ls); + for (auto const & l : ls) + s << l; + return s; +} + +levels read_levels(deserializer & d) { + unsigned num = d.read_unsigned(); + buffer ls; + for (unsigned i = 0; i < num; i++) + ls.push_back(read_level(d)); + return to_list(ls.begin(), ls.end()); +} + class expr_serializer : public object_serializer { typedef object_serializer super; max_sharing_fn m_max_sharing_fn; @@ -401,26 +415,39 @@ class expr_serializer : public object_serializer(k), [&]() { serializer & s = get_owner(); switch (k) { - case expr_kind::Var: s << var_idx(a); break; - case expr_kind::Constant: s << const_name(a); write_core(const_type(a)); break; - case expr_kind::Type: s << ty_level(a); break; - case expr_kind::Value: to_value(a).write(s); break; - case expr_kind::Pair: write_core(pair_first(a)); write_core(pair_second(a)); write_core(pair_type(a)); break; - case expr_kind::Proj: s << proj_first(a); write_core(proj_arg(a)); break; - case expr_kind::HEq: write_core(heq_lhs(a)); write_core(heq_rhs(a)); break; - case expr_kind::App: - s << num_args(a); - for (unsigned i = 0; i < num_args(a); i++) - write_core(arg(a, i)); + case expr_kind::Var: + s << var_idx(a); + break; + case expr_kind::Constant: + s << const_name(a) << const_level_params(a); + break; + case expr_kind::Sort: + s << sort_level(a); + break; + case expr_kind::Macro: + to_macro(a).write(s); + break; + case expr_kind::Pair: + write_core(pair_first(a)); write_core(pair_second(a)); write_core(pair_type(a)); + break; + case expr_kind::Fst: case expr_kind::Snd: + write_core(proj_arg(a)); + break; + case expr_kind::App: + write_core(app_fn(a)); write_core(app_arg(a)); + break; + case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma: + s << binder_name(a); write_core(binder_domain(a)); write_core(binder_body(a)); + break; + case expr_kind::Let: + s << let_name(a); write_core(let_type(a)); write_core(let_value(a)); write_core(let_body(a)); + break; + case expr_kind::Meta: case expr_kind::Local: + s << mlocal_name(a); write_core(mlocal_type(a)); break; - case expr_kind::Lambda: - case expr_kind::Pi: - case expr_kind::Sigma: s << abst_name(a); write_core(abst_domain(a)); write_core(abst_body(a)); break; - case expr_kind::Let: s << let_name(a); write_core(let_type(a)); write_core(let_value(a)); write_core(let_body(a)); break; - case expr_kind::MetaVar: s << metavar_name(a) << metavar_lctx(a); break; } }); } @@ -442,74 +469,57 @@ public: } } + expr read_binder(expr_kind k) { + deserializer & d = get_owner(); + name n = read_name(d); + expr t = read(); + return mk_binder(k, n, t, read()); + } + expr read() { return super::read_core([&](char c) { deserializer & d = get_owner(); - if (c >= g_first_app_size_kind) { - // compressed application - unsigned num = c - g_first_app_size_kind; - buffer args; - for (unsigned i = 0; i < num; i++) - args.push_back(read()); - return mk_app(args); - } auto k = static_cast(c); switch (k) { case expr_kind::Var: return mk_var(d.read_unsigned()); case expr_kind::Constant: { auto n = read_name(d); - return mk_constant(n, read_opt()); + return mk_constant(n, read_levels(d)); } - case expr_kind::Type: - return mk_type(read_level(d)); + case expr_kind::Sort: + return mk_sort(read_level(d)); break; - case expr_kind::Value: - return read_value(d); + case expr_kind::Macro: + return read_macro(d); case expr_kind::Pair: { expr f = read(); expr s = read(); return mk_pair(f, s, read()); } - case expr_kind::HEq: { - expr lhs = read(); - return mk_heq(lhs, read()); - } - case expr_kind::Proj: { - bool f = d.read_bool(); - return mk_proj(f, read()); - } + case expr_kind::Fst: + return mk_fst(read()); + case expr_kind::Snd: + return mk_snd(read()); case expr_kind::App: { - buffer args; - unsigned num = d.read_unsigned(); - for (unsigned i = 0; i < num; i++) - args.push_back(read()); - return mk_app(args); - } - case expr_kind::Lambda: { - name n = read_name(d); - expr d = read(); - return mk_lambda(n, d, read()); - } - case expr_kind::Pi: { - name n = read_name(d); - expr d = read(); - return mk_pi(n, d, read()); - } - case expr_kind::Sigma: { - name n = read_name(d); - expr d = read(); - return mk_sigma(n, d, read()); + expr f = read(); + return mk_app(f, read()); } + case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma: + return read_binder(k); case expr_kind::Let: { name n = read_name(d); optional t = read_opt(); expr v = read(); return mk_let(n, t, v, read()); } - case expr_kind::MetaVar: { + case expr_kind::Meta: { name n = read_name(d); - return mk_metavar(n, read_local_context(d)); + return mk_metavar(n, read()); + } + case expr_kind::Local: { + name n = read_name(d); + return mk_local(n, read()); }} throw_corrupted_file(); // LCOV_EXCL_LINE }); @@ -534,5 +544,4 @@ serializer & operator<<(serializer & s, expr const & n) { expr read_expr(deserializer & d) { return d.get_extension(g_expr_sd.m_d_extid).read(); } -#endif } diff --git a/src/kernel/max_sharing.cpp b/src/kernel/max_sharing.cpp index 5d9fe1cc0..af3f014de 100644 --- a/src/kernel/max_sharing.cpp +++ b/src/kernel/max_sharing.cpp @@ -46,45 +46,29 @@ struct max_sharing_fn::imp { } expr res; switch (a.kind()) { - case expr_kind::Constant: - res = update_const(a, apply(const_type(a))); - break; - case expr_kind::Var: case expr_kind::Type: case expr_kind::Value: + case expr_kind::Constant: case expr_kind::Var: + case expr_kind::Sort: case expr_kind::Macro: res = a; break; - case expr_kind::HEq: - res = update_heq(a, apply(heq_lhs(a)), apply(heq_rhs(a))); - break; case expr_kind::Pair: - res = update_pair(a, [=](expr const & f, expr const & s, expr const & t) { - return std::make_tuple(apply(f), apply(s), apply(t)); - }); + res = update_pair(a, apply(pair_first(a)), apply(pair_second(a)), apply(pair_type(a))); break; - case expr_kind::Proj: + case expr_kind::Fst: case expr_kind::Snd: res = update_proj(a, apply(proj_arg(a))); break; case expr_kind::App: - res = update_app(a, [=](expr const & c) { return apply(c); }); + res = update_app(a, apply(app_fn(a)), apply(app_arg(a))); break; - case expr_kind::Sigma: - case expr_kind::Lambda: - case expr_kind::Pi: - res = update_abst(a, [=](expr const & t, expr const & b) { return std::make_pair(apply(t), apply(b)); }); + case expr_kind::Sigma: case expr_kind::Lambda: case expr_kind::Pi: + res = update_binder(a, apply(binder_domain(a)), apply(binder_body(a))); break; case expr_kind::Let: - res = update_let(a, [=](optional const & t, expr const & v, expr const & b) { - return std::make_tuple(apply(t), apply(v), apply(b)); - }); + res = update_let(a, apply(let_type(a)), apply(let_value(a)), apply(let_body(a))); break; - case expr_kind::MetaVar: { - res = update_metavar(a, [=](local_entry const & e) -> local_entry { - if (e.is_inst()) - return mk_inst(e.s(), apply(e.v())); - else - return e; - }); + case expr_kind::Meta: case expr_kind::Local: + res = update_mlocal(a, apply(mlocal_type(a))); break; - }} + } cache(res); return res; } @@ -102,4 +86,4 @@ expr max_sharing(expr const & a) { else return max_sharing_fn::imp()(a); } -} // namespace lean +}