
   0 | module Lana.JSON.Decoder
   1 | 
   2 | -- Transitive import bug
   3 | import Data.List.Quantifiers as Bug
   4 | import Data.SortedMap as Map
   5 | import Data.Finite as Finite
   6 | import Data.List.Elem as Bug
   7 | 
   8 | import Lana.Name as LC
   9 | import Lana.Class as LC
  10 | 
  11 | import JSON.Simple.FromJSON as Simp
  12 | import JSON.Parser as P
  13 | 
  14 | -- Like in Aeson, a Parser is
  15 | -- the *result* of parsing
  16 | public export
  17 | Parser : Type -> Type
  18 | Parser a = Either JSONErr a
  19 | 
  20 | AObject : Type
  21 | AObject = List (Pair String P.JSON)
  22 | 
  23 | export
  24 | data JDecoder a = MkJDecoder LC.Name (P.JSON -> Parser a)
  25 | 
  26 | export
  27 | decodeJSON : JDecoder a -> JSON -> Parser a
  28 | decodeJSON (MkJDecoder unusedName f) json = f json
  29 | 
  30 | record MyObject (a: Type) where
  31 |   constructor MkMyObject
  32 |   fields: List String
  33 |   decoder: AObject -> Parser a
  34 | 
  35 | record MyField (a: Type) where
  36 |   constructor MkMyField
  37 |   name: String
  38 |   decoder: AObject -> Parser a
  39 | 
  40 | record MyAdditionalFields (a: Type) where
  41 |   constructor MkMyAdditionalFields
  42 |   additionalFieldsDecoder: (List String -> AObject -> Parser a)
  43 | 
  44 | record MyUnionMembers (allTypes: List Type) where
  45 |   constructor MkMyUnionMembers
  46 |   parseNameAndJSON: LC.Name -> JSON ->
  47 |                     Parser (Union allTypes)
  48 | 
  49 | mkField : {a: Type} ->
  50 |           {b: Type} ->
  51 |           MyObject (a -> b) ->
  52 |           MyField a ->
  53 |           MyObject b
  54 | mkField (MkMyObject fieldNames parseF) fieldVal =
  55 |   MkMyObject keys dec
  56 |   where
  57 |     keys : List String
  58 |     keys = fieldVal.name :: fieldNames
  59 |     dec :  AObject -> Parser b
  60 |     dec aObject =
  61 |       let p : Parser (a -> b)
  62 |           p = parseF aObject
  63 |        in p <*> fieldVal.decoder aObject
  64 | 
  65 | mkAdditional: {obj: Type} ->
  66 |               {a: Type} ->
  67 |               MyObject (a -> obj) ->
  68 |               MyAdditionalFields a ->
  69 |               MyObject obj
  70 | mkAdditional (MkMyObject fieldNames parseF) fields =
  71 |   MkMyObject fieldNames dec
  72 |   where
  73 |     dec : AObject -> Parser obj
  74 |     dec aObject =
  75 |       parseF aObject
  76 |         <*> additionalFieldsDecoder fields fieldNames aObject
  77 | 
  78 | mkUnionCombine: {types: List Type} ->
  79 |                 MyUnionMembers types ->
  80 |                 MyUnionMembers types ->
  81 |                 MyUnionMembers types
  82 | mkUnionCombine left right =
  83 |   let
  84 |     f : LC.Name -> JSON -> Parser (Union types)
  85 |     f name value = do
  86 |       case left.parseNameAndJSON name value of
  87 |         Right suc => Right suc
  88 |         Left _ =>
  89 |           case right.parseNameAndJSON name value of
  90 |             Right suc => Right suc
  91 |             Left _ => Left . MkPair [] $
  92 |               "All union parsing options for "
  93 |               <+> name.nameUnqualified
  94 |               <+> " failed."
  95 |   in
  96 |   MkMyUnionMembers f
  97 | 
  98 | mkAdditionalFields:
  99 |     {a: Type} ->
 100 |     JDecoder a ->
 101 |     MyAdditionalFields (Map.SortedMap String a)
 102 | mkAdditionalFields (MkJDecoder unusedName parseValue) =
 103 |   let
 104 |     f: List String -> AObject ->
 105 |        Parser (Map.SortedMap String a)
 106 |     f definedFields object =
 107 |       let
 108 |         additionalKeysMap : Map.SortedMap String JSON
 109 |         additionalKeysMap =
 110 |           foldr
 111 |             Map.delete
 112 |             (Map.fromList object)
 113 |             definedFields
 114 |       in
 115 |         traverse parseValue additionalKeysMap
 116 |   in
 117 |     MkMyAdditionalFields f
 118 | 
 119 | mkUnionMemberWithIndex: {a: Type} ->
 120 |                         {types: List Type} ->
 121 |                         Elem a types ->
 122 |                         (JSON -> Parser a) ->
 123 |                         MyUnionMembers types
 124 | mkUnionMemberWithIndex elem parseMember =
 125 |   MkMyUnionMembers $ \name, json =>
 126 |     case elem of
 127 |       Data.List.Elem.Here =>
 128 |         map Data.List.Quantifiers.Any.Here $
 129 |           parseMember json
 130 |       Data.List.Elem.There there =>
 131 |         let
 132 |           inner = mkUnionMemberWithIndex there parseMember
 133 |         in
 134 |           map Data.List.Quantifiers.Any.There $
 135 |             inner.parseNameAndJSON name json
 136 | 
 137 | export
 138 | implementation LC.Lana JDecoder where
 139 |   Object = const MyObject
 140 |   Field = const MyField
 141 |   AdditionalFields = const MyAdditionalFields
 142 |   UnionMembers a b = MyUnionMembers a
 143 | 
 144 |   schemaName (MkJDecoder name unusedParser) = name
 145 | 
 146 |   double =
 147 |     MkJDecoder (LC.unqualifiedName "double") $
 148 |       withDouble "double" pure
 149 | 
 150 |   text =
 151 |     MkJDecoder (LC.unqualifiedName "text") $
 152 |       withString "text" pure
 153 | 
 154 |   boolean =
 155 |     MkJDecoder (LC.unqualifiedName "boolean") $
 156 |       withBoolean "boolean" pure
 157 | 
 158 |   array (MkJDecoder name itemForValue) =
 159 |     MkJDecoder (LC.annotateName name "array") $
 160 |       withArray "array" (traverse itemForValue)
 161 | 
 162 |   null =
 163 |     MkJDecoder (LC.unqualifiedName "null") $ \case
 164 |       JNull => pure LC.MkNull
 165 |       _ => Left (MkPair [] "Expected null")
 166 | 
 167 |   nullable (MkJDecoder name parseValue) =
 168 |     MkJDecoder (LC.annotateName name "nullable") $ \case
 169 |       JNull => pure (Left LC.MkNull)
 170 |       value => map Right (parseValue value)
 171 | 
 172 |   required key unusedAccessor (MkJDecoder unusedName parseValue) =
 173 |     MkMyField key $ \aObject =>
 174 |       explicitParseField parseValue aObject key
 175 | 
 176 |   optional key unusedAccessor (MkJDecoder unusedName parseValue) =
 177 |     MkMyField key $ \aObject =>
 178 |       explicitParseFieldMaybe parseValue aObject key
 179 | 
 180 |   additionalFields = const mkAdditionalFields
 181 | 
 182 |   mapField f (MkMyField name parseField) =
 183 |     MkMyField name (map f . parseField)
 184 | 
 185 |   constructor f =
 186 |     MkMyObject [] (\unusedObject => pure f)
 187 | 
 188 |   field = mkField
 189 | 
 190 |   additional = mkAdditional
 191 | 
 192 |   objectNamed name (MkMyObject unusedDefinedFields parseObject) =
 193 |     MkJDecoder name $
 194 |       withObject (LC.nameToString name) parseObject
 195 | 
 196 |   finiteNamed name toText =
 197 |     let
 198 |       decodingMap =
 199 |         SortedMap.fromList
 200 |           . map (\e => (toText e, e))
 201 |           $ Finite.values
 202 |     in
 203 |       MkJDecoder name $
 204 |         withString (LC.nameToString name) $ \textValue =>
 205 |           case SortedMap.lookup textValue decodingMap of
 206 |             Just enumValue => pure enumValue
 207 |             Nothing =>
 208 |               fail $
 209 |                 "Unrecognized value for "
 210 |                   <+> LC.nameToString name
 211 |                   <+> " enum: "
 212 |                   <+> show textValue
 213 | 
 214 |   validateNamed name unusedUncheck check (MkJDecoder unusedUnvalidatedName parseValue) =
 215 |     MkJDecoder name $ \jsonValue => do
 216 |       uncheckedValue <- parseValue jsonValue
 217 |       case check uncheckedValue of
 218 |         Right checkedValue => pure checkedValue
 219 |         Left err => Left . MkPair [] $
 220 |           "Error validating "
 221 |           <+> LC.nameToString name
 222 |           <+> ": " <+> err
 223 | 
 224 |   unionNamed name (MkMyUnionMembers parseMembers) =
 225 |     MkJDecoder name (parseMembers name)
 226 | 
 227 |   unionMemberWithIndex index (MkJDecoder unusedName parseMember) =
 228 |     mkUnionMemberWithIndex index parseMember
 229 | 
 230 |   unionCombine = mkUnionCombine
 231 | 
 232 |   jsonString (MkJDecoder name parseValue) =
 233 |     MkJDecoder name $
 234 |       withString name.nameUnqualified $ \jsonText =>
 235 |         case parseJSON Virtual jsonText of
 236 |           Left parseErr =>
 237 |             Left . MkPair [] $
 238 |               "Error decoding nested json string: "
 239 |               <+> interpolate parseErr.error
 240 |           Right value => parseValue value
 241 |