From efa96d7e2f4c3085434fe51ce4f735e22b9e0120 Mon Sep 17 00:00:00 2001 From: xenia Date: Sat, 9 Sep 2023 12:57:31 +0200 Subject: [PATCH] Response structure --- src/Main.agda | 99 ++++++++++++++++++++++++++++++++++++++++----------- 1 file changed, 78 insertions(+), 21 deletions(-) diff --git a/src/Main.agda b/src/Main.agda index 95608bb..7318837 100644 --- a/src/Main.agda +++ b/src/Main.agda @@ -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))) - L.∷ L.[] + 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)) )))