From c59fcde1fb50b40228e3ca15b8b889a3b14f78de Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 9 Apr 2024 10:28:09 +0200 Subject: [PATCH 1/3] chore: rename fields of Subarray to follow Lean conventions --- RELEASES.md | 2 + src/Init/Data/Array/Subarray.lean | 63 ++++++++++++++++++++----------- src/Init/Data/Stream.lean | 3 +- 3 files changed, 45 insertions(+), 23 deletions(-) diff --git a/RELEASES.md b/RELEASES.md index ef21b2fce362..1308ddc1277c 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -112,6 +112,8 @@ fact.def : * The coercion from `String` to `Name` was removed. Previously, it was `Name.mkSimple`, which does not separate strings at dots, but experience showed that this is not always the desired coercion. For the previous behavior, manually insert a call to `Name.mkSimple`. +* The `Subarray` fields `as`, `h₁` and `h₂` have been renamed to `array`, `start_le_stop`, and `stop_le_array_size`, respectively. This more closely follows standard Lean conventions. Deprecated aliases for the field projects were added; these will be removed in a future release. + v4.7.0 --------- diff --git a/src/Init/Data/Array/Subarray.lean b/src/Init/Data/Array/Subarray.lean index 4ae0daf73ca9..9ad6c6dfb502 100644 --- a/src/Init/Data/Array/Subarray.lean +++ b/src/Init/Data/Array/Subarray.lean @@ -9,11 +9,20 @@ import Init.Data.Array.Basic universe u v w structure Subarray (α : Type u) where - as : Array α + array : Array α start : Nat stop : Nat - h₁ : start ≤ stop - h₂ : stop ≤ as.size + start_le_stop : start ≤ stop + stop_le_array_size : stop ≤ array.size + +@[deprecated] +def Subarray.as (s : Subarray α) : Array α := s.array + +@[deprecated] +def Subarray.h₁ (s : Subarray α) : s.start ≤ s.stop := s.start_le_stop + +@[deprecated] +def Subarray.h₂ (s : Subarray α) : s.stop ≤ s.array.size := s.stop_le_array_size namespace Subarray @@ -21,13 +30,13 @@ def size (s : Subarray α) : Nat := s.stop - s.start def get (s : Subarray α) (i : Fin s.size) : α := - have : s.start + i.val < s.as.size := by - apply Nat.lt_of_lt_of_le _ s.h₂ + have : s.start + i.val < s.array.size := by + apply Nat.lt_of_lt_of_le _ s.stop_le_array_size have := i.isLt simp [size] at this rw [Nat.add_comm] exact Nat.add_lt_of_lt_sub this - s.as[s.start + i.val] + s.array[s.start + i.val] instance : GetElem (Subarray α) Nat α fun xs i => i < xs.size where getElem xs i h := xs.get ⟨i, h⟩ @@ -42,7 +51,7 @@ abbrev get! [Inhabited α] (s : Subarray α) (i : Nat) : α := def popFront (s : Subarray α) : Subarray α := if h : s.start < s.stop then - { s with start := s.start + 1, h₁ := Nat.le_of_lt_succ (Nat.add_lt_add_right h 1) } + { s with start := s.start + 1, start_le_stop := Nat.le_of_lt_succ (Nat.add_lt_add_right h 1) } else s @@ -50,7 +59,7 @@ def popFront (s : Subarray α) : Subarray α := let sz := USize.ofNat s.stop let rec @[specialize] loop (i : USize) (b : β) : m β := do if i < sz then - let a := s.as.uget i lcProof + let a := s.array.uget i lcProof match (← f a b) with | ForInStep.done b => pure b | ForInStep.yield b => loop (i+1) b @@ -68,27 +77,27 @@ instance : ForIn m (Subarray α) α where @[inline] def foldlM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : β → α → m β) (init : β) (as : Subarray α) : m β := - as.as.foldlM f (init := init) (start := as.start) (stop := as.stop) + as.array.foldlM f (init := init) (start := as.start) (stop := as.stop) @[inline] def foldrM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → β → m β) (init : β) (as : Subarray α) : m β := - as.as.foldrM f (init := init) (start := as.stop) (stop := as.start) + as.array.foldrM f (init := init) (start := as.stop) (stop := as.start) @[inline] def anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Subarray α) : m Bool := - as.as.anyM p (start := as.start) (stop := as.stop) + as.array.anyM p (start := as.start) (stop := as.stop) @[inline] def allM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Subarray α) : m Bool := - as.as.allM p (start := as.start) (stop := as.stop) + as.array.allM p (start := as.start) (stop := as.stop) @[inline] def forM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Subarray α) : m PUnit := - as.as.forM f (start := as.start) (stop := as.stop) + as.array.forM f (start := as.start) (stop := as.stop) @[inline] def forRevM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Subarray α) : m PUnit := - as.as.forRevM f (start := as.stop) (stop := as.start) + as.array.forRevM f (start := as.stop) (stop := as.start) @[inline] def foldl {α : Type u} {β : Type v} (f : β → α → β) (init : β) (as : Subarray α) : β := @@ -135,15 +144,25 @@ variable {α : Type u} def toSubarray (as : Array α) (start : Nat := 0) (stop : Nat := as.size) : Subarray α := if h₂ : stop ≤ as.size then - if h₁ : start ≤ stop then - { as := as, start := start, stop := stop, h₁ := h₁, h₂ := h₂ } - else - { as := as, start := stop, stop := stop, h₁ := Nat.le_refl _, h₂ := h₂ } + if h₁ : start ≤ stop then + { array := as, start := start, stop := stop, + start_le_stop := h₁, stop_le_array_size := h₂ } + else + { array := as, start := stop, stop := stop, + start_le_stop := Nat.le_refl _, stop_le_array_size := h₂ } else - if h₁ : start ≤ as.size then - { as := as, start := start, stop := as.size, h₁ := h₁, h₂ := Nat.le_refl _ } - else - { as := as, start := as.size, stop := as.size, h₁ := Nat.le_refl _, h₂ := Nat.le_refl _ } + if h₁ : start ≤ as.size then + { array := as, + start := start, + stop := as.size, + start_le_stop := h₁, + stop_le_array_size := Nat.le_refl _ } + else + { array := as, + start := as.size, + stop := as.size, + start_le_stop := Nat.le_refl _, + stop_le_array_size := Nat.le_refl _ } @[coe] def ofSubarray (s : Subarray α) : Array α := Id.run do diff --git a/src/Init/Data/Stream.lean b/src/Init/Data/Stream.lean index 2eb2fb5143c7..f045327471fc 100644 --- a/src/Init/Data/Stream.lean +++ b/src/Init/Data/Stream.lean @@ -94,7 +94,8 @@ instance : Stream (Subarray α) α where next? s := if h : s.start < s.stop then have : s.start + 1 ≤ s.stop := Nat.succ_le_of_lt h - some (s.as.get ⟨s.start, Nat.lt_of_lt_of_le h s.h₂⟩, { s with start := s.start + 1, h₁ := this }) + some (s.as.get ⟨s.start, Nat.lt_of_lt_of_le h s.stop_le_array_size⟩, + { s with start := s.start + 1, start_le_stop := this }) else none From 9cdc5899d40de55daa96e7eb5248f4b5e2462325 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Wed, 10 Apr 2024 13:56:14 +0200 Subject: [PATCH 2/3] Update src/Init/Data/Array/Subarray.lean Co-authored-by: Eric Wieser --- src/Init/Data/Array/Subarray.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Init/Data/Array/Subarray.lean b/src/Init/Data/Array/Subarray.lean index 9ad6c6dfb502..b57d8eaace9f 100644 --- a/src/Init/Data/Array/Subarray.lean +++ b/src/Init/Data/Array/Subarray.lean @@ -15,14 +15,14 @@ structure Subarray (α : Type u) where start_le_stop : start ≤ stop stop_le_array_size : stop ≤ array.size -@[deprecated] -def Subarray.as (s : Subarray α) : Array α := s.array +@[deprecated Subarray.array] +abbrev Subarray.as (s : Subarray α) : Array α := s.array -@[deprecated] -def Subarray.h₁ (s : Subarray α) : s.start ≤ s.stop := s.start_le_stop +@[deprecated Subarray.start_le_stop] +theorem Subarray.h₁ (s : Subarray α) : s.start ≤ s.stop := s.start_le_stop -@[deprecated] -def Subarray.h₂ (s : Subarray α) : s.stop ≤ s.array.size := s.stop_le_array_size +@[deprecated Subarray.stop_le_array_size] +theorem Subarray.h₂ (s : Subarray α) : s.stop ≤ s.as.size := s.stop_le_array_size namespace Subarray From 3b05cd23c0dc277e94eafd2577608ec25b15f576 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 12 Apr 2024 18:02:01 +0200 Subject: [PATCH 3/3] chore: become owner of Subarray --- CODEOWNERS | 1 + 1 file changed, 1 insertion(+) diff --git a/CODEOWNERS b/CODEOWNERS index 38719d9da924..864c2200cfb1 100644 --- a/CODEOWNERS +++ b/CODEOWNERS @@ -21,3 +21,4 @@ /src/Lean/Server/ @mhuisi /src/Lean/Widget/ @Vtec234 /src/runtime/io.cpp @joehendrix +/src/Init/Data/Array/Subarray.lean @david-christiansen