Response structure

This commit is contained in:
xenia 2023-09-09 12:57:31 +02:00
parent 1ff2708d6e
commit efa96d7e2f

View File

@ -23,41 +23,98 @@ open import NonEmpty
open import Parse-HTTP
open import Parse-HTTP.URL hiding (_/_)
open import Parse-HTTP.Methods
open import Parse-HTTP.Helpers
open import HTML
import HTML.Syntax
import HTML.Render
import UTF-8
response-with-content : S.String String List Byte List Byte
response-with-content status-code status content-type response-data =
UTF-8.encode-string (S.toList (status-line S.++ "\r\n" S.++ headers-lines S.++ "\r\n")) L.++ response-data
data Content-Type : Type where
text/plain text/html : Content-Type
instance
ShowContent-Type : Show Content-Type
ShowContent-Type .show text/plain = "text/plain"
ShowContent-Type .show text/html = "text/html"
record Response : Type where
field
status-code :
status : String
headers : List Header -- all headers besides Content-Type and Content-Length
content : Maybe (Content-Type × List Byte) -- mime type and data
open Response
crlfᵇ : List Byte
crlfᵇ = string-to-ascii-list "\r\n"
encode-response : Response List Byte
encode-response res =
UTF-8.encode-string (S.toList (status-line)) L.++ crlfᵇ L.++
encoded-headers L.++ crlfᵇ L.++
(proj₂ <$> res .content or-else L.[])
where
status-line : String
status-line = "HTTP/1.1 " S.++ show status-code S.++ " " S.++ status
status-line = "HTTP/1.1 " S.++ show (res .status-code) S.++ " " S.++ (res .status)
response-headers : List String
response-headers =
("Content-Type: " S.++ content-type S.++ "; charset=utf-8")
L.∷ ("Content-Length: " S.++ (show (L.length response-data)))
extra-headers : List Header
extra-headers = case res .content of λ where
cake L.[]
(real (content-type , content))
record
{ name = string-to-ascii-list⁺ "Content-Type"
; value = UTF-8.encode-string (S.toList (show content-type)) ++⁺ string-to-ascii-list⁺ "; charset=utf-8"
}
L.∷ record
{ name = string-to-ascii-list⁺ "Content-Length"
; value =
(list-to-list⁺? (UTF-8.encode-string (S.toList (show (L.length content)))))
or-else (string-to-ascii-list⁺ "mjau")
}
L.∷ L.[]
headers-lines : String
headers-lines = L.foldr (λ hdr rest hdr S.++ "\r\n" S.++ rest) "" response-headers
encode-header : Header List Byte
encode-header hdr = list⁺-to-list (hdr .name ⁺++⁺ string-to-ascii-list⁺ ": " ⁺++⁺ hdr .value)
where
open Header
response-without-content : S.String List Byte
response-without-content status-code status =
UTF-8.encode-string (S.toList (
"HTTP/1.1 " S.++ show status-code S.++ " " S.++ status S.++ "\r\n\r\n"
))
encoded-headers : List Byte
encoded-headers =
L.concat (
L.map
(λ h encode-header h L.++ crlfᵇ)
(res .headers L.++ extra-headers)
)
200-ok : S.String List Byte List Byte
200-ok content-type response-data = response-with-content 200 "OK" content-type response-data
200-ok : Content-Type List Byte List Byte
200-ok content-type content =
encode-response
record
{ status-code = 200
; status = "OK"
; headers = L.[]
; content = real (content-type , content)
}
400-bad-request : List Byte
400-bad-request = response-without-content 400 "Bad Request"
400-bad-request =
encode-response
record
{ status-code = 400
; status = "Bad Request"
; headers = L.[]
; content = real (text/plain , string-to-ascii-list "what is bro doing")
}
404-not-found : List Byte
404-not-found = response-with-content 404 "Not Found" "text/plain" (UTF-8.encode-string (S.toList "3: could not find the resource :("))
404-not-found =
encode-response
record
{ status-code = 404
; status = "Not Found"
; headers = L.[]
; content = real (text/plain , string-to-ascii-list "not found :(")
}
module Pages where
open HTML
@ -91,7 +148,7 @@ handle-request req =
if (req .target .path) == ("index.html" / $)
then pure (
200-ok
"text/html"
text/html
(UTF-8.encode-string (S.toList (
HTML.Render.render-element (Pages.render-index (req .target .query))
)))