0 | module Web.Internal.FetchTypes
  1 |
  2 | import JS
  3 |
  4 | %default total
  5 |
  6 |
  7 | --------------------------------------------------------------------------------
  8 | --          Enums
  9 | --------------------------------------------------------------------------------
 10 |
 11 | namespace RequestDestination
 12 |
 13 |   public export
 14 |   data RequestDestination =
 15 |       Empty
 16 |     | Audio
 17 |     | Audioworklet
 18 |     | Document
 19 |     | Embed
 20 |     | Font
 21 |     | Frame
 22 |     | Iframe
 23 |     | Image
 24 |     | Manifest
 25 |     | Object
 26 |     | Paintworklet
 27 |     | Report
 28 |     | Script
 29 |     | Sharedworker
 30 |     | Style
 31 |     | Track
 32 |     | Video
 33 |     | Worker
 34 |     | Xslt
 35 |
 36 |   public export
 37 |   Show RequestDestination where
 38 |     show Empty = ""
 39 |     show Audio = "audio"
 40 |     show Audioworklet = "audioworklet"
 41 |     show Document = "document"
 42 |     show Embed = "embed"
 43 |     show Font = "font"
 44 |     show Frame = "frame"
 45 |     show Iframe = "iframe"
 46 |     show Image = "image"
 47 |     show Manifest = "manifest"
 48 |     show Object = "object"
 49 |     show Paintworklet = "paintworklet"
 50 |     show Report = "report"
 51 |     show Script = "script"
 52 |     show Sharedworker = "sharedworker"
 53 |     show Style = "style"
 54 |     show Track = "track"
 55 |     show Video = "video"
 56 |     show Worker = "worker"
 57 |     show Xslt = "xslt"
 58 |
 59 |   public export
 60 |   Eq RequestDestination where
 61 |     (==) = (==) `on` show
 62 |
 63 |   public export
 64 |   Ord RequestDestination where
 65 |     compare = compare `on` show
 66 |
 67 |   public export
 68 |   read : String -> Maybe RequestDestination
 69 |   read "" = Just Empty
 70 |   read "audio" = Just Audio
 71 |   read "audioworklet" = Just Audioworklet
 72 |   read "document" = Just Document
 73 |   read "embed" = Just Embed
 74 |   read "font" = Just Font
 75 |   read "frame" = Just Frame
 76 |   read "iframe" = Just Iframe
 77 |   read "image" = Just Image
 78 |   read "manifest" = Just Manifest
 79 |   read "object" = Just Object
 80 |   read "paintworklet" = Just Paintworklet
 81 |   read "report" = Just Report
 82 |   read "script" = Just Script
 83 |   read "sharedworker" = Just Sharedworker
 84 |   read "style" = Just Style
 85 |   read "track" = Just Track
 86 |   read "video" = Just Video
 87 |   read "worker" = Just Worker
 88 |   read "xslt" = Just Xslt
 89 |   read _ = Nothing
 90 |
 91 |   export
 92 |   ToFFI RequestDestination String where
 93 |     toFFI = show
 94 |
 95 |   export
 96 |   FromFFI RequestDestination String where
 97 |     fromFFI = read
 98 |
 99 |
