core / init.data.array.basic

source

structure d_array (n : ℕ) (α : fin n → Type u) :

Type u

data : Π (i : fin n), α i

In the VM, d_array is implemented as a persistent array.

Instances for d_array

d_array.has_sizeof_inst

source

def d_array.nil {α : fin 0 → Type u_1} :

d_array 0 α

The empty array.

Equations

d_array.nil = {data := λ (_x : fin 0), d_array.nil._match_1 _x}
d_array.nil._match_1 ⟨x, h⟩ = absurd h _

source

def d_array.read {n : ℕ} {α : fin n → Type u} (a : d_array n α) (i : fin n) :

α i

read a i reads the ith member of a. Has builtin VM implementation.

Equations

a.read i = a.data i

source

def d_array.write {n : ℕ} {α : fin n → Type u} (a : d_array n α) (i : fin n) (v : α i) :

d_array n α

write a i v sets the ith member of a to be v. Has builtin VM implementation.

Equations

a.write i v = {data := λ (j : fin n), dite (i = j) (λ (h : i = j), h.rec_on v) (λ (h : ¬i = j), a.read j)}

source

def d_array.iterate_aux {n : ℕ} {α : fin n → Type u} {β : Type w} (a : d_array n α) (f : Π (i : fin n), α i → β → β) (i : ℕ) :

i ≤ n → β → β

Equations

a.iterate_aux f (j + 1) h b = let i : fin n := ⟨j, h⟩ in f i (a.read i) (a.iterate_aux f j _ b)
a.iterate_aux f 0 h b = b

source

def d_array.iterate {n : ℕ} {α : fin n → Type u} {β : Type w} (a : d_array n α) (b : β) (f : Π (i : fin n), α i → β → β) :

β

Fold over the elements of the given array in ascending order. Has builtin VM implementation.

Equations

a.iterate b f = a.iterate_aux f n d_array.iterate._proof_1 b

source

def d_array.foreach {n : ℕ} {α : fin n → Type u} {α' : fin n → Type v} (a : d_array n α) (f : Π (i : fin n), α i → α' i) :

d_array n α'

Map the array. Has builtin VM implementation.

Equations

a.foreach f = {data := λ (i : fin n), f i (a.read i)}

source

def d_array.map {n : ℕ} {α : fin n → Type u} {α' : fin n → Type v} (f : Π (i : fin n), α i → α' i) (a : d_array n α) :

d_array n α'

Equations

d_array.map f a = a.foreach f

source

