From 445d4f67934d6e14ccc44e3feb8f5f0366919463 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 8 Dec 2013 18:11:35 -0800 Subject: [PATCH] refactor(kernel/unification_constraint): remove 'null' unification_constraint and its operator bool Signed-off-by: Leonardo de Moura --- src/kernel/unification_constraint.h | 42 +++++++++++++++++++-------- src/library/elaborator/elaborator.cpp | 27 ++++++++--------- 2 files changed, 44 insertions(+), 25 deletions(-) diff --git a/src/kernel/unification_constraint.h b/src/kernel/unification_constraint.h index de2c279e4..377d98e20 100644 --- a/src/kernel/unification_constraint.h +++ b/src/kernel/unification_constraint.h @@ -51,12 +51,16 @@ public: void set_justification(justification const & j) { lean_assert(!m_justification); m_justification = j; } }; +class unification_constraint_eq; +class unification_constraint_convertible; +class unification_constraint_max; +class unification_constraint_choice; + class unification_constraint { private: unification_constraint_cell * m_ptr; explicit unification_constraint(unification_constraint_cell * ptr):m_ptr(ptr) {} public: - unification_constraint():m_ptr(nullptr) {} unification_constraint(unification_constraint const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); } unification_constraint(unification_constraint && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; } ~unification_constraint() { if (m_ptr) m_ptr->dec_ref(); } @@ -67,22 +71,25 @@ public: unification_constraint & operator=(unification_constraint && s) { LEAN_MOVE_REF(unification_constraint, s); } unification_constraint_kind kind() const { return m_ptr->kind(); } - unification_constraint_cell * raw() const { return m_ptr; } - - explicit operator bool() const { return m_ptr != nullptr; } format pp(formatter const & fmt, options const & opts, pos_info_provider const * p = nullptr, bool include_justification = false) const { - lean_assert(m_ptr); return m_ptr->pp(fmt, opts, p, include_justification); } - justification const & get_justification() const { lean_assert(m_ptr); return m_ptr->get_justification(); } + justification const & get_justification() const { return m_ptr->get_justification(); } void set_justification(justification const & j) { lean_assert(!get_justification()); lean_assert(m_ptr); m_ptr->set_justification(j); } + context const & get_context() const { return m_ptr->get_context(); } + friend unification_constraint mk_eq_constraint(context const & c, expr const & lhs, expr const & rhs, justification const & j); friend unification_constraint mk_convertible_constraint(context const & c, expr const & from, expr const & to, justification const & j); friend unification_constraint mk_max_constraint(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, justification const & j); friend unification_constraint mk_choice_constraint(context const & c, expr const & mvar, unsigned num, expr const * choices, justification const & j); + + friend unification_constraint_eq * to_eq(unification_constraint const & c); + friend unification_constraint_convertible * to_convertible(unification_constraint const & c); + friend unification_constraint_max * to_max(unification_constraint const & c); + friend unification_constraint_choice * to_choice(unification_constraint const & c); }; /** @@ -159,13 +166,24 @@ inline bool is_convertible(unification_constraint const & c) { return c.kind() = inline bool is_max(unification_constraint const & c) { return c.kind() == unification_constraint_kind::Max; } inline bool is_choice(unification_constraint const & c) { return c.kind() == unification_constraint_kind::Choice; } -inline unification_constraint_eq * to_eq(unification_constraint const & c) { lean_assert(is_eq(c)); return static_cast(c.raw()); } -inline unification_constraint_convertible * to_convertible(unification_constraint const & c) { lean_assert(is_convertible(c)); return static_cast(c.raw()); } -inline unification_constraint_max * to_max(unification_constraint const & c) { lean_assert(is_max(c)); return static_cast(c.raw()); } -inline unification_constraint_choice * to_choice(unification_constraint const & c) { lean_assert(is_choice(c)); return static_cast(c.raw()); } +inline unification_constraint_eq * to_eq(unification_constraint const & c) { + lean_assert(is_eq(c)); return static_cast(c.m_ptr); +} -inline context const & get_context(unification_constraint const & c) { return c.raw()->get_context(); } -inline justification const & get_justification(unification_constraint const & c) { return c.raw()->get_justification(); } +inline unification_constraint_convertible * to_convertible(unification_constraint const & c) { + lean_assert(is_convertible(c)); return static_cast(c.m_ptr); +} + +inline unification_constraint_max * to_max(unification_constraint const & c) { + lean_assert(is_max(c)); return static_cast(c.m_ptr); +} + +inline unification_constraint_choice * to_choice(unification_constraint const & c) { + lean_assert(is_choice(c)); return static_cast(c.m_ptr); +} + +inline context const & get_context(unification_constraint const & c) { return c.get_context(); } +inline justification const & get_justification(unification_constraint const & c) { return c.get_justification(); } inline expr const & eq_lhs(unification_constraint const & c) { return to_eq(c)->get_lhs(); } inline expr const & eq_rhs(unification_constraint const & c) { return to_eq(c)->get_rhs(); } inline expr const & convertible_from(unification_constraint const & c) { return to_convertible(c)->get_from(); } diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index a5e7c2065..25940fd1d 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -985,16 +985,15 @@ class elaborator::imp { // Remark: in principle, there are infinite number of choices. // We approximate and only consider the most useful ones. justification new_jst(new destruct_justification(c)); - unification_constraint new_c; if (is_bool(a)) { expr choices[5] = { Bool, Type(), Type(level() + 1), TypeM, TypeU }; - new_c = mk_choice_constraint(get_context(c), b, 5, choices, new_jst); + push_front(mk_choice_constraint(get_context(c), b, 5, choices, new_jst)); + return true; } else { expr choices[5] = { a, Type(ty_level(a) + 1), Type(ty_level(a) + 2), TypeM, TypeU }; - new_c = mk_choice_constraint(get_context(c), b, 5, choices, new_jst); + push_front(mk_choice_constraint(get_context(c), b, 5, choices, new_jst)); + return true; } - push_front(new_c); - return true; } else { return false; } @@ -1048,16 +1047,18 @@ class elaborator::imp { // // Remark: we also give preference to lower bounds justification new_jst(new destruct_justification(c)); - unification_constraint new_c; if (b == Type()) { expr choices[2] = { Type(), Bool }; - new_c = mk_choice_constraint(get_context(c), a, 2, choices, new_jst); + push_front(mk_choice_constraint(get_context(c), a, 2, choices, new_jst)); + return true; } else if (b == TypeU) { expr choices[5] = { TypeU, TypeM, Type(level() + 1), Type(), Bool }; - new_c = mk_choice_constraint(get_context(c), a, 5, choices, new_jst); + push_front(mk_choice_constraint(get_context(c), a, 5, choices, new_jst)); + return true; } else if (b == TypeM) { expr choices[4] = { TypeM, Type(level() + 1), Type(), Bool }; - new_c = mk_choice_constraint(get_context(c), a, 4, choices, new_jst); + push_front(mk_choice_constraint(get_context(c), a, 4, choices, new_jst)); + return true; } else { level const & lvl = ty_level(b); lean_assert(!lvl.is_bottom()); @@ -1076,18 +1077,18 @@ class elaborator::imp { if (!L.is_bottom()) choices.push_back(Type()); choices.push_back(Bool); - new_c = mk_choice_constraint(get_context(c), a, choices.size(), choices.data(), new_jst); + push_front(mk_choice_constraint(get_context(c), a, choices.size(), choices.data(), new_jst)); + return true; } else if (is_uvar(lvl)) { expr choices[4] = { Type(level() + 1), Type(), b, Bool }; - new_c = mk_choice_constraint(get_context(c), a, 4, choices, new_jst); + push_front(mk_choice_constraint(get_context(c), a, 4, choices, new_jst)); + return true; } else { lean_assert(is_max(lvl)); // TODO(Leo) return false; } } - push_front(new_c); - return true; } else { return false; }