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

refactor(kernel): serializer and deserializer

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-02-17 21:32:24 -08:00
parent 74f74d2f79
commit f986963a95
3 changed files with 88 additions and 95 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/kernel/CMakeLists.txt
View file

@ -1,11 +1,11 @@
add_library(kernel level.cpp diff_cnstrs.cpp expr.cpp expr_eq_fn.cpp 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 for_each_fn.cpp occurs.cpp replace_fn.cpp free_vars.cpp abstract.cpp
instantiate.cpp context.cpp formatter.cpp instantiate.cpp context.cpp formatter.cpp max_sharing.cpp
# normalizer.cpp context.cpp level.cpp object.cpp environment.cpp # normalizer.cpp object.cpp environment.cpp
# type_checker.cpp kernel.cpp occurs.cpp metavar.cpp # type_checker.cpp kernel.cpp metavar.cpp
# justification.cpp unification_constraint.cpp kernel_exception.cpp # justification.cpp unification_constraint.cpp kernel_exception.cpp
# type_checker_justification.cpp pos_info_provider.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 # universe_constraints.cpp
) )

135
src/kernel/expr.cpp
View file

@ -16,7 +16,7 @@ Author: Leonardo de Moura
#include "kernel/expr.h" #include "kernel/expr.h"
#include "kernel/expr_eq_fn.h" #include "kernel/expr_eq_fn.h"
#include "kernel/free_vars.h" #include "kernel/free_vars.h"
// #include "kernel/max_sharing.h" #include "kernel/max_sharing.h"
namespace lean { namespace lean {
static expr g_dummy(mk_var(0)); static expr g_dummy(mk_var(0));
@ -384,7 +384,21 @@ expr copy(expr const & a) {
lean_unreachable(); // LCOV_EXCL_LINE 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<level> 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<expr, expr_hash_alloc, expr_eqp> { class expr_serializer : public object_serializer<expr, expr_hash_alloc, expr_eqp> {
typedef object_serializer<expr, expr_hash_alloc, expr_eqp> super; typedef object_serializer<expr, expr_hash_alloc, expr_eqp> super;
max_sharing_fn m_max_sharing_fn; max_sharing_fn m_max_sharing_fn;
@ -401,26 +415,39 @@ class expr_serializer : public object_serializer<expr, expr_hash_alloc, expr_eqp
void write_core(expr const & a) { void write_core(expr const & a) {
auto k = a.kind(); auto k = a.kind();
super::write_core(a, k, [&]() { super::write_core(a, static_cast<char>(k), [&]() {
serializer & s = get_owner(); serializer & s = get_owner();
switch (k) { switch (k) {
case expr_kind::Var: s << var_idx(a); break; case expr_kind::Var:
case expr_kind::Constant: s << const_name(a); write_core(const_type(a)); break; s << var_idx(a);
case expr_kind::Type: s << ty_level(a); break; break;
case expr_kind::Value: to_value(a).write(s); break; case expr_kind::Constant:
case expr_kind::Pair: write_core(pair_first(a)); write_core(pair_second(a)); write_core(pair_type(a)); break; s << const_name(a) << const_level_params(a);
case expr_kind::Proj: s << proj_first(a); write_core(proj_arg(a)); break; break;
case expr_kind::HEq: write_core(heq_lhs(a)); write_core(heq_rhs(a)); break; case expr_kind::Sort:
case expr_kind::App: s << sort_level(a);
s << num_args(a); break;
for (unsigned i = 0; i < num_args(a); i++) case expr_kind::Macro:
write_core(arg(a, i)); 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; 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() { expr read() {
return super::read_core([&](char c) { return super::read_core([&](char c) {
deserializer & d = get_owner(); deserializer & d = get_owner();
if (c >= g_first_app_size_kind) {
// compressed application
unsigned num = c - g_first_app_size_kind;
buffer<expr> args;
for (unsigned i = 0; i < num; i++)
args.push_back(read());
return mk_app(args);
}
auto k = static_cast<expr_kind>(c); auto k = static_cast<expr_kind>(c);
switch (k) { switch (k) {
case expr_kind::Var: case expr_kind::Var:
return mk_var(d.read_unsigned()); return mk_var(d.read_unsigned());
case expr_kind::Constant: { case expr_kind::Constant: {
auto n = read_name(d); auto n = read_name(d);
return mk_constant(n, read_opt()); return mk_constant(n, read_levels(d));
} }
case expr_kind::Type: case expr_kind::Sort:
return mk_type(read_level(d)); return mk_sort(read_level(d));
break; break;
case expr_kind::Value: case expr_kind::Macro:
return read_value(d); return read_macro(d);
case expr_kind::Pair: { case expr_kind::Pair: {
expr f = read(); expr f = read();
expr s = read(); expr s = read();
return mk_pair(f, s, read()); return mk_pair(f, s, read());
} }
case expr_kind::HEq: { case expr_kind::Fst:
expr lhs = read(); return mk_fst(read());
return mk_heq(lhs, read()); case expr_kind::Snd:
} return mk_snd(read());
case expr_kind::Proj: {
bool f = d.read_bool();
return mk_proj(f, read());
}
case expr_kind::App: { case expr_kind::App: {
buffer<expr> args; expr f = read();
unsigned num = d.read_unsigned(); return mk_app(f, read());
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());
} }
case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma:
return read_binder(k);
case expr_kind::Let: { case expr_kind::Let: {
name n = read_name(d); name n = read_name(d);
optional<expr> t = read_opt(); optional<expr> t = read_opt();
expr v = read(); expr v = read();
return mk_let(n, t, v, read()); return mk_let(n, t, v, read());
} }
case expr_kind::MetaVar: { case expr_kind::Meta: {
name n = read_name(d); 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 throw_corrupted_file(); // LCOV_EXCL_LINE
}); });
@ -534,5 +544,4 @@ serializer & operator<<(serializer & s, expr const & n) {
expr read_expr(deserializer & d) { expr read_expr(deserializer & d) {
return d.get_extension<expr_deserializer>(g_expr_sd.m_d_extid).read(); return d.get_extension<expr_deserializer>(g_expr_sd.m_d_extid).read();
} }
#endif
} }

40
src/kernel/max_sharing.cpp
View file

@ -46,45 +46,29 @@ struct max_sharing_fn::imp {
} }
expr res; expr res;
switch (a.kind()) { switch (a.kind()) {
case expr_kind::Constant: case expr_kind::Constant: case expr_kind::Var:
res = update_const(a, apply(const_type(a))); case expr_kind::Sort: case expr_kind::Macro:
break;
case expr_kind::Var: case expr_kind::Type: case expr_kind::Value:
res = a; res = a;
break; break;
case expr_kind::HEq:
res = update_heq(a, apply(heq_lhs(a)), apply(heq_rhs(a)));
break;
case expr_kind::Pair: case expr_kind::Pair:
res = update_pair(a, [=](expr const & f, expr const & s, expr const & t) { res = update_pair(a, apply(pair_first(a)), apply(pair_second(a)), apply(pair_type(a)));
return std::make_tuple(apply(f), apply(s), apply(t));
});
break; break;
case expr_kind::Proj: case expr_kind::Fst: case expr_kind::Snd:
res = update_proj(a, apply(proj_arg(a))); res = update_proj(a, apply(proj_arg(a)));
break; break;
case expr_kind::App: 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; break;
case expr_kind::Sigma: case expr_kind::Sigma: case expr_kind::Lambda: case expr_kind::Pi:
case expr_kind::Lambda: res = update_binder(a, apply(binder_domain(a)), apply(binder_body(a)));
case expr_kind::Pi:
res = update_abst(a, [=](expr const & t, expr const & b) { return std::make_pair(apply(t), apply(b)); });
break; break;
case expr_kind::Let: case expr_kind::Let:
res = update_let(a, [=](optional<expr> const & t, expr const & v, expr const & b) { res = update_let(a, apply(let_type(a)), apply(let_value(a)), apply(let_body(a)));
return std::make_tuple(apply(t), apply(v), apply(b));
});
break; break;
case expr_kind::MetaVar: { case expr_kind::Meta: case expr_kind::Local:
res = update_metavar(a, [=](local_entry const & e) -> local_entry { res = update_mlocal(a, apply(mlocal_type(a)));
if (e.is_inst())
return mk_inst(e.s(), apply(e.v()));
else
return e;
});
break; break;
}} }
cache(res); cache(res);
return res; return res;
} }
@ -102,4 +86,4 @@ expr max_sharing(expr const & a) {
else else
return max_sharing_fn::imp()(a); return max_sharing_fn::imp()(a);
} }
} // namespace lean }