From 81af33536b40359b4a7481a5526c132213df1f4e Mon Sep 17 00:00:00 2001
From: Sofia Rodrigues <sofia@algebraic.dev>
Date: Fri, 31 May 2024 14:51:06 -0300
Subject: [PATCH] fix: problem with chunked encoding

---
 Http.lean                            | 2 +-
 Http/Protocols/Http1/Data/Chunk.lean | 9 ++++++++-
 2 files changed, 9 insertions(+), 2 deletions(-)

diff --git a/Http.lean b/Http.lean
index 0b5a0d6..ae1f784 100644
--- a/Http.lean
+++ b/Http.lean
@@ -6,4 +6,4 @@ namespace Http
 
 export Http.IO (Connection)
 export Http.IO.Server (server)
-export Http.Protocols.Http1.Data (Chunk Trailers)
+export Http.Protocols.Http1.Data (Chunk Trailers Chunk.fromString)
diff --git a/Http/Protocols/Http1/Data/Chunk.lean b/Http/Protocols/Http1/Data/Chunk.lean
index 9ca2af4..78e7f4b 100644
--- a/Http/Protocols/Http1/Data/Chunk.lean
+++ b/Http/Protocols/Http1/Data/Chunk.lean
@@ -14,14 +14,21 @@ structure Chunk where
   extensions: Http.Data.Headers
   data: ByteArray
 
+def Chunk.fromString (x: String) : Chunk :=
+  Chunk.mk Data.Headers.empty (String.toUTF8 x)
+
 /-- 'Trailer' is defined as a type alias for Headers, which represents the trailing headers that may
 be sent after the last chunk in an HTTP/1.1 response. -/
 abbrev Trailers := Http.Data.Headers
 
 instance : ToString Chunk where
   toString s := String.fromUTF8! s.data
+
 instance : Serialize Chunk where
   serialize chunk := do
     let extensions := chunk.extensions.headers.toList.map $ λ(k, v) => ";" ++ k ++ ": " ++ String.quote (String.intercalate ", " v.toList)
-    BufferBuilder.write (String.intercalate "\r\n" extensions)
+    BufferBuilder.write (toHex chunk.data.size)
+    BufferBuilder.write (String.join extensions)
+    BufferBuilder.write "\r\n"
     BufferBuilder.write chunk.data
+    BufferBuilder.write "\r\n"