0 | module Derive.FromJSON.Simple
  1 |
  2 | import JSON.Simple.Option
  3 | import JSON.Simple.FromJSON
  4 | import public Derive.Show
  5 | import Language.Reflection.Util
  6 |
  7 | %default total
  8 |
  9 | --------------------------------------------------------------------------------
 10 | --          Claims
 11 | --------------------------------------------------------------------------------
 12 |
 13 | ||| General type of a `fromJSON` function with the given list
 14 | ||| of implicit and auto-implicit arguments, plus the given argument type
 15 | ||| to be displayed.
 16 | |||
 17 | ||| TODO: Use fresh names for `v` and `obj`.
 18 | export
 19 | generalFromJsonType : (implicits : List Arg) -> (arg : TTImp) -> TTImp
 20 | generalFromJsonType is arg =
 21 |   piAll `(Parser JSON ~(arg)) is
 22 |
 23 | ||| Top-level function declaration implementing the `fromJSON` function for
 24 | ||| the given data type.
 25 | export
 26 | fromJsonClaim : Visibility -> (fun : Name) -> (p : ParamTypeInfo) -> Decl
 27 | fromJsonClaim vis fun p =
 28 |   let tpe := generalFromJsonType (allImplicits p "FromJSON") p.applied
 29 |    in simpleClaim vis fun tpe
 30 |
 31 | ||| Top-level declaration of the `FromJSON` implementation for the given data type.
 32 | export
 33 | fromJsonImplClaim : Visibility -> (impl : Name) -> (p : ParamTypeInfo) -> Decl
 34 | fromJsonImplClaim vis impl p = implClaimVis vis impl (implType "FromJSON" p)
 35 |
 36 | --------------------------------------------------------------------------------
 37 | --          Definitions
 38 | --------------------------------------------------------------------------------
 39 |
 40 | val : Name
 41 | val = "val"
 42 |
 43 | bval : TTImp
 44 | bval = bindVar val
 45 |
 46 | vval : TTImp
 47 | vval = var val
 48 |
 49 | obj : Name
 50 | obj = "obj"
 51 |
 52 | bobj : TTImp
 53 | bobj = bindVar obj
 54 |
 55 | vobj : TTImp
 56 | vobj = var obj
 57 |
 58 | matchArray : SnocList (BoundArg 2 p) -> TTImp -> TTImp
 59 | matchArray [<]                  s = s
 60 | matchArray (sx :< BA _ [_,y] _) s =
 61 |   matchArray sx `(Data.Vect.(::) ~(bindVar y) ~(s))
 62 |
 63 | constClause : DCon -> Clause
 64 | constClause c = patClause c.tag c.applied
 65 |
 66 | matchEither : (pat,res : TTImp) -> Name -> TTImp
 67 | matchEither pat res x =
 68 |   `(case ~(pat) of
 69 |      Right ~(bindVar x) => ~(res)
 70 |      Left e             => Left e)
 71 |
 72 | ||| Top-level definition of the `FromJSON` implementation for the given data type.
 73 | export
 74 | fromJsonImplDef : (fun,impl : Name) -> Decl
 75 | fromJsonImplDef f i = def i [patClause (var i) (var "MkFromJSON" `app` var f)]
 76 |
 77 | parameters (nms : List Name) (o : Options) (tpeName : TTImp) (err : TTImp)
 78 |
 79 |   dec : Name -> TTImp
 80 |   dec n =
 81 |     let name := fieldName o n
 82 |         fnm := primVal (Str name)
 83 |      in case o.replaceMissingKeysWithNull name of
 84 |           True  => `(optField ~(vobj) ~(fnm))
 85 |           False => `(field ~(vobj) ~(fnm))
 86 |
 87 |   decFields : SnocList (BoundArg 2 RegularNamed) -> (res : TTImp) -> TTImp
 88 |   decFields [<] res = `(withObject ~(tpeName) $ \ ~(bobj) => ~(res))
 89 |   decFields (sx :< (BA a [x,y] _)) res =
 90 |     let pat := assertIfRec nms a.type (dec $ argName a)
 91 |      in decFields sx (matchEither pat res x)
 92 |
 93 |   decValues : SnocList (BoundArg 2 Regular) -> (res : TTImp) -> TTImp
 94 |   decValues sx res =
 95 |     let nargs := `(Prelude.fromInteger ~(primVal $ BI $ cast (length sx)))
 96 |         mtch  := matchArray sx `(Data.Vect.Nil)
 97 |      in `(withArrayN ~(nargs) ~(tpeName) $ \ ~(mtch) => ~(go sx res))
 98 |
 99 |     where
100 |       go : SnocList (BoundArg 2 Regular) -> TTImp -> TTImp
101 |       go [<]                    res = res
102 |       go (sx :< (BA a [x,y] _)) res =
103 |         let pat := assertIfRec nms a.type `(fromJSON ~(var y))
104 |          in go sx (matchEither pat res x)
105 |
106 |   consts : List DCon -> TTImp
107 |   consts ds =
108 |     let catch := patClause `(s) `(fail $ ~(err) ++ show s)
109 |         cse   :=  lam (lambdaArg {a = Name} "x") $
110 |                   iCase `(x) implicitFalse (map constClause ds ++ [catch])
111 |      in `(withString ~(tpeName) ~(cse))
112 |
113 |   withArgs : DCon -> List DCon -> TTImp
114 |   withArgs d ds = case o.sum of
115 |     UntaggedValue         => untagged
116 |     ObjectWithSingleField => `(fromSingleField ~(tpeName) ~(pairCases))
117 |     TwoElemArray          => `(fromTwoElemArray ~(tpeName) ~(pairCases))
118 |     (TaggedObject tg cs)  =>
119 |       let tf := primVal $ Str tg
120 |           cf := primVal $ Str cs
121 |        in `(fromTaggedObject ~(tpeName) ~(tf) ~(cf) ~(pairCases))
122 |
123 |     where
124 |       rhs : DCon -> TTImp
125 |       rhs c = case c.args of
126 |         Const       => decFields [<] c.applied -- not possible
127 |         Fields [<x] => case o.unwrapUnary of
128 |           True  => assertIfRec nms x.arg.type `(map ~(var c.name) . fromJSON)
129 |           False => decFields [<x]  c.applied
130 |         Values [<x] => case o.unwrapUnary of
131 |           True  => assertIfRec nms x.arg.type `(map ~(var c.name) . fromJSON)
132 |           False => decValues [<x]  c.applied
133 |         Fields sx   => decFields sx  c.applied
134 |         Values sx   => decValues sx  c.applied
135 |
136 |       clause : DCon -> Clause
137 |       clause c =
138 |         let rightHand := `(prependPath (~(rhs c) ~(vval)) $ Key ~(c.tag))
139 |          in patClause `(MkPair ~(c.tag) ~(bval)) rightHand
140 |
141 |       pairCases : TTImp
142 |       pairCases =
143 |         let clauses := map clause (d :: ds)
144 |             catch   := patClause `(MkPair s _) `(fail $ ~(err) ++ show s)
145 |          in lam (lambdaArg {a = Name} "x") $
146 |             iCase `(x) implicitFalse (clauses ++ [catch])
147 |
148 |       untagged : TTImp
149 |       untagged = foldl (\t,c => `(JSON.Simple.FromJSON.(<|>) ~(t) ~(rhs c))) (rhs d) ds
150 |
151 |
152 |   decSum : (constants, withArgs : List DCon) -> TTImp
153 |   decSum [] []        = `(fail $ "Uninhabited type: " ++ ~(tpeName))
154 |   decSum [] (w :: ws) = withArgs w ws
155 |   decSum cs []        = consts cs
156 |   decSum cs (w :: ws) = `(~(consts cs) <|> ~(withArgs w ws))
157 |
158 |   decRecord : DCon -> TTImp
159 |   decRecord c = case c.args of
160 |     Const       => consts [c]
161 |     Fields [<x] => assertIfRec nms x.arg.type `(map ~(var c.name) . fromJSON)
162 |     Values [<x] => assertIfRec nms x.arg.type `(map ~(var c.name) . fromJSON)
163 |     Fields sx   => decFields sx c.applied
164 |     Values sx   => decValues sx c.applied
165 |
166 |   export
167 |   fromJsonClause : (fun : Name) -> TypeInfo -> Clause
168 |   fromJsonClause fun x = case map (dcon o) x.cons of
169 |     [c] =>
170 |       if o.unwrapRecords then patClause (var fun) (decRecord c)
171 |       else if isConst c then patClause (var fun) (decSum [c] [])
172 |       else patClause (var fun) (decSum [] [c])
173 |     cs  =>
174 |       let (consts,withArgs) := partition isConst cs
175 |        in  patClause (var fun) (decSum consts withArgs)
176 |
177 |   export
178 |   fromJsonDef : Name -> TypeInfo -> Decl
179 |   fromJsonDef fun ti = def fun [fromJsonClause fun ti]
180 |
181 | --------------------------------------------------------------------------------
182 | --          Deriving
183 | --------------------------------------------------------------------------------
184 |
185 | err : Named a => a -> TTImp
186 | err v = primVal $ Str $ "Unexpected constructor tag for \{v.nameStr}: "
187 |
188 | export
189 | customFromJSON :
190 |      Visibility
191 |   -> Options
192 |   -> List Name
193 |   -> ParamTypeInfo
194 |   -> Res (List TopLevel)
195 | customFromJSON vis o nms p =
196 |   let fun  := funName p "fromJson"
197 |       impl := implName p "FromJSON"
198 |    in Right
199 |         [ TL (fromJsonClaim vis fun p)
200 |              (fromJsonDef nms o p.namePrim (err p) fun p.info)
201 |         , TL (fromJsonImplClaim vis impl p) (fromJsonImplDef fun impl)
202 |         ]
203 |
204 | ||| Generate declarations and implementations for
205 | ||| `FromJSON` for a given data type
206 | ||| using default settings.
207 | export %inline
208 | FromJSON : List Name -> ParamTypeInfo -> Res (List TopLevel)
209 | FromJSON = customFromJSON Export defaultOptions
210 |