# 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) 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

```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) id
        | 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") 
```