257 lines
6.6 KiB
Markdown
257 lines
6.6 KiB
Markdown
# Numerical Parsers
|
|
|
|
```idris
|
|
module Parser.Numbers
|
|
|
|
import public Parser
|
|
|
|
import Data.Vect
|
|
import Control.Eff
|
|
```
|
|
|
|
<!-- idris
|
|
import System
|
|
-->
|
|
|
|
## Base Abstraction
|
|
|
|
```idris
|
|
public export
|
|
record Base where
|
|
constructor MkBase
|
|
base : Nat
|
|
digits : Vect base Char
|
|
%name Base b
|
|
|
|
export
|
|
hasDigit : Base -> Char -> Bool
|
|
hasDigit (MkBase base digits) c = any (== c) digits
|
|
|
|
export
|
|
digitValue : Base -> Char -> Maybe Nat
|
|
digitValue (MkBase base digits) c = digitValue' digits 0
|
|
where
|
|
digitValue' : Vect n Char -> (idx : Nat) -> Maybe Nat
|
|
digitValue' [] idx = Nothing
|
|
digitValue' (x :: xs) idx =
|
|
if x == c
|
|
then Just idx
|
|
else digitValue' xs (S idx)
|
|
|
|
public export
|
|
base10 : Base
|
|
base10 = MkBase 10
|
|
['0', '1', '2', '3', '4', '5', '6', '7', '8', '9']
|
|
|
|
public export
|
|
hex : Base
|
|
hex = MkBase 16
|
|
['0', '1', '2', '3', '4', '5', '6', '7', '8', '9', 'a', 'b', 'c', 'd', 'e', 'f']
|
|
```
|
|
|
|
## Parsers
|
|
|
|
### Nat
|
|
|
|
```idris
|
|
export
|
|
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)
|
|
| 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
|
|
natBase10 : Parser Nat
|
|
natBase10 = nat base10
|
|
```
|
|
|
|
### Integer
|
|
|
|
```idris
|
|
export
|
|
integer : Base -> Parser Integer
|
|
integer b = do
|
|
negative <- map isJust . tryMaybe $ parseExactChar '-'
|
|
value <- map natToInteger $ nat b
|
|
if negative
|
|
then pure $ negate value
|
|
else pure $ value
|
|
|
|
export
|
|
integerBase10 : Parser Integer
|
|
integerBase10 = integer base10
|
|
```
|
|
|
|
### Double
|
|
|
|
```idris
|
|
-- TODO: Replicate `parseDouble` logic and make this base-generic
|
|
export
|
|
double : Parser Double
|
|
double = do
|
|
starting_state <- save
|
|
integer <- integer
|
|
fraction <- tryMaybe fraction
|
|
exponent <- tryMaybe exponent
|
|
let str = case (fraction, exponent) of
|
|
(Nothing, Nothing) =>
|
|
integer
|
|
(Nothing, (Just exponent)) =>
|
|
"\{integer}e\{exponent}"
|
|
((Just fraction), Nothing) =>
|
|
"\{integer}.\{fraction}"
|
|
((Just fraction), (Just exponent)) =>
|
|
"\{integer}.\{fraction}e\{exponent}"
|
|
Just out <- pure $ parseDouble str
|
|
| _ =>
|
|
throw $ MkParseError starting_state "Std failed to parse as double: \{str}"
|
|
pure out
|
|
where
|
|
parseDigit : Parser Char
|
|
parseDigit = do
|
|
GotChar char <- parseChar (hasDigit base10)
|
|
| GotError e => throwParseError "\{show e} is not a digit"
|
|
| EndOfInput => throwParseError "End Of Input"
|
|
pure char
|
|
integer : Parser String
|
|
integer = do
|
|
sign <- tryMaybe $ parseExactChar '-'
|
|
error <- replaceError "Expected digit"
|
|
digits <- map forget $ atLeastOne error parseDigit
|
|
case sign of
|
|
Nothing => pure $ pack digits
|
|
Just x => pure $ pack (x :: digits)
|
|
fraction : Parser String
|
|
fraction = do
|
|
decimal <- parseExactChar '.'
|
|
error <- replaceError "Expected digit"
|
|
digits <- map forget $ atLeastOne error parseDigit
|
|
pure $ pack digits
|
|
exponent : Parser String
|
|
exponent = do
|
|
e <- parseTheseChars ['e', 'E']
|
|
sign <- parseTheseChars ['+', '-']
|
|
error <- replaceError "Expected digit"
|
|
digits <- map forget $ atLeastOne error parseDigit
|
|
pure . pack $ sign :: digits
|
|
```
|
|
|
|
## Unit tests
|
|
|
|
Test roundtripping a value through the provided parser
|
|
|
|
```idris
|
|
roundtrip : Eq a => Show a => a -> (p : Parser a) -> IO Bool
|
|
roundtrip x p = do
|
|
let string = show x
|
|
putStrLn "Roundtripping \{string}"
|
|
Just state <- newInternalIO string
|
|
| _ => do
|
|
putStrLn "Failed to produce parser for \{string}"
|
|
pure False
|
|
Right result <- runEff (rundownFirst p) [handleParserStateIO state] {m = IO}
|
|
| Left err => do
|
|
printLn err
|
|
pure False
|
|
putStrLn "Input: \{string} Output: \{show result}"
|
|
pure $ x == result
|
|
```
|
|
|
|
Do some roundtrip tests with the nat parser
|
|
|
|
```idris
|
|
-- @@test Nat round trip
|
|
natRoundTrip : IO Bool
|
|
natRoundTrip = pure $
|
|
!(roundtrip 0 natBase10)
|
|
&& !(roundtrip 1 natBase10)
|
|
&& !(roundtrip 100 natBase10)
|
|
&& !(roundtrip 1234 natBase10)
|
|
&& !(roundtrip 1234567890 natBase10)
|
|
&& !(roundtrip 1234567890000 natBase10)
|
|
&& !(roundtrip 12345678901234567890 natBase10)
|
|
```
|
|
|
|
```idris
|
|
-- @@test Integer round trip
|
|
integerRoundTrip : IO Bool
|
|
integerRoundTrip = pure $
|
|
!(roundtrip 0 integerBase10)
|
|
&& !(roundtrip 1 integerBase10)
|
|
&& !(roundtrip 100 integerBase10)
|
|
&& !(roundtrip 1234 integerBase10)
|
|
&& !(roundtrip 1234567890 integerBase10)
|
|
&& !(roundtrip 1234567890000 integerBase10)
|
|
&& !(roundtrip 12345678901234567890 integerBase10)
|
|
&& !(roundtrip (-1) integerBase10)
|
|
&& !(roundtrip (-100) integerBase10)
|
|
&& !(roundtrip (-1234) integerBase10)
|
|
&& !(roundtrip (-1234567890) integerBase10)
|
|
&& !(roundtrip (-1234567890000) integerBase10)
|
|
&& !(roundtrip (-12345678901234567890) integerBase10)
|
|
```
|
|
|
|
Compare our parsing of a double to the standard library's
|
|
|
|
```idris
|
|
compareDouble : String -> IO Bool
|
|
compareDouble string = do
|
|
Just state <- newInternalIO string
|
|
| _ => do
|
|
putStrLn "Failed to produce parser for \{string}"
|
|
pure False
|
|
Right result <-
|
|
runEff (rundownFirst double) [handleParserStateIO state] {m = IO}
|
|
| Left err => do
|
|
printLn err
|
|
pure False
|
|
putStrLn "Input: \{string} Output: \{show result}"
|
|
Just double' <- pure $ parseDouble string
|
|
| _ => do
|
|
printLn "Std failed to parse as double: \{string}"
|
|
pure False
|
|
pure $ result == double'
|
|
```
|
|
|
|
```idris
|
|
-- @@test Double Std Comparison
|
|
doubleRoundTrip : IO Bool
|
|
doubleRoundTrip = pure $
|
|
!(compareDouble "0")
|
|
&& !(compareDouble "1")
|
|
&& !(compareDouble "100")
|
|
&& !(compareDouble "1234")
|
|
&& !(compareDouble "1234567890")
|
|
&& !(compareDouble "1234567890000")
|
|
&& !(compareDouble "12345678901234567890")
|
|
&& !(compareDouble "-1")
|
|
&& !(compareDouble "-100")
|
|
&& !(compareDouble "-1234")
|
|
&& !(compareDouble "-1234567890")
|
|
&& !(compareDouble "-1234567890000")
|
|
&& !(compareDouble "-12345678901234567890")
|
|
&& !(compareDouble "0.0")
|
|
&& !(compareDouble "1.0")
|
|
&& !(compareDouble "-1.0")
|
|
&& !(compareDouble "-0.0")
|
|
&& !(compareDouble "-0.0")
|
|
&& !(compareDouble "0.1234")
|
|
&& !(compareDouble "0.01234")
|
|
&& !(compareDouble "-0.1234")
|
|
&& !(compareDouble "-0.01234")
|
|
&& !(compareDouble "1.234e+5")
|
|
&& !(compareDouble "1.234e-5")
|
|
&& !(compareDouble "-1.234e+5")
|
|
&& !(compareDouble "-1.234e-5")
|
|
```
|