feat: introduce Body type class and some Body types for HTTP

src/Std/Internal/Http/Data.lean

@@ -14,6 +14,7 @@ public import Std.Internal.Http.Data.Status
 public import Std.Internal.Http.Data.Chunk
 public import Std.Internal.Http.Data.Headers
 public import Std.Internal.Http.Data.URI
+public import Std.Internal.Http.Data.Body
 
 /-!
 # HTTP Data Types

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

@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Std.Internal.Async.ContextAsync
+public import Std.Internal.Http.Data.Headers
+public import Std.Internal.Http.Data.Body.Basic
+public import Std.Internal.Http.Data.Body.Length
+public import Std.Internal.Http.Data.Body.Reader
+public import Std.Internal.Http.Data.Body.Writer
+public import Std.Internal.Http.Data.Body.Stream
+public import Std.Internal.Http.Data.Body.Empty
+public import Std.Internal.Http.Data.Body.Full

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

@@ -0,0 +1,61 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Std.Internal.Async.ContextAsync
+public import Std.Internal.Http.Data.Headers
+public import Std.Internal.Http.Data.Body.Length
+
+public section
+
+/-!
+# Body.Basic
+
+This module defines shared types for HTTP body handling.
+-/
+
+namespace Std.Http.Body
+
+set_option linter.all true
+
+/--
+Typeclass for types that can be converted to a `ByteArray`.
+-/
+class ToByteArray (α : Type) where
+
+  /--
+  Transforms into a `ByteArray`.
+  -/
+  toByteArray : α → ByteArray
+
+instance : ToByteArray ByteArray where
+  toByteArray := id
+
+instance : ToByteArray String where
+  toByteArray := String.toUTF8
+
+/--
+Typeclass for types that can be decoded from a `ByteArray`. The conversion may fail with an error
+message if the bytes are not valid for the target type.
+-/
+class FromByteArray (α : Type) where
+
+  /--
+  Attempts to decode a `ByteArray` into the target type, returning an error message on failure.
+  -/
+  fromByteArray : ByteArray → Except String α
+
+instance : FromByteArray ByteArray where
+  fromByteArray := .ok
+
+instance : FromByteArray String where
+  fromByteArray bs :=
+    match String.fromUTF8? bs with
+    | some s => .ok s
+    | none => .error "invalid UTF-8 encoding"
+
+end Std.Http.Body

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

@@ -0,0 +1,103 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Std.Internal.Async
+public import Std.Internal.Http.Data.Request
+public import Std.Internal.Http.Data.Response
+public import Std.Internal.Http.Data.Body.Length
+public import Std.Internal.Http.Data.Body.Reader
+public import Std.Internal.Http.Data.Chunk
+
+public section
+
+/-!
+# Body.Empty
+
+Represents an always-empty, already-closed body handle.
+-/
+
+namespace Std.Http.Body
+open Std Internal IO Async
+
+set_option linter.all true
+
+/--
+An empty body handle.
+-/
+structure Empty where
+deriving Inhabited
+
+namespace Empty
+
+/--
+Receives from an empty body, always returning end-of-stream.
+-/
+@[inline]
+def recv (_ : Empty) : Async (Option Chunk) :=
+  pure none
+
+/--
+Closes an empty body (no-op).
+-/
+@[inline]
+def close (_ : Empty) : Async Unit :=
+  pure ()
+
+/--
+Empty bodies are always closed for reading.
+-/
+@[inline]
+def isClosed (_ : Empty) : Async Bool :=
+  pure true
+
+open Internal.IO.Async in
+
+/--
+Selector that immediately resolves with end-of-stream for an empty body.
+-/
+@[inline]
+def recvSelector (_ : Empty) : Selector (Option Chunk) where
+  tryFn := pure (some none)
+  registerFn waiter := do
+    let lose := pure ()
+    let win promise := do
+      promise.resolve (.ok none)
+    waiter.race lose win
+  unregisterFn := pure ()
+
+end Empty
+
+instance : Reader Empty where
+  recv := Empty.recv
+  close := Empty.close
+  isClosed := Empty.isClosed
+  recvSelector := Empty.recvSelector
+
+end Std.Http.Body
+
+namespace Std.Http.Request.Builder
+open Internal.IO.Async
+
+/--
+Builds a request with an empty body.
+-/
+def blank (builder : Builder) : Async (Request Body.Empty) :=
+  pure <| builder.body {}
+
+end Std.Http.Request.Builder
+
+namespace Std.Http.Response.Builder
+open Internal.IO.Async
+
+/--
+Builds a response with an empty body.
+-/
+def blank (builder : Builder) : Async (Response Body.Empty) :=
+  pure <| builder.body {}
+
+end Std.Http.Response.Builder