Documentation

Init.Data.String.Basic

def List.asString (s : List Char) :

Equations

List.asString s = { data := s }

instance String.instLTString :

Equations

String.instLTString = { lt := fun s₁ s₂ => s₁.data < s₂.data }

@[extern lean_string_dec_lt]

instance String.decLt (s₁ : String) (s₂ : String) :

Decidable (s₁ < s₂)

Equations

String.decLt s₁ s₂ = List.hasDecidableLt s₁.data s₂.data

@[extern lean_string_length]

def String.length :

Equations

String.length x = match x with | { data := s } => List.length s

@[extern lean_string_push]

def String.push :

String → Char → String

Equations

String.push x x = match x, x with | { data := s }, c => { data := s ++ [c] }

@[extern lean_string_append]

def String.append :

String → String → String

Equations

String.append x x = match x, x with | { data := a }, { data := b } => { data := a ++ b }

def String.toList (s : String) :

Equations

String.toList s = s.data

@[extern lean_string_utf8_get]

def String.get :

String → String.Pos → Char

Equations

String.get x x = match x, x with | { data := s }, p => String.utf8GetAux s 0 p

def String.getOp (self : String) (idx : String.Pos) :

Equations

String.getOp self idx = String.get self idx

@[extern lean_string_utf8_set]

def String.set :

String → String.Pos → Char → String

Equations

String.set x x x = match x, x, x with | { data := s }, i, c => { data := String.utf8SetAux c s 0 i }

def String.modify (s : String) (i : String.Pos) (f : Char → Char) :

Equations

String.modify s i f = String.set s i (f (String.get s i))

@[extern lean_string_utf8_next]

def String.next (s : String) (p : String.Pos) :

Equations

String.next s p = let c := String.get s p; p + String.csize c

@[extern lean_string_utf8_prev]

def String.prev :

String → String.Pos → String.Pos

Equations

String.prev x x = match x, x with | { data := s }, p => if p = 0 then 0 else String.utf8PrevAux s 0 p

def String.front (s : String) :

Equations

String.front s = String.get s 0

def String.back (s : String) :

Equations

String.back s = String.get s (String.prev s (String.bsize s))

@[extern lean_string_utf8_at_end]

def String.atEnd :

String → String.Pos → Bool

Equations

String.atEnd x x = match x, x with | s, p => decide (p ≥ String.utf8ByteSize s)

partial def String.posOfAux (s : String) (c : Char) (stopPos : String.Pos) (pos : String.Pos) :

@[inline]

def String.posOf (s : String) (c : Char) :

Equations

String.posOf s c = String.posOfAux s c (String.bsize s) 0

partial def String.revPosOfAux (s : String) (c : Char) (pos : String.Pos) :

Option String.Pos

def String.revPosOf (s : String) (c : Char) :

Option String.Pos

Equations

String.revPosOf s c = if (String.bsize s == 0) = true then none else String.revPosOfAux s c (String.prev s (String.bsize s))

partial def String.findAux (s : String) (p : Char → Bool) (stopPos : String.Pos) (pos : String.Pos) :

@[inline]

def String.find (s : String) (p : Char → Bool) :

Equations

String.find s p = String.findAux s p (String.bsize s) 0

partial def String.revFindAux (s : String) (p : Char → Bool) (pos : String.Pos) :

Option String.Pos

def String.revFind (s : String) (p : Char → Bool) :

Option String.Pos

Equations

String.revFind s p = if (String.bsize s == 0) = true then none else String.revFindAux s p (String.prev s (String.bsize s))

def String.firstDiffPos (a : String) (b : String) :

Equations

String.firstDiffPos a b = let stopPos := Nat.min (String.bsize a) (String.bsize b); (fun loop => loop 0) (String.firstDiffPos.loop a b stopPos)

partial def String.firstDiffPos.loop (a : String) (b : String) (stopPos : Nat) (i : String.Pos) :

@[extern lean_string_utf8_extract]

