diff --git a/src/kernel/context.cpp b/src/kernel/context.cpp index c8d7fe2f32..44f7ce19a5 100644 --- a/src/kernel/context.cpp +++ b/src/kernel/context.cpp @@ -9,6 +9,11 @@ Author: Leonardo de Moura #include "kernel/context.h" namespace lean { +context::context(std::initializer_list> const & l) { + for (auto const & p : l) + m_list = cons(context_entry(name(p.first), p.second), m_list); +} + std::pair context::lookup_ext(unsigned i) const { list const * it1 = &m_list; while (*it1) { diff --git a/src/kernel/context.h b/src/kernel/context.h index 1813eb1830..242de2cf2d 100644 --- a/src/kernel/context.h +++ b/src/kernel/context.h @@ -27,6 +27,8 @@ public: name const & get_name() const { return m_name; } optional const & get_domain() const { return m_domain; } optional const & get_body() const { return m_body; } + friend bool operator==(context_entry const & e1, context_entry const & e2) { return e1.m_domain == e2.m_domain && e1.m_body == e2.m_body; } + friend bool operator!=(context_entry const & e1, context_entry const & e2) { return !(e1 == e2); } }; /** @@ -41,6 +43,7 @@ public: context(context const & c, name const & n, expr const & d, expr const & b):m_list(context_entry(n, d, b), c.m_list) {} context(context const & c, name const & n, expr const & d):m_list(context_entry(n, d), c.m_list) {} context(context const & c, context_entry const & e):m_list(e, c.m_list) {} + context(std::initializer_list> const & l); explicit context(list const & l):m_list(l) {} context_entry const & lookup(unsigned vidx) const; std::pair lookup_ext(unsigned vidx) const; @@ -65,6 +68,8 @@ public: \pre size() >= i */ context insert_at(unsigned i, name const & n, expr const & d) const; + friend bool operator==(context const & ctx1, context const & ctx2) { return ctx1.m_list == ctx2.m_list; } + friend bool operator!=(context const & ctx1, context const & ctx2) { return !(ctx1 == ctx2); } }; /** diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp index a34e0c3881..88efd1d70d 100644 --- a/src/tests/kernel/expr.cpp +++ b/src/tests/kernel/expr.cpp @@ -353,6 +353,14 @@ static void tst18() { lean_assert_eq(mk_bin_lop(f, a, {a1, a2, a3}), f(f(a1, a2), a3)); } +static void tst19() { + expr T1 = Const("T1"); + expr T2 = Const("T2"); + lean_assert(extend(extend(context(), "a", T1), "b", T2) == context({{"a", T1}, {"b", T2}})); + lean_assert(extend(extend(context(), "a", T1), "b", T2) == context({{"b", T1}, {"a", T2}})); // names don't matter + lean_assert(extend(extend(context(), "a", T2), "b", T2) != context({{"a", T1}, {"b", T2}})); +} + int main() { save_stack_info(); lean_assert(sizeof(expr) == sizeof(optional)); @@ -374,6 +382,7 @@ int main() { tst16(); tst17(); tst18(); + tst19(); std::cout << "sizeof(expr): " << sizeof(expr) << "\n"; std::cout << "sizeof(expr_app): " << sizeof(expr_app) << "\n"; std::cout << "sizeof(expr_cell): " << sizeof(expr_cell) << "\n";