0 | module HTTP.API.Encode
  1 |
  2 | import Data.List.Quantifiers as L
  3 | import Data.Vect
  4 | import public Data.ByteString
  5 | import public HTTP.Header.Types
  6 | import JSON.Simple
  7 |
  8 | %default total
  9 |
 10 | ||| An interface for encode a value as raw bytes
 11 | |||
 12 | ||| This is used for encoding values in URL paths and query strings
 13 | ||| but - in general - not for encoding value in the message body.
 14 | ||| Use `EncodeVia` for that.
 15 | public export
 16 | interface Encode (0 a : Type) where
 17 |   encode : a -> ByteString
 18 |
 19 | ||| An interface for encoding values as a list of bytestrings.
 20 | public export
 21 | interface EncodeMany (0 a : Type) where
 22 |   encodeMany : a -> List ByteString
 23 |
 24 | export %inline
 25 | Encode a => EncodeMany a where
 26 |   encodeMany v = [encode v]
 27 |
 28 | encodeHL :
 29 |      {auto all : L.All.All (EncodeMany . f) ts}
 30 |   -> L.All.All f ts
 31 |   -> List ByteString
 32 | encodeHL           []      = []
 33 | encodeHL @{_ :: _} (x::xs) = encodeMany x ++ encodeHL xs
 34 |
 35 | export %inline
 36 | L.All.All (EncodeMany . f) ts => EncodeMany (L.All.All f ts) where
 37 |   encodeMany = encodeHL
 38 |
 39 | encodeList : EncodeMany t => List t -> List ByteString
 40 | encodeList []      = []
 41 | encodeList (x::xs) = encodeMany x ++ encodeList xs
 42 |
 43 | export %inline
 44 | EncodeMany a => EncodeMany (Vect n a) where
 45 |   encodeMany = encodeList . toList
 46 |
 47 | export %inline
 48 | EncodeMany a => EncodeMany (List a) where
 49 |   encodeMany = encodeList
 50 |
 51 | export %inline
 52 | EncodeMany a => EncodeMany (SnocList a) where
 53 |   encodeMany = encodeList . (<>> [])
 54 |
 55 | --------------------------------------------------------------------------------
 56 | -- EncodeVia interface
 57 | --------------------------------------------------------------------------------
 58 |
 59 | export %inline
 60 | applicationOctettStream : MediaType
 61 | applicationOctettStream = MT "application" "octett-stream"
 62 |
 63 | export %inline
 64 | applicationJSON : MediaType
 65 | applicationJSON = MT "application" "json"
 66 |
 67 | export %inline
 68 | textPlain : MediaType
 69 | textPlain = MT "text" "plain"
 70 |
 71 | export %inline
 72 | multipartFormData : MediaType
 73 | multipartFormData = MT "multipart" "form-data"
 74 |
 75 | public export
 76 | 0 Text : Type
 77 | Text = String
 78 |
 79 | public export
 80 | 0 Octett : Type
 81 | Octett = ByteString
 82 |
 83 | public export
 84 | 0 OctettList : Type
 85 | OctettList = List ByteString
 86 |
 87 | public export
 88 | interface EncodeVia (0 from, to : Type) where
 89 |   encodeAs : from -> to
 90 |   toBytes  : to -> List ByteString
 91 |   mediaType : MediaType
 92 |
 93 | export %inline
 94 | encodeVia : (v : f) -> EncodeVia f t -> List ByteString
 95 | encodeVia v c = toBytes @{c} $ encodeAs @{c} v
 96 |
 97 | export %inline
 98 | Interpolation a => EncodeVia a String where
 99 |   encodeAs  = interpolate
100 |   toBytes   = pure . fromString
101 |   mediaType = textPlain
102 |
103 | export %inline
104 | Cast a ByteString => EncodeVia a ByteString where
105 |   encodeAs  = cast
106 |   toBytes   = pure
107 |   mediaType = applicationOctettStream
108 |
109 | export %inline
110 | Cast a (List ByteString) => EncodeVia a (List ByteString) where
111 |   encodeAs  = cast
112 |   toBytes   = id
113 |   mediaType = applicationOctettStream
114 |
115 | export %inline
116 | ToJSON a => EncodeVia a JSON where
117 |   encodeAs  = toJSON
118 |   toBytes   = pure . fromString . show
119 |   mediaType = applicationJSON
120 |
121 | --------------------------------------------------------------------------------
122 | -- Implementations
123 | --------------------------------------------------------------------------------
124 |
125 | export %inline
126 | Encode ByteString where encode = id
127 |
128 | export %inline
129 | Encode String where encode = fromString
130 |
131 | export
132 | Encode Nat where
133 |   encode = encode . show
134 |
135 | export
136 | Encode Integer where
137 |   encode = encode. show
138 |
139 | export
140 | Encode Bits8 where
141 |   encode = encode. show
142 |
143 | export
144 | Encode Bits16 where
145 |   encode = encode. show
146 |
147 | export
148 | Encode Bits32 where
149 |   encode = encode. show
150 |
151 | export
152 | Encode Bits64 where
153 |   encode = encode. show
154 |
155 | export
156 | Encode Int8 where
157 |   encode = encode. show
158 |
159 | export
160 | Encode Int16 where
161 |   encode = encode. show
162 |
163 | export
164 | Encode Int32 where
165 |   encode = encode. show
166 |
167 | export
168 | Encode Int64 where
169 |   encode = encode. show
170 |
171 | export
172 | Encode Double where
173 |   encode = encode. show
174 |