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 = ⊥
@@ -78,6 +83,12 @@ instance
   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/Main.agda

@@ -73,7 +73,7 @@ module Pages where
         < p >
           "welcome to the " ,
           < span & style ＝ "color: white;" > "index" </ span > ,
-          ((λ q → < span & style ＝ "color: fuchsia;" > " (query = " , q , ")" </ span >) <$> query or-else L.[])
+          (((λ q → < span & style ＝ "color: fuchsia;" > " (query = " , q , ")" </ span >) <$> query) or-else L.[])
           </ p >
       </ body >
     </ html >
@@ -104,7 +104,7 @@ handle sock = do
       (do
         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 ("  target = " S.++ show (req .target))
         putStrLn ("  version = " S.++ show (req .version))
         putStrLn ("  headers = " S.++ show (req .headers))
         case req .content of λ where

src/NonEmpty.agda

@@ -3,6 +3,7 @@ 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
@@ -40,3 +41,9 @@ instance
   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 (<ᵇ⇒<)
@@ -32,7 +34,6 @@ private
 module Parse-URL where
   open import Parse-HTTP.URL
 
-
   -- commonly used sub-parsers
   private
     gen-delims sub-delims reserved unreserved : [ Parser Byte ]
@@ -54,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
@@ -67,34 +73,24 @@ module Parse-URL where
   parse-query = decode-utf8⁺ <$?>′ many (pchar <|>′ any-of "/?")
   parse-fragment = parse-query
 
-  record RequestTarget : Type where
+  parse-absolute-url : [ Parser (Authority × Path) ]
-    field
+  parse-absolute-url =
-      path : Path
+    (parse-scheme >?=′ (_== "http"))
-      query : Maybe String.String
+    <&⃗>□ exact (string-to-ascii-vec "://")
-  open RequestTarget public
+    <&⃗>□ parse-authority
-
+    <&>□ parse-path
-  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
+  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
 
 module Parse-Header where
+  open import Parse-HTTP.URL using (Authority)
+
   record Header : Type where
     field
       name : List⁺ Byte
@@ -105,12 +101,22 @@ module Parse-Header where
     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 List.[] = cake
+  content-length headers =
-  content-length (hdr List.∷ rest) =
+    get-field (string-to-ascii-list⁺ "Content-Length") headers
-    if decode-utf8⁺ (hdr .name) == real "Content-Length"
+    >>= parse-list⁺ number
-      then (λ x → x .result) <$> (number .parse (proj₂ (list⁺-to-vec (hdr .value))))
+
-      else content-length rest
+  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 ]
@@ -141,6 +147,32 @@ 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.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
 
@@ -149,8 +181,7 @@ module Parse-Request where
     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-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)))
@@ -176,7 +207,7 @@ module Parse-Request where
   record Request : Type where
     field
       method : HTTP-Method
-      target : RequestTarget
+      target : URL
       version : HTTP-Version
       headers : List.List Header
       content : Maybe (List.List Byte)
@@ -184,7 +215,8 @@ module Parse-Request where
   parse-request : [ Parser Request ]
   parse-request =
     ((parse-request-line <&⃖>□ crlf) <&>□ many (parse-header <&⃖>□ crlf))
-    >>=′ λ ((method , target , version) , headers) → enbox (
+    >$?=′ find-target
+    >>=′ λ (method , target , version , headers) → enbox (
       case content-length (list⁺-to-list headers) of λ where
         cake →
           (
@@ -202,5 +234,12 @@ module Parse-Request where
             <$>′ (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

@@ -7,6 +7,8 @@ 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
 
@@ -35,13 +37,24 @@ 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-vec : (s : String.String) → {string-is-ascii s} → Vec Byte (String.length s)
-string-to-ascii x {prf} = go (String.toList x)
+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)
 

src/Parse-HTTP/Test.agda

@@ -75,32 +75,37 @@ 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-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" ⟩
+              ≡ 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\n\r\nmjau:)\r\n")
+  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 = record { path = "site" / "index.html" / $ ; query = real "mjau" }
+                   ; target = http:// "agda.nu" ꞉ 80 / ("site" / "index.html" / $) ¿ real "mjau"
                    ; version = HTTP11
                    ; headers =
-                     record { name = vec-to-list⁺ (string-to-ascii "Content-Length") ; value = vec-to-list⁺ (string-to-ascii "6") }
+                     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.[]
-                   ; body = real (Vec.toList (string-to-ascii "mjau:)"))
+                   ; content = real (list⁺-to-list (string-to-ascii-list⁺ "mjau:)"))
                    }
                  , _
                  , enc "\r\n"

src/Parse-HTTP/URL.agda

@@ -1,6 +1,6 @@
 open import Agda.Primitive renaming (Set to Type)
 
-import Data.String as String
+import Data.String as S
 open import Data.Nat
 open import Data.Bool
 
@@ -10,23 +10,30 @@ module Parse-HTTP.URL where
 record Authority : Type where
   constructor _꞉_
   field
-    host : String.String -- TODO: Split out IP:s as a separate type?
+    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
-  _/_ : String.String → Path → Path
+  _/_ : S.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
+  ShowPath .show (p / rest@(_ / _)) = p S.++ "/" S.++ show rest
 
   EqPath : Eq Path
   EqPath ._==_ $        $        = true
@@ -37,17 +44,21 @@ instance
 infixr 5 _/_
 
 record URL : Type where
-  constructor http://_/_¿_#_
+  constructor http://_/_¿_
   field
     authority : Authority
     path : Path
-    query : Maybe String.String
+    query : Maybe S.String
-    fragment : Maybe String.String
 open URL public
 
-infix 0 http://_/_¿_#_
+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" # cake
+  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