Skip to content

Commit 85d7f33

Browse files
TwoFXTwoFX
authored
feat: String.Slice.toInt? (#11358)
This PR adds `String.Slice.toInt?` and variants. Closes #11275.
1 parent d99c515 commit 85d7f33

File tree

4 files changed

+151
-90
lines changed

4 files changed

+151
-90
lines changed

‎src/Init/Data/String.lean‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,6 @@ public import Init.Data.String.Defs
1313
public import Init.Data.String.Extra
1414
public import Init.Data.String.Iterator
1515
public import Init.Data.String.Lemmas
16-
public import Init.Data.String.Repr
1716
public import Init.Data.String.Bootstrap
1817
public import Init.Data.String.Slice
1918
public import Init.Data.String.Pattern

‎src/Init/Data/String/Repr.lean‎

Lines changed: 0 additions & 89 deletions
This file was deleted.

‎src/Init/Data/String/Search.lean‎

Lines changed: 72 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -420,6 +420,78 @@ Examples:
420420
@[inline] def toNat! (s : String) : Nat :=
421421
s.toSlice.toNat!
422422

423+
/--
424+
Interprets a string as the decimal representation of an integer, returning it. Returns {lean}`none`
425+
if the string does not contain a decimal integer.
426+
427+
A string can be interpreted as a decimal integer if it only consists of at least one decimal digit
428+
and optionally {lit}`-` in front. Leading `+` characters are not allowed.
429+
430+
Use {name (scope := "Init.Data.String.Search")}`String.isInt` to check whether {name}`String.toInt?`
431+
would return {lean}`some`. {name (scope := "Init.Data.String.Search")}`String.toInt!` is an
432+
alternative that panics instead of returning {lean}`none` when the string is not an integer.
433+
434+
Examples:
435+
* {lean}`"".toInt? = none`
436+
* {lean}`"-".toInt? = none`
437+
* {lean}`"0".toInt? = some 0`
438+
* {lean}`"5".toInt? = some 5`
439+
* {lean}`"-5".toInt? = some (-5)`
440+
* {lean}`"587".toInt? = some 587`
441+
* {lean}`"-587".toInt? = some (-587)`
442+
* {lean}`" 5".toInt? = none`
443+
* {lean}`"2-3".toInt? = none`
444+
* {lean}`"0xff".toInt? = none`
445+
-/
446+
@[inline] def toInt? (s : String) : Option Int :=
447+
s.toSlice.toInt?
448+
449+
/--
450+
Checks whether the string can be interpreted as the decimal representation of an integer.
451+
452+
A string can be interpreted as a decimal integer if it only consists of at least one decimal digit
453+
and optionally {lit}`-` in front. Leading `+` characters are not allowed.
454+
455+
Use {name}`String.toInt?` or {name (scope := "Init.Data.String.Search")}`String.toInt!` to convert
456+
such a string to an integer.
457+
458+
Examples:
459+
* {lean}`"".isInt = false`
460+
* {lean}`"-".isInt = false`
461+
* {lean}`"0".isInt = true`
462+
* {lean}`"-0".isInt = true`
463+
* {lean}`"5".isInt = true`
464+
* {lean}`"587".isInt = true`
465+
* {lean}`"-587".isInt = true`
466+
* {lean}`"+587".isInt = false`
467+
* {lean}`" 5".isInt = false`
468+
* {lean}`"2-3".isInt = false`
469+
* {lean}`"0xff".isInt = false`
470+
-/
471+
@[inline] def isInt (s : String) : Bool :=
472+
s.toSlice.isInt
473+
474+
/--
475+
Interprets a string as the decimal representation of an integer, returning it. Panics if the string
476+
does not contain a decimal integer.
477+
478+
A string can be interpreted as a decimal integer if it only consists of at least one decimal digit
479+
and optionally {lit}`-` in front. Leading `+` characters are not allowed.
480+
481+
Use {name}`String.isInt` to check whether {name}`String.toInt!` would return a value.
482+
{name}`String.toInt?` is a safer alternative that returns {lean}`none` instead of panicking when the
483+
string is not an integer.
484+
485+
Examples:
486+
* {lean}`"0".toInt! = 0`
487+
* {lean}`"5".toInt! = 5`
488+
* {lean}`"587".toInt! = 587`
489+
* {lean}`"-587".toInt! = -587`
490+
-/
491+
@[inline] def toInt! (s : String) : Int :=
492+
s.toSlice.toInt!
493+
494+
423495
/--
424496
Returns the first character in {name}`s`. If {name}`s` is empty, returns {name}`none`.
425497

‎src/Init/Data/String/Slice.lean‎

Lines changed: 79 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1339,6 +1339,85 @@ Examples:
13391339
def front (s : Slice) : Char :=
13401340
s.front?.getD default
13411341

1342+
/--
1343+
Checks whether the slice can be interpreted as the decimal representation of an integer.
1344+
1345+
A slice can be interpreted as a decimal integer if it only consists of at least one decimal digit
1346+
and optionally {lit}`-` in front. Leading {lit}`+` characters are not allowed.
1347+
1348+
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.
1349+
1350+
Examples:
1351+
* {lean}`"".toSlice.isInt = false`
1352+
* {lean}`"-".toSlice.isInt = false`
1353+
* {lean}`"0".toSlice.isInt = true`
1354+
* {lean}`"-0".toSlice.isInt = true`
1355+
* {lean}`"5".toSlice.isInt = true`
1356+
* {lean}`"587".toSlice.isInt = true`
1357+
* {lean}`"-587".toSlice.isInt = true`
1358+
* {lean}`"+587".toSlice.isInt = false`
1359+
* {lean}`" 5".toSlice.isInt = false`
1360+
* {lean}`"2-3".toSlice.isInt = false`
1361+
* {lean}`"0xff".toSlice.isInt = false`
1362+
-/
1363+
def isInt (s : Slice) : Bool :=
1364+
if s.front = '-' then
1365+
(s.drop 1).isNat
1366+
else
1367+
s.isNat
1368+
1369+
/--
1370+
Interprets a slice as the decimal representation of an integer, returning it. Returns {lean}`none` if
1371+
the string does not contain a decimal integer.
1372+
1373+
A string can be interpreted as a decimal integer if it only consists of at least one decimal digit
1374+
and optionally {lit}`-` in front. Leading {lit}`+` characters are not allowed.
1375+
1376+
Use {name}`Slice.isInt` to check whether {name}`Slice.toInt?` would return {lean}`some`.
1377+
{name (scope := "Init.Data.String.Slice")}`Slice.toInt!` is an alternative that panics instead of
1378+
returning {lean}`none` when the string is not an integer.
1379+
1380+
Examples:
1381+
* {lean}`"".toSlice.toInt? = none`
1382+
* {lean}`"-".toSlice.toInt? = none`
1383+
* {lean}`"0".toSlice.toInt? = some 0`
1384+
* {lean}`"5".toSlice.toInt? = some 5`
1385+
* {lean}`"-5".toSlice.toInt? = some (-5)`
1386+
* {lean}`"587".toSlice.toInt? = some 587`
1387+
* {lean}`"-587".toSlice.toInt? = some (-587)`
1388+
* {lean}`" 5".toSlice.toInt? = none`
1389+
* {lean}`"2-3".toSlice.toInt? = none`
1390+
* {lean}`"0xff".toSlice.toInt? = none`
1391+
-/
1392+
def toInt? (s : Slice) : Option Int :=
1393+
if s.front = '-' then
1394+
Int.negOfNat <$> (s.drop 1).toNat?
1395+
else
1396+
Int.ofNat <$> s.toNat?
1397+
1398+
/--
1399+
Interprets a string as the decimal representation of an integer, returning it. Panics if the string
1400+
does not contain a decimal integer.
1401+
1402+
A string can be interpreted as a decimal integer if it only consists of at least one decimal digit
1403+
and optionally {lit}`-` in front. Leading `+` characters are not allowed.
1404+
1405+
Use {name}`Slice.isInt` to check whether {name}`Slice.toInt!` would return a value.
1406+
{name}`Slice.toInt?` is a safer alternative that returns {lean}`none` instead of panicking when the
1407+
string is not an integer.
1408+
1409+
Examples:
1410+
* {lean}`"0".toSlice.toInt! = 0`
1411+
* {lean}`"5".toSlice.toInt! = 5`
1412+
* {lean}`"587".toSlice.toInt! = 587`
1413+
* {lean}`"-587".toSlice.toInt! = -587`
1414+
-/
1415+
@[inline]
1416+
def toInt! (s : Slice) : Int :=
1417+
match s.toInt? with
1418+
| some v => v
1419+
| none => panic "Int expected"
1420+
13421421
/--
13431422
Returns the last character in {name}`s`. If {name}`s` is empty, returns {name}`none`.
13441423

0 commit comments

Comments
 (0)