diff --git a/src/Base.agda b/src/Base.agda index b4c0b13..8136755 100644 --- a/src/Base.agda +++ b/src/Base.agda @@ -3,8 +3,10 @@ open import Data.Bool open import Data.Empty open import Data.Unit open import Data.Nat -import Data.String as String -open import Data.List +import Data.String as S +import Data.List as L +open S using (String) +open L using (List) module Base where @@ -84,14 +86,14 @@ instance 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 + EqList ._==_ L.[] L.[] = true + EqList ._==_ (x L.∷ xs) (y L.∷ ys) = x == y ∧ xs == ys + EqList ._==_ (_ L.∷ _) L.[] = false + EqList ._==_ L.[] (_ L.∷ _) = false record Show (T : Type) : Type₁ where field - show : T → String.String + show : T → String open Show ⦃...⦄ public @@ -100,14 +102,14 @@ instance ShowNat : Show ℕ ShowNat .show x = show-ℕ x - ShowString : Show String.String - ShowString .show x = String.show x + ShowString : Show String + ShowString .show x = S.show x ShowList : {A : Type} → ⦃ Show A ⦄ → Show (List A) - ShowList {A} .show x = "[" String.++ go x String.++ "]" + ShowList {A} .show x = "[" S.++ go x S.++ "]" where - go : List A → String.String - go [] = "" - go (x ∷ []) = show x - go (x ∷ xs) = show x String.++ ", " String.++ go xs + go : List A → String + go L.[] = "" + go (x L.∷ L.[]) = show x + go (x L.∷ xs) = show x S.++ ", " S.++ go xs diff --git a/src/Parse-HTTP.agda b/src/Parse-HTTP.agda index b7f46d1..7918015 100644 --- a/src/Parse-HTTP.agda +++ b/src/Parse-HTTP.agda @@ -2,16 +2,18 @@ open import Agda.Primitive renaming (Set to Type) -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 (<ᵇ⇒<) open import Data.Bool hiding (_<_) open import Data.Unit open import Data.Product -import Data.String as String -import Data.Char as Char +import Data.String as S +import Data.List as L +import Data.Vec as V +open S using (String) +open L using (List) +open V using (Vec) open import Base @@ -28,8 +30,8 @@ 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) + decode-utf8⁺ : List⁺ Byte → Maybe String + decode-utf8⁺ bs = S.fromList <$> UTF-8.decode-string (list⁺-to-list bs) module Parse-URL where open import Parse-HTTP.URL @@ -45,13 +47,13 @@ module Parse-URL where pchar : [ Parser Byte ] pchar = unreserved <|>′ percent-encoded <|>′ sub-delims <|>′ any-of ":@" - parse-scheme : [ Parser String.String ] + parse-scheme : [ Parser String ] parse-scheme = decode-utf8⁺ <$?>′ many (letter <|>′ digit <|>′ any-of "+-.") parse-authority : [ Parser Authority ] parse-authority = (λ auth → auth .port <ᵇ 2 ^ 16) ′ unchecked where - reg-name : [ Parser String.String ] + reg-name : [ Parser String ] reg-name = decode-utf8⁺ <$?>′ (many (unreserved <|>′ percent-encoded <|>′ sub-delims)) unchecked : [ Parser Authority ] @@ -60,16 +62,16 @@ module Parse-URL where parse-path : [ Parser Path ] parse-path = - List.foldr (λ (slash , seg) path → seg / path) $ <$>′ + L.foldr (λ (slash , seg) path → seg / path) $ <$>′ ( (list⁺-to-list <$>′ many (any-of "/" <&>′ enbox segment)) - <|>′ ((λ _ → List.[]) <$>′ any-of "/") + <|>′ ((λ _ → L.[]) <$>′ any-of "/") ) where - segment : [ Parser String.String ] + segment : [ Parser String ] segment = decode-utf8⁺ <$?>′ many pchar - parse-query parse-fragment : [ Parser String.String ] + parse-query parse-fragment : [ Parser String ] parse-query = decode-utf8⁺ <$?>′ many (pchar <|>′ any-of "/?") parse-fragment = parse-query @@ -99,21 +101,21 @@ module Parse-Header where instance ShowHeader : Show Header - ShowHeader .show hdr = show ⦃ ShowByteList ⦄ (list⁺-to-list (hdr .name)) String.++ ": " String.++ show ⦃ ShowByteList ⦄ (list⁺-to-list (hdr .value)) + ShowHeader .show hdr = show ⦃ ShowByteList ⦄ (list⁺-to-list (hdr .name)) S.++ ": " S.++ 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) = + get-field : List⁺ Byte → List Header → Maybe (List⁺ Byte) + get-field field-name L.[] = cake + get-field field-name (hdr L.∷ 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 Header → Maybe ℕ content-length headers = get-field (string-to-ascii-list⁺ "Content-Length") headers >>= parse-list⁺ number - host : List.List Header → Maybe Authority + host : List Header → Maybe Authority host headers = get-field (string-to-ascii-list⁺ "Host") headers >>= parse-list⁺ parse-authority @@ -157,7 +159,7 @@ module Parse-Request where record RequestTarget : Type where field path : RequestTargetPath - query : Maybe String.String + query : Maybe String open RequestTarget public parse-request-target : [ Parser RequestTarget ] @@ -209,8 +211,8 @@ module Parse-Request where method : HTTP-Method target : URL version : HTTP-Version - headers : List.List Header - content : Maybe (List.List Byte) + headers : List Header + content : Maybe (List Byte) parse-request : [ Parser Request ] parse-request = @@ -225,12 +227,12 @@ module Parse-Request where ) (real 0) → ( - (λ _ → record { method = method; target = target; version = version; headers = list⁺-to-list headers; content = real List.[] }) + (λ _ → record { method = method; target = target; version = version; headers = list⁺-to-list headers; content = real L.[] }) <$>′ (crlf <&>□ crlf) ) (real n@(suc _)) → ( - (λ content → record { method = method; target = target; version = version; headers = list⁺-to-list headers; content = real (toList content) }) + (λ content → record { method = method; target = target; version = version; headers = list⁺-to-list headers; content = real (V.toList content) }) <$>′ (crlf <&⃗>□ (repeat n any₁)) ) ) diff --git a/src/Parse-HTTP/Helpers.agda b/src/Parse-HTTP/Helpers.agda index 88f59e0..b235395 100644 --- a/src/Parse-HTTP/Helpers.agda +++ b/src/Parse-HTTP/Helpers.agda @@ -1,19 +1,22 @@ open import Agda.Primitive renaming (Set to Type) +open import Relation.Binary.PropositionalEquality hiding ([_]) + open import Data.Nat 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 +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 Indexed open import NonEmpty open import Bits-and-Bytes @@ -24,39 +27,40 @@ open import Parsing (Byte) module Parse-HTTP.Helpers where -- Bytes are compared against codepoints, meaning any non-ascii Chars will be death -_is_ : Byte → Char.Char → Bool -x is c = x .value == Char.toℕ c +_is_ : Byte → Char → Bool +x is c = x .value == C.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) +_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.List Char.Char → Bool -list-is-ascii List.[] = true -list-is-ascii (c List.∷ chs) = (Char.toℕ c <ᵇ 128) ∧ list-is-ascii chs +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.String → Type -string-is-ascii x = T (list-is-ascii (String.toList x)) +string-is-ascii : String → Type +string-is-ascii x = T (list-is-ascii (S.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) +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.List Char.Char) → Vec Byte (List.length l) - go List.[] = [] - go (ch List.∷ chs) = mkClip (Char.toℕ ch) ∷ go chs + 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) → {string-is-ascii s} → {T (0 <ᵇ String.length s)} → List⁺ Byte +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 : String.length s ≢ 0 - len≢0 = m′ any₁) <|>′ p) fail (String.toList x) +any-of : String → [ Parser Byte ] +any-of x = L.foldr (λ ch p → ((_is ch) ′ any₁) <|>′ p) fail (S.toList x) uppercase lowercase letter digit : [ Parser Byte ] uppercase = (_between 'A' and 'Z') ′ any₁ @@ -74,26 +78,26 @@ space = (λ _ → tt) <$>′ any-of " " spaces = (λ _ → tt) <$>′ many space percent-encoded : [ Parser Byte ] -percent-encoded = (λ where (a ∷ b ∷ []) → mkClip (a * 16 + b)) <$>′ unencoded-percent-encoding +percent-encoded = (λ where (a V.∷ b V.∷ V.[]) → mkClip (a * 16 + b)) <$>′ unencoded-percent-encoding where unhex : Byte → Maybe ℕ -- char to hex digit unhex x = if x between '0' and '9' - then real (x .value ∸ (Char.toℕ '0')) + then real (x .value ∸ (C.toℕ '0')) else if x between 'a' and 'f' - then real (x .value ∸ (Char.toℕ 'a') + 10) + then real (x .value ∸ (C.toℕ 'a') + 10) else if x between 'A' and 'F' - then real (x .value ∸ (Char.toℕ 'A') + 10) + then real (x .value ∸ (C.toℕ 'A') + 10) else cake hex-digit : [ Parser ℕ ] hex-digit = unhex <$?>′ any₁ unencoded-percent-encoding : [ Parser (Vec ℕ 2) ] - unencoded-percent-encoding = exact (bytes.PERCENT ∷ []) >>′ enbox (repeat 2 hex-digit) + unencoded-percent-encoding = exact (bytes.PERCENT V.∷ V.[]) >>′ enbox (repeat 2 hex-digit) digit-ℕ : [ Parser ℕ ] -digit-ℕ = (λ x → x .value ∸ Char.toℕ '0') <$>′ digit +digit-ℕ = (λ x → x .value ∸ C.toℕ '0') <$>′ digit number : [ Parser ℕ ] number = foldl (λ n d → n * 10 + d) 0 <$>′ many digit-ℕ diff --git a/src/Parse-HTTP/Methods.agda b/src/Parse-HTTP/Methods.agda index 1fa4243..1954115 100644 --- a/src/Parse-HTTP/Methods.agda +++ b/src/Parse-HTTP/Methods.agda @@ -1,16 +1,18 @@ 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 + +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 --- HTTP Method: GET, POST, etc. data HTTP-Method : Type where GET HEAD POST PUT DELETE CONNECT OPTIONS TRACE PATCH : HTTP-Method @@ -18,7 +20,7 @@ instance ShowMethod : Show HTTP-Method ShowMethod .show x = go x where - go : HTTP-Method → String.String + go : HTTP-Method → String go GET = "GET" go HEAD = "HEAD" go POST = "POST" @@ -30,15 +32,15 @@ instance 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 > ]⁺ +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 ]⁺ diff --git a/src/Parse-HTTP/Test.agda b/src/Parse-HTTP/Test.agda index 0aec247..0b1d432 100644 --- a/src/Parse-HTTP/Test.agda +++ b/src/Parse-HTTP/Test.agda @@ -1,14 +1,19 @@ open import Relation.Binary.PropositionalEquality -open import Data.String -open import Data.Char open import Data.Product -import Data.List as List -import Data.Vec as Vec + +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 Parsing -open import UTF-8 +import UTF-8 open import NonEmpty open import Parse-HTTP @@ -18,8 +23,8 @@ open import Parse-HTTP.URL module Parse-HTTP.Test where -enc : (s : String) → Vec.Vec Byte (List.length (encode-string (toList s))) -enc x = Vec.fromList (encode-string (toList x)) +enc : (s : String) → V.Vec Byte (L.length (UTF-8.encode-string (S.toList s))) +enc x = V.fromList (UTF-8.encode-string (S.toList x)) module Test-Helpers where test-percent-encoding : percent-encoded .parse (enc "%69abc")