diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 2870cbe8c8..14f114fee5 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -184,7 +184,7 @@ static expr parse_let(parser & p, pos_info const & pos, bool in_do_block) { p.add_local(l); expr body = parse_let_body(p, pos, in_do_block); match_definition_scope match_scope(p.env()); - expr fn = p.save_pos(mk_local(p.next_name(), *g_let_match_name, mk_expr_placeholder(), mk_rec_info(true)), pos); + expr fn = p.save_pos(mk_local(p.next_name(), *g_let_match_name, mk_expr_placeholder(), mk_rec_info()), pos); expr eqn = Fun(fn, Fun(new_locals, p.save_pos(mk_equation(p.rec_save_pos(mk_app(fn, lhs), pos), body), pos), p), p); equations_header h = mk_match_header(match_scope.get_name(), match_scope.get_actual_name()); expr eqns = p.save_pos(mk_equations(h, 1, &eqn), pos); @@ -317,7 +317,7 @@ static expr parse_do(parser & p, bool has_braces) { // must introduce a "fake" match auto pos = ps[i]; match_definition_scope match_scope(p.env()); - expr fn = p.save_pos(mk_local(p.next_name(), *g_do_match_name, mk_expr_placeholder(), mk_rec_info(true)), pos); + expr fn = p.save_pos(mk_local(p.next_name(), *g_do_match_name, mk_expr_placeholder(), mk_rec_info()), pos); buffer locals; to_buffer(lhss_locals[i], locals); buffer eqs; @@ -745,7 +745,7 @@ static expr parse_lambda_constructor(parser & p, pos_info const & ini_pos) { body = parse_lambda_core(p, ini_pos); } match_definition_scope match_scope(p.env()); - expr fn = p.save_pos(mk_local(p.next_name(), *g_lambda_match_name, mk_expr_placeholder(), mk_rec_info(true)), pos); + expr fn = p.save_pos(mk_local(p.next_name(), *g_lambda_match_name, mk_expr_placeholder(), mk_rec_info()), pos); expr eqn = Fun(fn, Fun(locals, p.save_pos(mk_equation(p.rec_save_pos(mk_app(fn, pattern), pos), body), pos), p), p); equations_header h = mk_match_header(match_scope.get_name(), match_scope.get_actual_name()); expr x = p.rec_save_pos(mk_local(p.next_name(), "_x", mk_expr_placeholder(), binder_info()), pos); diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index 3e88d74b4d..40939b681c 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -144,7 +144,7 @@ static expr parse_mutual_definition(parser & p, buffer & lp_names, buffer< } check_valid_end_of_equations(p); } - expr fn = mk_local(mlocal_name(pre_fn), mlocal_pp_name(pre_fn), fn_type, mk_rec_info(true)); + expr fn = mk_local(mlocal_name(pre_fn), mlocal_pp_name(pre_fn), fn_type, mk_rec_info()); fns.push_back(fn); } if (p.curr_is_token(get_with_tk())) @@ -530,7 +530,7 @@ static std::tuple parse_definition(parser & p, buffer & p.next(); if (is_meta) { declaration_name_scope scope2("_main"); - fn = mk_local(mlocal_name(fn), mlocal_pp_name(fn), mlocal_type(fn), mk_rec_info(true)); + fn = mk_local(mlocal_name(fn), mlocal_pp_name(fn), mlocal_type(fn), mk_rec_info()); p.add_local(fn); val = p.parse_expr(); /* add fake equation */ @@ -545,7 +545,7 @@ static std::tuple parse_definition(parser & p, buffer & if (is_abbrev) throw exception("invalid abbreviation, abbreviations should not be defined using pattern matching"); declaration_name_scope scope2("_main"); - fn = mk_local(mlocal_name(fn), mlocal_pp_name(fn), mlocal_type(fn), mk_rec_info(true)); + fn = mk_local(mlocal_name(fn), mlocal_pp_name(fn), mlocal_type(fn), mk_rec_info()); p.add_local(fn); buffer eqns; if (p.curr_is_token(get_period_tk())) { diff --git a/src/frontends/lean/match_expr.cpp b/src/frontends/lean/match_expr.cpp index 72c6b2de28..caa966bd25 100644 --- a/src/frontends/lean/match_expr.cpp +++ b/src/frontends/lean/match_expr.cpp @@ -36,9 +36,9 @@ expr parse_match(parser & p, unsigned, expr const *, pos_info const & pos) { if (p.curr_is_token(get_colon_tk())) { p.next(); expr type = p.parse_expr(); - fn = mk_local(p.next_name(), *g_match_name, type, mk_rec_info(true)); + fn = mk_local(p.next_name(), *g_match_name, type, mk_rec_info()); } else { - fn = mk_local(p.next_name(), *g_match_name, mk_expr_placeholder(), mk_rec_info(true)); + fn = mk_local(p.next_name(), *g_match_name, mk_expr_placeholder(), mk_rec_info()); } p.check_token_next(get_with_tk(), "invalid 'match' expression, 'with' expected"); diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 0e5f23b2a2..62d53c3037 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -142,10 +142,6 @@ void expr_const::dealloc() { delete this; } -unsigned binder_info::hash() const { - return (m_rec << 3) | (m_implicit << 2) | (m_strict_implicit << 1) | m_inst_implicit; -} - // 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::Meta : expr_kind::FVar, n.hash(), is_meta || t.has_expr_metavar(), t.has_univ_metavar(), @@ -215,14 +211,6 @@ void expr_app::dealloc(buffer & todelete) { static unsigned dec(unsigned k) { return k == 0 ? 0 : k - 1; } -bool operator==(binder_info const & i1, binder_info const & i2) { - return - i1.is_implicit() == i2.is_implicit() && - i1.is_strict_implicit() == i2.is_strict_implicit() && - i1.is_inst_implicit() == i2.is_inst_implicit() && - i1.is_rec() == i2.is_rec(); -} - // Expr binders (Lambda, Pi) expr_binding::expr_binding(expr_kind k, name const & n, expr const & t, expr const & b, binder_info const & i): expr_composite(k, ::lean::hash(t.hash(), b.hash()), diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 7a8ca25a21..9184a15136 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -204,41 +204,38 @@ public: expr const & get_type() const { return m_type; } }; -/** - \brief Auxiliary annotation for binders (Lambda and Pi). This information - is only used for elaboration. -*/ +/** \brief Auxiliary annotation for binders (Lambda and Pi). */ class binder_info { - unsigned m_implicit:1; //! if true, binder argument is an implicit argument - unsigned m_strict_implicit:1; //! if true, binder argument is assumed to be a strict implicit argument - /** \brief if m_inst_implicit is true, binder argument is an implicit argument, and should be - inferred by class-instance resolution. */ - unsigned m_inst_implicit:1; - /** \brief Auxiliary internal attribute used to mark local constants representing recursive functions - in recursive equations. TODO(Leo): rename to eqn_decl since we also mark non recursive equations - (e.g., `match ... with ... end`) with this flag. */ - unsigned m_rec:1; + enum kind { Default, Implicit, StrictImplicit, InstImplicit, Rec }; + object * m_val; + binder_info(object * v):m_val(v) {} public: - binder_info(bool implicit = false, bool strict_implicit = false, bool inst_implicit = false, bool rec = false): - m_implicit(implicit), m_strict_implicit(strict_implicit), m_inst_implicit(inst_implicit), m_rec(rec) {} - bool is_implicit() const { return m_implicit; } - bool is_strict_implicit() const { return m_strict_implicit; } - bool is_inst_implicit() const { return m_inst_implicit; } - bool is_rec() const { return m_rec; } - unsigned hash() const; + binder_info():m_val(box(static_cast(Default))) {} + friend binder_info mk_implicit_binder_info(); + friend binder_info mk_strict_implicit_binder_info(); + friend binder_info mk_inst_implicit_binder_info(); + friend binder_info mk_rec_info(); + bool is_implicit() const { return unbox(m_val) == static_cast(Implicit); } + bool is_strict_implicit() const { return unbox(m_val) == static_cast(StrictImplicit); } + bool is_inst_implicit() const { return unbox(m_val) == static_cast(InstImplicit); } + bool is_rec() const { return unbox(m_val) == static_cast(Rec); } + unsigned hash() const { return unbox(m_val); } + friend bool operator==(binder_info const & i1, binder_info const & i2) { return i1.m_val == i2.m_val; } + friend bool operator!=(binder_info const & i1, binder_info const & i2) { return !(i1 == i2); } + friend binder_info read_binder_info(deserializer & d); + void serialize(serializer & s) const { s.write_object(m_val); } }; -inline binder_info mk_implicit_binder_info() { return binder_info(true); } -inline binder_info mk_strict_implicit_binder_info() { return binder_info(false, true); } -inline binder_info mk_inst_implicit_binder_info() { return binder_info(false, false, true); } -inline binder_info mk_rec_info(bool f) { return binder_info(false, false, false, f); } - +inline binder_info mk_implicit_binder_info() { return binder_info(box(static_cast(binder_info::Implicit))); } +inline binder_info mk_strict_implicit_binder_info() { return binder_info(box(static_cast(binder_info::StrictImplicit))); } +inline binder_info mk_inst_implicit_binder_info() { return binder_info(box(static_cast(binder_info::InstImplicit))); } +inline binder_info mk_rec_info() { return binder_info(box(static_cast(binder_info::Rec))); } inline bool is_explicit(binder_info const & bi) { return !bi.is_implicit() && !bi.is_strict_implicit() && !bi.is_inst_implicit(); } - -bool operator==(binder_info const & i1, binder_info const & i2); -inline bool operator!=(binder_info const & i1, binder_info const & i2) { return !(i1 == i2); } +inline serializer & operator<<(serializer & s, binder_info const & bi) { bi.serialize(s); return s; } +inline binder_info read_binder_info(deserializer & d) { return binder_info(d.read_object()); } +inline deserializer & operator>>(deserializer & d, binder_info & bi) { bi = read_binder_info(d); return d; } /** \brief Compute a hash code that takes binder_info into account. \remark This information is not cached like hash(). */ diff --git a/src/library/equations_compiler/pack_mutual.cpp b/src/library/equations_compiler/pack_mutual.cpp index daf0ba8a24..7cff453113 100644 --- a/src/library/equations_compiler/pack_mutual.cpp +++ b/src/library/equations_compiler/pack_mutual.cpp @@ -183,7 +183,7 @@ struct pack_mutual_fn { expr x = locals.push_local("_x", new_domain); expr new_codomain = mk_new_codomain(x, 0, codomains, codomains_lvl); expr new_fn_type = m_ctx.mk_pi(x, new_codomain); - expr new_fn = locals.push_local(new_fn_name, new_fn_type, mk_rec_info(true)); + expr new_fn = locals.push_local(new_fn_name, new_fn_type, mk_rec_info()); trace_debug_mutual(tout() << "new function " << new_fn_name << " : " << new_fn_type << "\n";); diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp index bc4c87d985..3a75a48c39 100644 --- a/src/library/equations_compiler/util.cpp +++ b/src/library/equations_compiler/util.cpp @@ -144,7 +144,7 @@ unpack_eqns::unpack_eqns(type_context_old & ctx, expr const & e): } expr unpack_eqns::update_fn_type(unsigned fidx, expr const & type) { - expr new_fn = m_locals.push_local(mlocal_pp_name(m_fns[fidx]), type, mk_rec_info(true)); + expr new_fn = m_locals.push_local(mlocal_pp_name(m_fns[fidx]), type, mk_rec_info()); m_fns[fidx] = new_fn; return new_fn; } diff --git a/src/library/kernel_serializer.cpp b/src/library/kernel_serializer.cpp index 7960db72d0..5c8831c13d 100644 --- a/src/library/kernel_serializer.cpp +++ b/src/library/kernel_serializer.cpp @@ -34,25 +34,6 @@ static expr read_macro_definition(deserializer & d, unsigned num, expr const * a return it->second(d, num, args); } -serializer & operator<<(serializer & s, binder_info const & i) { - unsigned w = - (i.is_rec() ? 8 : 0) + - (i.is_implicit() ? 4 : 0) + - (i.is_strict_implicit() ? 2 : 0) + - (i.is_inst_implicit() ? 1 : 0); - s.write_char(w); - return s; -} - -static binder_info read_binder_info(deserializer & d) { - unsigned w = d.read_char(); - bool rec = (w & 8) != 0; - bool imp = (w & 4) != 0; - bool s_imp = (w & 2) != 0; - bool i_imp = (w & 1) != 0; - return binder_info(imp, s_imp, i_imp, rec); -} - static name * g_binder_name = nullptr; class expr_serializer : public object_serializer { diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp index 471ef0910d..a187713ebf 100644 --- a/src/library/vm/vm_expr.cpp +++ b/src/library/vm/vm_expr.cpp @@ -91,7 +91,7 @@ binder_info to_binder_info(vm_obj const & o) { case 1: return mk_implicit_binder_info(); case 2: return mk_strict_implicit_binder_info(); case 3: return mk_inst_implicit_binder_info(); - default: return mk_rec_info(true); + default: return mk_rec_info(); } } @@ -205,7 +205,7 @@ unsigned expr_cases_on(vm_obj const & o, buffer & data) { break; } case expr_kind::Quote: - data.push_back(to_obj(quote_is_reflected(e))); + data.push_back(mk_vm_bool(quote_is_reflected(e))); data.push_back(to_obj(quote_value(e))); break; }