0 | ||| Automatic deriviation of JSON conversion interfaces.
  1 | |||
  2 | ||| (C) The Idris Community, 2021
  3 | module Language.LSP.Message.Derive
  4 |
  5 | -- NOTE: Elaborator functions are evaluated as if they are defined inside the
  6 | -- call location module, thus imported functions used inside elaborator
  7 | -- functions should be exported publicly or explicitly imported at call
  8 | -- location.
  9 | import public Data.Maybe
 10 | import public Data.SortedMap
 11 | import Data.String
 12 | import Language.JSON
 13 | import public Language.JSON.Interfaces
 14 | import Language.Reflection
 15 |
 16 | %language ElabReflection
 17 | %default total
 18 |
 19 | ||| Options for automatic derivation of `ToJSON`/`FromJSON` instances.
 20 | public export
 21 | record JSONDeriveOpts where
 22 |   constructor MkOpts
 23 |   ||| If tagged, values are converted to JSON object with one field where the
 24 |   ||| key is the name of the constructor and the value is the object obtained
 25 |   ||| from converting the arguments of the constructor.
 26 |   tagged : Bool
 27 |   ||| Renaming rules for arguments where the name of the argument does not
 28 |   ||| match the correspondent key in the translated JSON object.
 29 |   renames : List (String, String)
 30 |   ||| Fields that must be present in the JSON translation but have static
 31 |   ||| values.
 32 |   staticFields : List (String, JSON)
 33 |
 34 | public export
 35 | defaultOpts : JSONDeriveOpts
 36 | defaultOpts = MkOpts False [] []
 37 |
 38 | stripNs : Name -> Name
 39 | stripNs (NS _ x) = x
 40 | stripNs x = x
 41 |
 42 | covering
 43 | genReadableSym : String -> Elab Name
 44 | genReadableSym hint = do
 45 |   MN v i <- genSym hint
 46 |     | _ => fail "cannot generate readable argument name"
 47 |   pure $ UN $ Basic (v ++ show i)
 48 |
 49 | var : Name -> TTImp
 50 | var = IVar EmptyFC
 51 |
 52 | bindvar : Name -> TTImp
 53 | bindvar = IBindVar EmptyFC
 54 |
 55 | primStr : String -> TTImp
 56 | primStr = IPrimVal EmptyFC . Str
 57 |
 58 | patClause : TTImp -> TTImp -> Clause
 59 | patClause = PatClause EmptyFC
 60 |
 61 | implicit' : TTImp
 62 | implicit' = Implicit EmptyFC True
 63 |
 64 | -- TODO: add support for polymorphic types and maybe use another type for
 65 | -- optional fields in place of Maybe.
 66 | ||| Automatic derivation of `ToJSON` instances.
 67 | ||| NOTE: all the fields in each constructor MUST be named, record already
 68 | ||| comply but types declared with data must have constructors declared like
 69 | ||| this:
 70 | ||| ```idris example
 71 | ||| data Position : Type where
 72 | |||   MkPosition : (x : Integer) -> (y : Integer) -> Position
 73 | ||| ```
 74 | ||| If the tagging option is enabled, types with multiple constructors are
 75 | ||| translated to a JSON object with a single key-value pair where the key is
 76 | ||| constructor name (without the namespace) and the value is the JSON object
 77 | ||| translated as if untagged.
 78 | ||| Constructor arguments that are `Maybe` instances are omitted if `Nothing`
 79 | ||| and converted without the constructor if `Just`. If you need to translate a
 80 | ||| mandatory field that can be nullable use the `Null` type.
 81 | |||
 82 | ||| @ opts The automatic derivation options.
 83 | ||| @ name The name of the type to derive for. Can be without namespace if unambigous.
 84 | public export covering
 85 | deriveToJSON : (opts : JSONDeriveOpts) -> (name : Name) -> Elab ()
 86 | deriveToJSON opts n = do
 87 |     [(name, imp)] <- getType n
 88 |       | xs => fail $ show n ++ " must be in scope and unique. Possible referred types are: " ++ show (fst <$> xs)
 89 |     -- FIXME: temporary name for debugging, should be converted to a name impossible to define from users
 90 |     -- and should not be exported, unless a specific option is enabled.
 91 |     let funName = UN $ Basic ("toJSON" ++ show (stripNs n))
 92 |     let objName = UN $ Basic ("__impl_toJSON" ++ show (stripNs n))
 93 |     conNames <- getCons name
 94 |     cons <- for conNames $ \n => do
 95 |       [(conName, conImpl)] <- getType n
 96 |         | _ => fail $ show n ++ " constructor must be in scope and unique"
 97 |       (bindNames, rhs) <- genRHS conImpl
 98 |       let rhs = if opts.tagged
 99 |                    then `(JObject $ [MkPair ~(primStr $ show $ stripNs n) (JObject $ catMaybes ~rhs)])
100 |                    else `(JObject $ catMaybes ~rhs)
101 |       let lhs = `(~(var funName) ~(applyBinds (var conName) (reverse bindNames)))
102 |       pure $ patClause lhs rhs
103 |     let funclaim = IClaim $ MkFCVal EmptyFC $ MkIClaimData MW Export [Inline] (MkTy EmptyFC (NoFC funName) `(~(var name) -> JSON))
104 |     let fundecl = IDef EmptyFC funName cons
105 |     declare [funclaim, fundecl]
106 |     [(ifName, _)] <- getType `{ToJSON}
107 |       | _ => fail "ToJSON interface must be in scope and unique"
108 |     [NS _ (DN _ ifCon)] <- getCons ifName
109 |       | _ => fail "Interface constructor error"
110 |     let retty = `(ToJSON ~(var name))
111 |     let objclaim = IClaim $ MkFCVal EmptyFC $ MkIClaimData MW Export [Hint True, Inline] (MkTy EmptyFC (NoFC objName) retty)
112 |     let objrhs = `(~(var ifCon) ~(var funName))
113 |     let objdecl = IDef EmptyFC objName [(PatClause EmptyFC (var objName) objrhs)]
114 |     declare [objclaim, objdecl]
115 |   where
116 |     genRHS : TTImp -> Elab (List Name, TTImp)
117 |     genRHS (IPi _ _ _ (Just n) `(Prelude.Types.Maybe ~argTy) retTy) = do
118 |       (ns, rest) <- genRHS retTy
119 |       let name = primStr $ fromMaybe (show n) $ lookup (show n) opts.renames
120 |       pure (n :: ns, `(((MkPair ~name . toJSON) <$> ~(var n)) :: ~rest))
121 |     genRHS (IPi _ _ _ (Just n) argTy retTy) = do
122 |       (ns, rest) <- genRHS retTy
123 |       let name = primStr $ fromMaybe (show n) $ lookup (show n) opts.renames
124 |       pure (n :: ns, `(Just (MkPair ~name (toJSON ~(var n))) :: ~rest))
125 |     genRHS (IPi _ _ _ Nothing _ _) = fail $ "All arguments must be explicitly named"
126 |     genRHS _ = do
127 |       -- Hack required, because if you quote directly opts.staticFields the elaborator introduces unsolved holes
128 |       r <- traverse (\(k, v) => (k,) <$> quote v) opts.staticFields
129 |       pure ([], foldr (\(k, v), acc => `(Just (MkPair ~(primStr k) ~v) :: ~acc)) `([]) r)
130 |
131 |     applyBinds : TTImp -> List Name -> TTImp
132 |     applyBinds = foldr (\n, acc => `(~acc ~(bindvar n)))
133 |
134 | ||| Automatic derivation of `FromJSON` instances.
135 | ||| NOTE: all the fields in each constructor MUST be named, record already
136 | ||| comply but types declared with data must have constructors declared like
137 | ||| this:
138 | ||| ```idris example
139 | ||| data Position : Type where
140 | |||   MkPosition : (x : Integer) -> (y : Integer) -> Position
141 | ||| ```
142 | ||| If the tagging option is enabled, types with multiple constructors are
143 | ||| translated to a JSON object with a single key-value pair where the key is
144 | ||| constructor name (without the namespace) and the value is the JSON object
145 | ||| translated as if untagged.
146 | ||| Constructor arguments that are `Maybe` instances are omitted if `Nothing`
147 | ||| and converted without the constructor if `Just`. If you need to translate a
148 | ||| mandatory field that can be nullable use the `Null` type.
149 | |||
150 | ||| @ opts The automatic derivation options.
151 | ||| @ name The name of the type to derive for. Can be without namespace if unambigous.
152 | public export covering
153 | deriveFromJSON : (opts : JSONDeriveOpts) -> (name : Name) -> Elab ()
154 | deriveFromJSON opts n = do
155 |     [(name, imp)] <- getType n
156 |       | xs => fail $ show n ++ " must be in scope and unique. Possible referred types are: " ++ show (fst <$> xs)
157 |     -- FIXME: temporary name for debugging, should be converted to a name impossible to define from users
158 |     -- and should not be exported, unless a specific option is enabled.
159 |     let funName = UN $ Basic ("fromJSON" ++ show (stripNs n))
160 |     let objName = UN $ Basic ("__impl_fromJSON" ++ show (stripNs n))
161 |     conNames <- getCons name
162 |     argName <- genReadableSym "arg"
163 |     cons <- for conNames $ \n => do
164 |       [(conName, conImpl)] <- getType n
165 |         | _ => fail $ show n ++ "constructor must be in scope and unique"
166 |       args <- getArgs conImpl
167 |       pure (conName, args)
168 |     clauses <- traverse (\(cn, as) => genClause funName cn argName (reverse as)) cons
169 |     let clauses = if opts.tagged
170 |                      then (uncurry patClause <$> clauses)
171 |                      else [patClause `(~(var funName) (JObject ~(bindvar argName)))
172 |                                      (foldl (\acc, x => `(~x <|> ~acc)) `(Nothing) (snd <$> clauses))]
173 |     let funClaim = IClaim $ MkFCVal EmptyFC $ MkIClaimData MW Export [Inline] (MkTy EmptyFC (NoFC funName) `(JSON -> Maybe ~(var name)))
174 |     let funDecl = IDef EmptyFC funName (clauses ++ [patClause `(~(var funName) ~implicit') `(Nothing)])
175 |     declare [funClaim, funDecl]
176 |     [(ifName, _)] <- getType `{FromJSON}
177 |       | _ => fail "FromJSON interface must be in scope and unique"
178 |     [NS _ (DN _ ifCon)] <- getCons ifName
179 |       | _ => fail "Interface constructor error"
180 |     let retty = `(FromJSON ~(var name))
181 |     let objClaim = IClaim $ MkFCVal EmptyFC $ MkIClaimData MW Export [Hint True, Inline] (MkTy EmptyFC (NoFC objName) retty)
182 |     let objrhs = `(~(var ifCon) ~(var funName))
183 |     let objDecl = IDef EmptyFC objName [(PatClause EmptyFC (var objName) objrhs)]
184 |     declare [objClaim, objDecl]
185 |   where
186 |     getArgs : TTImp -> Elab (List (Name, TTImp))
187 |     getArgs (IPi _ _ _ (Just n) argTy retTy) = ((n, argTy) ::) <$> getArgs retTy
188 |     getArgs (IPi _ _ _ Nothing _ _) = fail $ "All arguments must be explicitly named"
189 |     getArgs _ = pure []
190 |
191 |     genClause : Name -> Name -> Name -> List (Name, TTImp) -> Elab (TTImp, TTImp)
192 |     genClause funName t m xs = do
193 |       let lhs = `(~(var funName) (JObject [MkPair ~(primStr $ show $ stripNs t) (JObject ~(bindvar m))]))
194 |       let rhs = foldr (\(n, type), acc => let name = primStr $ fromMaybe (show n) $ lookup (show n) opts.renames in
195 |                                               case type of
196 |                                                    `(Prelude.Types.Maybe _) => `(~acc <*> (pure $ lookup ~name ~(var m) >>= fromJSON))
197 |                                                    _ => `(~acc <*> (lookup ~name ~(var m) >>= fromJSON)))
198 |                       `(pure ~(var t)) xs
199 |       r <- traverse (\(k, v) => (k,) <$> quote v) opts.staticFields
200 |       let rhs = foldr (\(k, v), acc => `((lookup ~(primStr k) ~(var m) >>= (guard . (== ~v))) *> ~acc)) rhs r
201 |       pure (lhs, rhs)
202 |
203 | ||| Automatic derivation of `ToJSON` and `FromJSON` instances.
204 | ||| See `deriveToJSON` and `deriveFromJSON`.
205 | |||
206 | ||| @ opts The automatic derivation options.
207 | ||| @ name The name of the type to derive for. Can be without namespace if unambigous.
208 | public export covering
209 | deriveJSON : (opts : JSONDeriveOpts) -> (name : Name) -> Elab ()
210 | deriveJSON opts name = deriveToJSON opts name *> deriveFromJSON opts name
211 |