From 30ce419e063788fecfb607c04e2bd48eff8578a8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 23 Oct 2020 12:14:34 -0700 Subject: [PATCH] chore: move to new frontend --- src/Init/Data/String/Basic.lean | 477 ++++++++++++++++---------------- src/Init/Data/String/Extra.lean | 13 +- 2 files changed, 251 insertions(+), 239 deletions(-) diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean index 8aeabaea65..164769aa13 100644 --- a/src/Init/Data/String/Basic.lean +++ b/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 diff --git a/src/Init/Data/String/Extra.lean b/src/Init/Data/String/Extra.lean index 7b3de051a7..1b48e93bd0 100644 --- a/src/Init/Data/String/Extra.lean +++ b/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