numbers: Double Parser

README.md

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

advent.ipkg

@@ -19,7 +19,6 @@ depends = base
         , tailrec
         , eff
         , elab-util
-        , sop
         , ansi
         , if-unsolved-implicit
         , c-ffi
@@ -34,7 +33,6 @@ modules = Runner
         , Parser
         , Parser.Interface
         , Parser.Numbers
-        , Parser.JSON
 
 -- main file (i.e. file to load at REPL)
 main = Main

src/Parser/Interface.md

@@ -235,20 +235,6 @@ parseTheseChars cs = do
     EndOfInput => throwParseError "End of input"
 ```
 
-Attempt to parse an exact string
-
-```idris
-exactString : String -> Parser String
-exactString str with (asList str)
-  exactString "" | [] = pure ""
-  exactString input@(strCons c str) | (c :: x) = do
-    GotChar next <- parseChar (== c) id
-      | GotError err => throwParseError "Got \{show err} expected \{show c}"
-      | EndOfInput => throwParseError "End of input"
-    rest <- exactString str | x
-    pure input
-```
-
 ### Composition of boolean functions
 
 ```idris

src/Parser/JSON.md

@@ -1,211 +0,0 @@
-# JSON Parser
-
-```idris
-module Parser.JSON
-
-import public Parser
-import public Parser.Numbers
-
-import Structures.Dependent.DList
-```
-
-<!-- idris
-import System
-import Derive.Prelude
-import Generics.Derive
-
-%hide Generics.Derive.Eq
-%hide Generics.Derive.Ord
-%hide Generics.Derive.Show
-
-%language ElabReflection
--->
-
-## JSON components
-
-Types a JSON value is allowed to have
-
-```idris
-public export
-data JSONType : Type where
-  TObject : JSONType
-  TArray : JSONType
-  TString : JSONType
-  TNumber : JSONType
-  TBool : JSONType
-  TNull : JSONType
-%runElab derive "JSONType" [Generic, Meta, Eq, Ord, Show, DecEq]
-%name JSONType type, type2, type3
-```
-
-A JSON value indexed by its type
-
-```idris
-public export
-data JSONValue : JSONType -> Type where
-  VObject : {types : List JSONType} 
-    -> DList JSONType (\t => (String, JSONValue t)) types -> JSONValue TObject
-  VArray : {types : List JSONType}
-    -> DList JSONType JSONValue types -> JSONValue TArray
-  VString : (s : String) -> JSONValue TString
-  VNumber : (d : Double) -> JSONValue TNumber
-  VBool : (b : Bool) -> JSONValue TBool
-  VNull : JSONValue TNull
-%name JSONValue value, value2, value3
-```
-
-<!-- idris
-Show (JSONValue t) where
-  show (VObject xs) = 
-    let xs = dMap (\_,(key, value) => "\"\{key}\":\{show value}") xs
-    in assert_total $ "{\{joinBy "," xs}}"
-  show (VArray xs) = 
-    let xs = dMap (\_,e => show e) xs
-    in assert_total $ "[\{joinBy "," . map show $ xs}]"
-  show (VString s) = "\"\{s}\""
-  show (VNumber d) = show d
-  show (VBool False) = "false"
-  show (VBool True) = "true"
-  show VNull = "null"
-
-%hide Language.Reflection.TT.WithFC.value
--->
-
-## Parsers
-
-We are going to get mutually recursive here. Instead of using a `mutual` block,
-we will use the more modern style of declaring all our types ahead of our
-definitions.
-
-```idris
-export
-object : Parser (JSONValue TObject)
-export
-array : Parser (JSONValue TArray)
-export
-string : Parser (JSONValue TString)
-export
-number : Parser (JSONValue TNumber)
-export
-bool : Parser (JSONValue TBool)
-export
-null : Parser (JSONValue TNull)
-```
-
-Define a `whitespace` character class based on the json specifications
-
-```idris
-whitespace : Parser Char
-whitespace = do
-  result <- 
-    parseChar (\x => any (== x) $ the (List _) [' ', '\n', '\r', '\t']) id
-  case result of
-    GotChar char => pure char
-    GotError err => throwParseError "Expected whitespace, got: \{show err}"
-    EndOfInput => throwParseError "End of Input"
-```
-
-Convenience function
-
-```idris
-dpairize : {t : JSONType} -> 
-  Parser (JSONValue t) -> Parser (t' : JSONType ** JSONValue t')
-dpairize x = do
-  x <- x
-  pure (_ ** x)
-```
-
-Top level json value parser
-
-```idris
-export 
-value : Parser (t : JSONType ** JSONValue t)
-value = do 
-  _ <- many whitespace
-  val <- oneOfE 
-    (throwParseError "Expected JSON Value") 
-    (the (List _) 
-      [
-        dpairize object
-      , dpairize array
-      , dpairize string
-      , dpairize number
-      , dpairize bool
-      , dpairize null
-      ])
-  _ <- many whitespace
-  pure val
-```
-
-Now go through our json value types
-
-```idris
-object = do
-  oneOfE 
-    (throwParseError "Expected Object") 
-    (the (List _) [emptyObject, occupiedObject])
-  where
-    emptyObject : Parser (JSONValue TObject)
-    emptyObject = do
-      _ <- parseExactChar '{'
-      _ <- many whitespace
-      _ <- parseExactChar '}'
-      pure $ VObject Nil
-    firstKeyValue : Parser (t : JSONType ** (String, JSONValue t))
-    firstKeyValue = do
-      _ <- many whitespace
-      VString key <- string
-      _ <- many whitespace
-      _ <- parseExactChar ':'
-      (typ ** val) <- value
-      pure (typ ** (key, val))
-    restKeyValue : Parser (t : JSONType ** (String, JSONValue t))
-    restKeyValue = do
-      _ <- parseExactChar ','
-      firstKeyValue
-    occupiedObject : Parser (JSONValue TObject)
-    occupiedObject = do
-      _ <- parseExactChar '{'
-      first <- firstKeyValue
-      rest <- many restKeyValue
-      _ <- parseExactChar '}'
-      let (types ** xs) = DList.fromList (first :: rest)
-      pure $ VObject xs
-```
-
-```idris
-array = do
-  oneOfE 
-    (throwParseError "Expected Array") 
-    (the (List _) [emptyArray, occupiedArray])
-  where
-    emptyArray : Parser (JSONValue TArray)
-    emptyArray = do
-      _ <- parseExactChar '['
-      _ <- many whitespace
-      _ <- parseExactChar ']'
-      pure $ VArray Nil
-    restValue : Parser (t : JSONType ** JSONValue t)
-    restValue = do
-      _ <- parseExactChar ','
-      value
-    occupiedArray : Parser (JSONValue TArray)
-    occupiedArray = do
-      _ <- parseExactChar '['
-      first <- value
-      rest <- many restValue
-      _ <- parseExactChar ']'
-      let (types ** xs) = DList.fromList (first :: rest)
-      pure $ VArray xs
-```
-
-```idris
-string = do
-  _ <- parseExactChar '"'
-  -- TODO: Handle control characters properly
-  e1 <- parseError "Expected non-quote, got quote"
-  e2 <- parseError "End of input"
-  contents <- parseString . many $ parseCharE (not . (== '"')) (\_ => e1) e2
-  _ <- parseExactChar '"'
-  pure $ VString contents
-```

