From a6f0112fc5c394af7ad4325199ccf6d44aa04aed Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 24 Sep 2024 22:57:55 +1000 Subject: [PATCH] feat: refactor of Array (#5452) This is a second attempt at #5446, first reverting parts of #5403. --- src/Init/Core.lean | 5 ---- src/Init/Data/Array/Basic.lean | 3 +-- src/Init/Data/Array/BasicAux.lean | 4 +-- src/Init/Data/Array/Lemmas.lean | 25 +++++++------------ src/Init/Data/Repr.lean | 2 +- src/Init/Prelude.lean | 5 +++- src/Lean/Compiler/LCNF/Simp/ConstantFold.lean | 2 +- 7 files changed, 18 insertions(+), 28 deletions(-) diff --git a/src/Init/Core.lean b/src/Init/Core.lean index 86b8489ae6..28eda9455c 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -1382,11 +1382,6 @@ gen_injective_theorems% EStateM.Result gen_injective_theorems% Lean.Name gen_injective_theorems% Lean.Syntax -/-- Replacement for `Array.mk.injEq`; we avoid mentioning the constructor and prefer `List.toArray`. -/ -abbrev List.toArray_inj := @Array.mk.injEq - -attribute [deprecated List.toArray_inj (since := "2024-09-09")] Array.mk.injEq - theorem Nat.succ.inj {m n : Nat} : m.succ = n.succ → m = n := fun x => Nat.noConfusion x id diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index fe26d7b03d..fdcf69f9c6 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -73,8 +73,7 @@ theorem ext' {as bs : Array α} (h : as.toList = bs.toList) : as = bs := by @[simp] theorem toArrayAux_eq (as : List α) (acc : Array α) : (as.toArrayAux acc).toList = acc.toList ++ as := by induction as generalizing acc <;> simp [*, List.toArrayAux, Array.push, List.append_assoc, List.concat_eq_append] -@[simp] theorem toList_toArray (as : List α) : as.toArray.toList = as := by - simp [List.toArray, Array.mkEmpty] +@[simp] theorem toList_toArray (as : List α) : as.toArray.toList = as := rfl @[simp] theorem size_toArray (as : List α) : as.toArray.size = as.length := by simp [size] diff --git a/src/Init/Data/Array/BasicAux.lean b/src/Init/Data/Array/BasicAux.lean index d96e8c3a13..21f9cc3a2f 100644 --- a/src/Init/Data/Array/BasicAux.lean +++ b/src/Init/Data/Array/BasicAux.lean @@ -9,7 +9,7 @@ import Init.Data.Nat.Linear import Init.NotationExtra theorem Array.of_push_eq_push {as bs : Array α} (h : as.push a = bs.push b) : as = bs ∧ a = b := by - simp only [push, List.toArray_inj] at h + simp only [push, mk.injEq] at h have ⟨h₁, h₂⟩ := List.of_concat_eq_concat h cases as; cases bs simp_all @@ -34,7 +34,7 @@ private theorem List.of_toArrayAux_eq_toArrayAux {as bs : List α} {cs ds : Arra @[simp] theorem List.toArray_eq_toArray_eq (as bs : List α) : (as.toArray = bs.toArray) = (as = bs) := by apply propext; apply Iff.intro - · intro h; simp [toArray] at h; have := of_toArrayAux_eq_toArrayAux h rfl; exact this.1 + · intro h; simpa [toArray] using h · intro h; rw [h] def Array.mapM' [Monad m] (f : α → m β) (as : Array α) : m { bs : Array β // bs.size = as.size } := diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index 33a717e546..d872b7b109 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -19,11 +19,6 @@ This file contains some theorems about `Array` and `List` needed for `Init.Data. namespace Array -/-- We avoid mentioning the constructor `Array.mk` directly, preferring `List.toArray`. -/ -@[simp] theorem mk_eq_toArray (as : List α) : Array.mk as = as.toArray := by - apply ext' - simp - @[simp] theorem getElem_toList {a : Array α} {i : Nat} (h : i < a.size) : a.toList[i] = a[i] := rfl @[simp] theorem getElem_mk {xs : List α} {i : Nat} (h : i < xs.length) : (Array.mk xs)[i] = xs[i] := rfl @@ -68,14 +63,12 @@ open Array (a.toArrayAux b).size = b.size + a.length := by simp [size] -@[simp] theorem toArray_toList : (a : Array α) → a.toList.toArray = a - | ⟨l⟩ => ext' (toList_toArray l) +@[simp] theorem toArray_toList (a : Array α) : a.toList.toArray = a := rfl +@[deprecated toArray_toList (since := "2024-09-09")] +abbrev toArray_data := @toArray_toList @[simp] theorem getElem_toArray {a : List α} {i : Nat} (h : i < a.toArray.size) : - a.toArray[i] = a[i]'(by simpa using h) := by - have h₁ := mk_eq_toArray a - have h₂ := getElem_mk (by simpa using h) - simpa [h₁] using h₂ + a.toArray[i] = a[i]'(by simpa using h) := rfl @[simp] theorem toArray_concat {as : List α} {x : α} : (as ++ [x]).toArray = as.toArray.push x := by @@ -90,10 +83,10 @@ attribute [simp] uset @[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl -@[deprecated List.toArray_toList (since := "2024-09-09")] -abbrev toArray_data := @List.toArray_toList -@[deprecated List.toArray_toList (since := "2024-09-09")] -abbrev toArray_toList := @List.toArray_toList +@[simp] theorem toArray_toList (a : Array α) : a.toList.toArray = a := rfl + +@[deprecated toArray_toList (since := "2024-09-09")] +abbrev toArray_data := @toArray_toList @[simp] theorem toList_length {l : Array α} : l.toList.length = l.size := rfl @@ -647,7 +640,7 @@ theorem foldr_induction simp only [mem_def, map_toList, List.mem_map] theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) : - arr.mapM f = return (← arr.toList.mapM f).toArray := by + arr.mapM f = return mk (← arr.toList.mapM f) := by rw [mapM_eq_foldlM, foldlM_eq_foldlM_toList, ← List.foldrM_reverse] conv => rhs; rw [← List.reverse_reverse arr.toList] induction arr.toList.reverse with diff --git a/src/Init/Data/Repr.lean b/src/Init/Data/Repr.lean index 7c44ea5d6a..c1f7e522df 100644 --- a/src/Init/Data/Repr.lean +++ b/src/Init/Data/Repr.lean @@ -163,7 +163,7 @@ protected def _root_.USize.repr (n : @& USize) : String := /-- We statically allocate and memoize reprs for small natural numbers. -/ private def reprArray : Array String := Id.run do - List.range 128 |>.map (·.toUSize.repr) |> List.toArray + List.range 128 |>.map (·.toUSize.repr) |> Array.mk private def reprFast (n : Nat) : String := if h : n < 128 then Nat.reprArray.get ⟨n, h⟩ else diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 450271309d..739db00cf4 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -2584,6 +2584,9 @@ structure Array (α : Type u) where attribute [extern "lean_array_to_list"] Array.toList attribute [extern "lean_array_mk"] Array.mk +@[inherit_doc Array.mk, match_pattern] +abbrev List.toArray (xs : List α) : Array α := .mk xs + /-- Construct a new empty array with initial capacity `c`. -/ @[extern "lean_mk_empty_array_with_capacity"] def Array.mkEmpty {α : Type u} (c : @& Nat) : Array α where @@ -2730,7 +2733,7 @@ def List.redLength : List α → Nat -- This function is exported to C, where it is called by `Array.mk` -- (the constructor) to implement this functionality. @[inline, match_pattern, pp_nodot, export lean_list_to_array] -def List.toArray (as : List α) : Array α := +def List.toArrayImpl (as : List α) : Array α := as.toArrayAux (Array.mkEmpty as.redLength) /-- The typeclass which supplies the `>>=` "bind" function. See `Monad`. -/ diff --git a/src/Lean/Compiler/LCNF/Simp/ConstantFold.lean b/src/Lean/Compiler/LCNF/Simp/ConstantFold.lean index 9266a07017..b950aec8ba 100644 --- a/src/Lean/Compiler/LCNF/Simp/ConstantFold.lean +++ b/src/Lean/Compiler/LCNF/Simp/ConstantFold.lean @@ -180,7 +180,7 @@ let _x.26 := @Array.push _ _x.24 z def foldArrayLiteral : Folder := fun args => do let #[_, .fvar fvarId] := args | return none let some (list, typ, level) ← getPseudoListLiteral fvarId | return none - let arr := list.toArray + let arr := Array.mk list let lit ← mkPseudoArrayLiteral arr typ level return some lit