Move Response into HTTP
parent
ffb6ffde80
commit
50d8535c50
|
|
@ -2,6 +2,9 @@
|
|||
|
||||
open import Agda.Primitive renaming (Set to Type)
|
||||
|
||||
open import Data.Nat
|
||||
open import Data.Product
|
||||
|
||||
import Data.String as S
|
||||
import Data.List as L
|
||||
open S using (String)
|
||||
|
|
@ -64,6 +67,16 @@ module HTTP-Header where
|
|||
ShowHeader .show hdr = show ⦃ ShowByteList ⦄ (list⁺-to-list (hdr .name)) S.++ ": " S.++ show ⦃ ShowByteList ⦄ (list⁺-to-list (hdr .value))
|
||||
where
|
||||
open Header
|
||||
|
||||
|
||||
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"
|
||||
|
||||
open HTTP-Header public
|
||||
|
||||
module HTTP-Request where
|
||||
|
|
@ -92,3 +105,85 @@ module HTTP-Request where
|
|||
headers : List Header
|
||||
content : Maybe (List Byte)
|
||||
open HTTP-Request public
|
||||
|
||||
module HTTP-Response where
|
||||
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
|
||||
|
||||
encode-response : Response → List Byte
|
||||
encode-response res =
|
||||
UTF-8.encode-string status-line L.++ crlfᵇ L.++
|
||||
encoded-headers L.++ crlfᵇ L.++
|
||||
(proj₂ <$> res .content or-else L.[])
|
||||
where
|
||||
open Response
|
||||
|
||||
crlfᵇ : List Byte
|
||||
crlfᵇ = ASCII.encode-list "\r\n"
|
||||
|
||||
status-line : String
|
||||
status-line = "HTTP/1.1 " S.++ show (res .status-code) S.++ " " S.++ (res .status)
|
||||
|
||||
extra-headers : List Header
|
||||
extra-headers = case res .content of λ where
|
||||
cake → L.[]
|
||||
(real (content-type , content)) →
|
||||
record
|
||||
{ name = ASCII.encode-list⁺ "Content-Type"
|
||||
; value = UTF-8.encode-string (show content-type) ++⁺ ASCII.encode-list⁺ "; charset=utf-8"
|
||||
}
|
||||
L.∷ record
|
||||
{ name = ASCII.encode-list⁺ "Content-Length"
|
||||
; value =
|
||||
list-to-list⁺? (UTF-8.encode-string (show (L.length content)))
|
||||
or-else (ASCII.encode-list⁺ "mjau")
|
||||
}
|
||||
L.∷ L.[]
|
||||
|
||||
encode-header : Header → List Byte
|
||||
encode-header hdr = list⁺-to-list (hdr .name ⁺++⁺ ASCII.encode-list⁺ ": " ⁺++⁺ hdr .value)
|
||||
where
|
||||
open Header
|
||||
|
||||
encoded-headers : List Byte
|
||||
encoded-headers =
|
||||
L.concat (
|
||||
L.map
|
||||
(λ h → encode-header h L.++ crlfᵇ)
|
||||
(res .headers L.++ extra-headers)
|
||||
)
|
||||
|
||||
200-ok : Content-Type → String → Response
|
||||
200-ok content-type content =
|
||||
record
|
||||
{ status-code = 200
|
||||
; status = "OK"
|
||||
; headers = L.[]
|
||||
; content = real (content-type , UTF-8.encode-string content)
|
||||
}
|
||||
|
||||
400-bad-request : Response
|
||||
400-bad-request =
|
||||
record
|
||||
{ status-code = 400
|
||||
; status = "Bad Request"
|
||||
; headers = L.[]
|
||||
; content = real (text/plain , ASCII.encode-list "what is bro doing")
|
||||
}
|
||||
|
||||
404-not-found : Response
|
||||
404-not-found =
|
||||
record
|
||||
{ status-code = 404
|
||||
; status = "Not Found"
|
||||
; headers = L.[]
|
||||
; content = real (text/plain , ASCII.encode-list "not found :(")
|
||||
}
|
||||
|
||||
open HTTP-Response public
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -34,90 +34,6 @@ import HTML.Render
|
|||
import UTF-8
|
||||
import ASCII
|
||||
|
||||
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 HTTP.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ᵇ = ASCII.encode-list "\r\n"
|
||||
|
||||
encode-response : Response → List Byte
|
||||
encode-response res =
|
||||
UTF-8.encode-string 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 (res .status-code) S.++ " " S.++ (res .status)
|
||||
|
||||
extra-headers : List HTTP.Header
|
||||
extra-headers = case res .content of λ where
|
||||
cake → L.[]
|
||||
(real (content-type , content)) →
|
||||
record
|
||||
{ name = ASCII.encode-list⁺ "Content-Type"
|
||||
; value = UTF-8.encode-string (show content-type) ++⁺ ASCII.encode-list⁺ "; charset=utf-8"
|
||||
}
|
||||
L.∷ record
|
||||
{ name = ASCII.encode-list⁺ "Content-Length"
|
||||
; value =
|
||||
list-to-list⁺? (UTF-8.encode-string (show (L.length content)))
|
||||
or-else (ASCII.encode-list⁺ "mjau")
|
||||
}
|
||||
L.∷ L.[]
|
||||
|
||||
encode-header : HTTP.Header → List Byte
|
||||
encode-header hdr = list⁺-to-list (hdr .name ⁺++⁺ ASCII.encode-list⁺ ": " ⁺++⁺ hdr .value)
|
||||
where
|
||||
open HTTP.Header
|
||||
|
||||
encoded-headers : List Byte
|
||||
encoded-headers =
|
||||
L.concat (
|
||||
L.map
|
||||
(λ h → encode-header h L.++ crlfᵇ)
|
||||
(res .headers L.++ extra-headers)
|
||||
)
|
||||
|
||||
200-ok : Content-Type → String → Response
|
||||
200-ok content-type content =
|
||||
record
|
||||
{ status-code = 200
|
||||
; status = "OK"
|
||||
; headers = L.[]
|
||||
; content = real (content-type , UTF-8.encode-string content)
|
||||
}
|
||||
|
||||
400-bad-request : Response
|
||||
400-bad-request =
|
||||
record
|
||||
{ status-code = 400
|
||||
; status = "Bad Request"
|
||||
; headers = L.[]
|
||||
; content = real (text/plain , ASCII.encode-list "what is bro doing")
|
||||
}
|
||||
|
||||
404-not-found : Response
|
||||
404-not-found =
|
||||
record
|
||||
{ status-code = 404
|
||||
; status = "Not Found"
|
||||
; headers = L.[]
|
||||
; content = real (text/plain , ASCII.encode-list "not found :(")
|
||||
}
|
||||
|
||||
module Pages where
|
||||
open HTML
|
||||
|
||||
|
|
@ -146,7 +62,7 @@ module Pages where
|
|||
where
|
||||
open HTML.Syntax
|
||||
|
||||
handle-request : HTTP.Request → IO Response
|
||||
handle-request : HTTP.Request → IO HTTP.Response
|
||||
handle-request req =
|
||||
case req .target .path of λ where
|
||||
($) →
|
||||
|
|
@ -164,9 +80,9 @@ handle-request req =
|
|||
)
|
||||
("index.html" / $) →
|
||||
pure (
|
||||
200-ok text/html (HTML.Render.render-element (Pages.render-index (req .target .query)))
|
||||
HTTP.200-ok HTTP.text/html (HTML.Render.render-element (Pages.render-index (req .target .query)))
|
||||
)
|
||||
_ → pure 404-not-found
|
||||
_ → pure HTTP.404-not-found
|
||||
where
|
||||
open HTTP.Request using (target)
|
||||
open URL
|
||||
|
|
@ -189,12 +105,12 @@ handle sock = do
|
|||
case req .content of λ where
|
||||
(real c) → putStrLn (" content = " S.++ show ⦃ ShowByteList ⦄ c)
|
||||
cake → putStrLn " no content"
|
||||
encode-response <$> handle-request req
|
||||
HTTP.encode-response <$> handle-request req
|
||||
)
|
||||
cake →
|
||||
(do
|
||||
putStrLn "Got an invalid request"
|
||||
encode-response <$> pure 400-bad-request
|
||||
HTTP.encode-response <$> pure HTTP.400-bad-request
|
||||
)
|
||||
where
|
||||
open HTTP.Request
|
||||
|
|
|
|||
Loading…
Reference in New Issue