git.iko.soy/Idris-dev
on 2aa64bd help sign in
Idris-dev/javascript/JavaScript/JSON.idr
46 lines 1.5 kB history raw
1module JSON
3import Data.SortedMap
5data JSONType : Type where
6 JSONArray : (n : Nat) -> Vect n JSONType -> JSONType
7 JSONString : JSONType
8 JSONNumber : JSONType
9 JSONBool : JSONType
10 JSONObject : SortedMap String JSONType -> JSONType
11 JSONNull : JSONType
13mutual
14 using (ts : Vect n JSONType, fs : SortedMap String JSONType)
15 namespace JArray
16 data JArray : (n : Nat) -> Vect n JSONType -> Type where
17 Nil : JArray 0 []
18 (::) : JSON t -> JArray n ts -> JArray (S n) (t :: ts)
20 namespace JObject
21 data JObject : SortedMap String JSONType -> Type where
22 Nil : JObject empty
23 (::) : (f : (String, JSON t)) ->
24 JObject fs ->
25 JObject (insert (fst f) t fs)
27 data JSON : JSONType -> Type where
28 JSString : String -> JSON JSONString
29 JSNumber : Float -> JSON JSONNumber
30 JSBool : Bool -> JSON JSONBool
31 JSNull : JSON JSONNull
32 JSArray : JArray n ts -> JSON (JSONArray n ts)
33 JSObject : JObject fs -> JSON (JSONObject fs)
35index : (i : Fin n) -> JSON (JSONArray n ts) -> JSON (index i ts)
36index fZ (JSArray (x :: xs)) = x
37index (fS i) (JSArray (x :: xs)) = index i (JSArray xs)
39infixl 8 ++
41(++) : JSON (JSONArray m ts1) ->
42 JSON (JSONArray n ts2) ->
43 JSON (JSONArray (m + n) (ts1 ++ ts2))
44(++) (JSArray []) ys = ys
45(++) (JSArray (x :: xs)) ys with ((JSArray xs) ++ ys)
46 | (JSArray as) = JSArray (x :: as)