src/Parser/Numbers.md

@@ -96,10 +96,9 @@ integerBase10 = integer base10
 ### Double
 
 ```idris
--- TODO: Replicate `parseDouble` logic and make this base-generic
 export
-double : Parser Double
+double : Base -> Parser Double
-double = do
+double b = do
   starting_state <- save
   integer <- integer
   fraction <- tryMaybe fraction
@@ -120,7 +119,7 @@ double = do
   where
     parseDigit : Parser Char
     parseDigit = do
-      GotChar char <- parseChar (hasDigit base10) id
+      GotChar char <- parseChar (hasDigit b) id
         | GotError e => throwParseError "\{show e} is not a digit"
         | EndOfInput => throwParseError "End Of Input"
       pure char
@@ -145,6 +144,10 @@ double = do
       error <- replaceError "Expected digit"
       digits <- map forget $ atLeastOne error parseDigit
       pure . pack $ sign :: digits
+
+export
+doubleBase10 : Parser Double
+doubleBase10 = double base10
 ```
 
 ## Unit tests
@@ -212,7 +215,7 @@ compareDouble string = do
       putStrLn "Failed to produce parser for \{string}"
       pure False
   Right result <- 
-    runEff (rundownFirst double) [handleParserStateIO state] {m = IO}
+    runEff (rundownFirst doubleBase10) [handleParserStateIO state] {m = IO}
     | Left err => do
       printLn err
       pure False