
   0 | module Lana.JSON.Encoder
   1 | 
   2 | import Data.List.Elem
   3 | import Data.List.Elem.Extra as ElemExtra
   4 | import Data.List.Quantifiers
   5 | 
   6 | -- Transitive import bug. If these can be removed with no error during
   7 | -- compilation, the bug has been fixed in Idris2.
   8 | import Data.SortedMap as Map
   9 | import Data.Finite as Finite
  10 | 
  11 | import Lana.Class as LC
  12 | import Lana.Name as LC
  13 | import JSON.Encoder as JE
  14 | --import JSON.ToJSON
  15 | import JSON.Simple.ToJSON
  16 | import JSON.Parser as JP
  17 | 
  18 | export
  19 | EncodedJSON : Type -> Type
  20 | EncodedJSON a = JSON
  21 | 
  22 | export
  23 | forgetEncodedJSON : EncodedJSON a -> JSON
  24 | forgetEncodedJSON = id
  25 | 
  26 | export
  27 | data JEncoder a = MkJEncoder LC.Name (a -> EncodedJSON a)
  28 | 
  29 | -- Suspicious instance since it doesn't actually do anything
  30 | --Functor EncodedJSON where
  31 | --  map f json = json
  32 | 
  33 | -- Suspicious instance since it doesn't actually do anything
  34 | Functor JEncoder where
  35 |   map f jenc = assert_total $ idris_crash "todo"
  36 | 
  37 | Series : Type
  38 | Series = List (Pair String JSON)
  39 | 
  40 | export
  41 | encode : JEncoder a -> a -> EncodedJSON a
  42 | encode (MkJEncoder name toEncoding) = toEncoding
  43 | 
  44 | export
  45 | MyObject: Type -> Type -> Type
  46 | MyObject object constructor = (object -> Series)
  47 | 
  48 | MyField: Type -> Type -> Type
  49 | MyField object constructor = (object -> Series)
  50 | 
  51 | mkAdditional: (obj -> Map.SortedMap String a) -> (a -> EncodedJSON a) -> obj -> Series
  52 | mkAdditional accessor toEncoding anObj =
  53 |   let
  54 |     l : List (Pair String a)
  55 |     l = Map.toList (accessor anObj)
  56 |     fun : List (Pair String a) -> Series
  57 |     fun =
  58 |       concatMap
  59 |         (\(MkPair key value) => the Series [MkPair key (toEncoding value)])
  60 |   in fun l
  61 | 
  62 | mkUnionNamedFunctor : {fun: Type -> Type} -> Functor fun => {types: List Type} ->
  63 |   Any Prelude.Basics.id types ->
  64 |   ({el: Type} ->
  65 |     Elem el types ->
  66 |     el ->
  67 |     fun el) ->
  68 |   fun (Any Prelude.Basics.id types)
  69 | mkUnionNamedFunctor {types=[]} anyInEmpty g = absurd anyInEmpty
  70 | mkUnionNamedFunctor {types=(x :: xs)} anyInXOrXs g =
  71 |   case anyInXOrXs of
  72 |     Any.Here her =>
  73 |       map (Any.Here . id) $ g {el=x} Elem.Here (the x her)
  74 |     Any.There thr =>
  75 |       let xsPrf : fun (Any Prelude.Basics.id xs)
  76 |           xsPrf = mkUnionNamedFunctor {types=xs} thr $ \iElem, iEl => g (Elem.There iElem) iEl
  77 |        in map Any.There xsPrf
  78 | 
  79 | mkUnionNamed : {types: List Type} ->
  80 |   Any Prelude.Basics.id types ->
  81 |   ({el: Type} ->
  82 |     Elem el types ->
  83 |     el ->
  84 |     EncodedJSON el) ->
  85 |   EncodedJSON (Any Prelude.Basics.id types)
  86 | mkUnionNamed {types=[]} anyInEmpty g = absurd anyInEmpty
  87 | mkUnionNamed {types=(x :: xs)} anyInXOrXs g =
  88 |   case anyInXOrXs of
  89 |     Any.Here her =>
  90 |       g {el=x} Elem.Here (the x her)
  91 |     Any.There thr =>
  92 |       let xsPrf : EncodedJSON (Any Prelude.Basics.id xs)
  93 |           xsPrf = mkUnionNamed {types=xs} thr $ \iElem, iEl => g (Elem.There iElem) iEl
  94 |        in xsPrf
  95 | 
  96 | mkUnionMemberWithIndex : Elem a types ->
  97 |                          (a -> EncodedJSON a) ->
  98 |                          ({elem: Type} -> Elem elem [a] -> elem -> EncodedJSON elem)
  99 | mkUnionMemberWithIndex unusedAInTypes aEncoder Data.List.Elem.Here anElem = aEncoder anElem
 100 | 
 101 | mkUnionCombine :
 102 |     {left, right: List Type} ->
 103 |     ({elem: Type} -> Elem elem left  -> elem -> EncodedJSON elem) ->
 104 |     ({elem: Type} -> Elem elem right -> elem -> EncodedJSON elem) ->
 105 |     ({elem: Type} -> Elem elem (left ++ right) -> elem -> EncodedJSON elem)
 106 | mkUnionCombine encodeLeft encodeRight elemLeftRight elem =
 107 |   case ElemExtra.elemAppLorR left right elemLeftRight of
 108 |     Left inLeft => encodeLeft inLeft elem
 109 |     Right inRight => encodeRight inRight elem
 110 | 
 111 | export
 112 | implementation LC.Lana JEncoder where
 113 |   Object = MyObject
 114 | 
 115 |   Field = MyField
 116 | 
 117 |   AdditionalFields object constructor = (object -> Series)
 118 | 
 119 |   UnionMembers allTypes handledTypes
 120 |     = {elem: Type} -> Elem elem handledTypes -> elem -> EncodedJSON elem
 121 | 
 122 |   schemaName (MkJEncoder name toEncoding) =
 123 |     name
 124 | 
 125 |   double =
 126 |     MkJEncoder (LC.unqualifiedName "double") toJSON
 127 | 
 128 |   text =
 129 |     MkJEncoder (LC.unqualifiedName "text") toJSON
 130 | 
 131 |   boolean =
 132 |     MkJEncoder (LC.unqualifiedName "boolean") toJSON
 133 | 
 134 |   null =
 135 |     MkJEncoder
 136 |       (LC.unqualifiedName "null")
 137 |       (\LC.MkNull => JNull)
 138 | 
 139 |   array (MkJEncoder name itemToEncoding) =
 140 |     MkJEncoder
 141 |       (LC.annotateName name "array")
 142 |       (JArray . map itemToEncoding)
 143 | 
 144 |   nullable (MkJEncoder name toEncoding) =
 145 |     MkJEncoder (LC.annotateName name "nullable") $ \mbValue =>
 146 |       case mbValue of
 147 |         Left LC.MkNull => JNull
 148 |         Right value => toEncoding value
 149 | 
 150 |   required key accessor (MkJEncoder unusedName toEncoding) =
 151 |     \object =>
 152 |       [MkPair key (toEncoding (accessor object))]
 153 | 
 154 |   optional key accessor (MkJEncoder unusedName toEncoding) =
 155 |     \object =>
 156 |       case accessor object of
 157 |         Just value =>
 158 |           [MkPair key (toEncoding value)]
 159 |         Nothing =>
 160 |           []
 161 | 
 162 |   additionalFields accessor (MkJEncoder unusedName toEncoding) =
 163 |     mkAdditional accessor toEncoding
 164 | 
 165 |   mapField unusedF encoder =
 166 |     encoder
 167 | 
 168 |   constructor unusedF =
 169 |     \_ => []
 170 | 
 171 |   field mkStart mkNext =
 172 |     \object =>
 173 |       mkStart object <+> mkNext object
 174 | 
 175 |   additional mkStart mkRest =
 176 |     \object =>
 177 |       mkStart object <+> mkRest object
 178 | 
 179 |   objectNamed name toSeries =
 180 |     MkJEncoder name (JE.object . toSeries)
 181 | 
 182 |   finiteNamed name toText =
 183 |     MkJEncoder name (JE.string . toText)
 184 | 
 185 |   validateNamed name uncheck check (MkJEncoder unvalidatedName toEncoding) =
 186 |     MkJEncoder name (toEncoding . uncheck)
 187 | 
 188 |   unionNamed {types} name builder =
 189 |     let
 190 |       f : Union types -> EncodedJSON (Union types)
 191 |       f = flip (mkUnionNamed {types}) builder
 192 | 
 193 |       -- This seems nice in a way, because it uses a generic function,
 194 |       -- which has seemingly sensible proof fmapping inside.
 195 |       -- But JEncoder has no sensible functor instance, it seems.
 196 |       -- And this returns the wrong type anyway.
 197 |       -- And it ignores a value
 198 |       g : Union types -> JEncoder (Union types)
 199 |       g a = mkUnionNamedFunctor {fun=JEncoder} {types} a $
 200 |               \elPrf, el => MkJEncoder name $
 201 |                 \_ => builder elPrf el
 202 | 
 203 |     in MkJEncoder name f
 204 | 
 205 | 
 206 |   unionMemberWithIndex index encoder =
 207 |       let
 208 |         -- It's important that this let is _inside_ the 'UnionMembers'
 209 |         -- constructor so that it lazy enough to allow the recursive reference
 210 |         -- of 'anyJSON' to itself within arrays.
 211 |         MkJEncoder name toEncoding = encoder
 212 |       in
 213 |         mkUnionMemberWithIndex index toEncoding
 214 | 
 215 |   unionCombine = mkUnionCombine
 216 | 
 217 |   jsonString (MkJEncoder name toEncoding) =
 218 |     MkJEncoder
 219 |       name
 220 |       ( JE.string
 221 |         . JE.stringify
 222 |         . toEncoding
 223 |       )
 224 |