@@ -0,0 +1,31 @@
1+module JSON
2+
3+import Data.SortedMap
4+
5+data JSONType : Type where
6+ JSONArray : Vect JSONType n -> JSONType
7+ JSONString : JSONType
8+ JSONNumber : JSONType
9+ JSONBool : JSONType
10+ JSONObject : SortedMap String JSONType -> JSONType
11+ JSONNull : JSONType
12+
13+mutual
14+ using (ts : Vect JSONType n, fs : SortedMap String JSONType)
15+ namespace JArray
16+ data JArray : Vect JSONType n -> Type where
17+ Nil : JArray []
18+ (::) : JSON t -> JArray ts -> JArray (t :: ts)
19+
20+ namespace JObject
21+ data JObject : SortedMap String JSONType -> Type where
22+ Nil : JObject empty
23+ (::) : (f : (String, JSON t)) -> JObject fs -> JObject (insert (fst f) t fs)
24+
25+ data JSON : JSONType -> Type where
26+ JSString : String -> JSON JSONString
27+ JSNumber : Float -> JSON JSONNumber
28+ JSBool : Bool -> JSON JSONBool
29+ JSNull : JSON JSONNull
30+ JSArray : JArray ts -> JSON (JSONArray ts)
31+ JSObject : JObject fs -> JSON (JSONObject fs)