
   0 | ||| Interface and utilities for encoding Idris2 values to JSON
   1 | ||| via an entermediate `Value` representation.
   2 | |||
   3 | ||| For regular algebraic data types, implementations can automatically
   4 | ||| be derived using elaborator reflection (see module `Derive.ToJSON`)
   5 | |||
   6 | ||| Operators and functionality strongly influenced by Haskell's aeson
   7 | ||| library
   8 | module JSON.Simple.ToJSON
   9 | 
  10 | import Data.List.Quantifiers as LQ
  11 | import Data.List1
  12 | import Data.Singleton
  13 | import Data.SortedMap
  14 | import Data.String
  15 | import Data.Vect
  16 | import Data.Vect.Quantifiers as VQ
  17 | import JSON.Parser
  18 | import JSON.Simple.Option
  19 | 
  20 | ||| Interface for encoding an Idris value as a JSON value.
  21 | public export
  22 | interface ToJSON a where
  23 |   constructor MkToJSON
  24 |   toJSON : a -> JSON
  25 | 
  26 | ||| Interface for encoding an Idris value as a key in a JSON object
  27 | public export
  28 | interface ToJSONKey a where
  29 |   constructor MkToJSONKey
  30 |   toKey : a -> String
  31 | 
  32 | export %inline
  33 | jpair : ToJSONKey k => ToJSON a => k -> a -> (String,JSON)
  34 | jpair s val = (toKey s, toJSON val)
  35 | 
  36 | export %inline
  37 | encode : ToJSON a => a -> String
  38 | encode = show . toJSON
  39 | 
  40 | ||| Encodes a value as a single-field object. The field has the given
  41 | ||| name.
  42 | |||
  43 | ||| This corresponds to the `ObjectWithSingleField` option
  44 | ||| for encoding sum types.
  45 | export %inline
  46 | singleField : String -> JSON -> JSON
  47 | singleField s x = JObject [(s,x)]
  48 | 
  49 | ||| Encodes a value plus a string as a two-element array.
  50 | |||
  51 | ||| This corresponds to the `TwoElemArray` option
  52 | ||| for encoding sum types.
  53 | export %inline
  54 | twoElemArray : String -> JSON -> JSON
  55 | twoElemArray s x = JArray [JString s, x]
  56 | 
  57 | ||| Encodes a value plus a string as a tagged object.
  58 | |||
  59 | ||| This corresponds to the `TaggedObject` option
  60 | ||| for encoding sum types.
  61 | export
  62 | taggedObject : (tagField, contentField, tag : String) -> JSON -> JSON
  63 | taggedObject tf cf tag x = JObject [(tf, JString tag), (cf, x)]
  64 | 
  65 | --------------------------------------------------------------------------------
  66 | --          Implementations
  67 | --------------------------------------------------------------------------------
  68 | 
  69 | export
  70 | ToJSON JSON where toJSON = id
  71 | 
  72 | export
  73 | ToJSON Void where
  74 |   toJSON x impossible
  75 | 
  76 | export %inline
  77 | ToJSON String where toJSON = JString
  78 | 
  79 | export %inline
  80 | ToJSONKey String where toKey = id
  81 | 
  82 | export %inline
  83 | ToJSON Char where toJSON = JString . singleton
  84 | 
  85 | export %inline
  86 | ToJSONKey Char where toKey = singleton
  87 | 
  88 | export %inline
  89 | ToJSON Double where toJSON = JDouble
  90 | 
  91 | export %inline
  92 | ToJSON Bits8 where toJSON = JInteger . cast
  93 | 
  94 | export %inline
  95 | ToJSON Bits16 where toJSON = JInteger . cast
  96 | 
  97 | export %inline
  98 | ToJSON Bits32 where toJSON = JInteger . cast
  99 | 
 100 | export %inline
 101 | ToJSON Bits64 where toJSON = JInteger . cast
 102 | 
 103 | export %inline
 104 | ToJSON Int8 where toJSON = JInteger . cast
 105 | 
 106 | export %inline
 107 | ToJSON Int16 where toJSON = JInteger . cast
 108 | 
 109 | export %inline
 110 | ToJSON Int32 where toJSON = JInteger . cast
 111 | 
 112 | export %inline
 113 | ToJSON Int64 where toJSON = JInteger . cast
 114 | 
 115 | export %inline
 116 | ToJSON Int where toJSON = JInteger . cast
 117 | 
 118 | export %inline
 119 | ToJSON Integer where toJSON = JInteger
 120 | 
 121 | export %inline
 122 | ToJSON Nat where toJSON = JInteger . cast
 123 | 
 124 | export %inline
 125 | ToJSON Bool where toJSON = JBool
 126 | 
 127 | export %inline
 128 | ToJSONKey Double where toKey = cast
 129 | 
 130 | export %inline
 131 | ToJSONKey Bits8 where toKey = cast
 132 | 
 133 | export %inline
 134 | ToJSONKey Bits16 where toKey = cast
 135 | 
 136 | export %inline
 137 | ToJSONKey Bits32 where toKey = cast
 138 | 
 139 | export %inline
 140 | ToJSONKey Bits64 where toKey = cast
 141 | 
 142 | export %inline
 143 | ToJSONKey Int8 where toKey = cast
 144 | 
 145 | export %inline
 146 | ToJSONKey Int16 where toKey = cast
 147 | 
 148 | export %inline
 149 | ToJSONKey Int32 where toKey = cast
 150 | 
 151 | export %inline
 152 | ToJSONKey Int64 where toKey = cast
 153 | 
 154 | export %inline
 155 | ToJSONKey Int where toKey = cast
 156 | 
 157 | export %inline
 158 | ToJSONKey Integer where toKey = cast
 159 | 
 160 | export %inline
 161 | ToJSONKey Nat where toKey = cast
 162 | 
 163 | export %inline
 164 | ToJSONKey Bool where toKey = show
 165 | 
 166 | export
 167 | ToJSON a => ToJSON (Maybe a) where
 168 |   toJSON Nothing  = JNull
 169 |   toJSON (Just a) = toJSON a
 170 | 
 171 | export
 172 | ToJSON a => ToJSON (List a) where
 173 |   toJSON = JArray . map toJSON
 174 | 
 175 | export
 176 | ToJSON a => ToJSON (SnocList a) where
 177 |   toJSON = toJSON . (<>> [])
 178 | 
 179 | export
 180 | ToJSON a => ToJSON (List1 a) where
 181 |   toJSON = toJSON . forget
 182 | 
 183 | export
 184 | ToJSON a => ToJSON (Vect n a) where
 185 |   toJSON = toJSON . toList
 186 | 
 187 | export
 188 | ToJSON () where
 189 |   toJSON () = JArray Nil
 190 | 
 191 | export
 192 | ToJSON a => ToJSON b => ToJSON (Either a b) where
 193 |   toJSON (Left a)  = JObject [jpair "Left"  a]
 194 |   toJSON (Right b) = JObject [jpair "Right" b]
 195 | 
 196 | export
 197 | ToJSON a => ToJSON b => ToJSON (a, b) where
 198 |   toJSON (x,y) = JArray [toJSON x, toJSON y]
 199 | 
 200 | export
 201 | (ps : LQ.All.All (ToJSON . f) ts) => ToJSON (All f ts) where
 202 |   toJSON = JArray . forget . zipPropertyWith (\_,v => toJSON v) ps
 203 | 
 204 | export
 205 | ToJSONKey k => ToJSON v => ToJSON (SortedMap k v) where
 206 |   toJSON = JObject . map (uncurry jpair) . SortedMap.toList
 207 | 
 208 | export
 209 | zipAllWith :
 210 |      (f : {0 x : a} -> p x -> q x -> r x)
 211 |   -> VQ.All.All p xs
 212 |   -> All q xs
 213 |   -> All r xs
 214 | zipAllWith f [] [] = []
 215 | zipAllWith f (px :: pxs) (qx :: qxs) = f px qx :: zipAllWith f pxs qxs
 216 | 
 217 | export
 218 | (ps : VQ.All.All (ToJSON . f) ts) => ToJSON (VQ.All.All f ts) where
 219 |   toJSON = JArray . toList . forget . zipAllWith (\_,v => toJSON v) ps
 220 | 
 221 | export %inline
 222 | {v : a} -> ToJSON a => ToJSON (Singleton v) where
 223 |   toJSON _ = toJSON v
 224 |