From 913fd14549a12b904e87e83f8c2f43c50f68fffb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 14 Aug 2013 16:35:04 -0700
Subject: [PATCH] Add operator== to list

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontend/frontend.cpp      | 10 +++++++---
 src/frontend/operator_info.cpp | 18 ++++++++++++++++++
 src/frontend/operator_info.h   |  3 +++
 src/tests/util/list.cpp        | 15 ++++++++++++++-
 src/util/list.h                | 18 ++++++++++++++++--
 5 files changed, 58 insertions(+), 6 deletions(-)

diff --git a/src/frontend/frontend.cpp b/src/frontend/frontend.cpp
index 87d3a4f84..c0c50fe82 100644
--- a/src/frontend/frontend.cpp
+++ b/src/frontend/frontend.cpp
@@ -5,18 +5,22 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <atomic>
+#include <unordered_map>
 #include "frontend.h"
 #include "environment.h"
+#include "operator_info.h"
 
 namespace lean {
-
-static name g_overload_prefix(name(0u), "overload");
-
 /** \brief Implementation of the Lean frontend */
 struct frontend::imp {
+    // Remark: only named objects are stored in the dictionary.
+    typedef std::unordered_map<name, operator_info, name_hash, name_eq> operator_table;
     std::atomic<unsigned> m_num_children;
     std::shared_ptr<imp>  m_parent;
     environment           m_env;
+    operator_table        m_nud; // nud table for Pratt's parser
+    operator_table        m_led; // led table for Pratt's parser
+    operator_table        m_name_to_operator; // map internal names to operators (this is used for pretty printing)
 
     bool has_children() const { return m_num_children > 0; }
     void inc_children() { m_num_children++; }
diff --git a/src/frontend/operator_info.cpp b/src/frontend/operator_info.cpp
index 6306ff138..128dfdd61 100644
--- a/src/frontend/operator_info.cpp
+++ b/src/frontend/operator_info.cpp
@@ -30,6 +30,15 @@ struct operator_info::imp {
     imp(imp const & s):
         m_rc(1), m_fixity(s.m_fixity), m_assoc(s.m_assoc), m_precedence(s.m_precedence), m_op_parts(s.m_op_parts), m_names(s.m_names) {
     }
+
+    bool is_eq(imp const & other) const {
+        return
+            m_fixity == other.m_fixity &&
+            m_assoc == other.m_assoc &&
+            m_precedence == other.m_precedence &&
+            m_op_parts == other.m_op_parts;
+    }
+
 };
 
 operator_info::operator_info(imp * p):m_ptr(p) {}
@@ -62,6 +71,15 @@ list<name> const & operator_info::get_op_name_parts() const { lean_assert(m_ptr)
 
 operator_info operator_info::copy() const { return operator_info(new imp(*m_ptr)); }
 
+bool operator==(operator_info const & op1, operator_info const & op2) {
+    if ((op1.m_ptr == nullptr) != (op2.m_ptr == nullptr))
+        return false;
+    if (op1.m_ptr)
+        return op1.m_ptr->is_eq(*(op2.m_ptr));
+    else
+        return true;
+}
+
 operator_info infixr(name const & op, unsigned precedence) {
     return operator_info(new operator_info::imp(op, fixity::Infix,  associativity::Right, precedence));
 }
diff --git a/src/frontend/operator_info.h b/src/frontend/operator_info.h
index b373e59fe..cf8ceebc7 100644
--- a/src/frontend/operator_info.h
+++ b/src/frontend/operator_info.h
@@ -83,6 +83,9 @@ public:
 
     /** \brief Return a copy of the operator. */
     operator_info copy() const;
+
+    friend bool operator==(operator_info const & op1, operator_info const & op2);
+    friend bool operator!=(operator_info const & op1, operator_info const & op2) { return !(op1 == op2); }
 };
 operator_info infixl(name const & op, unsigned precedence);
 operator_info infixr(name const & op, unsigned precedence);
diff --git a/src/tests/util/list.cpp b/src/tests/util/list.cpp
index 3dfaa7c8b..07a333f13 100644
--- a/src/tests/util/list.cpp
+++ b/src/tests/util/list.cpp
@@ -17,7 +17,7 @@ static void tst1() {
         l = list<int>(i, l);
         lean_assert(!is_nil(l));
         lean_assert(car(l) == i);
-        lean_assert(cdr(l) == old);
+        lean_assert(is_eqp(cdr(l), old));
     }
     std::cout << l << "\n";
 }
@@ -45,9 +45,22 @@ static void tst3() {
     lean_assert(length(tail(list<int>(10, list<int>()))) == 0);
 }
 
+static void tst4() {
+    list<int> l1{1, 2, 3};
+    list<int> l2{1, 2, 3};
+    lean_assert(l1 == l2);
+    lean_assert(l1 != cons(1, l2));
+    lean_assert(l1 != tail(l1));
+    lean_assert(list<int>() == list<int>());
+    lean_assert(l2 != list<int>());
+    lean_assert(l1 != list<int>({1, 2, 3, 4}));
+    lean_assert(l1 != tail(list<int>{1, 2, 3, 4}));
+}
+
 int main() {
     tst1();
     tst2();
     tst3();
+    tst4();
     return has_violations() ? 1 : 0;
 }
diff --git a/src/util/list.h b/src/util/list.h
index ce54ff260..85d24367c 100644
--- a/src/util/list.h
+++ b/src/util/list.h
@@ -49,8 +49,22 @@ public:
     friend bool is_nil(list const & l) { return l.m_ptr == nullptr; }
     friend T const & head(list const & l) { lean_assert(!is_nil(l)); return l.m_ptr->m_head; }
     friend list const & tail(list const & l) { lean_assert(!is_nil(l)); return l.m_ptr->m_tail; }
-    friend bool operator==(list const & l1, list const & l2) { return l1.m_ptr == l2.m_ptr; }
-    friend bool operator!=(list const & l1, list const & l2) { return l1.m_ptr != l2.m_ptr; }
+
+    friend bool is_eqp(list const & l1, list const & l2) { return l1.m_ptr == l2.m_ptr; }
+    friend bool operator==(list const & l1, list const & l2) {
+        cell * it1 = l1.m_ptr;
+        cell * it2 = l2.m_ptr;
+        while (it1 != nullptr && it2 != nullptr) {
+            if (it1 == it2)
+                return true;
+            if (it1->m_head != it2->m_head)
+                return false;
+            it1 = it1->m_tail.m_ptr;
+            it2 = it2->m_tail.m_ptr;
+        }
+        return it1 == nullptr && it2 == nullptr;
+    }
+    friend bool operator!=(list const & l1, list const & l2) { return !(l1 == l2); }
 
     class iterator {
         friend class list;