From faaf42e66cca5eaf87cb1a9de0d644c0cf3162c7 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Fri, 24 Jan 2025 16:33:29 -0500 Subject: [PATCH] Add parsers for numerical values --- README.md | 4 + advent.ipkg | 1 + src/Parser/Numbers.md | 257 ++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 262 insertions(+) create mode 100644 src/Parser/Numbers.md diff --git a/README.md b/README.md index 6f18796..5e93985 100644 --- a/README.md +++ b/README.md @@ -71,6 +71,10 @@ solution. Internal state of a parser + - [Numbers](src/Parser/Numbers.md) + + Parsers for numerical values in multiple bases + ## Index of years and days - 2015 diff --git a/advent.ipkg b/advent.ipkg index 56f6e75..e8aff07 100644 --- a/advent.ipkg +++ b/advent.ipkg @@ -32,6 +32,7 @@ modules = Runner , Array , Parser , Parser.Interface + , Parser.Numbers -- main file (i.e. file to load at REPL) main = Main diff --git a/src/Parser/Numbers.md b/src/Parser/Numbers.md new file mode 100644 index 0000000..e7adbf8 --- /dev/null +++ b/src/Parser/Numbers.md @@ -0,0 +1,257 @@ +# Numerical Parsers + +```idris +module Parser.Numbers + +import public Parser + +import Data.Vect +import Control.Eff +``` + +```idris hide +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 <- 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 + +```idris +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 + +```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 <- 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 + +```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") +```