fix: small fixes

Http/Data/Cookie/Parser.lean

@@ -36,7 +36,6 @@ private def sameSiteAttribute : Lean.Parsec SameSite := do
 -- TODO: Add 'token' parsr class satisfy instead of this
 private def parseAttribute (cookie: Cookie) : Lean.Parsec Cookie := do
   let name ← token
-  dbg_trace name
   match name.toLower with
   | "samesite" => return { cookie with sameSite := (← skipChar '=' *> sameSiteAttribute) }
   | "expires" => return { cookie with expires := (← skipChar '=' *> expiresAttribute) }

Http/Data/Headers.lean

@@ -78,11 +78,13 @@ instance : ToString Headers where
 def Headers.empty : Headers := Lean.HashMap.empty
 
 /-- Adds a new value to the header map -/
-def Headers.add (headers: Headers) (name: HeaderName) (value: String) : Headers :=
-  dbg_trace (repr name)
+def Headers.addRaw (headers: Headers) (name: HeaderName) (value: String) : Headers :=
   let arr := (· ++ ", " ++ value) <$> headers.find? name
   headers.insert name (arr.getD value)
 
+def Headers.add [i:Http.Classes.Canonical α] (headers: Headers) (name: HeaderName) (value: α) : Headers :=
+  headers.addRaw name (i.repr value)
+
 /-- Get the first value of a header s-/
 def Headers.find? (headers: Headers) (name: HeaderName) [i: HeaderVal name α] : Option α := do
   let res ← HashMap.find? headers name

Http/Data/Headers/Other/Date.lean

@@ -13,7 +13,7 @@ open Http.Classes
 -/
 def Date := Time.DateTime .GMT
 
-instance : Canonical Date where
+instance : Canonical (Time.DateTime .GMT) where
   repr date := RFC822.format date
 
 instance : Header .date Date where

Http/IO/Connection.lean

@@ -56,5 +56,7 @@ def Connection.end (connection: Connection) (alive: Bool) : IO Unit := connectio
     if res.isSome then
       connection.rawWrite (ToBuffer.toBuffer #[] Chunk.zeroed)
 
+  connection.response.set Data.Response.empty
+
   if !alive then
     connection.close

Http/IO/Server.lean

@@ -24,7 +24,7 @@ def onConnection (conn: IO.Ref Connection) (onConn: Connection → IO Unit) (req
 
 def badRequest (conn: Connection) := do
   let headers := Headers.empty
-              |>.add "Connection" "close"
+              |>.addRaw "connection" "close"
 
   let response := Response.mk (Status.badRequest) (Version.v11) headers
   let _ ← conn.write (Chunk.mk Headers.empty (ToString.toString response).toUTF8)
@@ -61,7 +61,6 @@ def readSocket
         let data ← ref.get
         let res ← IO.toUVIO $ Parser.feed data bytes
         ref.set res
-        IO.toUVIO $ IO.println s!"--- {res.error} {repr res.state}"
         if res.error ≠ 0 then
           let conn ← connRef.get
           IO.toUVIO $ badRequest conn

Http/Protocols/Http1/Data/Chunk.lean

@@ -71,7 +71,7 @@ def TrailersImp.valid (name: String.CI) : Bool :=
 def TrailersImp.add (trailers: TrailersImp) (name: String) (value: String) : TrailersImp :=
   let ci := String.CI.new name
   if TrailersImp.valid ci
-    then Headers.add trailers (Standard.parse name) value
+    then Headers.addRaw trailers (Standard.parse name) value
     else trailers
 
 inductive TrailersImp.WellFormed : TrailersImp → Prop where

Http/Protocols/Http1/Parser.lean

@@ -77,14 +77,14 @@ private def endField (data: State) : IO (State × Nat) := do
           else (data, true)
     | _ => (data, true)
 
-  let headers := data.req.headers.add prop value
+  let headers := data.req.headers.addRaw prop value
   pure ({ data with req := { data.req with headers }, prop := "", value := ""}, if code then 0 else 1)
 
 private def onEndFieldExt (data: State) : IO (State × Nat) := do
   let prop := data.prop.toLower
   let value := data.value
 
-  let chunkHeaders := data.chunkHeaders.add prop value
+  let chunkHeaders := data.chunkHeaders.addRaw prop value
   pure ({ data with chunkHeaders, prop := "", value := ""}, 0)
 
 private def onEndFieldTrailer (data: State) : IO (State × Nat) := do

Http/Util/Format.lean

@@ -7,12 +7,12 @@ def toHexChar (n : Nat) : Char :=
 
 def toHex (n : Nat) : String := Id.run do
   let mut value := n
-  let mut result := ""
+  let mut result := #[]
   if value == 0 then return "0"
 
   while value > 0 do
     let digit := value % 16
     result := result.push $ toHexChar digit
     value := value / 16
 
-  return result
+  return result.reverse.foldl String.push ""