From acade175b61513f8189bc8a7605bdaa49ddfe6dc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 3 May 2018 15:39:18 -0700 Subject: [PATCH] feat(library/init/data/array): store dimension in the array The array dimension is now stored inside the array. The main motivation is that it reflects the actual runtime implementation. We need to store the array size to be able to GC it. So, it feels silly to have the array size stored in each array object, but we cannot use this information. For example, in the `hashmap` we implemented the bucket array using `array`, and we store the `size` of the array. Same for the Lean3 `buffer` object. The `buffer` object doesn't even need to exist. The actual `array` implementation is the `buffer` --- library/init/data/array/basic.lean | 202 ++++++++++++++------------- library/init/data/array/default.lean | 2 +- library/init/data/hashmap/basic.lean | 73 +++++----- src/library/vm/vm_array.cpp | 59 ++++---- tests/lean/run/array1.lean | 27 ++++ 5 files changed, 200 insertions(+), 163 deletions(-) create mode 100644 tests/lean/run/array1.lean diff --git a/library/init/data/array/basic.lean b/library/init/data/array/basic.lean index e94dab6075..822ba12fe8 100644 --- a/library/init/data/array/basic.lean +++ b/library/init/data/array/basic.lean @@ -1,133 +1,137 @@ /- -Copyright (c) 2017 Microsoft Corporation. All rights reserved. +Copyright (c) 2018 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura, Mario Carneiro +Authors: Leonardo de Moura -/ prelude -import init.data.nat.basic init.data.fin.basic +import init.data.nat.basic init.data.fin.basic init.data.usize init.data.repr init.function universes u v w -/- In the VM, d_array is implemented a persistent array. -/ -structure d_array (n : nat) (α : fin n → Type u) := -(data : Π i : fin n, α i) +/- +The compiler has special support for arrays. +They are implemented as a dynamic array. +-/ -namespace d_array -variables {n : nat} {α : fin n → Type u} {β : Type v} +structure array (α : Type u) := +(sz : nat) +(data : fin sz → α) -def nil {α} : d_array 0 α := -{data := λ ⟨x, h⟩, absurd h (nat.not_lt_zero x)} +/- TODO: mark as builtin -/ +def mk_array {α : Type u} (n : nat) (v : α) : array α := +{ sz := n, + data := λ _, v} -/- has builtin VM implementation -/ -def read (a : d_array n α) (i : fin n) : α i := -a.data i - -/- has builtin VM implementation -/ -def write (a : d_array n α) (i : fin n) (v : α i) : d_array n α := -{data := λ j, if h : i = j then eq.rec_on h v else a.read j} - -def iterate_aux (a : d_array n α) (f : Π i : fin n, α i → β → β) : Π (i : nat), i ≤ n → β → β -| 0 h b := b -| (j+1) h b := - let i : fin n := ⟨j, h⟩ in - f i (a.read i) (iterate_aux j (nat.le_of_lt h) b) - -/- has builtin VM implementation -/ -def iterate (a : d_array n α) (b : β) (f : Π i : fin n, α i → β → β) : β := -iterate_aux a f n (nat.le_refl _) b - -/- has builtin VM implementation -/ -def foreach (a : d_array n α) (f : Π i : fin n, α i → α i) : d_array n α := -iterate a a $ λ i v a', a'.write i (f i v) - -def map (f : Π i : fin n, α i → α i) (a : d_array n α) : d_array n α := -foreach a f - -def map₂ (f : Π i : fin n, α i → α i → α i) (a b : d_array n α) : d_array n α := -foreach b (λ i, f i (a.read i)) - -def foldl (a : d_array n α) (b : β) (f : Π i : fin n, α i → β → β) : β := -iterate a b f - -def rev_iterate_aux (a : d_array n α) (f : Π i : fin n, α i → β → β) : Π (i : nat), i ≤ n → β → β -| 0 h b := b -| (j+1) h b := - let i : fin n := ⟨j, h⟩ in - rev_iterate_aux j (nat.le_of_lt h) (f i (a.read i) b) - -def rev_iterate (a : d_array n α) (b : β) (f : Π i : fin n, α i → β → β) : β := -rev_iterate_aux a f n (nat.le_refl _) b - -end d_array - -def array (n : nat) (α : Type u) : Type u := -d_array n (λ _, α) - -/- has builtin VM implementation -/ -def mk_array {α} (n) (v : α) : array n α := -{data := λ _, v} +theorem sz_mk_array_eq {α : Type u} (n : nat) (v : α) : (mk_array n v).sz = n := +rfl namespace array -variables {n : nat} {α : Type u} {β : Type v} +variables {α : Type u} {β : Type v} -def nil {α} : array 0 α := -d_array.nil +/- TODO: mark as builtin -/ +def nil : array α := +{ sz := 0, + data := λ ⟨x, h⟩, absurd h (nat.not_lt_zero x) } -def read (a : array n α) (i : fin n) : α := -d_array.read a i +def empty (a : array α) : bool := +a.sz = 0 -def write (a : array n α) (i : fin n) (v : α) : array n α := -d_array.write a i v +/- TODO: mark as builtin -/ +def read (a : array α) (i : fin a.sz) : α := +a.data i -def iterate (a : array n α) (b : β) (f : fin n → α → β → β) : β := -d_array.iterate a b f +/- TODO: mark as builtin -/ +def write (a : array α) (i : fin a.sz) (v : α) : array α := +{ sz := a.sz, + data := λ j, if h : i = j then v else a.data j } -def foreach (a : array n α) (f : fin n → α → α) : array n α := -iterate a a (λ i v a', a'.write i (f i v)) +theorem sz_write_eq (a : array α) (i : fin a.sz) (v : α) : (write a i v).sz = a.sz := +rfl -def map (f : α → α) (a : array n α) : array n α := -foreach a (λ _, f) +/- TODO: add builtin -/ +def read' [inhabited α] (a : array α) (i : nat) : α := +if h : i < a.sz then a.read ⟨i, h⟩ else default α -def map₂ (f : α → α → α) (a b : array n α) : array n α := -foreach b (λ i, f (a.read i)) +/- TODO: add builtin -/ +def write' (a : array α) (i : nat) (v : α) : array α := +if h : i < a.sz then a.write ⟨i, h⟩ v else a -def foldl (a : array n α) (b : β) (f : α → β → β) : β := +/- TODO: add builtin -/ +def uread [inhabited α] (a : array α) (i : usize) : α := +if h : i.val < a.sz then a.read ⟨i.val, h⟩ else default α + +/- TODO: add builtin -/ +def uwrite (a : array α) (i : usize) (v : α) : array α := +if h : i.val < a.sz then a.write ⟨i.val, h⟩ v else a + +/- TODO: mark as builtin -/ +def push (a : array α) (v : α) : array α := +{ sz := nat.succ a.sz, + data := λ ⟨j, h₁⟩, + if h₂ : j = a.sz then v + else a.data ⟨j, nat.lt_of_le_of_ne (nat.le_of_lt_succ h₁) h₂⟩ } + +/- TODO: mark as builtin -/ +def pop (a : array α) : array α := +{ sz := nat.pred a.sz, + data := λ ⟨j, h⟩, a.read ⟨j, nat.lt_of_lt_of_le h (nat.pred_le _)⟩ } + +private def iterate_aux (a : array α) (f : Π i : fin a.sz, α → β → β) : Π (i : nat), i ≤ a.sz → β → β +| 0 h b := b +| (j+1) h b := + let i : fin a.sz := ⟨j, h⟩ in + f i (a.read i) (iterate_aux j (nat.le_of_lt h) b) + +/- TODO : mark as builtin -/ +def iterate (a : array α) (b : β) (f : Π i : fin a.sz, α → β → β) : β := +iterate_aux a f a.sz (nat.le_refl _) b + +def foldl (a : array α) (b : β) (f : α → β → β) : β := iterate a b (λ _, f) -def rev_list (a : array n α) : list α := -a.foldl [] (::) +private def rev_iterate_aux (a : array α) (f : Π i : fin a.sz, α → β → β) : Π (i : nat), i ≤ a.sz → β → β +| 0 h b := b +| (j+1) h b := + let i : fin a.sz := ⟨j, h⟩ in + rev_iterate_aux j (nat.le_of_lt h) (f i (a.read i) b) -def rev_iterate (a : array n α) (b : β) (f : fin n → α → β → β) : β := -d_array.rev_iterate a b f +/- TODO: mark as builtin -/ +def rev_iterate (a : array α) (b : β) (f : Π i : fin a.sz, α → β → β) : β := +rev_iterate_aux a f a.sz (nat.le_refl _) b -def rev_foldl (a : array n α) (b : β) (f : α → β → β) : β := +def rev_foldl (a : array α) (b : β) (f : α → β → β) : β := rev_iterate a b (λ _, f) -def to_list (a : array n α) : list α := +def to_list (a : array α) : list α := a.rev_foldl [] (::) -theorem push_back_idx {j n} (h₁ : j < n + 1) (h₂ : j ≠ n) : j < n := -nat.lt_of_le_of_ne (nat.le_of_lt_succ h₁) h₂ +instance [has_repr α] : has_repr (array α) := +⟨repr ∘ to_list⟩ -/- has builtin VM implementation -/ -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₂⟩} +private def foreach_aux (a : array α) (f : Π i : fin a.sz, α → α) : { a' : array α // a'.sz = a.sz } := +iterate a ⟨a, rfl⟩ $ λ i v ⟨a', h⟩, + let i' : fin a'.sz := eq.rec_on h.symm i in + ⟨a'.write i' (f i v), (sz_write_eq a' i' (f i v)) ▸ h⟩ -theorem pop_back_idx {j n} (h : j < n) : j < n + 1 := -nat.lt.step h +/- TODO : mark as builtin -/ +def foreach (a : array α) (f : Π i : fin a.sz, α → α) : array α := +(foreach_aux a f).val -/- has builtin VM implementation -/ -def pop_back (a : array (n+1) α) : array n α := -{data := λ ⟨j, h⟩, a.read ⟨j, pop_back_idx h⟩} +theorem sz_foreach_eq (a : array α) (f : Π i : fin a.sz, α → α) : (foreach a f).sz = a.sz := +(foreach_aux a f).property -protected def mem (v : α) (a : array n α) : Prop := -∃ i : fin n, read a i = v +def map (f : α → α) (a : array α) : array α := +foreach a (λ _, f) -instance : has_mem α (array n α) := ⟨array.mem⟩ - -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 : nat) (v : α) : array n α := -if h : i < n then a.write ⟨i, h⟩ v else a +def map₂ (f : α → α → α) (a b : array α) : array α := +if h : a.sz ≤ b.sz +then foreach a (λ ⟨i, h'⟩, f (b.read ⟨i, nat.lt_of_lt_of_le h' h⟩)) +else foreach b (λ ⟨i, h'⟩, f (a.read ⟨i, nat.lt_trans h' (nat.gt_of_not_le h)⟩)) end array + +def list.to_array_aux {α : Type u} : list α → array α → array α +| [] r := r +| (a::as) r := list.to_array_aux as (r.push a) + +def list.to_array {α : Type u} (l : list α) : array α := +l.to_array_aux array.nil diff --git a/library/init/data/array/default.lean b/library/init/data/array/default.lean index 05427fa21e..0760a52cf6 100644 --- a/library/init/data/array/default.lean +++ b/library/init/data/array/default.lean @@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Gabriel Ebner -/ prelude -import init.data.array.basic init.data.array.lemmas +import init.data.array.basic diff --git a/library/init/data/hashmap/basic.lean b/library/init/data/hashmap/basic.lean index df7e4b71b9..ec9a78463e 100644 --- a/library/init/data/hashmap/basic.lean +++ b/library/init/data/hashmap/basic.lean @@ -7,24 +7,29 @@ prelude import init.data.array.basic init.data.list.basic init.data.option.basic universes u v w -def bucket_array (α : Type u) (β : α → Type v) (n : nat) := -array n (list (Σ a, β a)) +def bucket_array (α : Type u) (β : α → Type v) := +{ b : array (list (Σ a, β a)) // b.sz > 0 } + +def bucket_array.write {α : Type u} {β : α → Type v} (data : bucket_array α β) (i : fin data.val.sz) (d : list (Σ a, β a)) : bucket_array α β := +⟨ data.val.write i d, + calc (data.val.write i d).sz = data.val.sz : array.sz_write_eq _ _ _ + ... > 0 : data.property ⟩ structure hashmap_imp (α : Type u) (β : α → Type v) := -(size nbuckets : nat) -(nz_buckets : nbuckets > 0) -(buckets : bucket_array α β nbuckets) +(size : nat) +(buckets : bucket_array α β) def mk_hashmap_imp {α : Type u} {β : α → Type v} (nbuckets := 8) : hashmap_imp α β := let n := if nbuckets = 0 then 8 else nbuckets in { size := 0, - nbuckets := n, - nz_buckets := show (if nbuckets = 0 then 8 else nbuckets) > 0, from - match nbuckets with - | 0 := nat.zero_lt_succ _ - | (nat.succ x) := nat.zero_lt_succ _ - end, - buckets := mk_array n [] } + buckets := + ⟨ mk_array n [], + calc (mk_array n []).sz = n : sz_mk_array_eq _ _ + ... = if nbuckets = 0 then 8 else nbuckets : rfl + ... > 0 : + match nbuckets with + | 0 := nat.zero_lt_succ _ + | (nat.succ x) := nat.zero_lt_succ _ ⟩ } namespace hashmap_imp variables {α : Type u} {β : α → Type v} @@ -32,12 +37,12 @@ variables {α : Type u} {β : α → Type v} def mk_idx {n : nat} (h : n > 0) (i : nat) : fin n := ⟨i % n, nat.mod_lt _ h⟩ -def reinsert_aux (hash_fn : α → nat) {n : nat} (h : n > 0) (data : bucket_array α β n) (a : α) (b : β a) : bucket_array α β n := -let bidx := mk_idx h (hash_fn a) in -data.write bidx (⟨a, b⟩ :: data.read bidx) +def reinsert_aux (hash_fn : α → nat) (data : bucket_array α β) (a : α) (b : β a) : bucket_array α β := +let bidx := mk_idx data.property (hash_fn a) in +data.write bidx (⟨a, b⟩ :: data.val.read bidx) -def fold_buckets {δ : Type w} {n : nat} (data : bucket_array α β n) (d : δ) (f : δ → Π a, β a → δ) : δ := -data.foldl d (λ b d, b.foldl (λ r (p : Σ a, β a), f r p.1 p.2) d) +def fold_buckets {δ : Type w} (data : bucket_array α β) (d : δ) (f : δ → Π a, β a → δ) : δ := +data.val.foldl d (λ b d, b.foldl (λ r (p : Σ a, β a), f r p.1 p.2) d) def find_aux [decidable_eq α] (a : α) : list (Σ a, β a) → option (β a) | [] := none @@ -49,9 +54,8 @@ def contains_aux [decidable_eq α] (a : α) (l : list (Σ a, β a)) : bool := def find [decidable_eq α] (hash_fn : α → nat) (m : hashmap_imp α β) (a : α) : option (β a) := match m with -| ⟨_, nbuckets, nz, buckets⟩ := +| ⟨_, buckets, nz⟩ := find_aux a (buckets.read (mk_idx nz (hash_fn a))) -end def fold {δ : Type w} (m : hashmap_imp α β) (d : δ) (f : δ → Π a, β a → δ) : δ := fold_buckets m.buckets d f @@ -66,31 +70,28 @@ def erase_aux [decidable_eq α] (a : α) : list (Σ a, β a) → list (Σ a, β def insert [decidable_eq α] (hash_fn : α → nat) (m : hashmap_imp α β) (a : α) (b : β a) : hashmap_imp α β := match m with -| ⟨size, nbuckets, nz, buckets⟩ := - let bidx := mk_idx nz (hash_fn a) in - let bkt := buckets.read bidx in +| ⟨size, buckets⟩ := + let bidx := mk_idx buckets.property (hash_fn a) in + let bkt := buckets.val.read bidx in if contains_aux a bkt - then ⟨size, nbuckets, nz, buckets.write bidx (replace_aux a b bkt)⟩ + then ⟨size, buckets.write bidx (replace_aux a b bkt)⟩ else let size' := size + 1 in let buckets' := buckets.write bidx (⟨a, b⟩::bkt) in - if size' <= nbuckets - then ⟨size', nbuckets, nz, buckets'⟩ - else let nbuckets' := nbuckets * 2 in - let nz' : nbuckets' > 0 := nat.mul_pos nz (nat.zero_lt_bit0 nat.one_ne_zero) in - ⟨size', nbuckets', nz', - fold_buckets buckets' (mk_array nbuckets' []) $ - λ r a b, reinsert_aux hash_fn nz' r a b⟩ -end + if size' <= buckets.val.sz + then ⟨size', buckets'⟩ + else let nbuckets' := buckets.val.sz * 2 in + let nz' : nbuckets' > 0 := nat.mul_pos buckets.property (nat.zero_lt_bit0 nat.one_ne_zero) in + ⟨ size', + fold_buckets buckets' ⟨mk_array nbuckets' [], nz'⟩ (reinsert_aux hash_fn) ⟩ def erase [decidable_eq α] (hash_fn : α → nat) (m : hashmap_imp α β) (a : α) : hashmap_imp α β := match m with -| ⟨size, nbuckets, nz, buckets⟩ := - let bidx : fin nbuckets := ⟨hash_fn a % nbuckets, nat.mod_lt _ nz⟩ in - let bkt := buckets.read bidx in +| ⟨ size, buckets ⟩ := + let bidx := mk_idx buckets.property (hash_fn a) in + let bkt := buckets.val.read bidx in if contains_aux a bkt - then ⟨size - 1, nbuckets, nz, buckets.write bidx $ erase_aux a bkt⟩ + then ⟨size - 1, buckets.write bidx $ erase_aux a bkt⟩ else m -end inductive well_formed [decidable_eq α] (hash_fn : α → nat) : hashmap_imp α β → Prop | mk_wff : ∀ n, well_formed (mk_hashmap_imp n) diff --git a/src/library/vm/vm_array.cpp b/src/library/vm/vm_array.cpp index 3c7a36b8be..72247d2ef1 100644 --- a/src/library/vm/vm_array.cpp +++ b/src/library/vm/vm_array.cpp @@ -63,16 +63,20 @@ vm_obj to_obj(parray const & a) { return mk_vm_external(new vm_array(a)); } -vm_obj d_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 */ +vm_obj array_sz(vm_obj const &, vm_obj const & a) { + return mk_vm_nat(to_array(a).size()); +} + +vm_obj array_read(vm_obj const &, vm_obj const & a, vm_obj const & i) { + /* TODO(Leo): handle case where i is too big */ unsigned idx = force_to_unsigned(i); lean_vm_check(idx < to_array(a).size()); parray const & _a = to_array(a); return _a[idx]; } -vm_obj d_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 */ +vm_obj array_write(vm_obj const &, vm_obj const & a, vm_obj const & i, vm_obj const & v) { + /* TODO(Leo): handle case where i is too big */ unsigned idx = force_to_unsigned(i); parray const & p = to_array(a); lean_vm_check(idx < p.size()); @@ -86,7 +90,7 @@ vm_obj d_array_write(vm_obj const &, vm_obj const &, vm_obj const & a, vm_obj co } } -vm_obj array_push_back(vm_obj const &, vm_obj const &, vm_obj const & a, vm_obj const & v) { +vm_obj array_push(vm_obj const &, vm_obj const & a, vm_obj const & v) { parray const & p = to_array(a); if (a.raw()->get_rc() == 1) { const_cast &>(p).push_back(v); @@ -98,7 +102,7 @@ vm_obj array_push_back(vm_obj const &, vm_obj const &, vm_obj const & a, vm_obj } } -vm_obj array_pop_back(vm_obj const &, vm_obj const &, vm_obj const & a) { +vm_obj array_pop(vm_obj const &, vm_obj const & a) { parray const & p = to_array(a); if (a.raw()->get_rc() == 1) { const_cast &>(p).pop_back(); @@ -117,7 +121,7 @@ vm_obj mk_array(vm_obj const & /* alpha */, vm_obj const & n, vm_obj const & v) return to_obj(a); } -vm_obj d_array_mk(vm_obj const & n, vm_obj const & /* alpha */, vm_obj const & fn) { +vm_obj array_mk(vm_obj const & /* alpha */, vm_obj const & n, vm_obj const & fn) { /* TODO(Leo): handle case where n is too big */ unsigned _n = force_to_unsigned(n); parray a; @@ -127,10 +131,10 @@ vm_obj d_array_mk(vm_obj const & n, vm_obj const & /* alpha */, vm_obj const & f return to_obj(a); } -vm_obj d_array_foreach(vm_obj const & n, vm_obj const & /* alpha */, vm_obj const & a, vm_obj const & fn) { +vm_obj array_foreach(vm_obj const & /* alpha */, vm_obj const & a, vm_obj const & fn) { /* TODO(Leo): handle case where n is too big */ - unsigned _n = force_to_unsigned(n); parray const & p = to_array(a); + unsigned _n = p.size(); if (a.raw()->get_rc() == 1) { parray & _p = const_cast &>(p); for (unsigned i = 0; i < _n; i++) @@ -145,11 +149,10 @@ vm_obj d_array_foreach(vm_obj const & n, vm_obj const & /* alpha */, vm_obj cons } } -vm_obj d_array_iterate(vm_obj const & n, vm_obj const & /* alpha */, vm_obj const & /* beta */, - vm_obj const & a, vm_obj const & b, vm_obj const & fn) { - /* TODO(Leo): handle case where n is too big */ - unsigned _n = force_to_unsigned(n); +vm_obj array_iterate(vm_obj const & /* alpha */, vm_obj const & /* beta */, + vm_obj const & a, vm_obj const & b, vm_obj const & fn) { parray const & p = to_array(a); + unsigned _n = p.size(); vm_obj r = b; for (unsigned i = 0; i < _n; i++) r = invoke(fn, mk_vm_nat(i), p[i], r); @@ -158,30 +161,32 @@ vm_obj d_array_iterate(vm_obj const & n, vm_obj const & /* alpha */, vm_obj cons static unsigned g_array_read_idx = -1; -unsigned d_array_cases_on(vm_obj const & o, buffer & data) { - vm_obj d[3] = {o, mk_vm_unit(), mk_vm_unit()}; - vm_obj fn = mk_vm_closure(g_array_read_idx, 3, d); +unsigned array_cases_on(vm_obj const & o, buffer & data) { + vm_obj d[2] = {o, mk_vm_unit()}; + vm_obj fn = mk_vm_closure(g_array_read_idx, 2, d); + data.push_back(mk_vm_nat(to_array(o).size())); data.push_back(fn); return 0; } void initialize_vm_array() { - DECLARE_VM_BUILTIN(name({"d_array", "mk"}), d_array_mk); - DECLARE_VM_BUILTIN(name({"mk_array"}), mk_array); - DECLARE_VM_BUILTIN(name({"d_array", "data"}), d_array_read); - DECLARE_VM_BUILTIN(name({"d_array", "read"}), d_array_read); - DECLARE_VM_BUILTIN(name({"d_array", "write"}), d_array_write); - DECLARE_VM_BUILTIN(name({"array", "push_back"}), array_push_back); - DECLARE_VM_BUILTIN(name({"array", "pop_back"}), array_pop_back); - DECLARE_VM_BUILTIN(name({"d_array", "foreach"}), d_array_foreach); - DECLARE_VM_BUILTIN(name({"d_array", "iterate"}), d_array_iterate); - DECLARE_VM_CASES_BUILTIN(name({"d_array", "cases_on"}), d_array_cases_on); + DECLARE_VM_BUILTIN(name({"array", "mk"}), array_mk); + DECLARE_VM_BUILTIN(name({"mk_array"}), mk_array); + DECLARE_VM_BUILTIN(name({"array", "sz"}), array_sz); + DECLARE_VM_BUILTIN(name({"array", "data"}), array_read); + DECLARE_VM_BUILTIN(name({"array", "read"}), array_read); + DECLARE_VM_BUILTIN(name({"array", "write"}), array_write); + DECLARE_VM_BUILTIN(name({"array", "push"}), array_push); + DECLARE_VM_BUILTIN(name({"array", "pop"}), array_pop); + DECLARE_VM_BUILTIN(name({"array", "foreach"}), array_foreach); + DECLARE_VM_BUILTIN(name({"array", "iterate"}), array_iterate); + 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({"d_array", "read"})); + g_array_read_idx = *get_vm_builtin_idx(name({"array", "read"})); } } diff --git a/tests/lean/run/array1.lean b/tests/lean/run/array1.lean new file mode 100644 index 0000000000..f0d80552f0 --- /dev/null +++ b/tests/lean/run/array1.lean @@ -0,0 +1,27 @@ +#check @array.mk + +#eval mk_array 4 1 + +def v : array nat := @array.mk nat 10 (λ ⟨i, _⟩, i) + +#eval array.map (+10) v + +def w : array nat := +(mk_array 9 1).push 3 + +def f : fin w.sz → nat := +array.cases_on w (λ _ f, f) + +#eval f ⟨1, sorry⟩ +#eval f ⟨9, sorry⟩ + +#eval (((mk_array 1 1).push 2).push 3).foldl 0 (+) + +def array_sum (a : array nat) : nat := +a.foldl 0 (+) + +#eval array_sum (mk_array 10 1) + +#eval (mk_array 10 1).data ⟨1, dec_trivial⟩ + 20 +#eval (mk_array 10 1).data ⟨2, dec_trivial⟩ +#eval (mk_array 10 3).data ⟨2, dec_trivial⟩