src/Base.agda

@@ -26,11 +26,6 @@ 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
@@ -43,7 +38,7 @@ _or-else_ : {A : Type} → Maybe A → A → A
 (real x) or-else _ = x
 cake or-else x = x
 
-infix 1 _or-else_
+infix 10 _or-else_
 
 is-real : {A : Type} → Maybe A → Type
 is-real cake = ⊥
@@ -77,18 +72,6 @@ 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,61 +33,15 @@ 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 =
-    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.++ ">"
+  ShowByte .show x = "< " String.++ show (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,105 +11,66 @@ 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; ShowByteList)
+open import Bits-and-Bytes using (Byte)
 open import SysIO
 open import Socket
 open import Indexed
 open import Parsing (Byte)
 open import NonEmpty
-open import Parse-HTTP
-open import Parse-HTTP.URL hiding (_/_)
-open import Parse-HTTP.Methods
-import HTML
+open import Parse-HTTP hiding (_/_)
+open import HTML
 import UTF-8
 
-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
-    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
+200-ok content-type response-data = UTF-8.encode-string (S.toList (headers S.++ "\r\n\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))
 
 400-bad-request : List Byte
-400-bad-request = response-without-content 400 "Bad Request"
+400-bad-request = UTF-8.encode-string (S.toList "400 Bad Request\r\n\r\n")
 
-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 :("))
+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" </ title > ,
+      < meta & name ＝ "description" , content ＝ "Simple webpage rendered in Agda DSL" /> ,
+      < meta & name ＝ "author" , content ＝ "xenia" />
+    </ head > ,
+    < body >
+      < h 1 > "hi" </ h 1 > ,
+      < p >
+        "you requested " ,
+        < span & style ＝ "color: white;" > show path </ span > ,
+        ((λ q → < span & style ＝ "color: fuchsia;" > "?" , q </ span >) <$> mquery or-else L.[])
+        </ p >
+    </ body >
+  </ html >
 
-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 > ,
-        < meta & name ＝ "description" , content ＝ "Simple webpage rendered in Agda DSL" /> ,
-        < meta & name ＝ "author" , content ＝ "xenia" />
-      </ head > ,
-      < body >
-        < h 1 > "hi" </ h 1 > ,
-        < p >
-          "welcome to the " ,
-          < span & style ＝ "color: white;" > "index" </ span > ,
-          (((λ q → < span & style ＝ "color: fuchsia;" > " (query = " , q , ")" </ span >) <$> query) or-else L.[])
-          </ p >
-      </ body >
-    </ html >
-
-handle-request : Request → IO (List Byte)
+handle-request : (Path × Maybe String) → IO (List Byte)
 handle-request 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
-
+  pure (
+    200-ok
+      "text/html"
+      (UTF-8.encode-string (S.toList (
+        render-dom (render-page req)
+      )))
+  )
 
 handle : Socket → IO (List Byte)
 handle sock = do
   putStrLn "handle: new connection‼"
   let got = get-bytes sock
 
-  case parse-request .parse (V.fromList got) of λ where
-    (real ⟨ req , _ , _ ⟩) →
+  let parsed = parse-get-request .parse (V.fromList got)
+
+  case parsed of λ where
+    (real ⟨ req@(path ,,, mquery) , _ , _ ⟩) →
       (do
-        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"
+        putStrLn ("handle: path = " S.++ show path S.++ ", query = " S.++ mquery or-else "(no query)")
         handle-request req
       )
     cake →
@@ -117,8 +78,6 @@ handle sock = do
         putStrLn "Got an invalid request"
         pure 400-bad-request
       )
-  where
-    open Request
 
 run-port : ℕ
 run-port = 1337

src/NonEmpty.agda

@@ -1,15 +1,10 @@
+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
@@ -28,22 +23,8 @@ 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,8 +1,6 @@
-{-# 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 (<ᵇ⇒<)
@@ -21,18 +19,103 @@ 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
 
--- helper functions
-private
-  decode-utf8⁺ : List⁺ Byte → Maybe String.String
-  decode-utf8⁺ bs = String.fromList <$> UTF-8.decode-string (list⁺-to-list bs)
+-- 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
-  open import Parse-HTTP.URL
+  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)
 
   -- commonly used sub-parsers
   private
@@ -55,16 +138,11 @@ 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))
-                  <$>′ (reg-name <&?>□ any-of ":" <&>□ number)
+      unchecked = (λ (host , rest) → host ꞉ (proj₂ <$> rest or-else 80))
+                  <$>′ (reg-name <&?>′ enbox (any-of ":" <&>′ enbox number))
 
   parse-path : [ Parser Path ]
