From 7e87f2c8fb56654a4d677295604b503984df7a6c Mon Sep 17 00:00:00 2001 From: xenia Date: Thu, 7 Sep 2023 15:18:42 +0200 Subject: [PATCH] Parse full request, including headers and body --- src/Base.agda | 6 + src/Bits-and-Bytes.agda | 48 +++++++- src/Main.agda | 117 ++++++++++++------ src/NonEmpty.agda | 18 ++- src/Parse-HTTP.agda | 233 ++++++++++++++++++++---------------- src/Parse-HTTP/Helpers.agda | 17 ++- src/Parse-HTTP/Methods.agda | 45 +++++++ src/Parse-HTTP/Test.agda | 24 +++- src/Parse-HTTP/URL.agda | 53 ++++++++ 9 files changed, 410 insertions(+), 151 deletions(-) create mode 100644 src/Parse-HTTP/Methods.agda create mode 100644 src/Parse-HTTP/URL.agda diff --git a/src/Base.agda b/src/Base.agda index a2bf003..e56bb90 100644 --- a/src/Base.agda +++ b/src/Base.agda @@ -72,6 +72,12 @@ instance EqString : Eq Data.String.String EqString ._==_ a b = a Data.String.== b + EqMaybe : {T : Type} → ⦃ Eq T ⦄ → Eq (Maybe T) + EqMaybe ._==_ (real a) (real b) = a == b + EqMaybe ._==_ cake cake = true + EqMaybe ._==_ (real _) cake = false + EqMaybe ._==_ cake (real _) = false + record Show (T : Type) : Type₁ where field show : T → String.String diff --git a/src/Bits-and-Bytes.agda b/src/Bits-and-Bytes.agda index dda854e..823495c 100644 --- a/src/Bits-and-Bytes.agda +++ b/src/Bits-and-Bytes.agda @@ -33,15 +33,61 @@ module bytes where PERCENT = < 37 > BIG = < 0xff > +private + import Data.String as String + import Data.Fin as Fin + import Data.Char as Char + + toHexDigit : ℕ → String.String + toHexDigit 0 = "0" + toHexDigit 1 = "1" + toHexDigit 2 = "2" + toHexDigit 3 = "3" + toHexDigit 4 = "4" + toHexDigit 5 = "5" + toHexDigit 6 = "6" + toHexDigit 7 = "7" + toHexDigit 8 = "8" + toHexDigit 9 = "9" + toHexDigit 10 = "a" + toHexDigit 11 = "b" + toHexDigit 12 = "c" + toHexDigit 13 = "d" + toHexDigit 14 = "e" + toHexDigit 15 = "f" + toHexDigit x = "?" + + toHex : ℕ → String.String + toHex n = toHexDigit (DivMod.quotient divmod) String.++ toHexDigit (Fin.toℕ (DivMod.remainder divmod)) + where + divmod : DivMod n 16 + divmod = n divMod 16 + + instance EqByte : Eq Byte EqByte ._==_ a b = a .value == b .value ShowByte : Show Byte - ShowByte .show x = "< " String.++ show (x .value) String.++ " >" + ShowByte .show x = + if (0x20 ≤ᵇ x .value) ∧ (x .value <ᵇ 0x7f) ∧ not (x .value == 0x60) + then "`" String.++ String.fromChar (Char.fromℕ (x .value)) String.++ "`" + else "<" String.++ toHex (x .value) String.++ ">" where import Data.String as String + import Data.List as List + + ShowByteList : Show (List.List Byte) + ShowByteList .show xs = "'" String.++ show-inner xs String.++ "'" + where + show-inner : List.List Byte → String.String + show-inner List.[] = "" + show-inner (x List.∷ xs) = + if (0x20 ≤ᵇ x .value) ∧ (x .value <ᵇ 0x7f) + then String.fromChar (Char.fromℕ (x .value)) String.++ show-inner xs + else "\\x" String.++ toHex (x .value) String.++ show-inner xs + mkClip : ℕ → Byte mkClip v = case v _) open import Data.Unit using (⊤; tt) +open import Data.Bool open import Base -open import Bits-and-Bytes using (Byte) +open import Bits-and-Bytes using (Byte; ShowByteList) open import SysIO open import Socket open import Indexed open import Parsing (Byte) open import NonEmpty -open import Parse-HTTP hiding (_/_) -open import HTML +open import Parse-HTTP +open import Parse-HTTP.URL hiding (_/_) +open import Parse-HTTP.Methods +import HTML import UTF-8 -200-ok : S.String → List Byte → List Byte -200-ok content-type response-data = UTF-8.encode-string (S.toList (headers S.++ "\r\n\r\n")) L.++ response-data +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 where - headers : String - headers = "HTTP/1.1 200 OK\r\nContent-Type: " S.++ content-type S.++ "; charset=utf-8\r\nContent-Length: " S.++ (show (L.length response-data)) + status-line : String + status-line = "HTTP/1.1 " S.++ show status-code S.++ " " S.++ 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.[] + + headers-lines : String + headers-lines = L.foldr (λ hdr rest → hdr S.++ "\r\n" S.++ rest) "" response-headers + +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" + )) + +200-ok : S.String → List Byte → List Byte +200-ok content-type response-data = response-with-content 200 "OK" content-type response-data 400-bad-request : List Byte -400-bad-request = UTF-8.encode-string (S.toList "400 Bad Request\r\n\r\n") +400-bad-request = response-without-content 400 "Bad Request" -render-page : (Path × Maybe String) → DOM -render-page (path ,,, mquery) = - < html & lang ＝ "en" , style ＝ "color: yellow; background: black; padding: 1em;" > - < head > - < title > "Test page in Agda" , - < meta & name ＝ "description" , content ＝ "Simple webpage rendered in Agda DSL" /> , - < meta & name ＝ "author" , content ＝ "xenia" /> - , - < body > - < h 1 > "hi" , - < p > - "you requested " , - < span & style ＝ "color: white;" > show path , - ((λ q → < span & style ＝ "color: fuchsia;" > "?" , q ) <$> mquery or-else L.[]) - - - +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 :(")) -handle-request : (Path × Maybe String) → IO (List Byte) +module Pages where + open HTML + + render-index : Maybe S.String → HTML.DOM + render-index query = + < html & lang ＝ "en" , style ＝ "color: yellow; background: black; padding: 1em;" > + < head > + < title > "Test page in Agda" , + < meta & name ＝ "description" , content ＝ "Simple webpage rendered in Agda DSL" /> , + < meta & name ＝ "author" , content ＝ "xenia" /> + , + < body > + < h 1 > "hi" , + < p > + "welcome to the " , + < span & style ＝ "color: white;" > "index" , + ((λ q → < span & style ＝ "color: fuchsia;" > " (query = " , q , ")" ) <$> query or-else L.[]) + + + + +handle-request : Request → IO (List Byte) handle-request req = - pure ( - 200-ok - "text/html" - (UTF-8.encode-string (S.toList ( - render-dom (render-page req) - ))) - ) + if (req .target .path) == ("index.html" / $) + then pure ( + 200-ok + "text/html" + (UTF-8.encode-string (S.toList ( + HTML.render-dom (Pages.render-index (req .target .query)) + ))) + ) + else pure 404-not-found + where + open Request using (target) + open import Parse-HTTP.URL + handle : Socket → IO (List Byte) handle sock = do putStrLn "handle: new connection‼" let got = get-bytes sock - let parsed = parse-get-request .parse (V.fromList got) - - case parsed of λ where - (real ⟨ req@(path ,,, mquery) , _ , _ ⟩) → + case parse-request .parse (V.fromList got) of λ where + (real ⟨ req , _ , _ ⟩) → (do - putStrLn ("handle: path = " S.++ show path S.++ ", query = " S.++ mquery or-else "(no query)") + putStrLn "handle: got request" + putStrLn (" method = " S.++ show (req .method)) + putStrLn (" target .path = " S.++ show (req .target .path) S.++ (λ q → ", target .query = " S.++ show q) <$> (req .target .query) or-else "") + putStrLn (" version = " S.++ show (req .version)) + putStrLn (" headers = " S.++ show (req .headers)) + case req .content of λ where + (real c) → putStrLn (" content = " S.++ show ⦃ ShowByteList ⦄ c) + cake → putStrLn " no content" handle-request req ) cake → @@ -78,6 +117,8 @@ handle sock = do putStrLn "Got an invalid request" pure 400-bad-request ) + where + open Request run-port : ℕ run-port = 1337 diff --git a/src/NonEmpty.agda b/src/NonEmpty.agda index d58c5b6..c2a583a 100644 --- a/src/NonEmpty.agda +++ b/src/NonEmpty.agda @@ -1,10 +1,14 @@ -module NonEmpty where - -open import Data.List using (List; []; _∷_) open import Agda.Primitive renaming (Set to Type) +open import Data.Product +open import Data.Nat +open import Data.List using (List; []; _∷_) +import Data.Vec as V + open import Base +module NonEmpty where + data List⁺ (A : Type) : Type where [_]⁺ : A → List⁺ A _∷⁺_ : A → List⁺ A → List⁺ A @@ -23,6 +27,14 @@ list⁺-to-list : {A : Type} → List⁺ A → List A list⁺-to-list [ x ]⁺ = x ∷ [] list⁺-to-list (x ∷⁺ xs) = x ∷ list⁺-to-list xs +list⁺-to-vec : {A : Type} → List⁺ A → Σ ℕ λ n → V.Vec A (suc n) +list⁺-to-vec [ x ]⁺ = 0 , x V.∷ V.[] +list⁺-to-vec (x ∷⁺ xs) = _ , x V.∷ (proj₂ (list⁺-to-vec xs)) + +vec-to-list⁺ : {A : Type} → {n : ℕ} → V.Vec A (suc n) → List⁺ A +vec-to-list⁺ (x V.∷ V.[]) = [ x ]⁺ +vec-to-list⁺ (x V.∷ xs@(_ V.∷ _)) = x ∷⁺ vec-to-list⁺ xs + instance ShowList⁺ : {A : Type} → ⦃ Show A ⦄ → Show (List⁺ A) ShowList⁺ .show x = show (list⁺-to-list x) String.++ "⁺" diff --git a/src/Parse-HTTP.agda b/src/Parse-HTTP.agda index d7c2a85..1869ae5 100644 --- a/src/Parse-HTTP.agda +++ b/src/Parse-HTTP.agda @@ -19,103 +19,19 @@ open import Bits-and-Bytes import UTF-8 open import Parsing (Byte) +open import Parse-HTTP.Methods open import Parse-HTTP.Helpers module Parse-HTTP where --- HTTP Method: GET, POST, etc. -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.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-enc : HTTP-Method → Σ ℕ λ n → Vec Byte (suc n) -name-of-enc GET = _ , < 71 > ∷ < 69 > ∷ < 84 > ∷ [] -name-of-enc HEAD = _ , < 72 > ∷ < 69 > ∷ < 65 > ∷ < 68 > ∷ [] -name-of-enc POST = _ , < 80 > ∷ < 79 > ∷ < 83 > ∷ < 84 > ∷ [] -name-of-enc PUT = _ , < 80 > ∷ < 85 > ∷ < 84 > ∷ [] -name-of-enc DELETE = _ , < 68 > ∷ < 69 > ∷ < 76 > ∷ < 69 > ∷ < 84 > ∷ < 69 > ∷ [] -name-of-enc CONNECT = _ , < 67 > ∷ < 79 > ∷ < 78 > ∷ < 78 > ∷ < 69 > ∷ < 67 > ∷ < 84 > ∷ [] -name-of-enc OPTIONS = _ , < 79 > ∷ < 80 > ∷ < 84 > ∷ < 73 > ∷ < 79 > ∷ < 78 > ∷ < 83 > ∷ [] -name-of-enc TRACE = _ , < 84 > ∷ < 82 > ∷ < 65 > ∷ < 67 > ∷ < 69 > ∷ [] -name-of-enc PATCH = _ , < 80 > ∷ < 65 > ∷ < 84 > ∷ < 67 > ∷ < 72 > ∷ [] - -http-methods : List⁺ HTTP-Method -http-methods = GET ∷⁺ HEAD ∷⁺ POST ∷⁺ PUT ∷⁺ DELETE ∷⁺ CONNECT ∷⁺ OPTIONS ∷⁺ TRACE ∷⁺ [ PATCH ]⁺ - -parse-specific-http-method : HTTP-Method → [ Parser HTTP-Method ] -parse-specific-http-method m = (λ _ → m) <$>′ exact name - where - name-len : ℕ - name-len = proj₁ (name-of-enc m) - name : Vec Byte (suc name-len) - name = proj₂ (name-of-enc m) - - parse-name : [ Parser ⊤ ] - parse-name = exact name - -parse-http-method : [ Parser HTTP-Method ] -parse-http-method = foldl (λ p m → p <|>′ (parse-specific-http-method m)) fail http-methods - - +-- helper functions +private + decode-utf8⁺ : List⁺ Byte → Maybe String.String + decode-utf8⁺ bs = String.fromList <$> UTF-8.decode-string (list⁺-to-list bs) module Parse-URL where - record Authority : Type where - constructor _꞉_ - field - host : String.String -- TODO: Split out IP:s as a separate type? - port : ℕ - -- TODO: maybe include {port-in-range} : port < 2 ^ 16 - open Authority public + open import Parse-HTTP.URL - infix 10 _꞉_ - - data Path : Type where - $ : Path -- end - _/_ : String.String → Path → Path - open Path public - - instance - ShowPath : Show Path - ShowPath .show $ = "(empty path)" - ShowPath .show (p / $) = p - ShowPath .show (p / rest@(_ / _)) = p String.++ "/" String.++ show rest - - infixr 5 _/_ - - record URL : Type where - constructor http://_/_¿_#_ - field - authority : Authority - path : Path - query : Maybe String.String - fragment : Maybe String.String - open URL public - - infix 0 http://_/_¿_#_ - - private - sample-url : URL - sample-url = http:// "coral.shoes" ꞉ 80 / ("pages" / "index.html" / $) ¿ real "key=value" # cake - - -- helper functions - private - - decode-utf8⁺ : List⁺ Byte → Maybe String.String - decode-utf8⁺ bs = String.fromList <$> UTF-8.decode-string (list⁺-to-list bs) -- commonly used sub-parsers private @@ -151,8 +67,14 @@ module Parse-URL where parse-query = decode-utf8⁺ <$?>′ many (pchar <|>′ any-of "/?") parse-fragment = parse-query - parse-path-and-query : [ Parser (Path × Maybe String.String) ] - parse-path-and-query = parse-path <&?>□ (any-of "?" <&⃗>□ parse-query) + record RequestTarget : Type where + field + path : Path + query : Maybe String.String + open RequestTarget public + + parse-request-target : [ Parser RequestTarget ] + parse-request-target = (λ (path , mquery) → record { path = path ; query = mquery }) <$>′ (parse-path <&?>□ (any-of "?" <&⃗>□ parse-query)) parse-url : [ Parser URL ] parse-url = enurl <$?>′ parse-parts @@ -165,21 +87,120 @@ module Parse-URL where parse-parts : [ Parser (String.String × Authority × (Path × Maybe String.String) × Maybe String.String) ] parse-parts = - parse-scheme <&>□ - (any-of ":" <&>□ repeat 2 (any-of "/")) <&⃗>□ - parse-authority <&>□ - (parse-path <&?>□ (any-of "?" <&⃗>□ parse-query)) - <&?>□ (any-of "#" <&⃗>□ parse-fragment) + parse-scheme + <&>□ (any-of ":" <&>□ repeat 2 (any-of "/")) + <&⃗>□ parse-authority + <&>□ (parse-path <&?>□ (any-of "?" <&⃗>□ parse-query)) + <&?>□ (any-of "#" <&⃗>□ parse-fragment) open Parse-URL public -parse-http-version : [ Parser ⊤ ] -parse-http-version = (λ _ → tt) <$>′ (exact (< 72 > ∷ < 84 > ∷ < 84 > ∷ < 80 > ∷ < 47 > ∷ []) <&>□ many (digit <|>′ any-of ".")) +module Parse-Header where + record Header : Type where + field + name : List⁺ Byte + value : List⁺ Byte + open Header -parse-get-request : [ Parser (Path × Maybe String.String) ] -parse-get-request = - parse-specific-http-method GET <&⃗>□ - spaces <&⃗>□ - parse-path-and-query <&⃖>□ - spaces <&>□ - parse-http-version + instance + ShowHeader : Show Header + ShowHeader .show hdr = show ⦃ ShowByteList ⦄ (list⁺-to-list (hdr .name)) String.++ ": " String.++ show ⦃ ShowByteList ⦄ (list⁺-to-list (hdr .value)) + content-length : List.List Header → Maybe ℕ + content-length List.[] = cake + content-length (hdr List.∷ rest) = + if decode-utf8⁺ (hdr .name) == real "Content-Length" + then (λ x → x .result) <$> (number .parse (proj₂ (list⁺-to-vec (hdr .value)))) + else content-length rest + + private + parse-vchar-sp : [ Parser Byte ] + parse-vchar-sp = (λ x → (0x20 ≤ᵇ x .value) ∧ (x .value ≤ᵇ 0x7e)) ′ any₁ + + parse-token : [ Parser (List⁺ Byte) ] + parse-token = many parse-tchar + where + parse-tchar : [ Parser Byte ] + parse-tchar = digit <|>′ letter <|>′ any-of "!#$%&'*+-.^_`|~" + + parse-field-content : [ Parser (List⁺ Byte) ] + parse-field-content = many parse-vchar-sp + + parse-header : [ Parser Header ] + parse-header = + (λ (name , value) → record { name = name ; value = value }) + <$>′ ( + parse-token + <&>□ any-of ":" + <&⃗>□ spaces + <&⃗>□ parse-field-content + ) + + parse-headers⁺ : [ Parser (List⁺ Header) ] + parse-headers⁺ = many parse-header + +open Parse-Header public + +module Parse-Request where + 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 "HTTP/1.1") + + + parse-specific-http-method : HTTP-Method → [ Parser HTTP-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 = foldr (λ m p → parse-specific-http-method m <|>′ p) fail http-methods + + parse-request-line : [ Parser (HTTP-Method × RequestTarget × HTTP-Version) ] + parse-request-line = + parse-http-method + <&>□ ( + spaces + <&⃗>□ ( + parse-request-target + <&>□ ( + spaces + <&⃗>□ parse-http-version + ) + ) + ) + + + record Request : Type where + field + method : HTTP-Method + target : RequestTarget + version : HTTP-Version + headers : List.List Header + content : Maybe (List.List Byte) + + parse-request : [ Parser Request ] + parse-request = + ((parse-request-line <&⃖>□ crlf) <&>□ many (parse-header <&⃖>□ crlf)) + >>=′ λ ((method , target , version) , headers) → enbox ( + case content-length (list⁺-to-list headers) of λ where + cake → + ( + (λ _ → record { method = method; target = target; version = version; headers = list⁺-to-list headers; content = cake }) + <$>′ crlf + ) + (real 0) → + ( + (λ _ → record { method = method; target = target; version = version; headers = list⁺-to-list headers; content = real List.[] }) + <$>′ (crlf <&>□ crlf) + ) + (real n@(suc _)) → + ( + (λ content → record { method = method; target = target; version = version; headers = list⁺-to-list headers; content = real (toList content) }) + <$>′ (crlf <&⃗>□ (repeat n any₁)) + ) + ) + +open Parse-Request public diff --git a/src/Parse-HTTP/Helpers.agda b/src/Parse-HTTP/Helpers.agda index 3d3bf77..6069f7d 100644 --- a/src/Parse-HTTP/Helpers.agda +++ b/src/Parse-HTTP/Helpers.agda @@ -5,6 +5,7 @@ open import Data.Bool hiding (_<_) open import Data.Unit open import Data.Vec hiding ([_]; foldl) import Data.List as List +open import Data.Product import Data.String as String import Data.Char as Char @@ -27,6 +28,20 @@ x is c = x .value == Char.toℕ c _between_and_ : Byte → Char.Char → Char.Char → Bool x between a and b = (Char.toℕ a ≤ᵇ x .value) ∧ (x .value ≤ᵇ Char.toℕ b) +list-is-ascii : List.List Char.Char → Bool +list-is-ascii List.[] = true +list-is-ascii (c List.∷ chs) = (Char.toℕ c <ᵇ 128) ∧ list-is-ascii chs + +string-is-ascii : String.String → Type +string-is-ascii x = T (list-is-ascii (String.toList x)) + +string-to-ascii : (s : String.String) → {string-is-ascii s} → Vec Byte (String.length s) +string-to-ascii x {prf} = go (String.toList x) + where + go : (l : List.List Char.Char) → Vec Byte (List.length l) + go List.[] = [] + go (ch List.∷ chs) = mkClip (Char.toℕ ch) ∷ go chs + any-of : String.String → [ Parser Byte ] any-of x = List.foldr (λ ch p → ((_is ch) ′ any₁) <|>′ p) fail (String.toList x) @@ -39,7 +54,7 @@ letter = uppercase <|>′ lowercase cr lf crlf : [ Parser ⊤ ] cr = (λ _ → tt) <$>′ any-of "\r" lf = (λ _ → tt) <$>′ any-of "\n" -crlf = cr >>′ enbox lf +crlf = (cr >>′ enbox lf) <|>′ lf -- we allow lf because :3 space spaces : [ Parser ⊤ ] space = (λ _ → tt) <$>′ any-of " " diff --git a/src/Parse-HTTP/Methods.agda b/src/Parse-HTTP/Methods.agda new file mode 100644 index 0000000..1fa4243 --- /dev/null +++ b/src/Parse-HTTP/Methods.agda @@ -0,0 +1,45 @@ +open import Agda.Primitive renaming (Set to Type) +import Data.String as String +open import Data.Product +open import Data.Nat +open import Data.Vec + +open import Bits-and-Bytes +open import NonEmpty +open import Base + +module Parse-HTTP.Methods where + +-- HTTP Method: GET, POST, etc. +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.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 = < 71 > ∷⁺ < 69 > ∷⁺ [ < 84 > ]⁺ +name-of-method HEAD = < 72 > ∷⁺ < 69 > ∷⁺ < 65 > ∷⁺ [ < 68 > ]⁺ +name-of-method POST = < 80 > ∷⁺ < 79 > ∷⁺ < 83 > ∷⁺ [ < 84 > ]⁺ +name-of-method PUT = < 80 > ∷⁺ < 85 > ∷⁺ [ < 84 > ]⁺ +name-of-method DELETE = < 68 > ∷⁺ < 69 > ∷⁺ < 76 > ∷⁺ < 69 > ∷⁺ < 84 > ∷⁺ [ < 69 > ]⁺ +name-of-method CONNECT = < 67 > ∷⁺ < 79 > ∷⁺ < 78 > ∷⁺ < 78 > ∷⁺ < 69 > ∷⁺ < 67 > ∷⁺ [ < 84 > ]⁺ +name-of-method OPTIONS = < 79 > ∷⁺ < 80 > ∷⁺ < 84 > ∷⁺ < 73 > ∷⁺ < 79 > ∷⁺ < 78 > ∷⁺ [ < 83 > ]⁺ +name-of-method TRACE = < 84 > ∷⁺ < 82 > ∷⁺ < 65 > ∷⁺ < 67 > ∷⁺ [ < 69 > ]⁺ +name-of-method PATCH = < 80 > ∷⁺ < 65 > ∷⁺ < 84 > ∷⁺ < 67 > ∷⁺ [ < 72 > ]⁺ + +http-methods : List⁺ HTTP-Method +http-methods = GET ∷⁺ HEAD ∷⁺ POST ∷⁺ PUT ∷⁺ DELETE ∷⁺ CONNECT ∷⁺ OPTIONS ∷⁺ TRACE ∷⁺ [ PATCH ]⁺ + diff --git a/src/Parse-HTTP/Test.agda b/src/Parse-HTTP/Test.agda index 35bef46..ec03dff 100644 --- a/src/Parse-HTTP/Test.agda +++ b/src/Parse-HTTP/Test.agda @@ -9,9 +9,12 @@ open import Base open import Bits-and-Bytes open import Parsing open import UTF-8 +open import NonEmpty open import Parse-HTTP open import Parse-HTTP.Helpers +open import Parse-HTTP.Methods +open import Parse-HTTP.URL module Parse-HTTP.Test where @@ -84,6 +87,23 @@ module Test-HTTP where ≡ real ⟨ http:// "www.rfc-editor.org" ꞉ 80 / ("rfc" / "rfc3986.html" / $) ¿ cake # real "section-2.1" , _ , enc "" ⟩ test-url = refl - test-request : parse-get-request .parse (enc "GET /site/index.html?mjau HTTP/1.1\nHeaders...") - ≡ real ⟨ ( ( "site" / "index.html" / $ ) , real "mjau" ) , _ , enc "\nHeaders..." ⟩ + test-header : parse-header .parse (enc "Content-Length: 6\r\n") + ≡ real ⟨ record { name = vec-to-list⁺ (string-to-ascii "Content-Length") ; value = vec-to-list⁺ (string-to-ascii "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\n\r\nmjau:)\r\n") + ≡ real + ⟨ record + { method = POST + ; target = record { path = "site" / "index.html" / $ ; query = real "mjau" } + ; version = HTTP11 + ; headers = + record { name = vec-to-list⁺ (string-to-ascii "Content-Length") ; value = vec-to-list⁺ (string-to-ascii "6") } + List.∷ List.[] + ; body = real (Vec.toList (string-to-ascii "mjau:)")) + } + , _ + , enc "\r\n" + ⟩ test-request = refl + diff --git a/src/Parse-HTTP/URL.agda b/src/Parse-HTTP/URL.agda new file mode 100644 index 0000000..cc6a55f --- /dev/null +++ b/src/Parse-HTTP/URL.agda @@ -0,0 +1,53 @@ +open import Agda.Primitive renaming (Set to Type) + +import Data.String as String +open import Data.Nat +open import Data.Bool + +open import Base + +module Parse-HTTP.URL where +record Authority : Type where + constructor _꞉_ + field + host : String.String -- TODO: Split out IP:s as a separate type? + port : ℕ + -- TODO: maybe include {port-in-range} : port < 2 ^ 16 +open Authority public + +infix 10 _꞉_ + +data Path : Type where + $ : Path -- end + _/_ : String.String → Path → Path +open Path public + +instance + ShowPath : Show Path + ShowPath .show $ = "(empty path)" + ShowPath .show (p / $) = p + ShowPath .show (p / rest@(_ / _)) = p String.++ "/" String.++ show rest + + EqPath : Eq Path + EqPath ._==_ $ $ = true + EqPath ._==_ (p / ps) (q / qs) = p == q ∧ ps == qs + EqPath ._==_ (_ / _) $ = false + EqPath ._==_ $ (_ / _) = false + +infixr 5 _/_ + +record URL : Type where + constructor http://_/_¿_#_ + field + authority : Authority + path : Path + query : Maybe String.String + fragment : Maybe String.String +open URL public + +infix 0 http://_/_¿_#_ + +private + sample-url : URL + sample-url = http:// "coral.shoes" ꞉ 80 / ("pages" / "index.html" / $) ¿ real "key=value" # cake +