Parse the request line properly

src/Base.agda

@@ -26,6 +26,11 @@ record Monad (M : Type → Type) : Type₁ where
   _<$>_ : {A B : Type} → (A → B) → M A → M B
   f <$> x = x >>= (λ a → pure (f a))
 
+  infixl 5 _>>=_
+  infixl 5 _>>_
+  infixr 4 _<$>_
+
+
 open Monad ⦃...⦄ public
 
 data Maybe (A : Type) : Type where
@@ -38,7 +43,7 @@ _or-else_ : {A : Type} → Maybe A → A → A
 (real x) or-else _ = x
 cake or-else x = x
 
-infix 10 _or-else_
+infix 1 _or-else_
 
 is-real : {A : Type} → Maybe A → Type
 is-real cake = ⊥
@@ -72,6 +77,18 @@ 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
+
+  EqList : {T : Type} → ⦃ Eq T ⦄ → Eq (List T)
+  EqList ._==_ []       []       = true
+  EqList ._==_ (x ∷ xs) (y ∷ ys) = x == y ∧ xs == ys
+  EqList ._==_ (_ ∷ _)  []       = false
+  EqList ._==_ []       (_ ∷ _)  = 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 = " S.++ show (req .target))
+        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,15 @@
-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; []; _∷_)
+open import Data.Bool
+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,8 +28,22 @@ 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.++ "⁺"
     where
       import Data.String as String
+
+  EqList⁺ : {T : Type} → ⦃ Eq T ⦄ → Eq (List⁺ T)
+  EqList⁺ ._==_ [ x ]⁺ [ y ]⁺       = x == y
+  EqList⁺ ._==_ (x ∷⁺ xs) (y ∷⁺ ys) = x == y ∧ xs == ys
+  EqList⁺ ._==_ (_ ∷⁺ _)  [ _ ]⁺    = false
+  EqList⁺ ._==_ [ _ ]⁺    (_ ∷⁺ _)  = false

src/Parse-HTTP.agda

@@ -1,6 +1,8 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+
 open import Agda.Primitive renaming (Set to Type)
 
-open import Data.Vec renaming (map to mapᵥ) hiding ([_]; foldr; foldl)
+open import Data.Vec renaming (map to mapᵥ) hiding ([_]; foldr; foldl; _>>=_)
 import Data.List as List
 open import Data.Nat
 open import Data.Nat.Properties using (<ᵇ⇒<)
@@ -19,104 +21,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
-
-
-
-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 ]
@@ -138,11 +55,16 @@ module Parse-URL where
       reg-name = decode-utf8⁺ <$?>′ (many (unreserved <|>′ percent-encoded <|>′ sub-delims))
 
       unchecked : [ Parser Authority ]
-      unchecked = (λ (host , rest) → host ꞉ (proj₂ <$> rest or-else 80))
+      unchecked = (λ (host , rest) → host ꞉ ((proj₂ <$> rest) or-else 80))
-                  <$>′ (reg-name <&?>′ enbox (any-of ":" <&>′ enbox number))
+                  <$>′ (reg-name <&?>□ any-of ":" <&>□ number)
 
   parse-path : [ Parser Path ]
-  parse-path = foldr (λ (slash , seg) path → seg / path) $ <$>′ (many (any-of "/" <&>′ enbox segment))
+  parse-path =
+      List.foldr (λ (slash , seg) path → seg / path) $ <$>′
+      (
+        (list⁺-to-list <$>′ many (any-of "/" <&>′ enbox segment))
+        <|>′ ((λ _ → List.[]) <$>′ any-of "/")
+      )
     where
       segment : [ Parser String.String ]
       segment = decode-utf8⁺ <$?>′ many pchar
@@ -151,35 +73,173 @@ 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-absolute-url : [ Parser (Authority × Path) ]
-  parse-path-and-query = parse-path <&?>□ (any-of "?" <&⃗>□ parse-query)
+  parse-absolute-url =
+    (parse-scheme >?=′ (_== "http"))
+    <&⃗>□ exact (string-to-ascii-vec "://")
+    <&⃗>□ parse-authority
+    <&>□ parse-path
 
   parse-url : [ Parser URL ]
-  parse-url = enurl <$?>′ parse-parts
+  parse-url =
-    where
+    parse-absolute-url
-      enurl : String.String × Authority × (Path × Maybe String.String) × Maybe String.String → Maybe URL
+    <&?>□ (any-of "?" <&⃗>□ parse-query)
-      enurl (scheme , auth , (path , mquery) , mfrag) =
+    >$=′ λ ((auth , path) , mquery) → http:// auth / path ¿ mquery
-        if true -- scheme == "http"
-          then real (http:// auth / path ¿ mquery # mfrag)
-          else cake
 
-      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)
 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 "."))
