diff --git a/src/HTTP.agda b/src/HTTP.agda index 19020bd..14089db 100644 --- a/src/HTTP.agda +++ b/src/HTTP.agda @@ -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 + + diff --git a/src/Main.agda b/src/Main.agda index 621a351..4cbad75 100644 --- a/src/Main.agda +++ b/src/Main.agda @@ -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