def d_array.map₂ {n : ℕ} {α : fin n → Type u} {α' : fin n → Type v} {α'' : fin n → Type w} (f : Π (i : fin n), α i → α' i → α'' i) (a : d_array n α) (b : d_array n α') :

d_array n α''

Equations

d_array.map₂ f a b = b.foreach (λ (i : fin n), f i (a.read i))

source

def d_array.foldl {n : ℕ} {α : fin n → Type u} {β : Type w} (a : d_array n α) (b : β) (f : Π (i : fin n), α i → β → β) :

β

Equations

a.foldl b f = a.iterate b f

source

def d_array.rev_iterate_aux {n : ℕ} {α : fin n → Type u} {β : Type w} (a : d_array n α) (f : Π (i : fin n), α i → β → β) (i : ℕ) :

i ≤ n → β → β

Equations

a.rev_iterate_aux f (j + 1) h b = let i : fin n := ⟨j, h⟩ in a.rev_iterate_aux f j _ (f i (a.read i) b)
a.rev_iterate_aux f 0 h b = b

source

def d_array.rev_iterate {n : ℕ} {α : fin n → Type u} {β : Type w} (a : d_array n α) (b : β) (f : Π (i : fin n), α i → β → β) :

β

Equations

a.rev_iterate b f = a.rev_iterate_aux f n d_array.rev_iterate._proof_1 b

source

@[simp]

theorem d_array.read_write {n : ℕ} {α : fin n → Type u} (a : d_array n α) (i : fin n) (v : α i) :

(a.write i v).read i = v

source

@[simp]

theorem d_array.read_write_of_ne {n : ℕ} {α : fin n → Type u} (a : d_array n α) {i j : fin n} (v : α i) :

i ≠ j → (a.write i v).read j = a.read j

source

@[protected]

theorem d_array.ext {n : ℕ} {α : fin n → Type u} {a b : d_array n α} (h : ∀ (i : fin n), a.read i = b.read i) :

a = b

source

@[protected]

theorem d_array.ext' {n : ℕ} {α : fin n → Type u} {a b : d_array n α} (h : ∀ (i : ℕ) (h : i < n), a.read ⟨i, h⟩ = b.read ⟨i, h⟩) :

a = b

source

@[protected]

def d_array.beq_aux {n : ℕ} {α : fin n → Type u} [Π (i : fin n), decidable_eq (α i)] (a b : d_array n α) (i : ℕ) :

i ≤ n → bool

Equations

a.beq_aux b (i + 1) h = ite (a.read ⟨i, h⟩ = b.read ⟨i, h⟩) (a.beq_aux b i _) bool.ff
a.beq_aux b 0 h = bool.tt

source

@[protected]

def d_array.beq {n : ℕ} {α : fin n → Type u} [Π (i : fin n), decidable_eq (α i)] (a b : d_array n α) :

bool

Boolean element-wise equality check.

Equations

a.beq b = a.beq_aux b n d_array.beq._proof_1

source

theorem d_array.of_beq_aux_eq_tt {n : ℕ} {α : fin n → Type u} [Π (i : fin n), decidable_eq (α i)] {a b : d_array n α} (i : ℕ) (h : i ≤ n) :

a.beq_aux b i h = bool.tt → ∀ (j : ℕ) (h' : j < i), a.read ⟨j, _⟩ = b.read ⟨j, _⟩

source

theorem d_array.of_beq_eq_tt {n : ℕ} {α : fin n → Type u} [Π (i : fin n), decidable_eq (α i)] {a b : d_array n α} :

a.beq b = bool.tt → a = b

source

theorem d_array.of_beq_aux_eq_ff {n : ℕ} {α : fin n → Type u} [Π (i : fin n), decidable_eq (α i)] {a b : d_array n α} (i : ℕ) (h : i ≤ n) :

a.beq_aux b i h = bool.ff → (∃ (j : ℕ) (h' : j < i), a.read ⟨j, _⟩ ≠ b.read ⟨j, _⟩)

source

theorem d_array.of_beq_eq_ff {n : ℕ} {α : fin n → Type u} [Π (i : fin n), decidable_eq (α i)] {a b : d_array n α} :

a.beq b = bool.ff → a ≠ b

source

@[protected, instance]

def d_array.decidable_eq {n : ℕ} {α : fin n → Type u} [Π (i : fin n), decidable_eq (α i)] :

decidable_eq (d_array n α)

Equations

d_array.decidable_eq = λ (a b : d_array n α), dite (a.beq b = bool.tt) (λ (h : a.beq b = bool.tt), decidable.is_true _) (λ (h : ¬a.beq b = bool.tt), decidable.is_false _)

source

def array (n : ℕ) (α : Type u) :

Type u

A non-dependent array (see d_array). Implemented in the VM as a persistent array.

Equations

array n α = d_array n (λ (_x : fin n), α)

Instances for array

source

def mk_array {α : Type u_1} (n : ℕ) (v : α) :

array n α

mk_array n v creates a new array of length n where each element is v. Has builtin VM implementation.

Equations

mk_array n v = {data := λ (_x : fin n), v}

source

def array.nil {α : Type u_1} :

array 0 α

Equations

array.nil = d_array.nil

source

def array.read {n : ℕ} {α : Type u} (a : array n α) (i : fin n) :

α

Equations

a.read i = d_array.read a i

source

def array.write {n : ℕ} {α : Type u} (a : array n α) (i : fin n) (v : α) :

array n α

Equations

a.write i v = d_array.write a i v

source

def array.iterate {n : ℕ} {α : Type u} {β : Type v} (a : array n α) (b : β) (f : fin n → α → β → β) :

β

Fold array starting from 0, folder function includes an index argument.

Equations

a.iterate b f = d_array.iterate a b f

source

def array.foreach {n : ℕ} {α : Type u} {β : Type v} (a : array n α) (f : fin n → α → β) :

array n β

Map each element of the given array with an index argument.

Equations

a.foreach f = d_array.foreach a f

source

def array.map₂ {n : ℕ} {α : Type u} (f : α → α → α) (a b : array n α) :

array n α

Equations

array.map₂ f a b = b.foreach (λ (i : fin n), f (a.read i))

source

def array.foldl {n : ℕ} {α : Type u} {β : Type v} (a : array n α) (b : β) (f : α → β → β) :

β

Equations

a.foldl b f = a.iterate b (λ (_x : fin n), f)

source

def array.rev_list {n : ℕ} {α : Type u} (a : array n α) :

list α

Equations

a.rev_list = a.foldl list.nil (λ (_x : α) (_y : list α), _x :: _y)

source

def array.rev_iterate {n : ℕ} {α : Type u} {β : Type v} (a : array n α) (b : β) (f : fin n → α → β → β) :

β

Equations

a.rev_iterate b f = d_array.rev_iterate a b f

source

def array.rev_foldl {n : ℕ} {α : Type u} {β : Type v} (a : array n α) (b : β) (f : α → β → β) :

β

Equations

a.rev_foldl b f = a.rev_iterate b (λ (_x : fin n), f)

source

def array.to_list {n : ℕ} {α : Type u} (a : array n α) :

list α

Equations

a.to_list = a.rev_foldl list.nil (λ (_x : α) (_y : list α), _x :: _y)

source

theorem array.push_back_idx {j n : ℕ} (h₁ : j < n + 1) (h₂ : j ≠ n) :

j < n

source

def array.push_back {n : ℕ} {α : Type u} (a : array n α) (v : α) :

array (n + 1) α

push_back a v pushes value v to the end of the array. Has builtin VM implementation.

Equations

a.push_back v = {data := λ (_x : fin (n + 1)), array.push_back._match_1 a v _x}
array.push_back._match_1 a v ⟨j, h₁⟩ = dite (j = n) (λ (h₂ : j = n), v) (λ (h₂ : ¬j = n), a.read ⟨j, _⟩)