feat(library): functional arrays

library/init/data/array.lean

@@ -0,0 +1,93 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.data.nat
+universes u w
+
+structure array (α : Type u) (n : nat) :=
+(data : fin n → α)
+
+def mk_array {α} (n) (v : α) : array α n :=
+{data := λ _, v}
+
+namespace array
+variables {α : Type u} {β : Type w} {n : nat}
+
+def read (a : array α n) (i : fin n) : α :=
+a^.data i
+
+def read' [inhabited α] (a : array α n) (i : nat) : α :=
+if h : i < n then a^.read ⟨i,h⟩ else default α
+
+def write (a : array α n) (i : fin n) (v : α) : array α n :=
+{data := λ j, if i = j then v else a^.read j}
+
+def write' (a : array α n) (i : nat) (v : α) : array α n :=
+if h : i < n then a^.write ⟨i, h⟩ v else a
+
+lemma push_back_idx {j n} : j < n + 1 → j ≠ n → j < n :=
+λ h₁ h₂, nat.lt_of_le_and_ne (nat.le_of_lt_succ h₁) h₂
+
+def push_back (a : array α n) (v : α) : array α (n+1) :=
+{data := λ ⟨j, h₁⟩, if h₂ : j = n then v else a^.read ⟨j, push_back_idx h₁ h₂⟩}
+
+lemma pop_back_idx {j n} : j < n → j < n + 1 :=
+λ h, nat.lt.step h
+
+def pop_back (a : array α (n+1)) : array α n :=
+{data := λ ⟨j, h⟩, a^.read ⟨j, pop_back_idx h⟩}
+
+lemma foreach_lt {a b c : nat} : a + c < b → a < b :=
+λ h, lt_of_le_of_lt (nat.le_add_right a c) h
+
+def foreach_aux (f : fin n → α → α) : Π (i : nat), i < n → array α n → array α n
+| 0     h a :=
+  let z : fin n := ⟨0, h⟩ in
+  a^.write z (f z (a^.read z))
+| (j+1) h a :=
+  let i : fin n := ⟨j+1, h⟩ in
+  have h' : j < n, from foreach_lt h,
+  foreach_aux j h' (a^.write i (f i (a^.read i)))
+
+def foreach : Π {n}, array α n → (fin n → α → α) → array α n
+| 0     a f:= a
+| (n+1) a f := foreach_aux f n  (nat.lt_succ_self _) a
+
+def map {α} {n} (f : α → α) (a : array α n) : array α n :=
+foreach a (λ _, f)
+
+def map₂ {α} {n} (f : α → α → α) (a b : array α n) : array α n :=
+foreach b (λ i, f (a^.read i))
+
+lemma fold_lt₁ {n} : n > 0 → n - 1 < n :=
+assume h,
+  have h₁ : 1 > 0, from dec_trivial,
+nat.sub_lt h h₁
+
+lemma fold_lt₂ {n i} : i + 1 < n → n - 2 - i < n  :=
+assume h,
+  have h₁ : 2 > 0,             from dec_trivial,
+  have h₂ : n > 0,             from lt.trans (nat.zero_lt_succ i) h,
+  have h₃ : n - 2 < n,         from nat.sub_lt h₂ h₁,
+  have h₄ : n - 2 - i ≤ n - 2, from nat.sub_le _ _,
+lt_of_le_of_lt h₄ h₃
+
+def fold_aux (f : α → β → β) : Π (i : nat), i < n → array α n → β → β
+| 0     h a b := f (a^.read ⟨n - 1, fold_lt₁ h⟩) b
+| (i+1) h a b := fold_aux i (foreach_lt h) a (f (a^.read ⟨n - 2 - i, fold_lt₂ h⟩) b)
+
+def fold : Π {n}, array α n → β → (α → β → β) → β
+| 0     a b fn := b
+| (n+1) a b fn := fold_aux fn n (nat.lt_succ_self _) a b
+
+protected def to_string [has_to_string α] (a : array α n) : string :=
+let p : string × bool := a^.fold ("", tt) (λ v ⟨r, first⟩, (r ++ if first then to_string v else ", " ++ to_string v, ff))
+in "[" ++ p.1 ++ "]"
+
+instance [has_to_string α] : has_to_string (array α n) :=
+⟨array.to_string⟩
+
+end array

