feat: adds a simple Http library to Std

src/Std/Internal.lean

@@ -9,6 +9,7 @@ prelude
 public import Std.Internal.Async
 public import Std.Internal.Parsec
 public import Std.Internal.UV
+public import Std.Internal.Http
 
 @[expose] public section
 

src/Std/Internal/Async/Basic.lean

@@ -138,6 +138,13 @@ Construct an `ETask` that is already resolved with value `x`.
 protected def pure (x : α) : ETask ε α :=
   Task.pure <| .ok x
 
+/--
+Returns `true` if a `ETask` has finished it's execution
+-/
+@[inline]
+protected def isFinished (x : ETask ε α) : BaseIO Bool := do
+  return (← IO.getTaskState x) == IO.TaskState.finished
+
 /--
 Creates a new `ETask` that will run after `x` has finished. If `x`:
 - errors, return an `ETask` that resolves to the error.
@@ -242,6 +249,13 @@ Construct an `AsyncTask` that is already resolved with value `x`.
 protected def pure (x : α) : AsyncTask α :=
   Task.pure <| .ok x
 
+/--
+Returns `true` if a `AsyncTask` has finished it's execution
+-/
+@[inline]
+protected def isFinished (x : AsyncTask α) : BaseIO Bool := do
+  return (← IO.getTaskState x) == IO.TaskState.finished
+
 /--
 Create a new `AsyncTask` that will run after `x` has finished.
 If `x`:

src/Std/Internal/Http.lean

@@ -0,0 +1,65 @@
+/-
+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.Http.Data
+public import Std.Internal.Http.Server
+
+public section
+
+namespace Std
+namespace Http
+
+set_option linter.all true
+
+/-!
+# Http
+
+A "low-level" HTTP 1.1 implementation for Lean. It is designed to be used with or without the
+`Async` library if you want to implement a custom `Connection`.
+
+# Overview
+
+This module of the standard library defines many concepts related to the HTTP protocol
+and its semantics in a Sans-IO format. The main function of this library is `Std.Http.Server.serve`,
+located in the module `Std.Internal.Http.Server`. It starts a simple HTTP/1.1 server that
+handles all requests and sends them to a simple handler function. It uses the default `Std.Internal.Async`
+library, but it can be customized to use whatever IO library you want, as the protocol implementation
+is pure.
+
+If you want to customize how your server handles sockets, you can use `Std.Http.Server.serveConnection`,
+which is a simple function to bind a handler to a `ClientConnection`.
+
+# Low-Level Protocol Implementation
+
+This library provides a low-level foundation that allows you to implement your own IO layer on top
+of it. The core protocol parsing and generation logic is available in `Std.Internal.Http.Protocol`,
+which provides pure functions for HTTP message parsing and serialization. This design allows you to
+integrate the HTTP protocol handling with any IO system or networking library of your choice, while
+reusing the robust protocol implementation.
+
+# Minimal Example
+
+```lean
+import Std.Internal.Http
+import Std.Internal.Async
+
+open Std.Internal.IO.Async
+open Std Http
+
+def handler (req : Request Body) : Async (Response Body) := do
+  let some data ← req.body.collectString
+    | return Response.badRequest "expected a utf8 body"
+
+  return Response.ok ("hi, " ++ data)
+
+def mainAsync : Async Unit := do
+  Server.serve (.v4 (.mk (.ofParts 0 0 0 0) 8080)) handler
+
+def main := mainAsync.block
+```
+-/

src/Std/Internal/Http/Data.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.Http.Data.Body
+public import Std.Internal.Http.Data.Headers
+public import Std.Internal.Http.Data.Method
+public import Std.Internal.Http.Data.Version
+public import Std.Internal.Http.Data.Request
+public import Std.Internal.Http.Data.Response
+public import Std.Internal.Http.Data.URI
+public import Std.Internal.Http.Data.Status
+public import Std.Internal.Http.Data.Version

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

@@ -0,0 +1,116 @@
+/-
+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.Http.Data.Body.Length
+public import Std.Internal.Http.Data.Body.ByteStream
+
+public section
+
+open Std Internal IO Async
+
+namespace Std
+namespace Http
+
+set_option linter.all true
+
+/--
+Type that represents the body of a request or response with streams of bytearrays or bytearrays of fixed
+size.
+-/
+inductive Body where
+  /--
+  Empty body with no content
+  -/
+  | zero
+
+  /--
+  Body containing raw byte data stored in memory
+  -/
+  | bytes (data : ByteArray)
+
+  /--
+  Body containing streaming data from a byte stream channel
+  -/
+  | stream (channel : Body.ByteStream)
+deriving Inhabited
+
+namespace Body
+
+/--
+Get content length of a body (if known).
+-/
+def getContentLength (body : Body) : Length :=
+  match body with
+  | zero => .fixed 0
+  | .bytes data => .fixed data.size
+  | .stream _ => .chunked
+
+/--
+Close the body and release any associated resources. For streaming bodies, this closes the underlying channel.
+For other body types, this is a no-op.
+-/
+def close (body : Body) : Async Unit :=
+  match body with
+  | .stream channel => channel.close
+  | _ => pure ()
+
+instance : Coe String Body where
+  coe := .bytes ∘ String.toUTF8
+
+instance : Coe ByteArray Body where
+  coe := .bytes
+
+instance : Coe Body.ByteStream Body where
+  coe := .stream
+
+/--
+Iterate over the body content in chunks, processing each ByteArray chunk with the given step function.
+This allows for memory-efficient processing of large bodies without loading everything into memory at once.
+-/
+@[inline]
+protected partial def forIn
+  {β : Type} (body : Body) (acc : β)
+  (step : ByteArray → β → Async (ForInStep β)) :
+  Async β := do
+    let rec @[specialize] loop (stream : ByteStream) (acc : β) : Async β := do
+      if let some data ← stream.recv then
+        match ← step data acc with
+        | .done res => pure res
+        | .yield res => loop stream res
+      else
+        return acc
+
+    match body with
+    | .zero => pure acc
+    | .bytes data =>
+      match ← step data acc with
+      | .done x => pure x
+      | .yield x => pure x
+    | .stream strea => loop strea acc
+
+instance : ForIn Async Body ByteArray where
+  forIn := Body.forIn
+
+/--
+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.
+-/
+def collectByteArray (body : Body) : Async ByteArray := do
+  let mut result := .empty
+  for x in body do result := result ++ x
+  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's a valid UTF8 string
+then it will return `some` otherwise `none`.
+-/
+def collectString (body : Body) : Async (Option String) := do
+  let mut result := .empty
+  for x in body do result := result ++ x
+  return String.fromUTF8? result