Merge branch 'sofia/async-http-h1' into sofia/async-http-server

src/Std/Internal/Http/Data/Body/Writer.lean

@@ -162,7 +162,7 @@ instance : Writer Full where
 instance : Writer Empty where
   send _ _ _ := throw <| .userError "cannot send"
   close _ := pure ()
-  isClosed _ := pure false
+  isClosed _ := pure true
   hasInterest _ := pure false
   getKnownSize _ := pure (some (.fixed 0))
   setKnownSize _ _ := pure ()

src/Std/Internal/Http/Internal/Char.lean

@@ -6,7 +6,6 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-import Std.Tactic.BVDecide
 public import Init.Data.String
 
 @[expose]

src/Std/Internal/Http/Protocol/H1.lean

@@ -893,7 +893,9 @@ def canContinue (machine : Machine dir) (status : Status) : Machine dir :=
         |>.setReaderState .closed
   | .receiving, _ => machine
 
-/-- Enqueues body chunks into the writer buffer for encoding and sending. -/
+/--
+Enqueues body chunks into the writer buffer for encoding and sending.
+-/
 @[inline]
 def sendData (machine : Machine dir) (data : Array Chunk) : Machine dir :=
   if data.isEmpty then
@@ -901,12 +903,16 @@ def sendData (machine : Machine dir) (data : Array Chunk) : Machine dir :=
   else
     machine.modifyWriter (fun writer => { writer with userData := writer.userData ++ data })
 
-/-- Takes and clears all accumulated events, returning the drained array. -/
+/--
+Takes and clears all accumulated events, returning the drained array.
+-/
 @[inline]
 def takeEvents (machine : Machine dir) : Machine dir × Array (Event dir) :=
   ({ machine with events := #[] }, machine.events)
 
-/-- Takes all accumulated output to send to the socket. -/
+/--
+Takes and clears accumulated output bytes, returning them as a buffer.
+-/
 @[inline]
 def takeOutput (machine : Machine dir) : Machine dir × ChunkedBuffer :=
   let output := machine.writer.outputData

src/Std/Internal/Http/Protocol/H1/Parser.lean

@@ -489,7 +489,8 @@ def parseReasonPhrase (limits : H1.Config) : Parser String := do
   liftOption <| String.fromUTF8? bytes.toByteArray
 
 /--
-Parses HTTP status code (3 digits)
+Parses a status-code (3 decimal digits), the following reason phrase, and the
+terminating CRLF; returns a typed `Status`.
 -/
 def parseStatusCode (limits : H1.Config) : Parser Status := do
   let d1 ← digit

src/Std/Internal/Http/Protocol/H1/Writer.lean

@@ -71,7 +71,7 @@ inductive Writer.State
   | complete
 
   /--
-  State that it has completed and cannot process more data.
+  Closed; no further data can be written.
   -/
   | closed
 deriving Inhabited, Repr, BEq