Init.Data.String.Basic

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

source

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

String

Equations

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

source

@[extern lean_string_utf8_next]

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

String.Pos

Equations

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

source

@[extern lean_string_utf8_prev]

def String.prev :

String → String.Pos → String.Pos

Equations

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

source

def String.front (s : String) :

Char

Equations

String.front s = String.get s 0

source

def String.back (s : String) :

Char

Equations

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

source

@[extern lean_string_utf8_at_end]

def String.atEnd :

String → String.Pos → Bool

Equations

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

source

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

String.Pos

source

@[inline]

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

String.Pos

Equations

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

source

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

Option String.Pos

source

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

Option String.Pos

Equations

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

source

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

String.Pos

source

@[inline]

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

String.Pos

Equations

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

source

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

Option String.Pos

source

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

Option String.Pos

Equations

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

source

@[inline]

abbrev String.Pos.min (p₁ : String.Pos) (p₂ : String.Pos) :

String.Pos

Equations

String.Pos.min p₁ p₂ = { byteIdx := Nat.min p₁.byteIdx p₂.byteIdx }

source

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

String.Pos

Equations

String.firstDiffPos a b = let stopPos := String.Pos.min (String.endPos a) (String.endPos b); String.firstDiffPos.loop a b stopPos 0

Returns the first position where the two strings differ.

source

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

String.Pos

source

@[extern lean_string_utf8_extract]

def String.extract :

String → String.Pos → String.Pos → String

Equations

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

source

def String.extract.go₁ :

List Char → String.Pos → String.Pos → String.Pos → List Char

Equations

String.extract.go₁ [] _fun_discr _fun_discr _fun_discr = []
String.extract.go₁ (c :: cs) _fun_discr _fun_discr _fun_discr = if _fun_discr = _fun_discr then String.extract.go₂ (c :: cs) _fun_discr _fun_discr else String.extract.go₁ cs (_fun_discr + c) _fun_discr _fun_discr

source

def String.extract.go₂ :

List Char → String.Pos → String.Pos → List Char

Equations

String.extract.go₂ [] _fun_discr _fun_discr = []
String.extract.go₂ (c :: cs) _fun_discr _fun_discr = if _fun_discr = _fun_discr then [] else c :: String.extract.go₂ cs (_fun_discr + c) _fun_discr

source

@[specialize]

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

List String

source

@[specialize]

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

List String

Equations

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

source

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

List String

source

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

List String

Equations

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

source

instance String.instInhabitedString :

Inhabited String

Equations

String.instInhabitedString = { default := "" }

source

instance String.instAppendString :

Append String

Equations

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

source

def String.str :

String → Char → String

Equations

String.str = String.push

source

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

String

Equations

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

source

def String.isEmpty (s : String) :

Bool

Equations

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

source

def String.join (l : List String) :

String

Equations

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

source

def String.singleton (c : Char) :

String

Equations

String.singleton c = String.push "" c

source

def String.intercalate (s : String) :

List String → String

Equations

String.intercalate s _fun_discr = match _fun_discr with | [] => "" | a :: as => String.intercalate.go a s as

source

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

source

structure String.Iterator :

Type

s : String
i : String.Pos

source

instance String.instDecidableEqIterator :

DecidableEq String.Iterator

Equations

String.instDecidableEqIterator = [anonymous]

source

def String.mkIterator (s : String) :

String.Iterator

Equations

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

source

@[inline]

abbrev String.iter (s : String) :

String.Iterator

Equations

String.iter = String.mkIterator

source

instance String.instSizeOfIterator :

SizeOf String.Iterator

Equations

String.instSizeOfIterator = { sizeOf := fun i => String.utf8ByteSize i.s - i.i.byteIdx }

source

theorem String.Iterator.sizeOf_eq (i : String.Iterator) :

sizeOf i = String.utf8ByteSize i.s - i.i.byteIdx

source

def String.Iterator.toString :

String.Iterator → String

Equations

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

source

def String.Iterator.remainingBytes :

String.Iterator → Nat

Equations

String.Iterator.remainingBytes _fun_discr = match _fun_discr with | { s := s, i := i } => (String.endPos s).byteIdx - i.byteIdx

source

def String.Iterator.pos :

String.Iterator → String.Pos

Equations

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

source

def String.Iterator.curr :

String.Iterator → Char

Equations

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

source

def String.Iterator.next :

String.Iterator → String.Iterator

Equations

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

source

def String.Iterator.prev :

String.Iterator → String.Iterator

Equations

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

source

def String.Iterator.atEnd :

String.Iterator → Bool

Equations

String.Iterator.atEnd _fun_discr = match _fun_discr with | { s := s, i := i } => decide (i.byteIdx ≥ (String.endPos s).byteIdx)

source

def String.Iterator.hasNext :

String.Iterator → Bool

Equations

String.Iterator.hasNext _fun_discr = match _fun_discr with | { s := s, i := i } => decide (i.byteIdx < (String.endPos s).byteIdx)

source

def String.Iterator.hasPrev :

String.Iterator → Bool

Equations

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

source

def String.Iterator.setCurr :

