0 | module Derive.ToJSON
  1 |
  2 | import JSON.Option
  3 | import JSON.ToJSON
  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 `toJSON` 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 name for `v`
 18 | export
 19 | generalToJsonType : (implicits : List Arg) -> (arg : TTImp) -> TTImp
 20 | generalToJsonType is arg = piAll `({0 v : _} -> Encoder v => ~(arg) -> v) is
 21 |
 22 | ||| Top-level function declaration implementing the `toJSON` function for
 23 | ||| the given data type.
 24 | export
 25 | toJsonClaim : (fun : Name) -> (p : ParamTypeInfo) -> Decl
 26 | toJsonClaim fun p =
 27 |   let tpe := generalToJsonType (allImplicits p "ToJSON") p.applied
 28 |    in public' fun tpe
 29 |
 30 | ||| Top-level declaration of the `ToJSON` implementation for the given data type.
 31 | export
 32 | toJsonImplClaim : (impl : Name) -> (p : ParamTypeInfo) -> Decl
 33 | toJsonImplClaim impl p = implClaim impl (implType "ToJSON" p)
 34 |
 35 | --------------------------------------------------------------------------------
 36 | --          Definitions
 37 | --------------------------------------------------------------------------------
 38 |
 39 | ||| Top-level definition of the `ToJSON` implementation for the given data type.
 40 | export
 41 | toJsonImplDef : (fun, impl : Name) -> Decl
 42 | toJsonImplDef f i = def i [patClause (var i) (var "MkToJSON" `app` var f)]
 43 |
 44 | parameters (nms : List Name) (o : Options)
 45 |
 46 |   encValue : BoundArg 2 Regular -> TTImp
 47 |   encValue (BA (MkArg _  _ _ t) [x,_] _) =
 48 |     assertIfRec nms t `(toJSON ~(var x))
 49 |
 50 |   encField : BoundArg 2 RegularNamed -> TTImp
 51 |   encField (BA a [x,_]  _) =
 52 |     let nm := fieldNamePrim o (argName a)
 53 |      in assertIfRec nms a.type `(jpair ~(nm) ~(var x))
 54 |
 55 |   encArgs : (unwrapUnary : Bool) -> (tag : TTImp) -> ArgInfo -> TTImp
 56 |   encArgs _    tag Const         = `(string  ~(tag))
 57 |   encArgs True _   (Fields [<v]) = encValue $ toRegular v
 58 |   encArgs True _   (Values [<v]) = encValue v
 59 |   encArgs _    _   (Fields sx)   = `(object ~(listOf $ map encField sx))
 60 |   encArgs _    _   (Values sx)   = `(array ~(listOf $ map encValue sx))
 61 |
 62 |   encSum : DCon -> TTImp
 63 |   encSum (DC n b _ tag Const) = encArgs o.unwrapUnary tag Const
 64 |   encSum (DC n b _ tag args)  =
 65 |     let flds := encArgs o.unwrapUnary tag args
 66 |      in case o.sum of
 67 |           UntaggedValue         => flds
 68 |           ObjectWithSingleField => `(singleField ~(tag) ~(flds))
 69 |           TwoElemArray          => `(twoElemArray ~(tag) ~(flds))
 70 |           (TaggedObject tg cs)  =>
 71 |             let tf := primVal $ Str tg
 72 |                 cf := primVal $ Str cs
 73 |              in `(taggedObject ~(tf) ~(cf) ~(tag) ~(flds))
 74 |
 75 |   sumClause : (fun : Name) -> DCon -> Clause
 76 |   sumClause fun c = patClause (var fun `app` c.bound) (encSum c)
 77 |
 78 |   recClause : (fun : Name) -> DCon -> Clause
 79 |   recClause fun c = patClause (var fun `app` c.bound) (encArgs o.unwrapUnary c.tag c.args)
 80 |
 81 |   export
 82 |   toJsonClauses : (fun : Name) -> TypeInfo -> List Clause
 83 |   toJsonClauses fun ti = case ti.cons of
 84 |     -- single constructor
 85 |     [x] => if o.unwrapRecords then [recClause fun $ dcon o x]
 86 |            else [sumClause fun (dcon o x)]
 87 |
 88 |     -- multi-constructor
 89 |     xs  => map (sumClause fun . dcon o) xs
 90 |
 91 |   export
 92 |   toJsonDef : Name -> TypeInfo -> Decl
 93 |   toJsonDef fun ti = def fun (toJsonClauses fun ti)
 94 |
 95 | --------------------------------------------------------------------------------
 96 | --          Deriving
 97 | --------------------------------------------------------------------------------
 98 |
 99 | export
100 | customToJSON : Options -> List Name -> ParamTypeInfo -> Res (List TopLevel)
101 | customToJSON o nms p =
102 |   let fun  := funName p "toJson"
103 |       impl := implName p "ToJSON"
104 |    in Right
105 |         [ TL (toJsonClaim fun p) (toJsonDef nms o fun p.info)
106 |         , TL (toJsonImplClaim impl p) (toJsonImplDef fun impl)
107 |         ]
108 |
109 | ||| Generate declarations and implementations for `ToJSON` for a given data type
110 | ||| using default settings.
111 | export %inline
112 | ToJSON : List Name -> ParamTypeInfo -> Res (List TopLevel)
113 | ToJSON = customToJSON defaultOptions
114 |