From 70fb2537390d4e1d02a8420415b78d6fe682b417 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 17 Mar 2025 19:22:01 +0100 Subject: [PATCH] doc: review of Array docstrings for manual (#7492) This PR adds missing `Array` docstrings and makes their style consistent. --- src/Init/Data/Array/Attach.lean | 46 +- src/Init/Data/Array/Basic.lean | 1114 +++++++++++++++-- src/Init/Data/Array/BasicAux.lean | 17 +- src/Init/Data/Array/BinSearch.lean | 45 + src/Init/Data/Array/FinRange.lean | 8 +- src/Init/Data/Array/InsertionSort.lean | 6 + src/Init/Data/Array/Lemmas.lean | 10 +- src/Init/Data/Array/Lex/Basic.lean | 9 +- src/Init/Data/Array/QSort.lean | 12 +- src/Init/Data/Array/Set.lean | 24 +- src/Init/Data/List/Attach.lean | 2 +- src/Init/Data/List/Basic.lean | 27 +- src/Init/Data/List/Control.lean | 4 +- src/Init/Data/List/FinRange.lean | 4 +- src/Init/Data/Vector/Basic.lean | 4 +- src/Init/Meta.lean | 10 + src/Init/Prelude.lean | 102 +- src/Lean/Data/Array.lean | 20 +- src/Std/Data/HashMap/Basic.lean | 12 +- .../lean/interactive/hover.lean.expected.out | 4 +- 20 files changed, 1318 insertions(+), 162 deletions(-) diff --git a/src/Init/Data/Array/Attach.lean b/src/Init/Data/Array/Attach.lean index d0ebd72aea..78263498ba 100644 --- a/src/Init/Data/Array/Attach.lean +++ b/src/Init/Data/Array/Attach.lean @@ -15,13 +15,12 @@ set_option linter.indexVariables true -- Enforce naming conventions for index va namespace Array /-- -`O(n)`. Partial map. If `f : Π a, P a → β` is a partial function defined on -`a : α` satisfying `P`, then `pmap f l h` is essentially the same as `map f l` -but is defined only when all members of `l` satisfy `P`, using the proof -to apply `f`. +Maps a partially defined function (defined on those terms of `α` that satisfy a predicate `P`) over +an array `xs : Array α`, given a proof that every element of `xs` in fact satisfies `P`. -We replace this at runtime with a more efficient version via the `csimp` lemma `pmap_eq_pmapImpl`. +`Array.pmap`, named for “partial map,” is the equivalent of `Array.map` for such partial functions. -/ + def pmap {P : α → Prop} (f : ∀ a, P a → β) (xs : Array α) (H : ∀ a ∈ xs, P a) : Array β := (xs.toList.pmap f (fun a m => H a (mem_def.mpr m))).toArray @@ -32,14 +31,27 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep @[inline] private unsafe def attachWithImpl (xs : Array α) (P : α → Prop) (_ : ∀ x ∈ xs, P x) : Array {x // P x} := unsafeCast xs -/-- `O(1)`. "Attach" a proof `P x` that holds for all the elements of `xs` to produce a new array - with the same elements but in the type `{x // P x}`. -/ +/-- +“Attaches” individual proofs to an array of values that satisfy a predicate `P`, returning an array +of elements in the corresponding subtype `{ x // P x }`. + +`O(1)`. +-/ @[implemented_by attachWithImpl] def attachWith (xs : Array α) (P : α → Prop) (H : ∀ x ∈ xs, P x) : Array {x // P x} := ⟨xs.toList.attachWith P fun x h => H x (Array.Mem.mk h)⟩ -/-- `O(1)`. "Attach" the proof that the elements of `xs` are in `xs` to produce a new array - with the same elements but in the type `{x // x ∈ xs}`. -/ +/-- +“Attaches” the proof that the elements of `xs` are in fact elements of `xs`, producing a new array with +the same elements but in the subtype `{ x // x ∈ xs }`. + +`O(1)`. + +This function is primarily used to allow definitions by [well-founded +recursion](lean-manual://section/well-founded-recursion) that use higher-order functions (such as +`Array.map`) to prove that an value taken from a list is smaller than the list. This allows the +well-founded recursion mechanism to prove that the function terminates. +-/ @[inline] def attach (xs : Array α) : Array {x // x ∈ xs} := xs.attachWith _ fun _ => id @[simp] theorem _root_.List.attachWith_toArray {l : List α} {P : α → Prop} {H : ∀ x ∈ l.toArray, P x} : @@ -542,11 +554,19 @@ Further, we provide simp lemmas that push `unattach` inwards. -/ /-- -A synonym for `l.map (·.val)`. Mostly this should not be needed by users. -It is introduced as in intermediate step by lemmas such as `map_subtype`, -and is ideally subsequently simplified away by `unattach_attach`. +Maps an array of terms in a subtype to the corresponding terms in the type by forgetting that they +satisfy the predicate. -If not, usually the right approach is `simp [Array.unattach, -Array.map_subtype]` to unfold. +This is the inverse of `Array.attachWith` and a synonym for `xs.map (·.val)`. + +Mostly this should not be needed by users. It is introduced as an intermediate step by lemmas such +as `map_subtype`, and is ideally subsequently simplified away by `unattach_attach`. + +This function is usually inserted automatically by Lean as an intermediate step while proving +termination. It is rarely used explicitly in code. It is introduced as an intermediate step during +the elaboration of definitions by [well-founded +recursion](lean-manual://section/well-founded-recursion). If this function is encountered in a proof +state, the right approach is usually the tactic `simp [Array.unattach, -Array.map_subtype]`. -/ def unattach {α : Type _} {p : α → Prop} (xs : Array { x // p x }) : Array α := xs.map (·.val) diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index d064ad7d81..5ea3c79feb 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -150,27 +150,44 @@ theorem size_eq_length_toList (xs : Array α) : xs.size = xs.toList.length := rf /-! ### Externs -/ -/-- Low-level version of `size` that directly queries the C array object cached size. - While this is not provable, `usize` always returns the exact size of the array since - the implementation only supports arrays of size less than `USize.size`. +/-- +Returns the size of the array as a platform-native unsigned integer. + +This is a low-level version of `Array.size` that directly queries the runtime system's +representation of arrays. While this is not provable, `Array.usize` always returns the exact size of +the array since the implementation only supports arrays of size less than `USize.size`. -/ @[extern "lean_array_size", simp] def usize (a : @& Array α) : USize := a.size.toUSize -/-- Low-level version of `fget` which is as fast as a C array read. - `Fin` values are represented as tag pointers in the Lean runtime. Thus, - `fget` may be slightly slower than `uget`. -/ +/-- +Low-level indexing operator which is as fast as a C array read. + +This avoids overhead due to unboxing a `Nat` used as an index. +-/ @[extern "lean_array_uget", simp] def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α := a[i.toNat] -/-- Low-level version of `fset` which is as fast as a C array fset. - `Fin` values are represented as tag pointers in the Lean runtime. Thus, - `fset` may be slightly slower than `uset`. -/ +/-- +Low-level modification operator which is as fast as a C array write. The modification is performed +in-place when the reference to the array is unique. + +This avoids overhead due to unboxing a `Nat` used as an index. +-/ @[extern "lean_array_uset"] def uset (xs : Array α) (i : USize) (v : α) (h : i.toNat < xs.size) : Array α := xs.set i.toNat v h +/-- +Removes the last element of an array. If the array is empty, then it is returned unmodified. The +modification is performed in-place when the reference to the array is unique. + +Examples: +* `#[1, 2, 3].pop = #[1, 2]` +* `#["orange", "yellow"].pop = #["orange"]` +* `(#[] : Array String).pop = #[]` +-/ @[extern "lean_array_pop"] def pop (xs : Array α) : Array α where toList := xs.toList.dropLast @@ -180,15 +197,29 @@ def pop (xs : Array α) : Array α where | ⟨[]⟩ => rfl | ⟨a::as⟩ => simp [pop, Nat.succ_sub_succ_eq_sub, size] +/-- +Creates an array that contains `n` repetitions of `v`. + +The corresponding `List` function is `List.replicate`. + +Examples: + * `Array.mkArray 2 true = #[true, true]` + * `Array.mkArray 3 () = #[(), (), ()]` + * `Array.mkArray 0 "anything" = #[]` +-/ @[extern "lean_mk_array"] def mkArray {α : Type u} (n : Nat) (v : α) : Array α where toList := List.replicate n v /-- -Swaps two entries in an array. +Swaps two elements of an array. The modification is performed in-place when the reference to the +array is unique. -This will perform the update destructively provided that `a` has a reference -count of 1 when called. +Examples: +* `#["red", "green", "blue", "brown"].swap 0 3 = #["brown", "green", "blue", "red"]` +* `#["red", "green", "blue", "brown"].swap 0 2 = #["blue", "green", "red", "brown"]` +* `#["red", "green", "blue", "brown"].swap 1 2 = #["red", "blue", "green", "brown"]` +* `#["red", "green", "blue", "brown"].swap 3 0 = #["brown", "green", "blue", "red"]` -/ @[extern "lean_array_fswap"] def swap (xs : Array α) (i j : @& Nat) (hi : i < xs.size := by get_elem_tactic) (hj : j < xs.size := by get_elem_tactic) : Array α := @@ -203,10 +234,15 @@ def swap (xs : Array α) (i j : @& Nat) (hi : i < xs.size := by get_elem_tactic) rw [size_set, size_set] /-- -Swaps two entries in an array, or returns the array unchanged if either index is out of bounds. +Swaps two elements of an array, returning the array unchanged if either index is out of bounds. The +modification is performed in-place when the reference to the array is unique. -This will perform the update destructively provided that `a` has a reference -count of 1 when called. +Examples: +* `#["red", "green", "blue", "brown"].swapIfInBounds 0 3 = #["brown", "green", "blue", "red"]` +* `#["red", "green", "blue", "brown"].swapIfInBounds 0 2 = #["blue", "green", "red", "brown"]` +* `#["red", "green", "blue", "brown"].swapIfInBounds 1 2 = #["red", "blue", "green", "brown"]` +* `#["red", "green", "blue", "brown"].swapIfInBounds 0 4 = #["red", "green", "blue", "brown"]` +* `#["red", "green", "blue", "brown"].swapIfInBounds 9 2 = #["red", "green", "blue", "brown"]` -/ @[extern "lean_array_swap"] def swapIfInBounds (xs : Array α) (i j : @& Nat) : Array α := @@ -228,6 +264,16 @@ instance : EmptyCollection (Array α) := ⟨Array.empty⟩ instance : Inhabited (Array α) where default := Array.empty +/-- +Checks whether an array is empty. + +An array is empty if its size is `0`. + +Examples: + * `(#[] : Array String).isEmpty = true` + * `#[1, 2].isEmpty = false` + * `#[()].isEmpty = false` +-/ def isEmpty (xs : Array α) : Bool := xs.size = 0 @@ -238,6 +284,16 @@ def isEqvAux (xs ys : Array α) (hsz : xs.size = ys.size) (p : α → α → Boo | i+1, h => p xs[i] (ys[i]'(hsz ▸ h)) && isEqvAux xs ys hsz p i (Nat.le_trans (Nat.le_add_right i 1) h) +/-- +Returns `true` if `as` and `bs` have the same length and they are pairwise related by `eqv`. + +Short-circuits at the first non-related pair of elements. + +Examples: +* `#[1, 2, 3].isEqv #[2, 3, 4] (· < ·) = true` +* `#[1, 2, 3].isEqv #[2, 2, 4] (· < ·) = false` +* `#[1, 2, 3].isEqv #[2, 3] (· < ·) = false` +-/ @[inline] def isEqv (xs ys : Array α) (p : α → α → Bool) : Bool := if h : xs.size = ys.size then isEqvAux xs ys h p xs.size (Nat.le_refl xs.size) @@ -247,11 +303,18 @@ def isEqvAux (xs ys : Array α) (hsz : xs.size = ys.size) (p : α → α → Boo instance [BEq α] : BEq (Array α) := ⟨fun xs ys => isEqv xs ys BEq.beq⟩ -/-- +/- `ofFn f` with `f : Fin n → α` returns the list whose ith element is `f i`. ``` ofFn f = #[f 0, f 1, ... , f(n - 1)] ``` -/ +/-- +Creates an array by applying `f` to each potential index in order, starting at `0`. + +Examples: + * `Array.ofFn (n := 3) toString = #["0", "1", "2"]` + * `Array.ofFn (fun i => #["red", "green", "blue"].get i.val i.isLt) = #["red", "green", "blue"]` +-/ def ofFn {n} (f : Fin n → α) : Array α := go 0 (emptyWithCapacity n) where /-- Auxiliary for `ofFn`. `ofFn.go f i acc = acc ++ #[f i, ..., f(n - 1)]` -/ @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion. @@ -259,39 +322,64 @@ def ofFn {n} (f : Fin n → α) : Array α := go 0 (emptyWithCapacity n) where if h : i < n then go (i+1) (acc.push (f ⟨i, h⟩)) else acc decreasing_by simp_wf; decreasing_trivial_pre_omega -/-- The array `#[0, 1, ..., n - 1]`. -/ +/-- +Constructs an array that contains all the numbers from `0` to `n`, exclusive. + +Examples: + * `Array.range 5 := #[0, 1, 2, 3, 4]` + * `Array.range 0 := #[]` + * `Array.range 1 := #[0]` +-/ def range (n : Nat) : Array Nat := ofFn fun (i : Fin n) => i -/-- The array `#[start, start + step, ..., start + step * (size - 1)]`. -/ +/-- +Constructs an array of numbers of size `size`, starting at `start` and increasing by +`step` at each element. + +In other words, `Array.range' start size step` is `#[start, start+step, ..., start+(len-1)*step]`. + +Examples: + * `Array.range' 0 3 (step := 1) = #[0, 1, 2]` + * `Array.range' 0 3 (step := 2) = #[0, 2, 4]` + * `Array.range' 0 4 (step := 2) = #[0, 2, 4, 6]` + * `Array.range' 3 4 (step := 2) = #[3, 5, 7, 9]` +-/ def range' (start size : Nat) (step : Nat := 1) : Array Nat := ofFn fun (i : Fin size) => start + step * i +/-- +Constructs a single-element array that contains `v`. + +Examples: + * `Array.singleton 5 = #[5]` + * `Array.singleton "one" = #["one"]` +-/ @[inline] protected def singleton (v : α) : Array α := #[v] /-- -Return the last element of an array, or panic if the array is empty. +Returns the last element of an array, or panics if the array is empty. -See `back` for the version that requires a proof the array is non-empty, -or `back?` for the version that returns an option. +Safer alternatives include `Array.back`, which requires a proof the array is non-empty, and +`Array.back?`, which returns an `Option`. -/ def back! [Inhabited α] (xs : Array α) : α := xs[xs.size - 1]! /-- -Return the last element of an array, given a proof that the array is not empty. +Returns the last element of an array, given a proof that the array is not empty. -See `back!` for the version that panics if the array is empty, -or `back?` for the version that returns an option. +See `Array.back!` for the version that panics if the array is empty, or `Array.back?` for the +version that returns an option. -/ def back (xs : Array α) (h : 0 < xs.size := by get_elem_tactic) : α := xs[xs.size - 1]'(Nat.sub_one_lt_of_lt h) /-- -Return the last element of an array, or `none` if the array is empty. +Returns the last element of an array, or `none` if the array is empty. -See `back!` for the version that panics if the array is empty, -or `back` for the version that requires a proof the array is non-empty. +See `Array.back!` for the version that panics if the array is empty, or `Array.back` for the version +that requires a proof the array is non-empty. -/ def back? (xs : Array α) : Option α := xs[xs.size - 1]? @@ -300,11 +388,31 @@ def back? (xs : Array α) : Option α := def get? (xs : Array α) (i : Nat) : Option α := if h : i < xs.size then some xs[i] else none +/-- +Swaps a new element with the element at the given index. + +Returns the value formerly found at `i`, paired with an array in which the value at `i` has been +replaced with `v`. + +Examples: +* `#["spinach", "broccoli", "carrot"].swapAt 1 "pepper" = ("broccoli", #["spinach", "pepper", "carrot"])` +* `#["spinach", "broccoli", "carrot"].swapAt 2 "pepper" = ("carrot", #["spinach", "broccoli", "pepper"])` +-/ @[inline] def swapAt (xs : Array α) (i : Nat) (v : α) (hi : i < xs.size := by get_elem_tactic) : α × Array α := let e := xs[i] let xs' := xs.set i v (e, xs') +/-- +Swaps a new element with the element at the given index. Panics if the index is out of bounds. + +Returns the value formerly found at `i`, paired with an array in which the value at `i` has been +replaced with `v`. + +Examples: +* `#["spinach", "broccoli", "carrot"].swapAt! 1 "pepper" = (#["spinach", "pepper", "carrot"], "broccoli")` +* `#["spinach", "broccoli", "carrot"].swapAt! 2 "pepper" = (#["spinach", "broccoli", "pepper"], "carrot")` +-/ @[inline] def swapAt! (xs : Array α) (i : Nat) (v : α) : α × Array α := if h : i < xs.size then @@ -313,19 +421,48 @@ def swapAt! (xs : Array α) (i : Nat) (v : α) : α × Array α := have : Inhabited (α × Array α) := ⟨(v, xs)⟩ panic! ("index " ++ toString i ++ " out of bounds") -/-- `shrink a n` returns the first `n` elements of `a`, implemented by repeatedly popping the last element. -/ +/-- +Returns the first `n` elements of an array. The resulting array is produced by repeatedly calling +`Array.pop`. If `n` is greater than the size of the array, it is returned unmodified. + +If the reference to the array is unique, then this function uses in-place modification. + +Examples: +* `#[0, 1, 2, 3, 4].shrink 2 = #[0, 1]` +* `#[0, 1, 2, 3, 4].shrink 0 = #[]` +* `#[0, 1, 2, 3, 4].shrink 10 = #[0, 1, 2, 3, 4]` +-/ def shrink (xs : Array α) (n : Nat) : Array α := let rec loop | 0, xs => xs | n+1, xs => loop n xs.pop loop (xs.size - n) xs -/-- `take a n` returns the first `n` elements of `a`, implemented by copying the first `n` elements. -/ +/-- +Returns a new array that contains the first `i` elements of `xs`. If `xs` has fewer than `i` +elements, the new array contains all the elements of `xs`. + +The returned array is always a new array, even if it contains the same elements as the input array. + +Examples: +* `#["red", "green", "blue"].take 1 = #["red"]` +* `#["red", "green", "blue"].take 2 = #["red", "green"]` +* `#["red", "green", "blue"].take 5 = #["red", "green", "blue"]` +-/ abbrev take (xs : Array α) (i : Nat) : Array α := extract xs 0 i @[simp] theorem take_eq_extract (xs : Array α) (i : Nat) : xs.take i = xs.extract 0 i := rfl -/-- `drop a n` removes the first `n` elements of `a`, implemented by copying the remaining elements. -/ +/-- +Removes the first `i` elements of `xs`. If `xs` has fewer than `i` elements, the new array is empty. + +The returned array is always a new array, even if it contains the same elements as the input array. + +Examples: +* `#["red", "green", "blue"].drop 1 = #["green", "blue"]` +* `#["red", "green", "blue"].drop 2 = #["blue"]` +* `#["red", "green", "blue"].drop 5 = #[]` +-/ abbrev drop (xs : Array α) (i : Nat) : Array α := extract xs i xs.size @[simp] theorem drop_eq_extract (xs : Array α) (i : Nat) : xs.drop i = xs.extract i xs.size := rfl @@ -343,6 +480,32 @@ unsafe def modifyMUnsafe [Monad m] (xs : Array α) (i : Nat) (f : α → m α) : else pure xs +/-- +Replaces the element at the given index, if it exists, with the result of applying the monadic +function `f` to it. If the index is invalid, the array is returned unmodified and `f` is not called. + +Examples: +```lean example +#eval #[1, 2, 3, 4].modifyM 2 fun x => do + IO.println s!"It was {x}" + return x * 10 +``` +```output +It was 3 +``` +```output +#[1, 2, 30, 4] +``` + +```lean example +#eval #[1, 2, 3, 4].modifyM 6 fun x => do + IO.println s!"It was {x}" + return x * 10 +``` +```output +#[1, 2, 3, 4] +``` +-/ @[implemented_by modifyMUnsafe] def modifyM [Monad m] (xs : Array α) (i : Nat) (f : α → m α) : m (Array α) := do if h : i < xs.size then @@ -352,11 +515,29 @@ def modifyM [Monad m] (xs : Array α) (i : Nat) (f : α → m α) : m (Array α) else pure xs +/-- +Replaces the element at the given index, if it exists, with the result of applying `f` to it. If the +index is invalid, the array is returned unmodified. + +Examples: + * `#[1, 2, 3].modify 0 (· * 10) = #[10, 2, 3]` + * `#[1, 2, 3].modify 2 (· * 10) = #[1, 2, 30]` + * `#[1, 2, 3].modify 3 (· * 10) = #[1, 2, 3]` +-/ @[inline] def modify (xs : Array α) (i : Nat) (f : α → α) : Array α := Id.run <| modifyM xs i f set_option linter.indexVariables false in -- Changing `idx` causes bootstrapping issues, haven't investigated. +/-- +Replaces the element at the given index, if it exists, with the result of applying `f` to it. If the +index is invalid, the array is returned unmodified. + +Examples: + * `#[1, 2, 3].modifyOp 0 (· * 10) = #[10, 2, 3]` + * `#[1, 2, 3].modifyOp 2 (· * 10) = #[1, 2, 30]` + * `#[1, 2, 3].modifyOp 3 (· * 10) = #[1, 2, 3]` +-/ @[inline] def modifyOp (xs : Array α) (idx : Nat) (f : α → α) : Array α := xs.modify idx f @@ -416,7 +597,35 @@ unsafe def foldlMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Mon else pure init -/-- Reference implementation for `foldlM` -/ +/-- +Folds a monadic function over a list from the left, accumulating a value starting with `init`. The +accumulated value is combined with the each element of the list in order, using `f`. + +The optional parameters `start` and `stop` control the region of the array to be folded. Folding +proceeds from `start` (inclusive) to `stop` (exclusive), so no folding occurs unless `start < stop`. +By default, the entire array is folded. + +Examples: +```lean example +example [Monad m] (f : α → β → m α) : + Array.foldlM (m := m) f x₀ #[a, b, c] = (do + let x₁ ← f x₀ a + let x₂ ← f x₁ b + let x₃ ← f x₂ c + pure x₃) + := by rfl +``` + +```lean example +example [Monad m] (f : α → β → m α) : + Array.foldlM (m := m) f x₀ #[a, b, c] (start := 1) = (do + let x₁ ← f x₀ b + let x₂ ← f x₁ c + pure x₂) + := by rfl +``` +-/ +-- Reference implementation for `foldlM` @[implemented_by foldlMUnsafe] def foldlM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : β → α → m β) (init : β) (as : Array α) (start := 0) (stop := as.size) : m β := let fold (stop : Nat) (h : stop ≤ as.size) := @@ -453,7 +662,35 @@ unsafe def foldrMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Mon else pure init -/-- Reference implementation for `foldrM` -/ +/-- +Folds a monadic function over an array from the right, accumulating a value starting with `init`. +The accumulated value is combined with the each element of the list in reverse order, using `f`. + +The optional parameters `start` and `stop` control the region of the array to be folded. Folding +proceeds from `start` (exclusive) to `stop` (inclusive), so no folding occurs unless `start > stop`. +By default, the entire array is folded. + +Examples: +```lean example +example [Monad m] (f : α → β → m β) : + Array.foldrM (m := m) f x₀ #[a, b, c] = (do + let x₁ ← f c x₀ + let x₂ ← f b x₁ + let x₃ ← f a x₂ + pure x₃) + := by rfl +``` + +```lean example +example [Monad m] (f : α → β → m β) : + Array.foldrM (m := m) f x₀ #[a, b, c] (start := 2) = (do + let x₁ ← f b x₀ + let x₂ ← f a x₁ + pure x₂) + := by rfl +``` +-/ +-- Reference implementation for `foldrM` @[implemented_by foldrMUnsafe] def foldrM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → β → m β) (init : β) (as : Array α) (start := as.size) (stop := 0) : m β := let rec fold (i : Nat) (h : i ≤ as.size) (b : β) : m β := do @@ -491,7 +728,11 @@ unsafe def mapMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad pure (unsafeCast bs) unsafeCast <| map 0 (unsafeCast as) -/-- Reference implementation for `mapM` -/ +/-- +Applies the monadic action `f` to every element in the array, left-to-right, and returns the array +of results. +-/ +-- Reference implementation for `mapM` @[implemented_by mapMUnsafe] def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (as : Array α) : m (Array β) := -- Note: we cannot use `foldlM` here for the reference implementation because this calls @@ -526,6 +767,15 @@ def mapFinIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : Nat → α → m β) (as : Array α) : m (Array β) := as.mapFinIdxM fun i a _ => f i a +/-- +Maps `f` over the array and collects the results with `<|>`. The result for the end of the array is +`failure`. + +Examples: + * `#[[], [1, 2], [], [2]].firstM List.head? = some 1` + * `#[[], [], []].firstM List.head? = none` + * `#[].firstM List.head? = none` +-/ @[inline] def firstM {α : Type u} {m : Type v → Type w} [Alternative m] (f : α → m β) (as : Array α) : m β := go 0 @@ -538,6 +788,27 @@ where termination_by as.size - i decreasing_by exact Nat.sub_succ_lt_self as.size i hlt +/-- +Returns the first non-`none` result of applying the monadic function `f` to each element of the +array, in order. Returns `none` if `f` returns `none` for all elements. + +Example: +```lean example +#eval #[7, 6, 5, 8, 1, 2, 6].findSomeM? fun i => do + if i < 5 then + return some (i * 10) + if i ≤ 6 then + IO.println s!"Almost! {i}" + return none +``` +```output +Almost! 6 +Almost! 5 +``` +```output +some 10 +``` +-/ @[inline] def findSomeM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m (Option β)) (as : Array α) : m (Option β) := do for a in as do @@ -547,8 +818,27 @@ def findSomeM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f return none /-- -Note that the universe level is contrained to `Type` here, -to avoid having to have the predicate live in `p : α → m (ULift Bool)`. +Returns the first element of the array for which the monadic predicate `p` returns `true`, or `none` +if no such element is found. Elements of the array are checked in order. + +The monad `m` is restricted to `Type → Type` to avoid needing to use `ULift Bool` in `p`'s type. + +Example: +```lean example +#eval #[7, 6, 5, 8, 1, 2, 6].findM? fun i => do + if i < 5 then + return true + if i ≤ 6 then + IO.println s!"Almost! {i}" + return false +``` +```output +Almost! 6 +Almost! 5 +``` +```output +some 1 +``` -/ @[inline] def findM? {α : Type} [Monad m] (p : α → m Bool) (as : Array α) : m (Option α) := do @@ -557,6 +847,11 @@ def findM? {α : Type} [Monad m] (p : α → m Bool) (as : Array α) : m (Option return a return none +/-- +Finds the index of the first element of an array for which the monadic predicate `p` returns `true`. +Elements are examined in order from left to right, and the search is terminated when an element that +satisfies `p` is found. If no such element exists in the array, then `none` is returned. +-/ @[inline] def findIdxM? [Monad m] (p : α → m Bool) (as : Array α) : m (Option Nat) := do let mut i := 0 @@ -585,6 +880,16 @@ unsafe def anyMUnsafe {α : Type u} {m : Type → Type w} [Monad m] (p : α → else pure false +/-- +Returns `true` if the monadic predicate `p` returns `true` for any element of `as`. + +Short-circuits upon encountering the first `true`. The elements in `as` are examined in order from +left to right. + +The optional parameters `start` and `stop` control the region of the array to be checked. Only the +elements with indices from `start` (inclusive) to `stop` (exclusive) are checked. By default, the +entire array is checked. +-/ @[implemented_by anyMUnsafe] def anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) (start := 0) (stop := as.size) : m Bool := let any (stop : Nat) (h : stop ≤ as.size) := @@ -605,10 +910,45 @@ def anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : else any as.size (Nat.le_refl _) +/-- +Returns `true` if the monadic predicate `p` returns `true` for every element of `as`. + +Short-circuits upon encountering the first `false`. The elements in `as` are examined in order from +left to right. + +The optional parameters `start` and `stop` control the region of the array to be checked. Only the +elements with indices from `start` (inclusive) to `stop` (exclusive) are checked. By default, the +entire array is checked. +-/ @[inline] def allM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) (start := 0) (stop := as.size) : m Bool := return !(← as.anyM (start := start) (stop := stop) fun v => return !(← p v)) +/-- +Returns the first non-`none` result of applying the monadic function `f` to each element of the +array in reverse order, from right to left. Once a non-`none` result is found, no further elements +are checked. Returns `none` if `f` returns `none` for all elements of the array. + +Examples: +```lean example +#eval #[1, 2, 0, -4, 1].findSomeRevM? (m := Except String) fun x => do + if x = 0 then throw "Zero!" + else if x < 0 then return (some x) + else return none +``` +```output +Except.ok (some (-4)) +``` +```lean example +#eval #[1, 2, 0, 4, 1].findSomeRevM? (m := Except String) fun x => do + if x = 0 then throw "Zero!" + else if x < 0 then return (some x) + else return none +``` +```output +Except.error "Zero!" +``` +-/ @[inline] def findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m (Option β)) (as : Array α) : m (Option β) := let rec @[specialize] find : (i : Nat) → i ≤ as.size → m (Option β) @@ -623,10 +963,40 @@ def findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] find i this find as.size (Nat.le_refl _) +/-- +Returns the last element of the array for which the monadic predicate `p` returns `true`, or `none` +if no such element is found. Elements of the array are checked in reverse, from right to left.. + +The monad `m` is restricted to `Type → Type` to avoid needing to use `ULift Bool` in `p`'s type. + +Example: +```lean example +#eval #[7, 5, 8, 1, 2, 6, 5, 8].findRevM? fun i => do + if i < 5 then + return true + if i ≤ 6 then + IO.println s!"Almost! {i}" + return false +``` +```output +Almost! 5 +Almost! 6 +``` +```output +some 2 +``` +-/ @[inline] def findRevM? {α : Type} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) : m (Option α) := as.findSomeRevM? fun a => return if (← p a) then some a else none +/-- +Applies the monadic action `f` to each element of an array, in order. + +The optional parameters `start` and `stop` control the region of the array to which `f` should be +applied. Iteration proceeds from `start` (inclusive) to `stop` (exclusive), so `f` is not invoked +unless `start < stop`. By default, the entire array is used. +-/ @[inline] protected def forM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Array α) (start := 0) (stop := as.size) : m PUnit := as.foldlM (fun _ => f) ⟨⟩ start stop @@ -638,33 +1008,95 @@ instance : ForM m (Array α) α where @[simp] theorem forM_eq_forM [Monad m] (f : α → m PUnit) : Array.forM f as 0 as.size = forM as f := rfl +/-- +Applies the monadic action `f` to each element of an array from right to left, in reverse order. + +The optional parameters `start` and `stop` control the region of the array to which `f` should be +applied. Iteration proceeds from `start` (exclusive) to `stop` (inclusive), so no `f` is not invoked +unless `start > stop`. By default, the entire array is used. +-/ @[inline] def forRevM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Array α) (start := as.size) (stop := 0) : m PUnit := as.foldrM (fun a _ => f a) ⟨⟩ start stop +/-- +Folds a function over an array from the left, accumulating a value starting with `init`. The +accumulated value is combined with the each element of the array in order, using `f`. + +The optional parameters `start` and `stop` control the region of the array to be folded. Folding +proceeds from `start` (inclusive) to `stop` (exclusive), so no folding occurs unless `start < stop`. +By default, the entire array is used. + +Examples: + * `#[a, b, c].foldl f z = f (f (f z a) b) c` + * `#[1, 2, 3].foldl (· ++ toString ·) "" = "123"` + * `#[1, 2, 3].foldl (s!"({·} {·})") "" = "((( 1) 2) 3)"` +-/ @[inline] def foldl {α : Type u} {β : Type v} (f : β → α → β) (init : β) (as : Array α) (start := 0) (stop := as.size) : β := Id.run <| as.foldlM f init start stop +/-- +Folds a function over an array from the right, accumulating a value starting with `init`. The +accumulated value is combined with the each element of the array in reverse order, using `f`. + +The optional parameters `start` and `stop` control the region of the array to be folded. Folding +proceeds from `start` (exclusive) to `stop` (inclusive), so no folding occurs unless `start > stop`. +By default, the entire array is used. + +Examples: + * `#[a, b, c].foldr f init = f a (f b (f c init))` + * `#[1, 2, 3].foldr (toString · ++ ·) "" = "123"` + * `#[1, 2, 3].foldr (s!"({·} {·})") "!" = "(1 (2 (3 !)))"` +-/ @[inline] def foldr {α : Type u} {β : Type v} (f : α → β → β) (init : β) (as : Array α) (start := as.size) (stop := 0) : β := Id.run <| as.foldrM f init start stop -/-- Sum of an array. +/-- +Computes the sum of the elements of an array. -`Array.sum #[a, b, c] = a + (b + (c + 0))` -/ +Examples: + * `#[a, b, c].sum = a + (b + (c + 0))` + * `#[1, 2, 5].sum = 8` +-/ @[inline] def sum {α} [Add α] [Zero α] : Array α → α := foldr (· + ·) 0 +/-- +Counts the number of elements in the array `as` that satisfy the Boolean predicate `p`. + +Examples: + * `#[1, 2, 3, 4, 5].countP (· % 2 == 0) = 2` + * `#[1, 2, 3, 4, 5].countP (· < 5) = 4` + * `#[1, 2, 3, 4, 5].countP (· > 5) = 0` +-/ @[inline] def countP {α : Type u} (p : α → Bool) (as : Array α) : Nat := as.foldr (init := 0) fun a acc => bif p a then acc + 1 else acc +/-- +Counts the number of times an element occurs in an array. + +Examples: + * `#[1, 1, 2, 3, 5].count 1 = 2` + * `#[1, 1, 2, 3, 5].count 5 = 1` + * `#[1, 1, 2, 3, 5].count 4 = 0` +-/ @[inline] def count {α : Type u} [BEq α] (a : α) (as : Array α) : Nat := countP (· == a) as +/-- +Applies a function to each element of the array, returning the resulting array of values. + +Examples: +* `#[a, b, c].map f = #[f a, f b, f c]` +* `#[].map Nat.succ = #[]` +* `#["one", "two", "three"].map (·.length) = #[3, 3, 5]` +* `#["one", "two", "three"].map (·.reverse) = #["eno", "owt", "eerht"]` +-/ @[inline] def map {α : Type u} {β : Type v} (f : α → β) (as : Array α) : Array β := Id.run <| as.mapM f @@ -672,21 +1104,49 @@ def map {α : Type u} {β : Type v} (f : α → β) (as : Array α) : Array β : instance : Functor Array where map := map -/-- Variant of `mapIdx` which receives the index as a `Fin as.size`. -/ +/-- +Applies a function to each element of the array along with the index at which that element is found, +returning the array of results. In addition to the index, the function is also provided with a proof +that the index is valid. + +`Array.mapIdx` is a variant that does not provide the function with evidence that the index is +valid. +-/ @[inline] def mapFinIdx {α : Type u} {β : Type v} (as : Array α) (f : (i : Nat) → α → (h : i < as.size) → β) : Array β := Id.run <| as.mapFinIdxM f +/-- +Applies a function to each element of the array along with the index at which that element is found, +returning the array of results. + +`Array.mapFinIdx` is a variant that additionally provides the function with a proof that the index +is valid. +-/ @[inline] def mapIdx {α : Type u} {β : Type v} (f : Nat → α → β) (as : Array α) : Array β := Id.run <| as.mapIdxM f -/-- Turns `#[a, b]` into `#[(a, 0), (b, 1)]`. -/ +/-- +Pairs each element of an array with its index, optionally starting from an index other than `0`. + +Examples: +* `#[a, b, c].zipIdx = #[(a, 0), (b, 1), (c, 2)]` +* `#[a, b, c].zipIdx 5 = #[(a, 5), (b, 6), (c, 7)]` +-/ def zipIdx (xs : Array α) (start := 0) : Array (α × Nat) := xs.mapIdx fun i a => (a, start + i) @[deprecated zipIdx (since := "2025-01-21")] abbrev zipWithIndex := @zipIdx +/-- +Returns the first element of the array for which the predicate `p` returns `true`, or `none` if no +such element is found. + +Examples: +* `#[7, 6, 5, 8, 1, 2, 6].find? (· < 5) = some 1` +* `#[7, 6, 5, 8, 1, 2, 6].find? (· < 1) = none` +-/ @[inline] def find? {α : Type u} (p : α → Bool) (as : Array α) : Option α := Id.run do @@ -695,24 +1155,80 @@ def find? {α : Type u} (p : α → Bool) (as : Array α) : Option α := return a return none +/-- +Returns the first non-`none` result of applying the function `f` to each element of the +array, in order. Returns `none` if `f` returns `none` for all elements. + +Example: +```lean example +#eval #[7, 6, 5, 8, 1, 2, 6].findSome? fun i => + if i < 5 then + some (i * 10) + else + none +``` +```output +some 10 +``` +-/ @[inline] def findSome? {α : Type u} {β : Type v} (f : α → Option β) (as : Array α) : Option β := Id.run <| as.findSomeM? f +/-- +Returns the first non-`none` result of applying the function `f` to each element of the +array, in order. Panics if `f` returns `none` for all elements. + +Example: +```lean example +#eval #[7, 6, 5, 8, 1, 2, 6].findSome? fun i => + if i < 5 then + some (i * 10) + else + none +``` +```output +some 10 +``` +-/ @[inline] def findSome! {α : Type u} {β : Type v} [Inhabited β] (f : α → Option β) (xs : Array α) : β := match xs.findSome? f with | some b => b | none => panic! "failed to find element" +/-- +Returns the first non-`none` result of applying `f` to each element of the array in reverse order, +from right to left. Returns `none` if `f` returns `none` for all elements of the array. + +Examples: + * `#[7, 6, 5, 8, 1, 2, 6].findSome? (fun x => if x < 5 then some (10 * x) else none) = some 10` + * `#[7, 6, 5, 8, 1, 2, 6].findSome? (fun x => if x < 1 then some (10 * x) else none) = none` +-/ @[inline] def findSomeRev? {α : Type u} {β : Type v} (f : α → Option β) (as : Array α) : Option β := Id.run <| as.findSomeRevM? f +/-- +Returns the last element of the array for which the predicate `p` returns `true`, or `none` if no +such element is found. + +Examples: +* `#[7, 6, 5, 8, 1, 2, 6].findRev? (· < 5) = some 2` +* `#[7, 6, 5, 8, 1, 2, 6].findRev? (· < 1) = none` +-/ @[inline] def findRev? {α : Type} (p : α → Bool) (as : Array α) : Option α := Id.run <| as.findRevM? p +/-- +Returns the index of the first element for which `p` returns `true`, or `none` if there is no such +element. + +Examples: +* `#[7, 6, 5, 8, 1, 2, 6].findIdx (· < 5) = some 4` +* `#[7, 6, 5, 8, 1, 2, 6].findIdx (· < 1) = none` +-/ @[inline] def findIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option Nat := let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion. @@ -723,6 +1239,14 @@ def findIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option Nat := decreasing_by simp_wf; decreasing_trivial_pre_omega loop 0 +/-- +Returns the index of the first element for which `p` returns `true`, or `none` if there is no such +element. The index is returned as a `Fin`, which guarantees that it is in bounds. + +Examples: +* `#[7, 6, 5, 8, 1, 2, 6].findFinIdx? (· < 5) = some (4 : Fin 7)` +* `#[7, 6, 5, 8, 1, 2, 6].findFinIdx? (· < 1) = none` +-/ @[inline] def findFinIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option (Fin as.size) := let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion. @@ -751,6 +1275,14 @@ theorem findIdx?_eq_map_findFinIdx?_val {xs : Array α} {p : α → Bool} : xs.findIdx? p = (xs.findFinIdx? p).map (·.val) := by simp [findIdx?, findFinIdx?, findIdx?_loop_eq_map_findFinIdx?_loop_val] +/-- +Returns the index of the first element for which `p` returns `true`, or the size of the array if +there is no such element. + +Examples: +* `#[7, 6, 5, 8, 1, 2, 6].findIdx (· < 5) = 4` +* `#[7, 6, 5, 8, 1, 2, 6].findIdx (· < 1) = 7` +-/ @[inline] def findIdx (p : α → Bool) (as : Array α) : Nat := (as.findIdx? p).getD as.size @@ -765,15 +1297,43 @@ decreasing_by simp_wf; decreasing_trivial_pre_omega @[deprecated idxOfAux (since := "2025-01-29")] abbrev indexOfAux := @idxOfAux +/-- +Returns the index of the first element equal to `a`, or the size of the array if no element is equal +to `a`. The index is returned as a `Fin`, which guarantees that it is in bounds. + +Examples: + * `#["carrot", "potato", "broccoli"].finIdxOf? "carrot" = some 0` + * `#["carrot", "potato", "broccoli"].finIdxOf? "broccoli" = some 2` + * `#["carrot", "potato", "broccoli"].finIdxOf? "tomato" = none` + * `#["carrot", "potato", "broccoli"].finIdxOf? "anything else" = none` +-/ def finIdxOf? [BEq α] (xs : Array α) (v : α) : Option (Fin xs.size) := idxOfAux xs v 0 @[deprecated "`Array.indexOf?` has been deprecated, use `idxOf?` or `finIdxOf?` instead." (since := "2025-01-29")] abbrev indexOf? := @finIdxOf? -/-- Returns the index of the first element equal to `a`, or the length of the array otherwise. -/ +/-- +Returns the index of the first element equal to `a`, or the size of the array if no element is equal +to `a`. + +Examples: + * `#["carrot", "potato", "broccoli"].idxOf "carrot" = 0` + * `#["carrot", "potato", "broccoli"].idxOf "broccoli" = 2` + * `#["carrot", "potato", "broccoli"].idxOf "tomato" = 3` + * `#["carrot", "potato", "broccoli"].idxOf "anything else" = 3` +-/ def idxOf [BEq α] (a : α) : Array α → Nat := findIdx (· == a) +/-- +Returns the index of the first element equal to `a`, or `none` if no element is equal to `a`. + +Examples: + * `#["carrot", "potato", "broccoli"].idxOf? "carrot" = some 0` + * `#["carrot", "potato", "broccoli"].idxOf? "broccoli" = some 2` + * `#["carrot", "potato", "broccoli"].idxOf? "tomato" = none` + * `#["carrot", "potato", "broccoli"].idxOf? "anything else" = none` +-/ def idxOf? [BEq α] (xs : Array α) (v : α) : Option Nat := (xs.finIdxOf? v).map (·.val) @@ -781,22 +1341,65 @@ def idxOf? [BEq α] (xs : Array α) (v : α) : Option Nat := def getIdx? [BEq α] (xs : Array α) (v : α) : Option Nat := xs.findIdx? fun a => a == v +/-- +Returns `true` if `p` returns `true` for any element of `as`. + +Short-circuits upon encountering the first `true`. + +The optional parameters `start` and `stop` control the region of the array to be checked. Only the +elements with indices from `start` (inclusive) to `stop` (exclusive) are checked. By default, the +entire array is checked. + +Examples: +* `#[2, 4, 6].any (· % 2 = 0) = true` +* `#[2, 4, 6].any (· % 2 = 1) = false` +* `#[2, 4, 5, 6].any (· % 2 = 0) = true` +* `#[2, 4, 5, 6].any (· % 2 = 1) = true` +-/ @[inline] def any (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool := Id.run <| as.anyM p start stop +/-- +Returns `true` if `p` returns `true` for every element of `as`. + +Short-circuits upon encountering the first `false`. + +The optional parameters `start` and `stop` control the region of the array to be checked. Only the +elements with indices from `start` (inclusive) to `stop` (exclusive) are checked. By default, the +entire array is checked. + +Examples: +* `#[a, b, c].all p = (p a && (p b && p c))` +* `#[2, 4, 6].all (· % 2 = 0) = true` +* `#[2, 4, 5, 6].all (· % 2 = 0) = false` +-/ @[inline] def all (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool := Id.run <| as.allM p start stop -/-- `as.contains a` is true if there is some element `b` in `as` such that `a == b`. -/ +/-- +Checks whether `a` is an element of `as`, using `==` to compare elements. + +`Array.elem` is a synonym that takes the element before the array. + +Examples: +* `#[1, 4, 2, 3, 3, 7].contains 3 = true` +* `Array.contains #[1, 4, 2, 3, 3, 7] 5 = false` +-/ def contains [BEq α] (as : Array α) (a : α) : Bool := as.any (a == ·) /-- -Variant of `Array.contains` with arguments reversed. +Checks whether `a` is an element of `as`, using `==` to compare elements. -For verification purposes, we simplify this to `contains`. +`Array.contains` is a synonym that takes the array before the element. + +For verification purposes, `Array.elem` is simplified to `Array.contains`. + +Example: +* `Array.elem 3 #[1, 4, 2, 3, 3, 7] = true` +* `Array.elem 5 #[1, 4, 2, 3, 3, 7] = false` -/ def elem [BEq α] (a : α) (as : Array α) : Bool := as.contains a @@ -808,40 +1411,97 @@ def elem [BEq α] (a : α) (as : Array α) : Bool := def toListImpl (as : Array α) : List α := as.foldr List.cons [] -/-- Prepends an `Array α` onto the front of a list. Equivalent to `as.toList ++ l`. -/ +/-- +Prepends an array to a list. The elements of the array are at the beginning of the resulting list. + +Equivalent to `as.toList ++ l`. + +Examples: +* `#[1, 2].toListAppend [3, 4] = [1, 2, 3, 4]` +* `#[1, 2].toListAppend [] = [1, 2]` +* `#[].toListAppend [3, 4, 5] = [3, 4, 5]` +-/ @[inline] def toListAppend (as : Array α) (l : List α) : List α := as.foldr List.cons l +/-- +Appends two arrays. Normally used via the `++` operator. + +Appending arrays takes time proportional to the length of the second array. + +Examples: + * `#[1, 2, 3] ++ #[4, 5] = #[1, 2, 3, 4, 5]`. + * `#[] ++ #[4, 5] = #[4, 5]`. + * `#[1, 2, 3] ++ #[] = #[1, 2, 3]`. +-/ protected def append (as : Array α) (bs : Array α) : Array α := bs.foldl (init := as) fun xs v => xs.push v instance : Append (Array α) := ⟨Array.append⟩ +/-- +Appends an array and a list. + +Takes time proportional to the length of the list.. + +Examples: + * `#[1, 2, 3].appendList [4, 5] = #[1, 2, 3, 4, 5]`. + * `#[].appendList [4, 5] = #[4, 5]`. + * `#[1, 2, 3].appendList [] = #[1, 2, 3]`. +-/ protected def appendList (as : Array α) (bs : List α) : Array α := bs.foldl (init := as) fun xs v => xs.push v instance : HAppend (Array α) (List α) (Array α) := ⟨Array.appendList⟩ + +/-- +Applies a monadic function that returns an array to each element of an array, from left to right. +The resulting arrays are appended. +-/ @[inline] def flatMapM [Monad m] (f : α → m (Array β)) (as : Array α) : m (Array β) := as.foldlM (init := empty) fun bs a => do return bs ++ (← f a) @[deprecated flatMapM (since := "2024-10-16")] abbrev concatMapM := @flatMapM +/-- +Applies a function that returns an array to each element of an array. The resulting arrays are +appended. + +Examples: +* `#[2, 3, 2].flatMap Array.range = #[0, 1, 0, 1, 2, 0, 1]` +* `#[['a', 'b'], ['c', 'd', 'e']].flatMap List.toArray = #['a', 'b', 'c', 'd', 'e']` +-/ @[inline] def flatMap (f : α → Array β) (as : Array α) : Array β := as.foldl (init := empty) fun bs a => bs ++ f a @[deprecated flatMap (since := "2024-10-16")] abbrev concatMap := @flatMap -/-- Joins array of array into a single array. +/-- +Appends the contents of array of arrays into a single array. The resulting array contains the same +elements as the nested arrays in the same order. -`flatten #[#[a₁, a₂, ⋯], #[b₁, b₂, ⋯], ⋯]` = `#[a₁, a₂, ⋯, b₁, b₂, ⋯]` +Examples: + * `#[#[5], #[4], #[3, 2]].flatten = #[5, 4, 3, 2]` + * `#[#[0, 1], #[], #[2], #[1, 0, 1]].flatten = #[0, 1, 2, 1, 0, 1]` + * `(#[] : Array Nat).flatten = #[]` -/ @[inline] def flatten (xss : Array (Array α)) : Array α := xss.foldl (init := empty) fun acc xs => acc ++ xs +/-- +Reverses an array by repeatedly swapping elements. + +The original array is modified in place if there are no other references to it. + +Examples: +* `(#[] : Array Nat).reverse = #[]` +* `#[0, 1].reverse = #[1, 0]` +* `#[0, 1, 2].reverse = #[2, 1, 0]` +-/ def reverse (as : Array α) : Array α := if h : as.size ≤ 1 then as @@ -860,21 +1520,113 @@ where else as +/-- +Returns the array of elements in `as` for which `p` returns `true`. + +Only elements from `start` (inclusive) to `stop` (exclusive) are considered. Elements outside that +range are discarded. By default, the entire array is considered. + +Examples: +* `#[1, 2, 5, 2, 7, 7].filter (· > 2) = #[5, 7, 7]` +* `#[1, 2, 5, 2, 7, 7].filter (fun _ => false) = #[]` +* `#[1, 2, 5, 2, 7, 7].filter (fun _ => true) = #[1, 2, 5, 2, 7, 7]` +* `#[1, 2, 5, 2, 7, 7].filter (· > 2) (start := 3) = #[7, 7]` +* `#[1, 2, 5, 2, 7, 7].filter (fun _ => true) (start := 3) = #[2, 7, 7]` +* `#[1, 2, 5, 2, 7, 7].filter (fun _ => true) (stop := 3) = #[1, 2, 5]` +-/ @[inline] def filter (p : α → Bool) (as : Array α) (start := 0) (stop := as.size) : Array α := as.foldl (init := #[]) (start := start) (stop := stop) fun acc a => if p a then acc.push a else acc +/-- +Applies the monadic predicate `p` to every element in the array, in order from left to right, and +returns the array of elements for which `p` returns `true`. + +Only elements from `start` (inclusive) to `stop` (exclusive) are considered. Elements outside that +range are discarded. By default, the entire array is checked. + +Example: +```lean example +#eval #[1, 2, 5, 2, 7, 7].filterM fun x => do + IO.println s!"Checking {x}" + return x < 3 +``` +```output +Checking 1 +Checking 2 +Checking 5 +Checking 2 +Checking 7 +Checking 7 +``` +```output +#[1, 2, 2] +``` +-/ @[inline] def filterM {α : Type} [Monad m] (p : α → m Bool) (as : Array α) (start := 0) (stop := as.size) : m (Array α) := as.foldlM (init := #[]) (start := start) (stop := stop) fun acc a => do if (← p a) then return acc.push a else return acc +/-- +Applies the monadic predicate `p` on every element in the array in reverse order, from right to +left, and returns those elements for which `p` returns `true`. The elements of the returned list are +in the same order as in the input list. + +Only elements from `start` (exclusive) to `stop` (inclusive) are considered. Elements outside that +range are discarded. Because the array is examined in reverse order, elements are only examined when +`start > stop`. By default, the entire array is considered. + +Example: +```lean example +#eval #[1, 2, 5, 2, 7, 7].filterRevM fun x => do + IO.println s!"Checking {x}" + return x < 3 +``` +```output +Checking 7 +Checking 7 +Checking 2 +Checking 5 +Checking 2 +Checking 1 +``` +```output +#[1, 2, 2] +``` +-/ @[inline] def filterRevM {α : Type} [Monad m] (p : α → m Bool) (as : Array α) (start := as.size) (stop := 0) : m (Array α) := reverse <$> as.foldrM (init := #[]) (start := start) (stop := stop) fun a acc => do if (← p a) then return acc.push a else return acc +/-- +Applies a monadic function that returns an `Option` to each element of an array, collecting the +non-`none` values. + +Only elements from `start` (inclusive) to `stop` (exclusive) are considered. Elements outside that +range are discarded. By default, the entire array is considered. + +Example: +```lean example +#eval #[1, 2, 5, 2, 7, 7].filterMapM fun x => do + IO.println s!"Examining {x}" + if x > 2 then return some (2 * x) + else return none +``` +```output +Examining 1 +Examining 2 +Examining 5 +Examining 2 +Examining 7 +Examining 7 +``` +```output +#[10, 14, 14] +``` +-/ @[specialize] def filterMapM [Monad m] (f : α → m (Option β)) (as : Array α) (start := 0) (stop := as.size) : m (Array β) := as.foldlM (init := #[]) (start := start) (stop := stop) fun bs a => do @@ -882,10 +1634,32 @@ def filterMapM [Monad m] (f : α → m (Option β)) (as : Array α) (start := 0) | some b => pure (bs.push b) | none => pure bs +/-- +Applies a function that returns an `Option` to each element of an array, collecting the non-`none` +values. + +Example: +```lean example +#eval #[1, 2, 5, 2, 7, 7].filterMap fun x => + if x > 2 then some (2 * x) else none +``` +```output +#[10, 14, 14] +``` +-/ @[inline] def filterMap (f : α → Option β) (as : Array α) (start := 0) (stop := as.size) : Array β := Id.run <| as.filterMapM f (start := start) (stop := stop) +/-- +Returns the largest element of the array, as determined by the comparison `lt`, or `none` if +the array is empty. + +Examples: +* `(#[] : Array Nat).getMax? (· < ·) = none` +* `#["red", "green", "blue"].getMax? (·.length < ·.length) = some "green"` +* `#["red", "green", "blue"].getMax? (· < ·) = some "red"` +-/ @[specialize] def getMax? (as : Array α) (lt : α → α → Bool) : Option α := if h : 0 < as.size then @@ -895,6 +1669,19 @@ def getMax? (as : Array α) (lt : α → α → Bool) : Option α := else none +/-- +Returns a pair of arrays that together contain all the elements of `as`. The first array contains +those elements for which `p` returns `true`, and the second contains those for which `p` returns +`false`. + +`as.partition p` is equivalent to `(as.filter p, as.filter (not ∘ p))`, but it is +more efficient since it only has to do one pass over the array. + +Examples: + * `#[1, 2, 5, 2, 7, 7].partition (· > 2) = (#[5, 7, 7], #[1, 2, 2])` + * `#[1, 2, 5, 2, 7, 7].partition (fun _ => false) = (#[], #[1, 2, 5, 2, 7, 7])` + * `#[1, 2, 5, 2, 7, 7].partition (fun _ => true) = (#[1, 2, 5, 2, 7, 7], #[])` +-/ @[inline] def partition (p : α → Bool) (as : Array α) : Array α × Array α := Id.run do let mut bs := #[] @@ -906,6 +1693,16 @@ def partition (p : α → Bool) (as : Array α) : Array α × Array α := Id.run cs := cs.push a return (bs, cs) +/-- +Removes all the elements that satisfy a predicate from the end of an array. + +The longest contiguous sequence of elements that all satisfy the predicate is removed. + +Examples: + * `#[0, 1, 2, 3, 4].popWhile (· > 2) = #[0, 1, 2]` + * `#[3, 2, 3, 4].popWhile (· > 2) = #[3, 2]` + * `(#[] : Array Nat).popWhile (· > 2) = #[]` +-/ @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion. def popWhile (p : α → Bool) (as : Array α) : Array α := if h : as.size > 0 then @@ -921,6 +1718,15 @@ decreasing_by simp_wf; decreasing_trivial_pre_omega popWhile p #[] = #[] := by simp [popWhile] +/-- +Returns a new array that contains the longest prefix of elements that satisfy the predicate `p` from +an array. + +Examples: + * `#[0, 1, 2, 3, 2, 1].takeWhile (· < 2) = #[0, 1]` + * `#[0, 1, 2, 3, 2, 1].takeWhile (· < 20) = #[0, 1, 2, 3, 2, 1]` + * `#[0, 1, 2, 3, 2, 1].takeWhile (· < 0) = #[]` +-/ def takeWhile (p : α → Bool) (as : Array α) : Array α := let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion. go (i : Nat) (acc : Array α) : Array α := @@ -936,11 +1742,16 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α := go 0 #[] /-- -Remove the element at a given index from an array without a runtime bounds checks, -using a `Nat` index and a tactic-provided bound. +Removes the element at a given index from an array without a run-time bounds check. -This function takes worst case O(n) time because -it has to backshift all elements at positions greater than `i`.-/ +This function takes worst-case `O(n)` time because it back-shifts all elements at positions +greater than `i`. + +Examples: +* `#["apple", "pear", "orange"].eraseIdx 0 = #["pear", "orange"]` +* `#["apple", "pear", "orange"].eraseIdx 1 = #["apple", "orange"]` +* `#["apple", "pear", "orange"].eraseIdx 2 = #["apple", "pear"]` +-/ @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion. def eraseIdx (xs : Array α) (i : Nat) (h : i < xs.size := by get_elem_tactic) : Array α := if h' : i + 1 < xs.size then @@ -961,42 +1772,79 @@ decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ h unfold eraseIdx simp [h'] -/-- Remove the element at a given index from an array, or do nothing if the index is out of bounds. +/-- +Removes the element at a given index from an array. Does nothing if the index is out of bounds. - This function takes worst case O(n) time because - it has to backshift all elements at positions greater than `i`.-/ +This function takes worst-case `O(n)` time because it back-shifts all elements at positions greater +than `i`. + +Examples: +* `#["apple", "pear", "orange"].eraseIdxIfInBounds 0 = #["pear", "orange"]` +* `#["apple", "pear", "orange"].eraseIdxIfInBounds 1 = #["apple", "orange"]` +* `#["apple", "pear", "orange"].eraseIdxIfInBounds 2 = #["apple", "pear"]` +* `#["apple", "pear", "orange"].eraseIdxIfInBounds 3 = #["apple", "pear", "orange"]` +* `#["apple", "pear", "orange"].eraseIdxIfInBounds 5 = #["apple", "pear", "orange"]` +-/ def eraseIdxIfInBounds (xs : Array α) (i : Nat) : Array α := if h : i < xs.size then xs.eraseIdx i h else xs -/-- Remove the element at a given index from an array, or panic if the index is out of bounds. +/-- +Removes the element at a given index from an array. Panics if the index is out of bounds. -This function takes worst case O(n) time because -it has to backshift all elements at positions greater than `i`. -/ +This function takes worst-case `O(n)` time because it back-shifts all elements at positions +greater than `i`. +-/ def eraseIdx! (xs : Array α) (i : Nat) : Array α := if h : i < xs.size then xs.eraseIdx i h else panic! "invalid index" -/-- Remove a specified element from an array, or do nothing if it is not present. +/-- +Removes the first occurrence of a specified element from an array, or does nothing if it is not +present. -This function takes worst case O(n) time because -it has to backshift all later elements. -/ +This function takes worst-case `O(n)` time because it back-shifts all later elements. + +Examples: +* `#[1, 2, 3].erase 2 = #[1, 3]` +* `#[1, 2, 3].erase 5 = #[1, 2, 3]` +* `#[1, 2, 3, 2, 1].erase 2 = #[1, 3, 2, 1]` +* `(#[] : List Nat).erase 2 = #[]` +-/ def erase [BEq α] (as : Array α) (a : α) : Array α := match as.finIdxOf? a with | none => as | some i => as.eraseIdx i -/-- Erase the first element that satisfies the predicate `p`. +/-- +Removes the first element that satisfies the predicate `p`. If no element satisfies `p`, the array +is returned unmodified. -This function takes worst case O(n) time because -it has to backshift all later elements. -/ +This function takes worst-case `O(n)` time because it back-shifts all later elements. + +Examples: +* `#["red", "green", "", "blue"].eraseP (·.isEmpty) = #["red", "green", "blue"]` +* `#["red", "green", "", "blue", ""].eraseP (·.isEmpty) = #["red", "green", "blue", ""]` +* `#["red", "green", "blue"].eraseP (·.length % 2 == 0) = #["red", "green"]` +* `#["red", "green", "blue"].eraseP (fun _ => true) = #["green", "blue"]` +* `(#[] : Array String).eraseP (fun _ => true) = #[]` +-/ def eraseP (as : Array α) (p : α → Bool) : Array α := match as.findFinIdx? p with | none => as | some i => as.eraseIdx i -/-- Insert element `a` at position `i`. +/-- +Inserts an element into an array at the specified index. If the index is greater than the size of +the array, then the array is returned unmodified. -This function takes worst case O(n) time because -it has to swap the inserted element into place. +In other words, the new element is inserted into the array `as` after the first `i` elements of +`as`. + +This function takes worst case `O(n)` time because it has to swap the inserted element into place. + +Examples: + * `#["tues", "thur", "sat"].insertIdx 1 "wed" = #["tues", "wed", "thur", "sat"]` + * `#["tues", "thur", "sat"].insertIdx 2 "wed" = #["tues", "thur", "wed", "sat"]` + * `#["tues", "thur", "sat"].insertIdx 3 "wed" = #["tues", "thur", "sat", "wed"]` -/ @[inline] def insertIdx (as : Array α) (i : Nat) (a : α) (_ : i ≤ as.size := by get_elem_tactic) : Array α := let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion. @@ -1014,7 +1862,21 @@ it has to swap the inserted element into place. @[deprecated insertIdx (since := "2024-11-20")] abbrev insertAt := @insertIdx -/-- Insert element `a` at position `i`. Panics if `i` is not `i ≤ as.size`. -/ +/-- +Inserts an element into an array at the specified index. Panics if the index is greater than the +size of the array. + +In other words, the new element is inserted into the array `as` after the first `i` elements of +`as`. + +This function takes worst case `O(n)` time because it has to swap the inserted element into place. +`Array.insertIdx` and `Array.insertIdxIfInBounds` are safer alternatives. + +Examples: + * `#["tues", "thur", "sat"].insertIdx! 1 "wed" = #["tues", "wed", "thur", "sat"]` + * `#["tues", "thur", "sat"].insertIdx! 2 "wed" = #["tues", "thur", "wed", "sat"]` + * `#["tues", "thur", "sat"].insertIdx! 3 "wed" = #["tues", "thur", "sat", "wed"]` +-/ def insertIdx! (as : Array α) (i : Nat) (a : α) : Array α := if h : i ≤ as.size then insertIdx as i a @@ -1022,7 +1884,21 @@ def insertIdx! (as : Array α) (i : Nat) (a : α) : Array α := @[deprecated insertIdx! (since := "2024-11-20")] abbrev insertAt! := @insertIdx! -/-- Insert element `a` at position `i`, or do nothing if `as.size < i`. -/ +/-- +Inserts an element into an array at the specified index. The array is returned unmodified if the +index is greater than the size of the array. + +In other words, the new element is inserted into the array `as` after the first `i` elements of +`as`. + +This function takes worst case `O(n)` time because it has to swap the inserted element into place. + +Examples: + * `#["tues", "thur", "sat"].insertIdxIfInBounds 1 "wed" = #["tues", "wed", "thur", "sat"]` + * `#["tues", "thur", "sat"].insertIdxIfInBounds 2 "wed" = #["tues", "thur", "wed", "sat"]` + * `#["tues", "thur", "sat"].insertIdxIfInBounds 3 "wed" = #["tues", "thur", "sat", "wed"]` + * `#["tues", "thur", "sat"].insertIdxIfInBounds 4 "wed" = #["tues", "thur", "sat"]` +-/ def insertIdxIfInBounds (as : Array α) (i : Nat) (a : α) : Array α := if h : i ≤ as.size then insertIdx as i a @@ -1043,8 +1919,15 @@ def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : N true decreasing_by simp_wf; decreasing_trivial_pre_omega -/-- Return true iff `as` is a prefix of `bs`. -That is, `bs = as ++ t` for some `t : List α`.-/ +/-- +Return `true` if `as` is a prefix of `bs`, or `false` otherwise. + +Examples: + * `#[0, 1, 2].isPrefixOf #[0, 1, 2, 3] = true` + * `#[0, 1, 2].isPrefixOf #[0, 1, 2] = true` + * `#[0, 1, 2].isPrefixOf #[0, 1] = false` + * `#[].isPrefixOf #[0, 1] = true` +-/ def isPrefixOf [BEq α] (as bs : Array α) : Bool := if h : as.size ≤ bs.size then isPrefixOfAux as bs h 0 @@ -1064,12 +1947,42 @@ def zipWithAux (as : Array α) (bs : Array β) (f : α → β → γ) (i : Nat) cs decreasing_by simp_wf; decreasing_trivial_pre_omega +/-- +Applies a function to the corresponding elements of two arrays, stopping at the end of the shorter +array. + +Examples: +* `#[1, 2].zipWith (· + ·) #[5, 6] = #[6, 8]` +* `#[1, 2, 3].zipWith (· + ·) #[5, 6, 10] = #[6, 8, 13]` +* `#[].zipWith (· + ·) #[5, 6] = #[]` +* `#[x₁, x₂, x₃].zipWith f #[y₁, y₂, y₃, y₄] = #[f x₁ y₁, f x₂ y₂, f x₃ y₃]` +-/ @[inline] def zipWith (f : α → β → γ) (as : Array α) (bs : Array β) : Array γ := zipWithAux as bs f 0 #[] +/-- +Combines two arrays into an array of pairs in which the first and second components are the +corresponding elements of each input array. The resulting array is the length of the shorter of the +input arrays. + +Examples: +* `#["Mon", "Tue", "Wed"].zip #[1, 2, 3] = #[("Mon", 1), ("Tue", 2), ("Wed", 3)]` +* `#["Mon", "Tue", "Wed"].zip #[1, 2] = #[("Mon", 1), ("Tue", 2)]` +* `#[x₁, x₂, x₃].zip #[y₁, y₂, y₃, y₄] = #[(x₁, y₁), (x₂, y₂), (x₃, y₃)]` +-/ def zip (as : Array α) (bs : Array β) : Array (α × β) := zipWith Prod.mk as bs +/-- +Applies a function to the corresponding elements of both arrays, stopping when there are no more +elements in either array. If one array is shorter than the other, the function is passed `none` for +the missing elements. + +Examples: +* `#[1, 6].zipWithAll min #[5, 2] = #[some 1, some 2]` +* `#[1, 2, 3].zipWithAll Prod.mk #[5, 6] = #[(some 1, some 5), (some 2, some 6), (some 3, none)]` +* `#[x₁, x₂].zipWithAll f #[y] = #[f (some x₁) (some y), f (some x₂) none]` +-/ def zipWithAll (f : Option α → Option β → γ) (as : Array α) (bs : Array β) : Array γ := go as bs 0 #[] where go (as : Array α) (bs : Array β) (i : Nat) (cs : Array γ) := @@ -1082,6 +1995,14 @@ where go (as : Array α) (bs : Array β) (i : Nat) (cs : Array γ) := termination_by max as.size bs.size - i decreasing_by simp_wf; decreasing_trivial_pre_omega +/-- +Separates an array of pairs into two arrays that contain the respective first and second components. + +Examples: +* `#[("Monday", 1), ("Tuesday", 2)].unzip = (#["Monday", "Tuesday"], #[1, 2])` +* `#[(x₁, y₁), (x₂, y₂), (x₃, y₃)].unzip = (#[x₁, x₂, x₃], #[y₁, y₂, y₃])` +* `(#[] : Array (Nat × String)).unzip = ((#[], #[]) : List Nat × List String)` +-/ def unzip (as : Array (α × β)) : Array α × Array β := as.foldl (init := (#[], #[])) fun (as, bs) (a, b) => (as.push a, bs.push b) @@ -1090,6 +2011,15 @@ def split (as : Array α) (p : α → Bool) : Array α × Array α := as.foldl (init := (#[], #[])) fun (as, bs) a => if p a then (as.push a, bs) else (as, bs.push a) +/-- +Replaces the first occurrence of `a` with `b` in an array. The modification is performed in-place +when the reference to the array is unique. Returns the array unmodified when `a` is not present. + +Examples: +* `#[1, 2, 3, 2, 1].replace 2 5 = #[1, 5, 3, 2, 1]` +* `#[1, 2, 3, 2, 1].replace 0 5 = #[1, 2, 3, 2, 1]` +* `#[].replace 2 5 = #[]` +-/ def replace [BEq α] (xs : Array α) (a b : α) : Array α := match xs.finIdxOf? a with | none => xs @@ -1110,14 +2040,26 @@ We do not currently intend to provide verification theorems for these functions. /-! ### leftpad and rightpad -/ /-- -Pads `l : Array α` on the left with repeated occurrences of `a : α` until it is of size `n`. -If `l` is initially larger than `n`, just return `l`. +Pads `xs : Array α` on the left with repeated occurrences of `a : α` until it is of size `n`. If `xs` +already has at least `n` elements, it is returned unmodified. + +Examples: + * `#[1, 2, 3].leftpad 5 0 = #[0, 0, 1, 2, 3]` + * `#["red", "green", "blue"].leftpad 4 "blank" = #["blank", "red", "green", "blue"]` + * `#["red", "green", "blue"].leftpad 3 "blank" = #["red", "green", "blue"]` + * `#["red", "green", "blue"].leftpad 1 "blank" = #["red", "green", "blue"]` -/ def leftpad (n : Nat) (a : α) (xs : Array α) : Array α := mkArray (n - xs.size) a ++ xs /-- -Pads `l : Array α` on the right with repeated occurrences of `a : α` until it is of size `n`. -If `l` is initially larger than `n`, just return `l`. +Pads `xs : Array α` on the right with repeated occurrences of `a : α` until it is of length `n`. If +`l` already has at least `n` elements, it is returned unmodified. + +Examples: + * `#[1, 2, 3].rightpad 5 0 = #[1, 2, 3, 0, 0]` + * `#["red", "green", "blue"].rightpad 4 "blank" = #["red", "green", "blue", "blank"]` + * `#["red", "green", "blue"].rightpad 3 "blank" = #["red", "green", "blue"]` + * `#["red", "green", "blue"].rightpad 1 "blank" = #["red", "green", "blue"]` -/ def rightpad (n : Nat) (a : α) (xs : Array α) : Array α := xs ++ mkArray (n - xs.size) a @@ -1130,8 +2072,12 @@ def rightpad (n : Nat) (a : α) (xs : Array α) : Array α := xs ++ mkArray (n - /-! ### eraseReps -/ /-- -`O(|l|)`. Erase repeated adjacent elements. Keeps the first occurrence of each run. -* `eraseReps #[1, 3, 2, 2, 2, 3, 5] = #[1, 3, 2, 3, 5]` +Erases repeated elements, keeping the first element of each run. + +`O(|as|)`. + +Example: +* `#[1, 3, 2, 2, 2, 3, 3, 5].eraseReps = #[1, 3, 2, 3, 5]` -/ def eraseReps {α} [BEq α] (as : Array α) : Array α := if h : 0 < as.size then @@ -1157,11 +2103,29 @@ private def allDiffAux [BEq α] (as : Array α) (i : Nat) : Bool := true decreasing_by simp_wf; decreasing_trivial_pre_omega +/-- +Returns `true` if no two elements of `as` are equal according to the `==` operator. + +Examples: + * `#["red", "green", "blue"].allDiff = true` + * `#["red", "green", "red"].allDiff = false` + * `(#[] : Array Nat).allDiff = true` +-/ def allDiff [BEq α] (as : Array α) : Bool := allDiffAux as 0 /-! ### getEvenElems -/ +/-- +Returns a new array that contains the elements at even indices in `as`, starting with the element at +index `0`. + +Examples: +* `#[0, 1, 2, 3, 4].getEvenElems = #[0, 2, 4]` +* `#[1, 2, 3, 4].getEvenElems = #[1, 3]` +* `#["red", "green", "blue"].getEvenElems = #["red", "blue"]` +* `(#[] : Array String).getEvenElems = #[]` +-/ @[inline] def getEvenElems (as : Array α) : Array α := (·.2) <| as.foldl (init := (true, Array.empty)) fun (even, acc) a => if even then diff --git a/src/Init/Data/Array/BasicAux.lean b/src/Init/Data/Array/BasicAux.lean index ba1ef50afd..a7849840c8 100644 --- a/src/Init/Data/Array/BasicAux.lean +++ b/src/Init/Data/Array/BasicAux.lean @@ -38,6 +38,11 @@ private theorem List.of_toArrayAux_eq_toArrayAux {as bs : List α} {cs ds : Arra theorem List.toArray_eq_toArray_eq (as bs : List α) : (as.toArray = bs.toArray) = (as = bs) := by simp +/-- +Applies the monadic action `f` to every element in the array, left-to-right, and returns the array +of results. Furthermore, the resulting array's type guarantees that it contains the same number of +elements as the input array. +-/ def Array.mapM' [Monad m] (f : α → m β) (as : Array α) : m { bs : Array β // bs.size = as.size } := go 0 ⟨mkEmpty as.size, rfl⟩ (by simp) where @@ -66,11 +71,19 @@ where return as /-- -Monomorphic `Array.mapM`. The internal implementation uses pointer equality, and does not allocate a new array -if the result of each `f a` is a pointer equal value `a`. +Applies a monadic function to each element of an array, returning the array of results. The function is +monomorphic: it is required to return a value of the same type. The internal implementation uses +pointer equality, and does not allocate a new array if the result of each function call is +pointer-equal to its argument. -/ @[implemented_by mapMonoMImp] def Array.mapMonoM [Monad m] (as : Array α) (f : α → m α) : m (Array α) := as.mapM f +/-- +Applies a function to each element of an array, returning the array of results. The function is +monomorphic: it is required to return a value of the same type. The internal implementation uses +pointer equality, and does not allocate a new array if the result of each function call is +pointer-equal to its argument. +-/ @[inline] def Array.mapMono (as : Array α) (f : α → α) : Array α := Id.run <| as.mapMonoM f diff --git a/src/Init/Data/Array/BinSearch.lean b/src/Init/Data/Array/BinSearch.lean index 5145813dc4..9c5b2668df 100644 --- a/src/Init/Data/Array/BinSearch.lean +++ b/src/Init/Data/Array/BinSearch.lean @@ -29,6 +29,16 @@ namespace Array else found (some a) termination_by lo hi => hi.1 - lo.1 +/-- +Binary search for an element equivalent to `k` in the sorted array `as`. Returns the element from +the array, if it is found, or `none` otherwise. + +The array `as` must be sorted according to the comparison operator `lt`, which should be a total +order. + +The optional parameters `lo` and `hi` determine the region of the array indices to be searched. Both +are inclusive, and default to searching the entire array. +-/ @[inline] def binSearch {α : Type} (as : Array α) (k : α) (lt : α → α → Bool) (lo := 0) (hi := as.size - 1) : Option α := if h : lo < as.size then let hi := if hi < as.size then hi else as.size - 1 @@ -39,6 +49,16 @@ termination_by lo hi => hi.1 - lo.1 else none +/-- +Binary search for an element equivalent to `k` in the sorted array `as`. Returns `true` if the +element is found, or `false` otherwise. + +The array `as` must be sorted according to the comparison operator `lt`, which should be a total +order. + +The optional parameters `lo` and `hi` determine the region of the array indices to be searched. Both +are inclusive, and default to searching the entire array. +-/ @[inline] def binSearchContains {α : Type} (as : Array α) (k : α) (lt : α → α → Bool) (lo := 0) (hi := as.size - 1) : Bool := if h : lo < as.size then let hi := if hi < as.size then hi else as.size - 1 @@ -68,6 +88,16 @@ termination_by lo hi => hi.1 - lo.1 as.modifyM mid <| fun v => merge v termination_by lo hi => hi.1 - lo.1 +/-- +Inserts an element `k` into a sorted array `as` such that the resulting array is sorted. + +The ordering predicate `lt` should be a total order on elements, and the array `as` should be sorted +with respect to `lt`. + +If an element that `lt` equates to `k` is already present in `as`, then `merge` is applied to the +existing element to determine the value of that position in the resulting array. If no element equal +to `k` is present, then `add` is used to determine the value to be inserted. +-/ @[specialize] def binInsertM {α : Type u} {m : Type u → Type v} [Monad m] (lt : α → α → Bool) (merge : α → m α) @@ -81,6 +111,21 @@ termination_by lo hi => hi.1 - lo.1 else if !lt k as[as.size - 1] then as.modifyM (as.size - 1) <| merge else binInsertAux lt merge add as k ⟨0, by omega⟩ ⟨as.size - 1, by omega⟩ (by simp) (by simpa using h') +/-- +Inserts an element into a sorted array such that the resulting array is sorted. If the element is +already present in the array, it is not inserted. + +The ordering predicate `lt` should be a total order on elements, and the array `as` should be sorted +with respect to `lt`. + +`Array.binInsertM` is a more general operator that provides greater control over the handling of +duplicate elements in addition to running in a monad. + +Examples: +* `#[0, 1, 3, 5].binInsert (· < ·) 2 = #[0, 1, 2, 3, 5]` +* `#[0, 1, 3, 5].binInsert (· < ·) 1 = #[0, 1, 3, 5]` +* `#[].binInsert (· < ·) 1 = #[1]` +-/ @[inline] def binInsert {α : Type u} (lt : α → α → Bool) (as : Array α) (k : α) : Array α := Id.run <| binInsertM lt (fun _ => k) (fun _ => k) as k diff --git a/src/Init/Data/Array/FinRange.lean b/src/Init/Data/Array/FinRange.lean index c6e4279b4d..2cc622385d 100644 --- a/src/Init/Data/Array/FinRange.lean +++ b/src/Init/Data/Array/FinRange.lean @@ -12,7 +12,13 @@ set_option linter.indexVariables true -- Enforce naming conventions for index va namespace Array -/-- `finRange n` is the array of all elements of `Fin n` in order. -/ +/-- +Returns an array of all elements of `Fin n` in order, starting at `0`. + +Examples: + * `Array.finRange 0 = (#[] : Array (Fin 0))` + * `Array.finRange 2 = (#[0, 1] : Array (Fin 2))` +-/ protected def finRange (n : Nat) : Array (Fin n) := ofFn fun i => i @[simp] theorem size_finRange (n) : (Array.finRange n).size = n := by diff --git a/src/Init/Data/Array/InsertionSort.lean b/src/Init/Data/Array/InsertionSort.lean index 1c2072563b..5ea2c62ecc 100644 --- a/src/Init/Data/Array/InsertionSort.lean +++ b/src/Init/Data/Array/InsertionSort.lean @@ -9,6 +9,12 @@ import Init.Data.Array.Basic set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. set_option linter.indexVariables true -- Enforce naming conventions for index variables. +/-- +Sorts an array using insertion sort. + +The optional parameter `lt` specifies an ordering predicate. It defaults to `LT.lt`, which must be +decidable to be used for sorting. +-/ @[inline] def Array.insertionSort (xs : Array α) (lt : α → α → Bool := by exact (· < ·)) : Array α := traverse xs 0 xs.size where diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index 1051c99585..1fcc145b73 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -3921,7 +3921,15 @@ theorem all_reverse {xs : Array α} : xs.reverse.all f 0 = xs.all f := by /-! ### toListRev -/ -/-- A more efficient version of `arr.toList.reverse`; for verification purposes we immediately simplify it. -/ +/-- +Converts an array to a list that contains the same elements in the opposite order. + +This is equivalent to, but more efficient than, `Array.toList ∘ List.reverse`. + +Examples: +* `#[1, 2, 3].toListRev = [3, 2, 1]` +* `#["blue", "yellow"].toListRev = ["yellow", "blue"]` +-/ @[inline] def toListRev (xs : Array α) : List α := xs.foldl (fun l t => t :: l) [] @[simp] theorem toListRev_eq (xs : Array α) : xs.toListRev = xs.toList.reverse := by diff --git a/src/Init/Data/Array/Lex/Basic.lean b/src/Init/Data/Array/Lex/Basic.lean index ccc9e0d759..a5b4b978dc 100644 --- a/src/Init/Data/Array/Lex/Basic.lean +++ b/src/Init/Data/Array/Lex/Basic.lean @@ -14,11 +14,12 @@ set_option linter.indexVariables true -- Enforce naming conventions for index va namespace Array /-- -Lexicographic comparator for arrays. +Compares arrays lexicographically with respect to a comparison `lt` on their elements. -`lex as bs lt` is true if -- `bs` is larger than `as` and `as` is pairwise equivalent via `==` to the initial segment of `bs`, or -- there is an index `i` such that `lt as[i] bs[i]`, and for all `j < i`, `as[j] == bs[j]`. +Specifically, `Array.lex as bs lt` is true if +* `bs` is larger than `as` and `as` is pairwise equivalent via `==` to the initial segment of `bs`, + or +* there is an index `i` such that `lt as[i] bs[i]`, and for all `j < i`, `as[j] == bs[j]`. -/ def lex [BEq α] (as bs : Array α) (lt : α → α → Bool := by exact (· < ·)) : Bool := Id.run do for h : i in [0 : min as.size bs.size] do diff --git a/src/Init/Data/Array/QSort.lean b/src/Init/Data/Array/QSort.lean index b4ee01fb3f..118e66e06b 100644 --- a/src/Init/Data/Array/QSort.lean +++ b/src/Init/Data/Array/QSort.lean @@ -30,6 +30,16 @@ private def qpartition {n} (as : Vector α n) (lt : α → α → Bool) (lo hi : (⟨i, ilo⟩, as.swap i hi) loop as lo lo +/-- +Sorts an array using the Quicksort algorithm. + +The optional parameter `lt` specifies an ordering predicate. It defaults to `LT.lt`, which must be +decidable to be used for sorting. Use `Array.qsortOrd` to sort the array according to the `Ord α` +instance. + +The optional parameters `low` and `high` delimit the region of the array that is sorted. Both are +inclusive, and default to sorting the entire array. +-/ @[inline] def qsort (as : Array α) (lt : α → α → Bool := by exact (· < ·)) (low := 0) (high := as.size - 1) : Array α := let rec @[specialize] sort {n} (as : Vector α n) (lo hi : Nat) @@ -50,7 +60,7 @@ private def qpartition {n} (as : Vector α n) (lt : α → α → Bool) (lo hi : set_option linter.unusedVariables.funArgs false in /-- -Sort an array using `compare` to compare elements. +Sorts an array using the Quicksort algorithm, using `Ord.compare` to compare elements. -/ def qsortOrd [ord : Ord α] (xs : Array α) : Array α := xs.qsort fun x y => compare x y |>.isLT diff --git a/src/Init/Data/Array/Set.lean b/src/Init/Data/Array/Set.lean index 85c40e84ff..5b19bbcbda 100644 --- a/src/Init/Data/Array/Set.lean +++ b/src/Init/Data/Array/Set.lean @@ -11,11 +11,16 @@ set_option linter.indexVariables true -- Enforce naming conventions for index va /-- -Set an element in an array, using a proof that the index is in bounds. -(This proof can usually be omitted, and will be synthesized automatically.) +Replaces the element at a given index in an array. -This will perform the update destructively provided that `a` has a reference -count of 1 when called. +No bounds check is performed, but the function requires a proof that the index is in bounds. This +proof can usually be omitted, and will be synthesized automatically. + +The array is modified in-place if there are no other references to it. + +Examples: +* `#[0, 1, 2].set 1 5 = #[0, 5, 2]` +* `#["orange", "apple"].set 1 "grape" = #["orange", "grape"]` -/ @[extern "lean_array_fset"] def Array.set (xs : Array α) (i : @& Nat) (v : α) (h : i < xs.size := by get_elem_tactic) : @@ -23,10 +28,15 @@ def Array.set (xs : Array α) (i : @& Nat) (v : α) (h : i < xs.size := by get_e toList := xs.toList.set i v /-- -Set an element in an array, or do nothing if the index is out of bounds. +Replaces the element at the provided index in an array. The array is returned unmodified if the +index is out of bounds. -This will perform the update destructively provided that `a` has a reference -count of 1 when called. +The array is modified in-place if there are no other references to it. + +Examples: +* `#[0, 1, 2].setIfInBounds 1 5 = #[0, 5, 2]` +* `#["orange", "apple"].setIfInBounds 1 "grape" = #["orange", "grape"]` +* `#["orange", "apple"].setIfInBounds 5 "grape" = #["orange", "apple"]` -/ @[inline] def Array.setIfInBounds (xs : Array α) (i : Nat) (v : α) : Array α := dite (LT.lt i xs.size) (fun h => xs.set i v h) (fun _ => xs) diff --git a/src/Init/Data/List/Attach.lean b/src/Init/Data/List/Attach.lean index 0b56f219d9..101ebd61f9 100644 --- a/src/Init/Data/List/Attach.lean +++ b/src/Init/Data/List/Attach.lean @@ -41,7 +41,7 @@ elements in the corresponding subtype `{ x // P x }`. (l : List α) (P : α → Prop) (H : ∀ x ∈ l, P x) : List {x // P x} := pmap Subtype.mk l H /-- -"Attaches" the proof that the elements of `l` are in fact elements of `l`, producing a new list with +“Attaches” the proof that the elements of `l` are in fact elements of `l`, producing a new list with the same elements but in the subtype `{ x // x ∈ l }`. `O(1)`. diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index 99ab13985d..3f54c30571 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -259,7 +259,7 @@ instance decidableLE [DecidableEq α] [LT α] [DecidableLT α] (l₁ l₂ : List inferInstanceAs (Decidable (Not _)) /-- -Compare lists lexicographically with respect to a comparison on their elements. +Compares lists lexicographically with respect to a comparison on their elements. The lexicographic order with respect to `lt` is: * `[].lex (b :: bs)` is `true` @@ -493,7 +493,7 @@ Returns the list of elements in `l` for which `p` returns `true`. `O(|l|)`. Examples: -* `[1, 2, 5, 2, 7, 7].filter (· > 2) = [5, 7, 7]` +* `[1, 2, 5, 2, 7, 7].filter (· > 2) = [5, 7, 7]` * `[1, 2, 5, 2, 7, 7].filter (fun _ => false) = []` * `[1, 2, 5, 2, 7, 7].filter (fun _ => true) = [1, 2, 5, 2, 7, 7]` -/ @@ -766,10 +766,10 @@ Pads `l : List α` on the left with repeated occurrences of `a : α` until it is already has at least `n` elements, it is returned unmodified. Examples: - * `[1, 2, 3].leftPad 5 0 = [0, 0, 1, 2, 3]` - * `["red", "green", "blue"].leftPad 4 "blank" = ["blank", "red", "green", "blue"]` - * `["red", "green", "blue"].leftPad 3 "blank" = ["red", "green", "blue"]` - * `["red", "green", "blue"].leftPad 1 "blank" = ["red", "green", "blue"]` + * `[1, 2, 3].leftpad 5 0 = [0, 0, 1, 2, 3]` + * `["red", "green", "blue"].leftpad 4 "blank" = ["blank", "red", "green", "blue"]` + * `["red", "green", "blue"].leftpad 3 "blank" = ["red", "green", "blue"]` + * `["red", "green", "blue"].leftpad 1 "blank" = ["red", "green", "blue"]` -/ def leftpad (n : Nat) (a : α) (l : List α) : List α := replicate (n - length l) a ++ l @@ -779,10 +779,10 @@ Pads `l : List α` on the right with repeated occurrences of `a : α` until it i `l` already has at least `n` elements, it is returned unmodified. Examples: - * `[1, 2, 3].rightPad 5 0 = [1, 2, 3, 0, 0]` - * `["red", "green", "blue"].rightPad 4 "blank" = ["red", "green", "blue", "blank"]` - * `["red", "green", "blue"].rightPad 3 "blank" = ["red", "green", "blue"]` - * `["red", "green", "blue"].rightPad 1 "blank" = ["red", "green", "blue"]` + * `[1, 2, 3].rightpad 5 0 = [1, 2, 3, 0, 0]` + * `["red", "green", "blue"].rightpad 4 "blank" = ["red", "green", "blue", "blank"]` + * `["red", "green", "blue"].rightpad 3 "blank" = ["red", "green", "blue"]` + * `["red", "green", "blue"].rightpad 1 "blank" = ["red", "green", "blue"]` -/ def rightpad (n : Nat) (a : α) (l : List α) : List α := l ++ replicate (n - length l) a @@ -1702,7 +1702,6 @@ Examples: * `[7, 6, 5, 8, 1, 2, 6].findIdx (· < 5) = some 4` * `[7, 6, 5, 8, 1, 2, 6].findIdx (· < 1) = none` -/ - def findIdx? (p : α → Bool) (l : List α) : Option Nat := go l 0 where @@ -1866,7 +1865,7 @@ def isPerm [BEq α] : List α → List α → Bool /-! ### any -/ /-- -Returns true if `p` returns `true` for any element of `l`. +Returns `true` if `p` returns `true` for any element of `l`. `O(|l|)`. Short-circuits upon encountering the first `true`. @@ -1886,7 +1885,7 @@ def any : (l : List α) → (p : α → Bool) → Bool /-! ### all -/ /-- -Returns true if `p` returns `true` for every element of `l`. +Returns `true` if `p` returns `true` for every element of `l`. `O(|l|)`. Short-circuits upon encountering the first `false`. @@ -1966,7 +1965,7 @@ Examples: /-- Combines two lists into a list of pairs in which the first and second components are the -corresponding elements of each list. The resulting list is the length of the shorter of the inputs +corresponding elements of each list. The resulting list is the length of the shorter of the input lists. `O(min |xs| |ys|)`. diff --git a/src/Init/Data/List/Control.lean b/src/Init/Data/List/Control.lean index e82a2df667..b678e7a65e 100644 --- a/src/Init/Data/List/Control.lean +++ b/src/Init/Data/List/Control.lean @@ -46,7 +46,7 @@ Users that want to use `mapM` with `Applicative` should use `mapA` instead. -/ /-- -Applies the monadic action `f` on every element in the list, left-to-right, and returns the list of +Applies the monadic action `f` to every element in the list, left-to-right, and returns the list of results. This implementation is tail recursive. `List.mapM'` is a a non-tail-recursive variant that may be @@ -243,7 +243,7 @@ def foldlM {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} : (f : s /-- Folds a monadic function over a list from the right, accumulating a value starting with `init`. The -accumulated value is combined with the each element of the list in order, using `f`. +accumulated value is combined with the each element of the list in reverse order, using `f`. Example: ```lean example diff --git a/src/Init/Data/List/FinRange.lean b/src/Init/Data/List/FinRange.lean index d1aaca3bc2..79d3624844 100644 --- a/src/Init/Data/List/FinRange.lean +++ b/src/Init/Data/List/FinRange.lean @@ -15,8 +15,8 @@ namespace List Lists all elements of `Fin n` in order, starting at `0`. Examples: - * `List.finRange 0 = ([] : List Fin 0)` - * `List.finRange 2 = ([0, 1] : List Fin 2)` + * `List.finRange 0 = ([] : List (Fin 0))` + * `List.finRange 2 = ([0, 1] : List (Fin 2))` -/ def finRange (n : Nat) : List (Fin n) := ofFn fun i => i diff --git a/src/Init/Data/Vector/Basic.lean b/src/Init/Data/Vector/Basic.lean index c9d616fbf6..0031b4d30e 100644 --- a/src/Init/Data/Vector/Basic.lean +++ b/src/Init/Data/Vector/Basic.lean @@ -29,7 +29,9 @@ deriving Repr, DecidableEq attribute [simp] Vector.size_toArray -/-- Convert `xs : Array α` to `Vector α xs.size`. -/ +/-- +Converts an array to a vector. The resulting vector's size is the array's size. +-/ abbrev Array.toVector (xs : Array α) : Vector α xs.size := .mk xs rfl namespace Vector diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index 1a49f03c58..d952cb8859 100644 --- a/src/Init/Meta.lean +++ b/src/Init/Meta.lean @@ -1207,9 +1207,19 @@ private partial def filterSepElemsMAux {m : Type → Type} [Monad m] (a : Array else pure acc +/-- +Filters an array of syntax, treating every other element as a separator rather than an element to +test with the monadic predicate `p`. The resulting array contains the tested elements for which `p` +returns `true`, separated by the corresponding separator elements. +-/ def filterSepElemsM {m : Type → Type} [Monad m] (a : Array Syntax) (p : Syntax → m Bool) : m (Array Syntax) := filterSepElemsMAux a p 0 #[] +/-- +Filters an array of syntax, treating every other element as a separator rather than an element to +test with the predicate `p`. The resulting array contains the tested elements for which `p` returns +`true`, separated by the corresponding separator elements. +-/ def filterSepElems (a : Array Syntax) (p : Syntax → Bool) : Array Syntax := Id.run <| a.filterSepElemsM p diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index af4b481ee9..98cc6c400d 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -2717,45 +2717,47 @@ def panic {α : Sort u} [Inhabited α] (msg : String) : α := attribute [nospecialize] Inhabited /-- -`Array α` is the type of [dynamic arrays](https://en.wikipedia.org/wiki/Dynamic_array) -with elements from `α`. This type has special support in the runtime. +`Array α` is the type of [dynamic arrays](https://en.wikipedia.org/wiki/Dynamic_array) with elements +from `α`. This type has special support in the runtime. -Arrays perform best when unshared; as long -as they are used "linearly" all updates will be performed destructively on the -array, so it has comparable performance to mutable arrays in imperative -programming languages. +Arrays perform best when unshared. As long as there is never more than one reference to an array, +all updates will be performed _destructively_. This results in performance comparable to mutable +arrays in imperative programming languages. -An array has a size and a capacity; the size is `Array.size` but the capacity -is not observable from Lean code. `Array.emptyWithCapacity n` creates an array which is equal to `#[]`, -but internally allocates an array of capacity `n`. +An array has a size and a capacity. The size is the number of elements present in the array, while +the capacity is the amount of memory currently allocated for elements. The size is accessible via +`Array.size`, but the capacity is not observable from Lean code. `Array.emptyWithCapacity n` creates +an array which is equal to `#[]`, but internally allocates an array of capacity `n`. When the size +exceeds the capacity, allocation is required to grow the array. -From the point of view of proofs `Array α` is just a wrapper around `List α`. +From the point of view of proofs, `Array α` is just a wrapper around `List α`. -/ structure Array (α : Type u) where /-- Converts a `List α` into an `Array α`. - You can also use the synonym `List.toArray` when dot notation is convenient. + The function `List.toArray` is preferred. - At runtime, this constructor is implemented by `List.toArrayImpl` and is O(n) in the length of the - list. + At runtime, this constructor is overridden by `List.toArrayImpl` and is `O(n)` in the length of + the list. -/ mk :: /-- - Converts a `Array α` into an `List α`. + Converts an `Array α` into a `List α` that contains the same elements in the same order. - At runtime, this projection is implemented by `Array.toListImpl` and is O(n) in the length of the - array. -/ + At runtime, this is implemented by `Array.toListImpl` and is `O(n)` in the length of the + array. + -/ toList : List α attribute [extern "lean_array_to_list"] Array.toList attribute [extern "lean_array_mk"] Array.mk /-- -Converts a `List α` into an `Array α`. `O(|xs|)`. +Converts a `List α` into an `Array α`. -At runtime, this operation is implemented by `List.toArrayImpl` and takes time linear in the length -of the list. `List.toArray` should be used instead of `Array.mk`. + `O(|xs|)`. At runtime, this operation is implemented by `List.toArrayImpl` and takes time linear in +the length of the list. `List.toArray` should be used instead of `Array.mk`. Examples: * `[1, 2, 3].toArray = #[1, 2, 3]` @@ -2764,7 +2766,8 @@ Examples: @[match_pattern] abbrev List.toArray (xs : List α) : Array α := .mk xs -/-- Construct a new empty array with initial capacity `c`. +/-- +Constructs a new empty array with initial capacity `c`. This will be deprecated in favor of `Array.emptyWithCapacity` in the future. -/ @@ -2774,14 +2777,26 @@ def Array.mkEmpty {α : Type u} (c : @& Nat) : Array α where set_option linter.unusedVariables false in -/-- Construct a new empty array with initial capacity `c`. -/ +/-- +Constructs a new empty array with initial capacity `c`. +-/ def Array.emptyWithCapacity {α : Type u} (c : @& Nat) : Array α where toList := List.nil -/-- Construct a new empty array. -/ +/-- +Constructs a new empty array with initial capacity `0`. + +Use `Array.emptyWithCapacity` to create an array with a greater initial capacity. +-/ def Array.empty {α : Type u} : Array α := emptyWithCapacity 0 -/-- Get the size of an array. This is a cached value, so it is O(1) to access. -/ +/-- +Gets the number of elements stored in an array. + +This is a cached value, so it is `O(1)` to access. The space allocated for an array, referred to as +its _capacity_, is at least as large as its size, but may be larger. The capacity of an array is an +internal detail that's not observable by Lean code. +-/ @[reducible, extern "lean_array_get_size"] def Array.size {α : Type u} (a : @& Array α) : Nat := a.toList.length @@ -2800,7 +2815,18 @@ arrays. def Array.getInternal {α : Type u} (a : @& Array α) (i : @& Nat) (h : LT.lt i a.size) : α := a.toList.get ⟨i, h⟩ -/-- Access an element from an array, or return `v₀` if the index is out of bounds. -/ +/-- +Returns the element at the provided index, counting from `0`. Returns the fallback value `v₀` if the +index is out of bounds. + +To return an `Option` depending on whether the index is in bounds, use `a[i]?`. To panic if the +index is out of bounds, use `a[i]!`. + +Examples: + * `#["spring", "summer", "fall", "winter"].getD 2 "never" = "fall"` + * `#["spring", "summer", "fall", "winter"].getD 0 "never" = "spring"` + * `#["spring", "summer", "fall", "winter"].getD 4 "never" = "never"` +-/ @[inline] abbrev Array.getD (a : Array α) (i : Nat) (v₀ : α) : α := dite (LT.lt i a.size) (fun h => a.getInternal i h) (fun _ => v₀) @@ -2814,8 +2840,14 @@ def Array.get!Internal {α : Type u} [Inhabited α] (a : @& Array α) (i : @& Na Array.getD a i default /-- -Push an element onto the end of an array. This is amortized O(1) because -`Array α` is internally a dynamic array. +Adds an element to the end of an array. The resulting array's size is one greater than the input +array. If there are no other references to the array, then it is modified in-place. + +This takes amortized `O(1)` time because `Array α` is represented by a dynamic array. + +Examples: +* `#[].push "apple" = #["apple"]` +* `#["apple"].push "orange" = #["apple", "orange"]` -/ @[extern "lean_array_push"] def Array.push {α : Type u} (a : Array α) (v : α) : Array α where @@ -2869,9 +2901,21 @@ protected def Array.appendCore {α : Type u} (as : Array α) (bs : Array α) : loop bs.size 0 as /-- - Returns the slice of `as` from indices `start` to `stop` (exclusive). - If `start` is greater or equal to `stop`, the result is empty. - If `stop` is greater than the length of `as`, the length is used instead. -/ +Returns the slice of `as` from indices `start` to `stop` (exclusive). The resulting array has size +`(min stop as.size) - start`. + +If `start` is greater or equal to `stop`, the result is empty. If `stop` is greater than the size of +`as`, the size is used instead. + +Examples: + * `#[0, 1, 2, 3, 4].extract 1 3 = #[1, 2]` + * `#[0, 1, 2, 3, 4].extract 1 30 = #[1, 2, 3, 4]` + * `#[0, 1, 2, 3, 4].extract 0 0 = #[]` + * `#[0, 1, 2, 3, 4].extract 2 1 = #[]` + * `#[0, 1, 2, 3, 4].extract 2 2 = #[]` + * `#[0, 1, 2, 3, 4].extract 2 3 = #[2]` + * `#[0, 1, 2, 3, 4].extract 2 4 = #[2, 3]` +-/ -- NOTE: used in the quotation elaborator output def Array.extract (as : Array α) (start : Nat := 0) (stop : Nat := as.size) : Array α := let rec loop (i : Nat) (j : Nat) (bs : Array α) : Array α := diff --git a/src/Lean/Data/Array.lean b/src/Lean/Data/Array.lean index 7c89fab45e..584d7ea933 100644 --- a/src/Lean/Data/Array.lean +++ b/src/Lean/Data/Array.lean @@ -15,12 +15,22 @@ is part of the public, user-facing standard library. -/ /-- -Given an array `a`, runs `f xᵢ xⱼ` for all `i < j`, removes those entries for which `f` returns -`false` (and will subsequently skip pairs if one element is removed), and returns the array of -remaining elements. +Compares each element of an array with all later elements using `f`. For each comparison, `f` +determines whether to keep both of its arguments. If `f` returns `false` for an argument, that +argument is removed from the array and does not participate in subsequent comparisons. Those +elements that were not discarded are returned. -This can be used to remove elements from an array where a “better” element, in some partial -order, exists in the array. +This can be used to remove elements from an array where a “better” element, in some partial order, +exists in the array. + +Example: +```lean example +#eval #["a", "r", "red", "x", "r"].filterPairsM fun x y => + pure (!(x.isPrefixOf y), true) +``` +```output +#["a", "red", "x", "r"] +``` -/ def filterPairsM {m} [Monad m] {α} (a : Array α) (f : α → α → m (Bool × Bool)) : m (Array α) := do diff --git a/src/Std/Data/HashMap/Basic.lean b/src/Std/Data/HashMap/Basic.lean index d0e7f3742f..fb91ff187c 100644 --- a/src/Std/Data/HashMap/Basic.lean +++ b/src/Std/Data/HashMap/Basic.lean @@ -289,8 +289,16 @@ end Unverified end Std.HashMap /-- -Groups all elements `x`, `y` in `xs` with `key x == key y` into the same array -`(xs.groupByKey key).find! (key x)`. Groups preserve the relative order of elements in `xs`. +Groups the elements of an array `xs` according to the function `key`, returning a hash map in which +each group is associated with its key. Groups preserve the relative order of elements in `xs`. + +Example: +```lean example +#eval #[0, 1, 2, 3, 4, 5, 6].groupByKey (· % 2) +``` +```output +Std.HashMap.ofList [(0, #[0, 2, 4, 6]), (1, #[1, 3, 5])] +``` -/ def Array.groupByKey [BEq α] [Hashable α] (key : β → α) (xs : Array β) : Std.HashMap α (Array β) := Id.run do diff --git a/tests/lean/interactive/hover.lean.expected.out b/tests/lean/interactive/hover.lean.expected.out index 455af3b7d8..dfe5be7afd 100644 --- a/tests/lean/interactive/hover.lean.expected.out +++ b/tests/lean/interactive/hover.lean.expected.out @@ -639,7 +639,7 @@ "end": {"line": 297, "character": 29}}, "contents": {"value": - "```lean\nList.zip.{u, v} {α : Type u} {β : Type v} : List α → List β → List (α × β)\n```\n***\nCombines two lists into a list of pairs in which the first and second components are the\ncorresponding elements of each list. The resulting list is the length of the shorter of the inputs\nlists.\n\n`O(min |xs| |ys|)`.\n\nExamples:\n* `[\"Mon\", \"Tue\", \"Wed\"].zip [1, 2, 3] = [(\"Mon\", 1), (\"Tue\", 2), (\"Wed\", 3)]`\n* `[\"Mon\", \"Tue\", \"Wed\"].zip [1, 2] = [(\"Mon\", 1), (\"Tue\", 2)]`\n* `[x₁, x₂, x₃].zip [y₁, y₂, y₃, y₄] = [(x₁, y₁), (x₂, y₂), (x₃, y₃)]`\n\n***\n*import Init.Data.List.Basic*", + "```lean\nList.zip.{u, v} {α : Type u} {β : Type v} : List α → List β → List (α × β)\n```\n***\nCombines two lists into a list of pairs in which the first and second components are the\ncorresponding elements of each list. The resulting list is the length of the shorter of the input\nlists.\n\n`O(min |xs| |ys|)`.\n\nExamples:\n* `[\"Mon\", \"Tue\", \"Wed\"].zip [1, 2, 3] = [(\"Mon\", 1), (\"Tue\", 2), (\"Wed\", 3)]`\n* `[\"Mon\", \"Tue\", \"Wed\"].zip [1, 2] = [(\"Mon\", 1), (\"Tue\", 2)]`\n* `[x₁, x₂, x₃].zip [y₁, y₂, y₃, y₄] = [(x₁, y₁), (x₂, y₂), (x₃, y₃)]`\n\n***\n*import Init.Data.List.Basic*", "kind": "markdown"}} {"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 297, "character": 19}} @@ -648,5 +648,5 @@ "end": {"line": 297, "character": 22}}, "contents": {"value": - "```lean\nList.zip.{u, v} {α : Type u} {β : Type v} : List α → List β → List (α × β)\n```\n***\nCombines two lists into a list of pairs in which the first and second components are the\ncorresponding elements of each list. The resulting list is the length of the shorter of the inputs\nlists.\n\n`O(min |xs| |ys|)`.\n\nExamples:\n* `[\"Mon\", \"Tue\", \"Wed\"].zip [1, 2, 3] = [(\"Mon\", 1), (\"Tue\", 2), (\"Wed\", 3)]`\n* `[\"Mon\", \"Tue\", \"Wed\"].zip [1, 2] = [(\"Mon\", 1), (\"Tue\", 2)]`\n* `[x₁, x₂, x₃].zip [y₁, y₂, y₃, y₄] = [(x₁, y₁), (x₂, y₂), (x₃, y₃)]`\n\n***\n*import Init.Data.List.Basic*", + "```lean\nList.zip.{u, v} {α : Type u} {β : Type v} : List α → List β → List (α × β)\n```\n***\nCombines two lists into a list of pairs in which the first and second components are the\ncorresponding elements of each list. The resulting list is the length of the shorter of the input\nlists.\n\n`O(min |xs| |ys|)`.\n\nExamples:\n* `[\"Mon\", \"Tue\", \"Wed\"].zip [1, 2, 3] = [(\"Mon\", 1), (\"Tue\", 2), (\"Wed\", 3)]`\n* `[\"Mon\", \"Tue\", \"Wed\"].zip [1, 2] = [(\"Mon\", 1), (\"Tue\", 2)]`\n* `[x₁, x₂, x₃].zip [y₁, y₂, y₃, y₄] = [(x₁, y₁), (x₂, y₂), (x₃, y₃)]`\n\n***\n*import Init.Data.List.Basic*", "kind": "markdown"}}