json: oneOfM refactor

This commit is contained in:
Nathan McCarty 2025-01-25 13:37:20 -05:00
parent aa1ae93165
commit 77dcc4d953

View file

@ -122,8 +122,7 @@ export
value : Parser (t : JSONType ** JSONValue t) value : Parser (t : JSONType ** JSONValue t)
value = do value = do
surround whitespace $ oneOfE surround whitespace $ oneOfE
(throwParseError "Expected JSON Value") "Expected JSON Value"
(the (List _)
[ [
dpairize object dpairize object
, dpairize array , dpairize array
@ -131,7 +130,7 @@ value = do
, dpairize number , dpairize number
, dpairize bool , dpairize bool
, dpairize null , dpairize null
]) ]
``` ```
Now go through our json value types Now go through our json value types
@ -139,8 +138,8 @@ Now go through our json value types
```idris ```idris
object = do object = do
oneOfE oneOfE
(throwParseError "Expected Object") "Expected Object"
(the (List _) [emptyObject, occupiedObject]) [emptyObject, occupiedObject]
where where
emptyObject : Parser (JSONValue TObject) emptyObject : Parser (JSONValue TObject)
emptyObject = do emptyObject = do
@ -171,8 +170,8 @@ object = do
```idris ```idris
array = do array = do
oneOfE oneOfE
(throwParseError "Expected Array") "Expected Array"
(the (List _) [emptyArray, occupiedArray]) [emptyArray, occupiedArray]
where where
emptyArray : Parser (JSONValue TArray) emptyArray : Parser (JSONValue TArray)
emptyArray = do emptyArray = do
@ -214,8 +213,8 @@ number = do
```idris ```idris
bool = do bool = do
oneOfE oneOfE
(throwParseError "Expected Bool") "Expected Bool"
(the (List _) [true, false]) [true, false]
where where
true : Parser (JSONValue TBool) true : Parser (JSONValue TBool)
true = do true = do