feat(kernel/context): add operator== for contexts, and new constructor

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/kernel/context.cpp

@@ -9,6 +9,11 @@ Author: Leonardo de Moura
 #include "kernel/context.h"
 
 namespace lean {
+context::context(std::initializer_list<std::pair<char const *, expr const &>> const & l) {
+    for (auto const & p : l)
+        m_list = cons(context_entry(name(p.first), p.second), m_list);
+}
+
 std::pair<context_entry const &, context> context::lookup_ext(unsigned i) const {
     list<context_entry> const * it1 = &m_list;
     while (*it1) {

src/kernel/context.h

@@ -27,6 +27,8 @@ public:
     name const & get_name() const   { return m_name; }
     optional<expr> const & get_domain() const { return m_domain; }
     optional<expr> 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<std::pair<char const *, expr const &>> const & l);
     explicit context(list<context_entry> const & l):m_list(l) {}
     context_entry const & lookup(unsigned vidx) const;
     std::pair<context_entry const &, context> 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); }
 };
 
 /**

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<expr>));
@@ -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";