Numerical Parsers
module Parser.Numbers
import public Parser
import Data.Vect
import Control.Eff
Base Abstraction
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
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 <- charPredicate (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
export
integer : Base -> Parser Integer
integer b = do
negative <- map isJust . tryMaybe $ charExact '-'
value <- map natToInteger $ nat b
if negative
then pure $ negate value
else pure $ value
export
integerBase10 : Parser Integer
integerBase10 = integer base10
Double
-- 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 <- charPredicate (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 $ charExact '-'
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 <- charExact '.'
error <- replaceError "Expected digit"
digits <- map forget $ atLeastOne error parseDigit
pure $ pack digits
exponent : Parser String
exponent = do
e <- theseChars ['e', 'E']
sign <- theseChars ['+', '-']
error <- replaceError "Expected digit"
digits <- map forget $ atLeastOne error parseDigit
pure . pack $ sign :: digits
Unit tests
Test roundtripping a value through the provided parser
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
-- @@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)
-- @@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
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'
-- @@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")