def String.extract :

String → String.Pos → String.Pos → String

Equations

String.extract x x x = match x, x, x with | { data := s }, b, e => if b ≥ e then { data := [] } else { data := String.utf8ExtractAux₁ s 0 b e }

@[specialize]

partial def String.splitAux (s : String) (p : Char → Bool) (b : String.Pos) (i : String.Pos) (r : List String) :

@[specialize]

def String.split (s : String) (p : Char → Bool) :

Equations

String.split s p = String.splitAux s p 0 0 []

partial def String.splitOnAux (s : String) (sep : String) (b : String.Pos) (i : String.Pos) (j : String.Pos) (r : List String) :

def String.splitOn (s : String) (sep : optParam String " ") :

Equations

String.splitOn s sep = if (sep == "") = true then [s] else String.splitOnAux s sep 0 0 0 []

instance String.instInhabitedString :

Inhabited String

Equations

String.instInhabitedString = { default := "" }

instance String.instAppendString :

Equations

String.instAppendString = { append := String.append }

def String.str :

String → Char → String

Equations

String.str = String.push

def String.pushn (s : String) (c : Char) (n : Nat) :

Equations

String.pushn s c n = Nat.repeat (fun s => String.push s c) n s

def String.isEmpty (s : String) :

Equations

String.isEmpty s = (String.bsize s == 0)

def String.join (l : List String) :

Equations

String.join l = List.foldl (fun r s => r ++ s) "" l

def String.singleton (c : Char) :

Equations

String.singleton c = String.push "" c

def String.intercalate (s : String) :

List String → String

Equations

String.intercalate s x = (fun go => match x with | [] => "" | a :: as => go a s as) String.intercalate.go

def String.intercalate.go (acc : String) (s : String) :

List String → String

Equations

String.intercalate.go acc s (a :: as) = String.intercalate.go (acc ++ s ++ a) s as
String.intercalate.go acc s [] = acc

structure String.Iterator :

Type

s : String
i : String.Pos

instance String.instDecidableEqIterator :

DecidableEq String.Iterator

Equations

String.instDecidableEqIterator = [anonymous]

def String.mkIterator (s : String) :

String.Iterator

Equations

String.mkIterator s = { s := s, i := 0 }

def String.Iterator.toString :

String.Iterator → String

Equations

String.Iterator.toString x = match x with | { s := s, i := x } => s

def String.Iterator.remainingBytes :

String.Iterator → Nat

Equations

String.Iterator.remainingBytes x = match x with | { s := s, i := i } => String.bsize s - i

def String.Iterator.pos :

String.Iterator → String.Pos

Equations

String.Iterator.pos x = match x with | { s := s, i := i } => i

def String.Iterator.curr :

String.Iterator → Char

Equations

String.Iterator.curr x = match x with | { s := s, i := i } => String.get s i

def String.Iterator.next :

String.Iterator → String.Iterator

Equations

String.Iterator.next x = match x with | { s := s, i := i } => { s := s, i := String.next s i }

def String.Iterator.prev :

String.Iterator → String.Iterator

Equations

String.Iterator.prev x = match x with | { s := s, i := i } => { s := s, i := String.prev s i }

def String.Iterator.hasNext :

String.Iterator → Bool

Equations

String.Iterator.hasNext x = match x with | { s := s, i := i } => decide (i < String.utf8ByteSize s)

def String.Iterator.hasPrev :

String.Iterator → Bool

Equations

String.Iterator.hasPrev x = match x with | { s := s, i := i } => decide (i > 0)

def String.Iterator.setCurr :

String.Iterator → Char → String.Iterator

Equations

String.Iterator.setCurr x x = match x, x with | { s := s, i := i }, c => { s := String.set s i c, i := i }

def String.Iterator.toEnd :

String.Iterator → String.Iterator

Equations

String.Iterator.toEnd x = match x with | { s := s, i := x } => { s := s, i := String.bsize s }

