Add redirect to index

src/ASCII.agda

@@ -0,0 +1,50 @@
+open import Agda.Primitive renaming (Set to Type)
+
+open import Relation.Binary.PropositionalEquality hiding ([_])
+
+open import Data.Bool
+open import Data.Nat
+
+import Data.List as L
+import Data.Vec as V
+import Data.String as S
+import Data.Char as C
+open L using (List)
+open V using (Vec)
+open S using (String)
+open C using (Char)
+
+open import Base
+open import Bits-and-Bytes
+open import NonEmpty
+
+module ASCII where
+
+list-is-ascii : List Char → Bool
+list-is-ascii L.[] = true
+list-is-ascii (c L.∷ chs) = (C.toℕ c <ᵇ 128) ∧ list-is-ascii chs
+
+string-is-ascii : String → Type
+string-is-ascii x = T (list-is-ascii (S.toList x))
+
+encode-vec : (s : String) → {string-is-ascii s} → Vec Byte (S.length s)
+encode-vec x {prf} = go (S.toList x)
+  where
+    go : (l : List Char) → Vec Byte (L.length l)
+    go L.[] = V.[]
+    go (ch L.∷ chs) = mkClip (C.toℕ ch) V.∷ go chs
+
+encode-list⁺ : (s : String) → {string-is-ascii s} → {T (0 <ᵇ S.length s)} → List⁺ Byte
+encode-list⁺ s {ascii} {nonempty} = vec-to-list⁺ v
+  where
+    open import Data.Nat.Properties
+    open S
+
+    len≢0 : length s ≢ 0
+    len≢0 = m<n⇒n≢0 (<ᵇ⇒< 0 (length s) nonempty)
+
+    v : Vec Byte (suc (pred (length s)))
+    v = subst (λ x → Vec Byte x) (sym (suc[pred[n]]≡n {length s} len≢0)) (encode-vec s {ascii})
+
+encode-list : (s : String) → {string-is-ascii s} → List Byte
+encode-list s {ascii} = V.toList (encode-vec s {ascii})

src/HTTP.agda

@@ -0,0 +1,94 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+
+open import Agda.Primitive renaming (Set to Type)
+
+import Data.String as S
+import Data.List as L
+open S using (String)
+open L using (List)
+
+open import Base
+
+open import NonEmpty
+open import Bits-and-Bytes
+
+import UTF-8
+import ASCII
+
+open import HTTP.URL
+
+module HTTP where
+
+module HTTP-Method where
+  data Method : Type where
+    GET HEAD POST PUT DELETE CONNECT OPTIONS TRACE PATCH : Method
+
+  instance
+    ShowMethod : Show Method
+    ShowMethod .show x = go x
+      where
+        go : Method → 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 : Method → List⁺ Byte
+  name-of-method GET     = ASCII.encode-list⁺ "GET"
+  name-of-method HEAD    = ASCII.encode-list⁺ "HEAD"
+  name-of-method POST    = ASCII.encode-list⁺ "POST"
+  name-of-method PUT     = ASCII.encode-list⁺ "PUT"
+  name-of-method DELETE  = ASCII.encode-list⁺ "DELETE"
+  name-of-method CONNECT = ASCII.encode-list⁺ "CONNECT"
+  name-of-method OPTIONS = ASCII.encode-list⁺ "OPTIONS"
+  name-of-method TRACE   = ASCII.encode-list⁺ "TRACE"
+  name-of-method PATCH   = ASCII.encode-list⁺ "PATCH"
+
+  http-methods : List⁺ Method
+  http-methods = GET ∷⁺ HEAD ∷⁺ POST ∷⁺ PUT ∷⁺ DELETE ∷⁺ CONNECT ∷⁺ OPTIONS ∷⁺ TRACE ∷⁺ [ PATCH ]⁺
+open HTTP-Method public
+
+module HTTP-Header where
+  record Header : Type where
+    field
+      name : List⁺ Byte
+      value : List⁺ Byte
+
+  instance
+    ShowHeader : Show Header
+    ShowHeader .show hdr = show ⦃ ShowByteList ⦄ (list⁺-to-list (hdr .name)) S.++ ": " S.++ show ⦃ ShowByteList ⦄ (list⁺-to-list (hdr .value))
+      where
+        open Header
+open HTTP-Header public
+
+module HTTP-Request where
+  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
+
+  data Version : Type where
+    HTTP11 : Version -- we only support 1.1
+
+  instance
+    ShowVersion : Show Version
+    ShowVersion .show HTTP11 = "HTTP/1.1"
+
+  record Request : Type where
+    field
+      method : Method
+      target : URL
+      version : Version
+      headers : List Header
+      content : Maybe (List Byte)
+open HTTP-Request public

