advent/src/Parser/Numbers.md

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 <- 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
natBase10 : Parser Nat
natBase10 = nat base10

Integer

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

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)