From 1ff2708d6e0ca1cebce6a93d2f0552858c46bd3d Mon Sep 17 00:00:00 2001
From: xenia <xenia.agda@gmail.com>
Date: Sat, 9 Sep 2023 12:57:04 +0200
Subject: [PATCH] string-to-ascii-list function

---
 src/Parse-HTTP/Helpers.agda | 3 +++
 src/Parse-HTTP/Test.agda    | 2 +-
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/Parse-HTTP/Helpers.agda b/src/Parse-HTTP/Helpers.agda
index b235395..af6966c 100644
--- a/src/Parse-HTTP/Helpers.agda
+++ b/src/Parse-HTTP/Helpers.agda
@@ -59,6 +59,9 @@ string-to-ascii-list⁺ s {ascii} {nonempty} = vec-to-list⁺ v
     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)
 
diff --git a/src/Parse-HTTP/Test.agda b/src/Parse-HTTP/Test.agda
index 0b1d432..1bb0c55 100644
--- a/src/Parse-HTTP/Test.agda
+++ b/src/Parse-HTTP/Test.agda
@@ -110,7 +110,7 @@ module Test-HTTP where
                      record { name = string-to-ascii-list⁺ "Content-Length" ; value = string-to-ascii-list⁺ "6" }
                      List.∷ record { name = string-to-ascii-list⁺ "Host" ; value = string-to-ascii-list⁺ "agda.nu" }
                      List.∷ List.[]
-                   ; content = real (list⁺-to-list (string-to-ascii-list⁺ "mjau:)"))
+                   ; content = real (string-to-ascii-list "mjau:)")
                    }
                  , _
                  , enc "\r\n"