feat: cancellation backwards

Author: algebraic-dev

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

@@ -90,18 +90,18 @@ instance : ForIn ContextAsync Body Chunk where
     | .stream stream' => ByteStream.forIn' stream' acc step
 
 /--
-Collect all data from the body into a single `ByteArray`. This reads the entire body content into memory,
-so use with caution for large bodies as it may consume significant memory.
+Collect all data from the body into a single `ByteArray`. This reads the entire body content into memory
+and consumes significant memory for large bodies.
 -/
 def collectByteArray (body : Body) : Async ByteArray := do
   let mut result := .empty
   for x in body do result := result ++ x.data
   return result
 
 /--
-Collect all data from the body into a single `String`. This reads the entire body content into memory,
-so use with caution for large bodies as it may consume significant memory. If it is a valid UTF-8 string
-then it will return `some` otherwise `none`.
+Collect all data from the body into a single `String`. This reads the entire body content into memory
+and consumes significant memory for large bodies. Returns `some` if the data is valid UTF-8, otherwise
+`none`.
 -/
 def collectString (body : Body) : Async (Option String) := do
   let mut result := .empty

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

@@ -20,7 +20,7 @@ public section
 
 A `ByteStream` represents an asynchronous channel for streaming byte data in chunks. It provides an
 interface for producers and consumers to exchange byte arrays with optional chunk metadata (extensions),
-aking it suitable for HTTP chunked transfer encoding and other streaming scenarios.
+making it suitable for HTTP chunked transfer encoding and other streaming scenarios.
 -/
 
 namespace Std.Http.Body
@@ -54,8 +54,8 @@ def empty : Async ByteStream :=
   emptyWithCapacity
 
 /--
-Tries to receive a chunk from the stream. Returns `some` with a chunk when data is available, or `none`
-hen the stream is closed or no data is available.
+Attempts to receive a chunk from the stream. Returns `some` with a chunk when data is available, or `none`
+when the stream is closed or no data is available.
 -/
 def tryRecv (stream : ByteStream) : Async (Option Chunk) := do
   stream.channel.tryRecv
