xenia/henttp
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Rename Parse-HTTP to HTTP, separate parsing into HTTP.Parse

Browse Source
This commit is contained in:
xenia 2023-09-09 22:27:42 +02:00
parent 4907f2abeb
commit 088b2e3fe0
8 changed files with 205 additions and 172 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

50
src/ASCII.agda Normal file
View File

@ -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})

94
src/HTTP.agda Normal file
View File

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

82
src/Parse-HTTP.agda → src/HTTP/Parse.agda
View File

@ -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) =

24
src/Parse-HTTP/Test.agda → src/HTTP/Test.agda
View File

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

3
src/Parse-HTTP/URL.agda → src/HTTP/URL.agda
View File

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

47
src/Main.agda
View File

@ -20,14 +20,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 +43,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 +59,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 +103,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 +112,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 +131,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,7 +143,7 @@ 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
("index.html" / $) →
@ -150,8 +152,9 @@ handle-request req =
)
_ → 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 +162,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 +181,7 @@ handle sock = do
encode-response <$> pure 400-bad-request
)
where
open Request
open HTTP.Request
run-port : ℕ
run-port = 1337

47
src/Parse-HTTP/Methods.agda
View File

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

30
src/Parse-HTTP/Helpers.agda → src/ParseHelpers.agda
View File

@ -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)