def String.Iterator.extract :

String.Iterator → String.Iterator → String

Equations

String.Iterator.extract x x = match x, x with | { s := s₁, i := b }, { s := s₂, i := e } => if (decide (s₁ ≠ s₂) || decide (b > e)) = true then "" else String.extract s₁ b e

def String.Iterator.forward :

String.Iterator → Nat → String.Iterator

Equations

String.Iterator.forward x 0 = x
String.Iterator.forward x (Nat.succ n) = String.Iterator.forward (String.Iterator.next x) n

def String.Iterator.remainingToString :

String.Iterator → String

Equations

String.Iterator.remainingToString x = match x with | { s := s, i := i } => String.extract s i (String.bsize s)

def String.Iterator.nextn :

String.Iterator → Nat → String.Iterator

Equations

String.Iterator.nextn x 0 = x
String.Iterator.nextn x (Nat.succ n) = String.Iterator.nextn (String.Iterator.next x) n

def String.Iterator.prevn :

String.Iterator → Nat → String.Iterator

Equations

String.Iterator.prevn x 0 = x
String.Iterator.prevn x (Nat.succ n) = String.Iterator.prevn (String.Iterator.prev x) n

partial def String.offsetOfPosAux (s : String) (pos : String.Pos) (i : String.Pos) (offset : Nat) :

def String.offsetOfPos (s : String) (pos : String.Pos) :

Equations

String.offsetOfPos s pos = String.offsetOfPosAux s pos 0 0

@[specialize]

def String.foldlAux {α : Type u} (f : α → Char → α) (s : String) (stopPos : String.Pos) (i : String.Pos) (a : α) :

α

Equations

String.foldlAux f s stopPos i a = (fun loop => loop i a) (String.foldlAux.loop f s stopPos)

partial def String.foldlAux.loop {α : Type u} (f : α → Char → α) (s : String) (stopPos : String.Pos) (i : String.Pos) (a : α) :

α

@[inline]

def String.foldl {α : Type u} (f : α → Char → α) (init : α) (s : String) :

α

Equations

String.foldl f init s = String.foldlAux f s (String.bsize s) 0 init

@[specialize]

def String.foldrAux {α : Type u} (f : Char → α → α) (a : α) (s : String) (stopPos : String.Pos) (i : String.Pos) :

α

Equations

String.foldrAux f a s stopPos i = (fun loop => loop i) (String.foldrAux.loop f a s stopPos)

partial def String.foldrAux.loop {α : Type u} (f : Char → α → α) (a : α) (s : String) (stopPos : String.Pos) (i : String.Pos) :

α

@[inline]

def String.foldr {α : Type u} (f : Char → α → α) (init : α) (s : String) :

α

Equations

String.foldr f init s = String.foldrAux f init s (String.bsize s) 0

@[specialize]

def String.anyAux (s : String) (stopPos : String.Pos) (p : Char → Bool) (i : String.Pos) :

Equations

String.anyAux s stopPos p i = (fun loop => loop i) (String.anyAux.loop s stopPos p)

partial def String.anyAux.loop (s : String) (stopPos : String.Pos) (p : Char → Bool) (i : String.Pos) :

@[inline]

def String.any (s : String) (p : Char → Bool) :

Equations

String.any s p = String.anyAux s (String.bsize s) p 0

@[inline]

def String.all (s : String) (p : Char → Bool) :

Equations

String.all s p = !String.any s fun c => !p c

def String.contains (s : String) (c : Char) :

Equations

String.contains s c = String.any s fun a => a == c

@[specialize]

partial def String.mapAux (f : Char → Char) (i : String.Pos) (s : String) :

@[inline]

def String.map (f : Char → Char) (s : String) :

Equations

String.map f s = String.mapAux f 0 s

def String.isNat (s : String) :

Equations

String.isNat s = String.all s fun c => Char.isDigit c

def String.toNat? (s : String) :

Equations

