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