From 4907f2abeb65cc398dee9e7b5fa20017b7b01b90 Mon Sep 17 00:00:00 2001
From: xenia <xenia.agda@gmail.com>
Date: Sat, 9 Sep 2023 21:47:10 +0200
Subject: [PATCH] Make encode-/decode-string actually take and return Strings,
 rather than List Chars

---
 src/Main.agda            |  75 +++++++--------
 src/Parse-HTTP.agda      |  43 +++++----
 src/Parse-HTTP/Test.agda |   4 +-
 src/Parse-HTTP/URL.agda  |   2 +-
 src/UTF-8.agda           | 200 +++++++++++++++++++++------------------
 src/UTF-8/Test.agda      |   4 +-
 6 files changed, 173 insertions(+), 155 deletions(-)

diff --git a/src/Main.agda b/src/Main.agda
index 7318837..a8f37ed 100644
--- a/src/Main.agda
+++ b/src/Main.agda
@@ -50,7 +50,7 @@ crlfᵇ = string-to-ascii-list "\r\n"
 
 encode-response : Response → List Byte
 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.++
   (proj₂ <$> res .content or-else L.[])
   where
@@ -63,12 +63,12 @@ encode-response res =
       (real (content-type , content)) →
         record
           { 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
           { name = string-to-ascii-list⁺ "Content-Length"
           ; 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")
           }
         L.∷ L.[]
@@ -86,35 +86,32 @@ encode-response res =
           (res .headers L.++ extra-headers)
       )
 
-200-ok : Content-Type → List Byte → List Byte
+200-ok : Content-Type → String → Response
 200-ok content-type content =
-  encode-response
-    record
-    { status-code = 200
-    ; status = "OK"
-    ; headers = L.[]
-    ; content = real (content-type , content)
-    }
+  record
+  { status-code = 200
+  ; status = "OK"
+  ; headers = L.[]
+  ; content = real (content-type , UTF-8.encode-string content)
+  }
 
-400-bad-request : List Byte
+400-bad-request : Response
 400-bad-request =
-  encode-response
-    record
-    { status-code = 400
-    ; status = "Bad Request"
-    ; headers = L.[]
-    ; content = real (text/plain , string-to-ascii-list "what is bro doing")
-    }
+  record
+  { status-code = 400
+  ; status = "Bad Request"
+  ; headers = L.[]
+  ; content = real (text/plain , string-to-ascii-list "what is bro doing")
+  }
 
-404-not-found : List Byte
+404-not-found : Response
 404-not-found =
-  encode-response
-    record
-    { status-code = 404
-    ; status = "Not Found"
-    ; headers = L.[]
-    ; content = real (text/plain , string-to-ascii-list "not found :(")
-    }
+  record
+  { status-code = 404
+  ; status = "Not Found"
+  ; headers = L.[]
+  ; content = real (text/plain , string-to-ascii-list "not found :(")
+  }
 
 module Pages where
   open HTML
@@ -130,10 +127,11 @@ module Pages where
       < body >
         < h 1 >
           < span style= "color: yellow;" > "hen" </ span > ,
-          < span style= "color: purple;" > "ttp" </ span >
+          < span style= "color: fuchsia;" > "ttp" </ span >
         </ h 1 > ,
+        < h 3 > "what is this?" </ h 1 > ,
         < p >
-          "what is this?"
+          "henttp is an HTTP server, HTML DSL and (soon to be) router, written in Agda"
         </ p >
       </ body > ,
       < footer >
@@ -143,17 +141,14 @@ module Pages where
     where
       open HTML.Syntax
 
-handle-request : Request → IO (List Byte)
+handle-request : Request → IO Response
 handle-request req =