+  open import Parse-HTTP.URL using (Authority)
 
-parse-get-request : [ Parser (Path × Maybe String.String) ]
+  record Header : Type where
-parse-get-request =
+    field
-  parse-specific-http-method GET <&⃗>□
+      name : List⁺ Byte
-  spaces <&⃗>□
+      value : List⁺ Byte
-  parse-path-and-query <&⃖>□
+  open Header
-  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))
+
+  get-field : List⁺ Byte → List.List Header → Maybe (List⁺ Byte)
+  get-field field-name List.[] = cake
+  get-field field-name (hdr List.∷ rest) =
+    if hdr .name == field-name
+      then real (hdr .value)
+      else get-field field-name rest
+
+  content-length : List.List Header → Maybe ℕ
+  content-length headers =
+    get-field (string-to-ascii-list⁺ "Content-Length") headers
+    >>= parse-list⁺ number
+
+  host : List.List Header → Maybe Authority
+  host headers =
+    get-field (string-to-ascii-list⁺ "Host") headers
+    >>= parse-list⁺ parse-authority
+
+  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
+  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.String
+  open RequestTarget public
+
+  parse-request-target : [ Parser RequestTarget ]
+  parse-request-target =
+    (parse-origin-form <|>′ parse-absolute-form) <&?>□ (any-of "?" <&⃗>□ parse-query)
+    >$=′ λ (path , query) → record { path = path; query = query }
+    where
+      parse-origin-form parse-absolute-form : [ Parser RequestTargetPath ]
+      parse-origin-form =
+        parse-path >$=′ OriginForm
+
+      parse-absolute-form =
+        parse-absolute-url >$=′ λ (auth , path) → AbsoluteForm auth path
+
+
+  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 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 : URL
+      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))
+    >$?=′ find-target
+    >>=′ λ (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₁))
+          )
+    )
+    where
+      find-target : ((HTTP-Method × RequestTarget × HTTP-Version) × List⁺ Header) → Maybe (HTTP-Method × URL × HTTP-Version × List⁺ Header)
+      find-target ((method , record { path = OriginForm path        ; query = query } , ver) , headers) =
+        Parse-Header.host (list⁺-to-list headers) >>= λ auth →
+          real (method , (http:// auth / path ¿ query) , ver , headers)
+      find-target ((method , record { path = AbsoluteForm auth path ; query = query } , ver) , headers) =
+        real (method , (http:// auth / path ¿ query) , ver , headers)
+
+open Parse-Request public

src/Parse-HTTP/Helpers.agda

@@ -5,6 +5,9 @@ open import Data.Bool hiding (_<_)
 open import Data.Unit
 open import Data.Vec hiding ([_]; foldl)
 import Data.List as List
+open import Data.Product
+
+open import Relation.Binary.PropositionalEquality hiding ([_])
 
 import Data.String as String
 import Data.Char as Char
@@ -27,6 +30,31 @@ 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-vec : (s : String.String) → {string-is-ascii s} → Vec Byte (String.length s)
+string-to-ascii-vec 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
+
+string-to-ascii-list⁺ : (s : String.String) → {string-is-ascii s} → {T (0 <ᵇ String.length s)} → List⁺ Byte
+string-to-ascii-list⁺ s {ascii} {nonempty} = vec-to-list⁺ v
+  where
+    open import Data.Nat.Properties
+
+    len≢0 : String.length s ≢ 0
+    len≢0 = m<n⇒n≢0 (<ᵇ⇒< 0 (String.length s) nonempty)
+
+    v : Vec Byte (suc (pred (String.length s)))
+    v = subst (λ x → Vec Byte x) (sym (suc[pred[n]]≡n {String.length s} len≢0)) (string-to-ascii-vec s {ascii})
+
 any-of : String.String → [ Parser Byte ]
 any-of x = List.foldr (λ ch p → ((_is ch) <?>′ any₁) <|>′ p) fail (String.toList x)
 
@@ -39,7 +67,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
 
@@ -72,18 +75,40 @@ module Test-HTTP where
                               ≡ cake
   test-auth-port-out-of-range = refl
 
-  test-path₁ : parse-path .parse (enc "/mjau/cat.html?meowing=true")
+  test-path : parse-path .parse (enc "/mjau/cat.html?meowing=true")
              ≡ real ⟨ "mjau" / "cat.html" / $ , _ , enc "?meowing=true" ⟩
-  test-path₁ = refl
+  test-path = refl
 
-  test-path₂ : parse-path .parse (enc "/%68%65%77%77%6f/%3f%5e%2f%2f%5e%3f?mjau")
+  test-path-encoded : parse-path .parse (enc "/%68%65%77%77%6f/%3f%5e%2f%2f%5e%3f?mjau")
              ≡ real ⟨ "hewwo" / "?^//^?" / $ , _ , enc "?mjau" ⟩
-  test-path₂ = refl
+  test-path-encoded = refl
 
-  test-url : parse-url .parse (enc "http://www.rfc-editor.org/rfc/rfc3986.html#section-2.1")
+  test-path-bare : parse-path .parse (enc "/")
-           ≡ real ⟨ http:// "www.rfc-editor.org" ꞉ 80 / ("rfc" / "rfc3986.html" / $) ¿ cake # real "section-2.1" , _ , enc "" ⟩
+                 ≡ real ⟨ $ , _ , enc "" ⟩
+  test-path-bare = refl
+
+  test-url : parse-url .parse (enc "http://www.rfc-editor.org/rfc/rfc3986.html")
+           ≡ real ⟨ http:// "www.rfc-editor.org" ꞉ 80 / ("rfc" / "rfc3986.html" / $) ¿ cake , _ , 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 = string-to-ascii-list⁺ "Content-Length" ; value = string-to-ascii-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")
+               ≡ real
+                 ⟨ record
+                   { method = POST
+                   ; 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" }
+                     List.∷ record { name = string-to-ascii-list⁺ "Host" ; value = string-to-ascii-list⁺ "agda.nu" }
+                     List.∷ List.[]
+                   ; content = real (list⁺-to-list (string-to-ascii-list⁺ "mjau:)"))
+                   }
+                 , _
+                 , enc "\r\n"
+                 ⟩
   test-request = refl
+

src/Parse-HTTP/URL.agda

@@ -0,0 +1,64 @@
+open import Agda.Primitive renaming (Set to Type)
+
+import Data.String as S
+open import Data.Nat
+open import Data.Bool
+
+open import Base
+
+module Parse-HTTP.URL where
+record Authority : Type where
+  constructor _꞉_
+  field
+    host : S.String -- TODO: Split out IP:s as a separate type?
+    port : ℕ
+    -- TODO: maybe include {port-in-range} : port < 2 ^ 16
+open Authority public
+
+instance
+  ShowAuthority : Show Authority
+  ShowAuthority .show x =
+    if x .port == 80
+      then x .host
+      else x .host S.++ ":" S.++ show (x .port)
+
+infix 10 _꞉_
+
+data Path : Type where
+  $ : Path -- end
+  _/_ : S.String → Path → Path
+open Path public
+
+instance
+  ShowPath : Show Path
+  ShowPath .show $ = "(empty path)"
+  ShowPath .show (p / $) = p
+  ShowPath .show (p / rest@(_ / _)) = p S.++ "/" S.++ 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 S.String
+open URL public
+
+infix 0 http://_/_¿_
+
+instance
+  ShowURL : Show URL
+  ShowURL .show url =
+    "http://" S.++ show (url .authority) S.++ "/" S.++ show (url .path) S.++ ((λ q → "?" S.++ q) <$> url .query or-else "")
+
+private
+  sample-url : URL
+  sample-url = http:// "coral.shoes" ꞉ 80 / ("pages" / "index.html" / $) ¿ real "key=value"
+

src/Parsing.agda

@@ -28,8 +28,17 @@ open Parse public
 record Parser (A : Type) (n : ℕ) : Type where
   field
     parse : Vec T n → Maybe (Parse A n)
+
 open Parser public
 
+parse-list⁺ : {A : Type} → [ Parser A ] → List⁺ T → Maybe A
+parse-list⁺ p l =
+  p .parse (proj₂ (list⁺-to-vec l))
+  >>= λ parse →
+    if parse .m == 0
+      then pure (parse .result)
+      else cake
+
 -- Parser combinators
 _<$>′_ : {A B : Type} → (A → B) → [ Parser A →′ Parser B ]
 (f <$>′ p) .parse a = do
@@ -136,6 +145,17 @@ _>>=′_ : {A B : Type} → [ Parser A →′ ((k′ A) →′ □ Parser B) →
 _>>′_ : {A B : Type} → [ Parser A →′ □ Parser B →′ Parser B ]
 pa >>′ pb = pa >>=′ λ _ → pb
 
+_>$=′_ : {A B : Type} → [ Parser A →′ k′ (A → B) →′ Parser B ]
+pa >$=′ f = f <$>′ pa
+
+_>?=′_ : {A : Type} → [ Parser A →′ k′ (A → Bool) →′ Parser A ]
+pa >?=′ f = f <?>′ pa
+
+_>$?=′_ : {A B : Type} → [ Parser A →′ k′ (A → Maybe B) →′ Parser B ]
+pa >$?=′ f = f <$?>′ pa
+
+infixl 10 _>>=′_ _>>′_ _>$=′_ _>$?=′_ _>?=′_
+
 fail : {A : Type} → [ Parser A ]
 fail .parse _ = cake