diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md index 7441ed6..c69ea2c 100644 --- a/src/Parser/JSON.md +++ b/src/Parser/JSON.md @@ -68,6 +68,16 @@ Show (JSONValue t) where show (VBool True) = "true" show VNull = "null" +Eq (JSONValue t) where + (VObject xs) == (VObject ys) = + assert_total $ xs $== ys + (VArray xs) == (VArray ys) = + assert_total $ xs $== ys + (VString s) == (VString str) = s == str + (VNumber d) == (VNumber dbl) = d == dbl + (VBool b) == (VBool x) = b == x + VNull == VNull = True + %hide Language.Reflection.TT.WithFC.value --> @@ -242,12 +252,30 @@ quickSmoke : IO Bool quickSmoke = do let input = "{\"string\":\"string\",\"number\":5,\"true\":true,\"false\":false,\"null\":null,\"array\":[1,2,3]}" putStrLn input - Right parsed <- runFirstIO object input + Right (type ** parsed) <- runFirstIO value input | Left err => do printLn err pure False - putStrLn "Input: \{input}\nOutput: \{show parsed}" + putStrLn "Input: \{input}\nOutput: \{show type} -> \{show parsed}" case parsed of - VObject xs => ?quickSmoke_rhs_0 + VObject {types} xs => do + putStrLn "Output types: \{show types}" + case decEq types [TString, TNumber, TBool, TBool, TNull, TArray] of + No contra => pure False + Yes Refl => case xs of + [ ("string", str) + , ("number", num) + , ("true", bool_t) + , ("false", bool_f) + , ("null", nul) + , ("array", arr) + ] => pure $ + str == VString "string" + && num == VNumber 5.0 + && bool_t == VBool True + && bool_f == VBool False + && nul == VNull + && arr == VArray [VNumber 1.0, VNumber 2.0, VNumber 3.0] + _ => pure False _ => pure False ```