library/init/data/default.lean

@@ -5,4 +5,4 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.data.basic init.data.sigma init.data.nat init.data.char init.data.string
-import init.data.list init.data.sum init.data.subtype init.data.int
+import init.data.list init.data.sum init.data.subtype init.data.int init.data.array

src/library/compiler/simp_inductive.cpp

@@ -169,7 +169,7 @@ class simp_inductive_fn : public compiler_step_visitor {
             get_constructor_info(cnames[i], rel_fields);
             auto p = visit_minor_premise(args[i+1], rel_fields);
             expr new_minor = p.first;
-            if (i == 0 && has_trivial_structure(I_name, rel_fields)) {
+            if (i == 0 && !is_builtin && has_trivial_structure(I_name, rel_fields)) {
                 /* Optimization for an inductive datatype that has a single constructor with only one relevant field */
                 return beta_reduce(mk_app(new_minor, args[0]));
             }
@@ -193,26 +193,30 @@ class simp_inductive_fn : public compiler_step_visitor {
     }
 
     expr visit_constructor(name const & fn, buffer<expr> const & args) {
-        bool is_builtin  = is_vm_builtin_function(fn);
-        name I_name      = *inductive::is_intro_rule(env(), fn);
-        unsigned nparams = *inductive::get_num_params(env(), I_name);
-        unsigned cidx    = get_constructor_idx(env(), fn);
-        buffer<bool> rel_fields;
-        get_constructor_info(fn, rel_fields);
-        lean_assert(args.size() == nparams + rel_fields.size());
-        buffer<expr> new_args;
-        for (unsigned i = 0; i < rel_fields.size(); i++) {
-            if (rel_fields[i]) {
-                new_args.push_back(visit(args[nparams + i]));
-            }
-        }
-        if (has_trivial_structure(I_name, rel_fields)) {
-            lean_assert(new_args.size() == 1);
-            return new_args[0];
-        } else if (is_builtin) {
+        if (is_vm_builtin_function(fn)) {
+            buffer<expr> new_args;
+            for (expr const & arg : args)
+                new_args.push_back(visit(arg));
             return mk_app(mk_constant(fn), new_args);
         } else {
-            return mk_app(mk_cnstr(cidx), new_args);
+            name I_name      = *inductive::is_intro_rule(env(), fn);
+            unsigned nparams = *inductive::get_num_params(env(), I_name);
+            unsigned cidx    = get_constructor_idx(env(), fn);
+            buffer<bool> rel_fields;
+            get_constructor_info(fn, rel_fields);
+            lean_assert(args.size() == nparams + rel_fields.size());
+            buffer<expr> new_args;
+            for (unsigned i = 0; i < rel_fields.size(); i++) {
+                if (rel_fields[i]) {
+                    new_args.push_back(visit(args[nparams + i]));
+                }
+            }
+            if (has_trivial_structure(I_name, rel_fields)) {
+                lean_assert(new_args.size() == 1);
+                return new_args[0];
+            } else {
+                return mk_app(mk_cnstr(cidx), new_args);
+            }
         }
     }
 

src/library/parray.h

@@ -0,0 +1,322 @@
+/*
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include <memory>
+#include <algorithm>
+#include "util/memory_pool.h"
+#include "util/debug.h"
+#include "util/buffer.h"
+#include "util/thread.h"
+
+namespace lean {
+
+template<typename T>
+class parray {
+    enum cell_kind { Set, PushBack, PopBack, Root };
+
+    static size_t capacity(T * vs) {
+        return vs == nullptr ? 0 : (reinterpret_cast<size_t*>(vs))[-1];
+    }
+
+    static T * allocate_raw_array(size_t c) {
+        size_t * mem = static_cast<size_t*>(malloc(sizeof(T)*c + sizeof(size_t)));
+        *mem = c;
+        ++mem;
+        T * r = reinterpret_cast<T*>(mem);
+        lean_assert(capacity(r) == c);
+        return r;
+    }
+
+    static void deallocate_raw_array(T * vs) {
+        if (vs == nullptr)
+            return;
+        size_t * mem = reinterpret_cast<size_t*>(vs);
+        --mem;
+        free(mem);
+    }
+
+    static void deallocate_array(T * vs, size_t sz) {
+        std::for_each(vs, vs + sz, [](T & e) { e.~T(); });
+        deallocate_raw_array(vs);
+    }
+
+    static T * expand(T * vs, size_t sz) {
+        size_t curr_capacity = capacity(vs);
+        size_t new_capacity  = curr_capacity == 0 ? 2 : (3 * curr_capacity + 1) >> 1;
+        T * new_vs           = allocate_raw_array(new_capacity);
+        std::uninitialized_copy(vs, vs + sz, new_vs);
+        deallocate_array(vs, sz);
+        return new_vs;
+    }
+
+    struct cell {
+        unsigned     m_rc;
+        cell_kind    m_kind;
+        union {
+            size_t   m_idx;
+            size_t   m_size;
+        };
+        T m_elem;
+        union {
+            cell  * m_next;
+            T *     m_values;
+        };
+
+        cell_kind kind() const { return static_cast<cell_kind>(m_kind); }
+        unsigned idx() const { lean_assert(kind() != Root); return m_idx; }
+        unsigned size() const { lean_assert(kind() == Root); return m_size; }
+        cell * next() const { lean_assert(kind() != Root); return m_next; }
+        T const & elem() const { lean_assert(kind() == Set || kind() == PushBack); return m_elem; }
+        cell():m_rc(1), m_kind(Root), m_size(0), m_values(0) {}
+    };
+
+    static memory_pool & get_allocator() {
+        LEAN_THREAD_PTR(memory_pool, g_allocator);
+        if (!g_allocator)
+            g_allocator = allocate_thread_memory_pool(sizeof(cell));
+        return *g_allocator;
+    }
+
+    static void deallocate_cell(cell * c) {
+        while (true) {
+            cell * next = nullptr;
+            switch (c->kind()) {
+            case Set:
+            case PushBack:
+            case PopBack:
+                next = c->next();
+                break;
+            case Root:
+                deallocate_array(c->m_values, c->m_size);
+                break;
+            }
+            c->~cell();
+            get_allocator().recycle(c);
+            if (next == nullptr)
+                return;
+            lean_assert(next->m_rc > 0);
+            next->m_rc--;
+            if (next->m_rc > 0)
+                return;
+            c = next;
+        }
+    }
+
+    static void inc_ref(cell * c) {
+        if (c == nullptr) return;
+        c->m_rc++;
+    }
+
+    static void dec_ref(cell * c) {
+        if (c == nullptr) return;
+        lean_assert(c->m_rc > 0);
+        c->m_rc--;
+        if (c->m_rc == 0)
+            deallocate_cell(c);
+    }
+
+    static cell * mk_cell() {
+        return new (get_allocator().allocate()) cell();
+    }
+
+    static void reroot(cell * r) {
+        lean_assert(r->m_rc > 0);
+        if (r->kind() == Root)
+            return;
+        buffer<cell *, 1024> cs;
+        size_t i = 0;
+        cell * c   = r;
+        while (c->kind() != Root) {
+            cs.push_back(c);
+            c = c->next();
+            i++;
+        }
+        cell * last = c;
+        size_t sz   = c->m_size;
+        T * vs      = c->m_values;
+        i           = cs.size();
+        while (i > 0) {
+            --i;
+            cell * p = cs[i];
+            lean_assert(p->kind() != Root);
+            lean_assert(p->m_next == c);
+            switch (p->kind()) {
+            case Set:
+                c->m_kind    = Set;
+                c->m_idx     = p->m_idx;
+                c->m_elem    = vs[c->m_idx];
+                vs[p->m_idx] = p->m_elem;
+                break;
+            case PushBack:
+                c->m_kind = PopBack;
+                if (sz == capacity(vs))
+                    vs = expand(vs, sz);
+                c->m_idx  = sz;
+                vs[sz]    = p->m_elem;
+                sz++;
+                break;
+            case PopBack:
+                c->m_kind = PushBack;
+                --sz;
+                c->m_idx  = sz;
+                c->m_elem = vs[sz];
+                break;
+            case Root:
+                lean_unreachable();
+                break;
+            }
+            c->m_next   = p;
+            c = p;
+        }
+        lean_assert(c == r);
+        r->m_kind   = Root;
+        r->m_values = vs;
+        r->m_size   = sz;
+        inc_ref(r);
+        dec_ref(last);
+    }
+
+    static T const & read(cell * c, size_t i) {
+        if (c->kind() != Root)
+            reroot(c);
+        lean_assert(c->kind() == Root);
+        lean_assert(i < c->size());
+        return c->m_values[i];
+    }
+
+    static size_t size(cell * c) {
+        if (c->kind() != Root)
+            reroot(c);
+        return c->size();
+    }
+
+    static cell * write(cell * c, size_t i, T const & v) {
+        if (c->kind() != Root)
+            reroot(c);
+        if (c->m_rc == 1) {
+            lean_assert(i < c->size());
+            c->m_values[i] = v;
+            return c;
+        } else {
+            cell * new_cell       = mk_cell();
+            new_cell->m_values    = c->m_values;
+            new_cell->m_size      = c->m_size;
+            c->m_kind             = Set;
+            c->m_idx              = i;
+            c->m_elem             = new_cell->m_values[i];
+            c->m_next             = new_cell;
+            c->m_rc--;
+            new_cell->m_rc++;
+            new_cell->m_values[i] = v;
+            return new_cell;
+        }
+    }
+
+    static void push_back_core(cell * c, T const & v) {
+        if (c->m_size == capacity(c->m_values))
+            c->m_values = expand(c->m_values, c->m_size);
+        new (c->m_values + c->m_size) T(v);
+        c->m_size++;
+    }
+
+    static cell * push_back(cell * c, T const & v) {
+        if (c->kind() != Root)
+            reroot(c);
+        if (c->m_rc == 1) {
+            push_back_core(c, v);
+            return c;
+        } else {
+            cell * new_cell       = mk_cell();
+            new_cell->m_values    = c->m_values;
+            new_cell->m_size      = c->m_size;
+            c->m_kind             = PopBack;
+            c->m_next             = new_cell;
+            c->m_rc--;
+            new_cell->m_rc++;
+            push_back_core(new_cell, v);
+            return new_cell;
+        }
+    }
+
+    static void pop_back_core(cell * c) {
+        lean_assert(c->m_size > 0);
+        c->m_size--;
+        c->m_values[c->m_size].~T();
+    }
+
+    static cell * pop_back(cell * c) {
+        if (c->kind() != Root)
+            reroot(c);
+        lean_assert(c->m_size > 0);
+        if (c->m_rc == 1) {
+            pop_back_core(c);
+            return c;
+        } else {
+            cell * new_cell       = mk_cell();
+            new_cell->m_values    = c->m_values;
+            new_cell->m_size      = c->m_size;
+            c->m_kind             = PushBack;
+            c->m_elem             = new_cell->m_values[c->m_size - 1];
+            c->m_next             = new_cell;
+            c->m_rc--;
+            new_cell->m_rc++;
+            pop_back_core(new_cell);
+            return new_cell;
+        }
+    }
+
+    cell * m_cell;
+public:
+    parray():m_cell(mk_cell()) {}
+    parray(size_t sz, T const & v):m_cell(mk_cell()) {
+        m_cell->m_size   = sz;
+        m_cell->m_values = allocate_raw_array(sz);
+        std::uninitialized_fill(m_cell->m_values, m_cell->m_values + sz, v);
+    }
+    parray(parray const & s):m_cell(s.m_cell) { if (m_cell) inc_ref(m_cell); }
+    parray(parray && s):m_cell(s.m_cell) { s.m_cell = nullptr; }
+    ~parray() { if (m_cell) dec_ref(m_cell); }
+
+    parray & operator=(parray const & s) {
+        if (s.m_cell)
+            inc_ref(s.m_cell);
+        cell * new_cell = s.m_cell;
+        if (m_cell)
+            dec_ref(m_cell);
+        m_cell = new_cell;
+        return *this;
+    }
+
+    parray & operator=(parray && s) {
+        if (m_cell)
+            dec_ref(m_cell);
+        m_cell = s.m_ptr;
+        s.m_ptr = nullptr;
+        return *this;
+    }
+
+    size_t size() const {
+        return size(m_cell);
+    }
+
+    T const & operator[](size_t i) const {
+        return read(m_cell, i);
+    }
+
+    void set(size_t i, T const & v) {
+        m_cell = write(m_cell, i, v);
+    }
+
+    void push_back(T const & v) {
+        m_cell = push_back(m_cell, v);
+    }
+
+    void pop_back() {
+        m_cell = pop_back(m_cell);
+    }
+};
+}

src/library/vm/CMakeLists.txt

@@ -1,4 +1,4 @@
 add_library(vm OBJECT vm.cpp optimize.cpp vm_nat.cpp vm_string.cpp vm_aux.cpp vm_io.cpp vm_name.cpp
   vm_options.cpp vm_format.cpp vm_rb_map.cpp vm_level.cpp vm_expr.cpp vm_exceptional.cpp
   vm_declaration.cpp vm_environment.cpp vm_list.cpp vm_pexpr.cpp vm_task.cpp
-  vm_native.cpp vm_int.cpp init_module.cpp vm_parser.cpp)
+  vm_native.cpp vm_int.cpp init_module.cpp vm_parser.cpp vm_array.cpp)

src/library/vm/init_module.cpp

@@ -23,6 +23,7 @@ Author: Leonardo de Moura
 #include "library/vm/vm_environment.h"
 #include "library/vm/vm_task.h"
 #include "library/vm/vm_parser.h"
+#include "library/vm/vm_array.h"
 
 namespace lean {
 void initialize_vm_core_module() {
@@ -45,8 +46,10 @@ void initialize_vm_core_module() {
     initialize_vm_declaration();
     initialize_vm_environment();
     initialize_vm_parser();
+    initialize_vm_array();
 }
 void finalize_vm_core_module() {
+    finalize_vm_array();
     finalize_vm_parser();
     finalize_vm_environment();
     finalize_vm_declaration();
@@ -73,6 +76,7 @@ void initialize_vm_module() {
     initialize_vm_expr_builtin_idxs();
     initialize_vm_exceptional_builtin_idxs();
     initialize_vm_format_builtin_idxs();
+    initialize_vm_array_builtin_idxs();
 }
 void finalize_vm_module() {
     finalize_vm();

src/library/vm/vm_array.cpp

@@ -0,0 +1,137 @@
+/*
+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/parray.h"
+#include "library/vm/vm.h"
+#include "library/vm/vm_nat.h"
+
+namespace lean {
+struct vm_array : public vm_external {
+    parray<vm_obj> m_array;
+    vm_array(parray<vm_obj> const & a):m_array(a) {}
+    virtual ~vm_array() {}
+    virtual void dealloc() override { this->~vm_array(); get_vm_allocator().deallocate(sizeof(vm_array), this); }
+    virtual vm_external * ts_clone(vm_clone_fn const &) override;
+    virtual vm_external * clone(vm_clone_fn const &) override { lean_unreachable(); }
+};
+
+/* Auxiliary object used by vm_array::ts_clone.
+   This is the "thread safe" version used when creating a ts_vm_obj that contains
+   a nested vm_array. */
+struct vm_array_ts_copy : public vm_external {
+    std::vector<vm_obj> m_entries;
+    virtual ~vm_array_ts_copy() {
+        /* The object ts_vm_obj manages the life cycle of all vm_obj's.
+           We should prevent this destructor from invoking the destructor of
+           vm_obj's nested in m_entries. */
+        for (auto & p : m_entries) {
+            p.steal_ptr();
+        }
+    }
+    virtual void dealloc() override { lean_unreachable(); }
+    virtual vm_external * ts_clone(vm_clone_fn const &) override { lean_unreachable(); }
+    virtual vm_external * clone(vm_clone_fn const &) override;
+};
+
+vm_external * vm_array::ts_clone(vm_clone_fn const & fn) {
+    vm_array_ts_copy * r = new vm_array_ts_copy();
+    size_t sz = m_array.size();
+    for (size_t i = 0; i < sz; i++) {
+        r->m_entries.emplace_back(fn(m_array[i]));
+    }
+    return r;
+}
+
+vm_external * vm_array_ts_copy::clone(vm_clone_fn const & fn) {
+    parray<vm_obj> array;
+    for (vm_obj const & p : m_entries) {
+        array.push_back(fn(p));
+    }
+    return new (get_vm_allocator().allocate(sizeof(vm_array))) vm_array(array);
+}
+
+parray<vm_obj> const & to_array(vm_obj const & o) {
+    lean_vm_check(dynamic_cast<vm_array*>(to_external(o)));
+    return static_cast<vm_array*>(to_external(o))->m_array;
+}
+
+vm_obj to_obj(parray<vm_obj> const & a) {
+    return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_array))) vm_array(a));
+}
+
+vm_obj array_read(vm_obj const &, vm_obj const &, vm_obj const & a, vm_obj const & i) {
+    /* TODO(Leo): handle case where n is too big */
+    unsigned idx = force_to_unsigned(i);
+    lean_vm_check(idx < to_array(a).size());
+    parray<vm_obj> const & _a = to_array(a);
+    return _a[idx];
+}
+
+vm_obj array_write(vm_obj const &, vm_obj const &, vm_obj const & a, vm_obj const & i, vm_obj const & v) {
+    /* TODO(Leo): handle case where n is too big */
+    unsigned idx = force_to_unsigned(i);
+    lean_vm_check(idx < to_array(a).size());
+    parray<vm_obj> _a = to_array(a);
+    _a.set(idx, v);
+    return to_obj(_a);
+}
+
+vm_obj array_push_back(vm_obj const &, vm_obj const &, vm_obj const & a, vm_obj const & v) {
+    parray<vm_obj> _a = to_array(a);
+    _a.push_back(v);
+    return to_obj(_a);
+}
+
+vm_obj array_pop_back(vm_obj const &, vm_obj const &, vm_obj const & a) {
+    parray<vm_obj> _a = to_array(a);
+    lean_vm_check(_a.size() != 0);
+    _a.pop_back();
+    return to_obj(_a);
+}
+
+vm_obj mk_array(vm_obj const &, vm_obj const & n, vm_obj const & v) {
+    /* TODO(Leo): handle case where n is too big */
+    unsigned _n = force_to_unsigned(n);
+    parray<vm_obj> a(_n, v);
+    return to_obj(a);
+}
+
+vm_obj array_mk(vm_obj const &, vm_obj const & n, vm_obj const & fn) {
+    /* TODO(Leo): handle case where n is too big */
+    unsigned _n = force_to_unsigned(n);
+    parray<vm_obj> a;
+    for (unsigned i = 0; i < _n; ++i) {
+        a.push_back(invoke(fn, mk_vm_nat(i)));
+    }
+    return to_obj(a);
+}
+
+static unsigned g_array_read_idx = -1;
+
+unsigned array_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
+    vm_obj d[3] = {o, mk_vm_unit(), mk_vm_unit()};
+    vm_obj fn = mk_vm_closure(g_array_read_idx, 3, d);
+    data.push_back(fn);
+    return 0;
+}
+
+void initialize_vm_array() {
+    DECLARE_VM_BUILTIN(name({"array", "mk"}),               array_mk);
+    DECLARE_VM_BUILTIN(name({"mk_array"}),                  mk_array);
+    DECLARE_VM_BUILTIN(name({"array", "read"}),             array_read);
+    DECLARE_VM_BUILTIN(name({"array", "write"}),            array_write);
+    DECLARE_VM_BUILTIN(name({"array", "push_back"}),        array_push_back);
+    DECLARE_VM_BUILTIN(name({"array", "pop_back"}),         array_pop_back);
+    DECLARE_VM_CASES_BUILTIN(name({"array", "cases_on"}),   array_cases_on);
+}
+
+void finalize_vm_array() {
+}
+
+void initialize_vm_array_builtin_idxs() {
+    g_array_read_idx = *get_vm_builtin_idx(name({"array", "read"}));
+}
+}