String.toNat? s = if String.isNat s = true then some (String.foldl (fun n c => n * 10 + (Char.toNat c - Char.toNat (Char.ofNat 48))) 0 s) else none

def String.substrEq (s1 : String) (off1 : String.Pos) (s2 : String) (off2 : String.Pos) (sz : Nat) :

Equations

String.substrEq s1 off1 s2 off2 sz = (fun loop => decide (off1 + sz ≤ String.bsize s1) && decide (off2 + sz ≤ String.bsize s2) && loop off1 off2 (off1 + sz)) (String.substrEq.loop s1 s2)

partial def String.substrEq.loop (s1 : String) (s2 : String) (off1 : String.Pos) (off2 : String.Pos) (stop1 : String.Pos) :

def String.isPrefixOf (p : String) (s : String) :

Equations

String.isPrefixOf p s = String.substrEq p 0 s 0 (String.bsize p)

def String.replace (s : String) (pattern : String) (replacement : String) :

Equations

String.replace s pattern replacement = (fun loop => loop "" 0 0) (String.replace.loop s pattern replacement)

partial def String.replace.loop (s : String) (pattern : String) (replacement : String) (acc : String) (accStop : String.Pos) (pos : String.Pos) :

@[inline]

def Substring.isEmpty (ss : Substring) :

Equations

Substring.isEmpty ss = (Substring.bsize ss == 0)

@[inline]

def Substring.toString :

Substring → String

Equations

Substring.toString x = match x with | { str := s, startPos := b, stopPos := e } => String.extract s b e

@[inline]

def Substring.toIterator :

Substring → String.Iterator

Equations

Substring.toIterator x = match x with | { str := s, startPos := b, stopPos := x } => { s := s, i := b }

@[inline]

def Substring.get :

Substring → String.Pos → Char

Equations

Substring.get x x = match x, x with | { str := s, startPos := b, stopPos := x }, p => String.get s (b + p)

@[inline]

def Substring.next :

Substring → String.Pos → String.Pos

Equations

Substring.next x x = match x, x with | { str := s, startPos := b, stopPos := e }, p => let absP := b + p; if absP = e then p else String.next s absP - b

@[inline]

def Substring.prev :

Substring → String.Pos → String.Pos

Equations

Substring.prev x x = match x, x with | { str := s, startPos := b, stopPos := x }, p => let absP := b + p; if absP = b then p else String.prev s absP - b

def Substring.nextn :

Substring → Nat → String.Pos → String.Pos

Equations

Substring.nextn x 0 x = x
Substring.nextn x (Nat.succ i) x = Substring.nextn x i (Substring.next x x)

def Substring.prevn :

Substring → String.Pos → Nat → String.Pos

Equations

Substring.prevn x 0 x = x
Substring.prevn x (Nat.succ i) x = Substring.prevn x i (Substring.prev x x)

@[inline]

def Substring.front (s : Substring) :

Equations

Substring.front s = Substring.get s 0

@[inline]

def Substring.posOf (s : Substring) (c : Char) :

Equations

Substring.posOf s c = match s with | { str := s, startPos := b, stopPos := e } => String.posOfAux s c e b - b

@[inline]

def Substring.drop :

Substring → Nat → Substring

Equations

Substring.drop x x = match x, x with | ss@h:{ str := s, startPos := b, stopPos := e }, n => { str := s, startPos := b + Substring.nextn ss n 0, stopPos := e }

@[inline]

def Substring.dropRight :

Substring → Nat → Substring

Equations

Substring.dropRight x x = match x, x with | ss@h:{ str := s, startPos := b, stopPos := e }, n => { str := s, startPos := b, stopPos := b + Substring.prevn ss n (Substring.bsize ss) }

@[inline]

def Substring.take :

Substring → Nat → Substring

Equations

Substring.take x x = match x, x with | ss@h:{ str := s, startPos := b, stopPos := e }, n => { str := s, startPos := b, stopPos := b + Substring.nextn ss n 0 }

