0 | ||| HTTP status codes
  1 | module Pact.WAI.StatusCode
  2 |
  3 | import Derive.Prelude
  4 | import Data.Nat
  5 | import Data.Nat.Order
  6 |
  7 | %language ElabReflection
  8 | %default total
  9 |
 10 | ||| A HTTP status code.
 11 | |||
 12 | ||| The status code is a 3-digit number, the first digit of which
 13 | ||| indicates the class of status code.
 14 | |||
 15 | public export
 16 | record StatusCode where
 17 |   constructor MkStatusCode
 18 |   code : Nat
 19 |   { auto 0 gte100: 100 <= code = True }
 20 |   { auto 0 lte599: code <= 599 = True }
 21 |
 22 | %runElab derive "StatusCode" [Show,Eq,Ord]
 23 |
 24 | public export
 25 | implementation Interpolation StatusCode where
 26 |   interpolate (MkStatusCode code) = show code
 27 |
 28 | public export
 29 | ok : StatusCode
 30 | ok = MkStatusCode 200
 31 |
 32 | public export
 33 | badRequest : StatusCode
 34 | badRequest = MkStatusCode 400
 35 |
 36 | public export
 37 | unauthorized : StatusCode
 38 | unauthorized = MkStatusCode 401
 39 |
 40 | public export
 41 | forbidden : StatusCode
 42 | forbidden = MkStatusCode 403
 43 |
 44 | public export
 45 | notFound : StatusCode
 46 | notFound = MkStatusCode 404
 47 |
 48 | public export
 49 | internalServerError : StatusCode
 50 | internalServerError = MkStatusCode 500
 51 |
 52 |
 53 | ||| 100 - Continue
 54 | public export
 55 | code_100 : StatusCode
 56 | code_100 = MkStatusCode 100
 57 |
 58 | ||| 101 - Switching Protocols
 59 | public export
 60 | code_101 : StatusCode
 61 | code_101 = MkStatusCode 101
 62 |
 63 | ||| 102 - Processing
 64 | public export
 65 | code_102 : StatusCode
 66 | code_102 = MkStatusCode 102
 67 |
 68 | ||| 103 - Early Hints
 69 | public export
 70 | code_103 : StatusCode
 71 | code_103 = MkStatusCode 103
 72 |
 73 |
 74 | ||| 200 - OK
 75 | public export
 76 | code_200 : StatusCode
 77 | code_200 = MkStatusCode 200
 78 |
 79 | ||| 201 - Created
 80 | public export
 81 | code_201 : StatusCode
 82 | code_201 = MkStatusCode 201
 83 |
 84 | ||| 202 - Accepted
 85 | public export
 86 | code_202 : StatusCode
 87 | code_202 = MkStatusCode 202
 88 |
 89 | ||| 203 - Non-Authoritative Information 
 90 | public export
 91 | code_203 : StatusCode
 92 | code_203 = MkStatusCode 203
 93 |
 94 | ||| 204 - No Content
 95 | public export
 96 | code_204 : StatusCode
 97 | code_204 = MkStatusCode 204
 98 |
 99 | ||| 205 - Reset Content