-  parse-path =
-      List.foldr (λ (slash , seg) path → seg / path) $ <$>′
-      (
-        (list⁺-to-list <$>′ many (any-of "/" <&>′ enbox segment))
-        <|>′ ((λ _ → List.[]) <$>′ any-of "/")
-      )
+  parse-path = foldr (λ (slash , seg) path → seg / path) $ <$>′ (many (any-of "/" <&>′ enbox segment))
     where
       segment : [ Parser String.String ]
       segment = decode-utf8⁺ <$?>′ many pchar
@@ -73,173 +151,35 @@ module Parse-URL where
   parse-query = decode-utf8⁺ <$?>′ many (pchar <|>′ any-of "/?")
   parse-fragment = parse-query
 
-  parse-absolute-url : [ Parser (Authority × Path) ]
-  parse-absolute-url =
-    (parse-scheme >?=′ (_== "http"))
-    <&⃗>□ exact (string-to-ascii-vec "://")
-    <&⃗>□ parse-authority
-    <&>□ parse-path
+  parse-path-and-query : [ Parser (Path × Maybe String.String) ]
+  parse-path-and-query = parse-path <&?>□ (any-of "?" <&⃗>□ parse-query)
 
   parse-url : [ Parser URL ]
-  parse-url =
-    parse-absolute-url
-    <&?>□ (any-of "?" <&⃗>□ parse-query)
-    >$=′ λ ((auth , path) , mquery) → http:// auth / path ¿ mquery
+  parse-url = enurl <$?>′ parse-parts
+    where
+      enurl : String.String × Authority × (Path × Maybe String.String) × Maybe String.String → Maybe URL
+      enurl (scheme , auth , (path , mquery) , mfrag) =
+        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)
+parse-http-version : [ Parser ⊤ ]
+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) ]
+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))
-
-  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,9 +5,6 @@ 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
@@ -30,31 +27,6 @@ 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)
 
@@ -67,7 +39,7 @@ letter = uppercase <|>′ lowercase
 cr lf crlf : [ Parser ⊤ ]
 cr = (λ _ → tt) <$>′ any-of "\r"
 lf = (λ _ → tt) <$>′ any-of "\n"
-crlf = (cr >>′ enbox lf) <|>′ lf -- we allow lf because :3
+crlf = cr >>′ enbox lf
 
 space spaces : [ Parser ⊤ ]
 space = (λ _ → tt) <$>′ any-of " "

src/Parse-HTTP/Methods.agda

@@ -1,45 +0,0 @@
-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,12 +9,9 @@ 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
 
@@ -75,40 +72,18 @@ 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-encoded : parse-path .parse (enc "/%68%65%77%77%6f/%3f%5e%2f%2f%5e%3f?mjau")
+  test-path₂ : parse-path .parse (enc "/%68%65%77%77%6f/%3f%5e%2f%2f%5e%3f?mjau")
              ≡ real ⟨ "hewwo" / "?^//^?" / $ , _ , enc "?mjau" ⟩
-  test-path-encoded = refl
+  test-path₂ = refl
 
-  test-path-bare : parse-path .parse (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 : parse-url .parse (enc "http://www.rfc-editor.org/rfc/rfc3986.html#section-2.1")
+           ≡ real ⟨ http:// "www.rfc-editor.org" ꞉ 80 / ("rfc" / "rfc3986.html" / $) ¿ cake # real "section-2.1" , _ , enc "" ⟩
   test-url = refl
 
-  test-header : parse-header .parse (enc "Content-Length: 6\r\n")
-              ≡ real ⟨ record { name = string-to-ascii-list⁺ "Content-Length" ; value = string-to-ascii-list⁺ "6" } , _ , enc "\r\n" ⟩
-  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 : parse-get-request .parse (enc "GET /site/index.html?mjau HTTP/1.1\nHeaders...")
+           ≡ real ⟨ ( ( "site" / "index.html" / $ ) , real "mjau" ) , _ , enc "\nHeaders..." ⟩
   test-request = refl
-

src/Parse-HTTP/URL.agda

@@ -1,64 +0,0 @@
-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,17 +28,8 @@ 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
@@ -145,17 +136,6 @@ _>>=′_ : {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