Make imports in List, Vec, String and Char more consistent
This commit is contained in:
parent
ef97390a8b
commit
000ea2fc71
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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₁))
|
||||
)
|
||||
)
|
||||
|
|
|
|||
|
|
@ -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<n⇒n≢0 (<ᵇ⇒< 0 (String.length s) nonempty)
|
||||
len≢0 : length s ≢ 0
|
||||
len≢0 = m<n⇒n≢0 (<ᵇ⇒< 0 (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})
|
||||
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})
|
||||
|
||||
any-of : String.String → [ Parser Byte ]
|
||||
any-of x = List.foldr (λ ch p → ((_is ch) <?>′ 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-ℕ
|
||||
|
|
|
|||
|
|
@ -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 ]⁺
|
||||
|
|
|
|||
|
|
@ -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")
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user