0 | module JSON.Option
  1 |
  2 | import Derive.Prelude
  3 |
  4 | %language ElabReflection
  5 |
  6 | ||| Specifies how to encode constructors of a sum datatype.
  7 | public export
  8 | data SumEncoding : Type where
  9 |   ||| Constructor names won't be encoded. Instead only the contents of the
 10 |   ||| constructor will be encoded as if the type had a single constructor. JSON
 11 |   ||| encodings have to be disjoint for decoding to work properly.
 12 |   |||
 13 |   ||| When decoding, constructors are tried in the order of definition. If some
 14 |   ||| encodings overlap, the first one defined will succeed.
 15 |   |||
 16 |   ||| Note: Nullary constructors are encoded as strings (using
 17 |   ||| constructorTagModifier).  Having a nullary constructor
 18 |   ||| alongside a single field constructor that encodes to a
 19 |   ||| string leads to ambiguity.
 20 |   |||
 21 |   ||| Note: Only the last error is kept when decoding, so in the case of
 22 |   ||| malformed JSON, only an error for the last constructor will be reported.
 23 |   UntaggedValue         : SumEncoding
 24 |
 25 |   ||| A constructor will be encoded to an object with a single field named
 26 |   ||| after the constructor tag (modified by the constructorTagModifier) which
 27 |   ||| maps to the encoded contents of the constructor.
 28 |   ObjectWithSingleField : SumEncoding
 29 |
 30 |   ||| A constructor will be encoded to a 2-element array where the first
 31 |   ||| element is the tag of the constructor (modified by the constructorTagModifier)
 32 |   ||| and the second element the encoded contents of the constructor.
 33 |   TwoElemArray          : SumEncoding
 34 |
 35 |   ||| A constructor will be encoded to an object with a field `tagFieldName`
 36 |   ||| which specifies the constructor tag (modified by the
 37 |   ||| constructorTagModifier). If the constructor is a record the
 38 |   ||| encoded record fields will be unpacked into this object. So
 39 |   ||| make sure that your record doesn't have a field with the
 40 |   ||| same label as the tagFieldName.  Otherwise the tag gets
 41 |   ||| overwritten by the encoded value of that field! If the constructor
 42 |   ||| is not a record the encoded constructor contents will be
 43 |   ||| stored under the contentsFieldName field.
 44 |   TaggedObject          :  (tagFieldName : String)
 45 |                         -> (contentsFieldName : String)
 46 |                         -> SumEncoding
 47 |
 48 | %runElab derive "SumEncoding" [Show,Eq]
 49 |
 50 | ||| Corresponds to `TaggedObject "tag" "contents"`
 51 | public export
 52 | defaultTaggedObject : SumEncoding
 53 | defaultTaggedObject = TaggedObject "tag" "contents"
 54 |
 55 | public export
 56 | record Options where
 57 |   constructor MkOptions
 58 |   ||| How to encode sum types
 59 |   sum                        : SumEncoding
 60 |
 61 |   ||| If `True`, the single field from a unary data constructor
 62 |   ||| will be unwrapped.
 63 |   unwrapUnary                : Bool
 64 |
 65 |   ||| If `True`, missing keys in a JSON objects will be
 66 |   ||| replaced with `Null` during decoding.
 67 |   replaceMissingKeysWithNull : Bool
 68 |
 69 |   ||| If `True`, single constructor data types will be
 70 |   ||| encoded without a tag for the constructor name.
 71 |   unwrapRecords              : Bool
 72 |
 73 |   ||| This function is used to adjust constructor names
 74 |   ||| during encoding and decoding
 75 |   constructorTagModifier     : String -> String
 76 |
 77 |   ||| This function is used to adjust constructor argument names
 78 |   ||| during encoding and decoding
 79 |   fieldNameModifier          : String -> String
 80 |
 81 | public export
 82 | defaultOptions : Options
 83 | defaultOptions = MkOptions defaultTaggedObject True False True id id
 84 |
 85 | public export
 86 | fieldName : Named a => Options -> a -> String
 87 | fieldName o v = o.fieldNameModifier v.nameStr
 88 |
 89 | public export
 90 | fieldNamePrim : Named a => Options -> a -> TTImp
 91 | fieldNamePrim o v = primVal (Str $ fieldName o v)
 92 |
 93 | public export
 94 | constructorTag : Named a => Options -> a -> String
 95 | constructorTag o v = o.constructorTagModifier v.nameStr
 96 |
 97 | public export
 98 | constructorTagPrim : Named a => Options -> a -> TTImp
 99 | constructorTagPrim o v = primVal (Str $ constructorTag o v)
100 |
101 | --------------------------------------------------------------------------------
102 | --          Constructors
103 | --------------------------------------------------------------------------------
104 |
105 | public export
106 | data ArgInfo : Type where
107 |   Const  : ArgInfo
108 |   Fields : SnocList (BoundArg 2 RegularNamed) -> ArgInfo
109 |   Values : SnocList (BoundArg 2 Regular) -> ArgInfo
110 |
111 | public export
112 | record DCon where
113 |   constructor DC
114 |   name    : Name
115 |   bound   : TTImp
116 |   applied : TTImp
117 |   tag     : TTImp
118 |   args    : ArgInfo
119 |
120 | argInfo : SnocList (BoundArg 2 Regular) -> ArgInfo
121 | argInfo [<]  = Const
122 | argInfo sx   = maybe (Values sx) Fields $ traverse toNamed sx
123 |
124 | public export
125 | isConst : DCon -> Bool
126 | isConst (DC _ _ _ _ Const) = True
127 | isConst _                  = False
128 |
129 | public export
130 | toRegular : BoundArg n RegularNamed -> BoundArg n Regular
131 | toRegular (BA arg vars prf) = BA arg vars %search
132 |
133 | export
134 | dcon : Options -> Con n vs -> DCon
135 | dcon o c =
136 |   let xs  := freshNames "x" c.arty
137 |       ys  := freshNames "y" c.arty
138 |       bc  := bindCon c xs
139 |       ac  := `(Right ~(applyCon c xs))
140 |       sx  := boundArgs regular c.args [xs,ys]
141 |       tag := constructorTagPrim o c
142 |   in DC c.name bc ac tag $ argInfo sx
143 |