0 | module Derive.ToJSON.Simple
  1 |
  2 | import JSON.Simple.Option
  3 | import JSON.Simple.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 `(~(arg) -> JSON) is
 21 |
 22 | ||| Top-level function declaration implementing the `toJSON` function for
 23 | ||| the given data type.
 24 | export
 25 | toJsonClaim : Visibility -> (fun : Name) -> (p : ParamTypeInfo) -> Decl
 26 | toJsonClaim vis fun p =
 27 |   let tpe := generalToJsonType (allImplicits p "ToJSON") p.applied
 28 |    in simpleClaim vis fun tpe
 29 |
 30 | ||| Top-level declaration of the `ToJSON` implementation for the given data type.
 31 | export
 32 | toJsonImplClaim : Visibility -> (impl : Name) -> (p : ParamTypeInfo) -> Decl
 33 | toJsonImplClaim vis impl p = implClaimVis vis 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         = `(JString  ~(tag))
 57 |   encArgs True _   (Fields [<v]) = encValue $ toRegular v
 58 |   encArgs True _   (Values [<v]) = encValue v
 59 |   encArgs _    _   (Fields sx)   = `(JObject ~(listOf $ map encField sx))
 60 |   encArgs _    _   (Values sx)   = `(JArray ~(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] =>
 86 |       if o.unwrapRecords then [recClause fun $ dcon o x]
 87 |       else [sumClause fun (dcon o x)]
 88 |
 89 |     -- multi-constructor
 90 |     xs  => map (sumClause fun . dcon o) xs
 91 |
 92 |   export
 93 |   toJsonDef : Name -> TypeInfo -> Decl
 94 |   toJsonDef fun ti = def fun (toJsonClauses fun ti)
 95 |
 96 | --------------------------------------------------------------------------------
 97 | --          Deriving
 98 | --------------------------------------------------------------------------------
 99 |
100 | export
101 | customToJSON :
102 |      Visibility
103 |   -> Options
104 |   -> List Name
105 |   -> ParamTypeInfo
106 |   -> Res (List TopLevel)
107 | customToJSON vis o nms p =
108 |   let fun  := funName p "toJson"
109 |       impl := implName p "ToJSON"
110 |    in Right
111 |         [ TL (toJsonClaim vis fun p) (toJsonDef nms o fun p.info)
112 |         , TL (toJsonImplClaim vis impl p) (toJsonImplDef fun impl)
113 |         ]
114 |
115 | ||| Generate declarations and implementations for `ToJSON` for a given data type
116 | ||| using default settings.
117 | export %inline
118 | ToJSON : List Name -> ParamTypeInfo -> Res (List TopLevel)
119 | ToJSON = customToJSON Export defaultOptions
120 |