feat(kernel/expr): remove 'contextual' flag from binder_info

This commit is contained in:
Leonardo de Moura 2016-02-29 12:41:43 -08:00
parent b41c65f549
commit 2b1d734544
8 changed files with 16 additions and 34 deletions

View file

@ -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_IMPLICIT: return mk_implicit_binder_info();
case LEAN_BINDER_STRICT_IMPLICIT: return mk_strict_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_INST_IMPLICIT: return mk_inst_implicit_binder_info();
case LEAN_BINDER_HIDDEN: return mk_contextual_info(false);
} }
lean_unreachable(); lean_unreachable();
} }
@ -68,8 +67,6 @@ static lean_binder_kind of_binder_info(binder_info k) {
return LEAN_BINDER_INST_IMPLICIT; return LEAN_BINDER_INST_IMPLICIT;
else if (k.is_strict_implicit()) else if (k.is_strict_implicit())
return LEAN_BINDER_STRICT_IMPLICIT; return LEAN_BINDER_STRICT_IMPLICIT;
else if (!k.is_contextual())
return LEAN_BINDER_HIDDEN;
else else
return LEAN_BINDER_DEFAULT; return LEAN_BINDER_DEFAULT;
} }

View file

@ -41,8 +41,7 @@ typedef enum {
LEAN_BINDER_DEFAULT, // (x : A) LEAN_BINDER_DEFAULT, // (x : A)
LEAN_BINDER_IMPLICIT, // {x : A} LEAN_BINDER_IMPLICIT, // {x : A}
LEAN_BINDER_STRICT_IMPLICIT, // {{x : A}} LEAN_BINDER_STRICT_IMPLICIT, // {{x : A}}
LEAN_BINDER_INST_IMPLICIT, // [x : A] LEAN_BINDER_INST_IMPLICIT // [x : A]
LEAN_BINDER_HIDDEN // like (x : A) but not included in proof goals
} lean_binder_kind; } lean_binder_kind;
/** \brief Create a variable with de-Bruijn index \c i. /** \brief Create a variable with de-Bruijn index \c i.

View file

@ -341,7 +341,7 @@ static expr parse_using_expr(parser & p, pos_info const & using_pos) {
if (!is_local(l)) if (!is_local(l))
throw parser_error("invalid 'using' declaration for 'have', local expected", id_pos); throw parser_error("invalid 'using' declaration for 'have', local expected", id_pos);
expr new_l; 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))) { if (p.is_local_variable_parameter(local_pp_name(l))) {
expr new_type = p.save_pos(mk_as_is(mlocal_type(l)), id_pos); 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); new_l = p.save_pos(mk_local(mlocal_name(l), local_pp_name(l), new_type, bi), id_pos);

View file

@ -941,7 +941,6 @@ expr elaborator::visit_binding(expr e, expr_kind k, constraint_seq & cs) {
ds.push_back(d); ds.push_back(d);
expr l = mk_local(binding_name(e), d, binding_info(e)); expr l = mk_local(binding_name(e), d, binding_info(e));
if (!is_match_binder_name(binding_name(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); m_full_context.add_local(l);
} }

View file

@ -139,7 +139,7 @@ void expr_const::dealloc() {
} }
unsigned binder_info::hash() const { 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 // 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) { bool operator==(binder_info const & i1, binder_info const & i2) {
return return
i1.is_implicit() == i2.is_implicit() && i1.is_implicit() == i2.is_implicit() &&
i1.is_contextual() == i2.is_contextual() &&
i1.is_strict_implicit() == i2.is_strict_implicit() && 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) // Expr binders (Lambda, Pi)

View file

@ -208,9 +208,6 @@ public:
*/ */
class binder_info { class binder_info {
unsigned m_implicit:1; //! if true, binder argument is an implicit argument 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 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 /** \brief if m_inst_implicit is true, binder argument is an implicit argument, and should be
inferred by class-instance resolution. */ inferred by class-instance resolution. */
@ -219,23 +216,19 @@ class binder_info {
in recursive equations */ in recursive equations */
unsigned m_rec:1; unsigned m_rec:1;
public: public:
binder_info(bool implicit = false, bool contextual = true, bool strict_implicit = false, bool inst_implicit = false, bool rec = false): binder_info(bool implicit = false, bool strict_implicit = false, bool inst_implicit = false, bool rec = false):
m_implicit(implicit), m_contextual(contextual), m_strict_implicit(strict_implicit), m_implicit(implicit), m_strict_implicit(strict_implicit), m_inst_implicit(inst_implicit), m_rec(rec) {}
m_inst_implicit(inst_implicit), m_rec(rec) {}
bool is_implicit() const { return m_implicit; } 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_strict_implicit() const { return m_strict_implicit; }
bool is_inst_implicit() const { return m_inst_implicit; } bool is_inst_implicit() const { return m_inst_implicit; }
bool is_rec() const { return m_rec; } bool is_rec() const { return m_rec; }
unsigned hash() const; 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_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_strict_implicit_binder_info() { return binder_info(false, true); }
inline binder_info mk_inst_implicit_binder_info() { return binder_info(false, true, false, true); } inline binder_info mk_inst_implicit_binder_info() { return binder_info(false, 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, false, false, f); }
inline binder_info mk_rec_info(bool f) { return binder_info(false, true, false, false, f); }
inline bool is_explicit(binder_info const & bi) { inline bool is_explicit(binder_info const & bi) {
return !bi.is_implicit() && !bi.is_strict_implicit() && !bi.is_inst_implicit(); return !bi.is_implicit() && !bi.is_strict_implicit() && !bi.is_inst_implicit();

View file

@ -118,9 +118,8 @@ static expr read_macro_definition(deserializer & d, unsigned num, expr const * a
serializer & operator<<(serializer & s, binder_info const & i) { serializer & operator<<(serializer & s, binder_info const & i) {
unsigned w = unsigned w =
(i.is_rec() ? 16 : 0) + (i.is_rec() ? 8 : 0) +
(i.is_implicit() ? 8 : 0) + (i.is_implicit() ? 4 : 0) +
(i.is_contextual() ? 4 : 0) +
(i.is_strict_implicit() ? 2 : 0) + (i.is_strict_implicit() ? 2 : 0) +
(i.is_inst_implicit() ? 1 : 0); (i.is_inst_implicit() ? 1 : 0);
s.write_char(w); s.write_char(w);
@ -129,12 +128,11 @@ serializer & operator<<(serializer & s, binder_info const & i) {
static binder_info read_binder_info(deserializer & d) { static binder_info read_binder_info(deserializer & d) {
unsigned w = d.read_char(); unsigned w = d.read_char();
bool rec = (w & 16) != 0; bool rec = (w & 8) != 0;
bool imp = (w & 8) != 0; bool imp = (w & 4) != 0;
bool ctx = (w & 4) != 0;
bool s_imp = (w & 2) != 0; bool s_imp = (w & 2) != 0;
bool i_imp = (w & 1) != 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; static name * g_binder_name = nullptr;

View file

@ -158,8 +158,6 @@ struct print_expr_fn {
out() << "{"; out() << "{";
else if (binding_info(e).is_inst_implicit()) else if (binding_info(e).is_inst_implicit())
out() << "["; out() << "[";
else if (!binding_info(e).is_contextual())
out() << "[[";
else if (binding_info(e).is_strict_implicit()) else if (binding_info(e).is_strict_implicit())
out() << "{{"; out() << "{{";
else else
@ -170,8 +168,6 @@ struct print_expr_fn {
out() << "}"; out() << "}";
else if (binding_info(e).is_inst_implicit()) else if (binding_info(e).is_inst_implicit())
out() << "]"; out() << "]";
else if (!binding_info(e).is_contextual())
out() << "]]";
else if (binding_info(e).is_strict_implicit()) else if (binding_info(e).is_strict_implicit())
out() << "}}"; out() << "}}";
else else