From 85d7f3321c751b300c85dbcf164c2ef32e28cea9 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Tue, 25 Nov 2025 16:48:41 +0100 Subject: [PATCH] feat: `String.Slice.toInt?` (#11358) This PR adds `String.Slice.toInt?` and variants. Closes #11275. --- src/Init/Data/String.lean | 1 - src/Init/Data/String/Repr.lean | 89 -------------------------------- src/Init/Data/String/Search.lean | 72 ++++++++++++++++++++++++++ src/Init/Data/String/Slice.lean | 79 ++++++++++++++++++++++++++++ 4 files changed, 151 insertions(+), 90 deletions(-) delete mode 100644 src/Init/Data/String/Repr.lean diff --git a/src/Init/Data/String.lean b/src/Init/Data/String.lean index eaf176126a..32b65b317f 100644 --- a/src/Init/Data/String.lean +++ b/src/Init/Data/String.lean @@ -13,7 +13,6 @@ public import Init.Data.String.Defs public import Init.Data.String.Extra public import Init.Data.String.Iterator public import Init.Data.String.Lemmas -public import Init.Data.String.Repr public import Init.Data.String.Bootstrap public import Init.Data.String.Slice public import Init.Data.String.Pattern diff --git a/src/Init/Data/String/Repr.lean b/src/Init/Data/String/Repr.lean deleted file mode 100644 index 64d86db3a8..0000000000 --- a/src/Init/Data/String/Repr.lean +++ /dev/null @@ -1,89 +0,0 @@ -/- -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura, Mario Carneiro --/ -module - -prelude -public import Init.Data.String.Substring -import Init.Data.String.Search - -public section - -/-- -Interprets a string as the decimal representation of an integer, returning it. Returns `none` if -the string does not contain a decimal integer. - -A string can be interpreted as a decimal integer if it only consists of at least one decimal digit -and optionally `-` in front. Leading `+` characters are not allowed. - -Use `String.isInt` to check whether `String.toInt?` would return `some`. `String.toInt!` is an -alternative that panics instead of returning `none` when the string is not an integer. - -Examples: - * `"".toInt? = none` - * `"-".toInt? = none` - * `"0".toInt? = some 0` - * `"5".toInt? = some 5` - * `"-5".toInt? = some (-5)` - * `"587".toInt? = some 587` - * `"-587".toInt? = some (-587)` - * `" 5".toInt? = none` - * `"2-3".toInt? = none` - * `"0xff".toInt? = none` --/ -def String.toInt? (s : String) : Option Int := do - if s.front = '-' then do - let v ← (s.toRawSubstring.drop 1).toNat?; - pure <| - Int.ofNat v - else - Int.ofNat <$> s.toNat? - -/-- -Checks whether the string can be interpreted as the decimal representation of an integer. - -A string can be interpreted as a decimal integer if it only consists of at least one decimal digit -and optionally `-` in front. Leading `+` characters are not allowed. - -Use `String.toInt?` or `String.toInt!` to convert such a string to an integer. - -Examples: - * `"".isInt = false` - * `"-".isInt = false` - * `"0".isInt = true` - * `"-0".isInt = true` - * `"5".isInt = true` - * `"587".isInt = true` - * `"-587".isInt = true` - * `"+587".isInt = false` - * `" 5".isInt = false` - * `"2-3".isInt = false` - * `"0xff".isInt = false` --/ -def String.isInt (s : String) : Bool := - if s.front = '-' then - (s.toRawSubstring.drop 1).isNat - else - s.isNat - -/-- -Interprets a string as the decimal representation of an integer, returning it. Panics if the string -does not contain a decimal integer. - -A string can be interpreted as a decimal integer if it only consists of at least one decimal digit -and optionally `-` in front. Leading `+` characters are not allowed. - -Use `String.isInt` to check whether `String.toInt!` would return a value. `String.toInt?` is a safer -alternative that returns `none` instead of panicking when the string is not an integer. - -Examples: - * `"0".toInt! = 0` - * `"5".toInt! = 5` - * `"587".toInt! = 587` - * `"-587".toInt! = -587` --/ -def String.toInt! (s : String) : Int := - match s.toInt? with - | some v => v - | none => panic "Int expected" diff --git a/src/Init/Data/String/Search.lean b/src/Init/Data/String/Search.lean index 8a369f59f3..059ae87369 100644 --- a/src/Init/Data/String/Search.lean +++ b/src/Init/Data/String/Search.lean @@ -420,6 +420,78 @@ Examples: @[inline] def toNat! (s : String) : Nat := s.toSlice.toNat! +/-- +Interprets a string as the decimal representation of an integer, returning it. Returns {lean}`none` +if the string does not contain a decimal integer. + +A string can be interpreted as a decimal integer if it only consists of at least one decimal digit +and optionally {lit}`-` in front. Leading `+` characters are not allowed. + +Use {name (scope := "Init.Data.String.Search")}`String.isInt` to check whether {name}`String.toInt?` +would return {lean}`some`. {name (scope := "Init.Data.String.Search")}`String.toInt!` is an +alternative that panics instead of returning {lean}`none` when the string is not an integer. + +Examples: + * {lean}`"".toInt? = none` + * {lean}`"-".toInt? = none` + * {lean}`"0".toInt? = some 0` + * {lean}`"5".toInt? = some 5` + * {lean}`"-5".toInt? = some (-5)` + * {lean}`"587".toInt? = some 587` + * {lean}`"-587".toInt? = some (-587)` + * {lean}`" 5".toInt? = none` + * {lean}`"2-3".toInt? = none` + * {lean}`"0xff".toInt? = none` +-/ +@[inline] def toInt? (s : String) : Option Int := + s.toSlice.toInt? + +/-- +Checks whether the string can be interpreted as the decimal representation of an integer. + +A string can be interpreted as a decimal integer if it only consists of at least one decimal digit +and optionally {lit}`-` in front. Leading `+` characters are not allowed. + +Use {name}`String.toInt?` or {name (scope := "Init.Data.String.Search")}`String.toInt!` to convert +such a string to an integer. + +Examples: + * {lean}`"".isInt = false` + * {lean}`"-".isInt = false` + * {lean}`"0".isInt = true` + * {lean}`"-0".isInt = true` + * {lean}`"5".isInt = true` + * {lean}`"587".isInt = true` + * {lean}`"-587".isInt = true` + * {lean}`"+587".isInt = false` + * {lean}`" 5".isInt = false` + * {lean}`"2-3".isInt = false` + * {lean}`"0xff".isInt = false` +-/ +@[inline] def isInt (s : String) : Bool := + s.toSlice.isInt + +/-- +Interprets a string as the decimal representation of an integer, returning it. Panics if the string +does not contain a decimal integer. + +A string can be interpreted as a decimal integer if it only consists of at least one decimal digit +and optionally {lit}`-` in front. Leading `+` characters are not allowed. + +Use {name}`String.isInt` to check whether {name}`String.toInt!` would return a value. +{name}`String.toInt?` is a safer alternative that returns {lean}`none` instead of panicking when the +string is not an integer. + +Examples: + * {lean}`"0".toInt! = 0` + * {lean}`"5".toInt! = 5` + * {lean}`"587".toInt! = 587` + * {lean}`"-587".toInt! = -587` +-/ +@[inline] def toInt! (s : String) : Int := + s.toSlice.toInt! + + /-- Returns the first character in {name}`s`. If {name}`s` is empty, returns {name}`none`. diff --git a/src/Init/Data/String/Slice.lean b/src/Init/Data/String/Slice.lean index 06290a832a..3f7f23e4b3 100644 --- a/src/Init/Data/String/Slice.lean +++ b/src/Init/Data/String/Slice.lean @@ -1339,6 +1339,85 @@ Examples: def front (s : Slice) : Char := s.front?.getD default +/-- +Checks whether the slice can be interpreted as the decimal representation of an integer. + +A slice can be interpreted as a decimal integer if it only consists of at least one decimal digit +and optionally {lit}`-` in front. Leading {lit}`+` characters are not allowed. + +Use {name (scope := "Init.Data.String.Slice")}`String.Slice.toInt?` or {name (scope := "Init.Data.String.Slice")}`String.toInt!` to convert such a string to an integer. + +Examples: + * {lean}`"".toSlice.isInt = false` + * {lean}`"-".toSlice.isInt = false` + * {lean}`"0".toSlice.isInt = true` + * {lean}`"-0".toSlice.isInt = true` + * {lean}`"5".toSlice.isInt = true` + * {lean}`"587".toSlice.isInt = true` + * {lean}`"-587".toSlice.isInt = true` + * {lean}`"+587".toSlice.isInt = false` + * {lean}`" 5".toSlice.isInt = false` + * {lean}`"2-3".toSlice.isInt = false` + * {lean}`"0xff".toSlice.isInt = false` +-/ +def isInt (s : Slice) : Bool := + if s.front = '-' then + (s.drop 1).isNat + else + s.isNat + +/-- +Interprets a slice as the decimal representation of an integer, returning it. Returns {lean}`none` if +the string does not contain a decimal integer. + +A string can be interpreted as a decimal integer if it only consists of at least one decimal digit +and optionally {lit}`-` in front. Leading {lit}`+` characters are not allowed. + +Use {name}`Slice.isInt` to check whether {name}`Slice.toInt?` would return {lean}`some`. +{name (scope := "Init.Data.String.Slice")}`Slice.toInt!` is an alternative that panics instead of +returning {lean}`none` when the string is not an integer. + +Examples: + * {lean}`"".toSlice.toInt? = none` + * {lean}`"-".toSlice.toInt? = none` + * {lean}`"0".toSlice.toInt? = some 0` + * {lean}`"5".toSlice.toInt? = some 5` + * {lean}`"-5".toSlice.toInt? = some (-5)` + * {lean}`"587".toSlice.toInt? = some 587` + * {lean}`"-587".toSlice.toInt? = some (-587)` + * {lean}`" 5".toSlice.toInt? = none` + * {lean}`"2-3".toSlice.toInt? = none` + * {lean}`"0xff".toSlice.toInt? = none` +-/ +def toInt? (s : Slice) : Option Int := + if s.front = '-' then + Int.negOfNat <$> (s.drop 1).toNat? + else + Int.ofNat <$> s.toNat? + +/-- +Interprets a string as the decimal representation of an integer, returning it. Panics if the string +does not contain a decimal integer. + +A string can be interpreted as a decimal integer if it only consists of at least one decimal digit +and optionally {lit}`-` in front. Leading `+` characters are not allowed. + +Use {name}`Slice.isInt` to check whether {name}`Slice.toInt!` would return a value. +{name}`Slice.toInt?` is a safer alternative that returns {lean}`none` instead of panicking when the +string is not an integer. + +Examples: + * {lean}`"0".toSlice.toInt! = 0` + * {lean}`"5".toSlice.toInt! = 5` + * {lean}`"587".toSlice.toInt! = 587` + * {lean}`"-587".toSlice.toInt! = -587` +-/ +@[inline] +def toInt! (s : Slice) : Int := + match s.toInt? with + | some v => v + | none => panic "Int expected" + /-- Returns the last character in {name}`s`. If {name}`s` is empty, returns {name}`none`.