fix: use String.Slice (#98)

Author: fgdorais

UnicodeBasic/CharacterDatabase.lean

@@ -12,21 +12,21 @@ namespace Unicode
   around field values are not significant. Line comments are prefixed with a
   number sign `#` (U+0023).
 -/
-structure UCDStream extends Substring.Raw where
+structure UCDStream extends String.Slice where
   /-- `isUnihan` is true if the records are tab separated -/
   isUnihan := false
 deriving Inhabited
 
 namespace UCDStream
 
-/-- Make a `UCDStream` from a substring -/
-def ofSubstring (str : Substring.Raw) : UCDStream := { str with }
+/-- Make a `UCDStream` from a string slice -/
+def ofStringSlice (str : String.Slice) : UCDStream := { str with }
 
 /-- Make a `UCDStream` from a string -/
-def ofString (str : String) : UCDStream where
-  str := str
-  startPos := 0
-  stopPos := str.rawEndPos
+def ofString (str : String) : UCDStream := ofStringSlice str.toSlice
+
+/-- Make a `UCDStream` from a substring -/
+def ofSubstring (str : Substring.Raw) : UCDStream := ofStringSlice str.toString.toSlice
 
 /-- Make a `UCDStream` from a file -/
 def ofFile (path : System.FilePath) : IO UCDStream :=
@@ -36,29 +36,30 @@ def ofFile (path : System.FilePath) : IO UCDStream :=
 
   Line comments are stripped and blank lines are skipped.
 -/
-protected partial def nextLine? (stream : UCDStream) : Option (Substring.Raw × UCDStream) := do
-  if stream.isEmpty then failure else
-    let line := stream.trimLeft.takeWhile (.!='\n')
-    let nextPos := stream.next line.stopPos
-    let line := (line.takeWhile (.!='#')).trimRight
+protected partial def nextLine? (stream : UCDStream) : Option (String.Slice × UCDStream) := do
+  let line := stream.trimAsciiEnd.takeWhile (.!='\n')
+  if h : line.rawEndPos < stream.rawEndPos then
+    let nextPos := stream.findNextPos line.rawEndPos h
+    let line := (line.takeWhile (.!='#')).trimAsciiEnd
     if line.isEmpty then
-      UCDStream.nextLine? {stream with startPos := nextPos}
+      UCDStream.nextLine? {stream with toSlice := stream.replaceStart nextPos}
     else
-      return (line, {stream with startPos := nextPos})
+      return (line, {stream with toSlice := stream.replaceStart nextPos})
+  else failure
 
 /-- Get the next record from the `UCDStream`
 
   Spaces around field values are trimmed.
 -/
-protected def next? (stream : UCDStream) : Option (Array Substring.Raw × UCDStream) := do
+protected def next? (stream : UCDStream) : Option (Array String.Slice × UCDStream) := do
     let sep := if stream.isUnihan then "\t" else ";"
     let mut arr := #[]
     let (line, table) ← stream.nextLine?
-    for item in line.splitOn sep do
-      arr := arr.push item.trim
+    for item in line.split sep do
+      arr := arr.push item.trimAscii
     return (arr, table)
 
-instance : Std.Stream UCDStream (Array Substring.Raw) where
+instance : Std.Stream UCDStream (Array String.Slice) where
   next? := UCDStream.next?
 
 end UCDStream

UnicodeBasic/TableLookup.lean

@@ -36,7 +36,7 @@ private partial def find (c : UInt32) (t : USize → UInt32) (lo hi : USize) : U
     find c t mid hi
 
 /-- Parse a simple table -/
-private def parseTable (s : String) (f : UInt32 → Array Substring.Raw → α) : Thunk <| Array (UInt32 × α) := Id.run do
+private def parseTable (s : String) (f : UInt32 → Array String.Slice → α) : Thunk <| Array (UInt32 × α) := Id.run do
   let mut r := #[]
   let mut stream := UCDStream.ofString s
   for record in stream do
@@ -46,7 +46,7 @@ private def parseTable (s : String) (f : UInt32 → Array Substring.Raw → α)
   return r
 
 /-- Parse a range compressed data table -/
-private def parseDataTable (s : String) (f : UInt32 → UInt32 → Array Substring.Raw → α) : Thunk <| Array (UInt32 × UInt32 × α) := Id.run do
+private def parseDataTable (s : String) (f : UInt32 → UInt32 → Array String.Slice → α) : Thunk <| Array (UInt32 × UInt32 × α) := Id.run do
   let mut r := #[]
   let mut stream := UCDStream.ofString s
   for record in stream do
@@ -171,7 +171,7 @@ where
         else if x[0]! == "<square>" then some .square
         else if x[0]! == "<fraction>" then some .fraction
         else if x[0]! == "<compat>" then some .compat
-        else panic! s!"invalid compatibility tag {x[0]!}"
+        else panic! s!"invalid compatibility tag {x[0]!.copy}"
       (tag, x[1:].toArray.map ofHexString!)
 
 /-- Get general category of a code point using lookup table
@@ -194,7 +194,7 @@ def lookupName (c : UInt32) : String :=
     match table[find c (fun i => table[i]!.1) 0 table.size.toUSize]! with
     | (_, v, d) =>
       if c ≤ v then
-        if d.get 0 == '<' then
+        if Char.ofUInt8 (d.getUTF8Byte! 0) == '<' then
           if d == "<Control>" then
             s!"<control-{toHexStringAux c}>"
           else if d == "<Private Use>" then
@@ -227,12 +227,12 @@ def lookupName (c : UInt32) : String :=
             "TANGUT COMPONENT-" ++ i
           else if d == "<Tangut Ideograph>" then
             "TANGUT IDEOGRAPH-" ++ toHexStringAux c
-          else panic! s!"unknown name range {d}"
-        else Substring.Raw.toString d
+          else panic! s!"unknown name range {d.copy}"
+        else String.Slice.copy d
       else s!"<noncharacter-{toHexStringAux c}>"
 where
   str : String := include_str "../data/table/Name.txt"
-  table : Thunk <| Array (UInt32 × UInt32 × Substring.Raw) :=
+  table : Thunk <| Array (UInt32 × UInt32 × String.Slice) :=
     parseDataTable str fun _ _ x => x[0]!
 
 /-- Get numeric value of a code point using lookup table
@@ -265,7 +265,7 @@ where
   str : String := include_str "../data/table/Numeric_Value.txt"
   table : Thunk <| Array (UInt32 × UInt32 × NumericType) :=
     parseDataTable str fun _ _ a =>
-      let s := a[0]!.toString
+      let s := a[0]!.copy
       if s == "decimal" then
         .decimal 0
       else if "digit".isPrefixOf s then