diff --git a/src/ASCII.agda b/src/ASCII.agda new file mode 100644 index 0000000..15ed2a0 --- /dev/null +++ b/src/ASCII.agda @@ -0,0 +1,50 @@ +open import Agda.Primitive renaming (Set to Type) + +open import Relation.Binary.PropositionalEquality hiding ([_]) + +open import Data.Bool +open import Data.Nat + +import Data.List as L +import Data.Vec as V +import Data.String as S +import Data.Char as C +open L using (List) +open V using (Vec) +open S using (String) +open C using (Char) + +open import Base +open import Bits-and-Bytes +open import NonEmpty + +module ASCII where + +list-is-ascii : List Char → Bool +list-is-ascii L.[] = true +list-is-ascii (c L.∷ chs) = (C.toℕ c <ᵇ 128) ∧ list-is-ascii chs + +string-is-ascii : String → Type +string-is-ascii x = T (list-is-ascii (S.toList x)) + +encode-vec : (s : String) → {string-is-ascii s} → Vec Byte (S.length s) +encode-vec x {prf} = go (S.toList x) + where + go : (l : List Char) → Vec Byte (L.length l) + go L.[] = V.[] + go (ch L.∷ chs) = mkClip (C.toℕ ch) V.∷ go chs + +encode-list⁺ : (s : String) → {string-is-ascii s} → {T (0 <ᵇ S.length s)} → List⁺ Byte +encode-list⁺ s {ascii} {nonempty} = vec-to-list⁺ v + where + open import Data.Nat.Properties + open S + + len≢0 : length s ≢ 0 + len≢0 = m?=′ (_== "http")) - <&⃗>□ exact (string-to-ascii-vec "://") + <&⃗>□ exact (ASCII.encode-vec "://") <&⃗>□ parse-authority <&>□ parse-path @@ -91,17 +90,8 @@ module Parse-URL where open Parse-URL public module Parse-Header where - open import Parse-HTTP.URL using (Authority) - - record Header : Type where - field - name : List⁺ Byte - value : List⁺ Byte - open Header - - instance - ShowHeader : Show Header - ShowHeader .show hdr = show ⦃ ShowByteList ⦄ (list⁺-to-list (hdr .name)) S.++ ": " S.++ show ⦃ ShowByteList ⦄ (list⁺-to-list (hdr .value)) + open import HTTP.URL using (Authority) + open HTTP.Header get-field : List⁺ Byte → List Header → Maybe (List⁺ Byte) get-field field-name L.[] = cake @@ -112,12 +102,12 @@ module Parse-Header where content-length : List Header → Maybe ℕ content-length headers = - get-field (string-to-ascii-list⁺ "Content-Length") headers + get-field (ASCII.encode-list⁺ "Content-Length") headers >>= parse-list⁺ number host : List Header → Maybe Authority host headers = - get-field (string-to-ascii-list⁺ "Host") headers + get-field (ASCII.encode-list⁺ "Host") headers >>= parse-list⁺ parse-authority private @@ -149,18 +139,7 @@ module Parse-Header where open Parse-Header public module Parse-Request where - open import Parse-HTTP.URL - - data RequestTargetPath : Type where - OriginForm : Path → RequestTargetPath - AbsoluteForm : Authority → Path → RequestTargetPath - -- We do not care about authority-form nor asterisk form as we don't do any CONNECT nor OPTIONS requests - - record RequestTarget : Type where - field - path : RequestTargetPath - query : Maybe String - open RequestTarget public + open import HTTP.URL parse-request-target : [ Parser RequestTarget ] parse-request-target = @@ -174,24 +153,16 @@ module Parse-Request where parse-absolute-form = parse-absolute-url >$=′ λ (auth , path) → AbsoluteForm auth path + parse-http-version : [ Parser Version ] + parse-http-version = (λ _ → HTTP11) <$>′ exact (ASCII.encode-vec "HTTP/1.1") - data HTTP-Version : Type where - HTTP11 : HTTP-Version -- we only support 1.1 - - instance - ShowHTTP-Version : Show HTTP-Version - ShowHTTP-Version .show HTTP11 = "HTTP/1.1" - - parse-http-version : [ Parser HTTP-Version ] - parse-http-version = (λ _ → HTTP11) <$>′ exact (string-to-ascii-vec "HTTP/1.1") - - parse-specific-http-method : HTTP-Method → [ Parser HTTP-Method ] + parse-specific-http-method : Method → [ Parser Method ] parse-specific-http-method m = (λ _ → m) <$>′ exact (proj₂ (list⁺-to-vec (name-of-method m))) - parse-http-method : [ Parser HTTP-Method ] + parse-http-method : [ Parser Method ] parse-http-method = foldr (λ m p → parse-specific-http-method m <|>′ p) fail http-methods - parse-request-line : [ Parser (HTTP-Method × RequestTarget × HTTP-Version) ] + parse-request-line : [ Parser (Method × RequestTarget × Version) ] parse-request-line = parse-http-method <&>□ ( @@ -206,13 +177,6 @@ module Parse-Request where ) - record Request : Type where - field - method : HTTP-Method - target : URL - version : HTTP-Version - headers : List Header - content : Maybe (List Byte) parse-request : [ Parser Request ] parse-request = @@ -249,7 +213,7 @@ module Parse-Request where } ) where - find-target : ((HTTP-Method × RequestTarget × HTTP-Version) × List⁺ Header) → Maybe (HTTP-Method × URL × HTTP-Version × List⁺ Header) + find-target : ((Method × RequestTarget × Version) × List⁺ Header) → Maybe (Method × URL × Version × List⁺ Header) find-target ((method , record { path = OriginForm path ; query = query } , ver) , headers) = (λ auth → method , (http:// auth / path ¿ query) , ver , headers) <$> Parse-Header.host (list⁺-to-list headers) find-target ((method , record { path = AbsoluteForm auth path ; query = query } , ver) , headers) = diff --git a/src/Parse-HTTP/Test.agda b/src/HTTP/Test.agda similarity index 81% rename from src/Parse-HTTP/Test.agda rename to src/HTTP/Test.agda index 301137c..f732466 100644 --- a/src/Parse-HTTP/Test.agda +++ b/src/HTTP/Test.agda @@ -14,23 +14,19 @@ open import Base open import Bits-and-Bytes open import Parsing import UTF-8 +import ASCII open import NonEmpty -open import Parse-HTTP -open import Parse-HTTP.Helpers -open import Parse-HTTP.Methods -open import Parse-HTTP.URL +open import HTTP +open import ParseHelpers +open import HTTP.URL +open import HTTP.Parse -module Parse-HTTP.Test where +module HTTP.Test where enc : (s : String) → V.Vec Byte (L.length (UTF-8.encode-string s)) enc x = V.fromList (UTF-8.encode-string x) -module Test-Helpers where - test-percent-encoding : percent-encoded .parse (enc "%69abc") - ≡ real ⟨ < 0x69 > , _ , enc "abc" ⟩ - test-percent-encoding = refl - module Test-HTTP where test-GET : (parse-http-method .parse (enc "GET /mjau.html")) ≡ real ⟨ GET , _ , enc " /mjau.html" ⟩ @@ -97,7 +93,7 @@ module Test-HTTP where test-url = refl test-header : parse-header .parse (enc "Content-Length: 6\r\n") - ≡ real ⟨ record { name = string-to-ascii-list⁺ "Content-Length" ; value = string-to-ascii-list⁺ "6" } , _ , enc "\r\n" ⟩ + ≡ real ⟨ record { name = ASCII.encode-list⁺ "Content-Length" ; value = ASCII.encode-list⁺ "6" } , _ , enc "\r\n" ⟩ test-header = refl test-request : parse-request .parse (enc "POST /site/index.html?mjau HTTP/1.1\r\nContent-Length: 6\r\nHost: agda.nu\r\n\r\nmjau:)\r\n") @@ -107,10 +103,10 @@ module Test-HTTP where ; target = http:// "agda.nu" ꞉ 80 / ("site" / "index.html" / $) ¿ real "mjau" ; version = HTTP11 ; headers = - record { name = string-to-ascii-list⁺ "Content-Length" ; value = string-to-ascii-list⁺ "6" } - L.∷ record { name = string-to-ascii-list⁺ "Host" ; value = string-to-ascii-list⁺ "agda.nu" } + record { name = ASCII.encode-list⁺ "Content-Length" ; value = ASCII.encode-list⁺ "6" } + L.∷ record { name = ASCII.encode-list⁺ "Host" ; value = ASCII.encode-list⁺ "agda.nu" } L.∷ L.[] - ; content = real (string-to-ascii-list "mjau:)") + ; content = real (ASCII.encode-list "mjau:)") } , _ , enc "\r\n" diff --git a/src/Parse-HTTP/URL.agda b/src/HTTP/URL.agda similarity index 98% rename from src/Parse-HTTP/URL.agda rename to src/HTTP/URL.agda index 52ac447..a19a7fe 100644 --- a/src/Parse-HTTP/URL.agda +++ b/src/HTTP/URL.agda @@ -6,7 +6,8 @@ open import Data.Bool open import Base -module Parse-HTTP.URL where +module HTTP.URL where + record Authority : Type where constructor _꞉_ field diff --git a/src/Main.agda b/src/Main.agda index a8f37ed..4dd94c1 100644 --- a/src/Main.agda +++ b/src/Main.agda @@ -20,14 +20,16 @@ open import Socket open import Indexed open import Parsing (Byte) open import NonEmpty -open import Parse-HTTP -open import Parse-HTTP.URL hiding (_/_) -open import Parse-HTTP.Methods -open import Parse-HTTP.Helpers + +import HTTP +import HTTP.Parse +import HTTP.URL as URL open import HTML import HTML.Syntax import HTML.Render + import UTF-8 +import ASCII data Content-Type : Type where text/plain text/html : Content-Type @@ -41,12 +43,12 @@ record Response : Type where field status-code : ℕ status : String - headers : List Header -- all headers besides Content-Type and Content-Length + 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ᵇ = string-to-ascii-list "\r\n" +crlfᵇ = ASCII.encode-list "\r\n" encode-response : Response → List Byte encode-response res = @@ -57,26 +59,26 @@ encode-response res = status-line : String status-line = "HTTP/1.1 " S.++ show (res .status-code) S.++ " " S.++ (res .status) - extra-headers : List Header + extra-headers : List HTTP.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 (show content-type) ++⁺ string-to-ascii-list⁺ "; charset=utf-8" + { name = ASCII.encode-list⁺ "Content-Type" + ; value = UTF-8.encode-string (show content-type) ++⁺ ASCII.encode-list⁺ "; charset=utf-8" } L.∷ record - { name = string-to-ascii-list⁺ "Content-Length" + { name = ASCII.encode-list⁺ "Content-Length" ; value = list-to-list⁺? (UTF-8.encode-string (show (L.length content))) - or-else (string-to-ascii-list⁺ "mjau") + or-else (ASCII.encode-list⁺ "mjau") } L.∷ L.[] - encode-header : Header → List Byte - encode-header hdr = list⁺-to-list (hdr .name ⁺++⁺ string-to-ascii-list⁺ ": " ⁺++⁺ hdr .value) + encode-header : HTTP.Header → List Byte + encode-header hdr = list⁺-to-list (hdr .name ⁺++⁺ ASCII.encode-list⁺ ": " ⁺++⁺ hdr .value) where - open Header + open HTTP.Header encoded-headers : List Byte encoded-headers = @@ -101,7 +103,7 @@ encode-response res = { status-code = 400 ; status = "Bad Request" ; headers = L.[] - ; content = real (text/plain , string-to-ascii-list "what is bro doing") + ; content = real (text/plain , ASCII.encode-list "what is bro doing") } 404-not-found : Response @@ -110,7 +112,7 @@ encode-response res = { status-code = 404 ; status = "Not Found" ; headers = L.[] - ; content = real (text/plain , string-to-ascii-list "not found :(") + ; content = real (text/plain , ASCII.encode-list "not found :(") } module Pages where @@ -129,7 +131,7 @@ module Pages where < span style= "color: yellow;" > "hen" , < span style= "color: fuchsia;" > "ttp" , - < h 3 > "what is this?" , + < h 3 > "what is this?" , < p > "henttp is an HTTP server, HTML DSL and (soon to be) router, written in Agda" @@ -141,7 +143,7 @@ module Pages where where open HTML.Syntax -handle-request : Request → IO Response +handle-request : HTTP.Request → IO Response handle-request req = case req .target .path of λ where ("index.html" / $) → @@ -150,8 +152,9 @@ handle-request req = ) _ → pure 404-not-found where - open Request using (target) - open import Parse-HTTP.URL + open HTTP.Request using (target) + open URL + open import ParseHelpers using (number) handle : Socket → IO (List Byte) @@ -159,7 +162,7 @@ handle sock = do putStrLn "handle: new connection‼" let got = get-bytes sock - case parse-request .parse (V.fromList got) of λ where + case HTTP.Parse.parse-request .parse (V.fromList got) of λ where (real ⟨ req , _ , _ ⟩) → (do putStrLn "handle: got request" @@ -178,7 +181,7 @@ handle sock = do encode-response <$> pure 400-bad-request ) where - open Request + open HTTP.Request run-port : ℕ run-port = 1337 diff --git a/src/Parse-HTTP/Methods.agda b/src/Parse-HTTP/Methods.agda deleted file mode 100644 index 1954115..0000000 --- a/src/Parse-HTTP/Methods.agda +++ /dev/null @@ -1,47 +0,0 @@ -open import Agda.Primitive renaming (Set to Type) -open import Data.Product -open import Data.Nat - -import Data.String as S -open S using (String) - -open import Bits-and-Bytes -open import NonEmpty -open import Base - -open import Parse-HTTP.Helpers - -module Parse-HTTP.Methods where - -data HTTP-Method : Type where - GET HEAD POST PUT DELETE CONNECT OPTIONS TRACE PATCH : HTTP-Method - -instance - ShowMethod : Show HTTP-Method - ShowMethod .show x = go x - where - go : HTTP-Method → String - go GET = "GET" - go HEAD = "HEAD" - go POST = "POST" - go PUT = "PUT" - go DELETE = "DELETE" - go CONNECT = "CONNECT" - go OPTIONS = "OPTIONS" - go TRACE = "TRACE" - go PATCH = "PATCH" - -name-of-method : HTTP-Method → List⁺ Byte -name-of-method GET = string-to-ascii-list⁺ "GET" -name-of-method HEAD = string-to-ascii-list⁺ "HEAD" -name-of-method POST = string-to-ascii-list⁺ "POST" -name-of-method PUT = string-to-ascii-list⁺ "PUT" -name-of-method DELETE = string-to-ascii-list⁺ "DELETE" -name-of-method CONNECT = string-to-ascii-list⁺ "CONNECT" -name-of-method OPTIONS = string-to-ascii-list⁺ "OPTIONS" -name-of-method TRACE = string-to-ascii-list⁺ "TRACE" -name-of-method PATCH = string-to-ascii-list⁺ "PATCH" - -http-methods : List⁺ HTTP-Method -http-methods = GET ∷⁺ HEAD ∷⁺ POST ∷⁺ PUT ∷⁺ DELETE ∷⁺ CONNECT ∷⁺ OPTIONS ∷⁺ TRACE ∷⁺ [ PATCH ]⁺ - diff --git a/src/Parse-HTTP/Helpers.agda b/src/ParseHelpers.agda similarity index 67% rename from src/Parse-HTTP/Helpers.agda rename to src/ParseHelpers.agda index af6966c..65af117 100644 --- a/src/Parse-HTTP/Helpers.agda +++ b/src/ParseHelpers.agda @@ -24,7 +24,7 @@ import UTF-8 open import Parsing (Byte) -module Parse-HTTP.Helpers where +module ParseHelpers where -- Bytes are compared against codepoints, meaning any non-ascii Chars will be death _is_ : Byte → Char → Bool @@ -33,34 +33,6 @@ x is c = x .value == C.toℕ c _between_and_ : Byte → Char → Char → Bool x between a and b = (C.toℕ a ≤ᵇ x .value) ∧ (x .value ≤ᵇ C.toℕ b) -list-is-ascii : List Char → Bool -list-is-ascii L.[] = true -list-is-ascii (c L.∷ chs) = (C.toℕ c <ᵇ 128) ∧ list-is-ascii chs - -string-is-ascii : String → Type -string-is-ascii x = T (list-is-ascii (S.toList x)) - -string-to-ascii-vec : (s : String) → {string-is-ascii s} → Vec Byte (S.length s) -string-to-ascii-vec x {prf} = go (S.toList x) - where - go : (l : List Char) → Vec Byte (L.length l) - go L.[] = V.[] - go (ch L.∷ chs) = mkClip (C.toℕ ch) V.∷ go chs - -string-to-ascii-list⁺ : (s : String) → {string-is-ascii s} → {T (0 <ᵇ S.length s)} → List⁺ Byte -string-to-ascii-list⁺ s {ascii} {nonempty} = vec-to-list⁺ v - where - open import Data.Nat.Properties - open S - - len≢0 : length s ≢ 0 - len≢0 = m′ any₁) <|>′ p) fail (S.toList x)