feat: rename Array.mkArray to replicate
diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 69d50d1..7d673c5 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean
@@ -161,7 +161,10 @@ | ⟨[]⟩ => rfl | ⟨a::as⟩ => simp [pop, Nat.succ_sub_succ_eq_sub, size] -@[extern "lean_mk_array"] +def replicate {α : Type u} (n : Nat) (v : α) : Array α where + toList := List.replicate n v + +@[extern "lean_mk_array", deprecated replicate (since := "2025-01-16")] def mkArray {α : Type u} (n : Nat) (v : α) : Array α where toList := List.replicate n v
diff --git a/src/Init/Data/Array/Find.lean b/src/Init/Data/Array/Find.lean index 4838ad6..fe8bd88 100644 --- a/src/Init/Data/Array/Find.lean +++ b/src/Init/Data/Array/Find.lean
@@ -98,21 +98,26 @@ cases L using array₂_induction simp [List.getLast?_flatten, ← List.map_reverse, List.findSome?_map, Function.comp_def] -theorem findSome?_mkArray : findSome? f (mkArray n a) = if n = 0 then none else f a := by +theorem findSome?_replicate : findSome? f (replicate n a) = if n = 0 then none else f a := by simp [← List.toArray_replicate, List.findSome?_replicate] -@[simp] theorem findSome?_mkArray_of_pos (h : 0 < n) : findSome? f (mkArray n a) = f a := by - simp [findSome?_mkArray, Nat.ne_of_gt h] +@[simp] theorem findSome?_replicate_of_pos (h : 0 < n) : findSome? f (replicate n a) = f a := by + simp [findSome?_replicate, Nat.ne_of_gt h] -- Argument is unused, but used to decide whether `simp` should unfold. -@[simp] theorem findSome?_mkArray_of_isSome (_ : (f a).isSome) : - findSome? f (mkArray n a) = if n = 0 then none else f a := by - simp [findSome?_mkArray] +@[simp] theorem findSome?_replicate_of_isSome (_ : (f a).isSome) : + findSome? f (replicate n a) = if n = 0 then none else f a := by + simp [findSome?_replicate] -@[simp] theorem findSome?_mkArray_of_isNone (h : (f a).isNone) : - findSome? f (mkArray n a) = none := by +@[simp] theorem findSome?_replicate_of_isNone (h : (f a).isNone) : + findSome? f (replicate n a) = none := by rw [Option.isNone_iff_eq_none] at h - simp [findSome?_mkArray, h] + simp [findSome?_replicate, h] + +@[deprecated findSome?_replicate (since := "2025-01-16")] abbrev findSome?_mkArray := @findSome?_replicate +@[deprecated findSome?_replicate_of_pos (since := "2025-01-16")] abbrev findSome?_mkArray_of_pos := @findSome?_replicate_of_pos +@[deprecated findSome?_replicate_of_isSome (since := "2025-01-16")] abbrev findSome?_mkArray_of_isSome := @findSome?_replicate_of_isSome +@[deprecated findSome?_replicate_of_isNone (since := "2025-01-16")] abbrev findSome?_mkArray_of_isNone := @findSome?_replicate_of_isNone /-! ### find? -/ @@ -244,34 +249,42 @@ (xs.flatMap f).find? p = none ↔ ∀ x ∈ xs, ∀ y ∈ f x, !p y := by simp -theorem find?_mkArray : - find? p (mkArray n a) = if n = 0 then none else if p a then some a else none := by +theorem find?_replicate : + find? p (replicate n a) = if n = 0 then none else if p a then some a else none := by simp [← List.toArray_replicate, List.find?_replicate] -@[simp] theorem find?_mkArray_of_length_pos (h : 0 < n) : - find? p (mkArray n a) = if p a then some a else none := by - simp [find?_mkArray, Nat.ne_of_gt h] +@[simp] theorem find?_replicate_of_length_pos (h : 0 < n) : + find? p (replicate n a) = if p a then some a else none := by + simp [find?_replicate, Nat.ne_of_gt h] -@[simp] theorem find?_mkArray_of_pos (h : p a) : - find? p (mkArray n a) = if n = 0 then none else some a := by - simp [find?_mkArray, h] +@[simp] theorem find?_replicate_of_pos (h : p a) : + find? p (replicate n a) = if n = 0 then none else some a := by + simp [find?_replicate, h] -@[simp] theorem find?_mkArray_of_neg (h : ¬ p a) : find? p (mkArray n a) = none := by - simp [find?_mkArray, h] +@[simp] theorem find?_replicate_of_neg (h : ¬ p a) : find? p (replicate n a) = none := by + simp [find?_replicate, h] -- This isn't a `@[simp]` lemma since there is already a lemma for `l.find? p = none` for any `l`. -theorem find?_mkArray_eq_none {n : Nat} {a : α} {p : α → Bool} : - (mkArray n a).find? p = none ↔ n = 0 ∨ !p a := by +theorem find?_replicate_eq_none {n : Nat} {a : α} {p : α → Bool} : + (replicate n a).find? p = none ↔ n = 0 ∨ !p a := by simp [← List.toArray_replicate, List.find?_replicate_eq_none, Classical.or_iff_not_imp_left] -@[simp] theorem find?_mkArray_eq_some {n : Nat} {a b : α} {p : α → Bool} : - (mkArray n a).find? p = some b ↔ n ≠ 0 ∧ p a ∧ a = b := by +@[simp] theorem find?_replicate_eq_some {n : Nat} {a b : α} {p : α → Bool} : + (replicate n a).find? p = some b ↔ n ≠ 0 ∧ p a ∧ a = b := by simp [← List.toArray_replicate] -@[simp] theorem get_find?_mkArray (n : Nat) (a : α) (p : α → Bool) (h) : - ((mkArray n a).find? p).get h = a := by +@[simp] theorem get_find?_replicate (n : Nat) (a : α) (p : α → Bool) (h) : + ((replicate n a).find? p).get h = a := by simp [← List.toArray_replicate] +@[deprecated find?_replicate (since := "2025-01-16")] abbrev find?_mkArray := @find?_replicate +@[deprecated find?_replicate_of_length_pos (since := "2025-01-16")] abbrev find?_mkArray_of_length_pos := @find?_replicate_of_length_pos +@[deprecated find?_replicate_of_pos (since := "2025-01-16")] abbrev find?_mkArray_of_pos := @find?_replicate_of_pos +@[deprecated find?_replicate_of_neg (since := "2025-01-16")] abbrev find?_mkArray_of_neg := @find?_replicate_of_neg +@[deprecated find?_replicate_eq_none (since := "2025-01-16")] abbrev find?_mkArray_eq_none := @find?_replicate_eq_none +@[deprecated find?_replicate_eq_some (since := "2025-01-16")] abbrev find?_mkArray_eq_some := @find?_replicate_eq_some +@[deprecated get_find?_mkArray (since := "2025-01-16")] abbrev get_find?_mkArray := @get_find?_replicate + theorem find?_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : Array α) (H : ∀ (a : α), a ∈ xs → P a) (p : β → Bool) : (xs.pmap f H).find? p = (xs.attach.find? (fun ⟨a, m⟩ => p (f a (H a m)))).map fun ⟨a, m⟩ => f a (H a m) := by
diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index b78fe30..8418794 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean
@@ -160,31 +160,38 @@ theorem singleton_inj : #[a] = #[b] ↔ a = b := by simp -/-! ### mkArray -/ +/-! ### replicate -/ -@[simp] theorem size_mkArray (n : Nat) (v : α) : (mkArray n v).size = n := +@[simp] theorem size_replicate (n : Nat) (v : α) : (replicate n v).size = n := List.length_replicate .. -@[simp] theorem toList_mkArray : (mkArray n a).toList = List.replicate n a := by - simp only [mkArray] +@[simp] theorem toList_replicate : (replicate n a).toList = List.replicate n a := by + simp only [replicate] -@[simp] theorem mkArray_zero : mkArray 0 a = #[] := rfl +@[simp] theorem replicate_zero : replicate 0 a = #[] := rfl -theorem mkArray_succ : mkArray (n + 1) a = (mkArray n a).push a := by +theorem replicate_succ : replicate (n + 1) a = (replicate n a).push a := by apply toList_inj.1 simp [List.replicate_succ'] -theorem mkArray_inj : mkArray n a = mkArray m b ↔ n = m ∧ (n = 0 ∨ a = b) := by +theorem replicate_inj : replicate n a = replicate m b ↔ n = m ∧ (n = 0 ∨ a = b) := by rw [← List.replicate_inj, ← toList_inj] simp -@[simp] theorem getElem_mkArray (n : Nat) (v : α) (h : i < (mkArray n v).size) : - (mkArray n v)[i] = v := by simp [← getElem_toList] +@[simp] theorem getElem_replicate (n : Nat) (v : α) (h : i < (replicate n v).size) : + (replicate n v)[i] = v := by simp [← getElem_toList] -theorem getElem?_mkArray (n : Nat) (v : α) (i : Nat) : - (mkArray n v)[i]? = if i < n then some v else none := by +theorem getElem?_replicate (n : Nat) (v : α) (i : Nat) : + (replicate n v)[i]? = if i < n then some v else none := by simp [getElem?_def] +@[deprecated size_replicate (since := "2025-01-16")] abbrev size_mkArray := @size_replicate +@[deprecated replicate_zero (since := "2025-01-16")] abbrev replicate_mkArray_zero := @replicate_zero +@[deprecated replicate_succ (since := "2025-01-16")] abbrev replicate_mkArray_succ := @replicate_succ +@[deprecated replicate_inj (since := "2025-01-16")] abbrev replicate_mkArray_inj := @replicate_inj +@[deprecated getElem_replicate (since := "2025-01-16")] abbrev getElem_mkArray := @getElem_replicate +@[deprecated getElem?_replicate (since := "2025-01-16")] abbrev getElem?_mkArray := @getElem?_replicate + /-! ## L[i] and L[i]? -/ @[simp] theorem getElem?_eq_none_iff {a : Array α} : a[i]? = none ↔ a.size ≤ i := by @@ -962,15 +969,17 @@ cases ys simp [List.length_eq_of_beq (by simpa using h)] -@[simp] theorem mkArray_beq_mkArray [BEq α] {a b : α} {n : Nat} : - (mkArray n a == mkArray n b) = (n == 0 || a == b) := by +@[simp] theorem replicate_beq_replicate [BEq α] {a b : α} {n : Nat} : + (replicate n a == replicate n b) = (n == 0 || a == b) := by cases n with | zero => simp | succ n => - rw [mkArray_succ, mkArray_succ, push_beq_push, mkArray_beq_mkArray] + rw [replicate_succ, replicate_succ, push_beq_push, replicate_beq_replicate] rw [Bool.eq_iff_iff] simp +contextual +@[deprecated replicate_beq_replicate (since := "2025-01-16")] abbrev mkArray_beq_mkArray := @replicate_beq_replicate + private theorem beq_of_beq_singleton [BEq α] {a b : α} : #[a] == #[b] → a == b := by intro h have : isEqv #[a] #[b] BEq.beq = true := h @@ -3182,42 +3191,48 @@ cases as simp [Array.sum, List.sum] -/-! ### mkArray -/ +/-! ### replicate -/ -theorem eq_mkArray_of_mem {a : α} {l : Array α} (h : ∀ (b) (_ : b ∈ l), b = a) : l = mkArray l.size a := by +theorem eq_replicate_of_mem {a : α} {l : Array α} (h : ∀ (b) (_ : b ∈ l), b = a) : l = replicate l.size a := by rcases l with ⟨l⟩ have := List.eq_replicate_of_mem (by simpa using h) rw [this] simp -theorem eq_mkArray_iff {a : α} {n} {l : Array α} : - l = mkArray n a ↔ l.size = n ∧ ∀ (b) (_ : b ∈ l), b = a := by +theorem eq_replicate_iff {a : α} {n} {l : Array α} : + l = replicate n a ↔ l.size = n ∧ ∀ (b) (_ : b ∈ l), b = a := by rcases l with ⟨l⟩ simp [← List.eq_replicate_iff, toArray_eq] -theorem map_eq_mkArray_iff {l : Array α} {f : α → β} {b : β} : - l.map f = mkArray l.size b ↔ ∀ x ∈ l, f x = b := by - simp [eq_mkArray_iff] +theorem map_eq_replicate_iff {l : Array α} {f : α → β} {b : β} : + l.map f = replicate l.size b ↔ ∀ x ∈ l, f x = b := by + simp [eq_replicate_iff] -@[simp] theorem mem_mkArray (a : α) (n : Nat) : b ∈ mkArray n a ↔ n ≠ 0 ∧ b = a := by - rw [mkArray, mem_toArray] +@[simp] theorem mem_replicate (a : α) (n : Nat) : b ∈ replicate n a ↔ n ≠ 0 ∧ b = a := by + rw [replicate, mem_toArray] simp -@[simp] theorem map_const (l : Array α) (b : β) : map (Function.const α b) l = mkArray l.size b := - map_eq_mkArray_iff.mpr fun _ _ => rfl +@[simp] theorem map_const (l : Array α) (b : β) : map (Function.const α b) l = replicate l.size b := + map_eq_replicate_iff.mpr fun _ _ => rfl -@[simp] theorem map_const_fun (x : β) : map (Function.const α x) = (mkArray ·.size x) := by +@[simp] theorem map_const_fun (x : β) : map (Function.const α x) = (replicate ·.size x) := by funext l simp /-- Variant of `map_const` using a lambda rather than `Function.const`. -/ -- This can not be a `@[simp]` lemma because it would fire on every `Array.map`. -theorem map_const' (l : Array α) (b : β) : map (fun _ => b) l = mkArray l.size b := +theorem map_const' (l : Array α) (b : β) : map (fun _ => b) l = replicate l.size b := map_const l b -@[simp] theorem sum_mkArray_nat (n : Nat) (a : Nat) : (mkArray n a).sum = n * a := by +@[simp] theorem sum_replicate_nat (n : Nat) (a : Nat) : (replicate n a).sum = n * a := by simp [sum_eq_sum_toList, List.sum_replicate_nat] +@[deprecated eq_replicate_of_mem (since := "2025-01-16")] abbrev eq_mkArray_of_mem := @eq_replicate_of_mem +@[deprecated eq_replicate_iff (since := "2025-01-16")] abbrev eq_mkArray_iff := @eq_replicate_iff +@[deprecated map_eq_replicate_iff (since := "2025-01-16")] abbrev map_eq_mkArray_iff := @map_eq_replicate_iff +@[deprecated mem_replicate (since := "2025-01-16")] abbrev mem_mkArray := @mem_replicate +@[deprecated sum_replicate_nat (since := "2025-01-16")] abbrev sum_mkArray_nat := @sum_replicate_nat + /-! ### reverse -/ @[simp] theorem mem_reverse {x : α} {as : Array α} : x ∈ as.reverse ↔ x ∈ as := by
diff --git a/src/Init/Data/List/ToArray.lean b/src/Init/Data/List/ToArray.lean index d76cc01..736bd13 100644 --- a/src/Init/Data/List/ToArray.lean +++ b/src/Init/Data/List/ToArray.lean
@@ -392,7 +392,7 @@ · simp · simp_all [List.set_eq_of_length_le] -@[simp] theorem toArray_replicate (n : Nat) (v : α) : (List.replicate n v).toArray = mkArray n v := rfl +@[simp] theorem toArray_replicate (n : Nat) (v : α) : (List.replicate n v).toArray = Array.replicate n v := rfl @[deprecated toArray_replicate (since := "2024-12-13")] abbrev _root_.Array.mkArray_eq_toArray_replicate := @toArray_replicate
diff --git a/src/Init/Data/Vector/Basic.lean b/src/Init/Data/Vector/Basic.lean index 32b336c..662abad 100644 --- a/src/Init/Data/Vector/Basic.lean +++ b/src/Init/Data/Vector/Basic.lean
@@ -52,13 +52,15 @@ @[inline] def mkEmpty (capacity : Nat) : Vector α 0 := ⟨.mkEmpty capacity, rfl⟩ /-- Makes a vector of size `n` with all cells containing `v`. -/ -@[inline] def mkVector (n) (v : α) : Vector α n := ⟨mkArray n v, by simp⟩ +@[inline] def replicate (n) (v : α) : Vector α n := ⟨Array.replicate n v, by simp⟩ + +@[deprecated replicate (since := "2025-01-16")] abbrev mkVector := @replicate /-- Returns a vector of size `1` with element `v`. -/ @[inline] def singleton (v : α) : Vector α 1 := ⟨#[v], rfl⟩ instance [Inhabited α] : Inhabited (Vector α n) where - default := mkVector n default + default := replicate n default /-- Get an element of a vector using a `Fin` index. -/ @[inline] def get (v : Vector α n) (i : Fin n) : α :=
diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean index 17964a6..bb73b49 100644 --- a/src/Init/Data/Vector/Lemmas.lean +++ b/src/Init/Data/Vector/Lemmas.lean
@@ -269,7 +269,9 @@ cases v simp -@[simp] theorem toArray_mkVector : (mkVector n a).toArray = mkArray n a := rfl +@[simp] theorem toArray_replicate : (replicate n a).toArray = Array.replicate n a := rfl + +@[deprecated toArray_replicate (since := "2025-01-16")] abbrev toArray_mkVector := @toArray_replicate @[simp] theorem toArray_inj {v w : Vector α n} : v.toArray = w.toArray ↔ v = w := by cases v @@ -389,7 +391,9 @@ cases v simp -@[simp] theorem toList_mkVector : (mkVector n a).toList = List.replicate n a := rfl +@[simp] theorem toList_replicate : (replicate n a).toList = List.replicate n a := rfl + +@[deprecated toList_replicate (since := "2025-01-16")] abbrev toList_mkVector := @toList_replicate theorem toList_inj {v w : Vector α n} : v.toList = w.toList ↔ v = w := by cases v @@ -468,15 +472,19 @@ theorem singleton_inj : #v[a] = #v[b] ↔ a = b := by simp -/-! ### mkVector -/ +/-! ### replicate -/ -@[simp] theorem mkVector_zero : mkVector 0 a = #v[] := rfl +@[simp] theorem replicate_zero : replicate 0 a = #v[] := rfl -theorem mkVector_succ : mkVector (n + 1) a = (mkVector n a).push a := by - simp [mkVector, Array.mkArray_succ] +theorem replicate_succ : replicate (n + 1) a = (replicate n a).push a := by + simp [replicate, Array.replicate_succ] -theorem mkVector_inj : mkVector n a = mkVector n b ↔ n = 0 ∨ a = b := by - simp [← toArray_inj, toArray_mkVector, Array.mkArray_inj] +theorem replicate_inj : replicate n a = replicate n b ↔ n = 0 ∨ a = b := by + simp [← toArray_inj, toArray_replicate, Array.replicate_inj] + +@[deprecated replicate_zero (since := "2025-01-16")] abbrev mkVector_zero := @replicate_zero +@[deprecated replicate_succ (since := "2025-01-16")] abbrev mkVector_succ := @replicate_succ +@[deprecated replicate_inj (since := "2025-01-16")] abbrev mkVector_inj := @replicate_inj /-! ## L[i] and L[i]? -/ @@ -1005,15 +1013,17 @@ cases w simp -@[simp] theorem mkVector_beq_mkVector [BEq α] {a b : α} {n : Nat} : - (mkVector n a == mkVector n b) = (n == 0 || a == b) := by +@[simp] theorem replicate_beq_replicate [BEq α] {a b : α} {n : Nat} : + (replicate n a == replicate n b) = (n == 0 || a == b) := by cases n with | zero => simp | succ n => - rw [mkVector_succ, mkVector_succ, push_beq_push, mkVector_beq_mkVector] + rw [replicate_succ, replicate_succ, push_beq_push, replicate_beq_replicate] rw [Bool.eq_iff_iff] simp +contextual +@[deprecated replicate_beq_replicate (since := "2025-01-16")] abbrev mkVector_beq_mkVector := @replicate_beq_replicate + @[simp] theorem reflBEq_iff [BEq α] [NeZero n] : ReflBEq (Vector α n) ↔ ReflBEq α := by match n, NeZero.ne n with | n + 1, _ => @@ -1021,8 +1031,8 @@ · intro h constructor intro a - suffices (mkVector (n + 1) a == mkVector (n + 1) a) = true by - rw [mkVector_succ, push_beq_push, Bool.and_eq_true] at this + suffices (replicate (n + 1) a == replicate (n + 1) a) = true by + rw [replicate_succ, push_beq_push, Bool.and_eq_true] at this exact this.2 simp · intro h @@ -1037,15 +1047,15 @@ · intro h constructor · intro a b h - have := mkVector_inj (n := n+1) (a := a) (b := b) + have := replicate_inj (n := n+1) (a := a) (b := b) simp only [Nat.add_one_ne_zero, false_or] at this rw [← this] apply eq_of_beq - rw [mkVector_beq_mkVector] + rw [replicate_beq_replicate] simpa · intro a - suffices (mkVector (n + 1) a == mkVector (n + 1) a) = true by - rw [mkVector_beq_mkVector] at this + suffices (replicate (n + 1) a == replicate (n + 1) a) = true by + rw [replicate_beq_replicate] at this simpa simp · intro h @@ -1131,8 +1141,8 @@ constructor · intro h ext a - replace h := congrFun h (mkVector n a) - simp only [mkVector, map_mk, mk.injEq, Array.map_inj_left, Array.mem_mkArray, and_imp, + replace h := congrFun h (replicate n a) + simp only [replicate, map_mk, mk.injEq, Array.map_inj_left, Array.mem_replicate, and_imp, forall_eq_apply_imp_iff] at h exact h (NeZero.ne n) · intro h; subst h; rfl
diff --git a/src/Lean/Compiler/IR/ExpandResetReuse.lean b/src/Lean/Compiler/IR/ExpandResetReuse.lean index 04dc752..0d8e771 100644 --- a/src/Lean/Compiler/IR/ExpandResetReuse.lean +++ b/src/Lean/Compiler/IR/ExpandResetReuse.lean
@@ -85,7 +85,7 @@ /-- Try to erase `inc` instructions on projections of `y` occurring in the tail of `bs`. Return the updated `bs` and a bit mask specifying which `inc`s have been removed. -/ def eraseProjIncFor (n : Nat) (y : VarId) (bs : Array FnBody) : Array FnBody × Mask := - eraseProjIncForAux y bs (mkArray n none) #[] + eraseProjIncForAux y bs (Array.replicate n none) #[] /-- Replace `reuse x ctor ...` with `ctor ...`, and remove `dec x` -/ partial def reuseToCtor (x : VarId) : FnBody → FnBody
diff --git a/src/Lean/Compiler/LCNF/FixedParams.lean b/src/Lean/Compiler/LCNF/FixedParams.lean index 5d216c2..490e1dc 100644 --- a/src/Lean/Compiler/LCNF/FixedParams.lean +++ b/src/Lean/Compiler/LCNF/FixedParams.lean
@@ -169,7 +169,7 @@ for decl in decls do let values := mkInitialValues decl.params.size let assignment := mkAssignment decl values - let fixed := Array.mkArray decl.params.size true + let fixed := Array.replicate decl.params.size true match decl.value with | .code c => match evalCode c |>.run { main := decl, decls, assignment } |>.run { fixed } with
diff --git a/src/Lean/Compiler/LCNF/Simp/DiscrM.lean b/src/Lean/Compiler/LCNF/Simp/DiscrM.lean index d6cb3f2..615b43e 100644 --- a/src/Lean/Compiler/LCNF/Simp/DiscrM.lean +++ b/src/Lean/Compiler/LCNF/Simp/DiscrM.lean
@@ -98,7 +98,7 @@ return { ctx with discrCtorMap := ctx.discrCtorMap.insert discr ctorInfo, ctorDiscrMap := ctx.ctorDiscrMap.insert ctor.toExpr discr } else -- For the discrCtor map, the constructor parameters are irrelevant for optimizations that use this information - let ctorInfo := .ctor ctorVal (mkArray ctorVal.numParams Arg.erased ++ fieldArgs) + let ctorInfo := .ctor ctorVal (Array.replicate ctorVal.numParams Arg.erased ++ fieldArgs) return { ctx with discrCtorMap := ctx.discrCtorMap.insert discr ctorInfo } @[inline, inherit_doc withDiscrCtorImp] def withDiscrCtor [MonadFunctorT DiscrM m] (discr : FVarId) (ctorName : Name) (ctorFields : Array Param) : m α → m α :=
diff --git a/src/Lean/Compiler/LCNF/SpecInfo.lean b/src/Lean/Compiler/LCNF/SpecInfo.lean index 0e7f2ce..ea512d7 100644 --- a/src/Lean/Compiler/LCNF/SpecInfo.lean +++ b/src/Lean/Compiler/LCNF/SpecInfo.lean
@@ -147,7 +147,7 @@ let mut declsInfo := #[] for decl in decls do if hasNospecializeAttribute (← getEnv) decl.name then - declsInfo := declsInfo.push (mkArray decl.params.size .other) + declsInfo := declsInfo.push (Array.replicate decl.params.size .other) else let specArgs? := getSpecializationArgs? (← getEnv) decl.name let contains (i : Nat) : Bool := specArgs?.getD #[] |>.contains i
diff --git a/src/Lean/Data/Array.lean b/src/Lean/Data/Array.lean index 7c89fab..7501d38 100644 --- a/src/Lean/Data/Array.lean +++ b/src/Lean/Data/Array.lean
@@ -24,7 +24,7 @@ -/ def filterPairsM {m} [Monad m] {α} (a : Array α) (f : α → α → m (Bool × Bool)) : m (Array α) := do - let mut removed := Array.mkArray a.size false + let mut removed := Array.replicate a.size false let mut numRemoved := 0 for h1 : i in [:a.size] do for h2 : j in [i+1:a.size] do unless removed[i]! || removed[j]! do
diff --git a/src/Lean/Data/FuzzyMatching.lean b/src/Lean/Data/FuzzyMatching.lean index 1ee2cd7..3f7614d 100644 --- a/src/Lean/Data/FuzzyMatching.lean +++ b/src/Lean/Data/FuzzyMatching.lean
@@ -99,11 +99,11 @@ between the substrings pattern[:i+1] and word[:j+1] assuming that pattern[i] misses at word[j] (k = 0, i.e. it was matched earlier), or matches at word[j] (k = 1). A value of `none` corresponds to a score of -∞, and is used where no such match/miss is possible or for unneeded parts of the table. -/ - let mut result : Array (Option Int) := Array.mkArray (pattern.length * word.length * 2) none - let mut runLengths : Array Int := Array.mkArray (pattern.length * word.length) 0 + let mut result : Array (Option Int) := Array.replicate (pattern.length * word.length * 2) none + let mut runLengths : Array Int := Array.replicate (pattern.length * word.length) 0 -- penalty for starting a consecutive run at each index - let mut startPenalties : Array Int := Array.mkArray word.length 0 + let mut startPenalties : Array Int := Array.replicate word.length 0 let mut lastSepIdx := 0 let mut penaltyNs : Int := 0 @@ -124,8 +124,8 @@ `word.length - pattern.length` at each index (because at the very end, we can only consider fuzzy matches of `pattern` with a longer substring of `word`). -/ for wordIdx in [patternIdx:word.length-(pattern.length - patternIdx - 1)] do - let missScore? := - if wordIdx >= 1 then + let missScore? := + if wordIdx >= 1 then selectBest (getMiss result patternIdx (wordIdx - 1)) (getMatch result patternIdx (wordIdx - 1)) @@ -134,7 +134,7 @@ let mut matchScore? := none if allowMatch (pattern.get ⟨patternIdx⟩) (word.get ⟨wordIdx⟩) (patternRoles.get! patternIdx) (wordRoles.get! wordIdx) then - if patternIdx >= 1 then + if patternIdx >= 1 then let runLength := runLengths.get! (getIdx (patternIdx - 1) (wordIdx - 1)) + 1 runLengths := runLengths.set! (getIdx patternIdx wordIdx) runLength @@ -213,7 +213,7 @@ /- Consecutive character match. -/ if let some bonus := consecutive then /- consecutive run bonus -/ - score := score + bonus + score := score + bonus return score /-- Match the given pattern with the given word using a fuzzy matching
diff --git a/src/Lean/Data/HashMap.lean b/src/Lean/Data/HashMap.lean index c373939..51fcc93 100644 --- a/src/Lean/Data/HashMap.lean +++ b/src/Lean/Data/HashMap.lean
@@ -32,7 +32,7 @@ def mkHashMapImp {α : Type u} {β : Type v} (capacity := 8) : HashMapImp α β := { size := 0 buckets := - ⟨mkArray (numBucketsForCapacity capacity).nextPowerOfTwo AssocList.nil, + ⟨Array.replicate (numBucketsForCapacity capacity).nextPowerOfTwo AssocList.nil, by simp; apply Nat.isPowerOfTwo_nextPowerOfTwo⟩ } namespace HashMapImp @@ -101,7 +101,7 @@ def expand [Hashable α] (size : Nat) (buckets : HashMapBucket α β) : HashMapImp α β := let bucketsNew : HashMapBucket α β := ⟨ - mkArray (buckets.val.size * 2) AssocList.nil, + Array.replicate (buckets.val.size * 2) AssocList.nil, by simp; apply Nat.mul2_isPowerOfTwo_of_isPowerOfTwo buckets.property ⟩ { size := size,
diff --git a/src/Lean/Data/HashSet.lean b/src/Lean/Data/HashSet.lean index e85d3db..1aaae76 100644 --- a/src/Lean/Data/HashSet.lean +++ b/src/Lean/Data/HashSet.lean
@@ -28,7 +28,7 @@ def mkHashSetImp {α : Type u} (capacity := 8) : HashSetImp α := { size := 0 buckets := - ⟨mkArray ((capacity * 4) / 3).nextPowerOfTwo [], + ⟨Array.replicate ((capacity * 4) / 3).nextPowerOfTwo [], by simp; apply Nat.isPowerOfTwo_nextPowerOfTwo⟩ } namespace HashSetImp @@ -92,7 +92,7 @@ def expand [Hashable α] (size : Nat) (buckets : HashSetBucket α) : HashSetImp α := let bucketsNew : HashSetBucket α := ⟨ - mkArray (buckets.val.size * 2) [], + Array.replicate (buckets.val.size * 2) [], by simp; apply Nat.mul2_isPowerOfTwo_of_isPowerOfTwo buckets.property ⟩ { size := size,
diff --git a/src/Lean/Data/PersistentHashMap.lean b/src/Lean/Data/PersistentHashMap.lean index 0308005..4803a73 100644 --- a/src/Lean/Data/PersistentHashMap.lean +++ b/src/Lean/Data/PersistentHashMap.lean
@@ -39,7 +39,7 @@ abbrev maxCollisions : Nat := 4 def mkEmptyEntriesArray {α β} : Array (Entry α β (Node α β)) := - (Array.mkArray PersistentHashMap.branching.toNat PersistentHashMap.Entry.null) + (Array.replicate PersistentHashMap.branching.toNat PersistentHashMap.Entry.null) end PersistentHashMap
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 7c28ced..4fe33e8 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean
@@ -735,7 +735,7 @@ let extDescrs ← persistentEnvExtensionsRef.get /- For extensions starting at `startingAt`, ensure their `importedEntries` array have size `mods.size`. -/ for extDescr in extDescrs[startingAt:] do - env := extDescr.toEnvExtension.modifyState env fun s => { s with importedEntries := mkArray mods.size #[] } + env := extDescr.toEnvExtension.modifyState env fun s => { s with importedEntries := Array.replicate mods.size #[] } /- For each module `mod`, and `mod.entries`, if the extension name is one of the extensions after `startingAt`, set `entries` -/ let extNameIdx ← mkExtNameMap startingAt for h : modIdx in [:mods.size] do
diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index f60754e..74ede5c 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean
@@ -1127,7 +1127,7 @@ @[inline] def getAppArgs (e : Expr) : Array Expr := let dummy := mkSort levelZero let nargs := e.getAppNumArgs - getAppArgsAux e (mkArray nargs dummy) (nargs-1) + getAppArgsAux e (Array.replicate nargs dummy) (nargs-1) private def getBoundedAppArgsAux : Expr → Array Expr → Nat → Array Expr | app f a, as, i + 1 => getBoundedAppArgsAux f (as.set! i a) i @@ -1142,7 +1142,7 @@ @[inline] def getBoundedAppArgs (maxArgs : Nat) (e : Expr) : Array Expr := let dummy := mkSort levelZero let nargs := min maxArgs e.getAppNumArgs - getBoundedAppArgsAux e (mkArray nargs dummy) nargs + getBoundedAppArgsAux e (Array.replicate nargs dummy) nargs private def getAppRevArgsAux : Expr → Array Expr → Array Expr | app f a, as => getAppRevArgsAux f (as.push a) @@ -1160,7 +1160,7 @@ @[inline] def withApp (e : Expr) (k : Expr → Array Expr → α) : α := let dummy := mkSort levelZero let nargs := e.getAppNumArgs - withAppAux k e (mkArray nargs dummy) (nargs-1) + withAppAux k e (Array.replicate nargs dummy) (nargs-1) /-- Return the function (name) and arguments of an application. -/ def getAppFnArgs (e : Expr) : Name × Array Expr := @@ -1173,7 +1173,7 @@ -/ @[inline] def getAppArgsN (e : Expr) (n : Nat) : Array Expr := let dummy := mkSort levelZero - loop n e (mkArray n dummy) + loop n e (Array.replicate n dummy) where loop : Nat → Expr → Array Expr → Array Expr | 0, _, as => as
diff --git a/src/Lean/Meta/SizeOf.lean b/src/Lean/Meta/SizeOf.lean index 367d5a5..54e4736 100644 --- a/src/Lean/Meta/SizeOf.lean +++ b/src/Lean/Meta/SizeOf.lean
@@ -196,7 +196,7 @@ let lemmaInfo ← getConstInfo lemmaName let lemmaArity ← forallTelescopeReducing lemmaInfo.type fun xs _ => return xs.size let lemmaArgMask := ctorParams.toArray.map some - let lemmaArgMask := lemmaArgMask ++ mkArray (lemmaArity - ctorInfo.numParams - ctorInfo.numFields) (none (α := Expr)) + let lemmaArgMask := lemmaArgMask ++ Array.replicate (lemmaArity - ctorInfo.numParams - ctorInfo.numFields) (none (α := Expr)) let lemmaArgMask := lemmaArgMask ++ ctorFields.toArray.map some mkAppOptM lemmaName lemmaArgMask
diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean index 0a2aed6..812f591 100644 --- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean +++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
@@ -419,10 +419,10 @@ || (getPPAnalyzeTrustSubtypeMk (← getOptions) && (← getExpr).isAppOfArity ``Subtype.mk 4) analyzeAppStagedCore { f, fType, args, mvars, bInfos, forceRegularApp } |>.run' { - bottomUps := mkArray args.size false, - higherOrders := mkArray args.size false, - provideds := mkArray args.size false, - funBinders := mkArray args.size false + bottomUps := Array.replicate args.size false, + higherOrders := Array.replicate args.size false, + provideds := Array.replicate args.size false, + funBinders := Array.replicate args.size false } if !rest.isEmpty then
diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean index ffd3691..77a6509 100644 --- a/src/Lean/Syntax.lean +++ b/src/Lean/Syntax.lean
@@ -495,7 +495,7 @@ stx def mkAntiquotNode (kind : Name) (term : Syntax) (nesting := 0) (name : Option String := none) (isPseudoKind := false) : Syntax := - let nesting := mkNullNode (mkArray nesting (mkAtom "$")) + let nesting := mkNullNode (Array.replicate nesting (mkAtom "$")) let term := if term.isIdent then term else if term.isOfKind `Lean.Parser.Term.hole then term[0] @@ -558,7 +558,7 @@ stx[1] def mkAntiquotSpliceNode (kind : SyntaxNodeKind) (contents : Array Syntax) (suffix : String) (nesting := 0) : Syntax := - let nesting := mkNullNode (mkArray nesting (mkAtom "$")) + let nesting := mkNullNode (Array.replicate nesting (mkAtom "$")) mkNode (kind ++ `antiquot_splice) #[mkAtom "$", nesting, mkAtom "[", mkNullNode contents, mkAtom "]", mkAtom suffix] -- `$x,*` etc.
diff --git a/src/Lean/Util/ForEachExprWhere.lean b/src/Lean/Util/ForEachExprWhere.lean index 6208d40..f95919f 100644 --- a/src/Lean/Util/ForEachExprWhere.lean +++ b/src/Lean/Util/ForEachExprWhere.lean
@@ -31,7 +31,7 @@ checked : Std.HashSet Expr unsafe def initCache : State := { - visited := mkArray cacheSize.toNat (cast lcProof ()) + visited := Array.replicate cacheSize.toNat (cast lcProof ()) checked := {} }
diff --git a/src/Lean/Util/ReplaceLevel.lean b/src/Lean/Util/ReplaceLevel.lean index 11d5881..02f2201 100644 --- a/src/Lean/Util/ReplaceLevel.lean +++ b/src/Lean/Util/ReplaceLevel.lean
@@ -56,8 +56,8 @@ visit e unsafe def initCache : State := - { keys := mkArray cacheSize.toNat (cast lcProof ()), -- `()` is not a valid `Expr` - results := mkArray cacheSize.toNat default } + { keys := Array.replicate cacheSize.toNat (cast lcProof ()), -- `()` is not a valid `Expr` + results := Array.replicate cacheSize.toNat default } unsafe def replaceUnsafe (f? : Level → Option Level) (e : Expr) : Expr := (replaceUnsafeM f? cacheSize e).run' initCache
diff --git a/src/Std/Data/DHashMap/Internal/Defs.lean b/src/Std/Data/DHashMap/Internal/Defs.lean index aaafacb..bc30712 100644 --- a/src/Std/Data/DHashMap/Internal/Defs.lean +++ b/src/Std/Data/DHashMap/Internal/Defs.lean
@@ -170,7 +170,7 @@ /-- Internal implementation detail of the hash map -/ @[inline] def empty (capacity := 8) : Raw₀ α β := - ⟨⟨0, mkArray (numBucketsForCapacity capacity).nextPowerOfTwo AssocList.nil⟩, + ⟨⟨0, Array.replicate (numBucketsForCapacity capacity).nextPowerOfTwo AssocList.nil⟩, by simpa using Nat.pos_of_isPowerOfTwo (Nat.isPowerOfTwo_nextPowerOfTwo _)⟩ -- Take `hash` as a function instead of `Hashable α` as per @@ -187,7 +187,7 @@ { d : Array (AssocList α β) // 0 < d.size } := let ⟨data, hd⟩ := data let nbuckets := data.size * 2 - go 0 data ⟨mkArray nbuckets AssocList.nil, by simpa [nbuckets] using Nat.mul_pos hd Nat.two_pos⟩ + go 0 data ⟨Array.replicate nbuckets AssocList.nil, by simpa [nbuckets] using Nat.mul_pos hd Nat.two_pos⟩ where /-- Inner loop of `expand`. Copies elements `source[i:]` into `target`, destroying `source` in the process. -/
diff --git a/src/Std/Data/DHashMap/Internal/Model.lean b/src/Std/Data/DHashMap/Internal/Model.lean index 4020b4a..19e9f1a 100644 --- a/src/Std/Data/DHashMap/Internal/Model.lean +++ b/src/Std/Data/DHashMap/Internal/Model.lean
@@ -219,8 +219,8 @@ namespace IsHashSelf @[simp] -theorem mkArray [BEq α] [Hashable α] {c : Nat} : IsHashSelf - (mkArray c (AssocList.nil : AssocList α β)) := +theorem replicate [BEq α] [Hashable α] {c : Nat} : IsHashSelf + (Array.replicate c (AssocList.nil : AssocList α β)) := ⟨by simp⟩ theorem uset [BEq α] [Hashable α] {m : Array (AssocList α β)} {i : USize} {h : i.toNat < m.size}
diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean index d441e5b..71a9c6f 100644 --- a/src/Std/Data/DHashMap/Internal/WF.lean +++ b/src/Std/Data/DHashMap/Internal/WF.lean
@@ -29,8 +29,8 @@ namespace Std.DHashMap.Internal @[simp] -theorem toListModel_mkArray_nil {c} : - toListModel (mkArray c (AssocList.nil : AssocList α β)) = [] := by +theorem toListModel_replicate_nil {c} : + toListModel (Array.replicate c (AssocList.nil : AssocList α β)) = [] := by suffices ∀ d, (List.replicate d AssocList.nil).flatMap AssocList.toList = [] from this _ intro d induction d <;> simp_all [List.replicate] @@ -143,7 +143,7 @@ @[simp] theorem toListModel_buckets_empty {c} : toListModel (empty c : Raw₀ α β).1.buckets = [] := - toListModel_mkArray_nil + toListModel_replicate_nil theorem wfImp_empty [BEq α] [Hashable α] {c} : Raw.WFImp (empty c : Raw₀ α β).1 where buckets_hash_self := by simp [Raw.empty, Raw₀.empty] @@ -229,7 +229,7 @@ {buckets : {d : Array (AssocList α β) // 0 < d.size}} : Perm (toListModel (expand buckets).1) (toListModel buckets.1) := by simpa [expand, expand.go_eq] using toListModel_foldl_reinsertAux (toListModel buckets.1) - ⟨mkArray (buckets.1.size * 2) .nil, by simpa using Nat.mul_pos buckets.2 Nat.two_pos⟩ + ⟨Array.replicate (buckets.1.size * 2) .nil, by simpa using Nat.mul_pos buckets.2 Nat.two_pos⟩ theorem toListModel_expandIfNecessary [BEq α] [Hashable α] [PartialEquivBEq α] (m : Raw₀ α β) : Perm (toListModel (expandIfNecessary m).1.2) (toListModel m.1.2) := by
diff --git a/src/Std/Sat/AIG/CNF.lean b/src/Std/Sat/AIG/CNF.lean index b43ced3..0dbf3d7 100644 --- a/src/Std/Sat/AIG/CNF.lean +++ b/src/Std/Sat/AIG/CNF.lean
@@ -162,7 +162,7 @@ /-- The `Cache` invariant always holds for an empty CNF when all nodes are unmarked. -/ -theorem Cache.Inv_init : Inv ([] : CNF (CNFVar aig)) (mkArray aig.decls.size false) (by simp) where +theorem Cache.Inv_init : Inv ([] : CNF (CNFVar aig)) (Array.replicate aig.decls.size false) (by simp) where hmark := by intro lhs rhs linv rinv idx hbound hmarked heq simp at hmarked @@ -254,7 +254,7 @@ A cache with no entries is valid for an empty CNF. -/ def Cache.init (aig : AIG Nat) : Cache aig [] where - marks := mkArray aig.decls.size false + marks := Array.replicate aig.decls.size false hmarks := by simp inv := Inv_init
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.lean index 108fc71..fddfb06 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.lean
@@ -67,7 +67,7 @@ namespace DefaultFormula instance {n : Nat} : Inhabited (DefaultFormula n) where - default := ⟨#[], #[], #[], Array.mkArray n unassigned⟩ + default := ⟨#[], #[], #[], Array.replicate n unassigned⟩ /-- Note: This function is only for reasoning about semantics. Its efficiency doesn't actually matter -/ def toList {n : Nat} (f : DefaultFormula n) : List (DefaultClause n) := @@ -88,7 +88,7 @@ field invariant described in the DefaultFormula doc comment. -/ def ofArray {n : Nat} (clauses : Array (Option (DefaultClause n))) : DefaultFormula n := - let assignments := clauses.foldl ofArray_fold_fn (Array.mkArray n unassigned) + let assignments := clauses.foldl ofArray_fold_fn (Array.replicate n unassigned) ⟨clauses, #[], #[], assignments⟩ def insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) : DefaultFormula n :=
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean index 41d343c..a9daad3 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
@@ -20,6 +20,7 @@ open Std.Sat open DefaultClause DefaultFormula Assignment +open Array (replicate) /-- This invariant states that if the `assignments` field of a default formula `f` indicates that `f` @@ -107,17 +108,17 @@ · simp only [ofArray] · have hsize : (ofArray arr).assignments.size = n := by simp only [ofArray, ← Array.foldl_toList] - have hb : (mkArray n unassigned).size = n := by simp only [Array.size_mkArray] + have hb : (replicate n unassigned).size = n := by simp only [Array.size_replicate] have hl (acc : Array Assignment) (ih : acc.size = n) (cOpt : Option (DefaultClause n)) (_cOpt_in_arr : cOpt ∈ arr.toList) : (ofArray_fold_fn acc cOpt).size = n := by rw [size_ofArray_fold_fn acc cOpt, ih] - exact List.foldlRecOn arr.toList ofArray_fold_fn (mkArray n unassigned) hb hl + exact List.foldlRecOn arr.toList ofArray_fold_fn (replicate n unassigned) hb hl apply Exists.intro hsize let ModifiedAssignmentsInvariant (assignments : Array Assignment) : Prop := ∃ hsize : assignments.size = n, ∀ i : PosFin n, ∀ b : Bool, hasAssignment b (assignments[i.1]'(by rw [hsize]; exact i.2.2)) → (unit (i, b)) ∈ toList (ofArray arr) - have hb : ModifiedAssignmentsInvariant (mkArray n unassigned) := by - have hsize : (mkArray n unassigned).size = n := by simp only [Array.size_mkArray] + have hb : ModifiedAssignmentsInvariant (replicate n unassigned) := by + have hsize : (replicate n unassigned).size = n := by simp only [Array.size_replicate] apply Exists.intro hsize intro i b h by_cases hb : b <;> simp [hasAssignment, hb, hasPosAssignment, hasNegAssignment] at h @@ -185,7 +186,7 @@ · next i_ne_l => simp only [Array.getElem_modify_of_ne (Ne.symm i_ne_l)] at h exact ih i b h - rcases List.foldlRecOn arr.toList ofArray_fold_fn (mkArray n unassigned) hb hl with ⟨_h_size, h'⟩ + rcases List.foldlRecOn arr.toList ofArray_fold_fn (replicate n unassigned) hb hl with ⟨_h_size, h'⟩ intro i b h simp only [ofArray, ← Array.foldl_toList] at h exact h' i b h