numbers: Nat parser
This commit is contained in:
parent
82b16a0e63
commit
1cc6bea78e
1 changed files with 18 additions and 0 deletions
|
@ -9,6 +9,10 @@ import Data.Vect
|
||||||
import Control.Eff
|
import Control.Eff
|
||||||
```
|
```
|
||||||
|
|
||||||
|
<!-- idris
|
||||||
|
import System
|
||||||
|
-->
|
||||||
|
|
||||||
## Base Abstraction
|
## Base Abstraction
|
||||||
|
|
||||||
```idris
|
```idris
|
||||||
|
@ -52,6 +56,20 @@ hex = MkBase 16
|
||||||
```idris
|
```idris
|
||||||
export
|
export
|
||||||
nat : Base -> Parser Nat
|
nat : Base -> Parser Nat
|
||||||
|
nat b = do
|
||||||
|
error <- replaceError "Expected digit"
|
||||||
|
(first ::: rest) <- atLeastOne error parseDigit
|
||||||
|
pure $ foldl (\acc, e => 10 * acc + e) first rest
|
||||||
|
where
|
||||||
|
parseDigit : Parser Nat
|
||||||
|
parseDigit = do
|
||||||
|
GotChar char <- parseChar (hasDigit b) id
|
||||||
|
| GotError e => throwParseError "\{show e} is not a digit"
|
||||||
|
| EndOfInput => throwParseError "End Of Input"
|
||||||
|
case digitValue b char of
|
||||||
|
Nothing =>
|
||||||
|
throwParseError "Failed to parse as base \{show b.base}: \{show char}"
|
||||||
|
Just x => pure x
|
||||||
|
|
||||||
export
|
export
|
||||||
natBase10 : Parser Nat
|
natBase10 : Parser Nat
|
||||||
|
|
Loading…
Add table
Reference in a new issue