String.Iterator → Char → String.Iterator

Equations

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

source

def String.Iterator.toEnd :

String.Iterator → String.Iterator

Equations

String.Iterator.toEnd _fun_discr = match _fun_discr with | { s := s, i := i } => { s := s, i := String.endPos s }

source

def String.Iterator.extract :

String.Iterator → String.Iterator → String

Equations

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

source

def String.Iterator.forward :

String.Iterator → Nat → String.Iterator

Equations

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

source

def String.Iterator.remainingToString :

String.Iterator → String

Equations

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

source

def String.Iterator.nextn :

String.Iterator → Nat → String.Iterator

Equations

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

source

def String.Iterator.prevn :

String.Iterator → Nat → String.Iterator

Equations

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

source

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

Nat

source

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

Nat

Equations

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

source

@[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 = String.foldlAux.loop f s stopPos i a

source

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

α

source

@[inline]

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

α

Equations

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

source

@[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 = String.foldrAux.loop f a s stopPos i

source

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

α

source

@[inline]

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

α

Equations

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

source

@[specialize]

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

Bool

Equations

String.anyAux s stopPos p i = String.anyAux.loop s stopPos p i

source

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

Bool

source

@[inline]

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

Bool

Equations

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

source

@[inline]

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

Bool

Equations

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

source

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

Bool

Equations

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

source

@[specialize]

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

String

source

@[inline]

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

String

Equations

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

source

def String.isNat (s : String) :

Bool

Equations

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

source

def String.toNat? (s : String) :

Option Nat

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

source

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

Bool

Equations

String.substrEq s1 off1 s2 off2 sz = (decide (off1.byteIdx + sz ≤ (String.endPos s1).byteIdx) && decide (off2.byteIdx + sz ≤ (String.endPos s2).byteIdx) && String.substrEq.loop s1 s2 off1 off2 { byteIdx := off1.byteIdx + sz })

Return true iff the substring of byte size sz starting at position off1 in s1 is equal to that starting at off2 in s2.. False if either substring of that byte size does not exist.

source

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

Bool

source

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

Bool

Equations

String.isPrefixOf p s = String.substrEq p 0 s 0 (String.endPos p).byteIdx

Return true iff p is a prefix of s

source

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

String

Equations

String.replace s pattern replacement = String.replace.loop s pattern replacement "" 0 0

Replace all occurrences of pattern in s with replacment.

source

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

String

source

@[inline]

def Substring.isEmpty (ss : Substring) :

Bool

Equations

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

source

@[inline]

def Substring.toString :

Substring → String

Equations

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

source

@[inline]

def Substring.toIterator :

Substring → String.Iterator

Equations

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

source

@[inline]

def Substring.get :

Substring → String.Pos → Char

Equations

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

Return the codepoint at the given offset into the substring.

source

@[inline]

def Substring.next :

Substring → String.Pos → String.Pos

Equations

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

Given an offset of a codepoint into the substring, return the offset there of the next codepoint.

source

@[inline]

def Substring.prev :

Substring → String.Pos → String.Pos

Equations

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

Given an offset of a codepoint into the substring, return the offset there of the previous codepoint.

source

def Substring.nextn :

Substring → Nat → String.Pos → String.Pos

Equations

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

source

def Substring.prevn :

Substring → Nat → String.Pos → String.Pos

Equations

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

source

@[inline]

def Substring.front (s : Substring) :

Char

Equations

Substring.front s = Substring.get s 0

source

@[inline]

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

String.Pos

Equations

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

Return the offset into s of the first occurence of c in s, or s.bsize if c doesn't occur.

source

@[inline]

def Substring.drop :

Substring → Nat → Substring

Equations

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

source

@[inline]

def Substring.dropRight :

Substring → Nat → Substring

Equations

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

source

@[inline]

def Substring.take :

Substring → Nat → Substring

Equations

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

source

@[inline]

def Substring.takeRight :

Substring → Nat → Substring

Equations

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

source

@[inline]

def Substring.atEnd :

Substring → String.Pos → Bool

Equations

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

source

@[inline]

def Substring.extract :

Substring → String.Pos → String.Pos → Substring

Equations

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

source

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

List Substring

Equations

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

source

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

List Substring

source

@[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

source

@[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

source

@[inline]

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

Bool

Equations

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

source

@[inline]

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

Bool

Equations

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

source

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

Bool

Equations

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

source

@[inline]

def Substring.takeWhile :

Substring → (Char → Bool) → Substring

Equations

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

source

@[inline]

def Substring.dropWhile :

Substring → (Char → Bool) → Substring

Equations

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

source

@[inline]

def Substring.takeRightWhile :

Substring → (Char → Bool) → Substring

Equations

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

source

@[inline]

def Substring.dropRightWhile :

Substring → (Char → Bool) → Substring

Equations

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

source

@[inline]

def Substring.trimLeft (s : Substring) :

Substring

Equations

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

source

@[inline]

def Substring.trimRight (s : Substring) :

Substring

Equations

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

source

@[inline]

def Substring.trim :

Substring → Substring

Equations

Substring.trim _fun_discr = match _fun_discr 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 }