From 01ea596aea45bbf0df99db60839a55b3965fc58b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 21 Jun 2018 14:04:18 -0700 Subject: [PATCH] refactor(kernel/expr): implement `expr` using `runtime/object` --- src/frontends/lean/builtin_exprs.cpp | 2 +- src/frontends/lean/definition_cmds.cpp | 4 +- src/frontends/lean/elaborator.cpp | 16 +- src/frontends/lean/notation_cmd.cpp | 2 +- src/frontends/lean/parse_table.cpp | 4 +- src/frontends/lean/parser.cpp | 10 +- src/frontends/lean/pp.cpp | 9 +- src/kernel/equiv_manager.cpp | 8 +- src/kernel/expr.cpp | 961 ++++++++---------- src/kernel/expr.h | 630 +++--------- src/kernel/expr_cache.cpp | 4 +- src/kernel/expr_eq_fn.cpp | 12 +- src/kernel/expr_pair.h | 2 +- src/kernel/for_each_fn.cpp | 10 +- src/kernel/instantiate.cpp | 14 +- src/kernel/level.h | 1 + src/kernel/old_type_checker.cpp | 36 +- src/kernel/replace_fn.cpp | 14 +- src/kernel/type_checker.cpp | 44 +- src/library/check.cpp | 2 +- src/library/compiler/cse.cpp | 6 +- src/library/compiler/inliner.cpp | 9 +- src/library/compiler/vm_compiler.cpp | 2 +- src/library/context_cache.cpp | 6 +- src/library/deep_copy.cpp | 26 +- .../equations_compiler/structural_rec.cpp | 2 +- src/library/expr_lt.cpp | 12 +- src/library/expr_unsigned_map.h | 2 +- src/library/head_map.cpp | 4 +- src/library/head_map.h | 2 +- src/library/inductive_compiler/nested.cpp | 4 +- src/library/kernel_serializer.cpp | 174 ---- src/library/kernel_serializer.h | 15 - src/library/locals.cpp | 2 +- src/library/max_sharing.cpp | 2 +- src/library/noncomputable.cpp | 26 +- src/library/normalize.cpp | 4 +- src/library/pos_info_provider.cpp | 22 +- src/library/print.cpp | 4 +- src/library/replace_visitor.cpp | 24 +- src/library/tactic/dsimplify.cpp | 2 +- src/library/tactic/kabstract.cpp | 2 +- src/library/tactic/simp_lemmas.cpp | 14 +- src/library/tactic/simplify.cpp | 2 +- src/library/type_context.cpp | 18 +- src/library/vm/vm_expr.cpp | 8 +- src/runtime/object.h | 1 + src/runtime/serializer.cpp | 68 +- src/runtime/serializer.h | 28 +- src/tests/util/serializer.cpp | 40 - src/util/name.cpp | 5 +- src/util/nat.h | 21 +- src/util/object_ref.h | 8 +- src/util/object_serializer.h | 70 -- src/util/sexpr/sexpr.cpp | 1 - 55 files changed, 870 insertions(+), 1551 deletions(-) delete mode 100644 src/util/object_serializer.h diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index f01582b3d1..1607945f8a 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -1012,7 +1012,7 @@ parse_table init_nud_table() { action Expr(mk_expr_action()); action Skip(mk_skip_action()); action Binders(mk_binders_action()); - expr x0 = mk_var(0); + expr x0 = mk_bvar(0); parse_table r; r = r.add({transition("by", mk_ext_action_core(parse_by))}, x0); r = r.add({transition("have", mk_ext_action(parse_have))}, x0); diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index 83d8dfcae1..a1ea4f17b7 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -334,9 +334,9 @@ static void get_args_for_instantiating_lemma(unsigned arity, buffer const & args, buffer & result) { for (unsigned i = 0; i < args.size(); i++) { - if (!is_var(lhs_args[i]) || var_idx(lhs_args[i]) >= arity) + if (!is_bvar(lhs_args[i]) || bvar_idx(lhs_args[i]) >= arity) throw_unexpected_error_at_copy_lemmas(); - result.push_back(args[arity - var_idx(lhs_args[i]) - 1]); + result.push_back(args[arity - bvar_idx(lhs_args[i]).get_small_value() - 1]); } } diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 4a69303f37..98f8b7b35a 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -967,7 +967,7 @@ expr elaborator::visit_function(expr const & fn, bool has_args, optional c // The expr_kind::App case can only happen when nary notation is used case expr_kind::App: r = visit(fn, expected_type); break; case expr_kind::FVar: r = fn; break; - case expr_kind::Constant: r = visit_const_core(fn); break; + case expr_kind::Const: r = visit_const_core(fn); break; case expr_kind::MData: r = visit_mdata(fn, expected_type, true); break; case expr_kind::Lambda: r = visit_lambda(fn, expected_type); break; case expr_kind::Let: r = visit_let(fn, expected_type); break; @@ -2070,7 +2070,7 @@ static level ground_uvars(level const & l) { static expr ground_uvars(expr const & e) { return replace_propagating_pos(e, [] (expr const & e, unsigned) { - if (!e.has_univ_metavar()) { + if (!has_univ_metavar(e)) { return some_expr(e); } else if (is_sort(e)) { return some_expr(mk_sort(ground_uvars(sort_level(e)))); @@ -2162,7 +2162,7 @@ static expr instantiate_rev_locals(expr const & a, unsigned n, expr const * subs if (offset >= get_loose_bvar_range(m)) return some_expr(m); // expression m does not contain free variables with idx >= offset if (is_var(m)) { - unsigned vidx = var_idx(m); + unsigned vidx = bvar_idx(m).get_small_value(); if (vidx >= offset) { unsigned h = offset + n; if (h < offset /* overflow, h is bigger than any vidx */ || vidx < h) { @@ -2170,7 +2170,7 @@ static expr instantiate_rev_locals(expr const & a, unsigned n, expr const * subs lean_assert(is_local(local)); return some_expr(copy_pos(m, copy(local))); } else { - return some_expr(copy_pos(m, mk_var(vidx - n))); + return some_expr(copy_pos(m, mk_bvar(vidx - n))); } } } @@ -2312,9 +2312,9 @@ static void check_equations_arity(buffer const & eqns) { expr const & lhs = equation_lhs(eqn); expr const & fn = get_app_fn(lhs); unsigned arity = get_app_num_args(lhs); - if (!is_var(fn) || var_idx(fn) >= nbinders) + if (!is_var(fn) || bvar_idx(fn) >= nbinders) throw_ill_formed_equation(eqn); - unsigned fidx = nbinders - var_idx(fn) - 1; + unsigned fidx = nbinders - bvar_idx(fn).get_small_value() - 1; if (fidx >= fidx2arity.size()) fidx2arity.resize(fidx+1, optional()); if (auto r = fidx2arity[fidx]) { @@ -3646,7 +3646,7 @@ expr elaborator::visit(expr const & e, optional const & expected_type) { return copy_pos(e, visit_sort(e)); case expr_kind::FVar: return copy_pos(e, visit_local(e, expected_type)); - case expr_kind::Constant: + case expr_kind::Const: return copy_pos(e, visit_constant(e, expected_type)); case expr_kind::Lambda: return copy_pos(e, visit_lambda(e, expected_type)); @@ -4121,7 +4121,7 @@ static optional resolve_local_name_core(environment const & env, local_con unsigned vidx = 0; for (name const & extra : extra_locals) { if (id == extra) - return some_expr(copy_pos(src, mk_var(vidx))); + return some_expr(copy_pos(src, mk_bvar(vidx))); vidx++; } diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp index d461f2cb88..381f1cc7a1 100644 --- a/src/frontends/lean/notation_cmd.cpp +++ b/src/frontends/lean/notation_cmd.cpp @@ -339,7 +339,7 @@ static action parse_action(parser & p, name const & prev_token, unsigned default return mk_expr_action(get_precedence(p.env(), new_tokens, prev_token)); } else if (p.curr_is_token_or_id(get_scoped_tk())) { p.next(); - return mk_scoped_expr_action(mk_var(0)); + return mk_scoped_expr_action(mk_bvar(0)); } else { p.check_token_next(get_lparen_tk(), "invalid notation declaration, '(', numeral or 'scoped' expected"); if (p.curr_is_token_or_id(get_foldl_tk()) || p.curr_is_token_or_id(get_foldr_tk())) { diff --git a/src/frontends/lean/parse_table.cpp b/src/frontends/lean/parse_table.cpp index f237e6fc05..834e12fb61 100644 --- a/src/frontends/lean/parse_table.cpp +++ b/src/frontends/lean/parse_table.cpp @@ -449,8 +449,8 @@ static expr expand_pp_pattern(unsigned num, transition const * ts, expr const & if (!is_var(a)) return a; return replace(a, [&](expr const & e) { - if (is_var(e)) { - unsigned vidx = var_idx(e); + if (is_bvar(e) && bvar_idx(e).is_small()) { + unsigned vidx = bvar_idx(e).get_small_value(); unsigned i = num; unsigned offset = 0; while (i > 0) { diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 0c76f18e6b..e22675c079 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -274,8 +274,8 @@ expr parser::rec_save_pos(expr const & e, pos_info p) { /** \brief Create a copy of \c e, and the position of new expression with p */ expr parser::copy_with_new_pos(expr const & e, pos_info p) { switch (e.kind()) { - case expr_kind::Sort: case expr_kind::Constant: case expr_kind::MVar: - case expr_kind::BVar: case expr_kind::FVar: case expr_kind::Lit: + case expr_kind::Sort: case expr_kind::Const: case expr_kind::MVar: + case expr_kind::BVar: case expr_kind::FVar: case expr_kind::Lit: return save_pos(copy(e), p); case expr_kind::MData: return save_pos(::lean::mk_mdata(mdata_data(e), copy_with_new_pos(mdata_expr(e), p)), p); @@ -1731,10 +1731,10 @@ static expr quote(expr const & e) { } lean_unreachable(); case expr_kind::BVar: - return mk_app(mk_constant({"expr", "bvar"}), quote(var_idx(e))); + return mk_app(mk_constant({"expr", "bvar"}), quote(bvar_idx(e).get_small_value())); case expr_kind::Sort: return mk_app(mk_constant({"expr", "sort"}), mk_expr_placeholder()); - case expr_kind::Constant: + case expr_kind::Const: return mk_app(mk_constant({"expr", "const"}), quote(const_name(e)), mk_expr_placeholder()); case expr_kind::MVar: return mk_expr_placeholder(); @@ -1902,7 +1902,7 @@ optional parser::resolve_local(name const & id, pos_info const & p, names unsigned vidx = 0; for (name const & extra : extra_locals) { if (id == extra) - return some_expr(save_pos(mk_var(vidx), p)); + return some_expr(save_pos(mk_bvar(vidx), p)); vidx++; } diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 5ceb87f366..21eed99c2d 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -635,8 +635,7 @@ auto pretty_fn::pp_child(expr const & e, unsigned bp, bool ignore_hide) -> resul } auto pretty_fn::pp_var(expr const & e) -> result { - unsigned vidx = var_idx(e); - return result(compose(format("#"), format(vidx))); + return result(compose(format("#"), format(bvar_idx(e).to_std_string()))); } auto pretty_fn::pp_sort(expr const & e) -> result { @@ -1235,8 +1234,8 @@ bool pretty_fn::match(expr const & p, expr const & e, buffer> & a return match(get_explicit_arg(p), e, args); } else if (is_as_atomic(p)) { return match(get_app_fn(get_as_atomic_arg(p)), e, args); - } else if (is_var(p)) { - unsigned vidx = var_idx(p); + } else if (is_bvar(p) && bvar_idx(p).is_small()) { + unsigned vidx = bvar_idx(p).get_small_value(); if (vidx >= args.size()) return false; unsigned i = args.size() - vidx - 1; @@ -1760,7 +1759,7 @@ auto pretty_fn::pp(expr const & e, bool ignore_hide) -> result { case expr_kind::Sort: return pp_sort(e); case expr_kind::MData: return pp_mdata(e); case expr_kind::Proj: return pp_proj(e); - case expr_kind::Constant: return pp_const(e); + case expr_kind::Const: return pp_const(e); case expr_kind::MVar: return pp_meta(e); case expr_kind::App: return pp_app(e); case expr_kind::Lambda: return pp_lambda(e); diff --git a/src/kernel/equiv_manager.cpp b/src/kernel/equiv_manager.cpp index b7943ee298..6912990e97 100644 --- a/src/kernel/equiv_manager.cpp +++ b/src/kernel/equiv_manager.cpp @@ -54,9 +54,9 @@ auto equiv_manager::to_node(expr const & e) -> node_ref { } bool equiv_manager::is_equiv_core(expr const & a, expr const & b) { - if (is_eqp(a, b)) return true; - if (m_use_hash && a.hash() != b.hash()) return false; - if (is_var(a) && is_var(b)) return var_idx(a) == var_idx(b); + if (is_eqp(a, b)) return true; + if (m_use_hash && hash(a) != hash(b)) return false; + if (is_bvar(a) && is_bvar(b)) return bvar_idx(a) == bvar_idx(b); node_ref r1 = find(to_node(a)); node_ref r2 = find(to_node(b)); if (r1 == r2) @@ -69,7 +69,7 @@ bool equiv_manager::is_equiv_core(expr const & a, expr const & b) { switch (a.kind()) { case expr_kind::BVar: lean_unreachable(); // LCOV_EXCL_LINE - case expr_kind::Constant: + case expr_kind::Const: result = const_name(a) == const_name(b) && compare(const_levels(a), const_levels(b), [](level const & l1, level const & l2) { return l1 == l2; }); diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 6c0c0a2989..2f28a38624 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -13,7 +13,6 @@ Author: Leonardo de Moura #include "util/list_fn.h" #include "util/hash.h" #include "util/buffer.h" -#include "util/object_serializer.h" #include "kernel/expr.h" #include "kernel/expr_eq_fn.h" #include "kernel/expr_sets.h" @@ -58,32 +57,102 @@ bool operator<(literal const & a, literal const & b) { lean_unreachable(); } -/* Auxiliary functions for computing scalar data offset into expression objects. */ +static inline unsigned hash(literal const & a) { + switch (a.kind()) { + case literal_kind::Nat: return a.get_nat().hash(); + case literal_kind::String: return hash_str(a.get_string().num_bytes(), a.get_string().data(), 17); + } + lean_unreachable(); +} + +static unsigned hash(levels const & ls) { + unsigned r = 23; + for (auto const & l : ls) + r = hash(hash(l), r); + return r; +} + +std::ostream & operator<<(std::ostream & out, expr_kind const & k) { + switch (k) { + case expr_kind::MData: out << "expr.mdata"; break; + case expr_kind::Proj: out << "expr.proj"; break; + case expr_kind::Lit: out << "expr.lit"; break; + case expr_kind::BVar: out << "expr.bvar"; break; + case expr_kind::FVar: out << "expr.fvar"; break; + case expr_kind::MVar: out << "expr.mvar"; break; + case expr_kind::Sort: out << "expr.sort"; break; + case expr_kind::Const: out << "expr.const"; break; + case expr_kind::App: out << "expr.app"; break; + case expr_kind::Lambda: out << "expr.lam"; break; + case expr_kind::Pi: out << "expr.pi"; break; + case expr_kind::Let: out << "expr.elet"; break; + case expr_kind::Quote: out << "expr.quote"; break; + } + return out; +} + +// ======================================= +// Safe arithmetic + +static unsigned safe_add(unsigned w1, unsigned w2) { + unsigned r = w1 + w2; + if (r < w1) + r = std::numeric_limits::max(); // overflow + return r; +} + +static unsigned safe_inc(unsigned w) { + if (w < std::numeric_limits::max()) + return w+1; + else + return w; +} + +static unsigned safe_dec(unsigned k) { + return k == 0 ? 0 : k - 1; +} + + +// ======================================= +// Scalar data offset calculation and setters/getters + inline constexpr unsigned num_obj_fields(expr_kind k) { return - k == expr_kind::App ? 2 : - k == expr_kind::Constant ? 2 : - k == expr_kind::FVar ? 3 : // TODO(Leo): it should be 1 after we remove support for legacy code - k == expr_kind::Lambda ? 3 : - k == expr_kind::Pi ? 3 : - k == expr_kind::BVar ? 1 : - k == expr_kind::Let ? 4 : - k == expr_kind::MVar ? 3 : // TODO(Leo): it should be 2 after we remove support for legacy code - k == expr_kind::Sort ? 1 : - k == expr_kind::Lit ? 1 : - k == expr_kind::MData ? 2 : - k == expr_kind::Proj ? 2 : + k == expr_kind::App ? 2 : + k == expr_kind::Const ? 2 : + k == expr_kind::FVar ? 3 : // TODO(Leo): it should be 1 after we remove support for legacy code + k == expr_kind::Lambda ? 3 : + k == expr_kind::Pi ? 3 : + k == expr_kind::BVar ? 1 : + k == expr_kind::Let ? 4 : + k == expr_kind::MVar ? 3 : // TODO(Leo): it should be 2 after we remove support for legacy code + k == expr_kind::Sort ? 1 : + k == expr_kind::Lit ? 1 : + k == expr_kind::MData ? 2 : + k == expr_kind::Proj ? 2 : /* k == expr_kind::Quote */ 1; } /* Expression scalar data offset. */ inline constexpr unsigned scalar_offset(expr_kind k) { return num_obj_fields(k) * sizeof(object*); } +inline constexpr unsigned binder_info_offset(expr_kind k) { + // Only for: k == expr_kind::Pi || k == expr_kind::Lambda || k == expr_kind::FVar + return scalar_offset(k); +} + +/* Legacy support */ +inline constexpr unsigned reflected_offset(expr_kind k) { + // Only for: k == expr_kind::Quote + return scalar_offset(k); +} + inline constexpr unsigned hash_offset(expr_kind k) { return k == expr_kind::FVar ? scalar_offset(k) + sizeof(unsigned char) : // for binder_info, TODO(Leo): delete after we remove support for legacy code k == expr_kind::Lambda ? scalar_offset(k) + sizeof(unsigned char) : // for binder_info k == expr_kind::Pi ? scalar_offset(k) + sizeof(unsigned char) : // for binder_info + k == expr_kind::Quote ? scalar_offset(k) + sizeof(unsigned char) : // for reflected scalar_offset(k); } @@ -94,245 +163,144 @@ inline constexpr size_t loose_bvar_range_offset(expr_kind k) { return depth_offs /* Size for scalar value area for non recursive expression. */ inline constexpr size_t expr_scalar_size(expr_kind k) { return flags_offset(k) + sizeof(unsigned char); } /* Size for scalar value area for recursive expression. */ -inline constexpr size_t recursive_expr_scalar_size(expr_kind k) { return loose_bvar_range_offset(k) + sizeof(unsigned); } +inline constexpr size_t rec_expr_scalar_size(expr_kind k) { return loose_bvar_range_offset(k) + sizeof(unsigned); } -/* Weight safe arith functions */ -static unsigned add_weight(unsigned w1, unsigned w2) { - unsigned r = w1 + w2; - if (r < w1) - r = std::numeric_limits::max(); // overflow - return r; +/* Set expr cached hash code and flags. All expressions contain them. + We provide the kind `k` to allow the compiler to compute offsets at compilation time. */ +template void set_scalar(expr const & e, unsigned hash, bool has_expr_mvar, bool has_univ_mvar, + bool has_fvar, bool has_univ_param) { + lean_assert(e.kind() == k); + unsigned char d = + (has_expr_mvar ? 1 : 0) + + (has_univ_mvar ? 2 : 0) + + (has_fvar ? 4 : 0) + + (has_univ_param ? 8 : 0); + cnstr_set_scalar(e.raw(), hash_offset(k), hash); + cnstr_set_scalar(e.raw(), flags_offset(k), d); } -static unsigned inc_weight(unsigned w) { - if (w < std::numeric_limits::max()) - return w+1; - else - return w; +/* Set expr cached weight, depth and loose bvar range. We only store this information in recursive expr constructors. + We provide the kind `k` to allow the compiler to compute offsets at compilation time. */ +template void set_rec_scalar(expr const & e, unsigned weight, unsigned depth, unsigned loose_bvar_range) { + lean_assert(e.kind() == k); + cnstr_set_scalar(e.raw(), weight_offset(k), weight); + cnstr_set_scalar(e.raw(), depth_offset(k), depth); + cnstr_set_scalar(e.raw(), loose_bvar_range_offset(k), loose_bvar_range); +} + +template void set_binder_info(expr const & e, binder_info bi) { + lean_assert(e.kind() == k); + cnstr_set_scalar(e.raw(), binder_info_offset(k), static_cast(bi)); +} + +/* Legacy support */ +void set_reflected(expr const & e, bool r) { + cnstr_set_scalar(e.raw(), reflected_offset(expr_kind::Quote), r); +} + +unsigned hash(expr const & e) { return cnstr_scalar(e.raw(), hash_offset(e.kind())); } +static inline unsigned char get_flags(expr const & e) { return cnstr_scalar(e.raw(), flags_offset(e.kind())); } +bool has_expr_mvar(expr const & e) { return (get_flags(e) & 1) != 0; } +bool has_univ_mvar(expr const & e) { return (get_flags(e) & 2) != 0; } +bool has_fvar(expr const & e) { return (get_flags(e) & 4) != 0; } +bool has_univ_param(expr const & e) { return (get_flags(e) & 8) != 0; } + +template unsigned get_weight_core(expr const & e) { return cnstr_scalar(e.raw(), weight_offset(k)); } + +unsigned get_weight(expr const & e) { + switch (e.kind()) { + case expr_kind::BVar: case expr_kind::Const: case expr_kind::Sort: + case expr_kind::MVar: case expr_kind::FVar: case expr_kind::Lit: + case expr_kind::Quote: + return 1; + case expr_kind::Lambda: return get_weight_core(e); + case expr_kind::Pi: return get_weight_core(e); + case expr_kind::App: return get_weight_core(e); + case expr_kind::Let: return get_weight_core(e); + case expr_kind::MData: return get_weight_core(e); + case expr_kind::Proj: return get_weight_core(e); + } + lean_unreachable(); // LCOV_EXCL_LINE +} + +template unsigned get_depth_core(expr const & e) { return cnstr_scalar(e.raw(), depth_offset(k)); } + +unsigned get_depth(expr const & e) { + switch (e.kind()) { + case expr_kind::BVar: case expr_kind::Const: case expr_kind::Sort: + case expr_kind::MVar: case expr_kind::FVar: case expr_kind::Lit: + case expr_kind::Quote: + return 1; + case expr_kind::Lambda: return get_depth_core(e); + case expr_kind::Pi: return get_depth_core(e); + case expr_kind::App: return get_depth_core(e); + case expr_kind::Let: return get_depth_core(e); + case expr_kind::MData: return get_depth_core(e); + case expr_kind::Proj: return get_depth_core(e); + } + lean_unreachable(); // LCOV_EXCL_LINE +} + +template unsigned get_loose_bvar_range_core(expr const & e) { return cnstr_scalar(e.raw(), loose_bvar_range_offset(k)); } + +unsigned get_loose_bvar_range(expr const & e) { + switch (e.kind()) { + case expr_kind::Const: case expr_kind::Sort: + case expr_kind::Quote: case expr_kind::Lit: + return 0; + case expr_kind::BVar: { + nat const & idx = bvar_idx(e); + return idx.is_small() ? safe_inc(idx.get_small_value()) : std::numeric_limits::max(); + } + case expr_kind::MVar: return get_loose_bvar_range_core(e); + case expr_kind::FVar: return get_loose_bvar_range_core(e); + case expr_kind::Lambda: return get_loose_bvar_range_core(e); + case expr_kind::Pi: return get_loose_bvar_range_core(e); + case expr_kind::App: return get_loose_bvar_range_core(e); + case expr_kind::Let: return get_loose_bvar_range_core(e); + case expr_kind::MData: return get_loose_bvar_range_core(e); + case expr_kind::Proj: return get_loose_bvar_range_core(e); + } + lean_unreachable(); // LCOV_EXCL_LINE +} + +bool is_atomic(expr const & e) { + switch (e.kind()) { + case expr_kind::Const: case expr_kind::Sort: + case expr_kind::BVar: case expr_kind::Lit: + case expr_kind::Quote: + return true; + case expr_kind::App: case expr_kind::MVar: + case expr_kind::FVar: case expr_kind::Lambda: + case expr_kind::Pi: case expr_kind::Let: + case expr_kind::MData: case expr_kind::Proj: + return false; + } + lean_unreachable(); // LCOV_EXCL_LINE +} + +bool quote_is_reflected(expr const & e) { + lean_assert(is_quote(e)); + return cnstr_scalar(e.raw(), reflected_offset(expr_kind::Quote)) != 0; +} + +binder_info binding_info(expr const & e) { + lean_assert(is_lambda(e) || is_pi(e)); + // Remark: lambda and Pi have the same memory layout + return static_cast(cnstr_scalar(e.raw(), binder_info_offset(expr_kind::Lambda))); +} + +/* Legacy */ +binder_info local_info(expr const & e) { + lean_assert(is_local(e)); + return static_cast(cnstr_scalar(e.raw(), binder_info_offset(expr_kind::FVar))); } static expr * g_nat_type = nullptr; static expr * g_string_type = nullptr; -static expr * g_dummy = nullptr; -expr::expr():expr(*g_dummy) {} - -unsigned hash_levels(levels const & ls) { - unsigned r = 23; - for (auto const & l : ls) - r = hash(hash(l), r); - return r; -} - -#ifdef LEAN_TRACK_LIVE_EXPRS -static atomic g_num_live_exprs(0); -unsigned get_num_live_exprs() { - return g_num_live_exprs; -} -#endif - -expr_cell::expr_cell(expr_kind k, unsigned h, bool has_expr_mv, bool has_univ_mv, - bool has_fvar, bool has_param_univ): - m_flags(0), - m_kind(static_cast(k)), - m_has_expr_mv(has_expr_mv), - m_has_univ_mv(has_univ_mv), - m_has_fvar(has_fvar), - m_has_param_univ(has_param_univ), - m_hash(h), - m_rc(0) { - #ifdef LEAN_TRACK_LIVE_EXPRS - atomic_fetch_add_explicit(&g_num_live_exprs, 1u, memory_order_release); - #endif -} - -expr_cell::expr_cell(expr_cell const & src): - m_kind(src.m_kind), - m_has_expr_mv(src.m_has_expr_mv), - m_has_univ_mv(src.m_has_univ_mv), - m_has_fvar(src.m_has_fvar), - m_has_param_univ(src.m_has_param_univ), - m_hash(src.m_hash), - m_rc(0) { - unsigned flgs = src.m_flags; - m_flags = flgs; - #ifdef LEAN_TRACK_LIVE_EXPRS - atomic_fetch_add_explicit(&g_num_live_exprs, 1u, memory_order_release); - #endif -} - -void expr_cell::dec_ref(expr & e, buffer & todelete) { - if (e.m_ptr) { - expr_cell * c = e.steal_ptr(); - lean_assert(!(e.m_ptr)); - if (c->dec_ref_core()) - todelete.push_back(c); - } -} - -optional expr_cell::is_arrow() const { - // it is stored in bits 0-1 - unsigned r = (m_flags & (1+2)); - if (r == 0) { - return optional(); - } else if (r == 1) { - return optional(true); - } else { - lean_assert(r == 2); - return optional(false); - } -} - -void expr_cell::set_is_arrow(bool flag) { - unsigned mask = flag ? 1 : 2; - m_flags |= mask; - lean_assert(is_arrow() && *is_arrow() == flag); -} - -bool is_metavar_app(expr const & e) { - return is_metavar(get_app_fn(e)); -} - -// Expr variables -expr_bvar::expr_bvar(unsigned idx): - expr_cell(expr_kind::BVar, idx, false, false, false, false), - m_vidx(idx) { - if (idx == std::numeric_limits::max()) - throw exception("invalid bound variable index, de Bruijn index is too big"); -} -void expr_bvar::dealloc() { - delete this; -} - -// Expr constants -expr_const::expr_const(name const & n, levels const & ls): - expr_cell(expr_kind::Constant, ::lean::hash(n.hash(), hash_levels(ls)), false, - has_meta(ls), false, has_param(ls)), - m_name(n), - m_levels(ls) { -} -void expr_const::dealloc() { - delete this; -} - -// Expr metavariables and local variables -expr_mlocal::expr_mlocal(bool is_meta, name const & n, name const & pp_n, expr const & t): - expr_composite(is_meta ? expr_kind::MVar : expr_kind::FVar, n.hash(), is_meta || t.has_expr_metavar(), t.has_univ_metavar(), - !is_meta || t.has_fvar(), t.has_param_univ(), - 1, get_loose_bvar_range(t)), - m_name(n), - m_pp_name(pp_n), - m_type(t) {} - -void expr_mlocal::dealloc(buffer & todelete) { - dec_ref(m_type, todelete); - delete this; -} - -expr_mlocal::expr_mlocal(expr_mlocal const & src, expr const & new_type): - expr_composite(src), m_name(src.m_name), m_pp_name(src.m_pp_name), m_type(new_type) {} - -expr_fvar::expr_fvar(name const & n, name const & pp_n, expr const & t, binder_info bi): - expr_mlocal(false, n, pp_n, t), m_bi(bi) {} - -expr_fvar::expr_fvar(expr_fvar const & src, expr const & new_type): - expr_mlocal(src, new_type), m_bi(src.m_bi) {} - -void expr_fvar::dealloc(buffer & todelete) { - dec_ref(m_type, todelete); - delete this; -} - -expr_composite::expr_composite(expr_composite const & src): - expr_cell(src), - m_weight(src.m_weight), - m_depth(src.m_depth), - m_loose_bvar_range(src.m_loose_bvar_range) { -} - -// Composite expressions -expr_composite::expr_composite(expr_kind k, unsigned h, bool has_expr_mv, bool has_univ_mv, - bool has_fvar, bool has_param_univ, unsigned w, unsigned bv_range): - expr_cell(k, h, has_expr_mv, has_univ_mv, has_fvar, has_param_univ), - m_weight(w), - m_depth(0), - m_loose_bvar_range(bv_range) {} - -// Expr applications -expr_app::expr_app(expr const & fn, expr const & arg): - expr_composite(expr_kind::App, ::lean::hash(fn.hash(), arg.hash()), - fn.has_expr_metavar() || arg.has_expr_metavar(), - fn.has_univ_metavar() || arg.has_univ_metavar(), - fn.has_fvar() || arg.has_fvar(), - fn.has_param_univ() || arg.has_param_univ(), - inc_weight(add_weight(get_weight(fn), get_weight(arg))), - std::max(get_loose_bvar_range(fn), get_loose_bvar_range(arg))), - m_fn(fn), m_arg(arg) { - m_depth = std::max(get_depth(fn), get_depth(arg)) + 1; - m_hash = ::lean::hash(m_hash, m_weight); - m_hash = ::lean::hash(m_hash, m_depth); -} - -expr_app::expr_app(expr_app const & src, expr const & new_fn, expr const & new_arg): - expr_composite(src), m_fn(new_fn), m_arg(new_arg) {} - -void expr_app::dealloc(buffer & todelete) { - dec_ref(m_fn, todelete); - dec_ref(m_arg, todelete); - delete this; -} - -static unsigned dec(unsigned k) { return k == 0 ? 0 : k - 1; } - -// Expr binders (Lambda, Pi) -expr_binding::expr_binding(expr_kind k, name const & n, expr const & t, expr const & b, binder_info i): - expr_composite(k, ::lean::hash(t.hash(), b.hash()), - t.has_expr_metavar() || b.has_expr_metavar(), - t.has_univ_metavar() || b.has_univ_metavar(), - t.has_fvar() || b.has_fvar(), - t.has_param_univ() || b.has_param_univ(), - inc_weight(add_weight(get_weight(t), get_weight(b))), - std::max(get_loose_bvar_range(t), dec(get_loose_bvar_range(b)))), - m_binder(n, t, i), - m_body(b) { - m_depth = std::max(get_depth(t), get_depth(b)) + 1; - m_hash = ::lean::hash(m_hash, m_weight); - m_hash = ::lean::hash(m_hash, m_depth); - lean_assert(k == expr_kind::Lambda || k == expr_kind::Pi); -} - -expr_binding::expr_binding(expr_binding const & src, expr const & d, expr const & b): - expr_composite(src), m_binder(src.m_binder, d), m_body(b) {} - -void expr_binding::dealloc(buffer & todelete) { - dec_ref(m_body, todelete); - dec_ref(m_binder.m_type, todelete); - delete this; -} - -// Expr Sort -expr_sort::expr_sort(level const & l): - expr_cell(expr_kind::Sort, ::lean::hash(l), false, has_meta(l), false, has_param(l)), - m_level(l) { -} -expr_sort::~expr_sort() {} -void expr_sort::dealloc() { - delete this; -} - -// Expr literals - -expr_lit::expr_lit(literal const & lit): - expr_cell(expr_kind::Lit, false, false, false, false, false), - m_lit(lit) { -} -expr_lit::~expr_lit() {} -void expr_lit::dealloc() { - delete this; -} - -expr lit_type(expr_ptr e) { +expr const & lit_type(expr const & e) { switch (lit_value(e).kind()) { case literal_kind::String: return *g_string_type; case literal_kind::Nat: return *g_nat_type; @@ -340,153 +308,171 @@ expr lit_type(expr_ptr e) { lean_unreachable(); } -// Expr metadata -expr_mdata::expr_mdata(kvmap const & data, expr const & e): - expr_composite(expr_kind::MData, e.hash(), - e.has_expr_metavar(), - e.has_univ_metavar(), - e.has_fvar(), - e.has_param_univ(), - inc_weight(get_weight(e)), - get_loose_bvar_range(e)), - m_data(data), m_expr(e) { - m_depth = get_depth(e) + 1; - m_hash = ::lean::hash(m_hash, m_weight); - m_hash = ::lean::hash(m_hash, m_depth); -} - -void expr_mdata::dealloc(buffer & todelete) { - dec_ref(m_expr, todelete); - delete this; -} - -// Expr projections -expr_proj::expr_proj(nat const & idx, expr const & e): - expr_composite(expr_kind::Proj, e.hash(), - e.has_expr_metavar(), - e.has_univ_metavar(), - e.has_fvar(), - e.has_param_univ(), - inc_weight(get_weight(e)), - get_loose_bvar_range(e)), - m_idx(idx), m_expr(e) { - m_depth = get_depth(e) + 1; - m_hash = ::lean::hash(m_hash, m_weight); - m_hash = ::lean::hash(m_hash, m_depth); -} - -void expr_proj::dealloc(buffer & todelete) { - dec_ref(m_expr, todelete); - delete this; -} - -// Let expressions -expr_let::expr_let(name const & n, expr const & t, expr const & v, expr const & b): - expr_composite(expr_kind::Let, - ::lean::hash(::lean::hash(t.hash(), v.hash()), b.hash()), - t.has_expr_metavar() || v.has_expr_metavar() || b.has_expr_metavar(), - t.has_univ_metavar() || v.has_univ_metavar() || b.has_univ_metavar(), - t.has_fvar() || v.has_fvar() || b.has_fvar(), - t.has_param_univ() || v.has_param_univ() || b.has_param_univ(), - inc_weight(add_weight(add_weight(get_weight(t), get_weight(v)), get_weight(b))), - std::max(std::max(get_loose_bvar_range(t), get_loose_bvar_range(v)), dec(get_loose_bvar_range(b)))), - m_name(n), m_type(t), m_value(v), m_body(b) { - m_depth = std::max(get_depth(t), std::max(get_depth(v), get_depth(b))) + 1; - m_hash = ::lean::hash(m_hash, m_weight); - m_hash = ::lean::hash(m_hash, m_depth); -} - -expr_let::expr_let(expr_let const & src, expr const & t, expr const & v, expr const & b): - expr_composite(src), m_name(src.m_name), m_type(t), m_value(v), m_body(b) {} - -void expr_let::dealloc(buffer & todelete) { - dec_ref(m_body, todelete); - dec_ref(m_value, todelete); - dec_ref(m_type, todelete); - delete this; -} - // ======================================= // Constructors -expr mk_bvar(unsigned idx) { - return expr(new expr_bvar(idx)); +static expr * g_dummy = nullptr; +expr::expr():expr(*g_dummy) {} + +expr mk_lit(literal const & l) { + inc(l.raw()); + expr r(mk_cnstr(static_cast(expr_kind::Lit), l.raw(), expr_scalar_size(expr_kind::Lit))); + set_scalar(r, hash(l), false, false, false, false); + return r; } + +expr mk_mdata(kvmap const & m, expr const & e) { + inc(m.raw()); inc(e.raw()); + expr r(mk_cnstr(static_cast(expr_kind::MData), m.raw(), e.raw(), rec_expr_scalar_size(expr_kind::MData))); + unsigned w = safe_inc(get_weight(e)); + unsigned d = get_depth(e) + 1; + unsigned h = hash(hash(e), hash(w, d)); + set_scalar(r, h, has_expr_mvar(e), has_univ_mvar(e), has_fvar(e), has_univ_param(e)); + set_rec_scalar(r, w, d, get_loose_bvar_range(e)); + return r; +} + +expr mk_proj(nat const & idx, expr const & e) { + inc(idx.raw()); inc(e.raw()); + expr r(mk_cnstr(static_cast(expr_kind::Proj), idx.raw(), e.raw(), rec_expr_scalar_size(expr_kind::Proj))); + unsigned w = safe_inc(get_weight(e)); + unsigned d = get_depth(e) + 1; + unsigned h = hash(hash(e), hash(idx.hash(), w)); + set_scalar(r, h, has_expr_mvar(e), has_univ_mvar(e), has_fvar(e), has_univ_param(e)); + set_rec_scalar(r, w, d, get_loose_bvar_range(e)); + return r; +} + +expr mk_bvar(nat const & idx) { + inc(idx.raw()); + expr r(mk_cnstr(static_cast(expr_kind::BVar), idx.raw(), expr_scalar_size(expr_kind::BVar))); + set_scalar(r, idx.hash(), false, false, false, false); + return r; +} + +/* Legacy */ +expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info bi) { + inc(n.raw()); inc(pp_n.raw()); inc(t.raw()); + expr r(mk_cnstr(static_cast(expr_kind::FVar), n.raw(), pp_n.raw(), t.raw(), rec_expr_scalar_size(expr_kind::FVar))); + set_binder_info(r, bi); + set_scalar(r, n.hash(), has_expr_mvar(t), has_univ_mvar(t), true, has_univ_param(t)); + set_rec_scalar(r, 1, 1, get_loose_bvar_range(t)); + return r; +} + expr mk_fvar(name const & n) { - return expr(new expr_fvar(n, n, expr(), mk_binder_info())); + return mk_local(n, n, expr(), mk_binder_info()); } -expr mk_constant(name const & n, levels const & ls) { - return expr(new expr_const(n, ls)); + +expr mk_const(name const & n, levels const & ls) { + inc(n.raw()); inc(ls.raw()); + expr r(mk_cnstr(static_cast(expr_kind::Const), n.raw(), ls.raw(), expr_scalar_size(expr_kind::Const))); + set_scalar(r, hash(n.hash(), hash(ls)), false, has_meta(ls), false, has_param(ls)); + return r; } + +expr mk_app(expr const & f, expr const & a) { + inc(f.raw()); inc(a.raw()); + expr r(mk_cnstr(static_cast(expr_kind::App), f.raw(), a.raw(), rec_expr_scalar_size(expr_kind::App))); + unsigned w = safe_inc(safe_add(get_weight(f), get_weight(a))); + unsigned d = std::max(get_depth(f), get_depth(a)) + 1; + unsigned h = hash(hash(hash(f), hash(a)), hash(d, w)); + set_scalar(r, h, + has_expr_mvar(f) || has_expr_mvar(a), + has_univ_mvar(f) || has_univ_mvar(a), + has_fvar(f) || has_fvar(a), + has_univ_param(f) || has_univ_param(a)); + set_rec_scalar(r, w, d, std::max(get_loose_bvar_range(f), get_loose_bvar_range(a))); + return r; +} + +expr mk_sort(level const & l) { + inc(l.raw()); + expr r(mk_cnstr(static_cast(expr_kind::Sort), l.raw(), expr_scalar_size(expr_kind::Sort))); + set_scalar(r, hash(l), false, has_meta(l), false, has_param(l)); + return r; +} + +template +expr mk_binding(name const & n, expr const & t, expr const & e, binder_info bi) { + lean_assert(k == expr_kind::Pi || k == expr_kind::Lambda); + inc(n.raw()); inc(t.raw()); inc(e.raw()); + expr r(mk_cnstr(static_cast(k), n.raw(), t.raw(), e.raw(), rec_expr_scalar_size(k))); + unsigned w = safe_inc(safe_add(get_weight(t), get_weight(e))); + unsigned d = std::max(get_depth(t), get_depth(e)) + 1; + unsigned h = hash(hash(d, w), hash(hash(t), hash(e))); + unsigned lbvr = std::max(get_loose_bvar_range(t), safe_dec(get_loose_bvar_range(e))); + set_binder_info(r, bi); + set_scalar(r, h, + has_expr_mvar(t) || has_expr_mvar(e), + has_univ_mvar(t) || has_univ_mvar(e), + has_fvar(t) || has_fvar(e), + has_univ_param(t) || has_univ_param(e)); + set_rec_scalar(r, w, d, lbvr); + return r; +} + +expr mk_lambda(name const & n, expr const & t, expr const & e, binder_info bi) { + return mk_binding(n, t, e, bi); +} + +expr mk_pi(name const & n, expr const & t, expr const & e, binder_info bi) { + return mk_binding(n, t, e, bi); +} + +static name * g_default_name = nullptr; + +expr mk_arrow(expr const & t, expr const & e) { + return mk_pi(*g_default_name, t, e, mk_binder_info()); +} + +expr mk_let(name const & n, expr const & t, expr const & v, expr const & b) { + inc(n.raw()); inc(t.raw()); inc(v.raw()); inc(b.raw()); + expr r(mk_cnstr(static_cast(expr_kind::Let), n.raw(), t.raw(), v.raw(), b.raw(), rec_expr_scalar_size(expr_kind::Let))); + unsigned w = safe_inc(safe_add(safe_add(get_weight(t), get_weight(v)), get_weight(b))); + unsigned d = std::max(get_depth(t), std::max(get_depth(v), get_depth(b))) + 1; + unsigned h = hash(hash(w, d), hash(hash(hash(t), hash(v)), hash(b))); + unsigned lbvr = std::max(get_loose_bvar_range(t), std::max(get_loose_bvar_range(v), safe_dec(get_loose_bvar_range(b)))); + set_scalar(r, h, + has_expr_mvar(t) || has_expr_mvar(v) || has_expr_mvar(b), + has_univ_mvar(t) || has_univ_mvar(v) || has_univ_mvar(b), + has_fvar(t) || has_fvar(v) || has_fvar(b), + has_univ_param(t) || has_univ_param(v) || has_univ_param(b)); + set_rec_scalar(r, w, d, lbvr); + return r; +} + +/* Legacy */ +expr mk_quote(bool reflected, expr const & val) { + inc(val.raw()); + expr r(mk_cnstr(static_cast(expr_kind::Quote), val.raw(), expr_scalar_size(expr_kind::Quote))); + set_scalar(r, hash(hash(val), reflected ? 17u : 11u), false, false, false, false); + set_reflected(r, reflected); + return r; +} + +/* Legacy */ expr mk_metavar(name const & n, name const & pp_n, expr const & t) { - return expr(new expr_mlocal(true, n, pp_n, t)); + inc(n.raw()); inc(pp_n.raw()); inc(t.raw()); + expr r(mk_cnstr(static_cast(expr_kind::MVar), n.raw(), pp_n.raw(), t.raw(), rec_expr_scalar_size(expr_kind::MVar))); + set_scalar(r, n.hash(), true, has_univ_mvar(t), has_fvar(t), has_univ_param(t)); + set_rec_scalar(r, 1, 1, get_loose_bvar_range(t)); + return r; } -expr mk_metavar(name const & n, expr const & t) { + +expr mk_mvar(name const & n, expr const & t) { return mk_metavar(n, n, t); } -expr mk_mdata(kvmap const & d, expr const & e) { - return expr(new expr_mdata(d, e)); -} -expr mk_proj(nat const & idx, expr const & e) { - return expr(new expr_proj(idx, e)); -} -expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info bi) { - return expr(new expr_fvar(n, pp_n, t, bi)); -} -expr mk_app(expr const & f, expr const & a) { - return expr(new expr_app(f, a)); -} -expr mk_binding(expr_kind k, name const & n, expr const & t, expr const & e, binder_info i) { - return expr(new expr_binding(k, n, t, e, i)); -} -expr mk_let(name const & n, expr const & t, expr const & v, expr const & b) { - return expr(new expr_let(n, t, v, b)); -} -expr mk_sort(level const & l) { - return expr(new expr_sort(l)); -} -expr mk_lit(literal const & l) { - return expr(new expr_lit(l)); -} + +static expr * g_Prop = nullptr; +static expr * g_Type0 = nullptr; + +expr mk_Prop() { return *g_Prop; } +expr mk_Type() { return *g_Type0; } // ======================================= +// Auxiliary constructors and accessors -typedef buffer del_buffer; -void expr_cell::dealloc() { - try { - del_buffer todo; - todo.push_back(this); - while (!todo.empty()) { - expr_cell * it = todo.back(); - todo.pop_back(); - #ifdef LEAN_TRACK_LIVE_EXPRS - atomic_fetch_sub_explicit(&g_num_live_exprs, 1u, memory_order_release); - #endif - lean_assert(it->get_rc() == 0); - switch (it->kind()) { - case expr_kind::Lit: static_cast(it)->dealloc(); break; - case expr_kind::MData: static_cast(it)->dealloc(todo); break; - case expr_kind::Proj: static_cast(it)->dealloc(todo); break; - case expr_kind::BVar: static_cast(it)->dealloc(); break; - case expr_kind::MVar: static_cast(it)->dealloc(todo); break; - case expr_kind::FVar: static_cast(it)->dealloc(todo); break; - case expr_kind::Constant: static_cast(it)->dealloc(); break; - case expr_kind::Sort: static_cast(it)->dealloc(); break; - case expr_kind::App: static_cast(it)->dealloc(todo); break; - case expr_kind::Lambda: - case expr_kind::Pi: static_cast(it)->dealloc(todo); break; - case expr_kind::Let: static_cast(it)->dealloc(todo); break; - - case expr_kind::Quote: static_cast(it)->dealloc(todo); break; - } - } - } catch (std::bad_alloc&) { - // We need this catch, because push_back may fail when expanding the buffer. - // In this case, we avoid the crash, and "accept" the memory leak. - } -} - -// Auxiliary constructors expr mk_app(expr const & f, unsigned num_args, expr const * args) { expr r = f; for (unsigned i = 0; i < num_args; i++) @@ -573,54 +559,37 @@ unsigned get_app_num_args(expr const & e) { return n; } -static name * g_default_name = nullptr; -static name const & get_default_var_name() { - return *g_default_name; -} - -bool is_default_var_name(name const & n) { return n == get_default_var_name(); } -expr mk_arrow(expr const & t, expr const & e) { - return mk_pi(get_default_var_name(), t, e, mk_binder_info()); -} - -static expr * g_Prop = nullptr; -static expr * g_Type1 = nullptr; -expr mk_Prop() { return *g_Prop; } -expr mk_Type() { return *g_Type1; } - -unsigned get_weight(expr const & e) { - switch (e.kind()) { - case expr_kind::BVar: case expr_kind::Constant: case expr_kind::Sort: - case expr_kind::MVar: case expr_kind::FVar: case expr_kind::Lit: - return 1; - case expr_kind::Lambda: case expr_kind::Pi: - case expr_kind::App: case expr_kind::Let: - case expr_kind::MData: case expr_kind::Proj: - return static_cast(e.raw())->m_weight; - - case expr_kind::Quote: - return 1; +bool is_arrow(expr const & t) { + if (!is_pi(t)) return false; + if (has_loose_bvars(t)) { + return !has_loose_bvar(binding_body(t), 0); + } else { + lean_assert(has_loose_bvars(binding_body(t)) == has_loose_bvar(binding_body(t), 0)); + return !has_loose_bvars(binding_body(t)); } - lean_unreachable(); // LCOV_EXCL_LINE } -unsigned get_depth(expr const & e) { - switch (e.kind()) { - case expr_kind::BVar: case expr_kind::Constant: case expr_kind::Sort: - case expr_kind::MVar: case expr_kind::FVar: case expr_kind::Lit: - return 1; - case expr_kind::Lambda: case expr_kind::Pi: - case expr_kind::App: case expr_kind::Let: - case expr_kind::MData: case expr_kind::Proj: - return static_cast(e.raw())->m_depth; - - - case expr_kind::Quote: - return 1; - } - lean_unreachable(); // LCOV_EXCL_LINE +bool is_default_var_name(name const & n) { + return n == *g_default_name; } +/* Legacy */ +optional has_expr_metavar_strict(expr const & e) { + if (!has_expr_metavar(e)) + return none_expr(); + optional r; + for_each(e, [&](expr const & e, unsigned) { + if (r || !has_expr_metavar(e)) return false; + if (is_metavar_app(e)) { r = e; return false; } + if (is_local(e)) return false; // do not visit type + return true; + }); + return r; +} + +// ======================================= +// Update + expr update_mdata(expr const & e, expr const & t) { if (!is_eqp(mdata_expr(e), t)) return mk_mdata(mdata_data(e), t); @@ -656,26 +625,6 @@ expr update_binding(expr const & e, expr const & new_domain, expr const & new_bo return e; } -expr update_mlocal(expr const & e, expr const & new_type) { - if (is_eqp(mlocal_type(e), new_type)) - return e; - else if (is_metavar(e)) - return mk_metavar(mlocal_name(e), mlocal_pp_name(e), new_type); - else - return mk_local(mlocal_name(e), mlocal_pp_name(e), new_type, local_info(e)); -} - -expr update_local(expr const & e, expr const & new_type, binder_info bi) { - if (is_eqp(mlocal_type(e), new_type) && local_info(e) == bi) - return e; - else - return mk_local(mlocal_name(e), mlocal_pp_name(e), new_type, bi); -} - -expr update_local(expr const & e, binder_info bi) { - return update_local(e, mlocal_type(e), bi); -} - expr update_sort(expr const & e, level const & new_level) { if (!is_eqp(sort_level(e), new_level)) return mk_sort(new_level); @@ -683,13 +632,20 @@ expr update_sort(expr const & e, level const & new_level) { return e; } -expr update_constant(expr const & e, levels const & new_levels) { +expr update_const(expr const & e, levels const & new_levels) { if (!is_eqp(const_levels(e), new_levels)) - return mk_constant(const_name(e), new_levels); + return mk_const(const_name(e), new_levels); else return e; } +expr update_mvar(expr const & e, expr const & new_type) { + if (is_eqp(mvar_type(e), new_type)) + return e; + else + return mk_mvar(mvar_name(e), new_type); +} + expr update_let(expr const & e, expr const & new_type, expr const & new_value, expr const & new_body) { if (!is_eqp(let_type(e), new_type) || !is_eqp(let_value(e), new_value) || !is_eqp(let_body(e), new_body)) return mk_let(let_name(e), new_type, new_value, new_body); @@ -697,48 +653,32 @@ expr update_let(expr const & e, expr const & new_type, expr const & new_value, e return e; } -bool is_atomic(expr const & e) { - switch (e.kind()) { - case expr_kind::Constant: case expr_kind::Sort: - case expr_kind::BVar: case expr_kind::Lit: - return true; - case expr_kind::App: case expr_kind::MVar: - case expr_kind::FVar: case expr_kind::Lambda: - case expr_kind::Pi: case expr_kind::Let: - case expr_kind::MData: case expr_kind::Proj: - return false; - - - case expr_kind::Quote: - return true; - } - lean_unreachable(); // LCOV_EXCL_LINE +/* Legacy */ +expr update_local(expr const & e, expr const & new_type, binder_info bi) { + if (is_eqp(mlocal_type(e), new_type) && local_info(e) == bi) + return e; + else + return mk_local(mlocal_name(e), mlocal_pp_name(e), new_type, bi); } -bool is_arrow(expr const & t) { - optional r = t.raw()->is_arrow(); - if (r) { - return *r; - } else { - bool res = is_pi(t) && !has_loose_bvar(binding_body(t), 0); - t.raw()->set_is_arrow(res); - return res; - } +/* Legacy */ +expr update_local(expr const & e, binder_info bi) { + return update_local(e, mlocal_type(e), bi); } -optional has_expr_metavar_strict(expr const & e) { - if (!has_expr_metavar(e)) - return none_expr(); - optional r; - for_each(e, [&](expr const & e, unsigned) { - if (r || !has_expr_metavar(e)) return false; - if (is_metavar_app(e)) { r = e; return false; } - if (is_local(e)) return false; // do not visit type - return true; - }); - return r; +/* Legacy */ +expr update_mlocal(expr const & e, expr const & new_type) { + if (is_eqp(mlocal_type(e), new_type)) + return e; + else if (is_metavar(e)) + return mk_metavar(mlocal_name(e), mlocal_pp_name(e), new_type); + else + return mk_local(mlocal_name(e), mlocal_pp_name(e), new_type, local_info(e)); } +// ======================================= +// Loose bound variable management + static bool has_loose_bvars_in_domain(expr const & b, unsigned vidx, bool strict) { if (is_pi(b)) { return @@ -762,7 +702,7 @@ bool has_loose_bvar(expr const & e, unsigned i) { if (n_i >= get_loose_bvar_range(e)) return false; // expression e does not contain bound variables with idx >= n_i if (is_var(e)) { - unsigned vidx = bvar_idx(e); + nat const & vidx = bvar_idx(e); if (vidx == n_i) found = true; } @@ -781,14 +721,15 @@ expr lower_loose_bvars(expr const & e, unsigned s, unsigned d) { return some_expr(e); // overflow, vidx can't be >= max unsigned if (s1 >= get_loose_bvar_range(e)) return some_expr(e); // expression e does not contain bound variables with idx >= s1 - if (is_var(e) && bvar_idx(e) >= s1) { + if (is_bvar(e) && bvar_idx(e) >= s1) { lean_assert(bvar_idx(e) >= offset + d); - return some_expr(mk_bvar(bvar_idx(e) - d)); + return some_expr(mk_bvar(bvar_idx(e) - nat(d))); } else { return none_expr(); } }); } + expr lower_loose_bvars(expr const & e, unsigned d) { return lower_loose_bvars(e, d, d); } @@ -803,10 +744,7 @@ expr lift_loose_bvars(expr const & e, unsigned s, unsigned d) { if (s1 >= get_loose_bvar_range(e)) return some_expr(e); // expression e does not contain bound variables with idx >= s1 if (is_var(e) && bvar_idx(e) >= s + offset) { - unsigned new_idx = bvar_idx(e) + d; - if (new_idx < bvar_idx(e)) - throw exception("invalid lift_loose_bvars operation, index overflow"); - return some_expr(mk_bvar(new_idx)); + return some_expr(mk_bvar(bvar_idx(e) + nat(d))); } else { return none_expr(); } @@ -817,6 +755,9 @@ expr lift_loose_bvars(expr const & e, unsigned d) { return lift_loose_bvars(e, 0, d); } +// ======================================= +// Implicit argument inference + expr infer_implicit(expr const & t, unsigned num_params, bool strict) { if (num_params == 0) { return t; @@ -839,31 +780,13 @@ expr infer_implicit(expr const & t, bool strict) { return infer_implicit(t, std::numeric_limits::max(), strict); } -std::ostream & operator<<(std::ostream & out, expr_kind const & k) { - switch (k) { - case expr_kind::MData: out << "MData"; break; - case expr_kind::Proj: out << "Proj"; break; - case expr_kind::Lit: out << "Lit"; break; - case expr_kind::BVar: out << "BVar"; break; - case expr_kind::FVar: out << "FVar"; break; - case expr_kind::MVar: out << "MVar"; break; - case expr_kind::Sort: out << "Sort"; break; - case expr_kind::Constant: out << "Constant"; break; - case expr_kind::App: out << "App"; break; - case expr_kind::Lambda: out << "Lambda"; break; - case expr_kind::Pi: out << "Pi"; break; - case expr_kind::Let: out << "Let"; break; - - - case expr_kind::Quote: out << "Quote"; break; - } - return out; -} +// ======================================= +// Initialization & Finalization void initialize_expr() { g_dummy = new expr(mk_constant("__expr_for_default_constructor__")); g_default_name = new name("a"); - g_Type1 = new expr(mk_sort(mk_level_one())); + g_Type0 = new expr(mk_sort(mk_level_one())); g_Prop = new expr(mk_sort(mk_level_zero())); /* TODO(Leo): add support for builtin constants in the kernel. Something similar to what we have in the library directory. */ @@ -873,27 +796,27 @@ void initialize_expr() { void finalize_expr() { delete g_Prop; - delete g_Type1; + delete g_Type0; delete g_dummy; delete g_default_name; delete g_nat_type; delete g_string_type; } -/* ================ LEGACY CODE ================ */ +#if 0 +// Expr metavariables and local variables +expr_mlocal::expr_mlocal(bool is_meta, name const & n, name const & pp_n, expr const & t): + expr_composite(is_meta ? expr_kind::MVar : expr_kind::FVar, n.hash(), is_meta || t.has_expr_metavar(), t.has_univ_metavar(), + !is_meta || t.has_fvar(), t.has_param_univ(), + 1, get_loose_bvar_range(t)), + m_name(n), + m_pp_name(pp_n), + m_type(t) {} -expr_quote::expr_quote(bool r, expr const & v): - expr_cell(expr_kind::Quote, v.hash(), false, false, false, false), - m_reflected(r), - m_value(v) { -} - -void expr_quote::dealloc(buffer & todelete) { - dec_ref(m_value, todelete); +void expr_mlocal::dealloc(buffer & todelete) { + dec_ref(m_type, todelete); delete this; } -expr mk_quote(bool reflected, expr const & val) { - return expr(new expr_quote(reflected, val)); -} +#endif } diff --git a/src/kernel/expr.h b/src/kernel/expr.h index b1c046a951..f68b3f9de4 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -69,7 +69,6 @@ inline serializer & operator<<(serializer & s, literal const & l) { l.serialize( inline literal read_literal(deserializer & d) { return literal::deserialize(d); } inline deserializer & operator>>(deserializer & d, literal & l) { l = read_literal(d); return d; } - /* ======================================= Expressions @@ -90,99 +89,44 @@ inductive expr | quote : bool → expr → expr */ -class expr; -enum class expr_kind { BVar, FVar, Sort, Constant, MVar, App, Lambda, Pi, Let, Lit, MData, Proj, Quote }; -class expr_cell { -protected: - // The bits of the following field mean: - // 0-1 - term is an arrow (0 - not initialized, 1 - is arrow, 2 - is not arrow) - // Remark: we use atomic_uchar because these flags are computed lazily (i.e., after the expression is created) - atomic_uchar m_flags; - unsigned m_kind:8; - unsigned m_has_expr_mv:1; // term contains expression metavariables - unsigned m_has_univ_mv:1; // term contains universe metavariables - unsigned m_has_fvar:1; // term contains free variables - unsigned m_has_param_univ:1; // term constains parametric universe levels - unsigned m_hash; // hash based on the structure of the expression (this is a good hash for structural equality) - MK_LEAN_RC(); // Declare m_rc counter - void dealloc(); +enum class expr_kind { BVar, FVar, Sort, Const, MVar, App, Lambda, Pi, Let, Lit, MData, Proj, Quote }; +class expr : public object_ref { + explicit expr(object * o):object_ref(o) { inc(o); } + explicit expr(object_ref && o):object_ref(o) {} - optional is_arrow() const; - void set_is_arrow(bool flag); - friend bool is_arrow(expr const & e); - - static void dec_ref(expr & c, buffer & todelete); - expr_cell(expr_cell const & src); // for hash_consing -public: - expr_cell(expr_kind k, unsigned h, bool has_expr_mv, bool has_univ_mv, bool has_fvar, bool has_param_univ); - expr_kind kind() const { return static_cast(m_kind); } - unsigned hash() const { return m_hash; } - bool has_expr_metavar() const { return m_has_expr_mv; } - bool has_univ_metavar() const { return m_has_univ_mv; } - bool has_fvar() const { return m_has_fvar; } - bool has_param_univ() const { return m_has_param_univ; } -}; - -typedef expr_cell * expr_ptr; - -/** - \brief Exprs for encoding formulas/expressions, types and proofs. -*/ -class expr { -private: - expr_cell * m_ptr; - explicit expr(expr_cell * ptr):m_ptr(ptr) { if (m_ptr) m_ptr->inc_ref(); } - friend class expr_cell; - expr_cell * steal_ptr() { expr_cell * r = m_ptr; m_ptr = nullptr; return r; } - friend class optional; -public: - /** - \brief The default constructor creates a reference to a "dummy" - expression. The actual "dummy" expression is not relevant, and - no procedure should rely on the kind of expression used. - - We have a default constructor because some collections only work - with types that have a default constructor. - */ - expr(); - expr(expr const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); } - expr(expr && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; } - ~expr() { if (m_ptr) m_ptr->dec_ref(); } - - friend void swap(expr & a, expr & b) { std::swap(a.m_ptr, b.m_ptr); } - - expr & operator=(expr const & s) { LEAN_COPY_REF(s); } - expr & operator=(expr && s) { LEAN_MOVE_REF(s); } - - expr_kind kind() const { return m_ptr->kind(); } - unsigned hash() const { return m_ptr ? m_ptr->hash() : 23; } - bool has_expr_metavar() const { return m_ptr->has_expr_metavar(); } - bool has_univ_metavar() const { return m_ptr->has_univ_metavar(); } - bool has_metavar() const { return has_expr_metavar() || has_univ_metavar(); } - bool has_fvar() const { return m_ptr->has_fvar(); } - bool has_param_univ() const { return m_ptr->has_param_univ(); } - - operator expr_ptr() const { return m_ptr; } - expr_cell * raw() const { return m_ptr; } - - friend expr mk_bvar(unsigned idx); - friend expr mk_fvar(name const & n); - friend expr mk_sort(level const & l); - friend expr mk_constant(name const & n, levels const & ls); - friend expr mk_metavar(name const & n, name const & pp_n, expr const & t); - friend expr mk_app(expr const & f, expr const & a); - friend expr mk_binding(expr_kind k, name const & n, expr const & t, expr const & e, binder_info i); - friend expr mk_let(name const & n, expr const & t, expr const & v, expr const & b); friend expr mk_lit(literal const & lit); - friend expr mk_mdata(kvmap const & m, expr const & e); + friend expr mk_mdata(kvmap const & d, expr const & e); friend expr mk_proj(nat const & idx, expr const & e); - friend bool is_eqp(expr const & a, expr const & b) { return a.m_ptr == b.m_ptr; } - // TODO(Leo): delete + friend expr mk_bvar(nat const & idx); + friend expr mk_const(name const & n, levels const & ls); + friend expr mk_app(expr const & f, expr const & a); + friend expr mk_sort(level const & l); + template friend expr mk_binding(name const & n, expr const & t, expr const & e, binder_info bi); + friend expr mk_let(name const & n, expr const & t, expr const & v, expr const & b); + friend expr mk_metavar(name const & n, name const & pp_n, expr const & t); friend expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info bi); friend expr mk_quote(bool reflected, expr const & val); +public: + expr(); + expr(expr const & other):object_ref(other) {} + expr(expr && other):object_ref(other) {} + expr_kind kind() const { return static_cast(cnstr_tag(raw())); } + + expr & operator=(expr const & other) { object_ref::operator=(other); return *this; } + expr & operator=(expr && other) { object_ref::operator=(other); return *this; } + + friend bool is_eqp(expr const & e1, expr const & e2) { return e1.raw() == e2.raw(); } + void serialize(serializer & s) const { s.write_object(raw()); } + static expr deserialize(deserializer & d) { return expr(d.read_object()); } }; -SPECIALIZE_OPTIONAL_FOR_SMART_PTR(expr) +typedef list_ref exprs; + +inline serializer & operator<<(serializer & s, expr const & e) { e.serialize(s); return s; } +inline serializer & operator<<(serializer & s, exprs const & es) { es.serialize(s); return s; } +inline expr read_expr(deserializer & d) { return expr::deserialize(d); } +inline exprs read_exprs(deserializer & d) { return read_list_ref(d); } +inline deserializer & operator>>(deserializer & d, expr & e) { e = read_expr(d); return d; } inline optional none_expr() { return optional(); } inline optional some_expr(expr const & e) { return optional(e); } @@ -192,200 +136,37 @@ inline bool is_eqp(optional const & a, optional const & b) { return static_cast(a) == static_cast(b) && (!a || is_eqp(*a, *b)); } -/** \brief Bounded variables. They are encoded using de Bruijn's indices. */ -class expr_bvar : public expr_cell { - unsigned m_vidx; // de Bruijn index - friend expr_cell; - void dealloc(); -public: - expr_bvar(unsigned idx); - unsigned get_vidx() const { return m_vidx; } -}; +unsigned hash(expr const & e); +bool has_expr_mvar(expr const & e); +bool has_univ_mvar(expr const & e); +inline bool has_mvar(expr const & e) { return has_expr_mvar(e) || has_univ_mvar(e); } +bool has_fvar(expr const & e); +bool has_univ_param(expr const & e); +unsigned get_weight(expr const & e); +unsigned get_depth(expr const & e); +unsigned get_loose_bvar_range(expr const & e); -/** \brief (parametric) Constants. */ -class expr_const : public expr_cell { - name m_name; - levels m_levels; - friend expr_cell; - void dealloc(); - expr_const(expr_const const &, levels const & new_levels); // for hash_consing -public: - expr_const(name const & n, levels const & ls); - name const & get_name() const { return m_name; } - levels const & get_levels() const { return m_levels; } -}; - -/** \brief Composite expressions */ -class expr_composite : public expr_cell { -protected: - unsigned m_weight; - unsigned m_depth; - unsigned m_loose_bvar_range; /* dangling bound variables */ - friend unsigned get_weight(expr const & e); - friend unsigned get_depth(expr const & e); - friend unsigned get_loose_bvar_range(expr const & e); - expr_composite(expr_composite const & src); // for hash_consing -public: - expr_composite(expr_kind k, unsigned h, bool has_expr_mv, bool has_univ_mv, bool has_fvar, - bool has_param_univ, unsigned w, unsigned fv_range); -}; - -/** \brief Metavariables and local constants */ -class expr_mlocal : public expr_composite { -protected: - name m_name; - name m_pp_name; // user facing name - expr m_type; - friend expr_cell; - void dealloc(buffer & todelete); - expr_mlocal(expr_mlocal const &, expr const & new_type); // for hash_consing -public: - expr_mlocal(bool is_meta, name const & n, name const & pp_n, expr const & t); - name const & get_name() const { return m_name; } - name const & get_pp_name() const { return m_pp_name; } - expr const & get_type() const { return m_type; } -}; - -/** \brief expr_mlocal subclass for local constants. */ -class expr_fvar : public expr_mlocal { - binder_info m_bi; - friend expr_cell; - void dealloc(buffer & todelete); - expr_fvar(expr_fvar const &, expr const & new_type); // for hash_consing -public: - expr_fvar(name const & n, name const & pp_name, expr const & t, binder_info bi); - binder_info get_info() const { return m_bi; } -}; - -/** \brief Applications */ -class expr_app : public expr_composite { - expr m_fn; - expr m_arg; - friend expr_cell; - void dealloc(buffer & todelete); - expr_app(expr_app const &, expr const & new_fn, expr const & new_arg); // for hash_consing -public: - expr_app(expr const & fn, expr const & arg); - expr const & get_fn() const { return m_fn; } - expr const & get_arg() const { return m_arg; } -}; - -class binder { - friend class expr_binding; - name m_name; - expr m_type; - binder_info m_info; - binder(binder const & src, expr const & new_type): // for hash_consing - m_name(src.m_name), m_type(new_type), m_info(src.m_info) {} -public: - binder(name const & n, expr const & t, binder_info bi): - m_name(n), m_type(t), m_info(bi) {} - name const & get_name() const { return m_name; } - expr const & get_type() const { return m_type; } - binder_info get_info() const { return m_info; } - binder update_type(expr const & t) const { return binder(m_name, t, m_info); } -}; - -/** \brief Lambda and Pi expressions */ -class expr_binding : public expr_composite { - binder m_binder; - expr m_body; - friend class expr_cell; - void dealloc(buffer & todelete); - expr_binding(expr_binding const &, expr const & new_domain, expr const & new_body); // for hash_consing -public: - expr_binding(expr_kind k, name const & n, expr const & t, expr const & e, - binder_info i); - name const & get_name() const { return m_binder.get_name(); } - expr const & get_domain() const { return m_binder.get_type(); } - expr const & get_body() const { return m_body; } - binder_info get_info() const { return m_binder.get_info(); } - binder const & get_binder() const { return m_binder; } -}; - -/** \brief Let-expressions */ -class expr_let : public expr_composite { - name m_name; - expr m_type; - expr m_value; - expr m_body; - friend class expr_cell; - void dealloc(buffer & todelete); - expr_let(expr_let const &, expr const & new_type, expr const & new_value, expr const & new_body); // for hash_consing -public: - expr_let(name const & n, expr const & t, expr const & v, expr const & b); - name const & get_name() const { return m_name; } - expr const & get_type() const { return m_type; } - expr const & get_value() const { return m_value; } - expr const & get_body() const { return m_body; } -}; - -/** \brief Sort */ -class expr_sort : public expr_cell { - level m_level; - friend expr_cell; - void dealloc(); - expr_sort(expr_sort const &, level const & new_level); // for hash_consing -public: - expr_sort(level const & l); - ~expr_sort(); - level const & get_level() const { return m_level; } -}; - -class expr_lit : public expr_cell { - literal m_lit; - friend expr_cell; - void dealloc(); -public: - expr_lit(literal const & lit); - ~expr_lit(); - literal const & get_literal() const { return m_lit; } -}; - -class expr_mdata : public expr_composite { - kvmap m_data; - expr m_expr; - friend expr_cell; - void dealloc(buffer & todelete); -public: - expr_mdata(kvmap const & m, expr const & e); - ~expr_mdata() {} - kvmap const & get_data() const { return m_data; } - expr const & get_expr() const { return m_expr; } -}; - -class expr_proj : public expr_composite { - nat m_idx; - expr m_expr; - friend expr_cell; - void dealloc(buffer & todelete); -public: - expr_proj(nat const & idx, expr const & e); - ~expr_proj() {} - nat const & get_idx() const { return m_idx; } - expr const & get_expr() const { return m_expr; } -}; +struct expr_hash { unsigned operator()(expr const & e) const { return hash(e); } }; // ======================================= // Testers -inline bool is_bvar(expr_ptr e) { return e->kind() == expr_kind::BVar; } -inline bool is_fvar(expr_ptr e) { return e->kind() == expr_kind::FVar; } -inline bool is_constant(expr_ptr e) { return e->kind() == expr_kind::Constant; } -inline bool is_metavar(expr_ptr e) { return e->kind() == expr_kind::MVar; } -inline bool is_app(expr_ptr e) { return e->kind() == expr_kind::App; } -inline bool is_lambda(expr_ptr e) { return e->kind() == expr_kind::Lambda; } -inline bool is_pi(expr_ptr e) { return e->kind() == expr_kind::Pi; } -inline bool is_let(expr_ptr e) { return e->kind() == expr_kind::Let; } -inline bool is_sort(expr_ptr e) { return e->kind() == expr_kind::Sort; } -inline bool is_lit(expr_ptr e) { return e->kind() == expr_kind::Lit; } -inline bool is_mdata(expr_ptr e) { return e->kind() == expr_kind::MData; } -inline bool is_proj(expr_ptr e) { return e->kind() == expr_kind::Proj; } -inline bool is_binding(expr_ptr e) { return is_lambda(e) || is_pi(e); } +inline bool is_bvar(expr const & e) { return e.kind() == expr_kind::BVar; } +inline bool is_fvar(expr const & e) { return e.kind() == expr_kind::FVar; } +inline bool is_const(expr const & e) { return e.kind() == expr_kind::Const; } +inline bool is_mvar(expr const & e) { return e.kind() == expr_kind::MVar; } +inline bool is_app(expr const & e) { return e.kind() == expr_kind::App; } +inline bool is_lambda(expr const & e) { return e.kind() == expr_kind::Lambda; } +inline bool is_pi(expr const & e) { return e.kind() == expr_kind::Pi; } +inline bool is_let(expr const & e) { return e.kind() == expr_kind::Let; } +inline bool is_sort(expr const & e) { return e.kind() == expr_kind::Sort; } +inline bool is_lit(expr const & e) { return e.kind() == expr_kind::Lit; } +inline bool is_mdata(expr const & e) { return e.kind() == expr_kind::MData; } +inline bool is_proj(expr const & e) { return e.kind() == expr_kind::Proj; } +inline bool is_binding(expr const & e) { return is_lambda(e) || is_pi(e); } bool is_atomic(expr const & e); bool is_arrow(expr const & t); -/** \brief Return true iff \c e is a metavariable or an application of a metavariable */ -bool is_metavar_app(expr const & e); +bool is_default_var_name(name const & n); // ======================================= // ======================================= @@ -394,137 +175,87 @@ expr mk_lit(literal const & lit); expr mk_mdata(kvmap const & d, expr const & e); expr mk_proj(nat const & idx, expr const & e); inline expr mk_proj(unsigned idx, expr const & e) { return mk_proj(nat(idx), e); } -expr mk_bvar(unsigned idx); +expr mk_bvar(nat const & idx); +inline expr mk_bvar(unsigned idx) { return mk_bvar(nat(idx)); } expr mk_fvar(name const & n); -inline expr BVar(unsigned idx) { return mk_bvar(idx); } -expr mk_constant(name const & n, levels const & ls); -inline expr mk_constant(name const & n) { return mk_constant(n, levels()); } -inline expr Const(name const & n) { return mk_constant(n); } -expr mk_metavar(name const & n, expr const & t); -expr mk_metavar(name const & n, name const & pp_n, expr const & t); +expr mk_const(name const & n, levels const & ls); +inline expr mk_const(name const & n) { return mk_const(n, levels()); } +expr mk_mvar(name const & n, expr const & t); +expr mk_mvar(name const & n, name const & pp_n, expr const & t); expr mk_app(expr const & f, expr const & a); expr mk_app(expr const & f, unsigned num_args, expr const * args); expr mk_app(unsigned num_args, expr const * args); -inline expr mk_app(std::initializer_list const & l) { - return mk_app(l.size(), l.begin()); -} +inline expr mk_app(std::initializer_list const & l) { return mk_app(l.size(), l.begin()); } inline expr mk_app(buffer const & args) { return mk_app(args.size(), args.data()); } -inline expr mk_app(expr const & f, buffer const & args) { - return mk_app(f, args.size(), args.data()); -} +inline expr mk_app(expr const & f, buffer const & args) { return mk_app(f, args.size(), args.data()); } expr mk_app(expr const & f, list const & args); +inline expr mk_app(expr const & e1, expr const & e2, expr const & e3) { return mk_app({e1, e2, e3}); } +inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({e1, e2, e3, e4}); } +inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({e1, e2, e3, e4, e5}); } expr mk_rev_app(expr const & f, unsigned num_args, expr const * args); expr mk_rev_app(unsigned num_args, expr const * args); inline expr mk_rev_app(buffer const & args) { return mk_rev_app(args.size(), args.data()); } -inline expr mk_rev_app(expr const & f, buffer const & args) { - return mk_rev_app(f, args.size(), args.data()); -} -expr mk_binding(expr_kind k, name const & n, expr const & t, expr const & e, binder_info i = mk_binder_info()); -inline expr mk_lambda(name const & n, expr const & t, expr const & e, binder_info i = mk_binder_info()) { - return mk_binding(expr_kind::Lambda, n, t, e, i); -} -inline expr mk_pi(name const & n, expr const & t, expr const & e, binder_info i = mk_binder_info()) { - return mk_binding(expr_kind::Pi, n, t, e, i); +inline expr mk_rev_app(expr const & f, buffer const & args) { return mk_rev_app(f, args.size(), args.data()); } +expr mk_lambda(name const & n, expr const & t, expr const & e, binder_info bi = mk_binder_info()); +expr mk_pi(name const & n, expr const & t, expr const & e, binder_info bi = mk_binder_info()); +inline expr mk_binding(expr_kind k, name const & n, expr const & t, expr const & e, binder_info bi = mk_binder_info()) { + return k == expr_kind::Pi ? mk_pi(n, t, e, bi) : mk_lambda(n, t, e, bi); } +expr mk_arrow(expr const & t, expr const & e); expr mk_let(name const & n, expr const & t, expr const & v, expr const & b); expr mk_sort(level const & l); - expr mk_Prop(); expr mk_Type(); - -bool is_default_var_name(name const & n); -expr mk_arrow(expr const & t, expr const & e); -inline expr operator>>(expr const & t, expr const & e) { return mk_arrow(t, e); } - -// Auxiliary -inline expr mk_app(expr const & e1, expr const & e2, expr const & e3) { - return mk_app({e1, e2, e3}); -} -inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { - return mk_app({e1, e2, e3, e4}); -} -inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { - return mk_app({e1, e2, e3, e4, e5}); -} - // ======================================= -// ======================================= -// Casting (these functions are only needed for low-level code) -inline expr_lit * to_lit(expr_ptr e) { lean_assert(is_lit(e)); return static_cast(e); } -inline expr_mdata * to_mdata(expr_ptr e) { lean_assert(is_mdata(e)); return static_cast(e); } -inline expr_proj * to_proj(expr_ptr e) { lean_assert(is_proj(e)); return static_cast(e); } -inline expr_bvar * to_bvar(expr_ptr e) { lean_assert(is_bvar(e)); return static_cast(e); } -inline expr_fvar * to_fvar(expr_ptr e) { lean_assert(is_fvar(e)); return static_cast(e); } -inline expr_const * to_constant(expr_ptr e) { lean_assert(is_constant(e)); return static_cast(e); } -inline expr_app * to_app(expr_ptr e) { lean_assert(is_app(e)); return static_cast(e); } -inline expr_binding * to_binding(expr_ptr e) { lean_assert(is_binding(e)); return static_cast(e); } -inline expr_sort * to_sort(expr_ptr e) { lean_assert(is_sort(e)); return static_cast(e); } -inline expr_mlocal * to_metavar(expr_ptr e) { lean_assert(is_metavar(e)); return static_cast(e); } -inline expr_let * to_let(expr_ptr e) { lean_assert(is_let(e)); return static_cast(e); } -// ======================================= - - // ======================================= // Accessors -inline unsigned get_rc(expr_ptr e) { return e->get_rc(); } -inline bool is_shared(expr_ptr e) { return get_rc(e) > 1; } -inline literal const & lit_value(expr_ptr e) { return to_lit(e)->get_literal(); } -expr lit_type(expr_ptr e); -inline expr const & mdata_expr(expr_ptr e) { return to_mdata(e)->get_expr(); } -inline kvmap const & mdata_data(expr_ptr e) { return to_mdata(e)->get_data(); } -inline expr const & proj_expr(expr_ptr e) { return to_proj(e)->get_expr(); } -inline nat const & proj_idx(expr_ptr e) { return to_proj(e)->get_idx(); } -inline unsigned bvar_idx(expr_ptr e) { return to_bvar(e)->get_vidx(); } -inline bool is_bvar(expr_ptr e, unsigned i) { return is_bvar(e) && bvar_idx(e) == i; } -inline name const & fvar_name(expr_ptr e) { return to_fvar(e)->get_name(); } -inline level const & sort_level(expr_ptr e) { return to_sort(e)->get_level(); } -inline name const & const_name(expr_ptr e) { return to_constant(e)->get_name(); } -inline levels const & const_levels(expr_ptr e) { return to_constant(e)->get_levels(); } -inline expr const & app_fn(expr_ptr e) { return to_app(e)->get_fn(); } -inline expr const & app_arg(expr_ptr e) { return to_app(e)->get_arg(); } -inline name const & binding_name(expr_ptr e) { return to_binding(e)->get_name(); } -inline expr const & binding_domain(expr_ptr e) { return to_binding(e)->get_domain(); } -inline expr const & binding_body(expr_ptr e) { return to_binding(e)->get_body(); } -inline binder_info binding_info(expr_ptr e) { return to_binding(e)->get_info(); } -inline binder const & binding_binder(expr_ptr e) { return to_binding(e)->get_binder(); } -inline name const & let_name(expr_ptr e) { return to_let(e)->get_name(); } -inline expr const & let_type(expr_ptr e) { return to_let(e)->get_type(); } -inline expr const & let_value(expr_ptr e) { return to_let(e)->get_value(); } -inline expr const & let_body(expr_ptr e) { return to_let(e)->get_body(); } +inline literal const & lit_value(expr const & e) { lean_assert(is_lit(e)); return static_cast(cnstr_obj_ref(e, 0)); } +expr const & lit_type(expr const & e); +inline kvmap const & mdata_data(expr const & e) { lean_assert(is_mdata(e)); return static_cast(cnstr_obj_ref(e, 0)); } +inline expr const & mdata_expr(expr const & e) { lean_assert(is_mdata(e)); return static_cast(cnstr_obj_ref(e, 1)); } +inline nat const & proj_idx(expr const & e) { lean_assert(is_proj(e)); return static_cast(cnstr_obj_ref(e, 0)); } +inline expr const & proj_expr(expr const & e) { lean_assert(is_proj(e)); return static_cast(cnstr_obj_ref(e, 1)); } +inline nat const & bvar_idx(expr const & e) { lean_assert(is_bvar(e)); return static_cast(cnstr_obj_ref(e, 0)); } +inline bool is_bvar(expr const & e, unsigned i) { return is_bvar(e) && bvar_idx(e) == i; } +inline name const & fvar_name(expr const & e) { lean_assert(is_fvar(e)); return static_cast(cnstr_obj_ref(e, 0)); } +inline level const & sort_level(expr const & e) { lean_assert(is_sort(e)); return static_cast(cnstr_obj_ref(e, 0)); } +inline name const & mvar_name(expr const & e) { lean_assert(is_mvar(e)); return static_cast(cnstr_obj_ref(e, 0)); } +inline expr const & mvar_type(expr const & e) { lean_assert(is_mvar(e)); return static_cast(cnstr_obj_ref(e, 2)); } +inline name const & const_name(expr const & e) { lean_assert(is_const(e)); return static_cast(cnstr_obj_ref(e, 0)); } +inline levels const & const_levels(expr const & e) { lean_assert(is_const(e)); return static_cast(cnstr_obj_ref(e, 1)); } +inline bool is_const(expr const & e, name const & n) { return is_const(e) && const_name(e) == n; } +inline expr const & app_fn(expr const & e) { lean_assert(is_app(e)); return static_cast(cnstr_obj_ref(e, 0)); } +inline expr const & app_arg(expr const & e) { lean_assert(is_app(e)); return static_cast(cnstr_obj_ref(e, 1)); } +inline name const & binding_name(expr const & e) { lean_assert(is_binding(e)); return static_cast(cnstr_obj_ref(e, 0)); } +inline expr const & binding_domain(expr const & e) { lean_assert(is_binding(e)); return static_cast(cnstr_obj_ref(e, 1)); } +inline expr const & binding_body(expr const & e) { lean_assert(is_binding(e)); return static_cast(cnstr_obj_ref(e, 2)); } +binder_info binding_info(expr const & e); +inline name const & let_name(expr const & e) { lean_assert(is_let(e)); return static_cast(cnstr_obj_ref(e, 0)); } +inline expr const & let_type(expr const & e) { lean_assert(is_let(e)); return static_cast(cnstr_obj_ref(e, 1)); } +inline expr const & let_value(expr const & e) { lean_assert(is_let(e)); return static_cast(cnstr_obj_ref(e, 2)); } +inline expr const & let_body(expr const & e) { lean_assert(is_let(e)); return static_cast(cnstr_obj_ref(e, 3)); } +inline bool is_shared(expr const & e) { return is_shared(e.raw()); } +// + +// ======================================= +// Update +expr update_app(expr const & e, expr const & new_fn, expr const & new_arg); +expr update_binding(expr const & e, expr const & new_domain, expr const & new_body); +expr update_binding(expr const & e, expr const & new_domain, expr const & new_body, binder_info bi); +expr update_sort(expr const & e, level const & new_level); +expr update_const(expr const & e, levels const & new_levels); +expr update_let(expr const & e, expr const & new_type, expr const & new_value, expr const & new_body); +expr update_mdata(expr const & e, expr const & new_e); +expr update_proj(expr const & e, expr const & new_e); +expr update_mvar(expr const & e, expr const & new_type); +// ======================================= -inline bool is_constant(expr const & e, name const & n) { return is_constant(e) && const_name(e) == n; } -inline bool has_metavar(expr const & e) { return e.has_metavar(); } -inline bool has_expr_metavar(expr const & e) { return e.has_expr_metavar(); } -inline bool has_univ_metavar(expr const & e) { return e.has_univ_metavar(); } -/** \brief Similar to \c has_expr_metavar, but ignores metavariables occurring in local constant types. - It also returns the meta-variable application found in \c e. -*/ -optional has_expr_metavar_strict(expr const & e); -inline bool has_fvar(expr const & e) { return e.has_fvar(); } -inline bool has_param_univ(expr const & e) { return e.has_param_univ(); } -unsigned get_weight(expr const & e); -unsigned get_depth(expr const & e); -/** \brief Return \c R s.t. the de Bruijn index of all loose bound variables - occurring in \c e is in the interval [0, R). */ -inline unsigned get_loose_bvar_range(expr const & e) { - switch (e.kind()) { - case expr_kind::BVar: return bvar_idx(e) + 1; - case expr_kind::Constant: case expr_kind::Sort: return 0; - case expr_kind::Quote: return 0; - case expr_kind::Lit: return 0; - default: return static_cast(e.raw())->m_loose_bvar_range; - } -} -/** \brief Return true iff the given expression has loose bound variables. */ -inline bool has_loose_bvars(expr const & e) { return get_loose_bvar_range(e) > 0; } -/** - \brief Given \c e of the form (...(f a1) ... an), store a1 ... an in args. +/** \brief Given \c e of the form (...(f a1) ... an), store a1 ... an in args. If \c e is not an application, then nothing is stored in args. - It returns the f. -*/ + It returns the f. */ expr const & get_app_args(expr const & e, buffer & args); /** \brief Similar to \c get_app_args, but stores at most num args. Examples: @@ -532,54 +263,34 @@ expr const & get_app_args(expr const & e, buffer & args); stores {b, c} in args and returns (f a) 2) get_app_args_at_most(f a b c, 4, args); - stores {a, b, c} in args and returns f -*/ + stores {a, b, c} in args and returns f */ expr const & get_app_args_at_most(expr const & e, unsigned num, buffer & args); -/** - \brief Similar to \c get_app_args, but arguments are stored in reverse order in \c args. - If e is of the form (...(f a1) ... an), then the procedure stores [an, ..., a1] in \c args. -*/ +/** \brief Similar to \c get_app_args, but arguments are stored in reverse order in \c args. + If e is of the form (...(f a1) ... an), then the procedure stores [an, ..., a1] in \c args. */ expr const & get_app_rev_args(expr const & e, buffer & args); /** \brief Given \c e of the form (...(f a_1) ... a_n), return \c f. If \c e is not an application, then return \c e. */ expr const & get_app_fn(expr const & e); /** \brief Given \c e of the form (...(f a_1) ... a_n), return \c n. If \c e is not an application, then return 0. */ unsigned get_app_num_args(expr const & e); -// ======================================= -// ======================================= -// Auxiliary functionals -/** \brief Functional object for hashing kernel expressions. */ -struct expr_hash { unsigned operator()(expr const & e) const { return e.hash(); } }; -// ======================================= - -// ======================================= -// Update -expr update_app(expr const & e, expr const & new_fn, expr const & new_arg); -expr update_binding(expr const & e, expr const & new_domain, expr const & new_body); -expr update_binding(expr const & e, expr const & new_domain, expr const & new_body, binder_info bi); -expr update_mlocal(expr const & e, expr const & new_type); -expr update_local(expr const & e, expr const & new_type, binder_info bi); -expr update_local(expr const & e, binder_info bi); -expr update_sort(expr const & e, level const & new_level); -expr update_constant(expr const & e, levels const & new_levels); -expr update_let(expr const & e, expr const & new_type, expr const & new_value, expr const & new_body); -expr update_mdata(expr const & e, expr const & t); -expr update_proj(expr const & e, expr const & t); -// ======================================= +/** \brief Return true iff \c e is a metavariable or an application of a metavariable */ +inline bool is_mvar_app(expr const & e) { return is_mvar(get_app_fn(e)); } // ======================================= // Loose bound variable management +/** \brief Return true iff the given expression has loose bound variables. */ +inline bool has_loose_bvars(expr const & e) { return get_loose_bvar_range(e) > 0; } + /** \brief Return true iff \c e contains the loose bound variable (var i). */ bool has_loose_bvar(expr const & e, unsigned i); -/** - \brief Lower the loose bound variables >= s in \c e by \c d. That is, a loose bound variable (var i) s.t. - i >= s is mapped into (var i-d). +/** \brief Lower the loose bound variables >= s in \c e by \c d. That is, a loose bound variable (var i) s.t. + i >= s is mapped into (var i-d). - \pre s >= d */ + \pre s >= d */ expr lower_loose_bvars(expr const & e, unsigned s, unsigned d); expr lower_loose_bvars(expr const & e, unsigned d); @@ -601,64 +312,53 @@ expr infer_implicit(expr const & t, unsigned num_params, bool strict); expr infer_implicit(expr const & t, bool strict); // ======================================= +// ======================================= +// Low level (raw) printing std::ostream & operator<<(std::ostream & out, expr_kind const & k); std::ostream & operator<<(std::ostream & out, expr const & e); - -#ifdef LEAN_TRACK_LIVE_EXPRS -unsigned get_num_live_exprs(); -#endif +// ======================================= void initialize_expr(); void finalize_expr(); - - -/* ------ LEGACY CODE ------------- - The following API is to support legacy code - -------------------------------- */ - -// TODO(Leo): delete -class expr_quote : public expr_cell { - bool m_reflected; - expr m_value; - friend class expr_cell; - void dealloc(buffer & todelete); -public: - expr_quote(bool r, expr const & v); - ~expr_quote() {} - bool is_reflected() const { return m_reflected; } - expr const & get_value() const { return m_value; } -}; - -inline bool is_var(expr_ptr e) { return is_bvar(e); } -inline bool is_local(expr_ptr e) { return is_fvar(e); } -inline bool is_mlocal(expr_ptr e) { return is_metavar(e) || is_local(e); } -inline bool is_quote(expr_ptr e) { return e->kind() == expr_kind::Quote; } -inline unsigned var_idx(expr_ptr e) { return bvar_idx(e); } -inline bool is_var(expr_ptr e, unsigned i) { return is_bvar(e, i); } -inline expr_bvar * to_var(expr_ptr e) { return to_bvar(e); } -inline expr_mlocal * to_mlocal(expr_ptr e) { lean_assert(is_mlocal(e)); return static_cast(e); } -inline expr_fvar * to_local(expr_ptr e) { return to_fvar(e); } -inline expr_quote * to_quote(expr_ptr e) { lean_assert(is_quote(e)); return static_cast(e); } - -inline name const & mlocal_name(expr_ptr e) { return to_mlocal(e)->get_name(); } -inline expr const & mlocal_type(expr_ptr e) { return to_mlocal(e)->get_type(); } -inline name const & mlocal_pp_name(expr_ptr e) { return to_mlocal(e)->get_pp_name(); } -inline binder_info local_info(expr_ptr e) { return to_local(e)->get_info(); } -inline expr mk_var(unsigned idx) { return mk_bvar(idx); } -inline expr Var(unsigned idx) { return mk_bvar(idx); } -expr mk_quote(bool reflected, expr const & val); +/* ================= LEGACY ============== */ +inline bool has_expr_metavar(expr const & e) { return has_expr_mvar(e); } +inline bool has_univ_metavar(expr const & e) { return has_univ_mvar(e); } +inline bool has_metavar(expr const & e) { return has_mvar(e); } +inline bool has_param_univ(expr const & e) { return has_univ_param(e); } +inline bool is_var(expr const & e) { return is_bvar(e); } +inline bool is_var(expr const & e, unsigned idx) { return is_bvar(e, idx); } +inline bool is_metavar(expr const & e) { return is_mvar(e); } +inline bool is_metavar_app(expr const & e) { return is_mvar_app(e); } +expr mk_metavar(name const & n, name const & pp_n, expr const & t); +inline expr mk_metavar(name const & n, expr const & t) { return mk_metavar(n, n, t); } expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info bi); inline expr mk_local(name const & n, expr const & t) { return mk_local(n, n, t, mk_binder_info()); } -inline expr mk_local(name const & n, expr const & t, binder_info bi) { - return mk_local(n, n, t, bi); -} -inline expr Local(name const & n, expr const & t, binder_info bi = mk_binder_info()) { - return mk_local(n, t, bi); -} +inline expr mk_local(name const & n, expr const & t, binder_info bi) { return mk_local(n, n, t, bi); } +inline expr Local(name const & n, expr const & t, binder_info bi = mk_binder_info()) { return mk_local(n, t, bi); } +inline name const & mlocal_name(expr const & e) { return static_cast(cnstr_obj_ref(e, 0)); } +inline name const & mlocal_pp_name(expr const & e) { return static_cast(cnstr_obj_ref(e, 1)); } +inline expr const & mlocal_type(expr const & e) { return static_cast(cnstr_obj_ref(e, 2)); } +inline expr mk_constant(name const & n, levels const & ls) { return mk_const(n, ls); } +inline expr mk_constant(name const & n) { return mk_constant(n, levels()); } +inline expr Const(name const & n) { return mk_constant(n); } +inline expr BVar(unsigned idx) { return mk_bvar(idx); } +inline expr Var(unsigned idx) { return mk_bvar(idx); } +inline bool is_constant(expr const & e) { return is_const(e); } +expr mk_quote(bool is_reflected, expr const & e); +inline expr const & quote_value(expr const & e) { return static_cast(cnstr_obj_ref(e, 0)); } +inline bool is_local(expr const & e) { return is_fvar(e); } +bool quote_is_reflected(expr const & e); +expr update_mlocal(expr const & e, expr const & new_type); +expr update_local(expr const & e, expr const & new_type, binder_info bi); +expr update_local(expr const & e, binder_info bi); +binder_info local_info(expr const & e); +inline expr update_constant(expr const & e, levels const & new_levels) { return update_const(e, new_levels); } +/** \brief Similar to \c has_expr_metavar, but ignores metavariables occurring in local constant types. + It also returns the meta-variable application found in \c e. */ +optional has_expr_metavar_strict(expr const & e); +inline bool is_constant(expr const & e, name const & n) { return is_const(e, n); } +inline bool is_quote(expr const & e) { return e.kind() == expr_kind::Quote; } +inline bool is_mlocal(expr const & e) { return is_local(e) || is_metavar(e); } inline bool has_local(expr const & e) { return has_fvar(e); } - -inline bool quote_is_reflected(expr const & e) { return to_quote(e)->is_reflected(); } -inline expr const & quote_value(expr const & e) { return to_quote(e)->get_value(); } - } diff --git a/src/kernel/expr_cache.cpp b/src/kernel/expr_cache.cpp index 5b8dfd33c7..9a13c1afe2 100644 --- a/src/kernel/expr_cache.cpp +++ b/src/kernel/expr_cache.cpp @@ -8,7 +8,7 @@ Author: Leonardo de Moura namespace lean { expr * expr_cache::find(expr const & e) { - unsigned i = e.hash() % m_capacity; + unsigned i = hash(e) % m_capacity; if (m_cache[i].m_expr && is_bi_equal(*m_cache[i].m_expr, e)) return &m_cache[i].m_result; else @@ -16,7 +16,7 @@ expr * expr_cache::find(expr const & e) { } void expr_cache::insert(expr const & e, expr const & v) { - unsigned i = e.hash() % m_capacity; + unsigned i = hash(e) % m_capacity; if (!m_cache[i].m_expr) m_used.push_back(i); m_cache[i].m_expr = e; diff --git a/src/kernel/expr_eq_fn.cpp b/src/kernel/expr_eq_fn.cpp index f86de11816..7a2ef9e036 100644 --- a/src/kernel/expr_eq_fn.cpp +++ b/src/kernel/expr_eq_fn.cpp @@ -18,8 +18,8 @@ Author: Leonardo de Moura namespace lean { struct eq_cache { struct entry { - expr_ptr m_a; - expr_ptr m_b; + object * m_a; + object * m_b; entry():m_a(nullptr), m_b(nullptr) {} }; unsigned m_capacity; @@ -30,7 +30,7 @@ struct eq_cache { bool check(expr const & a, expr const & b) { if (!is_shared(a) || !is_shared(b)) return false; - unsigned i = hash(a.hash(), b.hash()) % m_capacity; + unsigned i = hash(hash(a), hash(b)) % m_capacity; if (m_cache[i].m_a == a.raw() && m_cache[i].m_b == b.raw()) { return true; } else { @@ -64,9 +64,9 @@ class expr_eq_fn { bool apply(expr const & a, expr const & b) { if (is_eqp(a, b)) return true; - if (a.hash() != b.hash()) return false; + if (hash(a) != hash(b)) return false; if (a.kind() != b.kind()) return false; - if (is_var(a)) return var_idx(a) == var_idx(b); + if (is_bvar(a)) return bvar_idx(a) == bvar_idx(b); if (m_cache.check(a, b)) return true; switch (a.kind()) { @@ -82,7 +82,7 @@ class expr_eq_fn { proj_idx(a) == proj_idx(b); case expr_kind::Lit: return lit_value(a) == lit_value(b); - case expr_kind::Constant: + case expr_kind::Const: return const_name(a) == const_name(b) && compare(const_levels(a), const_levels(b), [](level const & l1, level const & l2) { return l1 == l2; }); diff --git a/src/kernel/expr_pair.h b/src/kernel/expr_pair.h index 4a96f058c1..c08f8dd0e2 100644 --- a/src/kernel/expr_pair.h +++ b/src/kernel/expr_pair.h @@ -11,7 +11,7 @@ typedef pair level_pair; typedef pair expr_pair; /** \brief Functional object for hashing expression pairs. */ struct expr_pair_hash { - unsigned operator()(expr_pair const & p) const { return hash(p.first.hash(), p.second.hash()); } + unsigned operator()(expr_pair const & p) const { return hash(hash(p.first), hash(p.second)); } }; /** \brief Functional object for comparing expression pairs. */ diff --git a/src/kernel/for_each_fn.cpp b/src/kernel/for_each_fn.cpp index 0b4604afa0..2998aba3ff 100644 --- a/src/kernel/for_each_fn.cpp +++ b/src/kernel/for_each_fn.cpp @@ -19,7 +19,7 @@ Author: Leonardo de Moura namespace lean { struct for_each_cache { struct entry { - expr_cell const * m_cell; + object const * m_cell; unsigned m_offset; entry():m_cell(nullptr) {} }; @@ -29,7 +29,7 @@ struct for_each_cache { for_each_cache(unsigned c):m_capacity(c), m_cache(c) {} bool visited(expr const & e, unsigned offset) { - unsigned i = hash(e.hash(), offset) % m_capacity; + unsigned i = hash(hash(e), offset) % m_capacity; if (m_cache[i].m_cell == e.raw() && m_cache[i].m_offset == offset) { return true; } else { @@ -70,7 +70,7 @@ class for_each_fn { unsigned offset = p.second; switch (e.kind()) { - case expr_kind::Constant: case expr_kind::BVar: + case expr_kind::Const: case expr_kind::BVar: case expr_kind::Sort: m_f(e, offset); goto begin_loop; @@ -85,8 +85,8 @@ class for_each_fn { goto begin_loop; switch (e.kind()) { - case expr_kind::Constant: case expr_kind::BVar: - case expr_kind::Sort: case expr_kind::Lit: + case expr_kind::Const: case expr_kind::BVar: + case expr_kind::Sort: case expr_kind::Lit: goto begin_loop; case expr_kind::MData: todo.emplace_back(mdata_expr(e), offset); diff --git a/src/kernel/instantiate.cpp b/src/kernel/instantiate.cpp index 3f9b8b981a..11b3e5f1c6 100644 --- a/src/kernel/instantiate.cpp +++ b/src/kernel/instantiate.cpp @@ -67,7 +67,7 @@ struct instantiate_easy_fn { if (!has_loose_bvars(a)) return some_expr(a); if (is_bvar(a) && bvar_idx(a) < n) - return some_expr(subst[rev ? n - bvar_idx(a) - 1 : bvar_idx(a)]); + return some_expr(subst[rev ? n - bvar_idx(a).get_small_value() - 1 : bvar_idx(a).get_small_value()]); if (app && is_app(a)) if (auto new_a = operator()(app_arg(a), false)) if (auto new_f = operator()(app_fn(a), true)) @@ -89,13 +89,13 @@ expr instantiate(expr const & a, unsigned s, unsigned n, expr const * subst) { if (s1 >= get_loose_bvar_range(m)) return some_expr(m); // expression m does not contain loose bound variables with idx >= s1 if (is_bvar(m)) { - unsigned vidx = bvar_idx(m); + nat const & vidx = bvar_idx(m); if (vidx >= s1) { unsigned h = s1 + n; if (h < s1 /* overflow, h is bigger than any vidx */ || vidx < h) { - return some_expr(lift_loose_bvars(subst[vidx - s1], offset)); + return some_expr(lift_loose_bvars(subst[vidx.get_small_value() - s1], offset)); } else { - return some_expr(mk_bvar(vidx - n)); + return some_expr(mk_bvar(vidx - nat(n))); } } } @@ -117,13 +117,13 @@ expr instantiate_rev(expr const & a, unsigned n, expr const * subst) { if (offset >= get_loose_bvar_range(m)) return some_expr(m); // expression m does not contain loose bound variables with idx >= offset if (is_bvar(m)) { - unsigned vidx = bvar_idx(m); + nat const & vidx = bvar_idx(m); if (vidx >= offset) { unsigned h = offset + n; if (h < offset /* overflow, h is bigger than any vidx */ || vidx < h) { - return some_expr(lift_loose_bvars(subst[n - (vidx - offset) - 1], offset)); + return some_expr(lift_loose_bvars(subst[n - (vidx.get_small_value() - offset) - 1], offset)); } else { - return some_expr(mk_bvar(vidx - n)); + return some_expr(mk_bvar(vidx - nat(n))); } } } diff --git a/src/kernel/level.h b/src/kernel/level.h index 6e11d8008d..d4552c96b2 100644 --- a/src/kernel/level.h +++ b/src/kernel/level.h @@ -90,6 +90,7 @@ inline serializer & operator<<(serializer & s, level const & l) { l.serialize(s) inline serializer & operator<<(serializer & s, levels const & ls) { ls.serialize(s); return s; } inline level read_level(deserializer & d) { return level::deserialize(d); } inline levels read_levels(deserializer & d) { return read_list_ref(d); } +inline deserializer & operator>>(deserializer & d, level & l) { l = read_level(d); return d; } inline optional none_level() { return optional(); } inline optional some_level(level const & e) { return optional(e); } diff --git a/src/kernel/old_type_checker.cpp b/src/kernel/old_type_checker.cpp index c549a29594..809d67727b 100644 --- a/src/kernel/old_type_checker.cpp +++ b/src/kernel/old_type_checker.cpp @@ -247,13 +247,13 @@ expr old_type_checker::infer_type_core(expr const & e, bool infer_only) { r = binding_domain(r); break; } - case expr_kind::MData: r = infer_type_core(mdata_expr(e), infer_only); break; - case expr_kind::Constant: r = infer_constant(e, infer_only); break; - case expr_kind::Lambda: r = infer_lambda(e, infer_only); break; - case expr_kind::Pi: r = infer_pi(e, infer_only); break; - case expr_kind::App: r = infer_app(e, infer_only); break; - case expr_kind::Let: r = infer_let(e, infer_only); break; - case expr_kind::Lit: r = infer_let(e, infer_only); break; + case expr_kind::MData: r = infer_type_core(mdata_expr(e), infer_only); break; + case expr_kind::Const: r = infer_constant(e, infer_only); break; + case expr_kind::Lambda: r = infer_lambda(e, infer_only); break; + case expr_kind::Pi: r = infer_pi(e, infer_only); break; + case expr_kind::App: r = infer_app(e, infer_only); break; + case expr_kind::Let: r = infer_let(e, infer_only); break; + case expr_kind::Lit: r = infer_let(e, infer_only); break; case expr_kind::Quote: throw_found_quote(m_env); } @@ -306,8 +306,8 @@ expr old_type_checker::whnf_core(expr const & e) { // handle easy cases switch (e.kind()) { - case expr_kind::BVar: case expr_kind::Sort: case expr_kind::MVar: case expr_kind::FVar: - case expr_kind::Pi: case expr_kind::Constant: case expr_kind::Lambda: case expr_kind::Lit: + case expr_kind::BVar: case expr_kind::Sort: case expr_kind::MVar: case expr_kind::FVar: + case expr_kind::Pi: case expr_kind::Const: case expr_kind::Lambda: case expr_kind::Lit: return e; case expr_kind::MData: return whnf_core(mdata_expr(e)); @@ -327,8 +327,8 @@ expr old_type_checker::whnf_core(expr const & e) { // do the actual work expr r; switch (e.kind()) { - case expr_kind::BVar: case expr_kind::Sort: case expr_kind::MVar: case expr_kind::FVar: - case expr_kind::Pi: case expr_kind::Constant: case expr_kind::Lambda: case expr_kind::Lit: + case expr_kind::BVar: case expr_kind::Sort: case expr_kind::MVar: case expr_kind::FVar: + case expr_kind::Pi: case expr_kind::Const: case expr_kind::Lambda: case expr_kind::Lit: case expr_kind::MData: lean_unreachable(); // LCOV_EXCL_LINE case expr_kind::Proj: { @@ -442,8 +442,8 @@ expr old_type_checker::whnf(expr const & e) { return whnf(mdata_expr(e)); case expr_kind::Proj: lean_unreachable(); - case expr_kind::Lambda: case expr_kind::App: - case expr_kind::Constant: case expr_kind::Let: + case expr_kind::Lambda: case expr_kind::App: + case expr_kind::Const: case expr_kind::Let: break; case expr_kind::Quote: throw_found_quote(m_env); } @@ -538,8 +538,8 @@ lbool old_type_checker::quick_is_def_eq(expr const & t, expr const & s, bool use return to_lbool(is_def_eq(sort_level(t), sort_level(s))); case expr_kind::MVar: lean_unreachable(); // LCOV_EXCL_LINE - case expr_kind::BVar: case expr_kind::FVar: case expr_kind::App: - case expr_kind::Constant: case expr_kind::Let: + case expr_kind::BVar: case expr_kind::FVar: case expr_kind::App: + case expr_kind::Const: case expr_kind::Let: // We do not handle these cases in this method. break; case expr_kind::Proj: @@ -613,9 +613,9 @@ bool old_type_checker::is_def_eq_proof_irrel(expr const & t, expr const & s) { } bool old_type_checker::failed_before(expr const & t, expr const & s) const { - if (t.hash() < s.hash()) { + if (hash(t) < hash(s)) { return m_failure_cache.find(mk_pair(t, s)) != m_failure_cache.end(); - } else if (t.hash() > s.hash()) { + } else if (hash(t) > hash(s)) { return m_failure_cache.find(mk_pair(s, t)) != m_failure_cache.end(); } else { return @@ -625,7 +625,7 @@ bool old_type_checker::failed_before(expr const & t, expr const & s) const { } void old_type_checker::cache_failure(expr const & t, expr const & s) { - if (t.hash() <= s.hash()) + if (hash(t) <= hash(s)) m_failure_cache.insert(mk_pair(t, s)); else m_failure_cache.insert(mk_pair(s, t)); diff --git a/src/kernel/replace_fn.cpp b/src/kernel/replace_fn.cpp index f0d87e129d..4795aad293 100644 --- a/src/kernel/replace_fn.cpp +++ b/src/kernel/replace_fn.cpp @@ -16,9 +16,9 @@ Author: Leonardo de Moura namespace lean { struct replace_cache { struct entry { - expr_cell * m_cell; - unsigned m_offset; - expr m_result; + object * m_cell; + unsigned m_offset; + expr m_result; entry():m_cell(nullptr) {} }; unsigned m_capacity; @@ -27,7 +27,7 @@ struct replace_cache { replace_cache(unsigned c):m_capacity(c), m_cache(c) {} expr * find(expr const & e, unsigned offset) { - unsigned i = hash(e.hash(), offset) % m_capacity; + unsigned i = hash(hash(e), offset) % m_capacity; if (m_cache[i].m_cell == e.raw() && m_cache[i].m_offset == offset) return &m_cache[i].m_result; else @@ -35,7 +35,7 @@ struct replace_cache { } void insert(expr const & e, unsigned offset, expr const & v) { - unsigned i = hash(e.hash(), offset) % m_capacity; + unsigned i = hash(hash(e), offset) % m_capacity; if (m_cache[i].m_cell == nullptr) m_used.push_back(i); m_cache[i].m_cell = e.raw(); @@ -79,8 +79,8 @@ class replace_rec_fn { return save_result(e, offset, *r, shared); } else { switch (e.kind()) { - case expr_kind::Constant: case expr_kind::Sort: - case expr_kind::BVar: case expr_kind::Lit: + case expr_kind::Const: case expr_kind::Sort: + case expr_kind::BVar: case expr_kind::Lit: return save_result(e, offset, e, shared); case expr_kind::MData: { expr new_e = apply(mdata_expr(e), offset); diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 5c4608cd4b..29dbde882b 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -243,22 +243,22 @@ expr type_checker::infer_type_core(expr const & e, bool infer_only) { expr r; switch (e.kind()) { - case expr_kind::Lit: r = lit_type(e); break; - case expr_kind::MData: r = infer_type_core(mdata_expr(e), infer_only); break; - case expr_kind::Proj: r = infer_proj(e, infer_only); break; - case expr_kind::FVar: r = infer_fvar(e); break; - case expr_kind::MVar: r = mlocal_type(e); break; + case expr_kind::Lit: r = lit_type(e); break; + case expr_kind::MData: r = infer_type_core(mdata_expr(e), infer_only); break; + case expr_kind::Proj: r = infer_proj(e, infer_only); break; + case expr_kind::FVar: r = infer_fvar(e); break; + case expr_kind::MVar: r = mlocal_type(e); break; case expr_kind::BVar: lean_unreachable(); // LCOV_EXCL_LINE case expr_kind::Sort: if (!infer_only) check_level(sort_level(e)); r = mk_sort(mk_succ(sort_level(e))); break; - case expr_kind::Constant: r = infer_constant(e, infer_only); break; - case expr_kind::Lambda: r = infer_lambda(e, infer_only); break; - case expr_kind::Pi: r = infer_pi(e, infer_only); break; - case expr_kind::App: r = infer_app(e, infer_only); break; - case expr_kind::Let: r = infer_let(e, infer_only); break; + case expr_kind::Const: r = infer_constant(e, infer_only); break; + case expr_kind::Lambda: r = infer_lambda(e, infer_only); break; + case expr_kind::Pi: r = infer_pi(e, infer_only); break; + case expr_kind::App: r = infer_app(e, infer_only); break; + case expr_kind::Let: r = infer_let(e, infer_only); break; case expr_kind::Quote: if (quote_is_reflected(e)) { @@ -347,8 +347,8 @@ expr type_checker::whnf_core(expr const & e) { // handle easy cases switch (e.kind()) { - case expr_kind::BVar: case expr_kind::Sort: case expr_kind::MVar: - case expr_kind::Pi: case expr_kind::Constant: case expr_kind::Lambda: + case expr_kind::BVar: case expr_kind::Sort: case expr_kind::MVar: + case expr_kind::Pi: case expr_kind::Const: case expr_kind::Lambda: case expr_kind::Lit: return e; case expr_kind::MData: @@ -373,8 +373,8 @@ expr type_checker::whnf_core(expr const & e) { // do the actual work expr r; switch (e.kind()) { - case expr_kind::BVar: case expr_kind::Sort: case expr_kind::MVar: case expr_kind::FVar: - case expr_kind::Pi: case expr_kind::Constant: case expr_kind::Lambda: + case expr_kind::BVar: case expr_kind::Sort: case expr_kind::MVar: case expr_kind::FVar: + case expr_kind::Pi: case expr_kind::Const: case expr_kind::Lambda: case expr_kind::Lit: case expr_kind::MData: lean_unreachable(); // LCOV_EXCL_LINE @@ -465,15 +465,15 @@ optional type_checker::unfold_definition(expr const & e) { expr type_checker::whnf(expr const & e) { // Do not cache easy cases switch (e.kind()) { - case expr_kind::BVar: case expr_kind::Sort: case expr_kind::MVar: case expr_kind::Pi: + case expr_kind::BVar: case expr_kind::Sort: case expr_kind::MVar: case expr_kind::Pi: case expr_kind::Lit: return e; case expr_kind::MData: return whnf(mdata_expr(e)); case expr_kind::FVar: return whnf_fvar(e); - case expr_kind::Lambda: case expr_kind::App: - case expr_kind::Constant: case expr_kind::Let: case expr_kind::Proj: + case expr_kind::Lambda: case expr_kind::App: + case expr_kind::Const: case expr_kind::Let: case expr_kind::Proj: break; case expr_kind::Quote: @@ -571,8 +571,8 @@ lbool type_checker::quick_is_def_eq(expr const & t, expr const & s, bool use_has return to_lbool(is_def_eq(mdata_expr(t), mdata_expr(s))); case expr_kind::MVar: lean_unreachable(); // LCOV_EXCL_LINE - case expr_kind::BVar: case expr_kind::FVar: case expr_kind::App: - case expr_kind::Constant: case expr_kind::Let: + case expr_kind::BVar: case expr_kind::FVar: case expr_kind::App: + case expr_kind::Const: case expr_kind::Let: case expr_kind::Proj: // We do not handle these cases in this method. break; @@ -646,9 +646,9 @@ bool type_checker::is_def_eq_proof_irrel(expr const & t, expr const & s) { } bool type_checker::failed_before(expr const & t, expr const & s) const { - if (t.hash() < s.hash()) { + if (hash(t) < hash(s)) { return m_failure_cache.find(mk_pair(t, s)) != m_failure_cache.end(); - } else if (t.hash() > s.hash()) { + } else if (hash(t) > hash(s)) { return m_failure_cache.find(mk_pair(s, t)) != m_failure_cache.end(); } else { return @@ -658,7 +658,7 @@ bool type_checker::failed_before(expr const & t, expr const & s) const { } void type_checker::cache_failure(expr const & t, expr const & s) { - if (t.hash() <= s.hash()) + if (hash(t) <= hash(s)) m_failure_cache.insert(mk_pair(t, s)); else m_failure_cache.insert(mk_pair(s, t)); diff --git a/src/library/check.cpp b/src/library/check.cpp index c3f371ceb1..508c109dab 100644 --- a/src/library/check.cpp +++ b/src/library/check.cpp @@ -108,7 +108,7 @@ struct check_fn { case expr_kind::Sort: case expr_kind::Lit: break; /* do nothing */ - case expr_kind::Constant: + case expr_kind::Const: return visit_constant(e); case expr_kind::BVar: lean_unreachable(); // LCOV_EXCL_LINE diff --git a/src/library/compiler/cse.cpp b/src/library/compiler/cse.cpp index 81f5d7b57a..0c60ea1698 100644 --- a/src/library/compiler/cse.cpp +++ b/src/library/compiler/cse.cpp @@ -47,9 +47,9 @@ class cse_fn : public compiler_step_visitor { void visit(expr const & e) { switch (e.kind()) { - case expr_kind::BVar: case expr_kind::Sort: - case expr_kind::MVar: case expr_kind::Pi: - case expr_kind::Constant: case expr_kind::FVar: + case expr_kind::BVar: case expr_kind::Sort: + case expr_kind::MVar: case expr_kind::Pi: + case expr_kind::Const: case expr_kind::FVar: case expr_kind::Lit: break; case expr_kind::Lambda: visit_lambda(e); break; diff --git a/src/library/compiler/inliner.cpp b/src/library/compiler/inliner.cpp index 80f309adee..41103469ef 100644 --- a/src/library/compiler/inliner.cpp +++ b/src/library/compiler/inliner.cpp @@ -53,10 +53,13 @@ class inline_simple_definitions_fn : public compiler_step_visitor { if (!is_constant(g) && !is_var(g)) return false; for (expr const & y : ys) { - if (!is_var(y) && !is_constant(y)) + if (!is_bvar(y) && !is_constant(y)) return false; - if (is_var(y)) { - unsigned vidx = var_idx(y); + if (is_bvar(y)) { + nat const & n_vidx = bvar_idx(y); + if (!n_vidx.is_small()) + return false; + unsigned vidx = n_vidx.get_small_value(); if (vidx >= bitmap.size()) bitmap.resize(vidx+1, false); if (bitmap[vidx]) { diff --git a/src/library/compiler/vm_compiler.cpp b/src/library/compiler/vm_compiler.cpp index 32a88f83a5..f36eabdeea 100644 --- a/src/library/compiler/vm_compiler.cpp +++ b/src/library/compiler/vm_compiler.cpp @@ -302,7 +302,7 @@ class vm_compiler_fn { case expr_kind::Lambda: lean_unreachable(); case expr_kind::MData: compile(mdata_expr(e), bpz, m); break; case expr_kind::Proj: compile_proj_cnstr(e, bpz, m); break; - case expr_kind::Constant: compile_constant(e); break; + case expr_kind::Const: compile_constant(e); break; case expr_kind::FVar: compile_local(e, m); break; case expr_kind::App: compile_app(e, bpz, m); break; case expr_kind::Let: compile_let(e, bpz, m); break; diff --git a/src/library/context_cache.cpp b/src/library/context_cache.cpp index ec39a4d3c1..b51160b6c6 100644 --- a/src/library/context_cache.cpp +++ b/src/library/context_cache.cpp @@ -71,9 +71,9 @@ void context_cache::set_equiv(transparency_mode m, expr const & e1, expr const & bool context_cache::get_is_def_eq_failure(transparency_mode m, expr const & t, expr const & s) { auto const & fcache = m_failure_cache[static_cast(m)]; - if (t.hash() < s.hash()) { + if (hash(t) < hash(s)) { return fcache.find(mk_pair(t, s)) != fcache.end(); - } else if (t.hash() > s.hash()) { + } else if (hash(t) > hash(s)) { return fcache.find(mk_pair(s, t)) != fcache.end(); } else { return @@ -84,7 +84,7 @@ bool context_cache::get_is_def_eq_failure(transparency_mode m, expr const & t, e void context_cache::set_is_def_eq_failure(transparency_mode m, expr const & t, expr const & s) { auto & fcache = m_failure_cache[static_cast(m)]; - if (t.hash() <= s.hash()) + if (hash(t) <= hash(s)) fcache.insert(mk_pair(t, s)); else fcache.insert(mk_pair(s, t)); diff --git a/src/library/deep_copy.cpp b/src/library/deep_copy.cpp index ab62c6e186..23f7545d85 100644 --- a/src/library/deep_copy.cpp +++ b/src/library/deep_copy.cpp @@ -11,19 +11,19 @@ Author: Leonardo de Moura namespace lean { expr copy(expr const & a) { switch (a.kind()) { - case expr_kind::Lit: return mk_lit(lit_value(a)); - case expr_kind::MData: return mk_mdata(mdata_data(a), mdata_expr(a)); - case expr_kind::Proj: return mk_proj(proj_idx(a), proj_expr(a)); - case expr_kind::BVar: return mk_var(var_idx(a)); - case expr_kind::FVar: return mk_local(mlocal_name(a), mlocal_pp_name(a), mlocal_type(a), local_info(a)); - case expr_kind::Constant: return mk_constant(const_name(a), const_levels(a)); - case expr_kind::Sort: return mk_sort(sort_level(a)); - case expr_kind::App: return mk_app(app_fn(a), app_arg(a)); - case expr_kind::Lambda: return mk_lambda(binding_name(a), binding_domain(a), binding_body(a), binding_info(a)); - case expr_kind::Pi: return mk_pi(binding_name(a), binding_domain(a), binding_body(a), binding_info(a)); - case expr_kind::MVar: return mk_metavar(mlocal_name(a), mlocal_pp_name(a), mlocal_type(a)); - case expr_kind::Let: return mk_let(let_name(a), let_type(a), let_value(a), let_body(a)); - case expr_kind::Quote: return mk_quote(quote_is_reflected(a), quote_value(a)); + case expr_kind::Lit: return mk_lit(lit_value(a)); + case expr_kind::MData: return mk_mdata(mdata_data(a), mdata_expr(a)); + case expr_kind::Proj: return mk_proj(proj_idx(a), proj_expr(a)); + case expr_kind::BVar: return mk_bvar(bvar_idx(a)); + case expr_kind::FVar: return mk_local(mlocal_name(a), mlocal_pp_name(a), mlocal_type(a), local_info(a)); + case expr_kind::Const: return mk_const(const_name(a), const_levels(a)); + case expr_kind::Sort: return mk_sort(sort_level(a)); + case expr_kind::App: return mk_app(app_fn(a), app_arg(a)); + case expr_kind::Lambda: return mk_lambda(binding_name(a), binding_domain(a), binding_body(a), binding_info(a)); + case expr_kind::Pi: return mk_pi(binding_name(a), binding_domain(a), binding_body(a), binding_info(a)); + case expr_kind::MVar: return mk_metavar(mlocal_name(a), mlocal_pp_name(a), mlocal_type(a)); + case expr_kind::Let: return mk_let(let_name(a), let_type(a), let_value(a), let_body(a)); + case expr_kind::Quote: return mk_quote(quote_is_reflected(a), quote_value(a)); } lean_unreachable(); // LCOV_EXCL_LINE } diff --git a/src/library/equations_compiler/structural_rec.cpp b/src/library/equations_compiler/structural_rec.cpp index bd5e4ece8c..9e1de26180 100644 --- a/src/library/equations_compiler/structural_rec.cpp +++ b/src/library/equations_compiler/structural_rec.cpp @@ -115,7 +115,7 @@ struct structural_rec_fn { bool check_rhs(expr const & e) { switch (e.kind()) { case expr_kind::BVar: case expr_kind::MVar: - case expr_kind::FVar: case expr_kind::Constant: + case expr_kind::FVar: case expr_kind::Const: case expr_kind::Sort: case expr_kind::Lit: return true; case expr_kind::App: { diff --git a/src/library/expr_lt.cpp b/src/library/expr_lt.cpp index 1a50121ca8..1c94e65ad6 100644 --- a/src/library/expr_lt.cpp +++ b/src/library/expr_lt.cpp @@ -16,15 +16,15 @@ bool is_lt(expr const & a, expr const & b, bool use_hash, local_context const * if (wa > wb) return false; if (a.kind() != b.kind()) return a.kind() < b.kind(); if (use_hash) { - if (a.hash() < b.hash()) return true; - if (a.hash() > b.hash()) return false; + if (hash(a) < hash(b)) return true; + if (hash(a) > hash(b)) return false; } if (a == b) return false; switch (a.kind()) { case expr_kind::Lit: return lit_value(a) < lit_value(b); case expr_kind::BVar: - return var_idx(a) < var_idx(b); + return bvar_idx(a) < bvar_idx(b); case expr_kind::MData: if (mdata_expr(a) != mdata_expr(b)) return is_lt(mdata_expr(a), mdata_expr(b), use_hash, lctx); @@ -35,7 +35,7 @@ bool is_lt(expr const & a, expr const & b, bool use_hash, local_context const * return is_lt(proj_expr(a), proj_expr(b), use_hash, lctx); else return proj_idx(a) < proj_idx(b); - case expr_kind::Constant: + case expr_kind::Const: if (const_name(a) != const_name(b)) return const_name(a) < const_name(b); else @@ -135,7 +135,7 @@ bool is_lt_no_level_params(expr const & a, expr const & b) { case expr_kind::Lit: return lit_value(a) < lit_value(b); case expr_kind::BVar: - return var_idx(a) < var_idx(b); + return bvar_idx(a) < bvar_idx(b); case expr_kind::MData: if (mdata_expr(a) != mdata_expr(b)) return is_lt_no_level_params(mdata_expr(a), mdata_expr(b)); @@ -146,7 +146,7 @@ bool is_lt_no_level_params(expr const & a, expr const & b) { return is_lt_no_level_params(proj_expr(a), proj_expr(b)); else return proj_idx(a) < proj_idx(b); - case expr_kind::Constant: + case expr_kind::Const: if (const_name(a) != const_name(b)) return const_name(a) < const_name(b); else diff --git a/src/library/expr_unsigned_map.h b/src/library/expr_unsigned_map.h index b022b8c8db..402043b67f 100644 --- a/src/library/expr_unsigned_map.h +++ b/src/library/expr_unsigned_map.h @@ -15,7 +15,7 @@ struct expr_unsigned { unsigned m_nargs; unsigned m_hash; expr_unsigned(expr const & fn, unsigned nargs): - m_expr(fn), m_nargs(nargs), m_hash(hash(m_expr.hash(), m_nargs)) {} + m_expr(fn), m_nargs(nargs), m_hash(hash(hash(m_expr), m_nargs)) {} }; struct expr_unsigned_hash_fn { diff --git a/src/library/head_map.cpp b/src/library/head_map.cpp index 8eed9fa288..546aa914e3 100644 --- a/src/library/head_map.cpp +++ b/src/library/head_map.cpp @@ -26,14 +26,14 @@ head_index::head_index(expr const & e) { } int head_index::cmp::operator()(head_index const & i1, head_index const & i2) const { - if (i1.m_kind != i2.m_kind || (i1.m_kind != expr_kind::Constant && i1.m_kind != expr_kind::FVar)) + if (i1.m_kind != i2.m_kind || (i1.m_kind != expr_kind::Const && i1.m_kind != expr_kind::FVar)) return static_cast(i1.m_kind) - static_cast(i2.m_kind); else return quick_cmp(i1.m_name, i2.m_name); } std::ostream & operator<<(std::ostream & out, head_index const & head_idx) { - if (head_idx.m_kind == expr_kind::Constant || head_idx.m_kind == expr_kind::FVar) + if (head_idx.m_kind == expr_kind::Const || head_idx.m_kind == expr_kind::FVar) out << head_idx.m_name; else out << head_idx.m_kind; diff --git a/src/library/head_map.h b/src/library/head_map.h index c5e2723cd0..76399e918f 100644 --- a/src/library/head_map.h +++ b/src/library/head_map.h @@ -15,7 +15,7 @@ struct head_index { expr_kind m_kind; name m_name; explicit head_index(expr_kind k = expr_kind::BVar):m_kind(k) {} - explicit head_index(name const & c):m_kind(expr_kind::Constant), m_name(c) {} + explicit head_index(name const & c):m_kind(expr_kind::Const), m_name(c) {} head_index(expr const & e); expr_kind kind() const { return m_kind; } name const & get_name() const { return m_name; } diff --git a/src/library/inductive_compiler/nested.cpp b/src/library/inductive_compiler/nested.cpp index dd6ce04b93..fc3dcfc66f 100644 --- a/src/library/inductive_compiler/nested.cpp +++ b/src/library/inductive_compiler/nested.cpp @@ -544,7 +544,7 @@ class add_nested_inductive_decl_fn { expr new_body = abstract(pack_nested_occs(instantiate(binding_body(e), l)), l); return update_binding(e, new_dom, new_body); } - case expr_kind::Constant: + case expr_kind::Const: case expr_kind::App: { buffer args; @@ -601,7 +601,7 @@ class add_nested_inductive_decl_fn { expr new_body = abstract(unpack_nested_occs(instantiate(binding_body(e), l)), l); return update_binding(e, new_dom, new_body); } - case expr_kind::Constant: + case expr_kind::Const: case expr_kind::App: { buffer args; diff --git a/src/library/kernel_serializer.cpp b/src/library/kernel_serializer.cpp index 8924f4e04a..d2b83c160f 100644 --- a/src/library/kernel_serializer.cpp +++ b/src/library/kernel_serializer.cpp @@ -5,182 +5,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#include "util/object_serializer.h" #include "kernel/expr.h" #include "kernel/declaration.h" #include "library/kernel_serializer.h" // Procedures for serializing and deserializing kernel objects (levels, exprs, declarations) namespace lean { -// Expression serialization -static name * g_binder_name = nullptr; - -class expr_serializer : public object_serializer { - typedef object_serializer super; - unsigned m_next_id; - - void write_binder_name(serializer & s, name const & a) { - // make sure binding names are atomic string - if (!a.is_atomic() || a.is_numeral()) { - s << g_binder_name->append_after(m_next_id); - m_next_id++; - } else { - s << a; - } - } - - void write_core(expr const & a) { - auto k = a.kind(); - super::write_core(a, static_cast(k), [&]() { - serializer & s = get_owner(); - switch (k) { - case expr_kind::BVar: - s << var_idx(a); - break; - case expr_kind::Lit: - s << lit_value(a); - break; - case expr_kind::MData: - s << mdata_data(a); - write_core(mdata_expr(a)); - break; - case expr_kind::Proj: - s << proj_idx(a); - write_core(proj_expr(a)); - break; - case expr_kind::Constant: - lean_assert(!const_name(a).is_anonymous()); - s << const_name(a) << const_levels(a); - break; - case expr_kind::Sort: - s << sort_level(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: - lean_assert(!binding_name(a).is_anonymous()); - write_binder_name(s, binding_name(a)); - s.write_char(static_cast(binding_info(a))); - write_core(binding_domain(a)); write_core(binding_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::MVar: - lean_assert(!mlocal_name(a).is_anonymous()); - s << mlocal_name(a) << mlocal_pp_name(a); write_core(mlocal_type(a)); - break; - case expr_kind::FVar: - lean_assert(!mlocal_name(a).is_anonymous()); - lean_assert(!mlocal_pp_name(a).is_anonymous()); - s << mlocal_name(a) << mlocal_pp_name(a); - s.write_char(static_cast(local_info(a))); write_core(mlocal_type(a)); - break; - - case expr_kind::Quote: - s << quote_is_reflected(a); - write_core(quote_value(a)); - break; - } - }); - } -public: - expr_serializer() { m_next_id = 0; } - void write(expr const & a) { - write_core(a); - } -}; - -class expr_deserializer : public object_deserializer { - typedef object_deserializer super; -public: - expr read_binding(expr_kind k) { - deserializer & d = get_owner(); - name n = read_name(d); - binder_info i = static_cast(d.read_char()); - expr t = read(); - return mk_binding(k, n, t, read(), i); - } - - expr read() { - return super::read_core([&](char c) { - deserializer & d = get_owner(); - auto k = static_cast(c); - switch (k) { - case expr_kind::BVar: - return mk_var(d.read_unsigned()); - case expr_kind::Lit: - return mk_lit(read_literal(d)); - case expr_kind::MData: { - kvmap m = read_list_ref>(d); - return mk_mdata(m, read()); - } - case expr_kind::Proj: { - nat idx = read_nat(d); - return mk_proj(idx, read()); - } - case expr_kind::Constant: { - auto n = read_name(d); - return mk_constant(n, read_levels(d)); - } - case expr_kind::Sort: - return mk_sort(read_level(d)); - case expr_kind::App: { - expr f = read(); - return mk_app(f, read()); - } - case expr_kind::Lambda: case expr_kind::Pi: - return read_binding(k); - case expr_kind::Let: { - name n = read_name(d); - expr t = read(); - expr v = read(); - return mk_let(n, t, v, read()); - } - case expr_kind::MVar: { - name n = read_name(d); - name pp_n = read_name(d); - return mk_metavar(n, pp_n, read()); - } - case expr_kind::FVar: { - name n = read_name(d); - name pp_n = read_name(d); - binder_info bi = static_cast(d.read_char()); - return mk_local(n, pp_n, read(), bi); - } - - case expr_kind::Quote: { - bool r = d.read_bool(); - expr v = read(); - return mk_quote(r, v); - } - } - throw corrupted_stream_exception(); // LCOV_EXCL_LINE - }); - } -}; - -struct expr_sd { - unsigned m_s_extid; - unsigned m_d_extid; - expr_sd() { - m_s_extid = serializer::register_extension([](){ return std::unique_ptr(new expr_serializer()); }); - m_d_extid = deserializer::register_extension([](){ return std::unique_ptr(new expr_deserializer()); }); - } -}; -static expr_sd * g_expr_sd = nullptr; - -serializer & operator<<(serializer & s, expr const & n) { - s.get_extension(g_expr_sd->m_s_extid).write(n); - return s; -} - -expr read_expr(deserializer & d) { - return d.get_extension(g_expr_sd->m_d_extid).read(); -} - serializer & operator<<(serializer & s, reducibility_hints const & h) { s << static_cast(h.get_kind()); if (h.is_regular()) @@ -310,12 +140,8 @@ inductive::certified_inductive_decl read_certified_inductive_decl(deserializer & } void initialize_kernel_serializer() { - g_binder_name = new name("a"); - g_expr_sd = new expr_sd(); } void finalize_kernel_serializer() { - delete g_expr_sd; - delete g_binder_name; } } diff --git a/src/library/kernel_serializer.h b/src/library/kernel_serializer.h index 972c8783e5..223468ed13 100644 --- a/src/library/kernel_serializer.h +++ b/src/library/kernel_serializer.h @@ -11,21 +11,6 @@ Author: Leonardo de Moura #include "kernel/inductive/inductive.h" namespace lean { -serializer & operator<<(serializer & s, level const & l); -level read_level(deserializer & d); -inline deserializer & operator>>(deserializer & d, level & l) { l = read_level(d); return d; } - -serializer & operator<<(serializer & s, levels const & ls); -levels read_levels(deserializer & d); - -serializer & operator<<(serializer & s, level_param_names const & ps); -level_param_names read_level_params(deserializer & d); -inline deserializer & operator>>(deserializer & d, level_param_names & ps) { ps = read_level_params(d); return d; } - -serializer & operator<<(serializer & s, expr const & e); -expr read_expr(deserializer & d); -inline deserializer & operator>>(deserializer & d, expr & e) { e = read_expr(d); return d; } - serializer & operator<<(serializer & s, declaration const & d); declaration read_declaration(deserializer & d); inline deserializer & operator>>(deserializer & d, declaration & decl) { decl = read_declaration(d); return d; } diff --git a/src/library/locals.cpp b/src/library/locals.cpp index a32e006980..4ea62cb711 100644 --- a/src/library/locals.cpp +++ b/src/library/locals.cpp @@ -72,7 +72,7 @@ void collect_locals(expr const & e, collected_locals & ls, bool restricted) { return; visited.insert(e); switch (e.kind()) { - case expr_kind::BVar: case expr_kind::Constant: + case expr_kind::BVar: case expr_kind::Const: case expr_kind::Sort: case expr_kind::Lit: break; // do nothing case expr_kind::MData: diff --git a/src/library/max_sharing.cpp b/src/library/max_sharing.cpp index 2ec2a48b16..9650052818 100644 --- a/src/library/max_sharing.cpp +++ b/src/library/max_sharing.cpp @@ -56,7 +56,7 @@ struct max_sharing_fn::imp { case expr_kind::BVar: case expr_kind::Lit: res = a; break; - case expr_kind::Constant: + case expr_kind::Const: res = update_constant(a, map(const_levels(a), [&](level const & l) { return apply(l); })); break; case expr_kind::Sort: diff --git a/src/library/noncomputable.cpp b/src/library/noncomputable.cpp index ea562083db..44245d4d23 100644 --- a/src/library/noncomputable.cpp +++ b/src/library/noncomputable.cpp @@ -188,19 +188,19 @@ struct get_noncomputable_reason_fn { void visit(expr const & e) { switch (e.kind()) { - case expr_kind::Sort: return; - case expr_kind::Lit: return; - case expr_kind::Constant: visit_constant(e); return; - case expr_kind::BVar: lean_unreachable(); - case expr_kind::MVar: lean_unreachable(); - case expr_kind::FVar: return; - case expr_kind::App: visit_app(e); return; - case expr_kind::Lambda: visit_binding(e); return; - case expr_kind::Pi: visit_binding(e); return; - case expr_kind::Let: visit_let(e); return; - case expr_kind::MData: visit_mdata(e); return; - case expr_kind::Proj: visit(proj_expr(e)); return; - case expr_kind::Quote: return; + case expr_kind::Sort: return; + case expr_kind::Lit: return; + case expr_kind::Const: visit_constant(e); return; + case expr_kind::BVar: lean_unreachable(); + case expr_kind::MVar: lean_unreachable(); + case expr_kind::FVar: return; + case expr_kind::App: visit_app(e); return; + case expr_kind::Lambda: visit_binding(e); return; + case expr_kind::Pi: visit_binding(e); return; + case expr_kind::Let: visit_let(e); return; + case expr_kind::MData: visit_mdata(e); return; + case expr_kind::Proj: visit(proj_expr(e)); return; + case expr_kind::Quote: return; } } diff --git a/src/library/normalize.cpp b/src/library/normalize.cpp index 88fc7f8c9f..247bf430d1 100644 --- a/src/library/normalize.cpp +++ b/src/library/normalize.cpp @@ -116,8 +116,8 @@ class normalize_fn { return e; e = m_ctx.whnf(e); switch (e.kind()) { - case expr_kind::BVar: case expr_kind::Constant: case expr_kind::Sort: - case expr_kind::MVar: case expr_kind::FVar: case expr_kind::Lit: + case expr_kind::BVar: case expr_kind::Const: case expr_kind::Sort: + case expr_kind::MVar: case expr_kind::FVar: case expr_kind::Lit: return e; case expr_kind::MData: lean_unreachable(); diff --git a/src/library/pos_info_provider.cpp b/src/library/pos_info_provider.cpp index f196355524..884f5ff432 100644 --- a/src/library/pos_info_provider.cpp +++ b/src/library/pos_info_provider.cpp @@ -74,7 +74,7 @@ void finalize_pos_info_provider() { struct replace_cache2 { struct entry { - expr_cell * m_cell; + object * m_cell; unsigned m_offset; expr m_result; entry():m_cell(nullptr) {} @@ -85,7 +85,7 @@ struct replace_cache2 { replace_cache2(unsigned c):m_capacity(c), m_cache(c) {} expr * find(expr const & e, unsigned offset) { - unsigned i = hash(e.hash(), offset) % m_capacity; + unsigned i = hash(hash(e), offset) % m_capacity; if (m_cache[i].m_cell == e.raw() && m_cache[i].m_offset == offset) return &m_cache[i].m_result; else @@ -93,7 +93,7 @@ struct replace_cache2 { } void insert(expr const & e, unsigned offset, expr const & v) { - unsigned i = hash(e.hash(), offset) % m_capacity; + unsigned i = hash(hash(e), offset) % m_capacity; if (m_cache[i].m_cell == nullptr) m_used.push_back(i); m_cache[i].m_cell = e.raw(); @@ -136,10 +136,10 @@ class replace_rec_fn2 { return save_result(e, offset, *r, shared); } else { switch (e.kind()) { - case expr_kind::Constant: case expr_kind::Sort: case expr_kind::BVar: + case expr_kind::Const: case expr_kind::Sort: case expr_kind::BVar: case expr_kind::Lit: return save_result(e, offset, e, shared); - case expr_kind::MVar: case expr_kind::FVar: { + case expr_kind::MVar: case expr_kind::FVar: { expr new_t = apply(mlocal_type(e), offset); return save_result(e, offset, copy_pos(e, update_mlocal(e, new_t)), shared); } @@ -193,8 +193,8 @@ struct instantiate_easy_fn2 { optional operator()(expr const & a, bool app) const { if (!has_loose_bvars(a)) return some_expr(a); - if (is_var(a) && var_idx(a) < n) - return some_expr(subst[rev ? n - var_idx(a) - 1 : var_idx(a)]); + if (is_bvar(a) && bvar_idx(a) < n) + return some_expr(subst[rev ? n - bvar_idx(a).get_small_value() - 1 : bvar_idx(a).get_small_value()]); if (app && is_app(a)) if (auto new_a = operator()(app_arg(a), false)) if (auto new_f = operator()(app_fn(a), true)) @@ -222,13 +222,13 @@ expr instantiate_propagating_pos(expr const & a, unsigned s, unsigned n, expr co return some_expr(m); // expression m does not contain free variables with idx >= s1 #endif if (is_var(m)) { - unsigned vidx = var_idx(m); + nat const & vidx = bvar_idx(m); if (vidx >= s1) { unsigned h = s1 + n; if (h < s1 /* overflow, h is bigger than any vidx */ || vidx < h) { - return some_expr(lift_loose_bvars(subst[vidx - s1], offset)); + return some_expr(lift_loose_bvars(subst[vidx.get_small_value() - s1], offset)); } else { - return some_expr(mk_var(vidx - n)); + return some_expr(mk_bvar(vidx - nat(n))); } } } @@ -257,7 +257,7 @@ expr abstract_propagating_pos(expr const & e, unsigned n, expr const * subst) { while (i > 0) { --i; if (mlocal_name(subst[i]) == mlocal_name(m)) - return some_expr(mk_var(offset + n - i - 1)); + return some_expr(mk_bvar(offset + n - i - 1)); } return none_expr(); } diff --git a/src/library/print.cpp b/src/library/print.cpp index 112ada62af..795a717041 100644 --- a/src/library/print.cpp +++ b/src/library/print.cpp @@ -223,9 +223,9 @@ struct print_expr_fn { print(proj_expr(a)); out() << "." << proj_idx(a).to_mpz(); break; case expr_kind::BVar: - out() << "#" << var_idx(a); + out() << "#" << bvar_idx(a); break; - case expr_kind::Constant: + case expr_kind::Const: print_const(a); break; case expr_kind::App: diff --git a/src/library/replace_visitor.cpp b/src/library/replace_visitor.cpp index 7c9a90e4d3..03790b1de9 100644 --- a/src/library/replace_visitor.cpp +++ b/src/library/replace_visitor.cpp @@ -67,18 +67,18 @@ expr replace_visitor::visit(expr const & e) { } switch (e.kind()) { - case expr_kind::Lit: return save_result(e, visit_lit(e), shared); - case expr_kind::MData: return save_result(e, visit_mdata(e), shared); - case expr_kind::Proj: return save_result(e, visit_proj(e), shared); - case expr_kind::Sort: return save_result(e, visit_sort(e), shared); - case expr_kind::Constant: return save_result(e, visit_constant(e), shared); - case expr_kind::BVar: return save_result(e, visit_var(e), shared); - case expr_kind::MVar: return save_result(e, visit_meta(e), shared); - case expr_kind::FVar: return save_result(e, visit_local(e), shared); - case expr_kind::App: return save_result(e, visit_app(e), shared); - case expr_kind::Lambda: return save_result(e, visit_lambda(e), shared); - case expr_kind::Pi: return save_result(e, visit_pi(e), shared); - case expr_kind::Let: return save_result(e, visit_let(e), shared); + case expr_kind::Lit: return save_result(e, visit_lit(e), shared); + case expr_kind::MData: return save_result(e, visit_mdata(e), shared); + case expr_kind::Proj: return save_result(e, visit_proj(e), shared); + case expr_kind::Sort: return save_result(e, visit_sort(e), shared); + case expr_kind::Const: return save_result(e, visit_constant(e), shared); + case expr_kind::BVar: return save_result(e, visit_var(e), shared); + case expr_kind::MVar: return save_result(e, visit_meta(e), shared); + case expr_kind::FVar: return save_result(e, visit_local(e), shared); + case expr_kind::App: return save_result(e, visit_app(e), shared); + case expr_kind::Lambda: return save_result(e, visit_lambda(e), shared); + case expr_kind::Pi: return save_result(e, visit_pi(e), shared); + case expr_kind::Let: return save_result(e, visit_let(e), shared); case expr_kind::Quote: return save_result(e, visit_quote(e), shared); } diff --git a/src/library/tactic/dsimplify.cpp b/src/library/tactic/dsimplify.cpp index 4b031e5138..1d456d6013 100644 --- a/src/library/tactic/dsimplify.cpp +++ b/src/library/tactic/dsimplify.cpp @@ -250,7 +250,7 @@ expr dsimplify_core_fn::visit(expr const & e) { case expr_kind::FVar: case expr_kind::Sort: case expr_kind::Lit: - case expr_kind::Constant: + case expr_kind::Const: new_e = curr_e; break; case expr_kind::MData: diff --git a/src/library/tactic/kabstract.cpp b/src/library/tactic/kabstract.cpp index d14c1b6d2c..5d56324da3 100644 --- a/src/library/tactic/kabstract.cpp +++ b/src/library/tactic/kabstract.cpp @@ -34,7 +34,7 @@ expr kabstract(type_context_old & ctx, expr const & e, expr const & t, occurrenc lean_trace("kabstract", scope_trace_env _(ctx.env(), ctx); tout() << "found target:\n" << s << "\n";); i++; - return some_expr(mk_var(offset)); + return some_expr(mk_bvar(offset)); } else { i++; } diff --git a/src/library/tactic/simp_lemmas.cpp b/src/library/tactic/simp_lemmas.cpp index da17346b4c..79c0d0f8a8 100644 --- a/src/library/tactic/simp_lemmas.cpp +++ b/src/library/tactic/simp_lemmas.cpp @@ -629,17 +629,17 @@ static bool is_permutation(expr const & lhs, expr const & rhs, unsigned offset, if (lhs.kind() != rhs.kind()) return false; switch (lhs.kind()) { - case expr_kind::Constant: case expr_kind::Sort: - case expr_kind::MVar: case expr_kind::FVar: case expr_kind::Lit: + case expr_kind::Const: case expr_kind::Sort: + case expr_kind::MVar: case expr_kind::FVar: case expr_kind::Lit: return lhs == rhs; case expr_kind::BVar: - if (var_idx(lhs) < offset) { + if (bvar_idx(lhs) < offset) { return lhs == rhs; // locally bound variable - } else if (var_idx(lhs) - offset < p.size()) { - if (p[var_idx(lhs) - offset]) { - return *(p[var_idx(lhs) - offset]) == var_idx(rhs) - offset; + } else if (bvar_idx(lhs) - nat(offset) < p.size()) { + if (p[bvar_idx(lhs).get_small_value() - offset]) { + return *(p[bvar_idx(lhs).get_small_value() - offset]) == bvar_idx(rhs).get_small_value() - offset; } else { - p[var_idx(lhs) - offset] = var_idx(rhs) - offset; + p[bvar_idx(lhs).get_small_value() - offset] = bvar_idx(rhs).get_small_value() - offset; return true; } } else { diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp index 9b3ef2451b..e97fcd2910 100644 --- a/src/library/tactic/simplify.cpp +++ b/src/library/tactic/simplify.cpp @@ -647,7 +647,7 @@ simp_result simplify_core_fn::visit(expr const & e, optional const & paren case expr_kind::FVar: case expr_kind::Sort: case expr_kind::Lit: - case expr_kind::Constant: + case expr_kind::Const: new_result = curr_result; break; case expr_kind::MVar: diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 5e713ca9a1..c0b7e965d7 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -770,9 +770,9 @@ optional type_context_old::reduce_recursor(expr const & e) { expr type_context_old::whnf_core(expr const & e0, bool proj_reduce) { expr e = e0; while (true) { switch (e.kind()) { - case expr_kind::BVar: case expr_kind::Sort: - case expr_kind::Pi: case expr_kind::Lambda: - case expr_kind::Constant: case expr_kind::Lit: + case expr_kind::BVar: case expr_kind::Sort: + case expr_kind::Pi: case expr_kind::Lambda: + case expr_kind::Const: case expr_kind::Lit: /* Remark: we do not unfold Constants eagerly in this method */ return e; case expr_kind::FVar: @@ -1011,7 +1011,7 @@ expr type_context_old::infer_core(expr const & e) { case expr_kind::Sort: r = mk_sort(mk_succ(sort_level(e))); break; - case expr_kind::Constant: + case expr_kind::Const: r = infer_constant(e); break; case expr_kind::Lambda: @@ -2452,7 +2452,7 @@ static optional is_eta_expanded(expr const & e) { if (!is_app(it)) return none_expr(); expr const & a = app_arg(it); - if (!is_var(a) || var_idx(a) != i) + if (!is_bvar(a) || bvar_idx(a) != i) return none_expr(); it = app_fn(it); } @@ -2704,9 +2704,9 @@ lbool type_context_old::quick_is_def_eq(expr const & e1, expr const & e2) { return to_lbool(is_def_eq_core(mdata_expr(e1), mdata_expr(e2))); case expr_kind::Lit: return to_lbool(lit_value(e1) == lit_value(e2)); - case expr_kind::MVar: case expr_kind::BVar: - case expr_kind::FVar: case expr_kind::App: - case expr_kind::Constant: case expr_kind::Proj: + case expr_kind::MVar: case expr_kind::BVar: + case expr_kind::FVar: case expr_kind::App: + case expr_kind::Const: case expr_kind::Proj: case expr_kind::Let: // We do not handle these cases in this method. break; @@ -3323,7 +3323,7 @@ lbool type_context_old::is_quick_class(expr const & type, name & result) { case expr_kind::MData: it = &mdata_expr(*it); break; - case expr_kind::Constant: + case expr_kind::Const: if (auto r = constant_is_class(*it)) { result = *r; return l_true; diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp index acb4c5872c..1784b5ce39 100644 --- a/src/library/vm/vm_expr.cpp +++ b/src/library/vm/vm_expr.cpp @@ -74,7 +74,7 @@ vm_obj to_obj(binder_info bi) { // introduction rules have the suffix for the same reason. vm_obj expr_bvar_intro(vm_obj const & n) { - return to_obj(mk_var(to_unsigned(n))); + return to_obj(mk_bvar(nat(vm_nat_to_mpz1(n)))); } vm_obj expr_sort_intro(vm_obj const & l) { @@ -148,12 +148,12 @@ unsigned expr_cases_on(vm_obj const & o, buffer & data) { expr const & e = to_expr(o); switch (e.kind()) { case expr_kind::BVar: - data.push_back(mk_vm_nat(var_idx(e))); + data.push_back(mk_vm_nat(bvar_idx(e).to_mpz())); break; case expr_kind::Sort: data.push_back(to_obj(sort_level(e))); break; - case expr_kind::Constant: + case expr_kind::Const: data.push_back(to_obj(const_name(e))); data.push_back(to_obj(const_levels(e))); break; @@ -248,7 +248,7 @@ vm_obj expr_has_bvar_idx(vm_obj const & e, vm_obj const & u) { } vm_obj expr_hash(vm_obj const & e) { - unsigned r = to_expr(e).hash() % LEAN_VM_MAX_SMALL_NAT; + unsigned r = hash(to_expr(e)) % LEAN_VM_MAX_SMALL_NAT; return mk_vm_simple(r); // make sure it is a simple value } diff --git a/src/runtime/object.h b/src/runtime/object.h index b21e013660..b00c14c2a8 100644 --- a/src/runtime/object.h +++ b/src/runtime/object.h @@ -13,6 +13,7 @@ Author: Leonardo de Moura #include "runtime/compiler_hints.h" #include "runtime/mpz.h" #include "runtime/int64.h" +#include "runtime/thread.h" namespace lean { inline void * alloca(size_t s) { diff --git a/src/runtime/serializer.cpp b/src/runtime/serializer.cpp index b1ef5c651b..08ef51cec2 100644 --- a/src/runtime/serializer.cpp +++ b/src/runtime/serializer.cpp @@ -17,28 +17,24 @@ Author: Leonardo de Moura namespace lean { void initialize_serializer() { - serializer::initialize(); - deserializer::initialize(); } void finalize_serializer() { - deserializer::finalize(); - serializer::finalize(); } -serializer_core::~serializer_core() { +serializer::~serializer() { for (std::pair const & it : m_obj_table) { dec_ref(it.first); } } -void serializer_core::write_unsigned_short(unsigned short i) { +void serializer::write_unsigned_short(unsigned short i) { static_assert(sizeof(i) == 2, "unexpected unsigned short size"); m_out.put((i >> 8) & 0xff); m_out.put(i & 0xff); } -void serializer_core::write_unsigned(unsigned i) { +void serializer::write_unsigned(unsigned i) { static_assert(sizeof(i) == 4, "unexpected unsigned size"); if (i < 255) { m_out.put(i & 0xff); @@ -51,13 +47,13 @@ void serializer_core::write_unsigned(unsigned i) { } } -void serializer_core::write_uint64(uint64 i) { +void serializer::write_uint64(uint64 i) { static_assert(sizeof(i) == 8, "unexpected uint64 size"); write_unsigned((i >> 32) & 0xffffffff); write_unsigned(i & 0xffffffff); } -void serializer_core::write_size_t(size_t i) { +void serializer::write_size_t(size_t i) { if (sizeof(i) == 8) { write_uint64(static_cast(i)); } else { @@ -66,17 +62,17 @@ void serializer_core::write_size_t(size_t i) { } } -void serializer_core::write_int(int i) { +void serializer::write_int(int i) { static_assert(sizeof(i) == 4, "unexpected int size"); write_unsigned(i); } -void serializer_core::write_blob(std::string const & s) { +void serializer::write_blob(std::string const & s) { write_unsigned(s.size()); m_out.write(&s[0], s.size()); } -void serializer_core::write_constructor(object * o) { +void serializer::write_constructor(object * o) { lean_assert(is_cnstr(o)); unsigned num_objs = cnstr_num_objs(o); unsigned scalar_sz = cnstr_scalar_size(o); @@ -93,7 +89,7 @@ void serializer_core::write_constructor(object * o) { m_out.put(*sit); } -void serializer_core::write_closure(object *) { // NOLINT +void serializer::write_closure(object *) { // NOLINT /* TODO(Leo): we need a table from function pointer to unique name id. For serializing bytecode, we will need to retrieve the unique name id too. @@ -104,7 +100,7 @@ void serializer_core::write_closure(object *) { // NOLINT throw exception("serializer for closures has not been implemented yet"); } -void serializer_core::write_array(object * o) { +void serializer::write_array(object * o) { lean_assert(is_array(o)); size_t sz = sarray_size(o); write_size_t(sz); @@ -114,7 +110,7 @@ void serializer_core::write_array(object * o) { write_object(*it); } -void serializer_core::write_scalar_array(object * o) { +void serializer::write_scalar_array(object * o) { lean_assert(is_sarray(o)); unsigned esz = sarray_elem_size(o); size_t sz = sarray_size(o); @@ -127,7 +123,7 @@ void serializer_core::write_scalar_array(object * o) { m_out.put(*it); } -void serializer_core::write_string_object(object * o) { +void serializer::write_string_object(object * o) { size_t sz = string_size(o); size_t len = string_len(o); write_size_t(sz); @@ -138,20 +134,20 @@ void serializer_core::write_string_object(object * o) { m_out.put(*it); } -void serializer_core::write_mpz(mpz const & n) { +void serializer::write_mpz(mpz const & n) { std::ostringstream out; out << n; write_string(out.str()); } -void serializer_core::write_external(object *) { // NOLINT +void serializer::write_external(object *) { // NOLINT /* TODO(Leo): we need support for registering serializers/deserializers for external objects. */ throw exception("serializer for external objects has not been implemented yet"); } -void serializer_core::write_object(object * o) { +void serializer::write_object(object * o) { if (is_scalar(o)) { m_out.put(0); write_unsigned(unbox(o)); @@ -182,7 +178,7 @@ void serializer_core::write_object(object * o) { corrupted_stream_exception::corrupted_stream_exception(): exception("corrupted binary file") {} -void serializer_core::write_double(double d) { +void serializer::write_double(double d) { std::ostringstream out; // TODO(Leo): the following code may miss precision. // We should use std::ios::hexfloat, but it is not supported by @@ -193,12 +189,12 @@ void serializer_core::write_double(double d) { write_string(out.str()); } -deserializer_core::~deserializer_core() { +deserializer::~deserializer() { for (object * o : m_objs) dec_ref(o); } -std::string deserializer_core::read_string() { +std::string deserializer::read_string() { std::string r; while (true) { char c = m_in.get(); @@ -211,7 +207,7 @@ std::string deserializer_core::read_string() { return r; } -unsigned deserializer_core::read_unsigned_ext() { +unsigned deserializer::read_unsigned_ext() { unsigned r; static_assert(sizeof(r) == 4, "unexpected unsigned size"); r = static_cast(m_in.get()) << 24; @@ -221,7 +217,7 @@ unsigned deserializer_core::read_unsigned_ext() { return r; } -unsigned short deserializer_core::read_unsigned_short() { +unsigned short deserializer::read_unsigned_short() { unsigned short r; static_assert(sizeof(r) == 2, "unexpected unsigned short size"); r = static_cast(m_in.get()) << 8; @@ -229,7 +225,7 @@ unsigned short deserializer_core::read_unsigned_short() { return r; } -uint64 deserializer_core::read_uint64() { +uint64 deserializer::read_uint64() { uint64 r; static_assert(sizeof(r) == 8, "unexpected uint64 size"); r = static_cast(read_unsigned()) << 32; @@ -237,7 +233,7 @@ uint64 deserializer_core::read_uint64() { return r; } -size_t deserializer_core::read_size_t() { +size_t deserializer::read_size_t() { if (sizeof(size_t) == 8) { return static_cast(read_uint64()); } else { @@ -246,7 +242,7 @@ size_t deserializer_core::read_size_t() { } } -double deserializer_core::read_double() { +double deserializer::read_double() { // TODO(Leo): use std::hexfloat as soon as it is supported by g++ std::istringstream in(read_string()); double r; @@ -254,18 +250,18 @@ double deserializer_core::read_double() { return r; } -mpz deserializer_core::read_mpz() { +mpz deserializer::read_mpz() { return mpz(read_string().c_str()); } -std::string deserializer_core::read_blob() { +std::string deserializer::read_blob() { unsigned sz = read_unsigned(); std::string s(sz, '\0'); m_in.read(&s[0], sz); return s; } -object * deserializer_core::read_constructor() { +object * deserializer::read_constructor() { unsigned tag = read_unsigned_short(); unsigned num_objs = read_unsigned_short(); unsigned scalar_sz = read_unsigned_short(); @@ -282,11 +278,11 @@ object * deserializer_core::read_constructor() { return r; } -object * deserializer_core::read_closure() { +object * deserializer::read_closure() { throw exception("serializer for closures has not been implemented yet"); } -object * deserializer_core::read_array() { +object * deserializer::read_array() { size_t sz = read_size_t(); object * r = alloc_array(sz, sz); for (size_t i = 0; i < sz; i++) { @@ -297,7 +293,7 @@ object * deserializer_core::read_array() { return r; } -object * deserializer_core::read_scalar_array() { +object * deserializer::read_scalar_array() { unsigned esz = read_unsigned(); size_t sz = read_size_t(); object * r = alloc_sarray(esz, sz, sz); @@ -308,7 +304,7 @@ object * deserializer_core::read_scalar_array() { return r; } -object * deserializer_core::read_string_object() { +object * deserializer::read_string_object() { size_t sz = read_size_t(); size_t len = read_size_t(); object * r = alloc_string(sz, sz, len); @@ -319,11 +315,11 @@ object * deserializer_core::read_string_object() { return r; } -object * deserializer_core::read_external() { +object * deserializer::read_external() { throw exception("serializer for external objects has not been implemented yet"); } -object * deserializer_core::read_object() { +object * deserializer::read_object() { unsigned c = m_in.get(); if (c == 0) { return box(read_unsigned()); diff --git a/src/runtime/serializer.h b/src/runtime/serializer.h index f116b3687b..544234161b 100644 --- a/src/runtime/serializer.h +++ b/src/runtime/serializer.h @@ -13,17 +13,12 @@ Author: Leonardo de Moura #include #include #include "runtime/int64.h" -#include "runtime/extensible_object.h" #include "runtime/optional.h" namespace lean { struct object; class mpz; -/** \brief Serializer - - TODO(Leo): rename it to `serializer`. We can do it after we remove `extensible_object`. -*/ -class serializer_core { +class serializer { std::ostream & m_out; std::unordered_map, std::equal_to> m_obj_table; void write_constructor(object * o); @@ -33,8 +28,8 @@ class serializer_core { void write_string_object(object * o); void write_external(object * o); public: - serializer_core(std::ostream & out):m_out(out) {} - ~serializer_core(); + serializer(std::ostream & out):m_out(out) {} + ~serializer(); void write_string(char const * str) { m_out.write(str, strlen(str) + 1); } void write_string(std::string const & str) { write_string(str.c_str()); } void write_unsigned_short(unsigned short i); @@ -50,8 +45,6 @@ public: void write_blob(std::string const &); }; -typedef extensible_object serializer; - inline serializer & operator<<(serializer & s, char const * str) { s.write_string(str); return s; } inline serializer & operator<<(serializer & s, std::string const & str) { s.write_string(str); return s; } inline serializer & operator<<(serializer & s, unsigned i) { s.write_unsigned(i); return s; } @@ -62,12 +55,7 @@ inline serializer & operator<<(serializer & s, bool b) { s.write_bool(b); return inline serializer & operator<<(serializer & s, double b) { s.write_double(b); return s; } inline serializer & operator<<(serializer & s, object * o) { s.write_object(o); return s; } -/** - \brief Deserializer. - - TODO(Leo): rename it to `deserializer`. We can do it after we remove `extensible_object`. -*/ -class deserializer_core { +class deserializer { std::istream & m_in; std::vector m_objs; optional m_fname; @@ -79,9 +67,9 @@ class deserializer_core { object * read_string_object(); object * read_external(); public: - deserializer_core(std::istream & in):m_in(in) {} - deserializer_core(std::istream & in, optional const & fname):m_in(in), m_fname(fname) {} - ~deserializer_core(); + deserializer(std::istream & in):m_in(in) {} + deserializer(std::istream & in, optional const & fname):m_in(in), m_fname(fname) {} + ~deserializer(); std::string read_string(); unsigned read_unsigned() { unsigned r = static_cast(m_in.get()); @@ -100,8 +88,6 @@ public: optional get_fname() const { return m_fname; } }; -typedef extensible_object deserializer; - inline deserializer & operator>>(deserializer & d, std::string & str) { str = d.read_string(); return d; } inline deserializer & operator>>(deserializer & d, unsigned & i) { i = d.read_unsigned(); return d; } inline deserializer & operator>>(deserializer & d, uint64 & i) { i = d.read_uint64(); return d; } diff --git a/src/tests/util/serializer.cpp b/src/tests/util/serializer.cpp index fdcf5361a9..ccc2382f7d 100644 --- a/src/tests/util/serializer.cpp +++ b/src/tests/util/serializer.cpp @@ -13,51 +13,11 @@ Author: Leonardo de Moura #include #include "runtime/debug.h" #include "util/test.h" -#include "util/object_serializer.h" #include "util/list.h" #include "util/name.h" #include "util/init_module.h" using namespace lean; -template -struct list_ptr_hash { unsigned operator()(list const & l) const { return std::hash::cell*>()(l.raw()); } }; -template -struct list_ptr_eq { bool operator()(list const & l1, list const & l2) const { return l1.raw() == l2.raw(); } }; - -class list_int_serializer : public object_serializer, list_ptr_hash, list_ptr_eq> { - typedef object_serializer, list_ptr_hash, list_ptr_eq> super; -public: - void write(list const & l) { - super::write(l, [&]() { - serializer & s = get_owner(); - if (l) { - s.write_bool(true); - s.write_int(head(l)); - write(tail(l)); - } else { - s.write_bool(false); - } - }); - } -}; - -class list_int_deserializer : public object_deserializer> { - typedef object_deserializer> super; -public: - list read() { - return super::read([&]() { - deserializer & d = get_owner(); - if (d.read_bool()) { - int h = d.read_int(); - list t = read(); - return cons(h, t); - } else { - return list(); - } - }); - } -}; - void display(std::ostringstream const & out) { std::cout << "OUT: "; auto str = out.str(); diff --git a/src/util/name.cpp b/src/util/name.cpp index f46a21ca18..83c76094e3 100644 --- a/src/util/name.cpp +++ b/src/util/name.cpp @@ -18,7 +18,6 @@ Author: Leonardo de Moura #include "util/buffer.h" #include "util/hash.h" #include "util/ascii.h" -#include "util/object_serializer.h" namespace lean { constexpr char const * anonymous_str = "[anonymous]"; @@ -254,10 +253,10 @@ int name::cmp_core(object * i1, object * i2) { } static unsigned num_digits(nat k) { - if (k == nat(0)) + if (k == 0) return 1; int r = 0; - while (k != nat(0)) { + while (k != 0) { k = k / nat(10); r++; } diff --git a/src/util/nat.h b/src/util/nat.h index b2411a755c..2d22bac395 100644 --- a/src/util/nat.h +++ b/src/util/nat.h @@ -40,18 +40,25 @@ public: friend bool operator==(nat const & a, nat const & b) { return nat_eq(a.raw(), b.raw()); } friend bool operator!=(nat const & a, nat const & b) { return !(a == b); } friend bool operator<=(nat const & a, nat const & b) { return nat_le(a.raw(), b.raw()); } - friend bool operator<(nat const & a, nat const & b) { return nat_lt(a.raw(), b.raw()); } + friend bool operator<(nat const & a, nat const & b) { return nat_lt(a.raw(), b.raw()); } friend bool operator>=(nat const & a, nat const & b) { return b <= a; } - friend bool operator>(nat const & a, nat const & b) { return b < a; } - friend nat operator+(nat const & a, nat const & b) { return wrap(nat_add(a.raw(), b.raw())); } - friend nat operator-(nat const & a, nat const & b) { return wrap(nat_sub(a.raw(), b.raw())); } - friend nat operator*(nat const & a, nat const & b) { return wrap(nat_mul(a.raw(), b.raw())); } - friend nat operator/(nat const & a, nat const & b) { return wrap(nat_div(a.raw(), b.raw())); } - friend nat operator%(nat const & a, nat const & b) { return wrap(nat_mod(a.raw(), b.raw())); } + friend bool operator>(nat const & a, nat const & b) { return b < a; } + friend bool operator==(nat const & a, unsigned b) { return a == nat(b); } + friend bool operator!=(nat const & a, unsigned b) { return !(a == b); } + friend bool operator<=(nat const & a, unsigned b) { return a <= nat(b); } + friend bool operator<(nat const & a, unsigned b) { return a < nat(b); } + friend bool operator>=(nat const & a, unsigned b) { return a >= nat(b); } + friend bool operator>(nat const & a, unsigned b) { return a > nat(b); } + friend nat operator+(nat const & a, nat const & b) { return wrap(nat_add(a.raw(), b.raw())); } + friend nat operator-(nat const & a, nat const & b) { return wrap(nat_sub(a.raw(), b.raw())); } + friend nat operator*(nat const & a, nat const & b) { return wrap(nat_mul(a.raw(), b.raw())); } + friend nat operator/(nat const & a, nat const & b) { return wrap(nat_div(a.raw(), b.raw())); } + friend nat operator%(nat const & a, nat const & b) { return wrap(nat_mod(a.raw(), b.raw())); } void serialize(serializer & s) const { s.write_object(raw()); } }; inline serializer & operator<<(serializer & s, nat const & n) { n.serialize(s); return s; } inline nat read_nat(deserializer & d) { return nat(d.read_object()); } inline deserializer & operator>>(deserializer & d, nat & n) { n = read_nat(d); return d; } +inline std::ostream & operator<<(std::ostream & out, nat const & n) { out << n.to_mpz(); return out; } }; diff --git a/src/util/object_ref.h b/src/util/object_ref.h index 069e0a3889..e6844ffc9b 100644 --- a/src/util/object_ref.h +++ b/src/util/object_ref.h @@ -39,13 +39,17 @@ public: object_ref mk_cnstr(unsigned tag, unsigned num_objs, object ** objs, unsigned scalar_sz = 0); inline object_ref mk_cnstr(unsigned tag, object * o, unsigned scalar_sz = 0) { return mk_cnstr(tag, 1, &o, scalar_sz); } inline object_ref mk_cnstr(unsigned tag, object * o1, object * o2, unsigned scalar_sz = 0) { - object * os[] = { o1, o2 }; + object * os[2] = { o1, o2 }; return mk_cnstr(tag, 2, os, scalar_sz); } inline object_ref mk_cnstr(unsigned tag, object * o1, object * o2, object * o3, unsigned scalar_sz = 0) { - object * os[] = { o1, o2, o3 }; + object * os[3] = { o1, o2, o3 }; return mk_cnstr(tag, 3, os, scalar_sz); } +inline object_ref mk_cnstr(unsigned tag, object * o1, object * o2, object * o3, object * o4, unsigned scalar_sz = 0) { + object * os[4] = { o1, o2, o3, o4 }; + return mk_cnstr(tag, 4, os, scalar_sz); +} /* The following definition is a low level hack that relies on the fact that sizeof(object_ref) == sizeof(object *). */ inline object_ref const & cnstr_obj_ref(object * o, unsigned i) { diff --git a/src/util/object_serializer.h b/src/util/object_serializer.h deleted file mode 100644 index 83f69927a7..0000000000 --- a/src/util/object_serializer.h +++ /dev/null @@ -1,70 +0,0 @@ -/* -Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -#include -#include "runtime/serializer.h" - -#ifndef LEAN_OBJECT_SERIALIZER_BUCKET_SIZE -#define LEAN_OBJECT_SERIALIZER_BUCKET_SIZE 8 -#endif - -namespace lean { -/** \brief Helper class for serializing objects. */ -template -class object_serializer : public serializer::extension { - std::unordered_map m_table; -public: - object_serializer(HashFn const & h = HashFn(), EqFn const & e = EqFn()):m_table(LEAN_OBJECT_SERIALIZER_BUCKET_SIZE, h, e) {} - - template - void write_core(T const & v, char k, F && f) { - auto it = m_table.find(v); - serializer & s = get_owner(); - if (it == m_table.end()) { - s.write_char(k + 1); - f(); - m_table.insert(std::make_pair(v, static_cast(m_table.size()))); - } else { - s.write_char(0); - s.write_unsigned(it->second); - } - } - - template - void write(T const & v, F && f) { - write_core(v, 0, f); - } -}; - -/** \brief Helper class for deserializing objects. */ -template -class object_deserializer : public deserializer::extension { - std::vector m_table; -public: - template - T read_core(F && f) { - deserializer & d = get_owner(); - char c = d.read_char(); - if (c != 0) { - T r = f(c-1); - m_table.push_back(r); - return r; - } else { - unsigned i = d.read_unsigned(); - if (i >= m_table.size()) - throw corrupted_stream_exception(); - return m_table[i]; - } - } - - template - T read(F && f) { - return read_core([&](char ) { return f(); }); - } -}; -} diff --git a/src/util/sexpr/sexpr.cpp b/src/util/sexpr/sexpr.cpp index 9c855247d8..a2ed8e70a8 100644 --- a/src/util/sexpr/sexpr.cpp +++ b/src/util/sexpr/sexpr.cpp @@ -13,7 +13,6 @@ Author: Leonardo de Moura #include "util/name.h" #include "util/escaped.h" #include "util/buffer.h" -#include "util/object_serializer.h" #include "util/sexpr/sexpr.h" namespace lean {