@[inline]

def Substring.takeRight :

Substring → Nat → Substring

Equations

Substring.takeRight x x = match x, x with | ss@h:{ str := s, startPos := b, stopPos := e }, n => { str := s, startPos := b + Substring.prevn ss n (Substring.bsize ss), stopPos := e }

@[inline]

def Substring.atEnd :

Substring → String.Pos → Bool

Equations

Substring.atEnd x x = match x, x with | { str := s, startPos := b, stopPos := e }, p => b + p == e

@[inline]

def Substring.extract :

Substring → String.Pos → String.Pos → Substring

Equations

Substring.extract x x x = match x, x, x with | { str := s, startPos := b, stopPos := e }, b', e' => if b' ≥ e' then { str := "", startPos := 0, stopPos := 0 } else { str := s, startPos := Nat.min e (b + b'), stopPos := Nat.min e (b + e') }

def Substring.splitOn (s : Substring) (sep : optParam String " ") :

Equations

Substring.splitOn s sep = if (sep == "") = true then [s] else (fun loop => loop 0 0 0 []) (Substring.splitOn.loop s sep)

partial def Substring.splitOn.loop (s : Substring) (sep : optParam String " ") (b : String.Pos) (i : String.Pos) (j : String.Pos) (r : List Substring) :

@[inline]

def Substring.foldl {α : Type u} (f : α → Char → α) (init : α) (s : Substring) :

α

Equations

Substring.foldl f init s = match s with | { str := s, startPos := b, stopPos := e } => String.foldlAux f s e b init

@[inline]

def Substring.foldr {α : Type u} (f : Char → α → α) (init : α) (s : Substring) :

α

Equations

Substring.foldr f init s = match s with | { str := s, startPos := b, stopPos := e } => String.foldrAux f init s e b

@[inline]

def Substring.any (s : Substring) (p : Char → Bool) :

Equations

Substring.any s p = match s with | { str := s, startPos := b, stopPos := e } => String.anyAux s e p b

@[inline]

def Substring.all (s : Substring) (p : Char → Bool) :

Equations

Substring.all s p = !Substring.any s fun c => !p c

def Substring.contains (s : Substring) (c : Char) :

Equations

Substring.contains s c = Substring.any s fun a => a == c

@[inline]

def Substring.takeWhile :

Substring → (Char → Bool) → Substring

Equations

Substring.takeWhile x x = match x, x with | { str := s, startPos := b, stopPos := e }, p => let e := Substring.takeWhileAux s e p b; { str := s, startPos := b, stopPos := e }

@[inline]

def Substring.dropWhile :

Substring → (Char → Bool) → Substring

Equations

Substring.dropWhile x x = match x, x with | { str := s, startPos := b, stopPos := e }, p => let b := Substring.takeWhileAux s e p b; { str := s, startPos := b, stopPos := e }

@[inline]

def Substring.takeRightWhile :

Substring → (Char → Bool) → Substring

Equations

Substring.takeRightWhile x x = match x, x with | { str := s, startPos := b, stopPos := e }, p => let b := Substring.takeRightWhileAux s b p e; { str := s, startPos := b, stopPos := e }

@[inline]

def Substring.dropRightWhile :

Substring → (Char → Bool) → Substring

Equations

Substring.dropRightWhile x x = match x, x with | { str := s, startPos := b, stopPos := e }, p => let e := Substring.takeRightWhileAux s b p e; { str := s, startPos := b, stopPos := e }

@[inline]

def Substring.trimLeft (s : Substring) :

Equations

Substring.trimLeft s = Substring.dropWhile s Char.isWhitespace

@[inline]

def Substring.trimRight (s : Substring) :

Equations

Substring.trimRight s = Substring.dropRightWhile s Char.isWhitespace

@[inline]

def Substring.trim :

Substring → Substring

Equations