-  if (req .target .path) == ("index.html" / $)
-    then pure (
-      200-ok
-        text/html
-        (UTF-8.encode-string (S.toList (
-          HTML.Render.render-element (Pages.render-index (req .target .query))
-        )))
+  case req .target .path of λ where
+    ("index.html" / $) →
+      pure (
+        200-ok text/html (HTML.Render.render-element (Pages.render-index (req .target .query)))
       )
-    else pure 404-not-found
+    _ → pure 404-not-found
   where
     open Request using (target)
     open import Parse-HTTP.URL
@@ -175,12 +170,12 @@ handle sock = do
         case req .content of λ where
           (real c) → putStrLn ("  content = " S.++ show ⦃ ShowByteList ⦄ c)
           cake → putStrLn "  no content"
-        handle-request req
+        encode-response <$> handle-request req
       )
     cake →
       (do
         putStrLn "Got an invalid request"
-        pure 400-bad-request
+        encode-response <$> pure 400-bad-request
       )
   where
     open Request
diff --git a/src/Parse-HTTP.agda b/src/Parse-HTTP.agda
index 7918015..e1d7b29 100644
--- a/src/Parse-HTTP.agda
+++ b/src/Parse-HTTP.agda
@@ -31,7 +31,7 @@ module Parse-HTTP where
 -- helper functions
 private
   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
   open import Parse-HTTP.URL
@@ -221,26 +221,37 @@ module Parse-Request where
     >>=′ λ (method , target , version , headers) → enbox (
       case content-length (list⁺-to-list headers) of λ where
         cake →
-          (
-            (λ _ → record { method = method; target = target; version = version; headers = list⁺-to-list headers; content = cake })
-            <$>′ crlf
-          )
+          crlf >$=′ λ _ →
+            record
+              { method = method
+              ; target = target
+              ; version = version
+              ; headers = list⁺-to-list headers
+              ; content = cake
+              }
         (real 0) →
-          (
-            (λ _ → record { method = method; target = target; version = version; headers = list⁺-to-list headers; content = real L.[] })
-            <$>′ (crlf <&>□ crlf)
-          )
+          (crlf <&>□ crlf) >$=′ λ _ →
+            record
+              { method = method
+              ; target = target
+              ; version = version
+              ; headers = list⁺-to-list headers
+              ; content = real L.[]
+              }
         (real n@(suc _)) →
-          (
-            (λ content → record { method = method; target = target; version = version; headers = list⁺-to-list headers; content = real (V.toList content) })
-            <$>′ (crlf <&⃗>□ (repeat n any₁))
-          )
+          (crlf <&⃗>□ repeat n any₁) >$=′ λ content →
+            record
+              { method = method
+              ; target = target
+              ; version = version
+              ; headers = list⁺-to-list headers
+              ; content = real (V.toList content)
+              }
     )
     where
       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) =
