README.md

@@ -68,10 +68,6 @@ solution.
 
     Internal state of a parser
 
-  - [ParserState](src/Parser/ParserState.md)
-
-    Parsers for numerical values in multiple bases
-
 ## Index of years and days
 
 - 2015

advent.ipkg

@@ -32,7 +32,6 @@ modules = Runner
         , Array
         , Parser
         , Parser.Interface
-        , Parser.Numbers
 
 -- main file (i.e. file to load at REPL)
 main = Main

src/Parser/Interface.md

@@ -19,9 +19,10 @@ Combine the parser state at time of error with an error message.
 
 ```idris
 public export
-data ParseError : Type where
+record ParseError where
-  MkParseError : (state : ParserInternal Id) -> (message : String) -> ParseError
+  constructor MkParseError
-  BeforeParse : (message : String) -> ParseError
+  state : ParserInternal Id
+  message : String
 ```
 
 <!-- idris
@@ -32,8 +33,6 @@ Show ParseError where
         (line, col) = (show line, show col)
         position = show state.position.index
     in "Error at line \{line}, column \{col} (\{position}): \{message}"
-  show (BeforeParse message) =
-    "Error before parsing: \{message}"
 -->
 
 ## Type Alias
@@ -96,29 +95,6 @@ rundownFirst f =
   runExcept . guardMaybe "No returning parses" . runChoose {f = Maybe} $ f
 ```
 
-Provide wrappers for `rundownFirst` for evaluating it in various contexts.
-
-```idris
-export
-runFirstIO : (f : Parser a) -> String -> IO (Either ParseError a)
-runFirstIO f str = do
-  Just state <- newInternalIO str
-    | _ => pure . Left $ BeforeParse "Empty input"
-  runEff (rundownFirst f) [handleParserStateIO state]
-
-export
-runFirst : (f : Parser a) -> String -> Eff fs (Either ParseError a)
-runFirst f str = do
-  Just state <- pure $ newInternal str
-    | _ => pure . Left $ BeforeParse "Empty input"
-  (result, _) <- lift . runParserState state . rundownFirst $ f
-  pure result
-
-export
-runFirst' : (f : Parser a) -> String -> Either ParseError a
-runFirst' f str = extract $ runFirst f str {fs = []}
-```
-
 ## Utility functionality
 
 ### Parser combinators
@@ -209,32 +185,6 @@ parseString' : Parser (List1 Char) -> Parser String
 parseString' x = parseString $ map forget x
 ```
 
-Attempt to parse a specified character
-
-```idris
-export
-parseExactChar : Char -> Parser Char
-parseExactChar c = do
-  result <- parseChar (== c) id
-  case result of
-    GotChar char => pure char
-    GotError err => throwParseError "Got \{show err} Expected \{show c}"
-    EndOfInput => throwParseError "End of input"
-```
-
-Attempt to parse one of a list of chars
-
-```idris
-export
-parseTheseChars : List Char -> Parser Char
-parseTheseChars cs = do
-  result <- parseChar (\x => any (== x) cs) id
-  case result of
-    GotChar char => pure char
-    GotError err => throwParseError "Got \{show err} Expected one of \{show cs}"
-    EndOfInput => throwParseError "End of input"
-```
-
 ### Composition of boolean functions
 
 ```idris

src/Parser/Numbers.md

@@ -1,260 +0,0 @@
-# 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
-export
-double : Base -> Parser Double
-double b = 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 b) 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
-
-export
-doubleBase10 : Parser Double
-doubleBase10 = double base10
-```
-
-## 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 doubleBase10) [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") 
-```

src/Parser/ParserState.md

@@ -281,36 +281,6 @@ newInternalIO str = do
   map Just $ newIORef internal
 ```
 
-### State context
-
-```idris
-unPS : ParserInternal Id -> ParserState a -> (a, ParserInternal Id)
-unPS pi Save = (pi, pi)
-unPS pi (Load pj) = ((), pi)
-unPS pi (ParseChar predicate err) = 
-  if pi.end_of_input
-    then (EndOfInput, pi)
-    else let
-      char = assert_total $ strIndex pi.input (cast pi.position.index)
-    in if predicate char
-      then case refine0 (pi.position.index + 1) {p = IsIndex pi.length} of
-        Nothing => 
-          (GotChar char, {end_of_input := True} pi)
-        Just (Element next _) => 
-          (GotChar char, {position := MkIndex next} pi)
-      else (GotError $ err char, pi)
-unPS pi ParseEoF = (pi.end_of_input, pi)
-
-export
-runParserState : Has ParserState fs => 
-  (s : ParserInternal Id) -> Eff fs t 
-  -> Eff (fs - ParserState) (t, ParserInternal Id)
-runParserState s = 
-  handleRelayS s (\x, y => pure (y, x)) $ \s2,ps,f =>
-    let (a, st) = unPS s2 ps 
-    in f st a
-```
-
 ## Footnotes
 
 [^1]: https://github.com/stefan-hoeck/idris2-barbies