100 | namespace RequestMode
101 |
102 |   public export
103 |   data RequestMode = Navigate | SameOrigin | NoCors | Cors
104 |
105 |   public export
106 |   Show RequestMode where
107 |     show Navigate = "navigate"
108 |     show SameOrigin = "same-origin"
109 |     show NoCors = "no-cors"
110 |     show Cors = "cors"
111 |
112 |   public export
113 |   Eq RequestMode where
114 |     (==) = (==) `on` show
115 |
116 |   public export
117 |   Ord RequestMode where
118 |     compare = compare `on` show
119 |
120 |   public export
121 |   read : String -> Maybe RequestMode
122 |   read "navigate" = Just Navigate
123 |   read "same-origin" = Just SameOrigin
124 |   read "no-cors" = Just NoCors
125 |   read "cors" = Just Cors
126 |   read _ = Nothing
127 |
128 |   export
129 |   ToFFI RequestMode String where
130 |     toFFI = show
131 |
132 |   export
133 |   FromFFI RequestMode String where
134 |     fromFFI = read
135 |
136 |
137 | namespace RequestCredentials
138 |
139 |   public export
140 |   data RequestCredentials = Omit | SameOrigin | Include
141 |
142 |   public export
143 |   Show RequestCredentials where
144 |     show Omit = "omit"
145 |     show SameOrigin = "same-origin"
146 |     show Include = "include"
147 |
148 |   public export
149 |   Eq RequestCredentials where
150 |     (==) = (==) `on` show
151 |
152 |   public export
153 |   Ord RequestCredentials where
154 |     compare = compare `on` show
155 |
156 |   public export
157 |   read : String -> Maybe RequestCredentials
158 |   read "omit" = Just Omit
159 |   read "same-origin" = Just SameOrigin
160 |   read "include" = Just Include
161 |   read _ = Nothing
162 |
163 |   export
164 |   ToFFI RequestCredentials String where
165 |     toFFI = show
166 |
167 |   export
168 |   FromFFI RequestCredentials String where
169 |     fromFFI = read
170 |
171 |
172 | namespace RequestCache
173 |
174 |   public export
175 |   data RequestCache =
176 |       Default
177 |     | NoStore
178 |     | Reload
179 |     | NoCache
180 |     | ForceCache
181 |     | OnlyIfCached
182 |
183 |   public export
184 |   Show RequestCache where
185 |     show Default = "default"
186 |     show NoStore = "no-store"
187 |     show Reload = "reload"
188 |     show NoCache = "no-cache"
189 |     show ForceCache = "force-cache"
190 |     show OnlyIfCached = "only-if-cached"
191 |
192 |   public export
193 |   Eq RequestCache where
194 |     (==) = (==) `on` show
195 |
196 |   public export
197 |   Ord RequestCache where
198 |     compare = compare `on` show
199 |
200 |   public export
201 |   read : String -> Maybe RequestCache
202 |   read "default" = Just Default
203 |   read "no-store" = Just NoStore
204 |   read "reload" = Just Reload
205 |   read "no-cache" = Just NoCache
206 |   read "force-cache" = Just ForceCache
207 |   read "only-if-cached" = Just OnlyIfCached
208 |   read _ = Nothing
209 |
210 |   export
211 |   ToFFI RequestCache String where
212 |     toFFI = show
213 |
214 |   export
215 |   FromFFI RequestCache String where
216 |     fromFFI = read
217 |
218 |
219 | namespace RequestRedirect
220 |
221 |   public export
222 |   data RequestRedirect = Follow | Error | Manual
223 |
224 |   public export
225 |   Show RequestRedirect where
226 |     show Follow = "follow"
227 |     show Error = "error"
228 |     show Manual = "manual"
229 |
230 |   public export
231 |   Eq RequestRedirect where
232 |     (==) = (==) `on` show
233 |
234 |   public export
235 |   Ord RequestRedirect where
236 |     compare = compare `on` show
237 |
238 |   public export
239 |   read : String -> Maybe RequestRedirect
240 |   read "follow" = Just Follow
241 |   read "error" = Just Error
242 |   read "manual" = Just Manual
243 |   read _ = Nothing
244 |
245 |   export
246 |   ToFFI RequestRedirect String where
247 |     toFFI = show
248 |
249 |   export
250 |   FromFFI RequestRedirect String where
251 |     fromFFI = read
252 |
253 |
254 | namespace ResponseType
255 |
256 |   public export
257 |   data ResponseType = Basic | Cors | Default | Error | Opaque | Opaqueredirect
258 |
259 |   public export
260 |   Show ResponseType where
261 |     show Basic = "basic"
262 |     show Cors = "cors"
263 |     show Default = "default"
264 |     show Error = "error"
265 |     show Opaque = "opaque"
266 |     show Opaqueredirect = "opaqueredirect"
267 |
268 |   public export
269 |   Eq ResponseType where
270 |     (==) = (==) `on` show
271 |
272 |   public export
273 |   Ord ResponseType where
274 |     compare = compare `on` show
275 |
276 |   public export
277 |   read : String -> Maybe ResponseType
278 |   read "basic" = Just Basic
279 |   read "cors" = Just Cors
280 |   read "default" = Just Default
281 |   read "error" = Just Error
282 |   read "opaque" = Just Opaque
283 |   read "opaqueredirect" = Just Opaqueredirect
284 |   read _ = Nothing
285 |
286 |   export
287 |   ToFFI ResponseType String where
288 |     toFFI = show
289 |
290 |   export
291 |   FromFFI ResponseType String where
292 |     fromFFI = read
293 |
294 |
295 | namespace ReferrerPolicy
296 |
297 |   public export
298 |   data ReferrerPolicy =
299 |       Empty
300 |     | NoReferrer
301 |     | NoReferrerWhenDowngrade
302 |     | SameOrigin
303 |     | Origin
304 |     | StrictOrigin
305 |     | OriginWhenCrossOrigin
306 |     | StrictOriginWhenCrossOrigin
307 |     | UnsafeUrl
308 |
309 |   public export
310 |   Show ReferrerPolicy where
311 |     show Empty = ""
312 |     show NoReferrer = "no-referrer"
313 |     show NoReferrerWhenDowngrade = "no-referrer-when-downgrade"
314 |     show SameOrigin = "same-origin"
315 |     show Origin = "origin"
316 |     show StrictOrigin = "strict-origin"
317 |     show OriginWhenCrossOrigin = "origin-when-cross-origin"
318 |     show StrictOriginWhenCrossOrigin = "strict-origin-when-cross-origin"
319 |     show UnsafeUrl = "unsafe-url"
320 |
321 |   public export
322 |   Eq ReferrerPolicy where
323 |     (==) = (==) `on` show
324 |
325 |   public export
326 |   Ord ReferrerPolicy where
327 |     compare = compare `on` show
328 |
329 |   public export
330 |   read : String -> Maybe ReferrerPolicy
331 |   read "" = Just Empty
332 |   read "no-referrer" = Just NoReferrer
333 |   read "no-referrer-when-downgrade" = Just NoReferrerWhenDowngrade
334 |   read "same-origin" = Just SameOrigin
335 |   read "origin" = Just Origin
336 |   read "strict-origin" = Just StrictOrigin
337 |   read "origin-when-cross-origin" = Just OriginWhenCrossOrigin
338 |   read "strict-origin-when-cross-origin" = Just StrictOriginWhenCrossOrigin
339 |   read "unsafe-url" = Just UnsafeUrl
340 |   read _ = Nothing
341 |
342 |   export
343 |   ToFFI ReferrerPolicy String where
344 |     toFFI = show
345 |
346 |   export
347 |   FromFFI ReferrerPolicy String where
348 |     fromFFI = read
349 |
350 |
351 |
352 | --------------------------------------------------------------------------------
353 | --          Interfaces
354 | --------------------------------------------------------------------------------
355 |
356 | export data Headers : Type where [external]
357 |
358 | export
359 | ToFFI Headers Headers where toFFI = id
360 |
361 | export
362 | FromFFI Headers Headers where fromFFI = Just
363 |
364 | export
365 | SafeCast Headers where
366 |   safeCast = unsafeCastOnPrototypeName "Headers"
367 |
368 | export data Request : Type where [external]
369 |
370 | export
371 | ToFFI Request Request where toFFI = id
372 |
373 | export
374 | FromFFI Request Request where fromFFI = Just
375 |
376 | export
377 | SafeCast Request where
378 |   safeCast = unsafeCastOnPrototypeName "Request"
379 |
380 | export data Response : Type where [external]
381 |
382 | export
383 | ToFFI Response Response where toFFI = id
384 |
385 | export
386 | FromFFI Response Response where fromFFI = Just
387 |
388 | export
389 | SafeCast Response where
390 |   safeCast = unsafeCastOnPrototypeName "Response"
391 |
392 |
393 | --------------------------------------------------------------------------------
394 | --          Dictionaries
395 | --------------------------------------------------------------------------------
396 |
397 | export data RequestInit : Type where [external]
398 |
399 | export
400 | ToFFI RequestInit RequestInit where toFFI = id
401 |
402 | export
403 | FromFFI RequestInit RequestInit where fromFFI = Just
404 |
405 | export data ResponseInit : Type where [external]
406 |
407 | export
408 | ToFFI ResponseInit ResponseInit where toFFI = id
409 |
410 | export
411 | FromFFI ResponseInit ResponseInit where fromFFI = Just
412 |
413 |
414 | --------------------------------------------------------------------------------
415 | --          Mixins
416 | --------------------------------------------------------------------------------
417 |
418 | export data Body : Type where [external]
419 |
420 | export
421 | ToFFI Body Body where toFFI = id
422 |
423 | export
424 | FromFFI Body Body where fromFFI = Just
425 |