0 | ||| The interfaces in this module abstract over how we
  1 | ||| encode and decode values from and to JSON.
  2 | |||
  3 | ||| This allows us to use different (probably backend dependant)
  4 | ||| intermediary data representations to be used by the actual
  5 | ||| marshallers `ToJSON` and `FromJSON`.
  6 | module JSON.Encoder
  7 |
  8 | import Data.List
  9 | import Data.Vect
 10 | import public JSON.Parser
 11 |
 12 | --------------------------------------------------------------------------------
 13 | --          Encoding
 14 | --------------------------------------------------------------------------------
 15 |
 16 | ||| Abstraction over JSON value encoding.
 17 | public export
 18 | interface Encoder v where
 19 |   ||| Converts the intermediary data representation
 20 |   ||| to a JSON string.
 21 |   stringify : v -> String
 22 |
 23 |   ||| Encodes a `String` value.
 24 |   string : String -> v
 25 |
 26 |   ||| Encodes a `Double` as a JSON `Double`.
 27 |   double : Double -> v
 28 |
 29 |   ||| Encodes a `Double` as a JSON `Integer`.
 30 |   integer : Integer -> v
 31 |
 32 |   ||| Encodes a `Bool` as a JSON `Boolean`.
 33 |   boolean : Bool -> v
 34 |
 35 |   ||| Encodes a `List` of values as a JSON `Array`.
 36 |   array : List v -> v
 37 |
 38 |   ||| Encodes a `List` key-value pairs as a JSON `Object`
 39 |   object : List (String,v) -> v
 40 |
 41 |   null : v
 42 |
 43 | --------------------------------------------------------------------------------
 44 | --          Decoding
 45 | --------------------------------------------------------------------------------
 46 |
 47 | ||| Abstraction over JSON Object representation for decoding.
 48 | ||| It is important that `obj` is the type that guides interface
 49 | ||| resolution here, otherwise operators like `.:` cannot conveniently
 50 | ||| be used, since Idris needs additional guidance to resolve interfaces.
 51 | public export
 52 | interface Object obj v | obj where
 53 |   lookup : String -> obj -> Maybe v
 54 |   pairs  : obj -> List (String,v)
 55 |
 56 | ||| Abstraction over JSON value representation for decoding.
 57 | public export
 58 | interface Object obj v => Value v obj | v where
 59 |   ||| Returns the actual value. This should be one of
 60 |   ||| "String", "Null", "Object", "Number", "Boolean", or "Array".
 61 |   ||| However, other types are possible as well, as this is
 62 |   ||| only used for error messages when something goes wrong.
 63 |   typeOf : v -> String
 64 |
 65 |   ||| Tries to convert a string to an intermediare value.
 66 |   parse : Origin -> String -> Either (ParseError Void) v
 67 |
 68 |   ||| Tries to convert a value to an `Object`.
 69 |   getObject : v -> Maybe obj
 70 |
 71 |   ||| Tries to convert a value to an `Array` of values.
 72 |   getArray : v -> Maybe (List v)
 73 |
 74 |   ||| Tries to convert a value to a `Boolean`.
 75 |   getBoolean : v -> Maybe Bool
 76 |
 77 |   ||| Tries to convert a value to a `Double`.
 78 |   getDouble : v -> Maybe Double
 79 |
 80 |   ||| Tries to convert a value to an `Integer`.
 81 |   getInteger : v -> Maybe Integer
 82 |
 83 |   ||| Tries to convert a value to a `String`.
 84 |   getString : v -> Maybe String
 85 |
 86 |   ||| `True`, if the value in question is `null`.
 87 |   isNull : v -> Bool
 88 |
 89 | public export
 90 | getArrayN : Value v obj => (n : Nat) -> v -> Maybe (Vect n v)
 91 | getArrayN n x = getArray x >>= toVect n
 92 |
 93 | --------------------------------------------------------------------------------
 94 | --          Implementations
 95 | --------------------------------------------------------------------------------
 96 |
 97 | export %inline
 98 | Encoder JSON where
 99 |   stringify = show
100 |   string    = JString
101 |   double    = JDouble
102 |   integer   = JInteger
103 |   boolean   = JBool
104 |   null      = JNull
105 |   array     = JArray
106 |   object    = JObject
107 |
108 | export %inline
109 | Object (List (String,JSON)) JSON where
110 |   lookup = Data.List.lookup
111 |   pairs = id
112 |
113 | export %inline
114 | Value JSON (List (String,JSON)) where
115 |   parse     = parseJSON
116 |
117 |   typeOf JNull        = "Null"
118 |   typeOf (JBool _)    = "Boolean"
119 |   typeOf (JDouble _)  = "Double"
120 |   typeOf (JInteger _)  = "Integer"
121 |   typeOf (JString _)  = "String"
122 |   typeOf (JArray _)   = "Array"
123 |   typeOf (JObject _)  = "Object"
124 |
125 |   getObject (JObject ps) = Just ps
126 |   getObject _            = Nothing
127 |
128 |   getDouble (JDouble v)  = Just v
129 |   getDouble (JInteger v) = Just (cast v)
130 |   getDouble _            = Nothing
131 |
132 |   getInteger (JInteger v) = Just v
133 |   getInteger _           = Nothing
134 |
135 |   getBoolean (JBool v)  = Just v
136 |   getBoolean _            = Nothing
137 |
138 |   getArray (JArray v) = Just v
139 |   getArray _          = Nothing
140 |
141 |   getString (JString v) = Just v
142 |   getString _           = Nothing
143 |
144 |   isNull JNull = True
145 |   isNull _     = False
146 |