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 |   ||| Each field name for which this is true can be omitted
 66 |   ||| and will behave like the value is null. This check
 67 |   ||| occurs before any replacement is done via `fieldNameModifier`
 68 |   replaceMissingKeysWithNull : String -> Bool
 69 |
 70 |   ||| If `True`, single constructor data types will be
 71 |   ||| encoded without a tag for the constructor name.
 72 |   unwrapRecords              : Bool
 73 |
 74 |   ||| This function is used to adjust constructor names
 75 |   ||| during encoding and decoding
 76 |   constructorTagModifier     : String -> String
 77 |
 78 |   ||| This function is used to adjust constructor argument names
 79 |   ||| during encoding and decoding
 80 |   fieldNameModifier          : String -> String
 81 |
 82 | public export
 83 | defaultOptions : Options
 84 | defaultOptions = MkOptions defaultTaggedObject True (const False) True id id
 85 |
 86 | public export
 87 | fieldName : Named a => Options -> a -> String
 88 | fieldName o v = o.fieldNameModifier v.nameStr
 89 |
 90 | public export
 91 | fieldNamePrim : Named a => Options -> a -> TTImp
 92 | fieldNamePrim o v = primVal (Str $ fieldName o v)
 93 |
 94 | public export
 95 | constructorTag : Named a => Options -> a -> String
 96 | constructorTag o v = o.constructorTagModifier v.nameStr
 97 |
 98 | public export
 99 | constructorTagPrim : Named a => Options -> a -> TTImp
100 | constructorTagPrim o v = primVal (Str $ constructorTag o v)
101 |
102 | --------------------------------------------------------------------------------
103 | --          Constructors
104 | --------------------------------------------------------------------------------
105 |
106 | public export
107 | data ArgInfo : Type where
108 |   Const  : ArgInfo
109 |   Fields : SnocList (BoundArg 2 RegularNamed) -> ArgInfo
110 |   Values : SnocList (BoundArg 2 Regular) -> ArgInfo
111 |
112 | public export
113 | record DCon where
114 |   constructor DC
115 |   name    : Name
116 |   bound   : TTImp
117 |   applied : TTImp
118 |   tag     : TTImp
119 |   args    : ArgInfo
120 |
121 | argInfo : SnocList (BoundArg 2 Regular) -> ArgInfo
122 | argInfo [<]  = Const
123 | argInfo sx   = maybe (Values sx) Fields $ traverse toNamed sx
124 |
125 | public export
126 | isConst : DCon -> Bool
127 | isConst (DC _ _ _ _ Const) = True
128 | isConst _                  = False
129 |
130 | public export
131 | toRegular : BoundArg n RegularNamed -> BoundArg n Regular
132 | toRegular (BA arg vars prf) = BA arg vars %search
133 |
134 | export
135 | dcon : Options -> Con n vs -> DCon
136 | dcon o c =
137 |   let xs  := freshNames "x" c.arty
138 |       ys  := freshNames "y" c.arty
139 |       bc  := bindCon c xs
140 |       ac  := `(Right ~(applyCon c xs))
141 |       sx  := boundArgs regular c.args [xs,ys]
142 |       tag := constructorTagPrim o c
143 |   in DC c.name bc ac tag $ argInfo sx
144 |