fix: small chunk fixes and grammar corrections

Http/Data/Headers/Name.lean

@@ -9,6 +9,7 @@ open Lean
 inductive TransferEncoding where
   | chunked
   | custom (value: String)
+  deriving BEq
 
 inductive HeaderName.Standard where
   | date

Http/Data/Status.lean

@@ -135,6 +135,21 @@ def Status.toCode : Status -> Nat
   | notExtended                   => 510
   | networkAuthenticationRequired => 511
 
+def isInformational (c : Status) :=
+  c.toCode < 200
+
+def isSuccess (c : Status) :=
+  200 ≤ c.toCode ∧ c.toCode < 300
+
+def isRedirection (c : Status) :=
+  300 ≤ c.toCode ∧ c.toCode < 400
+
+def isClientError (c : Status) :=
+  400 ≤ c.toCode ∧ c.toCode < 500
+
+def isServerError (c : Status) :=
+  500 ≤ c.toCode ∧ c.toCode < 600
+
 def Status.fromCode : Nat → Option Status
   | 100 => Option.some continued
   | 101 => Option.some switchingProtocols

Http/IO/Connection.lean

@@ -7,6 +7,10 @@ import LibUV
 
 namespace Http.IO
 
+open Http.Protocols.Http1.Data
+open Http.Data.HeaderName
+open Http.Data
+
 structure Connection where
   isClosing: IO.Ref Bool
   isChunked: Bool
@@ -29,8 +33,8 @@ def Connection.close (connection: Connection) : IO Unit := connection.guard do
   UV.IO.run connection.socket.stop
   connection.isClosing.set true
 
-def Connection.write [Serialize α] (connection: Connection) (data: α) : IO Unit := connection.guard do
-  connection.buffer.modify (ToBuffer.toBuffer · data)
+def Connection.write [Coe α Chunk] (connection: Connection) (data: α) : IO Unit := connection.guard do
+  connection.buffer.modify (ToBuffer.toBuffer · (Coe.coe data : Chunk))
 
 def Connection.rawWrite (connection: Connection) (buffer: Buffer) : IO Unit := do
   UV.IO.run do let _ ← connection.socket.write buffer (λ_ => pure ())
@@ -41,7 +45,13 @@ def Connection.flushBody (connection: Connection) : IO Unit := connection.guard
 
 def Connection.end (connection: Connection) (alive: Bool) : IO Unit := connection.guard do
   let response ← connection.response.get
+
   connection.rawWrite (ToBuffer.toBuffer #[] response)
   connection.flushBody
+
+  if let some (res : Array TransferEncoding) := response.headers.findAll? Standard.transferEncoding then
+    if res.contains TransferEncoding.chunked then
+      connection.rawWrite (ToBuffer.toBuffer #[] Chunk.zeroed)
+
   if !alive then
     connection.close

Http/Protocols/Http1/Data/Chunk.lean

@@ -17,6 +17,9 @@ structure Chunk where
 def Chunk.fromString (x: String) : Chunk :=
   Chunk.mk Data.Headers.empty (String.toUTF8 x)
 
+def Chunk.zeroed : Chunk :=
+  Chunk.mk Inhabited.default ByteArray.empty
+
 /-- '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
@@ -31,3 +34,15 @@ instance : Serialize Chunk where
     BufferBuilder.write "\r\n"
     BufferBuilder.write chunk.data
     BufferBuilder.write "\r\n"
+
+instance : Coe String Chunk where
+  coe := Chunk.fromString
+
+instance : Coe ByteArray Chunk where
+  coe := Chunk.mk Inhabited.default
+
+instance : Coe Chunk Chunk where
+  coe := id
+
+instance : Coe (Array ByteArray) Chunk where
+  coe := Chunk.mk Inhabited.default ∘ Array.foldl ByteArray.append ByteArray.empty

Http/Protocols/Http1/Grammar.lean

@@ -148,7 +148,7 @@ parser Grammar in Lean where
 
     node contentLength where
       peek '\r' (end value selectLineEnd)
-      is digit (call (mulAdd octal contentLength) contentLength)
+      is digit (call (mulAdd decimal contentLength) contentLength)
 
     node fieldLineValue where
       peek '\r' (end value selectLineEnd)