feat(library/parray): add trace option for tracking destructive updates

src/library/CMakeLists.txt

@@ -18,4 +18,4 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
   locals.cpp normalize.cpp discr_tree.cpp
   mt_task_queue.cpp st_task_queue.cpp task_helper.cpp
   messages.cpp message_buffer.cpp versioned_msg_buf.cpp message_builder.cpp module_mgr.cpp comp_val.cpp
-  documentation.cpp check.cpp arith_instance.cpp)
+  documentation.cpp check.cpp arith_instance.cpp parray.cpp)

src/library/init_module.cpp

@@ -51,6 +51,7 @@ Author: Leonardo de Moura
 #include "library/defeq_canonizer.h"
 #include "library/congr_lemma.h"
 #include "library/check.h"
+#include "library/parray.h"
 
 namespace lean {
 void initialize_library_core_module() {
@@ -112,9 +113,11 @@ void initialize_library_module() {
     initialize_defeq_canonizer();
     initialize_check();
     initialize_congr_lemma();
+    initialize_parray();
 }
 
 void finalize_library_module() {
+    finalize_parray();
     finalize_congr_lemma();
     finalize_check();
     finalize_defeq_canonizer();

src/library/parray.cpp

@@ -0,0 +1,14 @@
+/*
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "library/trace.h"
+namespace lean {
+void initialize_parray() {
+    register_trace_class(name{"array", "update"});
+}
+void finalize_parray() {
+}
+}

src/library/parray.h

@@ -12,8 +12,11 @@ Author: Leonardo de Moura
 #include "util/debug.h"
 #include "util/buffer.h"
 #include "util/thread.h"
+#include "library/trace.h"
 
 namespace lean {
+// TODO(Leo) add compilation flag for enabling this trace message
+#define lean_array_trace(CODE) lean_trace(name({"array", "update"}), CODE)
 
 template<typename T>
 class parray {
@@ -199,10 +202,12 @@ class parray {
         if (c->kind() != Root)
             reroot(c);
         if (c->m_rc == 1) {
+            lean_array_trace(tout() << "destructive write at #" << i << "\n";);
             lean_assert(i < c->size());
             c->m_values[i] = v;
             return c;
         } else {
+            lean_array_trace(tout() << "non-destructive write at #" << i << "\n";);
             cell * new_cell       = mk_cell();
             new_cell->m_values    = c->m_values;
             new_cell->m_size      = c->m_size;
@@ -228,9 +233,11 @@ class parray {
         if (c->kind() != Root)
             reroot(c);
         if (c->m_rc == 1) {
+            lean_array_trace(tout() << "destructive push_back\n";);
             push_back_core(c, v);
             return c;
         } else {
+            lean_array_trace(tout() << "non-destructive push_back\n";);
             cell * new_cell       = mk_cell();
             new_cell->m_values    = c->m_values;
             new_cell->m_size      = c->m_size;
@@ -254,9 +261,11 @@ class parray {
             reroot(c);
         lean_assert(c->m_size > 0);
         if (c->m_rc == 1) {
+            lean_array_trace(tout() << "destructive pop_back\n";);
             pop_back_core(c);
             return c;
         } else {
+            lean_array_trace(tout() << "non-destructive pop_back\n";);
             cell * new_cell       = mk_cell();
             new_cell->m_values    = c->m_values;
             new_cell->m_size      = c->m_size;
@@ -324,4 +333,6 @@ public:
         return m_cell->m_rc;
     }
 };
+void initialize_parray();
+void finalize_parray();
 }