src/library/vm/vm_array.h

@@ -0,0 +1,12 @@
+/*
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+namespace lean {
+void initialize_vm_array();
+void finalize_vm_array();
+void initialize_vm_array_builtin_idxs();
+}

src/tests/library/CMakeLists.txt

@@ -14,3 +14,6 @@ add_exec_test(head_map "head_map")
 add_executable(delayed_abstraction delayed_abstraction.cpp ${library_tst_objs})
 target_link_libraries(delayed_abstraction ${EXTRA_LIBS})
 add_exec_test(delayed_abstraction "delayed_abstraction")
+add_executable(parray parray.cpp ${library_tst_objs})
+target_link_libraries(parray ${EXTRA_LIBS})
+add_exec_test(parray "parray")

src/tests/library/parray.cpp

@@ -0,0 +1,130 @@
+/*
+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 <random>
+#include <vector>
+#include "util/test.h"
+#include "util/init_module.h"
+#include "util/sexpr/init_module.h"
+#include "kernel/init_module.h"
+#include "library/init_module.h"
+#include "library/parray.h"
+using namespace lean;
+
+void tst1() {
+    parray<unsigned> a(10, 0);
+    lean_assert(a[0] == 0);
+    lean_assert(a.size() == 10);
+    parray<unsigned> b = a;
+    a.set(0, 1);
+    lean_assert(a[0] == 1);
+    lean_assert(a[1] == 0);
+    lean_assert(b[0] == 0);
+    lean_assert(a[0] == 1);
+}
+
+void driver(unsigned max_sz, unsigned max_val, unsigned num_it,
+            double push_back_freq,
+            double pop_back_freq,
+            double set_freq,
+            double copy_freq) {
+    parray<unsigned> v1;
+    std::vector<unsigned> v2;
+    std::mt19937   rng;
+    rng.seed(static_cast<unsigned int>(time(0)));
+    std::uniform_int_distribution<unsigned int> uint_dist;
+    std::vector<std::pair<parray<unsigned>, std::vector<unsigned>>> copies;
+    size_t acc_sz = 0;
+    for (unsigned i = 0; i < num_it; i++) {
+        acc_sz += v1.size();
+        double f = static_cast<double>(uint_dist(rng) % 10000) / 10000.0;
+        if (f < copy_freq) {
+            copies.emplace_back(v1, v2);
+        }
+        f = static_cast<double>(uint_dist(rng) % 10000) / 10000.0;
+        if (f < push_back_freq) {
+            if (v1.size() < max_sz) {
+                unsigned a = uint_dist(rng) % max_val;
+                v1.push_back(a);
+                v2.push_back(a);
+            }
+        }
+        if (v1.size() > 0) {
+            f = static_cast<double>(uint_dist(rng) % 10000) / 10000.0;
+            if (f < pop_back_freq) {
+                if (v1.size() >= max_sz)
+                    continue;
+                v1.pop_back();
+                v2.pop_back();
+            }
+        }
+        if (v1.size() > 0) {
+            f = static_cast<double>(uint_dist(rng) % 10000) / 10000.0;
+            if (f < set_freq) {
+                unsigned idx = uint_dist(rng) % v1.size();
+                unsigned a   = uint_dist(rng) % max_val;
+                v1.set(idx, a);
+                v2[idx] = a;
+            }
+        }
+        f = static_cast<double>(uint_dist(rng) % 10000) / 10000.0;
+        lean_assert(v1.size() == v2.size());
+        for (unsigned i = 0; i < v2.size(); i++) {
+            lean_assert(v1[i] == v2[i]);
+        }
+    }
+    for (std::pair<parray<unsigned>, std::vector<unsigned>> const & p : copies) {
+        lean_assert(p.first.size() == p.second.size());
+        for (unsigned i = 0; i < p.second.size(); i++) {
+            lean_assert(p.first[i] == p.second[i]);
+        }
+    }
+    std::cout << "\n";
+    std::cout << "Copies created:  " << copies.size() << "\n";
+    std::cout << "Average size:    " << static_cast<double>(acc_sz) / static_cast<double>(num_it) << "\n";
+}
+
+static void tst2() {
+    driver(4,  32, 10000, 0.5, 0.1, 0.5, 0.1);
+    driver(4,  32, 10000, 0.5, 0.1, 0.5, 0.1);
+    driver(4,  32, 10000, 0.5, 0.1, 0.5, 0.5);
+    driver(16, 16, 100000, 0.5, 0.5, 0.5, 0.01);
+    driver(16, 16, 100000, 0.5, 0.1, 0.5, 0.01);
+    driver(16, 16, 100000, 0.5, 0.6, 0.5, 0.01);
+    driver(16, 16, 10000, 0.5, 0.1, 0.5, 0.0);
+}
+
+static void tst3(unsigned n) {
+    parray<unsigned> v1;
+    v1.push_back(0);
+    parray<unsigned> v2 = v1;
+    for (unsigned i = 0; i < n; i++)
+        v1.push_back(i);
+    unsigned r = 0;
+    for (unsigned i = 0; i < n; i++)
+        r += v1[n - i - 1];
+    std::cout << ">> " << r << "\n";
+}
+
+int main() {
+    save_stack_info();
+    initialize_util_module();
+    initialize_sexpr_module();
+    initialize_kernel_module();
+    initialize_library_core_module();
+    initialize_library_module();
+
+    tst1();
+    tst2();
+    tst3(100000);
+
+    finalize_library_module();
+    finalize_library_core_module();
+    finalize_kernel_module();
+    finalize_sexpr_module();
+    finalize_util_module();
+    return has_violations() ? 1 : 0;
+}

tests/lean/run/array1.lean

@@ -0,0 +1,26 @@
+check @array.mk
+
+vm_eval mk_array 4 1
+
+def v : array nat 10 :=
+@array.mk nat 10 (λ ⟨i, _⟩, i)
+
+vm_eval array.map (+10) v
+
+def w : array nat 10 :=
+(mk_array 9 1)^.push_back 3
+
+def f : fin 10 → nat :=
+array.cases_on w (λ f, f)
+
+vm_eval f ⟨9, dec_trivial⟩
+vm_eval f ⟨2, dec_trivial⟩
+
+vm_eval (((mk_array 1 1)^.push_back 2)^.push_back 3)^.fold 0 (+)
+
+def array_sum {n} (a : array nat n) : nat :=
+a^.fold 0 (+)
+
+vm_eval array_sum (mk_array 10 1)
+
+vm_eval (mk_array 10 1)^.data ⟨1, dec_trivial⟩