2 | module Network.HTTP.Status
5 | import Derive.Prelude
7 | %language ElabReflection
10 | record StatusCodeNumber (n : Nat) where
11 | constructor Abv100Und600
16 | is_status_code_number : (n : Nat) -> Dec (StatusCodeNumber n)
17 | is_status_code_number n =
21 | Yes ok2 => Yes (Abv100Und600 ok1 ok2)
22 | No nope => No (nope . gte100)
23 | No nope => No (nope . lte599)
26 | data StatusCodeClass : Type where
27 | Information : StatusCodeClass
28 | Successful : StatusCodeClass
29 | Redirection : StatusCodeClass
30 | ClientError : StatusCodeClass
31 | ServerError : StatusCodeClass
33 | %runElab derive "StatusCodeClass" [Eq, Show]
36 | data StatusCode : Nat -> Type where
37 | Continue : StatusCode 100
38 | SwitchingProtocols : StatusCode 101
39 | Processing : StatusCode 102
40 | EarlyHints : StatusCode 103
42 | Created : StatusCode 201
43 | Accepted : StatusCode 202
44 | NonAuthoritativeInformation : StatusCode 203
45 | NoContent : StatusCode 204
46 | ResetContent : StatusCode 205
47 | PartialContent : StatusCode 206
48 | MultiStatus : StatusCode 207
49 | AlreadyReported : StatusCode 208
50 | IMUsed : StatusCode 226
51 | MultipleChoices : StatusCode 300
52 | MovedPermanently : StatusCode 301
53 | Found : StatusCode 302
54 | SeeOther : StatusCode 303
55 | NotModified : StatusCode 304
56 | UseProxy : StatusCode 305
57 | TemporaryRedirect : StatusCode 307
58 | PermanentRedirect : StatusCode 308
59 | Unauthorized : StatusCode 401
60 | PaymentRequired : StatusCode 402
61 | Forbidden : StatusCode 403
62 | NotFound : StatusCode 404
63 | MethodNotAllowed : StatusCode 405
64 | NotAcceptable : StatusCode 406
65 | ProxyAuthenticationRequired : StatusCode 407
66 | RequestTimeout : StatusCode 408
67 | Conflict : StatusCode 409
68 | Gone : StatusCode 410
69 | LengthRequired : StatusCode 411
70 | PreconditionFailed : StatusCode 412
71 | ContentTooLarge : StatusCode 413
72 | URITooLong : StatusCode 414
73 | UnsupportedMediaType : StatusCode 415
74 | RangeNotSatisfiable : StatusCode 416
75 | ExpectationFailed : StatusCode 417
76 | MisdirectedRequest : StatusCode 421
77 | UnprocessableContent : StatusCode 422
78 | Locked : StatusCode 423
79 | FailedDependency : StatusCode 424
80 | TooEarly : StatusCode 425
81 | UpgradeRequired : StatusCode 426
82 | PreconditionRequired : StatusCode 428
83 | TooManyRequests : StatusCode 429
84 | RequestHeaderFieldsTooLarge : StatusCode 431
85 | UnavailableForLegalReasons : StatusCode 451
86 | InternalServerError : StatusCode 500
87 | NotImplemented : StatusCode 501
88 | BadGateway : StatusCode 502
89 | ServiceUnavailable : StatusCode 503
90 | GatewayTimeout : StatusCode 504
91 | HTTPVersionNotSupported : StatusCode 505
92 | VariantAlsoNegotiates : StatusCode 506
93 | InsufficientStorage : StatusCode 507
94 | LoopDetected : StatusCode 508
95 | NetworkAuthenticationRequired : StatusCode 511
96 | UnknownStatusCode : (n : Nat) -> StatusCodeNumber n -> StatusCode n
99 | Show (StatusCode n) where
100 | show Continue = "Continue"
101 | show SwitchingProtocols = "SwitchingProtocols"
102 | show Processing = "Processing"
103 | show EarlyHints = "EarlyHints"
105 | show Created = "Created"
106 | show Accepted = "Accepted"
107 | show NonAuthoritativeInformation = "NonAuthoritativeInformation"
108 | show NoContent = "NoContent"
109 | show ResetContent = "ResetContent"
110 | show PartialContent = "PartialContent"
111 | show MultiStatus = "MultiStatus"
112 | show AlreadyReported = "AlreadyReported"
113 | show IMUsed = "IMUsed"
114 | show MultipleChoices = "MultipleChoices"
115 | show MovedPermanently = "MovedPermanently"
116 | show Found = "Found"
117 | show SeeOther = "SeeOther"
118 | show NotModified = "NotModified"
119 | show UseProxy = "UseProxy"
120 | show TemporaryRedirect = "TemporaryRedirect"
121 | show PermanentRedirect = "PermanentRedirect"
122 | show Unauthorized = "Unauthorized"
123 | show PaymentRequired = "PaymentRequired"
124 | show Forbidden = "Forbidden"
125 | show NotFound = "NotFound"
126 | show MethodNotAllowed = "MethodNotAllowed"
127 | show NotAcceptable = "NotAcceptable"
128 | show ProxyAuthenticationRequired = "ProxyAuthenticationRequired"
129 | show RequestTimeout = "RequestTimeout"
130 | show Conflict = "Conflict"
132 | show LengthRequired = "LengthRequired"
133 | show PreconditionFailed = "PreconditionFailed"
134 | show ContentTooLarge = "ContentTooLarge"
135 | show URITooLong = "URITooLong"
136 | show UnsupportedMediaType = "UnsupportedMediaType"
137 | show RangeNotSatisfiable = "RangeNotSatisfiable"
138 | show ExpectationFailed = "ExpectationFailed"
139 | show MisdirectedRequest = "MisdirectedRequest"
140 | show UnprocessableContent = "UnprocessableContent"
141 | show Locked = "Locked"
142 | show FailedDependency = "FailedDependency"
143 | show TooEarly = "TooEarly"
144 | show UpgradeRequired = "UpgradeRequired"
145 | show PreconditionRequired = "PreconditionRequired"
146 | show TooManyRequests = "TooManyRequests"
147 | show RequestHeaderFieldsTooLarge = "RequestHeaderFieldsTooLarge"
148 | show UnavailableForLegalReasons = "UnavailableForLegalReasons"
149 | show InternalServerError = "InternalServerError"
150 | show NotImplemented = "NotImplemented"
151 | show BadGateway = "BadGateway"
152 | show ServiceUnavailable = "ServiceUnavailable"
153 | show GatewayTimeout = "GatewayTimeout"
154 | show HTTPVersionNotSupported = "HTTPVersionNotSupported"
155 | show VariantAlsoNegotiates = "VariantAlsoNegotiates"
156 | show InsufficientStorage = "InsufficientStorage"
157 | show LoopDetected = "LoopDetected"
158 | show NetworkAuthenticationRequired = "NetworkAuthenticationRequired"
159 | show (UnknownStatusCode n _) = "Unknown (" <+> show n <+> ")"
162 | status_code_to_nat : {n : Nat} -> StatusCode n -> Nat
163 | status_code_to_nat _ = n
166 | nat_to_status_code : (n : Nat) -> (prf : StatusCodeNumber n) -> StatusCode n
167 | nat_to_status_code 100 _ = Continue
168 | nat_to_status_code 101 _ = SwitchingProtocols
169 | nat_to_status_code 102 _ = Processing
170 | nat_to_status_code 103 _ = EarlyHints
171 | nat_to_status_code 200 _ = OK
172 | nat_to_status_code 201 _ = Created
173 | nat_to_status_code 202 _ = Accepted
174 | nat_to_status_code 203 _ = NonAuthoritativeInformation
175 | nat_to_status_code 204 _ = NoContent
176 | nat_to_status_code 205 _ = ResetContent
177 | nat_to_status_code 206 _ = PartialContent
178 | nat_to_status_code 207 _ = MultiStatus
179 | nat_to_status_code 208 _ = AlreadyReported
180 | nat_to_status_code 226 _ = IMUsed
181 | nat_to_status_code 300 _ = MultipleChoices
182 | nat_to_status_code 301 _ = MovedPermanently
183 | nat_to_status_code 302 _ = Found
184 | nat_to_status_code 303 _ = SeeOther
185 | nat_to_status_code 304 _ = NotModified
186 | nat_to_status_code 305 _ = UseProxy
187 | nat_to_status_code 307 _ = TemporaryRedirect
188 | nat_to_status_code 308 _ = PermanentRedirect
189 | nat_to_status_code 401 _ = Unauthorized
190 | nat_to_status_code 402 _ = PaymentRequired
191 | nat_to_status_code 403 _ = Forbidden
192 | nat_to_status_code 404 _ = NotFound
193 | nat_to_status_code 405 _ = MethodNotAllowed
194 | nat_to_status_code 406 _ = NotAcceptable
195 | nat_to_status_code 407 _ = ProxyAuthenticationRequired
196 | nat_to_status_code 408 _ = RequestTimeout
197 | nat_to_status_code 409 _ = Conflict
198 | nat_to_status_code 410 _ = Gone
199 | nat_to_status_code 411 _ = LengthRequired
200 | nat_to_status_code 412 _ = PreconditionFailed
201 | nat_to_status_code 413 _ = ContentTooLarge
202 | nat_to_status_code 414 _ = URITooLong
203 | nat_to_status_code 415 _ = UnsupportedMediaType
204 | nat_to_status_code 416 _ = RangeNotSatisfiable
205 | nat_to_status_code 417 _ = ExpectationFailed
206 | nat_to_status_code 421 _ = MisdirectedRequest
207 | nat_to_status_code 422 _ = UnprocessableContent
208 | nat_to_status_code 423 _ = Locked
209 | nat_to_status_code 424 _ = FailedDependency
210 | nat_to_status_code 425 _ = TooEarly
211 | nat_to_status_code 426 _ = UpgradeRequired
212 | nat_to_status_code 428 _ = PreconditionRequired
213 | nat_to_status_code 429 _ = TooManyRequests
214 | nat_to_status_code 431 _ = RequestHeaderFieldsTooLarge
215 | nat_to_status_code 451 _ = UnavailableForLegalReasons
216 | nat_to_status_code 500 _ = InternalServerError
217 | nat_to_status_code 501 _ = NotImplemented
218 | nat_to_status_code 502 _ = BadGateway
219 | nat_to_status_code 503 _ = ServiceUnavailable
220 | nat_to_status_code 504 _ = GatewayTimeout
221 | nat_to_status_code 505 _ = HTTPVersionNotSupported
222 | nat_to_status_code 506 _ = VariantAlsoNegotiates
223 | nat_to_status_code 507 _ = InsufficientStorage
224 | nat_to_status_code 508 _ = LoopDetected
225 | nat_to_status_code 511 _ = NetworkAuthenticationRequired
226 | nat_to_status_code n prf = UnknownStatusCode n prf
229 | status_code_class : {n : Nat} -> StatusCode n -> StatusCodeClass
230 | status_code_class code =
231 | case (status_code_to_nat code) `div` 100 of