chore: move to new frontend

src/Init/Data/String/Basic.lean

@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -10,7 +11,7 @@ import Init.Data.Option.Basic
 universes u
 
 structure String :=
-(data : List Char)
+  (data : List Char)
 
 /-- A byte position in a `String`. Internally, `String`s are UTF-8 encoded.
 Codepoint positions (counting the Unicode codepoints rather than bytes)
@@ -20,295 +21,301 @@ positions need to be translated internally to byte positions in linear-time. -/
 abbrev String.Pos := Nat
 
 structure Substring :=
-(str : String) (startPos : String.Pos) (stopPos : String.Pos)
+  (str : String)
+  (startPos : String.Pos)
+  (stopPos : String.Pos)
 
 attribute [extern "lean_string_mk"] String.mk
 attribute [extern "lean_string_data"] String.data
 
 @[extern "lean_string_dec_eq"]
 def String.decEq (s₁ s₂ : @& String) : Decidable (s₁ = s₂) :=
-match s₁, s₂ with
-| ⟨s₁⟩, ⟨s₂⟩ =>
- if h : s₁ = s₂ then isTrue (congrArg _ h)
- else isFalse (fun h' => String.noConfusion h' (fun h' => absurd h' h))
+  match s₁, s₂ with
+  | ⟨s₁⟩, ⟨s₂⟩ =>
+   if h : s₁ = s₂ then isTrue (congrArg _ h)
+   else isFalse (fun h' => String.noConfusion h' (fun h' => absurd h' h))
 
-instance : DecidableEq String :=
-String.decEq
+instance : DecidableEq String := String.decEq
 
 def List.asString (s : List Char) : String :=
-⟨s⟩
+  ⟨s⟩
 
 namespace String
 instance : HasLess String :=
-⟨fun s₁ s₂ => s₁.data < s₂.data⟩
+  ⟨fun s₁ s₂ => s₁.data < s₂.data⟩
 
 @[extern "lean_string_dec_lt"]
 instance decLt (s₁ s₂ : @& String) : Decidable (s₁ < s₂) :=
-List.hasDecidableLt s₁.data s₂.data
+  List.hasDecidableLt s₁.data s₂.data
 
 @[extern "lean_string_length"]
 def length : (@& String) → Nat
-| ⟨s⟩ => s.length
+  | ⟨s⟩ => s.length
 
 /- The internal implementation uses dynamic arrays and will perform destructive updates
    if the String is not shared. -/
 @[extern "lean_string_push"]
 def push : String → Char → String
-| ⟨s⟩, c => ⟨s ++ [c]⟩
+  | ⟨s⟩, c => ⟨s ++ [c]⟩
 
 /- The internal implementation uses dynamic arrays and will perform destructive updates
    if the String is not shared. -/
 @[extern "lean_string_append"]
 def append : String → (@& String) → String
-| ⟨a⟩, ⟨b⟩ => ⟨a ++ b⟩
+  | ⟨a⟩, ⟨b⟩ => ⟨a ++ b⟩
 
 /- O(n) in the runtime, where n is the length of the String -/
 def toList (s : String) : List Char :=
-s.data
+  s.data
 
 private def csize (c : Char) : Nat :=
-c.utf8Size.toNat
+  c.utf8Size.toNat
 
 private def utf8ByteSizeAux : List Char → Nat → Nat
-| [],    r => r
-| c::cs, r => utf8ByteSizeAux cs (r + csize c)
+  | [],    r => r
+  | c::cs, r => utf8ByteSizeAux cs (r + csize c)
 
 @[extern "lean_string_utf8_byte_size"]
 def utf8ByteSize : (@& String) → Nat
-| ⟨s⟩ => utf8ByteSizeAux s 0
+  | ⟨s⟩ => utf8ByteSizeAux s 0
 
 @[inline] def bsize (s : String) : Nat :=
-utf8ByteSize s
+  utf8ByteSize s
 
-@[inline] def toSubstring (s : String) : Substring :=
-{str := s, startPos := 0, stopPos := s.bsize}
+@[inline] def toSubstring (s : String) : Substring := {
+  str := s,
+  startPos := 0,
+  stopPos := s.bsize
+}
 
 private def utf8GetAux : List Char → Pos → Pos → Char
