
   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.ToJSON
   9 | 
  10 | import Data.List.Quantifiers as LQ
  11 | import Data.Vect.Quantifiers as VQ
  12 | import Data.SortedMap
  13 | import Data.List1
  14 | import Data.String
  15 | import Data.Vect
  16 | import JSON.Option
  17 | import JSON.Encoder
  18 | 
  19 | public export
  20 | interface ToJSON a where
  21 |   constructor MkToJSON
  22 |   toJSON : forall v . Encoder v => a -> v
  23 | 
  24 | export %inline
  25 | jpair : ToJSON a => Encoder v => String -> a -> (String,v)
  26 | jpair s val = (s, toJSON val)
  27 | 
  28 | export infixr 8 .=
  29 | 
  30 | ||| Deprecated: Use `jpair` instead
  31 | export %deprecate %inline
  32 | (.=) : ToJSON a => Encoder v => String -> a -> (String,v)
  33 | (.=) = jpair
  34 | 
  35 | export
  36 | encodeVia : (0 v : Type) -> Encoder v => ToJSON a => a -> String
  37 | encodeVia v val = stringify $ toJSON {v} val
  38 | 
  39 | export
  40 | encode : ToJSON a => a -> String
  41 | encode = encodeVia JSON
  42 | 
  43 | ||| Encodes a value as a single-field object. The field has the given
  44 | ||| name.
  45 | |||
  46 | ||| This corresponds to the `ObjectWithSingleField` option
  47 | ||| for encoding sum types.
  48 | export
  49 | singleField : Encoder v => String -> v -> v
  50 | singleField s x = object [(s,x)]
  51 | 
  52 | ||| Encodes a value plus a string as a two-element array.
  53 | |||
  54 | ||| This corresponds to the `TwoElemArray` option
  55 | ||| for encoding sum types.
  56 | export
  57 | twoElemArray : Encoder v => String -> v -> v
  58 | twoElemArray s x = array [string s, x]
  59 | 
  60 | ||| Encodes a value plus a string as a tagged object.
  61 | |||
  62 | ||| This corresponds to the `TaggedObject` option
  63 | ||| for encoding sum types.
  64 | export
  65 | taggedObject :
  66 |      {auto _ : Encoder v}
  67 |   -> (tagField, contentField, tag : String)
  68 |   -> v
  69 |   -> v
  70 | taggedObject tf cf tag x = object [(tf, string tag), (cf, x)]
  71 | 
  72 | --------------------------------------------------------------------------------
  73 | --          Implementations
  74 | --------------------------------------------------------------------------------
  75 | 
  76 | export
  77 | ToJSON Void where
  78 |   toJSON x impossible
  79 | 
  80 | export
  81 | ToJSON String where toJSON = string
  82 | 
  83 | export
  84 | ToJSON Char where toJSON = string . singleton
  85 | 
  86 | export
  87 | ToJSON Double where toJSON = double
  88 | 
  89 | export
  90 | ToJSON Bits8 where toJSON = integer . cast
  91 | 
  92 | export
  93 | ToJSON Bits16 where toJSON = integer . cast
  94 | 
  95 | export
  96 | ToJSON Bits32 where toJSON = integer . cast
  97 | 
  98 | export
  99 | ToJSON Bits64 where toJSON = integer . cast
 100 | 
 101 | export
 102 | ToJSON Int8 where toJSON = integer . cast
 103 | 
 104 | export
 105 | ToJSON Int16 where toJSON = integer . cast
 106 | 
 107 | export
 108 | ToJSON Int32 where toJSON = integer . cast
 109 | 
 110 | export
 111 | ToJSON Int64 where toJSON = integer . cast
 112 | 
 113 | export
 114 | ToJSON Int where toJSON = integer . cast
 115 | 
 116 | export
 117 | ToJSON Integer where toJSON = integer
 118 | 
 119 | export
 120 | ToJSON Nat where toJSON = integer . cast
 121 | 
 122 | export
 123 | ToJSON Bool where toJSON = boolean
 124 | 
 125 | export
 126 | ToJSON a => ToJSON (Maybe a) where
 127 |   toJSON Nothing  = null
 128 |   toJSON (Just a) = toJSON a
 129 | 
 130 | export
 131 | ToJSON a => ToJSON (List a) where
 132 |   toJSON = array . map toJSON
 133 | 
 134 | export
 135 | ToJSON a => ToJSON (SnocList a) where
 136 |   toJSON = toJSON . (<>> [])
 137 | 
 138 | export
 139 | ToJSON a => ToJSON (List1 a) where
 140 |   toJSON = toJSON . forget
 141 | 
 142 | export
 143 | ToJSON a => ToJSON (Vect n a) where
 144 |   toJSON = toJSON . toList
 145 | 
 146 | export
 147 | ToJSON () where
 148 |   toJSON () = array Nil
 149 | 
 150 | export
 151 | ToJSON a => ToJSON b => ToJSON (Either a b) where
 152 |   toJSON (Left a)  = object [jpair "Left"  a]
 153 |   toJSON (Right b) = object [jpair "Right" b]
 154 | 
 155 | export
 156 | ToJSON a => ToJSON b => ToJSON (a, b) where
 157 |   toJSON (x,y) = array [toJSON x, toJSON y]
 158 | 
 159 | export
 160 | ToJSON a => ToJSON (SortedMap String a) where
 161 |   toJSON = object . map (\(key, val) => (key, toJSON {v} val)) . SortedMap.toList
 162 | 
 163 | export
 164 | (ps : LQ.All.All (ToJSON . f) ts) => ToJSON (All f ts) where
 165 |   toJSON = array . forget . zipPropertyWith (\_,v => toJSON v) ps
 166 | 
 167 | 
 168 | export
 169 | zipAllWith :
 170 |      (f : {0 x : a} -> p x -> q x -> r x)
 171 |   -> VQ.All.All p xs
 172 |   -> All q xs
 173 |   -> All r xs
 174 | zipAllWith f [] [] = []
 175 | zipAllWith f (px :: pxs) (qx :: qxs) = f px qx :: zipAllWith f pxs qxs
 176 | 
 177 | export
 178 | (ps : VQ.All.All (ToJSON . f) ts) => ToJSON (VQ.All.All f ts) where
 179 |   toJSON = array . toList . forget . zipAllWith (\_,v => toJSON v) ps
 180 |