100 | public export
101 | code_205 : StatusCode
102 | code_205 = MkStatusCode 205
103 |
104 | ||| 206 - Partial Content
105 | public export
106 | code_206 : StatusCode
107 | code_206 = MkStatusCode 206
108 |
109 | ||| 207 - Multi-Status
110 | public export
111 | code_207 : StatusCode
112 | code_207 = MkStatusCode 207
113 |
114 | ||| 208 - Already Reported
115 | public export
116 | code_208 : StatusCode
117 | code_208 = MkStatusCode 208
118 |
119 | ||| 226 - IM Used
120 | public export
121 | code_226 : StatusCode
122 | code_226 = MkStatusCode 226
123 |
124 | ||| 300 - Multiple Choices
125 | public export
126 | code_300 : StatusCode
127 | code_300 = MkStatusCode 300
128 |
129 | ||| 301 - Moved Permanently
130 | public export
131 | code_301 : StatusCode
132 | code_301 = MkStatusCode 301
133 |
134 | ||| 302 - Found
135 | public export
136 | code_302 : StatusCode
137 | code_302 = MkStatusCode 302
138 |
139 | ||| 303 - See Other
140 | public export
141 | code_303 : StatusCode
142 | code_303 = MkStatusCode 303
143 |
144 | ||| 304 - Not Modified
145 | public export
146 | code_304 : StatusCode
147 | code_304 = MkStatusCode 304
148 |
149 | ||| 305 - Use Proxy
150 | public export
151 | code_305 : StatusCode
152 | code_305 = MkStatusCode 305
153 |
154 | ||| 307 - Temporary Redirect
155 | public export
156 | code_307 : StatusCode
157 | code_307 = MkStatusCode 307
158 |
159 | ||| 308 - Permanent Redirect
160 | public export
161 | code_308 : StatusCode
162 | code_308 = MkStatusCode 308
163 |
164 | ||| 400 - Bad Request
165 | public export
166 | code_400 : StatusCode
167 | code_400 = MkStatusCode 400
168 |
169 | ||| 401 - Unauthorized
170 | public export
171 | code_401 : StatusCode
172 | code_401 = MkStatusCode 401
173 |
174 | ||| 403 - Forbidden
175 | public export
176 | code_403 : StatusCode
177 | code_403 = MkStatusCode 403
178 |
179 | ||| 404 - Not Found
180 | public export
181 | code_404 : StatusCode
182 | code_404 = MkStatusCode 404
183 |
184 | ||| 405 - Method Not Allowed
185 | public export
186 | code_405 : StatusCode
187 | code_405 = MkStatusCode 405
188 |
189 | ||| 406 - Not Acceptable
190 | public export
191 | code_406 : StatusCode
192 | code_406 = MkStatusCode 406
193 |
194 | ||| 407 - Proxy Authentication Required
195 | public export
196 | code_407 : StatusCode
197 | code_407 = MkStatusCode 407
198 |
199 | ||| 408 - Request Timeout
200 | public export
201 | code_408 : StatusCode
202 | code_408 = MkStatusCode 408
203 |
204 | ||| 409 - Conflict
205 | public export
206 | code_409 : StatusCode
207 | code_409 = MkStatusCode 409
208 |
209 | ||| 410 - Gone
210 | public export
211 | code_410 : StatusCode
212 | code_410 = MkStatusCode 410
213 |
214 | ||| 411 - Length Required
215 | code_411 : StatusCode
216 | code_411 = MkStatusCode 411
217 |
218 | ||| 412 - Precondition Failed
219 | public export
220 | code_412 : StatusCode
221 | code_412 = MkStatusCode 412
222 |
223 | ||| 413 - Payload Too Large
224 | public export
225 | code_413 : StatusCode
226 | code_413 = MkStatusCode 413
227 |
228 | ||| 414 - URI Too Long
229 | public export
230 | code_414 : StatusCode
231 | code_414 = MkStatusCode 414
232 |
233 | ||| 415 - Unsupported Media Type
234 | public export
235 | code_415 : StatusCode
236 | code_415 = MkStatusCode 415
237 |
238 | ||| 416 - Range Not Satisfiable
239 | public export
240 | code_416 : StatusCode
241 | code_416 = MkStatusCode 416
242 |
243 | ||| 417 - Expectation Failed
244 | public export
245 | code_417 : StatusCode
246 | code_417 = MkStatusCode 417
247 |
248 | ||| 418 - I'm a teapot
249 | public export
250 | code_418 : StatusCode
251 | code_418 = MkStatusCode 418
252 |
253 | ||| 421 - Misdirected Request
254 | public export
255 | code_421 : StatusCode
256 | code_421 = MkStatusCode 421
257 |
258 | ||| 422 - Unprocessable Entity
259 | public export
260 | code_422 : StatusCode
261 | code_422 = MkStatusCode 422
262 |
263 | ||| 423 - Locked
264 | public export
265 | code_423 : StatusCode
266 | code_423 = MkStatusCode 423
267 |
268 | ||| 424 - Failed Dependency
269 | public export
270 | code_424 : StatusCode
271 | code_424 = MkStatusCode 424
272 |
273 | ||| 425 - Too Early
274 | public export
275 | code_425 : StatusCode
276 | code_425 = MkStatusCode 425
277 |
278 | ||| 426 - Upgrade Required
279 | public export
280 | code_426 : StatusCode
281 | code_426 = MkStatusCode 426
282 |
283 | ||| 428 - Precondition Required
284 | public export
285 | code_428 : StatusCode
286 | code_428 = MkStatusCode 428
287 |
288 | ||| 429 - Too Many Requests
289 | public export
290 | code_429 : StatusCode
291 | code_429 = MkStatusCode 429
292 |
293 | ||| 431 - Request Header Fields Too Large
294 | public export
295 | code_431 : StatusCode
296 | code_431 = MkStatusCode 431
297 |
298 | ||| 451 - Unavailable For Legal Reasons
299 | public export
300 | code_451 : StatusCode
301 | code_451 = MkStatusCode 451
302 |
303 | ||| 500 - Internal Server Error
304 | public export
305 | code_500 : StatusCode
306 | code_500 = MkStatusCode 500
307 |
308 | ||| 501 - Not Implemented
309 | public export
310 | code_501 : StatusCode
311 | code_501 = MkStatusCode 501
312 |
313 | ||| 502 - Bad Gateway
314 | public export
315 | code_502 : StatusCode
316 | code_502 = MkStatusCode 502
317 |
318 | ||| 503 - Service Unavailable
319 | public export
320 | code_503 : StatusCode
321 | code_503 = MkStatusCode 503
322 |
323 | ||| 504 - Gateway Timeout
324 | public export
325 | code_504 : StatusCode
326 | code_504 = MkStatusCode 504
327 |
328 | ||| 505 - HTTP Version Not Supported
329 | public export
330 | code_505 : StatusCode
331 | code_505 = MkStatusCode 505
332 |
333 | ||| 506 - Variant Also Negotiates
334 | public export
335 | code_506 : StatusCode
336 | code_506 = MkStatusCode 506
337 |
338 | ||| 507 - Insufficient Storage
339 | public export
340 | code_507 : StatusCode
341 | code_507 = MkStatusCode 507
342 |
343 | ||| 508 - Loop Detected
344 | public export
345 | code_508 : StatusCode
346 | code_508 = MkStatusCode 508
347 |
348 | ||| 510 - Not Extended
349 | public export
350 | code_510 : StatusCode
351 | code_510 = MkStatusCode 510
352 |
353 | ||| 511 - Network Authentication Required
354 | public export
355 | code_511 : StatusCode
356 | code_511 = MkStatusCode 511
357 |
358 | ||| Get the status message for a status code
359 | ||| @ code The status code
360 | |||
361 | ||| Returns the status message for the status code
362 | export
363 | statusMessage : StatusCode -> String
364 | statusMessage code = case code of
365 |   (MkStatusCode 100) => "Continue"
366 |   (MkStatusCode 101) => "Switching Protocols"
367 |   (MkStatusCode 102) => "Processing"
368 |   (MkStatusCode 103) => "Early Hints"
369 |   (MkStatusCode 200) => "OK"
370 |   (MkStatusCode 201) => "Created"
371 |   (MkStatusCode 202) => "Accepted"
372 |   (MkStatusCode 203) => "Non-Authoritative Information"
373 |   (MkStatusCode 204) => "No Content"
374 |   (MkStatusCode 205) => "Reset Content"
375 |   (MkStatusCode 206) => "Partial Content"
376 |   (MkStatusCode 207) => "Multi-Status"
377 |   (MkStatusCode 208) => "Already Reported"
378 |   (MkStatusCode 226) => "IM Used"
379 |   (MkStatusCode 300) => "Multiple Choices"
380 |   (MkStatusCode 301) => "Moved Permanently"
381 |   (MkStatusCode 302) => "Found"
382 |   (MkStatusCode 303) => "See Other"
383 |   (MkStatusCode 304) => "Not Modified"
384 |   (MkStatusCode 305) => "Use Proxy"
385 |   (MkStatusCode 307) => "Temporary Redirect"
386 |   (MkStatusCode 308) => "Permanent Redirect"
387 |   (MkStatusCode 400) => "Bad Request"
388 |   (MkStatusCode 401) => "Unauthorized"
389 |   (MkStatusCode 403) => "Forbidden"
390 |   (MkStatusCode 404) => "Not Found"
391 |   (MkStatusCode 405) => "Method Not Allowed"
392 |   (MkStatusCode 406) => "Not Acceptable"
393 |   (MkStatusCode 407) => "Proxy Authentication Required"
394 |   (MkStatusCode 408) => "Request Timeout"
395 |   (MkStatusCode 409) => "Conflict"
396 |   (MkStatusCode 410) => "Gone"
397 |   (MkStatusCode 411) => "Length Required"
398 |   (MkStatusCode 412) => "Precondition Failed"
399 |   (MkStatusCode 413) => "Payload Too Large"
400 |   (MkStatusCode 414) => "URI Too Long"
401 |   (MkStatusCode 415) => "Unsupported Media Type"
402 |   (MkStatusCode 416) => "Range Not Satisfiable"
403 |   (MkStatusCode 417) => "Expectation Failed"
404 |   (MkStatusCode 418) => "I'm a teapot"
405 |   (MkStatusCode 421) => "Misdirected Request"
406 |   (MkStatusCode 422) => "Unprocessable Entity"
407 |   (MkStatusCode 423) => "Locked"
408 |   (MkStatusCode 424) => "Failed Dependency"
409 |   (MkStatusCode 425) => "Too Early"
410 |   (MkStatusCode 426) => "Upgrade Required"
411 |   (MkStatusCode 428) => "Precondition Required"
412 |   (MkStatusCode 429) => "Too Many Requests"
413 |   (MkStatusCode 431) => "Request Header Fields Too Large"
414 |   (MkStatusCode 451) => "Unavailable For Legal Reasons"
415 |   (MkStatusCode 500) => "Internal Server Error"
416 |   (MkStatusCode 501) => "Not Implemented"
417 |   (MkStatusCode 502) => "Bad Gateway"
418 |   (MkStatusCode 503) => "Service Unavailable"
419 |   (MkStatusCode 504) => "Gateway Timeout"
420 |   (MkStatusCode 505) => "HTTP Version Not Supported"
421 |   (MkStatusCode 506) => "Variant Also Negotiates"
422 |   (MkStatusCode 507) => "Insufficient Storage"
423 |   (MkStatusCode 508) => "Loop Detected"
424 |   (MkStatusCode 510) => "Not Extended"
425 |   (MkStatusCode 511) => "Network Authentication Required"
426 |   (MkStatusCode code) => "Unknown Status Code"