src/HTTP/Parse.agda

@@ -1,7 +1,3 @@
-{-# OPTIONS --allow-unsolved-metas #-}
-
-open import Agda.Primitive renaming (Set to Type)
-
 open import Data.Nat
 open import Data.Nat.Properties using (<ᵇ⇒<)
 open import Data.Bool hiding (_<_)
@@ -11,22 +7,25 @@ open import Data.Product
 import Data.String as S
 import Data.List as L
 import Data.Vec as V
+import Data.Char as C
 open S using (String)
 open L using (List)
 open V using (Vec)
+open C using (Char)
 
 open import Base
-
-open import Indexed
 open import NonEmpty
 open import Bits-and-Bytes
-import UTF-8
-
+open import Indexed
 open import Parsing (Byte)
-open import Parse-HTTP.Methods
-open import Parse-HTTP.Helpers
 
-module Parse-HTTP where
+open import HTTP
+open import ParseHelpers
+
+import UTF-8
+import ASCII
+
+module HTTP.Parse where
 
 -- helper functions
 private
@@ -34,7 +33,7 @@ private
   decode-utf8⁺ bs = UTF-8.decode-string (list⁺-to-list bs)
 
 module Parse-URL where
-  open import Parse-HTTP.URL
+  open import HTTP.URL
 
   -- commonly used sub-parsers
   private
@@ -78,7 +77,7 @@ module Parse-URL where
   parse-absolute-url : [ Parser (Authority × Path) ]
   parse-absolute-url =
     (parse-scheme >?=′ (_== "http"))
-    <&⃗>□ exact (string-to-ascii-vec "://")
+    <&⃗>□ exact (ASCII.encode-vec "://")
     <&⃗>□ parse-authority
     <&>□ parse-path
 
@@ -91,17 +90,8 @@ module Parse-URL where
 open Parse-URL public
 
 module Parse-Header where
-  open import Parse-HTTP.URL using (Authority)
-
-  record Header : Type where
-    field
-      name : List⁺ Byte
-      value : List⁺ Byte
-  open Header
-
-  instance
-    ShowHeader : Show Header
-    ShowHeader .show hdr = show ⦃ ShowByteList ⦄ (list⁺-to-list (hdr .name)) S.++ ": " S.++ show ⦃ ShowByteList ⦄ (list⁺-to-list (hdr .value))
+  open import HTTP.URL using (Authority)
+  open HTTP.Header
 
   get-field : List⁺ Byte → List Header → Maybe (List⁺ Byte)
   get-field field-name L.[] = cake
@@ -112,12 +102,12 @@ module Parse-Header where
 
   content-length : List Header → Maybe ℕ
   content-length headers =
-    get-field (string-to-ascii-list⁺ "Content-Length") headers
+    get-field (ASCII.encode-list⁺ "Content-Length") headers
     >>= parse-list⁺ number
 
   host : List Header → Maybe Authority
   host headers =
-    get-field (string-to-ascii-list⁺ "Host") headers
+    get-field (ASCII.encode-list⁺ "Host") headers
     >>= parse-list⁺ parse-authority
 
   private
@@ -149,18 +139,7 @@ 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
-  open RequestTarget public
+  open import HTTP.URL
 
   parse-request-target : [ Parser RequestTarget ]
   parse-request-target =
@@ -174,24 +153,16 @@ module Parse-Request where
       parse-absolute-form =
         parse-absolute-url >$=′ λ (auth , path) → AbsoluteForm auth path
 
+  parse-http-version : [ Parser Version ]
+  parse-http-version = (λ _ → HTTP11) <$>′ exact (ASCII.encode-vec "HTTP/1.1")
 
-  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 : Method → [ Parser 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 : [ Parser 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 : [ Parser (Method × RequestTarget × Version) ]
   parse-request-line =
     parse-http-method
     <&>□ (
@@ -206,13 +177,6 @@ module Parse-Request where
     )
 
 
-  record Request : Type where
-    field
-      method : HTTP-Method
-      target : URL
-      version : HTTP-Version
-      headers : List Header
-      content : Maybe (List Byte)
 
   parse-request : [ Parser Request ]
   parse-request =
@@ -249,7 +213,7 @@ module Parse-Request where
               }
     )
     where
-      find-target : ((HTTP-Method × RequestTarget × HTTP-Version) × List⁺ Header) → Maybe (HTTP-Method × URL × HTTP-Version × List⁺ Header)
+      find-target : ((Method × RequestTarget × Version) × List⁺ Header) → Maybe (Method × URL × Version × List⁺ Header)
       find-target ((method , record { path = OriginForm path ; query = query } , ver) , headers) =
         (λ auth → method , (http:// auth / path ¿ query) , ver , headers) <$> Parse-Header.host (list⁺-to-list headers)
       find-target ((method , record { path = AbsoluteForm auth path ; query = query } , ver) , headers) =

src/HTTP/Test.agda

@@ -14,23 +14,19 @@ open import Base
 open import Bits-and-Bytes
 open import Parsing
 import UTF-8
+import ASCII
 open import NonEmpty
 
-open import Parse-HTTP
-open import Parse-HTTP.Helpers
-open import Parse-HTTP.Methods
-open import Parse-HTTP.URL
+open import HTTP
+open import ParseHelpers
+open import HTTP.URL
+open import HTTP.Parse
 
-module Parse-HTTP.Test where
+module HTTP.Test where
 
 enc : (s : String) → V.Vec Byte (L.length (UTF-8.encode-string s))
 enc x = V.fromList (UTF-8.encode-string x)
 
-module Test-Helpers where
-  test-percent-encoding : percent-encoded .parse (enc "%69abc")
-                        ≡ real ⟨ < 0x69 > , _ , enc "abc" ⟩
-  test-percent-encoding = refl
-
 module Test-HTTP where
   test-GET : (parse-http-method .parse (enc "GET /mjau.html"))
                    ≡ real ⟨ GET , _ , enc " /mjau.html" ⟩
@@ -97,7 +93,7 @@ module Test-HTTP where
   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" ⟩
+              ≡ real ⟨ record { name = ASCII.encode-list⁺ "Content-Length" ; value = ASCII.encode-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")
@@ -107,10 +103,10 @@ module Test-HTTP where
                    ; 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" }
-                     L.∷ record { name = string-to-ascii-list⁺ "Host" ; value = string-to-ascii-list⁺ "agda.nu" }
+                     record { name = ASCII.encode-list⁺ "Content-Length" ; value = ASCII.encode-list⁺ "6" }
+                     L.∷ record { name = ASCII.encode-list⁺ "Host" ; value = ASCII.encode-list⁺ "agda.nu" }
                      L.∷ L.[]
-                   ; content = real (string-to-ascii-list "mjau:)")
+                   ; content = real (ASCII.encode-list "mjau:)")
                    }
                  , _
                  , enc "\r\n"

src/HTTP/URL.agda

@@ -6,7 +6,8 @@ open import Data.Bool
 
 open import Base
 
-module Parse-HTTP.URL where
+module HTTP.URL where
+
 record Authority : Type where
   constructor _꞉_
   field

src/Main.agda

@@ -3,11 +3,14 @@
 module main where
 
 open import Agda.Primitive renaming (Set to Type)
+
 import Data.String as S
 import Data.Vec as V
 import Data.List as L
 open S using (String)
 open L using (List)
+open V using (Vec)
+
 open import Data.Product using (_×_; proj₁; proj₂; _,_)
 open import Data.Nat hiding (_<_; _>_)
 open import Data.Unit using (⊤; tt)
@@ -20,14 +23,16 @@ 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
-open import Parse-HTTP.Helpers
+
+import HTTP
+import HTTP.Parse
+import HTTP.URL as URL
 open import HTML
 import HTML.Syntax
 import HTML.Render
+
 import UTF-8
+import ASCII
 
 data Content-Type : Type where
   text/plain text/html : Content-Type
@@ -41,12 +46,12 @@ record Response : Type where
   field
     status-code : ℕ
     status : String
-    headers : List Header -- all headers besides Content-Type and Content-Length
+    headers : List HTTP.Header -- all headers besides Content-Type and Content-Length
     content : Maybe (Content-Type × List Byte) -- mime type and data
 open Response
 
 crlfᵇ : List Byte
-crlfᵇ = string-to-ascii-list "\r\n"
+crlfᵇ = ASCII.encode-list "\r\n"
 
 encode-response : Response → List Byte
 encode-response res =
@@ -57,26 +62,26 @@ encode-response res =
     status-line : String
     status-line = "HTTP/1.1 " S.++ show (res .status-code) S.++ " " S.++ (res .status)
 
-    extra-headers : List Header
+    extra-headers : List HTTP.Header
     extra-headers = case res .content of λ where
       cake → L.[]
       (real (content-type , content)) →
         record
-          { name = string-to-ascii-list⁺ "Content-Type"
-          ; value = UTF-8.encode-string (show content-type) ++⁺ string-to-ascii-list⁺ "; charset=utf-8"
+          { name = ASCII.encode-list⁺ "Content-Type"
+          ; value = UTF-8.encode-string (show content-type) ++⁺ ASCII.encode-list⁺ "; charset=utf-8"
           }
         L.∷ record
-          { name = string-to-ascii-list⁺ "Content-Length"
+          { name = ASCII.encode-list⁺ "Content-Length"
           ; value =
             list-to-list⁺? (UTF-8.encode-string (show (L.length content)))
-            or-else (string-to-ascii-list⁺ "mjau")
+            or-else (ASCII.encode-list⁺ "mjau")
           }
         L.∷ L.[]
 
-    encode-header : Header → List Byte
-    encode-header hdr = list⁺-to-list (hdr .name ⁺++⁺ string-to-ascii-list⁺ ": " ⁺++⁺ hdr .value)
+    encode-header : HTTP.Header → List Byte
+    encode-header hdr = list⁺-to-list (hdr .name ⁺++⁺ ASCII.encode-list⁺ ": " ⁺++⁺ hdr .value)
       where
-        open Header
+        open HTTP.Header
 
     encoded-headers : List Byte
     encoded-headers =
@@ -101,7 +106,7 @@ encode-response res =
   { status-code = 400
   ; status = "Bad Request"
   ; headers = L.[]
-  ; content = real (text/plain , string-to-ascii-list "what is bro doing")
+  ; content = real (text/plain , ASCII.encode-list "what is bro doing")
   }
 
 404-not-found : Response
@@ -110,7 +115,7 @@ encode-response res =
   { status-code = 404
   ; status = "Not Found"
   ; headers = L.[]
-  ; content = real (text/plain , string-to-ascii-list "not found :(")
+  ; content = real (text/plain , ASCII.encode-list "not found :(")
   }
 
 module Pages where
@@ -129,7 +134,7 @@ module Pages where
           < span style= "color: yellow;" > "hen" </ span > ,
           < span style= "color: fuchsia;" > "ttp" </ span >
         </ h 1 > ,
-        < h 3 > "what is this?" </ h 1 > ,
+        < h 3 > "what is this?" </ h 3 > ,
         < p >
           "henttp is an HTTP server, HTML DSL and (soon to be) router, written in Agda"
         </ p >
@@ -141,17 +146,31 @@ module Pages where
     where
       open HTML.Syntax
 
-handle-request : Request → IO Response
+handle-request : HTTP.Request → IO Response
 handle-request req =
   case req .target .path of λ where
+    ($) →
+      pure (
+        record
+          { status-code = 302
+          ; status = "Found"
+          ; headers =
+            record
+              { name = ASCII.encode-list⁺ "Location"
+              ; value = ASCII.encode-list⁺ ("/" S.++ show ("index.html" / $))
+              } L.∷ L.[]
+          ; content = cake
+          }
+      )
     ("index.html" / $) →
       pure (
         200-ok text/html (HTML.Render.render-element (Pages.render-index (req .target .query)))
       )
     _ → pure 404-not-found
   where
-    open Request using (target)
-    open import Parse-HTTP.URL
+    open HTTP.Request using (target)
+    open URL
+    open import ParseHelpers using (number)
 
 
 handle : Socket → IO (List Byte)
@@ -159,7 +178,7 @@ handle sock = do
   putStrLn "handle: new connection‼"
   let got = get-bytes sock
 
-  case parse-request .parse (V.fromList got) of λ where
+  case HTTP.Parse.parse-request .parse (V.fromList got) of λ where
     (real ⟨ req , _ , _ ⟩) →
       (do
         putStrLn "handle: got request"
@@ -178,7 +197,7 @@ handle sock = do
         encode-response <$> pure 400-bad-request
       )
   where
-    open Request
+    open HTTP.Request
 
 run-port : ℕ
 run-port = 1337

src/Parse-HTTP/Methods.agda

@@ -1,47 +0,0 @@
-open import Agda.Primitive renaming (Set to Type)
-open import Data.Product
-open import Data.Nat
-
-import Data.String as S
-open S using (String)
-
-open import Bits-and-Bytes
-open import NonEmpty
-open import Base
-
-open import Parse-HTTP.Helpers
-
-module Parse-HTTP.Methods where
-
-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
-      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     = string-to-ascii-list⁺ "GET"
-name-of-method HEAD    = string-to-ascii-list⁺ "HEAD"
-name-of-method POST    = string-to-ascii-list⁺ "POST"
-name-of-method PUT     = string-to-ascii-list⁺ "PUT"
-name-of-method DELETE  = string-to-ascii-list⁺ "DELETE"
-name-of-method CONNECT = string-to-ascii-list⁺ "CONNECT"
-name-of-method OPTIONS = string-to-ascii-list⁺ "OPTIONS"
-name-of-method TRACE   = string-to-ascii-list⁺ "TRACE"
-name-of-method PATCH   = string-to-ascii-list⁺ "PATCH"
-
-http-methods : List⁺ HTTP-Method
-http-methods = GET ∷⁺ HEAD ∷⁺ POST ∷⁺ PUT ∷⁺ DELETE ∷⁺ CONNECT ∷⁺ OPTIONS ∷⁺ TRACE ∷⁺ [ PATCH ]⁺
-

src/ParseHelpers.agda

@@ -24,7 +24,7 @@ import UTF-8
 
 open import Parsing (Byte)
 
-module Parse-HTTP.Helpers where
+module ParseHelpers where
 
 -- Bytes are compared against codepoints, meaning any non-ascii Chars will be death
 _is_ : Byte → Char → Bool
@@ -33,34 +33,6 @@ x is c = x .value == C.toℕ c
 _between_and_ : Byte → Char → Char → Bool
 x between a and b = (C.toℕ a ≤ᵇ x .value) ∧ (x .value ≤ᵇ C.toℕ b)
 
-list-is-ascii : List Char → Bool
-list-is-ascii L.[] = true
-list-is-ascii (c L.∷ chs) = (C.toℕ c <ᵇ 128) ∧ list-is-ascii chs
-
-string-is-ascii : String → Type
-string-is-ascii x = T (list-is-ascii (S.toList x))
-
-string-to-ascii-vec : (s : String) → {string-is-ascii s} → Vec Byte (S.length s)
-string-to-ascii-vec x {prf} = go (S.toList x)
-  where
-    go : (l : List Char) → Vec Byte (L.length l)
-    go L.[] = V.[]
-    go (ch L.∷ chs) = mkClip (C.toℕ ch) V.∷ go chs
-
-string-to-ascii-list⁺ : (s : String) → {string-is-ascii s} → {T (0 <ᵇ S.length s)} → List⁺ Byte
-string-to-ascii-list⁺ s {ascii} {nonempty} = vec-to-list⁺ v
-  where
-    open import Data.Nat.Properties
-    open S
-
-    len≢0 : length s ≢ 0
-    len≢0 = m<n⇒n≢0 (<ᵇ⇒< 0 (length s) nonempty)
-
-    v : Vec Byte (suc (pred (length s)))
-    v = subst (λ x → Vec Byte x) (sym (suc[pred[n]]≡n {length s} len≢0)) (string-to-ascii-vec s {ascii})
-
-string-to-ascii-list : (s : String) → {string-is-ascii s} → List Byte
-string-to-ascii-list s {ascii} = V.toList (string-to-ascii-vec s {ascii})
 
 any-of : String → [ Parser Byte ]
 any-of x = L.foldr (λ ch p → ((_is ch) <?>′ any₁) <|>′ p) fail (S.toList x)