Make encode-/decode-string actually take and return Strings, rather than List Chars
This commit is contained in:
parent
11cc587d1b
commit
4907f2abeb
|
|
@ -50,7 +50,7 @@ crlfᵇ = string-to-ascii-list "\r\n"
|
||||||
|
|
||||||
encode-response : Response → List Byte
|
encode-response : Response → List Byte
|
||||||
encode-response res =
|
encode-response res =
|
||||||
UTF-8.encode-string (S.toList (status-line)) L.++ crlfᵇ L.++
|
UTF-8.encode-string status-line L.++ crlfᵇ L.++
|
||||||
encoded-headers L.++ crlfᵇ L.++
|
encoded-headers L.++ crlfᵇ L.++
|
||||||
(proj₂ <$> res .content or-else L.[])
|
(proj₂ <$> res .content or-else L.[])
|
||||||
where
|
where
|
||||||
|
|
@ -63,12 +63,12 @@ encode-response res =
|
||||||
(real (content-type , content)) →
|
(real (content-type , content)) →
|
||||||
record
|
record
|
||||||
{ name = string-to-ascii-list⁺ "Content-Type"
|
{ name = string-to-ascii-list⁺ "Content-Type"
|
||||||
; value = UTF-8.encode-string (S.toList (show content-type)) ++⁺ string-to-ascii-list⁺ "; charset=utf-8"
|
; value = UTF-8.encode-string (show content-type) ++⁺ string-to-ascii-list⁺ "; charset=utf-8"
|
||||||
}
|
}
|
||||||
L.∷ record
|
L.∷ record
|
||||||
{ name = string-to-ascii-list⁺ "Content-Length"
|
{ name = string-to-ascii-list⁺ "Content-Length"
|
||||||
; value =
|
; value =
|
||||||
(list-to-list⁺? (UTF-8.encode-string (S.toList (show (L.length content)))))
|
list-to-list⁺? (UTF-8.encode-string (show (L.length content)))
|
||||||
or-else (string-to-ascii-list⁺ "mjau")
|
or-else (string-to-ascii-list⁺ "mjau")
|
||||||
}
|
}
|
||||||
L.∷ L.[]
|
L.∷ L.[]
|
||||||
|
|
@ -86,35 +86,32 @@ encode-response res =
|
||||||
(res .headers L.++ extra-headers)
|
(res .headers L.++ extra-headers)
|
||||||
)
|
)
|
||||||
|
|
||||||
200-ok : Content-Type → List Byte → List Byte
|
200-ok : Content-Type → String → Response
|
||||||
200-ok content-type content =
|
200-ok content-type content =
|
||||||
encode-response
|
record
|
||||||
record
|
{ status-code = 200
|
||||||
{ status-code = 200
|
; status = "OK"
|
||||||
; status = "OK"
|
; headers = L.[]
|
||||||
; headers = L.[]
|
; content = real (content-type , UTF-8.encode-string content)
|
||||||
; content = real (content-type , content)
|
}
|
||||||
}
|
|
||||||
|
|
||||||
400-bad-request : List Byte
|
400-bad-request : Response
|
||||||
400-bad-request =
|
400-bad-request =
|
||||||
encode-response
|
record
|
||||||
record
|
{ status-code = 400
|
||||||
{ status-code = 400
|
; status = "Bad Request"
|
||||||
; status = "Bad Request"
|
; headers = L.[]
|
||||||
; headers = L.[]
|
; content = real (text/plain , string-to-ascii-list "what is bro doing")
|
||||||
; content = real (text/plain , string-to-ascii-list "what is bro doing")
|
}
|
||||||
}
|
|
||||||
|
|
||||||
404-not-found : List Byte
|
404-not-found : Response
|
||||||
404-not-found =
|
404-not-found =
|
||||||
encode-response
|
record
|
||||||
record
|
{ status-code = 404
|
||||||
{ status-code = 404
|
; status = "Not Found"
|
||||||
; status = "Not Found"
|
; headers = L.[]
|
||||||
; headers = L.[]
|
; content = real (text/plain , string-to-ascii-list "not found :(")
|
||||||
; content = real (text/plain , string-to-ascii-list "not found :(")
|
}
|
||||||
}
|
|
||||||
|
|
||||||
module Pages where
|
module Pages where
|
||||||
open HTML
|
open HTML
|
||||||
|
|
@ -130,10 +127,11 @@ module Pages where
|
||||||
< body >
|
< body >
|
||||||
< h 1 >
|
< h 1 >
|
||||||
< span style= "color: yellow;" > "hen" </ span > ,
|
< span style= "color: yellow;" > "hen" </ span > ,
|
||||||
< span style= "color: purple;" > "ttp" </ span >
|
< span style= "color: fuchsia;" > "ttp" </ span >
|
||||||
</ h 1 > ,
|
</ h 1 > ,
|
||||||
|
< h 3 > "what is this?" </ h 1 > ,
|
||||||
< p >
|
< p >
|
||||||
"what is this?"
|
"henttp is an HTTP server, HTML DSL and (soon to be) router, written in Agda"
|
||||||
</ p >
|
</ p >
|
||||||
</ body > ,
|
</ body > ,
|
||||||
< footer >
|
< footer >
|
||||||
|
|
@ -143,17 +141,14 @@ module Pages where
|
||||||
where
|
where
|
||||||
open HTML.Syntax
|
open HTML.Syntax
|
||||||
|
|
||||||
handle-request : Request → IO (List Byte)
|
handle-request : Request → IO Response
|
||||||
handle-request req =
|
handle-request req =
|
||||||
if (req .target .path) == ("index.html" / $)
|
case req .target .path of λ where
|
||||||
then pure (
|
("index.html" / $) →
|
||||||
200-ok
|
pure (
|
||||||
text/html
|
200-ok text/html (HTML.Render.render-element (Pages.render-index (req .target .query)))
|
||||||
(UTF-8.encode-string (S.toList (
|
|
||||||
HTML.Render.render-element (Pages.render-index (req .target .query))
|
|
||||||
)))
|
|
||||||
)
|
)
|
||||||
else pure 404-not-found
|
_ → pure 404-not-found
|
||||||
where
|
where
|
||||||
open Request using (target)
|
open Request using (target)
|
||||||
open import Parse-HTTP.URL
|
open import Parse-HTTP.URL
|
||||||
|
|
@ -175,12 +170,12 @@ handle sock = do
|
||||||
case req .content of λ where
|
case req .content of λ where
|
||||||
(real c) → putStrLn (" content = " S.++ show ⦃ ShowByteList ⦄ c)
|
(real c) → putStrLn (" content = " S.++ show ⦃ ShowByteList ⦄ c)
|
||||||
cake → putStrLn " no content"
|
cake → putStrLn " no content"
|
||||||
handle-request req
|
encode-response <$> handle-request req
|
||||||
)
|
)
|
||||||
cake →
|
cake →
|
||||||
(do
|
(do
|
||||||
putStrLn "Got an invalid request"
|
putStrLn "Got an invalid request"
|
||||||
pure 400-bad-request
|
encode-response <$> pure 400-bad-request
|
||||||
)
|
)
|
||||||
where
|
where
|
||||||
open Request
|
open Request
|
||||||
|
|
|
||||||
|
|
@ -31,7 +31,7 @@ module Parse-HTTP where
|
||||||
-- helper functions
|
-- helper functions
|
||||||
private
|
private
|
||||||
decode-utf8⁺ : List⁺ Byte → Maybe String
|
decode-utf8⁺ : List⁺ Byte → Maybe String
|
||||||
decode-utf8⁺ bs = S.fromList <$> UTF-8.decode-string (list⁺-to-list bs)
|
decode-utf8⁺ bs = UTF-8.decode-string (list⁺-to-list bs)
|
||||||
|
|
||||||
module Parse-URL where
|
module Parse-URL where
|
||||||
open import Parse-HTTP.URL
|
open import Parse-HTTP.URL
|
||||||
|
|
@ -221,26 +221,37 @@ module Parse-Request where
|
||||||
>>=′ λ (method , target , version , headers) → enbox (
|
>>=′ λ (method , target , version , headers) → enbox (
|
||||||
case content-length (list⁺-to-list headers) of λ where
|
case content-length (list⁺-to-list headers) of λ where
|
||||||
cake →
|
cake →
|
||||||
(
|
crlf >$=′ λ _ →
|
||||||
(λ _ → record { method = method; target = target; version = version; headers = list⁺-to-list headers; content = cake })
|
record
|
||||||
<$>′ crlf
|
{ method = method
|
||||||
)
|
; target = target
|
||||||
|
; version = version
|
||||||
|
; headers = list⁺-to-list headers
|
||||||
|
; content = cake
|
||||||
|
}
|
||||||
(real 0) →
|
(real 0) →
|
||||||
(
|
(crlf <&>□ crlf) >$=′ λ _ →
|
||||||
(λ _ → record { method = method; target = target; version = version; headers = list⁺-to-list headers; content = real L.[] })
|
record
|
||||||
<$>′ (crlf <&>□ crlf)
|
{ method = method
|
||||||
)
|
; target = target
|
||||||
|
; version = version
|
||||||
|
; headers = list⁺-to-list headers
|
||||||
|
; content = real L.[]
|
||||||
|
}
|
||||||
(real n@(suc _)) →
|
(real n@(suc _)) →
|
||||||
(
|
(crlf <&⃗>□ repeat n any₁) >$=′ λ content →
|
||||||
(λ content → record { method = method; target = target; version = version; headers = list⁺-to-list headers; content = real (V.toList content) })
|
record
|
||||||
<$>′ (crlf <&⃗>□ (repeat n any₁))
|
{ method = method
|
||||||
)
|
; target = target
|
||||||
|
; version = version
|
||||||
|
; headers = list⁺-to-list headers
|
||||||
|
; content = real (V.toList content)
|
||||||
|
}
|
||||||
)
|
)
|
||||||
where
|
where
|
||||||
find-target : ((HTTP-Method × RequestTarget × HTTP-Version) × List⁺ Header) → Maybe (HTTP-Method × URL × HTTP-Version × List⁺ Header)
|
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) =
|
find-target ((method , record { path = OriginForm path ; query = query } , ver) , headers) =
|
||||||
Parse-Header.host (list⁺-to-list headers) >>= λ auth →
|
(λ auth → method , (http:// auth / path ¿ query) , ver , headers) <$> Parse-Header.host (list⁺-to-list headers)
|
||||||
real (method , (http:// auth / path ¿ query) , ver , headers)
|
|
||||||
find-target ((method , record { path = AbsoluteForm auth path ; query = query } , ver) , headers) =
|
find-target ((method , record { path = AbsoluteForm auth path ; query = query } , ver) , headers) =
|
||||||
real (method , (http:// auth / path ¿ query) , ver , headers)
|
real (method , (http:// auth / path ¿ query) , ver , headers)
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -23,8 +23,8 @@ open import Parse-HTTP.URL
|
||||||
|
|
||||||
module Parse-HTTP.Test where
|
module Parse-HTTP.Test where
|
||||||
|
|
||||||
enc : (s : String) → V.Vec Byte (L.length (UTF-8.encode-string (S.toList s)))
|
enc : (s : String) → V.Vec Byte (L.length (UTF-8.encode-string s))
|
||||||
enc x = V.fromList (UTF-8.encode-string (S.toList x))
|
enc x = V.fromList (UTF-8.encode-string x)
|
||||||
|
|
||||||
module Test-Helpers where
|
module Test-Helpers where
|
||||||
test-percent-encoding : percent-encoded .parse (enc "%69abc")
|
test-percent-encoding : percent-encoded .parse (enc "%69abc")
|
||||||
|
|
|
||||||
|
|
@ -41,7 +41,7 @@ instance
|
||||||
EqPath ._==_ (_ / _) $ = false
|
EqPath ._==_ (_ / _) $ = false
|
||||||
EqPath ._==_ $ (_ / _) = false
|
EqPath ._==_ $ (_ / _) = false
|
||||||
|
|
||||||
infixr 5 _/_
|
infixr 30 _/_
|
||||||
|
|
||||||
record URL : Type where
|
record URL : Type where
|
||||||
constructor http://_/_¿_
|
constructor http://_/_¿_
|
||||||
|
|
|
||||||
200
src/UTF-8.agda
200
src/UTF-8.agda
|
|
@ -4,22 +4,27 @@ module UTF-8 where
|
||||||
open import Agda.Primitive renaming (Set to Type)
|
open import Agda.Primitive renaming (Set to Type)
|
||||||
|
|
||||||
open import Data.Product
|
open import Data.Product
|
||||||
open import Data.Unit using (⊤; tt)
|
open import Data.Unit
|
||||||
open import Data.Empty
|
|
||||||
open import Data.Vec hiding ([_])
|
|
||||||
open import Data.List using (List) renaming (_∷_ to _∷ˡ_; [] to []ˡ; _++_ to _++ˡ_)
|
|
||||||
open import Data.Bool using (Bool; true; false; T)
|
|
||||||
open import Data.Nat
|
|
||||||
open import Relation.Binary.PropositionalEquality hiding ([_])
|
open import Relation.Binary.PropositionalEquality hiding ([_])
|
||||||
|
open import Data.Bool hiding (_<_; _<?_)
|
||||||
|
open import Data.Nat
|
||||||
|
open import Data.Nat.Properties using (<-trans; <ᵇ⇒<; ≤-refl; m≤n+m)
|
||||||
open import Relation.Nullary
|
open import Relation.Nullary
|
||||||
|
|
||||||
|
import Data.Vec as V
|
||||||
|
import Data.List as L
|
||||||
|
import Data.String as S
|
||||||
|
import Data.Char as C
|
||||||
|
open V using (Vec)
|
||||||
|
open L using (List)
|
||||||
|
open S using (String)
|
||||||
|
open C using (Char)
|
||||||
|
|
||||||
open import Base
|
open import Base
|
||||||
open import NonEmpty
|
open import NonEmpty
|
||||||
open import Bits-and-Bytes
|
open import Bits-and-Bytes
|
||||||
|
|
||||||
import Data.Char as C
|
|
||||||
open import Data.Nat.Properties using (<-trans; <ᵇ⇒<; ≤-refl; m≤n+m)
|
|
||||||
|
|
||||||
postulate
|
postulate
|
||||||
char-toℕ-in-range : (c : C.Char) → C.toℕ c < 0x110000
|
char-toℕ-in-range : (c : C.Char) → C.toℕ c < 0x110000
|
||||||
|
|
||||||
|
|
@ -32,6 +37,8 @@ encode-char ch = case x <? 0x80 of λ where
|
||||||
(yes x<0x10000) → encode-3 x x<0x10000
|
(yes x<0x10000) → encode-3 x x<0x10000
|
||||||
(no _) → encode-4 x x<0x110000
|
(no _) → encode-4 x x<0x110000
|
||||||
where
|
where
|
||||||
|
open V
|
||||||
|
|
||||||
x : ℕ
|
x : ℕ
|
||||||
x = C.toℕ ch
|
x = C.toℕ ch
|
||||||
|
|
||||||
|
|
@ -41,119 +48,124 @@ encode-char ch = case x <? 0x80 of λ where
|
||||||
encode-1 : (n : ℕ) → n < 0x80 → List Byte
|
encode-1 : (n : ℕ) → n < 0x80 → List Byte
|
||||||
encode-1 n n<0x80 = case enbits {7} n n<0x80 of λ where
|
encode-1 n n<0x80 = case enbits {7} n n<0x80 of λ where
|
||||||
(b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ []) →
|
(b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ []) →
|
||||||
Bit8-to-Byte (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ 𝟘 ∷ []) ∷ˡ
|
Bit8-to-Byte (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ 𝟘 ∷ []) L.∷
|
||||||
[]ˡ
|
L.[]
|
||||||
|
|
||||||
encode-2 : (n : ℕ) → n < 0x800 → List Byte
|
encode-2 : (n : ℕ) → n < 0x800 → List Byte
|
||||||
encode-2 n n<0x800 = case enbits {11} n n<0x800 of λ where
|
encode-2 n n<0x800 = case enbits {11} n n<0x800 of λ where
|
||||||
(b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ b7 ∷ b8 ∷ b9 ∷ b10 ∷ []) →
|
(b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ b7 ∷ b8 ∷ b9 ∷ b10 ∷ []) →
|
||||||
Bit8-to-Byte (b6 ∷ b7 ∷ b8 ∷ b9 ∷ b10 ∷ 𝟘 ∷ 𝟙 ∷ 𝟙 ∷ []) ∷ˡ
|
Bit8-to-Byte (b6 ∷ b7 ∷ b8 ∷ b9 ∷ b10 ∷ 𝟘 ∷ 𝟙 ∷ 𝟙 ∷ []) L.∷
|
||||||
Bit8-to-Byte (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ 𝟘 ∷ 𝟙 ∷ []) ∷ˡ
|
Bit8-to-Byte (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ 𝟘 ∷ 𝟙 ∷ []) L.∷
|
||||||
[]ˡ
|
L.[]
|
||||||
|
|
||||||
encode-3 : (n : ℕ) → n < 0x10000 → List Byte
|
encode-3 : (n : ℕ) → n < 0x10000 → List Byte
|
||||||
encode-3 n n<0x10000 = case enbits {16} n n<0x10000 of λ where
|
encode-3 n n<0x10000 = case enbits {16} n n<0x10000 of λ where
|
||||||
(b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ b7 ∷ b8 ∷ b9 ∷ b10 ∷ b11 ∷ b12 ∷ b13 ∷ b14 ∷ b15 ∷ []) →
|
(b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ b7 ∷ b8 ∷ b9 ∷ b10 ∷ b11 ∷ b12 ∷ b13 ∷ b14 ∷ b15 ∷ []) →
|
||||||
Bit8-to-Byte (b12 ∷ b13 ∷ b14 ∷ b15 ∷ 𝟘 ∷ 𝟙 ∷ 𝟙 ∷ 𝟙 ∷ []) ∷ˡ
|
Bit8-to-Byte (b12 ∷ b13 ∷ b14 ∷ b15 ∷ 𝟘 ∷ 𝟙 ∷ 𝟙 ∷ 𝟙 ∷ []) L.∷
|
||||||
Bit8-to-Byte (b6 ∷ b7 ∷ b8 ∷ b9 ∷ b10 ∷ b11 ∷ 𝟘 ∷ 𝟙 ∷ []) ∷ˡ
|
Bit8-to-Byte (b6 ∷ b7 ∷ b8 ∷ b9 ∷ b10 ∷ b11 ∷ 𝟘 ∷ 𝟙 ∷ []) L.∷
|
||||||
Bit8-to-Byte (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ 𝟘 ∷ 𝟙 ∷ []) ∷ˡ
|
Bit8-to-Byte (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ 𝟘 ∷ 𝟙 ∷ []) L.∷
|
||||||
[]ˡ
|
L.[]
|
||||||
|
|
||||||
encode-4 : (n : ℕ) → n < 0x110000 → List Byte
|
encode-4 : (n : ℕ) → n < 0x110000 → List Byte
|
||||||
encode-4 n n<0x110000 = case enbits {21} n (<-trans n<0x110000 (<ᵇ⇒< 0x110000 (2 ^ 21) tt)) of λ where
|
encode-4 n n<0x110000 = case enbits {21} n (<-trans n<0x110000 (<ᵇ⇒< 0x110000 (2 ^ 21) tt)) of λ where
|
||||||
(b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ b7 ∷ b8 ∷ b9 ∷ b10 ∷ b11 ∷ b12 ∷ b13 ∷ b14 ∷ b15 ∷
|
(b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ b7 ∷ b8 ∷ b9 ∷ b10 ∷ b11 ∷ b12 ∷ b13 ∷ b14 ∷ b15 ∷
|
||||||
b16 ∷ b17 ∷ b18 ∷ b19 ∷ b20 ∷ []) →
|
b16 ∷ b17 ∷ b18 ∷ b19 ∷ b20 ∷ []) →
|
||||||
Bit8-to-Byte (b18 ∷ b19 ∷ b20 ∷ 𝟘 ∷ 𝟙 ∷ 𝟙 ∷ 𝟙 ∷ 𝟙 ∷ []) ∷ˡ
|
Bit8-to-Byte (b18 ∷ b19 ∷ b20 ∷ 𝟘 ∷ 𝟙 ∷ 𝟙 ∷ 𝟙 ∷ 𝟙 ∷ []) L.∷
|
||||||
Bit8-to-Byte (b12 ∷ b13 ∷ b14 ∷ b15 ∷ b16 ∷ b17 ∷ 𝟘 ∷ 𝟙 ∷ []) ∷ˡ
|
Bit8-to-Byte (b12 ∷ b13 ∷ b14 ∷ b15 ∷ b16 ∷ b17 ∷ 𝟘 ∷ 𝟙 ∷ []) L.∷
|
||||||
Bit8-to-Byte (b6 ∷ b7 ∷ b8 ∷ b9 ∷ b10 ∷ b11 ∷ 𝟘 ∷ 𝟙 ∷ []) ∷ˡ
|
Bit8-to-Byte (b6 ∷ b7 ∷ b8 ∷ b9 ∷ b10 ∷ b11 ∷ 𝟘 ∷ 𝟙 ∷ []) L.∷
|
||||||
Bit8-to-Byte (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ 𝟘 ∷ 𝟙 ∷ []) ∷ˡ
|
Bit8-to-Byte (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ 𝟘 ∷ 𝟙 ∷ []) L.∷
|
||||||
[]ˡ
|
L.[]
|
||||||
|
|
||||||
encode-string : List C.Char → List Byte
|
encode-string : String → List Byte
|
||||||
encode-string []ˡ = []ˡ
|
encode-string s = go (S.toList s)
|
||||||
encode-string (c ∷ˡ cs) = encode-char c ++ˡ encode-string cs
|
where
|
||||||
|
go : List Char → List Byte
|
||||||
|
go L.[] = L.[]
|
||||||
|
go (c L.∷ cs) = encode-char c L.++ go cs
|
||||||
|
|
||||||
module decode where
|
module decode where
|
||||||
open import Indexed using ([_]; _→′_; □_; fix)
|
open import Indexed using ([_]; _→′_; □_; fix)
|
||||||
open import Parsing (Byte)
|
open import Parsing (Byte)
|
||||||
import Data.Fin as F
|
import Data.Fin as F
|
||||||
|
|
||||||
decode-≤-1 : {m : ℕ} → Vec Byte (1 + m) → Maybe (Parse C.Char (1 + m))
|
module _ where
|
||||||
decode-≤-1 (x ∷ xs) with Byte-to-Bit8 x
|
open V hiding ([_])
|
||||||
... | (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ 𝟘 ∷ [])
|
decode-≤-1 : {m : ℕ} → Vec Byte (1 + m) → Maybe (Parse C.Char (1 + m))
|
||||||
= real
|
decode-≤-1 (x ∷ xs) with Byte-to-Bit8 x
|
||||||
⟨ C.fromℕ (proj₁ (unbits {7} (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ [])))
|
... | (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ 𝟘 ∷ [])
|
||||||
, ≤-refl
|
= real
|
||||||
, xs ⟩
|
⟨ C.fromℕ (proj₁ (unbits {7} (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ [])))
|
||||||
... | _ = cake
|
, ≤-refl
|
||||||
|
, xs ⟩
|
||||||
|
... | _ = cake
|
||||||
|
|
||||||
decode-≤-2 : {m : ℕ} → Vec Byte (2 + m) → Maybe (Parse C.Char (2 + m))
|
decode-≤-2 : {m : ℕ} → Vec Byte (2 + m) → Maybe (Parse C.Char (2 + m))
|
||||||
decode-≤-2 {m} x@(x₁ ∷ x₂ ∷ xs) with Byte-to-Bit8 x₁ ,′ Byte-to-Bit8 x₂
|
decode-≤-2 {m} x@(x₁ ∷ x₂ ∷ xs) with Byte-to-Bit8 x₁ ,′ Byte-to-Bit8 x₂
|
||||||
... | (b6 ∷ b7 ∷ b8 ∷ b9 ∷ b10 ∷ 𝟘 ∷ 𝟙 ∷ 𝟙 ∷ [])
|
... | (b6 ∷ b7 ∷ b8 ∷ b9 ∷ b10 ∷ 𝟘 ∷ 𝟙 ∷ 𝟙 ∷ [])
|
||||||
, (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ 𝟘 ∷ 𝟙 ∷ [])
|
, (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ 𝟘 ∷ 𝟙 ∷ [])
|
||||||
= real
|
= real
|
||||||
⟨ C.fromℕ (proj₁ (unbits {11}
|
⟨ C.fromℕ (proj₁ (unbits {11}
|
||||||
( b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ b7
|
( b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ b7
|
||||||
∷ b8 ∷ b9 ∷ b10 ∷ []
|
∷ b8 ∷ b9 ∷ b10 ∷ []
|
||||||
)))
|
)))
|
||||||
, m≤n+m (suc m) 1
|
, m≤n+m (suc m) 1
|
||||||
, xs ⟩
|
, xs ⟩
|
||||||
... | _ = cake
|
... | _ = cake
|
||||||
|
|
||||||
decode-≤-3 : {m : ℕ} → Vec Byte (3 + m) → Maybe (Parse C.Char (3 + m))
|
decode-≤-3 : {m : ℕ} → Vec Byte (3 + m) → Maybe (Parse C.Char (3 + m))
|
||||||
decode-≤-3 {m} x@(x₁ ∷ x₂ ∷ x₃ ∷ xs) with Byte-to-Bit8 x₁ ,′ Byte-to-Bit8 x₂ ,′ Byte-to-Bit8 x₃
|
decode-≤-3 {m} x@(x₁ ∷ x₂ ∷ x₃ ∷ xs) with Byte-to-Bit8 x₁ ,′ Byte-to-Bit8 x₂ ,′ Byte-to-Bit8 x₃
|
||||||
... | (b12 ∷ b13 ∷ b14 ∷ b15 ∷ 𝟘 ∷ 𝟙 ∷ 𝟙 ∷ 𝟙 ∷ [])
|
... | (b12 ∷ b13 ∷ b14 ∷ b15 ∷ 𝟘 ∷ 𝟙 ∷ 𝟙 ∷ 𝟙 ∷ [])
|
||||||
, (b6 ∷ b7 ∷ b8 ∷ b9 ∷ b10 ∷ b11 ∷ 𝟘 ∷ 𝟙 ∷ [])
|
, (b6 ∷ b7 ∷ b8 ∷ b9 ∷ b10 ∷ b11 ∷ 𝟘 ∷ 𝟙 ∷ [])
|
||||||
, (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ 𝟘 ∷ 𝟙 ∷ [])
|
, (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ 𝟘 ∷ 𝟙 ∷ [])
|
||||||
= real
|
= real
|
||||||
⟨ C.fromℕ (proj₁ (unbits {16}
|
⟨ C.fromℕ (proj₁ (unbits {16}
|
||||||
( b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ b7
|
( b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ b7
|
||||||
∷ b8 ∷ b9 ∷ b10 ∷ b11 ∷ b12 ∷ b13 ∷ b14 ∷ b15 ∷ []
|
∷ b8 ∷ b9 ∷ b10 ∷ b11 ∷ b12 ∷ b13 ∷ b14 ∷ b15 ∷ []
|
||||||
)))
|
)))
|
||||||
, m≤n+m (suc m) 2
|
, m≤n+m (suc m) 2
|
||||||
, xs ⟩
|
, xs ⟩
|
||||||
... | _ = cake
|
... | _ = cake
|
||||||
|
|
||||||
decode-≤-4 : {m : ℕ} → Vec Byte (4 + m) → Maybe (Parse C.Char (4 + m))
|
decode-≤-4 : {m : ℕ} → Vec Byte (4 + m) → Maybe (Parse C.Char (4 + m))
|
||||||
decode-≤-4 {m} x@(x₁ ∷ x₂ ∷ x₃ ∷ x₄ ∷ xs) with Byte-to-Bit8 x₁ ,′ Byte-to-Bit8 x₂ ,′ Byte-to-Bit8 x₃ ,′ Byte-to-Bit8 x₄
|
decode-≤-4 {m} x@(x₁ ∷ x₂ ∷ x₃ ∷ x₄ ∷ xs) with Byte-to-Bit8 x₁ ,′ Byte-to-Bit8 x₂ ,′ Byte-to-Bit8 x₃ ,′ Byte-to-Bit8 x₄
|
||||||
... | (b18 ∷ b19 ∷ b20 ∷ 𝟘 ∷ 𝟙 ∷ 𝟙 ∷ 𝟙 ∷ 𝟙 ∷ [])
|
... | (b18 ∷ b19 ∷ b20 ∷ 𝟘 ∷ 𝟙 ∷ 𝟙 ∷ 𝟙 ∷ 𝟙 ∷ [])
|
||||||
, (b12 ∷ b13 ∷ b14 ∷ b15 ∷ b16 ∷ b17 ∷ 𝟘 ∷ 𝟙 ∷ [])
|
, (b12 ∷ b13 ∷ b14 ∷ b15 ∷ b16 ∷ b17 ∷ 𝟘 ∷ 𝟙 ∷ [])
|
||||||
, (b6 ∷ b7 ∷ b8 ∷ b9 ∷ b10 ∷ b11 ∷ 𝟘 ∷ 𝟙 ∷ [])
|
, (b6 ∷ b7 ∷ b8 ∷ b9 ∷ b10 ∷ b11 ∷ 𝟘 ∷ 𝟙 ∷ [])
|
||||||
, (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ 𝟘 ∷ 𝟙 ∷ [])
|
, (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ 𝟘 ∷ 𝟙 ∷ [])
|
||||||
= real
|
= real
|
||||||
⟨ C.fromℕ (proj₁ (unbits {21}
|
⟨ C.fromℕ (proj₁ (unbits {21}
|
||||||
( b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ b7
|
( b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ b7
|
||||||
∷ b8 ∷ b9 ∷ b10 ∷ b11 ∷ b12 ∷ b13 ∷ b14 ∷ b15
|
∷ b8 ∷ b9 ∷ b10 ∷ b11 ∷ b12 ∷ b13 ∷ b14 ∷ b15
|
||||||
∷ b16 ∷ b17 ∷ b18 ∷ b19 ∷ b20 ∷ []
|
∷ b16 ∷ b17 ∷ b18 ∷ b19 ∷ b20 ∷ []
|
||||||
)))
|
)))
|
||||||
, m≤n+m (suc m) 3
|
, m≤n+m (suc m) 3
|
||||||
, xs ⟩
|
, xs ⟩
|
||||||
... | _ = cake
|
... | _ = cake
|
||||||
|
|
||||||
parse-char : [ Parser C.Char ]
|
parse-char : [ Parser C.Char ]
|
||||||
parse-char {n} .parse [] = cake
|
parse-char {n} .parse [] = cake
|
||||||
parse-char {n} .parse xs@(_ ∷ _) = case decode-≤-1 xs of λ where
|
parse-char {n} .parse xs@(_ ∷ _) = case decode-≤-1 xs of λ where
|
||||||
(real x) → real x
|
(real x) → real x
|
||||||
cake → case xs of λ where
|
cake → case xs of λ where
|
||||||
(_ ∷ []) → cake
|
(_ ∷ []) → cake
|
||||||
(_ ∷ _ ∷ _) → case decode-≤-2 xs of λ where
|
(_ ∷ _ ∷ _) → case decode-≤-2 xs of λ where
|
||||||
(real x) → real x
|
(real x) → real x
|
||||||
cake → case xs of λ where
|
cake → case xs of λ where
|
||||||
(_ ∷ _ ∷ []) → cake
|
(_ ∷ _ ∷ []) → cake
|
||||||
(_ ∷ _ ∷ _ ∷ _) → case decode-≤-3 xs of λ where
|
(_ ∷ _ ∷ _ ∷ _) → case decode-≤-3 xs of λ where
|
||||||
(real x) → real x
|
(real x) → real x
|
||||||
cake → case xs of λ where
|
cake → case xs of λ where
|
||||||
(_ ∷ _ ∷ _ ∷ []) → cake
|
(_ ∷ _ ∷ _ ∷ []) → cake
|
||||||
(_ ∷ _ ∷ _ ∷ _ ∷ _) → decode-≤-4 xs
|
(_ ∷ _ ∷ _ ∷ _ ∷ _) → decode-≤-4 xs
|
||||||
|
|
||||||
parse-string : [ Parser (List⁺ C.Char) ]
|
parse-string : [ Parser (List⁺ C.Char) ]
|
||||||
parse-string = many-fix parse-char
|
parse-string = many-fix parse-char
|
||||||
|
|
||||||
decode-string : List Byte → Maybe (List C.Char)
|
decode-string : List Byte → Maybe String
|
||||||
decode-string []ˡ = real []ˡ
|
decode-string L.[] = real ""
|
||||||
decode-string xs@(_ ∷ˡ _) with parse-string .parse (fromList xs)
|
decode-string xs@(_ L.∷ _) with parse-string .parse (V.fromList xs)
|
||||||
... | real ⟨ r , _ , [] ⟩ = real (list⁺-to-list r)
|
... | real ⟨ r , _ , V.[] ⟩ = real (S.fromList (list⁺-to-list r))
|
||||||
... | _ = cake
|
... | _ = cake
|
||||||
|
|
||||||
open decode using (decode-string; parse-string; parse-char) public
|
open decode using (decode-string; parse-string; parse-char) public
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -33,7 +33,7 @@ encode-∘ : encode-char '∘' ≡ < 0xe2 > ∷ˡ < 0x88 > ∷ˡ < 0x98 > ∷ˡ
|
||||||
encode-∘ = refl
|
encode-∘ = refl
|
||||||
encode-𐄣 : encode-char '𐄣' ≡ < 0xf0 > ∷ˡ < 0x90 > ∷ˡ < 0x84 > ∷ˡ < 0xa3 > ∷ˡ []ˡ
|
encode-𐄣 : encode-char '𐄣' ≡ < 0xf0 > ∷ˡ < 0x90 > ∷ˡ < 0x84 > ∷ˡ < 0xa3 > ∷ˡ []ˡ
|
||||||
encode-𐄣 = refl
|
encode-𐄣 = refl
|
||||||
encode-blah : encode-string (S.toList "aö∘𐄣")
|
encode-blah : encode-string "aö∘𐄣"
|
||||||
≡ < 0x61 >
|
≡ < 0x61 >
|
||||||
∷ˡ < 0xc3 > ∷ˡ < 0xb6 >
|
∷ˡ < 0xc3 > ∷ˡ < 0xb6 >
|
||||||
∷ˡ < 0xe2 > ∷ˡ < 0x88 > ∷ˡ < 0x98 >
|
∷ˡ < 0xe2 > ∷ˡ < 0x88 > ∷ˡ < 0x98 >
|
||||||
|
|
@ -46,5 +46,5 @@ decode-blah : decode-string
|
||||||
∷ˡ < 0xe2 > ∷ˡ < 0x88 > ∷ˡ < 0x98 >
|
∷ˡ < 0xe2 > ∷ˡ < 0x88 > ∷ˡ < 0x98 >
|
||||||
∷ˡ < 0xf0 > ∷ˡ < 0x90 > ∷ˡ < 0x84 > ∷ˡ < 0xa3 >
|
∷ˡ < 0xf0 > ∷ˡ < 0x90 > ∷ˡ < 0x84 > ∷ˡ < 0xa3 >
|
||||||
∷ˡ []ˡ )
|
∷ˡ []ˡ )
|
||||||
≡ real (S.toList "aö∘𐄣")
|
≡ real "aö∘𐄣"
|
||||||
decode-blah = refl
|
decode-blah = refl
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue
Block a user