chore: use UTF8 instead of Utf8 in identifiers (#10636)

This PR renames `String.getUtf8Byte` to `String.getUTF8Byte` in order to
adhere to the standard library naming convention.

Author: TwoFX

src/Init/Data/String/Basic.lean

@@ -982,7 +982,7 @@ end ByteArray.utf8DecodeChar?
 
 open ByteArray.utf8DecodeChar?
 
-/- # `utf8DecodeChar?` and `validateUtf8At` -/
+/- # `utf8DecodeChar?` and `validateUTF8At` -/
 
 @[inline, expose]
 public def ByteArray.utf8DecodeChar? (bytes : ByteArray) (i : Nat) : Option Char :=
@@ -1006,7 +1006,7 @@ public def ByteArray.utf8DecodeChar? (bytes : ByteArray) (i : Nat) : Option Char
   else none
 
 @[inline, expose]
-public def ByteArray.validateUtf8At (bytes : ByteArray) (i : Nat) : Bool :=
+public def ByteArray.validateUTF8At (bytes : ByteArray) (i : Nat) : Bool :=
   if h₀ : i < bytes.size then
     match h : parseFirstByte bytes[i] with
     | .invalid => false
@@ -1212,9 +1212,9 @@ public theorem String.toByteArray_utf8EncodeChar_of_utf8DecodeChar?_eq_some {b :
     rw [← assemble₄_eq_some_iff_utf8EncodeChar_eq]
     exact ⟨this, h⟩
 
-public theorem ByteArray.validateUtf8At_eq_isSome_utf8DecodeChar? {b : ByteArray} {i : Nat} :
-    b.validateUtf8At i = (b.utf8DecodeChar? i).isSome := by
-  simp only [validateUtf8At, utf8DecodeChar?]
+public theorem ByteArray.validateUTF8At_eq_isSome_utf8DecodeChar? {b : ByteArray} {i : Nat} :
+    b.validateUTF8At i = (b.utf8DecodeChar? i).isSome := by
+  simp only [validateUTF8At, utf8DecodeChar?]
   split
   · split <;> (try split) <;> simp [verify₁_eq_isSome_assemble₁, verify₂_eq_isSome_assemble₂,
       verify₃_eq_isSome_assemble₃, verify₄_eq_isSome_assemble₄]
@@ -1285,9 +1285,9 @@ public theorem ByteArray.lt_size_of_isSome_utf8DecodeChar? {b : ByteArray} {i :
   have := c.utf8Size_pos
   omega
 
-public theorem ByteArray.lt_size_of_validateUtf8At {b : ByteArray} {i : Nat} :
-    validateUtf8At b i = true → i < b.size :=
-  validateUtf8At_eq_isSome_utf8DecodeChar? ▸ lt_size_of_isSome_utf8DecodeChar?
+public theorem ByteArray.lt_size_of_validateUTF8At {b : ByteArray} {i : Nat} :
+    validateUTF8At b i = true → i < b.size :=
+  validateUTF8At_eq_isSome_utf8DecodeChar? ▸ lt_size_of_isSome_utf8DecodeChar?
 
 public theorem ByteArray.utf8DecodeChar?_append_eq_some {b : ByteArray} {i : Nat} {c : Char} (h : utf8DecodeChar? b i = some c)
     (b' : ByteArray) : utf8DecodeChar? (b ++ b') i = some c := by
@@ -1366,7 +1366,7 @@ public theorem List.utf8DecodeChar_utf8Encode_cons {l : List Char} {c : Char} {h
     ByteArray.utf8DecodeChar (c::l).utf8Encode 0 h = c := by
   simp [ByteArray.utf8DecodeChar]
 
-/-! # `UInt8.IsUtf8FirstByte` -/
+/-! # `UInt8.IsUTF8FirstByte` -/
 
 namespace UInt8
 
@@ -1375,27 +1375,27 @@ Predicate for whether a byte can appear as the first byte of the UTF-8 encoding
 scalar value.
 -/
 @[expose]
-public def IsUtf8FirstByte (c : UInt8) : Prop :=
+public def IsUTF8FirstByte (c : UInt8) : Prop :=
   c &&& 0x80 = 0 ∨ c &&& 0xe0 = 0xc0 ∨ c &&& 0xf0 = 0xe0 ∨ c &&& 0xf8 = 0xf0
 
-public instance {c : UInt8} : Decidable c.IsUtf8FirstByte :=
+public instance {c : UInt8} : Decidable c.IsUTF8FirstByte :=
   inferInstanceAs <| Decidable (c &&& 0x80 = 0 ∨ c &&& 0xe0 = 0xc0 ∨ c &&& 0xf0 = 0xe0 ∨ c &&& 0xf8 = 0xf0)
 
-theorem isUtf8FirstByte_iff_parseFirstByte_ne_invalid {c : UInt8} :
-    c.IsUtf8FirstByte ↔ parseFirstByte c ≠ FirstByte.invalid := by
-  fun_cases parseFirstByte with simp_all [IsUtf8FirstByte]
+theorem isUTF8FirstByte_iff_parseFirstByte_ne_invalid {c : UInt8} :
+    c.IsUTF8FirstByte ↔ parseFirstByte c ≠ FirstByte.invalid := by
+  fun_cases parseFirstByte with simp_all [IsUTF8FirstByte]
 
 @[simp]
-public theorem isUtf8FirstByte_getElem_utf8EncodeChar {c : Char} {i : Nat} {hi : i < (String.utf8EncodeChar c).length} :
-    (String.utf8EncodeChar c)[i].IsUtf8FirstByte ↔ i = 0 := by
+public theorem isUTF8FirstByte_getElem_utf8EncodeChar {c : Char} {i : Nat} {hi : i < (String.utf8EncodeChar c).length} :
+    (String.utf8EncodeChar c)[i].IsUTF8FirstByte ↔ i = 0 := by
   obtain (rfl|hi₀) := Nat.eq_zero_or_pos i
-  · simp only [isUtf8FirstByte_iff_parseFirstByte_ne_invalid, iff_true]
+  · simp only [isUTF8FirstByte_iff_parseFirstByte_ne_invalid, iff_true]
     match h : c.utf8Size, c.utf8Size_pos, c.utf8Size_le_four with
     | 1, _, _ => simp [parseFirstByte_utf8EncodeChar_eq_done h]
     | 2, _, _ => simp [parseFirstByte_utf8EncodeChar_eq_oneMore h]
     | 3, _, _ => simp [parseFirstByte_utf8EncodeChar_eq_twoMore h]
     | 4, _, _ => simp [parseFirstByte_utf8EncodeChar_eq_threeMore h]
-  · simp only [isUtf8FirstByte_iff_parseFirstByte_ne_invalid, ne_eq, Nat.ne_of_lt' hi₀, iff_false,
+  · simp only [isUTF8FirstByte_iff_parseFirstByte_ne_invalid, ne_eq, Nat.ne_of_lt' hi₀, iff_false,
       Classical.not_not]
     apply parseFirstByte_eq_invalid_of_isInvalidContinuationByte_eq_false
     simp only [String.length_utf8EncodeChar] at hi
@@ -1408,12 +1408,12 @@ public theorem isUtf8FirstByte_getElem_utf8EncodeChar {c : Char} {i : Nat} {hi :
     | 4, _, _, 2, _, _ => simp [isInvalidContinuationByte_getElem_utf8EncodeChar_two_of_utf8Size_eq_four h]
     | 4, _, _, 3, _, _ => simp [isInvalidContinuationByte_getElem_utf8EncodeChar_three_of_utf8Size_eq_four h]
 
-public theorem isUtf8FirstByte_getElem_zero_utf8EncodeChar {c : Char} :
-    ((String.utf8EncodeChar c)[0]'(by simp [c.utf8Size_pos])).IsUtf8FirstByte := by
+public theorem isUTF8FirstByte_getElem_zero_utf8EncodeChar {c : Char} :
+    ((String.utf8EncodeChar c)[0]'(by simp [c.utf8Size_pos])).IsUTF8FirstByte := by
   simp
 
 @[expose]
-public def utf8ByteSize (c : UInt8) (_h : c.IsUtf8FirstByte) : String.Pos.Raw :=
+public def utf8ByteSize (c : UInt8) (_h : c.IsUTF8FirstByte) : String.Pos.Raw :=
   if c &&& 0x80 = 0 then
     ⟨1⟩
   else if c &&& 0xe0 = 0xc0 then
@@ -1430,7 +1430,7 @@ def _root_.ByteArray.utf8DecodeChar?.FirstByte.utf8ByteSize : FirstByte → Stri
   | .twoMore => ⟨3⟩
   | .threeMore => ⟨4⟩
 
-theorem utf8ByteSize_eq_utf8ByteSize_parseFirstByte {c : UInt8} {h : c.IsUtf8FirstByte} :
+theorem utf8ByteSize_eq_utf8ByteSize_parseFirstByte {c : UInt8} {h : c.IsUTF8FirstByte} :
     c.utf8ByteSize h = (parseFirstByte c).utf8ByteSize := by
   simp only [utf8ByteSize, FirstByte.utf8ByteSize, parseFirstByte, beq_iff_eq]
   split
@@ -1447,28 +1447,28 @@ theorem utf8ByteSize_eq_utf8ByteSize_parseFirstByte {c : UInt8} {h : c.IsUtf8Fir
 
 end UInt8
 
-public theorem ByteArray.isUtf8FirstByte_getElem_zero_utf8EncodeChar_append {c : Char} {b : ByteArray} :
-    (((String.utf8EncodeChar c).toByteArray ++ b)[0]'(by simp; have := c.utf8Size_pos; omega)).IsUtf8FirstByte := by
+public theorem ByteArray.isUTF8FirstByte_getElem_zero_utf8EncodeChar_append {c : Char} {b : ByteArray} :
+    (((String.utf8EncodeChar c).toByteArray ++ b)[0]'(by simp; have := c.utf8Size_pos; omega)).IsUTF8FirstByte := by
   rw [ByteArray.getElem_append_left (by simp [c.utf8Size_pos]),
-    List.getElem_toByteArray, UInt8.isUtf8FirstByte_getElem_utf8EncodeChar]
+    List.getElem_toByteArray, UInt8.isUTF8FirstByte_getElem_utf8EncodeChar]
 
-public theorem ByteArray.isUtf8FirstByte_of_isSome_utf8DecodeChar? {b : ByteArray} {i : Nat}
-    (h : (utf8DecodeChar? b i).isSome) : (b[i]'(lt_size_of_isSome_utf8DecodeChar? h)).IsUtf8FirstByte := by
+public theorem ByteArray.isUTF8FirstByte_of_isSome_utf8DecodeChar? {b : ByteArray} {i : Nat}
+    (h : (utf8DecodeChar? b i).isSome) : (b[i]'(lt_size_of_isSome_utf8DecodeChar? h)).IsUTF8FirstByte := by
   rw [utf8DecodeChar?_eq_utf8DecodeChar?_extract] at h
-  suffices ((b.extract i b.size)[0]'(lt_size_of_isSome_utf8DecodeChar? h)).IsUtf8FirstByte by
+  suffices ((b.extract i b.size)[0]'(lt_size_of_isSome_utf8DecodeChar? h)).IsUTF8FirstByte by
     simpa [ByteArray.getElem_extract, Nat.add_zero] using this
   obtain ⟨c, hc⟩ := Option.isSome_iff_exists.1 h
   conv => congr; congr; rw [eq_of_utf8DecodeChar?_eq_some hc]
-  exact isUtf8FirstByte_getElem_zero_utf8EncodeChar_append
+  exact isUTF8FirstByte_getElem_zero_utf8EncodeChar_append
 
-public theorem ByteArray.isUtf8FirstByte_of_validateUtf8At  {b : ByteArray} {i : Nat} :
-    (h : validateUtf8At b i = true) → (b[i]'(lt_size_of_validateUtf8At h)).IsUtf8FirstByte := by
-  simp only [validateUtf8At_eq_isSome_utf8DecodeChar?]
-  exact isUtf8FirstByte_of_isSome_utf8DecodeChar?
+public theorem ByteArray.isUTF8FirstByte_of_validateUTF8At  {b : ByteArray} {i : Nat} :
+    (h : validateUTF8At b i = true) → (b[i]'(lt_size_of_validateUTF8At h)).IsUTF8FirstByte := by
+  simp only [validateUTF8At_eq_isSome_utf8DecodeChar?]
+  exact isUTF8FirstByte_of_isSome_utf8DecodeChar?
 
 theorem Char.byteIdx_utf8ByteSize_getElem_utf8EncodeChar {c : Char} :
     (((String.utf8EncodeChar c)[0]'(by simp [c.utf8Size_pos])).utf8ByteSize
-      UInt8.isUtf8FirstByte_getElem_zero_utf8EncodeChar).byteIdx = c.utf8Size := by
+      UInt8.isUTF8FirstByte_getElem_zero_utf8EncodeChar).byteIdx = c.utf8Size := by
   rw [UInt8.utf8ByteSize_eq_utf8ByteSize_parseFirstByte]
   obtain (hc|hc|hc|hc) := c.utf8Size_eq
   · rw [parseFirstByte_utf8EncodeChar_eq_done hc, FirstByte.utf8ByteSize, hc]
@@ -1478,7 +1478,7 @@ theorem Char.byteIdx_utf8ByteSize_getElem_utf8EncodeChar {c : Char} :
 
 public theorem ByteArray.utf8Size_utf8DecodeChar {b : ByteArray} {i} {h} :
     (utf8DecodeChar b i h).utf8Size =
-      ((b[i]'(lt_size_of_isSome_utf8DecodeChar? h)).utf8ByteSize (isUtf8FirstByte_of_isSome_utf8DecodeChar? h)).byteIdx := by
+      ((b[i]'(lt_size_of_isSome_utf8DecodeChar? h)).utf8ByteSize (isUTF8FirstByte_of_isSome_utf8DecodeChar? h)).byteIdx := by
   rw [← Char.byteIdx_utf8ByteSize_getElem_utf8EncodeChar]
   simp only [List.getElem_eq_getElem_toByteArray, utf8EncodeChar_utf8DecodeChar]
   simp [ByteArray.getElem_extract]

src/Init/Data/String/Decode.lean

@@ -88,7 +88,7 @@ where
       have hr := by
         simp [Pos.Raw.le_iff] at h h2 ⊢
         omega
-      if lhs.getUtf8Byte (lstart + curr) hl == rhs.getUtf8Byte (rstart + curr) hr then
+      if lhs.getUTF8Byte (lstart + curr) hl == rhs.getUTF8Byte (rstart + curr) hr then
         go curr.inc
       else
         false

src/Init/Data/String/Pattern/Basic.lean

@@ -39,16 +39,16 @@ partial def buildTable (pat : Slice) : Array String.Pos.Raw :=
 where
   go (pos : String.Pos.Raw) (table : Array String.Pos.Raw) :=
     if h : pos < pat.utf8ByteSize then
-      let patByte := pat.getUtf8Byte pos h
+      let patByte := pat.getUTF8Byte pos h
       let distance := computeDistance table[table.size - 1]! patByte table
-      let distance := if patByte = pat.getUtf8Byte! distance then distance.inc else distance
+      let distance := if patByte = pat.getUTF8Byte! distance then distance.inc else distance
       go pos.inc (table.push distance)
     else
       table
 
   computeDistance (distance : String.Pos.Raw) (patByte : UInt8) (table : Array String.Pos.Raw) :
       String.Pos.Raw :=
-    if distance > 0 && patByte != pat.getUtf8Byte! distance then
+    if distance > 0 && patByte != pat.getUTF8Byte! distance then
       computeDistance table[distance.byteIdx - 1]! patByte table
     else
       distance
@@ -62,7 +62,7 @@ def iter (s : Slice) (pat : Slice) : Std.Iter (α := ForwardSliceSearcher s) (Se
 
 partial def backtrackIfNecessary (pat : Slice) (table : Array String.Pos.Raw) (stackByte : UInt8)
     (needlePos : String.Pos.Raw) : String.Pos.Raw :=
-  if needlePos != 0 && stackByte != pat.getUtf8Byte! needlePos then
+  if needlePos != 0 && stackByte != pat.getUTF8Byte! needlePos then
     backtrackIfNecessary pat table stackByte table[needlePos.byteIdx - 1]!
   else
     needlePos
@@ -95,9 +95,9 @@ instance (s : Slice) : Std.Iterators.Iterator (ForwardSliceSearcher s) Id (Searc
       let rec findNext (startPos : String.Pos.Raw)
           (currStackPos : String.Pos.Raw) (needlePos : String.Pos.Raw) (h : stackPos ≤ currStackPos) :=
         if h1 : currStackPos < s.utf8ByteSize then
-          let stackByte := s.getUtf8Byte currStackPos h1
+          let stackByte := s.getUTF8Byte currStackPos h1
           let needlePos := backtrackIfNecessary needle table stackByte needlePos
-          let patByte := needle.getUtf8Byte! needlePos
+          let patByte := needle.getUTF8Byte! needlePos
           if stackByte != patByte then
             let nextStackPos := s.findNextPos currStackPos h1 |>.offset
             let res := .rejected (s.pos! startPos) (s.pos! nextStackPos)

src/Init/Data/String/Pattern/String.lean

@@ -688,8 +688,8 @@ def eqIgnoreAsciiCase (s1 s2 : Slice) : Bool :=
 where
   go (s1 : Slice) (s1Curr : String.Pos.Raw) (s2 : Slice) (s2Curr : String.Pos.Raw) : Bool :=
     if h : s1Curr < s1.utf8ByteSize ∧ s2Curr < s2.utf8ByteSize then
-      let c1 := (s1.getUtf8Byte s1Curr h.left).toAsciiLower
-      let c2 := (s2.getUtf8Byte s2Curr h.right).toAsciiLower
+      let c1 := (s1.getUTF8Byte s1Curr h.left).toAsciiLower
+      let c2 := (s2.getUTF8Byte s2Curr h.right).toAsciiLower
       if c1 == c2 then
         go s1 s1Curr.inc s2 s2Curr.inc
       else
@@ -900,12 +900,12 @@ instance [Pure m] : Std.Iterators.Iterator ByteIterator m UInt8 where
       ∃ h1 : it.internalState.offset < it.internalState.s.utf8ByteSize,
         it.internalState.s = it'.internalState.s ∧
         it'.internalState.offset = it.internalState.offset.inc ∧
-        it.internalState.s.getUtf8Byte it.internalState.offset h1 = out
+        it.internalState.s.getUTF8Byte it.internalState.offset h1 = out
     | .skip _ => False
     | .done => ¬ it.internalState.offset < it.internalState.s.utf8ByteSize
   step := fun ⟨s, offset⟩ =>
     if h : offset < s.utf8ByteSize then
-      pure ⟨.yield ⟨s, offset.inc⟩ (s.getUtf8Byte offset h), by simp [h]⟩
+      pure ⟨.yield ⟨s, offset.inc⟩ (s.getUTF8Byte offset h), by simp [h]⟩
     else
       pure ⟨.done, by simp [h]⟩
 
@@ -981,7 +981,7 @@ instance [Pure m] : Std.Iterators.Iterator RevByteIterator m UInt8 where
         it.internalState.s = it'.internalState.s ∧
         it.internalState.offset ≠ 0 ∧
         it'.internalState.offset = it.internalState.offset.dec ∧
-        it.internalState.s.getUtf8Byte it.internalState.offset.dec h1 = out
+        it.internalState.s.getUTF8Byte it.internalState.offset.dec h1 = out
     | .skip _ => False
     | .done => it.internalState.offset = 0
   step := fun ⟨s, offset, hinv⟩ =>
@@ -994,7 +994,7 @@ instance [Pure m] : Std.Iterators.Iterator RevByteIterator m UInt8 where
         simp [String.Pos.Raw.le_iff, nextOffset] at hinv ⊢
         omega
       have hiter := by simp [nextOffset, hbound, h]
-      pure ⟨.yield ⟨s, nextOffset, hinv⟩ (s.getUtf8Byte nextOffset hbound), hiter⟩
+      pure ⟨.yield ⟨s, nextOffset, hinv⟩ (s.getUTF8Byte nextOffset hbound), hiter⟩
     else
       pure ⟨.done, by simpa using h⟩
 

src/Init/Data/String/Slice.lean

@@ -26,14 +26,14 @@ namespace Lean.Name
 -- If you change this, also change the corresponding function in `Init.Meta`.
 private partial def needsNoEscapeAsciiRest (s : String) (i : Nat) : Bool :=
   if h : i < s.utf8ByteSize then
-    let c := s.getUtf8Byte ⟨i⟩ h
+    let c := s.getUTF8Byte ⟨i⟩ h
     isIdRestAscii c && needsNoEscapeAsciiRest s (i + 1)
   else
     true
 
 -- If you change this, also change the corresponding function in `Init.Meta`.
 @[inline] private def needsNoEscapeAscii (s : String) (h : s.utf8ByteSize > 0) : Bool :=
-  let c := s.getUtf8Byte 0 h
+  let c := s.getUTF8Byte 0 h
   isIdFirstAscii c && needsNoEscapeAsciiRest s 1
 
 -- If you change this, also change the corresponding function in `Init.Meta`.

src/Init/Data/ToString/Name.lean

@@ -156,12 +156,6 @@ def isInaccessibleUserName : Name → Bool
   | Name.num p _   => isInaccessibleUserName p
   | _              => false
 
--- FIXME: `getUtf8Byte` is in `Init.Data.String.Extra`, which causes an import cycle with
--- `Init.Meta`. Moving `getUtf8Byte` up to `Init.Data.String.Basic` creates another import cycle.
--- Please replace this definition with `getUtf8Byte` when the string refactor is through.
-@[extern "lean_string_get_byte_fast"]
-private opaque getUtf8Byte' (s : @& String) (n : Nat) (h : n < s.utf8ByteSize) : UInt8
-
 section ToString
 
 /-!
@@ -177,14 +171,14 @@ inner-loop function like `Name.toString`.
 -- If you change this, also change the corresponding function in `Init.Data.ToString.Name`.
 private partial def needsNoEscapeAsciiRest (s : String) (i : Nat) : Bool :=
   if h : i < s.utf8ByteSize then
-    let c := getUtf8Byte' s i h
+    let c := String.Internal.getUTF8Byte s i h
     isIdRestAscii c && needsNoEscapeAsciiRest s (i + 1)
   else
     true
 
 -- If you change this, also change the corresponding function in `Init.Data.ToString.Name`.
 @[inline] private def needsNoEscapeAscii (s : String) (h : s.utf8ByteSize > 0) : Bool :=
-  let c := getUtf8Byte' s 0 h
+  let c := String.Internal.getUTF8Byte s 0 h
   isIdFirstAscii c && needsNoEscapeAsciiRest s 1
 
 -- If you change this, also change the corresponding function in `Init.Data.ToString.Name`.

src/Init/Meta/Defs.lean

@@ -3378,7 +3378,7 @@ def List.utf8Encode (l : List Char) : ByteArray :=
 Note that in order for this definition to be well-behaved it is necessary to know that this `m`
 is unique. To show this, one defines UTF-8 decoding and shows that encoding and decoding are
 mutually inverse. -/
-inductive ByteArray.IsValidUtf8 (b : ByteArray) : Prop
+inductive ByteArray.IsValidUTF8 (b : ByteArray) : Prop
   /-- Show that a byte -/
   | intro (m : List Char) (hm : Eq b (List.utf8Encode m))
 
@@ -3393,10 +3393,10 @@ modifications when the reference to the string is unique.
 structure String where ofByteArray ::
   /-- The bytes of the UTF-8 encoding of the string. Since strings have a special representation in
   the runtime, this function actually takes linear time and space at runtime. For efficient access
-  to the string's bytes, use `String.utf8ByteSize` and `String.getUtf8Byte`. -/
+  to the string's bytes, use `String.utf8ByteSize` and `String.getUTF8Byte`. -/
   bytes : ByteArray
   /-- The bytes of the string form valid UTF-8. -/
-  isValidUtf8 : ByteArray.IsValidUtf8 bytes
+  isValidUTF8 : ByteArray.IsValidUTF8 bytes
 
 attribute [extern "lean_string_to_utf8"] String.bytes
 attribute [extern "lean_string_from_utf8_unchecked"] String.ofByteArray

src/Init/Prelude.lean

@@ -64,7 +64,7 @@ private def needEscape (s : String) : Bool :=
 where
   go (s : String) (i : Nat) : Bool :=
     if h : i < s.utf8ByteSize then
-      let byte := s.getUtf8Byte ⟨i⟩ h
+      let byte := s.getUTF8Byte ⟨i⟩ h
       have h1 : byte.toNat < 256 := UInt8.toNat_lt_size byte
       have h2 : escapeTable.val.size = 256 := escapeTable.property
       if escapeTable.val.get byte.toNat (Nat.lt_of_lt_of_eq h1 h2.symm) == 0 then