@@ -89,17 +89,17 @@ def write (stream : ByteStream) (data : ByteArray) (extensions : Array (String 
   if data.isEmpty then
     return
 
-  let chunk : Chunk := { data := data, extensions := extensions }
+  let chunk := { data := data, extensions := extensions }
   let task ← stream.channel.send chunk
-  let task : AsyncTask _ := task.map (Except.mapError (fun x => userError (toString x)))
+  let task := task.map (Except.mapError (fun x => userError (toString x)))
   Async.ofAsyncTask task
 
 /--
 Writes a complete chunk with extensions to the stream.
 -/
 def writeChunk (stream : ByteStream) (chunk : Chunk) : Async Unit := do
   let task ← stream.channel.send chunk
-  let task : AsyncTask _ := task.map (Except.mapError (fun x => userError (toString x)))
+  let task := task.map (Except.mapError (fun x => userError (toString x)))
   Async.ofAsyncTask task
 
 /--
@@ -112,7 +112,7 @@ def getKnownSize (stream : ByteStream) : Async (Option Body.Length) := do
 
 /--
 Sets the known size of the stream.
-This is typically used when the total expected size is known ahead of time.
+Use this when the total expected size is known ahead of time.
 -/
 def setKnownSize (stream : ByteStream) (size : Option Body.Length) : Async Unit := do
   stream.knownSize.atomically do

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

@@ -13,7 +13,7 @@ public section
 /-!
 # Length
 
-This module defines the `Length` structure, that represents the Content-Length or Transfer-Encoding
+This module defines the `Length` type, that represents the Content-Length or Transfer-Encoding
 of an HTTP Request or response.
 -/
 

src/Std/Internal/Http/Data/Header/Map.lean

@@ -44,7 +44,7 @@ deriving Repr, Inhabited
 namespace Headers
 
 /--
-Tries to retrieve the `HeaderValue` for the given key.
+Retrieves the `HeaderValue` for the given key.
 Returns `none` if the header is absent.
 -/
 @[inline]
@@ -53,15 +53,15 @@ def get (headers : Headers) (name : HeaderName) : Option HeaderValue :=
   |>.map (.joinCommaSep)
 
 /--
-Tries to retrieve the `HeaderValue` for the given key.
+Retrieves all `HeaderValue` entries for the given key.
 Returns `none` if the header is absent.
 -/
 @[inline]
 def getAll? (headers : Headers) (name : HeaderName) : Option (Array HeaderValue) :=
   headers.data.get? name
 
 /--
-Tries to check if the entry is present in the `Headers`
+Checks if the entry is present in the `Headers`.
 -/
 @[inline]
 def hasEntry (headers : Headers) (name : HeaderName) (value : String) : Bool :=
@@ -70,7 +70,7 @@ def hasEntry (headers : Headers) (name : HeaderName) (value : String) : Bool :=
   |>.isSome
 
 /--
-Tries to retrieve the last header value for the given key.
+Retrieves the last header value for the given key.
 Returns `none` if the header is absent.
 -/
 @[inline]
@@ -80,7 +80,7 @@ def getLast? (headers : Headers) (name : HeaderName) : Option HeaderValue :=
 
 
 /--
-Like `get?`, but returns an empty HashSet if absent.
+Like `get?`, but returns a default value if absent.
 -/
 @[inline]
 def getD (headers : Headers) (name : HeaderName) (d : HeaderValue) : HeaderValue :=

src/Std/Internal/Http/Data/Header/Name.lean

@@ -105,9 +105,7 @@ def append (l : HeaderValue) (r : HeaderValue) : HeaderValue :=
   ⟨l.value ++ r.value, ?_⟩
 where finally
   unfold isValidHeaderValue
-  rw [String.toList_append]
-  rw [List.all_append]
-  rw [Bool.and_eq_true]
+  rw [String.toList_append, List.all_append, Bool.and_eq_true]
   constructor
   · exact l.validHeaderValue
   · exact r.validHeaderValue

src/Std/Internal/Http/Data/URI.lean

@@ -24,15 +24,15 @@ namespace Std.Http.RequestTarget
 set_option linter.all true
 
 /--
-Attempt to parse a `RequestTarget` from the given string.
+Attempts to parse a `RequestTarget` from the given string.
 -/
 @[inline]
 def parse? (string : String) : Option RequestTarget :=
   (Parser.parseRequestTarget <* Std.Internal.Parsec.eof).run string.toUTF8 |>.toOption
 
 
 /--
-Parse a `RequestTarget` from the given string. Panics if parsing fails. Use `parse?`
+Parses a `RequestTarget` from the given string. Panics if parsing fails. Use `parse?`
 if you need a safe option-returning version.
 -/
 @[inline]

src/Std/Internal/Http/Data/URI/Basic.lean

@@ -20,7 +20,7 @@ URI scheme (e.g., "http", "https", "ftp").
 abbrev Scheme := String
 
 /--
-User information component that usually contains the username and password.
+User information component containing the username and password.
 -/
 abbrev UserInfo := String
 
@@ -29,7 +29,7 @@ Host component of a URI, supporting domain names and IP addresses.
 -/
 inductive Host
   /--
-  A registered name (typically a domain name).
+  A registered name (e.g., a domain name).
   -/
   | name (name : String)
 
@@ -58,7 +58,7 @@ instance : Repr Host where
     | Host.ipv6 a => repr "ipv6" (toString a)
 
 /--
-TCP number port.
+TCP port number.
 -/
 abbrev Port := UInt16
 
@@ -70,7 +70,7 @@ on the network.
 -/
 structure Authority where
   /--
-  Optional user information like user and password.
+  Optional user information such as username and password.
   -/
   userInfo: Option UserInfo := none
 
@@ -162,12 +162,12 @@ inductive RequestTarget where
   | absoluteForm (uri : URI)
 
   /--
-  Request target using the authority-form, typically for CONNECT requests.
+  Request target using the authority-form (used for CONNECT requests).
   -/
   | authorityForm (authority : URI.Authority)
 
   /--
-  Asterisk-form request target, typically used with OPTIONS requests.
+  Asterisk-form request target (used with OPTIONS requests).
   -/
   | asteriskForm
 deriving Inhabited, Repr
@@ -223,8 +223,8 @@ private def byteToHex (b : UInt8) : ByteArray :=
   ByteArray.mk #['%'.toUInt8, hi, lo]
 
 /--
-Encodes a string as a URI component by percent-encoding all characters
---/
+Encodes a string as a URI component by percent-encoding all characters.
+-/
 def encodeURIComponent (s : String) : ByteArray :=
   s.toUTF8.foldl (init := ByteArray.emptyWithCapacity s.utf8ByteSize) fun acc c =>
     if isUnreserved c then  acc.push c else acc.append (byteToHex c)

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

@@ -336,7 +336,10 @@ def setHeaders (messageHead : Message.Head dir.swap) (machine : Machine dir) : M
 /-- Put some data inside the input of the machine. -/
 @[inline]
 def feed (machine : Machine ty) (data : ByteArray) : Machine ty :=
-  { machine with reader := machine.reader.feed data }
+  if machine.isReaderClosed then
+    machine
+  else
+    { machine with reader := machine.reader.feed data }
 
 /-- Signal that reader is not going to receive any more messages. -/
 @[inline]