diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md index 1f2377c..1b08b12 100644 --- a/src/Parser/JSON.md +++ b/src/Parser/JSON.md @@ -5,8 +5,92 @@ module Parser.JSON import public Parser import public Parser.Numbers + +import Structures.Dependent.DList ``` + +## 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 +``` + + + +## 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) +```