From 2265ef78c46838cda4348bb7ab51529b106a14ea Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 19 Nov 2013 16:27:31 -0800
Subject: [PATCH] feat(util/list): add emplace_front

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/tests/util/list.cpp | 15 +++++++++++++++
 src/util/list.h         |  9 +++++++++
 2 files changed, 24 insertions(+)

diff --git a/src/tests/util/list.cpp b/src/tests/util/list.cpp
index 06dbc06b37..a246c28c12 100644
--- a/src/tests/util/list.cpp
+++ b/src/tests/util/list.cpp
@@ -146,6 +146,20 @@ static void tst11(int sz, int num) {
     lean_assert(l == l2);
 }
 
+static void tst12() {
+    list<std::pair<int, char const *>> l;
+    lean_assert(is_nil(l));
+    l.emplace_front(20, "world");
+    l.emplace_front(10, "hello");
+    int sum = 0;
+    for (auto p : l) {
+        sum += p.first;
+        std::cout << p.second << " ";
+    }
+    std::cout << "\n";
+    lean_assert(sum == 30);
+}
+
 int main() {
     tst1();
     tst2();
@@ -158,5 +172,6 @@ int main() {
     tst9(100);
     tst10(1000, 5);
     tst11(1000, 5);
+    tst12();
     return has_violations() ? 1 : 0;
 }
diff --git a/src/util/list.h b/src/util/list.h
index 78eb29fa18..33321b1326 100644
--- a/src/util/list.h
+++ b/src/util/list.h
@@ -21,6 +21,8 @@ public:
         MK_LEAN_RC()
         T      m_head;
         list   m_tail;
+        template<typename... Fields>
+        cell(bool, list const & t, Fields&&... head):m_rc(1), m_head(head...), m_tail(t) {}
     public:
         cell(T const & h, list const & t):m_rc(1), m_head(h), m_tail(t) {}
         ~cell() {}
@@ -88,6 +90,13 @@ public:
     friend bool is_eqp(list const & l1, list const & l2) { return l1.m_ptr == l2.m_ptr; }
     friend bool is_eqp(list const & l1, cell const * l2) { return l1.m_ptr == l2; }
 
+    template<typename... Args>
+    void emplace_front(Args&&... args) {
+        cell * new_ptr = new cell(true, *this, args...);
+        if (m_ptr) m_ptr->dec_ref();
+        m_ptr = new_ptr;
+    }
+
     /** \brief Structural equality. */
     friend bool operator==(list const & l1, list const & l2) {
         cell * it1 = l1.m_ptr;