From bc69e7803f591dde077aa982ccd332e55ef3f7f5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 12 Sep 2013 11:18:26 -0700
Subject: [PATCH] Add support for writing a[i] = v instead of a.set(i, v) in
 the pdeque class.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/tests/util/pdeque.cpp | 21 +++++++++++++++++----
 src/util/pdeque.h         | 25 ++++++++++++++++++++-----
 2 files changed, 37 insertions(+), 9 deletions(-)

diff --git a/src/tests/util/pdeque.cpp b/src/tests/util/pdeque.cpp
index 5ae57bcbe0..99fafd45bf 100644
--- a/src/tests/util/pdeque.cpp
+++ b/src/tests/util/pdeque.cpp
@@ -67,7 +67,7 @@ static void tst1() {
     lean_assert(pop_back(push_back(q, 3)) == q);
 }
 
-static void driver(unsigned max_sz, unsigned max_val, unsigned num_ops, double push_freq, double copy_freq) {
+static void driver(unsigned max_sz, unsigned max_val, unsigned num_ops, double updt_freq, double copy_freq) {
     std::deque<int> q1;
     pdeque<int>     q2;
     pdeque<int>     q3;
@@ -84,18 +84,31 @@ static void driver(unsigned max_sz, unsigned max_val, unsigned num_ops, double p
             }
         }
         f = static_cast<double>(std::rand() % 10000) / 10000.0;
-        if (f < push_freq) {
+        if (f < updt_freq) {
             if (q1.size() >= max_sz)
                 continue;
             int v = std::rand() % max_val;
-            if (std::rand() % 2 == 0) {
+            switch (std::rand() % 3) {
+            case 0:
                 q1.push_front(v);
                 q2 = push_front(q2, v);
                 q3.push_front(v);
-            } else {
+                break;
+            case 1:
                 q1.push_back(v);
                 q2 = push_back(q2, v);
                 q3.push_back(v);
+                break;
+            default:
+                if (!empty(q2)) {
+                    unsigned idx = rand() % size(q2);
+                    q1[idx] = v;
+                    q2[idx] = v;
+                    q3[idx] = v;
+                    lean_assert(q1[idx] == q2[idx]);
+                    lean_assert(q1[idx] == q3[idx]);
+                }
+                break;
             }
         } else {
             if (q1.size() == 0)
diff --git a/src/util/pdeque.h b/src/util/pdeque.h
index c62cef6371..2ce8ee5cb9 100644
--- a/src/util/pdeque.h
+++ b/src/util/pdeque.h
@@ -264,7 +264,7 @@ public:
         \brief Access specified element
         \pre i < size()
     */
-    T const & operator[](unsigned i) const {
+    T const & get(unsigned i) const {
         lean_assert(i < size());
         cell const * it = m_ptr;
         unsigned input_i = i;
@@ -276,7 +276,7 @@ public:
                     if (const_cast<pdeque*>(this)->update_quota_on_read(cost))
                         return to_push_back(it).m_val;
                     else
-                        return operator[](input_i); // representation was updated
+                        return get(input_i); // representation was updated
                 }
                 break;
             case cell_kind::PushFront:
@@ -284,7 +284,7 @@ public:
                     if (const_cast<pdeque*>(this)->update_quota_on_read(cost))
                         return to_push_front(it).m_val;
                     else
-                        return operator[](input_i); // representation was updated
+                        return get(input_i); // representation was updated
                 } else {
                     i--;
                 }
@@ -299,14 +299,14 @@ public:
                     if (const_cast<pdeque*>(this)->update_quota_on_read(cost))
                         return to_set(it).m_val;
                     else
-                        return operator[](input_i); // representation was updated
+                        return get(input_i); // representation was updated
                 }
                 break;
             case cell_kind::Root:
                 if (const_cast<pdeque*>(this)->update_quota_on_read(cost))
                     return to_root(it).m_deque[i];
                 else
-                    return operator[](input_i); // representation was updated
+                    return get(input_i); // representation was updated
             }
             it = static_cast<delta_cell const *>(it)->m_prev;
             cost++;
@@ -432,6 +432,8 @@ public:
         switch (m_ptr->kind()) {
         case cell_kind::PushBack:
         case cell_kind::PopBack:
+        case cell_kind::PushFront:
+        case cell_kind::PopFront:
             set_core(i, v);
             break;
         case cell_kind::Set:
@@ -449,6 +451,19 @@ public:
         }
     }
 
+    class ref {
+        pdeque  &  m_deque;
+        unsigned   m_idx;
+    public:
+        ref(pdeque & v, unsigned i):m_deque(v), m_idx(i) {}
+        ref & operator=(T const & a) { m_deque.set(m_idx, a); return *this; }
+        operator T const &() const { return m_deque.get(m_idx); }
+    };
+
+    T const & operator[](unsigned i) const { return get(i); }
+
+    ref operator[](unsigned i) { return ref(*this, i); }
+
     class iterator {
         friend class pdeque;
         pdeque const & m_deque;