From 2b1d734544ad3564a7d0c8d727c32b1985bea003 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 29 Feb 2016 12:41:43 -0800 Subject: [PATCH] feat(kernel/expr): remove 'contextual' flag from binder_info --- src/api/expr.cpp | 3 --- src/api/lean_expr.h | 3 +-- src/frontends/lean/builtin_exprs.cpp | 2 +- src/frontends/lean/elaborator.cpp | 3 +-- src/kernel/expr.cpp | 6 +++--- src/kernel/expr.h | 17 +++++------------ src/library/kernel_serializer.cpp | 12 +++++------- src/library/print.cpp | 4 ---- 8 files changed, 16 insertions(+), 34 deletions(-) diff --git a/src/api/expr.cpp b/src/api/expr.cpp index 369ce9109..8bb1dee7b 100644 --- a/src/api/expr.cpp +++ b/src/api/expr.cpp @@ -56,7 +56,6 @@ static binder_info to_binder_info(lean_binder_kind k) { case LEAN_BINDER_IMPLICIT: return mk_implicit_binder_info(); case LEAN_BINDER_STRICT_IMPLICIT: return mk_strict_implicit_binder_info(); case LEAN_BINDER_INST_IMPLICIT: return mk_inst_implicit_binder_info(); - case LEAN_BINDER_HIDDEN: return mk_contextual_info(false); } lean_unreachable(); } @@ -68,8 +67,6 @@ static lean_binder_kind of_binder_info(binder_info k) { return LEAN_BINDER_INST_IMPLICIT; else if (k.is_strict_implicit()) return LEAN_BINDER_STRICT_IMPLICIT; - else if (!k.is_contextual()) - return LEAN_BINDER_HIDDEN; else return LEAN_BINDER_DEFAULT; } diff --git a/src/api/lean_expr.h b/src/api/lean_expr.h index 1b90f3629..cec7816e0 100644 --- a/src/api/lean_expr.h +++ b/src/api/lean_expr.h @@ -41,8 +41,7 @@ typedef enum { LEAN_BINDER_DEFAULT, // (x : A) LEAN_BINDER_IMPLICIT, // {x : A} LEAN_BINDER_STRICT_IMPLICIT, // {{x : A}} - LEAN_BINDER_INST_IMPLICIT, // [x : A] - LEAN_BINDER_HIDDEN // like (x : A) but not included in proof goals + LEAN_BINDER_INST_IMPLICIT // [x : A] } lean_binder_kind; /** \brief Create a variable with de-Bruijn index \c i. diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 5617a9cf5..446f2c203 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -341,7 +341,7 @@ static expr parse_using_expr(parser & p, pos_info const & using_pos) { if (!is_local(l)) throw parser_error("invalid 'using' declaration for 'have', local expected", id_pos); expr new_l; - binder_info bi = local_info(l).update_contextual(true); + binder_info bi = local_info(l); if (p.is_local_variable_parameter(local_pp_name(l))) { expr new_type = p.save_pos(mk_as_is(mlocal_type(l)), id_pos); new_l = p.save_pos(mk_local(mlocal_name(l), local_pp_name(l), new_type, bi), id_pos); diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index b127ec0b2..f856b3ab5 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -941,8 +941,7 @@ expr elaborator::visit_binding(expr e, expr_kind k, constraint_seq & cs) { ds.push_back(d); expr l = mk_local(binding_name(e), d, binding_info(e)); if (!is_match_binder_name(binding_name(e))) { - if (binding_info(e).is_contextual()) - m_context.add_local(l); + m_context.add_local(l); m_full_context.add_local(l); } ls.push_back(l); diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 19074d12c..4ecb3401c 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -139,7 +139,7 @@ void expr_const::dealloc() { } unsigned binder_info::hash() const { - return (m_implicit << 3) | (m_contextual << 2) | (m_strict_implicit << 1) | m_inst_implicit; + return (m_rec << 3) | (m_implicit << 2) | (m_strict_implicit << 1) | m_inst_implicit; } // Expr metavariables and local variables @@ -200,9 +200,9 @@ 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_contextual() == i2.is_contextual() && i1.is_strict_implicit() == i2.is_strict_implicit() && - i1.is_inst_implicit() == i2.is_inst_implicit(); + i1.is_inst_implicit() == i2.is_inst_implicit() && + i1.is_rec() == i2.is_rec(); } // Expr binders (Lambda, Pi) diff --git a/src/kernel/expr.h b/src/kernel/expr.h index a7ecbf513..339229e83 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -208,9 +208,6 @@ public: */ class binder_info { unsigned m_implicit:1; //! if true, binder argument is an implicit argument - /** if m_contextual is true, binder argument is assumed to be part of the context, - and may be argument for metavariables. */ - unsigned m_contextual:1; 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. */ @@ -219,23 +216,19 @@ class binder_info { in recursive equations */ unsigned m_rec:1; public: - binder_info(bool implicit = false, bool contextual = true, bool strict_implicit = false, bool inst_implicit = false, bool rec = false): - m_implicit(implicit), m_contextual(contextual), m_strict_implicit(strict_implicit), - m_inst_implicit(inst_implicit), m_rec(rec) {} + 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_contextual() const { return m_contextual; } 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 update_contextual(bool f) const { return binder_info(m_implicit, f, m_strict_implicit, m_inst_implicit, m_rec); } }; inline binder_info mk_implicit_binder_info() { return binder_info(true); } -inline binder_info mk_strict_implicit_binder_info() { return binder_info(false, true, true); } -inline binder_info mk_inst_implicit_binder_info() { return binder_info(false, true, false, true); } -inline binder_info mk_contextual_info(bool f) { return binder_info(false, f); } -inline binder_info mk_rec_info(bool f) { return binder_info(false, true, false, false, f); } +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 bool is_explicit(binder_info const & bi) { return !bi.is_implicit() && !bi.is_strict_implicit() && !bi.is_inst_implicit(); diff --git a/src/library/kernel_serializer.cpp b/src/library/kernel_serializer.cpp index d8b2601e2..560b4111c 100644 --- a/src/library/kernel_serializer.cpp +++ b/src/library/kernel_serializer.cpp @@ -118,9 +118,8 @@ static expr read_macro_definition(deserializer & d, unsigned num, expr const * a serializer & operator<<(serializer & s, binder_info const & i) { unsigned w = - (i.is_rec() ? 16 : 0) + - (i.is_implicit() ? 8 : 0) + - (i.is_contextual() ? 4 : 0) + + (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); @@ -129,12 +128,11 @@ serializer & operator<<(serializer & s, binder_info const & i) { static binder_info read_binder_info(deserializer & d) { unsigned w = d.read_char(); - bool rec = (w & 16) != 0; - bool imp = (w & 8) != 0; - bool ctx = (w & 4) != 0; + 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, ctx, s_imp, i_imp, rec); + return binder_info(imp, s_imp, i_imp, rec); } static name * g_binder_name = nullptr; diff --git a/src/library/print.cpp b/src/library/print.cpp index bb199c407..cc5fcbf34 100644 --- a/src/library/print.cpp +++ b/src/library/print.cpp @@ -158,8 +158,6 @@ struct print_expr_fn { out() << "{"; else if (binding_info(e).is_inst_implicit()) out() << "["; - else if (!binding_info(e).is_contextual()) - out() << "[["; else if (binding_info(e).is_strict_implicit()) out() << "{{"; else @@ -170,8 +168,6 @@ struct print_expr_fn { out() << "}"; else if (binding_info(e).is_inst_implicit()) out() << "]"; - else if (!binding_info(e).is_contextual()) - out() << "]]"; else if (binding_info(e).is_strict_implicit()) out() << "}}"; else