Substring.trim x = match x with | { str := s, startPos := b, stopPos := e } => let b := Substring.takeWhileAux s e Char.isWhitespace b; let e := Substring.takeRightWhileAux s b Char.isWhitespace e; { str := s, startPos := b, stopPos := e }

def Substring.isNat (s : Substring) :

Equations

Substring.isNat s = Substring.all s fun c => Char.isDigit c

def Substring.toNat? (s : Substring) :

Equations

Substring.toNat? s = if Substring.isNat s = true then some (Substring.foldl (fun n c => n * 10 + (Char.toNat c - Char.toNat (Char.ofNat 48))) 0 s) else none

def Substring.beq (ss1 : Substring) (ss2 : Substring) :

Equations

Substring.beq ss1 ss2 = (Substring.bsize ss1 == Substring.bsize ss2 && String.substrEq ss1.str ss1.startPos ss2.str ss2.startPos (Substring.bsize ss1))

instance Substring.hasBeq :

Equations

Substring.hasBeq = { beq := Substring.beq }

def String.drop (s : String) (n : Nat) :

Equations

String.drop s n = Substring.toString (Substring.drop (String.toSubstring s) n)

def String.dropRight (s : String) (n : Nat) :

Equations

String.dropRight s n = Substring.toString (Substring.dropRight (String.toSubstring s) n)

def String.take (s : String) (n : Nat) :

Equations

String.take s n = Substring.toString (Substring.take (String.toSubstring s) n)

def String.takeRight (s : String) (n : Nat) :

Equations

String.takeRight s n = Substring.toString (Substring.takeRight (String.toSubstring s) n)

def String.takeWhile (s : String) (p : Char → Bool) :

Equations

String.takeWhile s p = Substring.toString (Substring.takeWhile (String.toSubstring s) p)

def String.dropWhile (s : String) (p : Char → Bool) :

Equations

String.dropWhile s p = Substring.toString (Substring.dropWhile (String.toSubstring s) p)

def String.takeRightWhile (s : String) (p : Char → Bool) :

Equations

String.takeRightWhile s p = Substring.toString (Substring.takeRightWhile (String.toSubstring s) p)

def String.dropRightWhile (s : String) (p : Char → Bool) :

Equations

String.dropRightWhile s p = Substring.toString (Substring.dropRightWhile (String.toSubstring s) p)

def String.startsWith (s : String) (pre : String) :

Equations

String.startsWith s pre = (Substring.take (String.toSubstring s) (String.length pre) == String.toSubstring pre)

def String.endsWith (s : String) (post : String) :

Equations

String.endsWith s post = (Substring.takeRight (String.toSubstring s) (String.length post) == String.toSubstring post)

def String.trimRight (s : String) :

Equations

String.trimRight s = Substring.toString (Substring.trimRight (String.toSubstring s))

def String.trimLeft (s : String) :

Equations

String.trimLeft s = Substring.toString (Substring.trimLeft (String.toSubstring s))

def String.trim (s : String) :

Equations

String.trim s = Substring.toString (Substring.trim (String.toSubstring s))

@[inline]

def String.nextWhile (s : String) (p : Char → Bool) (i : String.Pos) :

Equations

String.nextWhile s p i = Substring.takeWhileAux s (String.bsize s) p i

@[inline]

def String.nextUntil (s : String) (p : Char → Bool) (i : String.Pos) :

Equations

String.nextUntil s p i = String.nextWhile s (fun c => !p c) i

def String.toUpper (s : String) :

Equations

String.toUpper s = String.map Char.toUpper s

def String.toLower (s : String) :

Equations

String.toLower s = String.map Char.toLower s

def String.capitalize (s : String) :

Equations

String.capitalize s = String.set s 0 (Char.toUpper (String.get s 0))

def String.decapitalize (s : String) :

Equations

String.decapitalize s = String.set s 0 (Char.toLower (String.get s 0))

def Char.toString (c : Char) :

Equations

Char.toString c = String.singleton c