-        Parse-Header.host (list⁺-to-list headers) >>= λ auth →
-          real (method , (http:// auth / path ¿ query) , ver , headers)
+      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) =
         real (method , (http:// auth / path ¿ query) , ver , headers)
 
diff --git a/src/Parse-HTTP/Test.agda b/src/Parse-HTTP/Test.agda
index f81bee5..301137c 100644
--- a/src/Parse-HTTP/Test.agda
+++ b/src/Parse-HTTP/Test.agda
@@ -23,8 +23,8 @@ open import Parse-HTTP.URL
 
 module Parse-HTTP.Test where
 
-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))
+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")
diff --git a/src/Parse-HTTP/URL.agda b/src/Parse-HTTP/URL.agda
index cf4fa64..52ac447 100644
--- a/src/Parse-HTTP/URL.agda
+++ b/src/Parse-HTTP/URL.agda
@@ -41,7 +41,7 @@ instance
   EqPath ._==_ (_ / _)  $        = false
   EqPath ._==_ $        (_ / _)  = false
 
-infixr 5 _/_
+infixr 30 _/_
 
 record URL : Type where
   constructor http://_/_¿_
diff --git a/src/UTF-8.agda b/src/UTF-8.agda
index 3b97f07..cc7dc2c 100644
--- a/src/UTF-8.agda
+++ b/src/UTF-8.agda
@@ -4,22 +4,27 @@ module UTF-8 where
 open import Agda.Primitive renaming (Set to Type)
 
 open import Data.Product
-open import Data.Unit using (⊤; tt)
-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 Data.Unit
+
 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
 
+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 NonEmpty
 open import Bits-and-Bytes
 
-import Data.Char as C
-open import Data.Nat.Properties using (<-trans; <ᵇ⇒<; ≤-refl; m≤n+m)
-
 postulate
   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
         (no _) → encode-4 x x<0x110000
   where
+    open V
+
     x : ℕ
     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 = case enbits {7} n n<0x80 of λ where
       (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 = case enbits {11} n n<0x800 of λ where
       (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ b7 ∷ b8 ∷ b9 ∷ b10 ∷ []) →
-        Bit8-to-Byte (b6 ∷ b7 ∷ b8 ∷ b9 ∷ b10 ∷ 𝟘  ∷ 𝟙 ∷ 𝟙 ∷ []) ∷ˡ
-        Bit8-to-Byte (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4  ∷ b5 ∷ 𝟘 ∷ 𝟙 ∷ []) ∷ˡ
-        []ˡ
+        Bit8-to-Byte (b6 ∷ b7 ∷ b8 ∷ b9 ∷ b10 ∷ 𝟘  ∷ 𝟙 ∷ 𝟙 ∷ []) L.∷
+        Bit8-to-Byte (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4  ∷ b5 ∷ 𝟘 ∷ 𝟙 ∷ []) L.∷
+        L.[]
 
     encode-3 : (n : ℕ) → n < 0x10000 → List Byte
     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 ∷ []) →
-        Bit8-to-Byte (b12 ∷ b13 ∷ b14 ∷ b15 ∷ 𝟘   ∷ 𝟙   ∷ 𝟙 ∷ 𝟙 ∷ []) ∷ˡ
-        Bit8-to-Byte (b6  ∷ b7  ∷ b8  ∷ b9  ∷ b10 ∷ b11 ∷ 𝟘 ∷ 𝟙 ∷ []) ∷ˡ
-        Bit8-to-Byte (b0  ∷ b1  ∷ b2  ∷ b3  ∷ b4  ∷ b5  ∷ 𝟘 ∷ 𝟙 ∷ []) ∷ˡ
-        []ˡ
+        Bit8-to-Byte (b12 ∷ b13 ∷ b14 ∷ b15 ∷ 𝟘   ∷ 𝟙   ∷ 𝟙 ∷ 𝟙 ∷ []) L.∷
+        Bit8-to-Byte (b6  ∷ b7  ∷ b8  ∷ b9  ∷ b10 ∷ b11 ∷ 𝟘 ∷ 𝟙 ∷ []) L.∷
+        Bit8-to-Byte (b0  ∷ b1  ∷ b2  ∷ b3  ∷ b4  ∷ b5  ∷ 𝟘 ∷ 𝟙 ∷ []) L.∷
+        L.[]
 
     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
       (b0  ∷ b1  ∷ b2  ∷ b3  ∷ b4  ∷ b5 ∷ b6 ∷ b7 ∷ b8 ∷ b9 ∷ b10 ∷ b11 ∷ b12 ∷ b13 ∷ b14 ∷ b15 ∷
        b16 ∷ b17 ∷ b18 ∷ b19 ∷ b20 ∷ []) →
-        Bit8-to-Byte (b18 ∷ b19 ∷ b20 ∷ 𝟘   ∷ 𝟙   ∷ 𝟙   ∷ 𝟙 ∷ 𝟙 ∷ []) ∷ˡ
-        Bit8-to-Byte (b12 ∷ b13 ∷ b14 ∷ b15 ∷ b16 ∷ b17 ∷ 𝟘 ∷ 𝟙 ∷ []) ∷ˡ
-        Bit8-to-Byte (b6  ∷ b7  ∷ b8  ∷ b9  ∷ b10 ∷ b11 ∷ 𝟘 ∷ 𝟙 ∷ []) ∷ˡ
-        Bit8-to-Byte (b0  ∷ b1  ∷ b2  ∷ b3  ∷ b4  ∷ b5  ∷ 𝟘 ∷ 𝟙 ∷ []) ∷ˡ
-        []ˡ
+        Bit8-to-Byte (b18 ∷ b19 ∷ b20 ∷ 𝟘   ∷ 𝟙   ∷ 𝟙   ∷ 𝟙 ∷ 𝟙 ∷ []) L.∷
+        Bit8-to-Byte (b12 ∷ b13 ∷ b14 ∷ b15 ∷ b16 ∷ b17 ∷ 𝟘 ∷ 𝟙 ∷ []) L.∷
+        Bit8-to-Byte (b6  ∷ b7  ∷ b8  ∷ b9  ∷ b10 ∷ b11 ∷ 𝟘 ∷ 𝟙 ∷ []) L.∷
+        Bit8-to-Byte (b0  ∷ b1  ∷ b2  ∷ b3  ∷ b4  ∷ b5  ∷ 𝟘 ∷ 𝟙 ∷ []) L.∷
+        L.[]
 
-encode-string : List C.Char → List Byte
-encode-string []ˡ = []ˡ
-encode-string (c ∷ˡ cs) = encode-char c ++ˡ encode-string cs
+encode-string : String → List Byte
+encode-string s = go (S.toList s)
+  where
+    go : List Char → List Byte
+    go L.[] = L.[]
+    go (c L.∷ cs) = encode-char c L.++ go cs
 
 module decode where
   open import Indexed using ([_]; _→′_; □_; fix)
   open import Parsing (Byte)
   import Data.Fin as F
 
-  decode-≤-1 : {m : ℕ} → Vec Byte (1 + m) → Maybe (Parse C.Char (1 + m))
-  decode-≤-1 (x ∷ xs) with Byte-to-Bit8 x
-  ...                 | (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ 𝟘 ∷ [])
-                        = real
-                          ⟨ C.fromℕ (proj₁ (unbits {7} (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ [])))
-                          , ≤-refl
-                          , xs ⟩
-  ...                 | _ = cake
+  module _ where
+    open V hiding ([_])
+    decode-≤-1 : {m : ℕ} → Vec Byte (1 + m) → Maybe (Parse C.Char (1 + m))
+    decode-≤-1 (x ∷ xs) with Byte-to-Bit8 x
+    ... | (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ 𝟘 ∷ [])
+          = real
+            ⟨ C.fromℕ (proj₁ (unbits {7} (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ [])))
+            , ≤-refl
+            , xs ⟩
+    ... | _ = cake
 
-  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₂
-  ...                 | (b6 ∷ b7 ∷ b8 ∷ b9 ∷ b10 ∷ 𝟘  ∷ 𝟙 ∷ 𝟙 ∷ [])
-                      , (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4  ∷ b5 ∷ 𝟘 ∷ 𝟙 ∷ [])
-                        = real
-                          ⟨ C.fromℕ (proj₁ (unbits {11}
-                            ( b0 ∷ b1 ∷ b2  ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ b7
-                            ∷ b8 ∷ b9 ∷ b10 ∷ []
-                            )))
-                          , m≤n+m (suc m) 1
-                          , xs ⟩
-  ...                 | _ = cake
+    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₂
+    ... | (b6 ∷ b7 ∷ b8 ∷ b9 ∷ b10 ∷ 𝟘  ∷ 𝟙 ∷ 𝟙 ∷ [])
+        , (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4  ∷ b5 ∷ 𝟘 ∷ 𝟙 ∷ [])
+          = real
+            ⟨ C.fromℕ (proj₁ (unbits {11}
+              ( b0 ∷ b1 ∷ b2  ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ b7
+              ∷ b8 ∷ b9 ∷ b10 ∷ []
+              )))
+            , m≤n+m (suc m) 1
+            , xs ⟩
+    ... | _ = cake
 
-  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₃
-  ...                 | (b12 ∷ b13 ∷ b14 ∷ b15 ∷ 𝟘   ∷ 𝟙   ∷ 𝟙 ∷ 𝟙 ∷ [])
-                      , (b6  ∷ b7  ∷ b8  ∷ b9  ∷ b10 ∷ b11 ∷ 𝟘 ∷ 𝟙 ∷ [])
-                      , (b0  ∷ b1  ∷ b2  ∷ b3  ∷ b4  ∷ b5  ∷ 𝟘 ∷ 𝟙 ∷ [])
-                        = real
-                          ⟨ C.fromℕ (proj₁ (unbits {16}
-                            ( b0 ∷ b1 ∷ b2  ∷ b3  ∷ b4  ∷ b5  ∷ b6  ∷ b7
-                            ∷ b8 ∷ b9 ∷ b10 ∷ b11 ∷ b12 ∷ b13 ∷ b14 ∷ b15 ∷ []
-                            )))
-                          , m≤n+m (suc m) 2
-                          , xs ⟩
-  ...                 | _ = cake
+    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₃
+    ... | (b12 ∷ b13 ∷ b14 ∷ b15 ∷ 𝟘   ∷ 𝟙   ∷ 𝟙 ∷ 𝟙 ∷ [])
+        , (b6  ∷ b7  ∷ b8  ∷ b9  ∷ b10 ∷ b11 ∷ 𝟘 ∷ 𝟙 ∷ [])
+        , (b0  ∷ b1  ∷ b2  ∷ b3  ∷ b4  ∷ b5  ∷ 𝟘 ∷ 𝟙 ∷ [])
+          = real
+            ⟨ C.fromℕ (proj₁ (unbits {16}
+              ( b0 ∷ b1 ∷ b2  ∷ b3  ∷ b4  ∷ b5  ∷ b6  ∷ b7
+              ∷ b8 ∷ b9 ∷ b10 ∷ b11 ∷ b12 ∷ b13 ∷ b14 ∷ b15 ∷ []
+              )))
+            , m≤n+m (suc m) 2
+            , xs ⟩
+    ... | _ = cake
 
-  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₄
-  ...                 | (b18 ∷ b19 ∷ b20 ∷ 𝟘   ∷ 𝟙   ∷ 𝟙   ∷ 𝟙 ∷ 𝟙 ∷ [])
-                      , (b12 ∷ b13 ∷ b14 ∷ b15 ∷ b16 ∷ b17 ∷ 𝟘 ∷ 𝟙 ∷ [])
-                      , (b6  ∷ b7  ∷ b8  ∷ b9  ∷ b10 ∷ b11 ∷ 𝟘 ∷ 𝟙 ∷ [])
-                      , (b0  ∷ b1  ∷ b2  ∷ b3  ∷ b4  ∷ b5  ∷ 𝟘 ∷ 𝟙 ∷ [])
-                        = real
-                          ⟨ C.fromℕ (proj₁ (unbits {21}
-                            ( b0  ∷ b1  ∷ b2  ∷ b3  ∷ b4  ∷ b5  ∷ b6  ∷ b7
-                            ∷ b8  ∷ b9  ∷ b10 ∷ b11 ∷ b12 ∷ b13 ∷ b14 ∷ b15
-                            ∷ b16 ∷ b17 ∷ b18 ∷ b19 ∷ b20 ∷ []
-                            )))
-                          , m≤n+m (suc m) 3
-                          , xs ⟩
-  ...                 | _ = cake
+    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₄
+    ... | (b18 ∷ b19 ∷ b20 ∷ 𝟘   ∷ 𝟙   ∷ 𝟙   ∷ 𝟙 ∷ 𝟙 ∷ [])
+        , (b12 ∷ b13 ∷ b14 ∷ b15 ∷ b16 ∷ b17 ∷ 𝟘 ∷ 𝟙 ∷ [])
+        , (b6  ∷ b7  ∷ b8  ∷ b9  ∷ b10 ∷ b11 ∷ 𝟘 ∷ 𝟙 ∷ [])
+        , (b0  ∷ b1  ∷ b2  ∷ b3  ∷ b4  ∷ b5  ∷ 𝟘 ∷ 𝟙 ∷ [])
+          = real
+            ⟨ C.fromℕ (proj₁ (unbits {21}
+              ( b0  ∷ b1  ∷ b2  ∷ b3  ∷ b4  ∷ b5  ∷ b6  ∷ b7
+              ∷ b8  ∷ b9  ∷ b10 ∷ b11 ∷ b12 ∷ b13 ∷ b14 ∷ b15
+              ∷ b16 ∷ b17 ∷ b18 ∷ b19 ∷ b20 ∷ []
+              )))
+            , m≤n+m (suc m) 3
+            , xs ⟩
+    ... | _ = cake
 
-  parse-char : [ Parser C.Char ]
-  parse-char {n} .parse [] = cake
-  parse-char {n} .parse xs@(_ ∷ _) = case decode-≤-1 xs of λ where
-    (real x) → real x
-    cake → case xs of λ where
-      (_ ∷ []) → cake
-      (_ ∷ _ ∷ _) → case decode-≤-2 xs of λ where
-        (real x) → real x
-        cake → case xs of λ where
-          (_ ∷ _ ∷ []) → cake
-          (_ ∷ _ ∷ _ ∷ _) → case decode-≤-3 xs of λ where
-            (real x) → real x
-            cake → case xs of λ where
-              (_ ∷ _ ∷ _ ∷ []) → cake
-              (_ ∷ _ ∷ _ ∷ _ ∷ _) → decode-≤-4 xs
+    parse-char : [ Parser C.Char ]
+    parse-char {n} .parse [] = cake
+    parse-char {n} .parse xs@(_ ∷ _) = case decode-≤-1 xs of λ where
+      (real x) → real x
+      cake → case xs of λ where
+        (_ ∷ []) → cake
+        (_ ∷ _ ∷ _) → case decode-≤-2 xs of λ where
+          (real x) → real x
+          cake → case xs of λ where
+            (_ ∷ _ ∷ []) → cake
+            (_ ∷ _ ∷ _ ∷ _) → case decode-≤-3 xs of λ where
+              (real x) → real x
+              cake → case xs of λ where
+                (_ ∷ _ ∷ _ ∷ []) → cake
+                (_ ∷ _ ∷ _ ∷ _ ∷ _) → decode-≤-4 xs
 
   parse-string : [ Parser (List⁺ C.Char) ]
   parse-string = many-fix parse-char
 
-  decode-string : List Byte → Maybe (List C.Char)
-  decode-string []ˡ = real []ˡ
-  decode-string xs@(_ ∷ˡ _) with parse-string .parse (fromList xs)
-  ...                      | real ⟨ r , _ , [] ⟩ = real (list⁺-to-list r)
-  ...                      | _ = cake
+  decode-string : List Byte → Maybe String
+  decode-string L.[] = real ""
+  decode-string xs@(_ L.∷ _) with parse-string .parse (V.fromList xs)
+  ... | real ⟨ r , _ , V.[] ⟩ = real (S.fromList (list⁺-to-list r))
+  ... | _ = cake
 
 open decode using (decode-string; parse-string; parse-char) public
 
diff --git a/src/UTF-8/Test.agda b/src/UTF-8/Test.agda
index 84aa4f0..97f5d30 100644
--- a/src/UTF-8/Test.agda
+++ b/src/UTF-8/Test.agda
@@ -33,7 +33,7 @@ encode-∘ : encode-char '∘' ≡ < 0xe2 > ∷ˡ < 0x88 > ∷ˡ < 0x98 > ∷ˡ
 encode-∘ = refl
 encode-𐄣 : encode-char '𐄣' ≡ < 0xf0 > ∷ˡ < 0x90 > ∷ˡ < 0x84 > ∷ˡ < 0xa3 > ∷ˡ []ˡ
 encode-𐄣 = refl
-encode-blah : encode-string (S.toList "aö∘𐄣")
+encode-blah : encode-string "aö∘𐄣"
             ≡ < 0x61 >
             ∷ˡ < 0xc3 > ∷ˡ < 0xb6 >
             ∷ˡ < 0xe2 > ∷ˡ < 0x88 > ∷ˡ < 0x98 >
@@ -46,5 +46,5 @@ decode-blah : decode-string
             ∷ˡ < 0xe2 > ∷ˡ < 0x88 > ∷ˡ < 0x98 >
             ∷ˡ < 0xf0 > ∷ˡ < 0x90 > ∷ˡ < 0x84 > ∷ˡ < 0xa3 >
             ∷ˡ []ˡ )
-            ≡ real (S.toList "aö∘𐄣")
+            ≡ real "aö∘𐄣"
 decode-blah = refl