-| [],    i, p => arbitrary Char
-| c::cs, i, p => if i = p then c else utf8GetAux cs (i + csize c) p
+  | [],    i, p => arbitrary Char
+  | c::cs, i, p => if i = p then c else utf8GetAux cs (i + csize c) p
 
 @[extern "lean_string_utf8_get"]
 def get : (@& String) → (@& Pos) → Char
-| ⟨s⟩, p => utf8GetAux s 0 p
+  | ⟨s⟩, p => utf8GetAux s 0 p
 
 private def utf8SetAux (c' : Char) : List Char → Pos → Pos → List Char
-| [],    i, p => []
-| c::cs, i, p =>
-  if i = p then (c'::cs) else c::(utf8SetAux cs (i + csize c) p)
+  | [],    i, p => []
+  | c::cs, i, p =>
+    if i = p then (c'::cs) else c::(utf8SetAux c' cs (i + csize c) p)
 
 @[extern "lean_string_utf8_set"]
 def set : String → (@& Pos) → Char → String
-| ⟨s⟩, i, c => ⟨utf8SetAux c s 0 i⟩
+  | ⟨s⟩, i, c => ⟨utf8SetAux c s 0 i⟩
 
 def modify (s : String) (i : Pos) (f : Char → Char) : String :=
-s.set i $ f $ s.get i
+  s.set i $ f $ s.get i
 
 @[extern "lean_string_utf8_next"]
 def next (s : @& String) (p : @& Pos) : Pos :=
-let c := get s p;
-p + csize c
+  let c := get s p
+  p + csize c
 
 private def utf8PrevAux : List Char → Pos → Pos → Pos
-| [],    i, p => 0
-| c::cs, i, p =>
-  let cz := csize c;
-  let i' := i + cz;
-  if i' = p then i else utf8PrevAux cs i' p
+  | [],    i, p => 0
+  | c::cs, i, p =>
+    let cz := csize c
+    let i' := i + cz
+    if i' = p then i else utf8PrevAux cs i' p
 
 @[extern "lean_string_utf8_prev"]
 def prev : (@& String) → (@& Pos) → Pos
-| ⟨s⟩, p => if p = 0 then 0 else utf8PrevAux s 0 p
+  | ⟨s⟩, p => if p = 0 then 0 else utf8PrevAux s 0 p
 
 def front (s : String) : Char :=
-get s 0
+  get s 0
 
 def back (s : String) : Char :=
-get s (prev s (bsize s))
+  get s (prev s (bsize s))
 
 @[extern "lean_string_utf8_at_end"]
 def atEnd : (@& String) → (@& Pos) → Bool
-| s, p => p ≥ utf8ByteSize s
+  | s, p => p ≥ utf8ByteSize s
 
 /- TODO: remove `partial` keywords after we restore the tactic
   framework and wellfounded recursion support -/
 
-partial def posOfAux (s : String) (c : Char) (stopPos : Pos) : Pos → Pos
-| pos =>
+partial def posOfAux (s : String) (c : Char) (stopPos : Pos) (pos : Pos) : Pos :=
   if pos == stopPos then pos
   else if s.get pos == c then pos
-       else posOfAux (s.next pos)
+       else posOfAux s c stopPos (s.next pos)
 
 @[inline] def posOf (s : String) (c : Char) : Pos :=
-posOfAux s c s.bsize 0
+  posOfAux s c s.bsize 0
 
-partial def revPosOfAux (s : String) (c : Char) : Pos → Option Pos
-| pos =>
+partial def revPosOfAux (s : String) (c : Char) (pos : Pos) : Option Pos :=
  if s.get pos == c then some pos
  else if pos == 0 then none
- else revPosOfAux (s.prev pos)
+ else revPosOfAux s c (s.prev pos)
 
 def revPosOf (s : String) (c : Char) : Option Pos :=
-if s.bsize == 0 then none
-else revPosOfAux s c (s.prev s.bsize)
+  if s.bsize == 0 then none
+  else revPosOfAux s c (s.prev s.bsize)
 
 private def utf8ExtractAux₂ : List Char → Pos → Pos → List Char
-| [],    _, _ => []
-| c::cs, i, e => if i = e then [] else c :: utf8ExtractAux₂ cs (i + csize c) e
+  | [],    _, _ => []
+  | c::cs, i, e => if i = e then [] else c :: utf8ExtractAux₂ cs (i + csize c) e
 
 private def utf8ExtractAux₁ : List Char → Pos → Pos → Pos → List Char
-| [],        _, _, _ => []
-| s@(c::cs), i, b, e => if i = b then utf8ExtractAux₂ s i e else utf8ExtractAux₁ cs (i + csize c) b e
+  | [],        _, _, _ => []
+  | s@(c::cs), i, b, e => if i = b then utf8ExtractAux₂ s i e else utf8ExtractAux₁ cs (i + csize c) b e
 
 @[extern "lean_string_utf8_extract"]
 def extract : (@& String) → (@& Pos) → (@& Pos) → String
-| ⟨s⟩, b, e => if b ≥ e then ⟨[]⟩ else ⟨utf8ExtractAux₁ s 0 b e⟩
+  | ⟨s⟩, b, e => if b ≥ e then ⟨[]⟩ else ⟨utf8ExtractAux₁ s 0 b e⟩
 
-@[specialize] partial def splitAux (s : String) (p : Char → Bool) : Pos → Pos → List String → List String
-| b, i, r =>
+@[specialize] partial def splitAux (s : String) (p : Char → Bool) (b : Pos) (i : Pos) (r : List String) : List String :=
   if s.atEnd i then
-    let r := if p (s.get i) then ""::(s.extract b (i-1))::r else (s.extract b i)::r;
+    let r := if p (s.get i) then ""::(s.extract b (i-1))::r else (s.extract b i)::r
     r.reverse
   else if p (s.get i) then
-    let i := s.next i;
-    splitAux i i (s.extract b (i-1)::r)
-  else splitAux b (s.next i) r
+    let i := s.next i
+    splitAux s p i i (s.extract b (i-1)::r)
+  else
+    splitAux s p b (s.next i) r
 
 @[specialize] def split (s : String) (p : Char → Bool) : List String :=
-splitAux s p 0 0 []
+  splitAux s p 0 0 []
 
-partial def splitOnAux (s sep : String) : Pos → Pos → Pos → List String → List String
-| b, i, j, r =>
+partial def splitOnAux (s sep : String) (b : Pos) (i : Pos) (j : Pos) (r : List String) : List String :=
   if s.atEnd i then
-    let r := if sep.atEnd j then ""::(s.extract b (i-j))::r else (s.extract b i)::r;
+    let r := if sep.atEnd j then ""::(s.extract b (i-j))::r else (s.extract b i)::r
     r.reverse
   else if s.get i == sep.get j then
-    let i := s.next i;
-    let j := sep.next j;
-    if sep.atEnd j then splitOnAux i i 0 (s.extract b (i-j)::r)
-    else splitOnAux b i j r
-  else splitOnAux b (s.next i) 0 r
+    let i := s.next i
+    let j := sep.next j
+    if sep.atEnd j then
+      splitOnAux s sep i i 0 (s.extract b (i-j)::r)
+    else
+      splitOnAux s sep b i j r
+  else
+    splitOnAux s sep b (s.next i) 0 r
 
 def splitOn (s : String) (sep : String := " ") : List String :=
-if sep == "" then [s] else splitOnAux s sep 0 0 0 []
+  if sep == "" then [s] else splitOnAux s sep 0 0 0 []
 
-instance : Inhabited String :=
-⟨""⟩
+instance : Inhabited String := ⟨""⟩
 
-instance : HasSizeof String :=
-⟨String.length⟩
+instance : HasSizeof String := ⟨String.length⟩
 
-instance : HasAppend String :=
-⟨String.append⟩
+instance : HasAppend String := ⟨String.append⟩
 
 def str : String → Char → String := push
 
 def pushn (s : String) (c : Char) (n : Nat) : String :=
-n.repeat (fun s => s.push c) s
+  n.repeat (fun s => s.push c) s
 
 def isEmpty (s : String) : Bool :=
-s.bsize == 0
+  s.bsize == 0
 
 def join (l : List String) : String :=
-l.foldl (fun r s => r ++ s) ""
+  l.foldl (fun r s => r ++ s) ""
 
 def singleton (c : Char) : String :=
-"".push c
+  "".push c
 
 def intercalate (s : String) (ss : List String) : String :=
-(List.intercalate s.toList (ss.map toList)).asString
+  (List.intercalate s.toList (ss.map toList)).asString
 
 structure Iterator :=
-(s : String) (i : Pos)
+  (s : String)
+  (i : Pos)
 
 def mkIterator (s : String) : Iterator :=
-⟨s, 0⟩
+  ⟨s, 0⟩
 
 namespace Iterator
 def toString : Iterator → String
-| ⟨s, _⟩ => s
+  | ⟨s, _⟩ => s
 
 def remainingBytes : Iterator → Nat
-| ⟨s, i⟩ => s.bsize - i
+  | ⟨s, i⟩ => s.bsize - i
 
 def pos : Iterator → Pos
-| ⟨s, i⟩ => i
+  | ⟨s, i⟩ => i
 
 def curr : Iterator → Char
-| ⟨s, i⟩ => get s i
+  | ⟨s, i⟩ => get s i
 
 def next : Iterator → Iterator
-| ⟨s, i⟩ => ⟨s, s.next i⟩
+  | ⟨s, i⟩ => ⟨s, s.next i⟩
 
 def prev : Iterator → Iterator
-| ⟨s, i⟩ => ⟨s, s.prev i⟩
+  | ⟨s, i⟩ => ⟨s, s.prev i⟩
 
 def hasNext : Iterator → Bool
-| ⟨s, i⟩ => i < utf8ByteSize s
+  | ⟨s, i⟩ => i < utf8ByteSize s
 
 def hasPrev : Iterator → Bool
-| ⟨s, i⟩ => i > 0
+  | ⟨s, i⟩ => i > 0
 
 def setCurr : Iterator → Char → Iterator
-| ⟨s, i⟩, c => ⟨s.set i c, i⟩
+  | ⟨s, i⟩, c => ⟨s.set i c, i⟩
 
 def toEnd : Iterator → Iterator
-| ⟨s, _⟩ => ⟨s, s.bsize⟩
+  | ⟨s, _⟩ => ⟨s, s.bsize⟩
 
 def extract : Iterator → Iterator → String
-| ⟨s₁, b⟩, ⟨s₂, e⟩ =>
-  if s₁ ≠ s₂ || b > e then ""
-  else s₁.extract b e
+  | ⟨s₁, b⟩, ⟨s₂, e⟩ =>
+    if s₁ ≠ s₂ || b > e then ""
+    else s₁.extract b e
 
 def forward : Iterator → Nat → Iterator
-| it, 0   => it
-| it, n+1 => forward it.next n
+  | it, 0   => it
+  | it, n+1 => forward it.next n
 
 def remainingToString : Iterator → String
-| ⟨s, i⟩ => s.extract i s.bsize
+  | ⟨s, i⟩ => s.extract i s.bsize
 
 /- (isPrefixOfRemaining it₁ it₂) is `true` Iff `it₁.remainingToString` is a prefix
    of `it₂.remainingToString`. -/
 def isPrefixOfRemaining : Iterator → Iterator → Bool
-| ⟨s₁, i₁⟩, ⟨s₂, i₂⟩ => s₁.extract i₁ s₁.bsize = s₂.extract i₂ (i₂ + (s₁.bsize - i₁))
+  | ⟨s₁, i₁⟩, ⟨s₂, i₂⟩ => s₁.extract i₁ s₁.bsize = s₂.extract i₂ (i₂ + (s₁.bsize - i₁))
 
 def nextn : Iterator → Nat → Iterator
-| it, 0   => it
-| it, i+1 => nextn it.next i
+  | it, 0   => it
+  | it, i+1 => nextn it.next i
 
 def prevn : Iterator → Nat → Iterator
-| it, 0   => it
-| it, i+1 => prevn it.prev i
+  | it, 0   => it
+  | it, i+1 => prevn it.prev i
 end Iterator
 
-partial def offsetOfPosAux (s : String) (pos : Pos) : Pos → Nat → Nat
-| i, offset =>
-  if i == pos || s.atEnd i then offset
-  else offsetOfPosAux (s.next i) (offset+1)
+partial def offsetOfPosAux (s : String) (pos : Pos) (i : Pos) (offset : Nat) : Nat :=
+  if i == pos || s.atEnd i then
+    offset
+  else
+    offsetOfPosAux s pos (s.next i) (offset+1)
 
 def offsetOfPos (s : String) (pos : Pos) : Nat :=
-offsetOfPosAux s pos 0 0
+  offsetOfPosAux s pos 0 0
 
-@[specialize] partial def foldlAux {α : Type u} (f : α → Char → α) (s : String) (stopPos : Pos) : Pos → α → α
-| i, a =>
-  if i == stopPos then a
-  else foldlAux (s.next i) (f a (s.get i))
+@[specialize] partial def foldlAux {α : Type u} (f : α → Char → α) (s : String) (stopPos : Pos) (i : Pos) (a : α) : α :=
+  let rec loop (i : Pos) (a : α) :=
+    if i == stopPos then a
+    else loop (s.next i) (f a (s.get i))
+  loop i a
 
 @[inline] def foldl {α : Type u} (f : α → Char → α) (a : α) (s : String) : α :=
-foldlAux f s s.bsize 0 a
+  foldlAux f s s.bsize 0 a
 
-@[specialize] partial def foldrAux {α : Type u} (f : Char → α → α) (a : α) (s : String) (stopPos : Pos) : Pos → α
-| i =>
-  if i == stopPos then a
-  else f (s.get i) (foldrAux (s.next i))
+@[specialize] partial def foldrAux {α : Type u} (f : Char → α → α) (a : α) (s : String) (stopPos : Pos) (i : Pos) : α :=
+  let rec loop (i : Pos) :=
+    if i == stopPos then a
+    else f (s.get i) (loop (s.next i))
+  loop i
 
 @[inline] def foldr {α : Type u} (f : Char → α → α) (a : α) (s : String) : α :=
-foldrAux f a s s.bsize 0
+  foldrAux f a s s.bsize 0
 
-@[specialize] partial def anyAux (s : String) (stopPos : Pos) (p : Char → Bool) : Pos → Bool
-| i =>
-  if i == stopPos then false
-  else if p (s.get i) then true
-  else anyAux (s.next i)
+@[specialize] partial def anyAux (s : String) (stopPos : Pos) (p : Char → Bool) (i : Pos) : Bool :=
+  let rec loop (i : Pos) :=
+    if i == stopPos then false
+    else if p (s.get i) then true
+    else loop (s.next i)
+  loop i
 
 @[inline] def any (s : String) (p : Char → Bool) : Bool :=
 anyAux s s.bsize p 0
@@ -319,184 +326,188 @@ anyAux s s.bsize p 0
 def contains (s : String) (c : Char) : Bool :=
 s.any (fun a => a == c)
 
-@[specialize] partial def mapAux (f : Char → Char) : Pos → String → String
-| i, s =>
+@[specialize] partial def mapAux (f : Char → Char) (i : Pos) (s : String) : String :=
   if s.atEnd i then s
   else
-    let c := f (s.get i);
-    let s := s.set i c;
-    mapAux (s.next i) s
+    let c := f (s.get i)
+    let s := s.set i c
+    mapAux f (s.next i) s
 
 @[inline] def map (f : Char → Char) (s : String) : String :=
-mapAux f 0 s
+  mapAux f 0 s
 
 def isNat (s : String) : Bool :=
-s.all $ fun c => c.isDigit
+  s.all $ fun c => c.isDigit
 
 def toNat? (s : String) : Option Nat :=
-if s.isNat then
-  some $ s.foldl (fun n c => n*10 + (c.toNat - '0'.toNat)) 0
-else
-  none
-
-partial def isPrefixOfAux (p s : String) : Pos → Bool
-| i =>
-  if p.atEnd i then true
+  if s.isNat then
+    some $ s.foldl (fun n c => n*10 + (c.toNat - '0'.toNat)) 0
   else
-    let c₁ := p.get i;
-    let c₂ := s.get i;
-    c₁ == c₂ && isPrefixOfAux (s.next i)
+    none
 
 /- Return true iff `p` is a prefix of `s` -/
-def isPrefixOf (p : String) (s : String) : Bool :=
-p.length ≤ s.length && isPrefixOfAux p s 0
+partial def isPrefixOf (p : String) (s : String) : Bool :=
+  let rec loop (i : Pos) :=
+    if p.atEnd i then true
+    else
+      let c₁ := p.get i
+      let c₂ := s.get i
+      c₁ == c₂ && loop (s.next i)
+  p.length ≤ s.length && loop 0
 
 end String
 
 namespace Substring
 
 @[inline] def toString : Substring → String
-| ⟨s, b, e⟩ => s.extract b e
+  | ⟨s, b, e⟩ => s.extract b e
 
 @[inline] def toIterator : Substring → String.Iterator
-| ⟨s, b, _⟩ => ⟨s, b⟩
+  | ⟨s, b, _⟩ => ⟨s, b⟩
 
 @[inline] def get : Substring → String.Pos → Char
-| ⟨s, b, _⟩, p => s.get (b+p)
+  | ⟨s, b, _⟩, p => s.get (b+p)
 
 @[inline] def next : Substring → String.Pos → String.Pos
-| ⟨s, b, e⟩, p =>
-  let p := s.next (b+p);
-  if p > e then e - b else p - b
+  | ⟨s, b, e⟩, p =>
+    let p := s.next (b+p)
+    if p > e then e - b else p - b
 
 @[inline] def prev : Substring → String.Pos → String.Pos
-| ⟨s, b, _⟩, p =>
-  if p = b then p else s.prev (b+p) - b
+  | ⟨s, b, _⟩, p =>
+    if p = b then p else s.prev (b+p) - b
 
 def nextn : Substring → Nat → String.Pos → String.Pos
-| ss, 0,   p => p
-| ss, i+1, p => ss.nextn i (ss.next p)
+  | ss, 0,   p => p
+  | ss, i+1, p => ss.nextn i (ss.next p)
 
 def prevn : Substring → String.Pos → Nat → String.Pos
-| ss, 0,   p => p
-| ss, i+1, p => ss.prevn i (ss.prev p)
+  | ss, 0,   p => p
+  | ss, i+1, p => ss.prevn i (ss.prev p)
 
 @[inline] def front (s : Substring) : Char :=
-s.get 0
+  s.get 0
 
 @[inline] def posOf (s : Substring) (c : Char) : String.Pos :=
-match s with
-| ⟨s, b, e⟩ => (String.posOfAux s c e b) - b
+  match s with
+  | ⟨s, b, e⟩ => (String.posOfAux s c e b) - b
 
 @[inline] def drop : Substring → Nat → Substring
-| ss@⟨s, b, e⟩, n => ⟨s, ss.nextn n b, e⟩
+  | ss@⟨s, b, e⟩, n => ⟨s, ss.nextn n b, e⟩
 
 @[inline] def dropRight : Substring → Nat → Substring
-| ss@⟨s, b, e⟩, n => ⟨s, b, ss.prevn n e⟩
+  | ss@⟨s, b, e⟩, n => ⟨s, b, ss.prevn n e⟩
 
 @[inline] def take : Substring → Nat → Substring
-| ss@⟨s, b, e⟩, n => ⟨s, b, ss.nextn n b⟩
+  | ss@⟨s, b, e⟩, n => ⟨s, b, ss.nextn n b⟩
 
 @[inline] def takeRight : Substring → Nat → Substring
-| ss@⟨s, b, e⟩, n => ⟨s, ss.prevn n e, e⟩
+  | ss@⟨s, b, e⟩, n => ⟨s, ss.prevn n e, e⟩
 
 @[inline] def atEnd : Substring → String.Pos → Bool
-| ⟨s, b, e⟩, p => b + p == e
+  | ⟨s, b, e⟩, p => b + p == e
 
 @[inline] def extract : Substring → String.Pos → String.Pos → Substring
-| ⟨s, b, _⟩, b', e' => if b' ≥ e' then ⟨"", 0, 1⟩ else ⟨s, b+b', b+e'⟩
+  | ⟨s, b, _⟩, b', e' => if b' ≥ e' then ⟨"", 0, 1⟩ else ⟨s, b+b', b+e'⟩
 
-partial def splitOnAux (s sep : String) (stopPos : String.Pos) : String.Pos → String.Pos → String.Pos → List Substring → List Substring
-| b, i, j, r =>
-  if i == stopPos then
-    let r := if sep.atEnd j then "".toSubstring::{str := s, startPos := b, stopPos := i-j}::r else {str := s, startPos := b, stopPos := i}::r;
-    r.reverse
-  else if s.get i == sep.get j then
-    let i := s.next i;
-    let j := sep.next j;
-    if sep.atEnd j then splitOnAux i i 0 ({str := s, startPos := b, stopPos := i-j}::r)
-    else splitOnAux b i j r
-  else splitOnAux b (s.next i) 0 r
-
-def splitOn (s : Substring) (sep : String := " ") : List Substring :=
-if sep == "" then [s] else splitOnAux s.str sep s.stopPos s.startPos s.startPos 0 []
+partial def splitOn (s : Substring) (sep : String := " ") : List Substring :=
+  if sep == "" then
+    [s]
+  else
+    let stopPos := s.stopPos
+    let str     := s.str
+    let rec loop (b i j : String.Pos) (r : List Substring) : List Substring :=
+      if i == stopPos then
+        let r := if sep.atEnd j then
+          "".toSubstring::{ str := str, startPos := b, stopPos := i-j } :: r
+        else
+          { str := str, startPos := b, stopPos := i } :: r
+        r.reverse
+      else if s.get i == sep.get j then
+        let i := s.next i
+        let j := sep.next j
+        if sep.atEnd j then
+          loop i i 0 ({ str := str, startPos := b, stopPos := i-j } :: r)
+        else
+          loop b i j r
+      else
+        loop b (s.next i) 0 r
+    loop s.startPos s.startPos 0 []
 
 @[inline] def foldl {α : Type u} (f : α → Char → α) (a : α) (s : Substring) : α :=
-match s with
-| ⟨s, b, e⟩ => String.foldlAux f s e b a
+  match s with
+  | ⟨s, b, e⟩ => String.foldlAux f s e b a
 
 @[inline] def foldr {α : Type u} (f : Char → α → α) (a : α) (s : Substring) : α :=
-match s with
-| ⟨s, b, e⟩ => String.foldrAux f a s e b
+  match s with
+  | ⟨s, b, e⟩ => String.foldrAux f a s e b
 
 @[inline] def any (s : Substring) (p : Char → Bool) : Bool :=
-match s with
-| ⟨s, b, e⟩ => String.anyAux s e p b
+  match s with
+  | ⟨s, b, e⟩ => String.anyAux s e p b
 
 @[inline] def all (s : Substring) (p : Char → Bool) : Bool :=
-!s.any (fun c => !p c)
+  !s.any (fun c => !p c)
 
 def contains (s : Substring) (c : Char) : Bool :=
-s.any (fun a => a == c)
+  s.any (fun a => a == c)
 
-@[specialize] partial def takeWhileAux (s : String) (stopPos : String.Pos) (p : Char → Bool) : String.Pos → String.Pos
-| i =>
+@[specialize] partial def takeWhileAux (s : String) (stopPos : String.Pos) (p : Char → Bool) (i : String.Pos) : String.Pos :=
   if i == stopPos then i
-  else if p (s.get i) then takeWhileAux (s.next i)
+  else if p (s.get i) then takeWhileAux s stopPos p (s.next i)
   else i
 
 @[inline] def takeWhile : Substring → (Char → Bool) → Substring
-| ⟨s, b, e⟩, p =>
-  let e := takeWhileAux s e p b;
-  ⟨s, b, e⟩
+  | ⟨s, b, e⟩, p =>
+    let e := takeWhileAux s e p b;
+    ⟨s, b, e⟩
 
 @[inline] def dropWhile : Substring → (Char → Bool) → Substring
-| ⟨s, b, e⟩, p =>
-  let b := takeWhileAux s e p b;
-  ⟨s, b, e⟩
+  | ⟨s, b, e⟩, p =>
+    let b := takeWhileAux s e p b;
+    ⟨s, b, e⟩
 
-@[specialize] partial def takeRightWhileAux (s : String) (begPos : String.Pos) (p : Char → Bool) : String.Pos → String.Pos
-| i =>
+@[specialize] partial def takeRightWhileAux (s : String) (begPos : String.Pos) (p : Char → Bool) (i : String.Pos) : String.Pos :=
   if i == begPos then i
   else
-    let i' := s.prev i;
-    let c  := s.get i';
+    let i' := s.prev i
+    let c  := s.get i'
     if !p c then i
-    else takeRightWhileAux i'
+    else takeRightWhileAux s begPos p i'
 
 @[inline] def takeRightWhile : Substring → (Char → Bool) → Substring
-| ⟨s, b, e⟩, p =>
-  let b := takeRightWhileAux s b p e;
-  ⟨s, b, e⟩
+  | ⟨s, b, e⟩, p =>
+    let b := takeRightWhileAux s b p e
+    ⟨s, b, e⟩
 
 @[inline] def dropRightWhile : Substring → (Char → Bool) → Substring
-| ⟨s, b, e⟩, p =>
-  let e := takeRightWhileAux s b p e;
-  ⟨s, b, e⟩
+  | ⟨s, b, e⟩, p =>
+    let e := takeRightWhileAux s b p e
+    ⟨s, b, e⟩
 
 @[inline] def trimLeft (s : Substring) : Substring :=
-s.dropWhile Char.isWhitespace
+  s.dropWhile Char.isWhitespace
 
 @[inline] def trimRight (s : Substring) : Substring :=
-s.dropRightWhile Char.isWhitespace
+  s.dropRightWhile Char.isWhitespace
 
 @[inline] def trim : Substring → Substring
-| ⟨s, b, e⟩ =>
-  let b := takeWhileAux s e Char.isWhitespace b;
-  let e := takeRightWhileAux s b Char.isWhitespace e;
-  ⟨s, b, e⟩
+  | ⟨s, b, e⟩ =>
+    let b := takeWhileAux s e Char.isWhitespace b
+    let e := takeRightWhileAux s b Char.isWhitespace e
+    ⟨s, b, e⟩
 
 def isNat (s : Substring) : Bool :=
-s.all $ fun c => c.isDigit
+  s.all $ fun c => c.isDigit
 
 def toNat? (s : Substring) : Option Nat :=
-if s.isNat then
-  some $ s.foldl (fun n c => n*10 + (c.toNat - '0'.toNat)) 0
-else
-  none
+  if s.isNat then
+    some $ s.foldl (fun n c => n*10 + (c.toNat - '0'.toNat)) 0
+  else
+    none
 
 def beq (ss1 ss2 : Substring) : Bool :=
-ss1.toString == ss2.toString
+  ss1.toString == ss2.toString
 
 instance hasBeq : HasBeq Substring := ⟨beq⟩
 
@@ -505,42 +516,42 @@ end Substring
 namespace String
 
 def drop (s : String) (n : Nat) : String :=
-(s.toSubstring.drop n).toString
+  (s.toSubstring.drop n).toString
 
 def dropRight (s : String) (n : Nat) : String :=
-(s.toSubstring.dropRight n).toString
+  (s.toSubstring.dropRight n).toString
 
 def take (s : String) (n : Nat) : String :=
-(s.toSubstring.take n).toString
+  (s.toSubstring.take n).toString
 
 def takeRight (s : String) (n : Nat) : String :=
-(s.toSubstring.takeRight n).toString
+  (s.toSubstring.takeRight n).toString
 
 def takeWhile (s : String) (p : Char → Bool) : String :=
-(s.toSubstring.takeWhile p).toString
+  (s.toSubstring.takeWhile p).toString
 
 def dropWhile (s : String) (p : Char → Bool) : String :=
-(s.toSubstring.dropWhile p).toString
+  (s.toSubstring.dropWhile p).toString
 
 def trimRight (s : String) : String :=
-s.toSubstring.trimRight.toString
+  s.toSubstring.trimRight.toString
 
 def trimLeft (s : String) : String :=
-s.toSubstring.trimLeft.toString
+  s.toSubstring.trimLeft.toString
 
 def trim (s : String) : String :=
-s.toSubstring.trim.toString
+  s.toSubstring.trim.toString
 
 @[inline] def nextWhile (s : String) (p : Char → Bool) (i : String.Pos) : String.Pos :=
-Substring.takeWhileAux s s.bsize p i
+  Substring.takeWhileAux s s.bsize p i
 
 @[inline] def nextUntil (s : String) (p : Char → Bool) (i : String.Pos) : String.Pos :=
-nextWhile s (fun c => !p c) i
+  nextWhile s (fun c => !p c) i
 
 def capitalize (s : String) :=
-s.set 0 $ (s.get 0).toUpper
+  s.set 0 $ (s.get 0).toUpper
 
 end String
 
 protected def Char.toString (c : Char) : String :=
-String.singleton c
+  String.singleton c

src/Init/Data/String/Extra.lean

@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -11,18 +12,18 @@ import Init.Util
 namespace String
 
 def toNat! (s : String) : Nat :=
-if s.isNat then
-  s.foldl (fun n c => n*10 + (c.toNat - '0'.toNat)) 0
-else
-  panic! "Nat expected"
+  if s.isNat then
+    s.foldl (fun n c => n*10 + (c.toNat - '0'.toNat)) 0
+  else
+    panic! "Nat expected"
 
 /--
   Convert a UTF-8 encoded `ByteArray` string to `String`.
   The result is unspecified if `a` is not properly UTF-8 encoded. -/
 @[extern "lean_string_from_utf8_unchecked"]
-constant fromUTF8Unchecked (a : @& ByteArray) : String := arbitrary _
+constant fromUTF8Unchecked (a : @& ByteArray) : String
 
 @[extern "lean_string_to_utf8"]
-constant toUTF8 (a : @& String) : ByteArray := arbitrary _
+constant toUTF8 (a : @& String) : ByteArray
 
 end String