diff --git a/src/Parser/Numbers.md b/src/Parser/Numbers.md index aa0e156..195570f 100644 --- a/src/Parser/Numbers.md +++ b/src/Parser/Numbers.md @@ -51,7 +51,11 @@ hex = MkBase 16 ```idris export -nat : Parser Nat +nat : Base -> Parser Nat + +export +natBase10 : Parser Nat +natBase10 = nat base10 ``` ## Unit tests @@ -68,7 +72,24 @@ roundtrip x p = do putStrLn "Failed to produce parser for \{string}" pure False Right result <- runEff (rundownFirst p) [handleParserStateIO state] {m = IO} - | Left err => ?show_err + | 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) +```