Parse full request, including headers and body

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

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 <? 256 of λ where
   (yes v<256) → record { value = v ; in-range = v<256 }

src/Main.agda

@@ -11,29 +11,57 @@ open L using (List)
 open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to _,,,_)
 open import Data.Nat hiding (_<_; _>_)
 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 Parse-HTTP
-open import HTML
+open import Parse-HTTP.URL hiding (_/_)
+open import Parse-HTTP.Methods
+import HTML
 import UTF-8
 
-200-ok : S.String → List Byte → List Byte
+response-with-content : ℕ → S.String → 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 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
+    status-line : 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 = "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
+404-not-found : List Byte
-render-page (path ,,, mquery) =
+404-not-found = response-with-content 404 "Not Found" "text/plain" (UTF-8.encode-string (S.toList "3: could not find the resource :("))
+
+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" </ title > ,
@@ -43,34 +71,45 @@ render-page (path ,,, mquery) =
       < body >
         < h 1 > "hi" </ h 1 > ,
         < p >
-        "you requested " ,
+          "welcome to the " ,
-        < span & style ＝ "color: white;" > show path </ span > ,
+          < span & style ＝ "color: white;" > "index" </ span > ,
-        ((λ q → < span & style ＝ "color: fuchsia;" > "?" , q </ span >) <$> mquery or-else L.[])
+          ((λ q → < span & style ＝ "color: fuchsia;" > " (query = " , q , ")" </ span >) <$> query or-else L.[])
           </ p >
       </ body >
     </ html >
 
-handle-request : (Path × Maybe String) → IO (List Byte)
+handle-request : Request → IO (List Byte)
 handle-request req =
-  pure (
+  if (req .target .path) == ("index.html" / $)
+    then pure (
       200-ok
         "text/html"
         (UTF-8.encode-string (S.toList (
-        render-dom (render-page req)
+          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 parse-request .parse (V.fromList got) of λ where
-
+    (real ⟨ req , _ , _ ⟩) →
-  case parsed of λ where
-    (real ⟨ req@(path ,,, mquery) , _ , _ ⟩) →
       (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

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.++ "⁺"

src/Parse-HTTP.agda

@@ -19,104 +19,20 @@ 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.
+-- helper functions
-data HTTP-Method : Type where
+private
-  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
-
-
-
-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
-
-  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)
 
+module Parse-URL where
+  open import Parse-HTTP.URL
+
+
   -- commonly used sub-parsers
   private
     gen-delims sub-delims reserved unreserved : [ Parser Byte ]
@@ -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) ]
+  record RequestTarget : Type where
-  parse-path-and-query = parse-path <&?>□ (any-of "?" <&⃗>□ parse-query)
+    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 <&>□
+        parse-scheme
-        (any-of ":" <&>□ repeat 2 (any-of "/")) <&⃗>□
+        <&>□ (any-of ":" <&>□ repeat 2 (any-of "/"))
-        parse-authority <&>□
+        <&⃗>□ parse-authority
-        (parse-path <&?>□ (any-of "?" <&⃗>□ parse-query))
+        <&>□ (parse-path <&?>□ (any-of "?" <&⃗>□ parse-query))
         <&?>□ (any-of "#" <&⃗>□ parse-fragment)
 open Parse-URL public
 
-parse-http-version : [ Parser ⊤ ]
+module Parse-Header where
-parse-http-version = (λ _ → tt) <$>′ (exact (< 72 > ∷ < 84 > ∷ < 84 > ∷ < 80 > ∷ < 47 > ∷ []) <&>□ many (digit <|>′ any-of "."))
+  record Header : Type where
+    field
+      name : List⁺ Byte
+      value : List⁺ Byte
+  open Header
 
-parse-get-request : [ Parser (Path × Maybe String.String) ]
+  instance
-parse-get-request =
+    ShowHeader : Show Header
-  parse-specific-http-method GET <&⃗>□
+    ShowHeader .show hdr = show ⦃ ShowByteList ⦄ (list⁺-to-list (hdr .name)) String.++ ": " String.++ show ⦃ ShowByteList ⦄ (list⁺-to-list (hdr .value))
-  spaces <&⃗>□
-  parse-path-and-query <&⃖>□
-  spaces <&>□
-  parse-http-version
 
+  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

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 " "

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 ]⁺
+

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...")
+  test-header : parse-header .parse (enc "Content-Length: 6\r\n")
-           ≡ real ⟨ ( ( "site" / "index.html" / $ ) , real "mjau" ) , _ , enc "\nHeaders..." ⟩
+              ≡ 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
+

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
+