Migrate Server.serve to Std.Http.Server (4.31)

LeanTea/Net/Server.lean

@@ -1,83 +1,144 @@
 import LeanTea.Net.Http
-import Std.Async.TCP
+import Std.Http.Server
+import Std.Async
 import Std.Net
 
 /-! # TCP server loop driving the HTTP handler
 
-Sequential accept loop — one connection at a time. -/
+Previously a hand-rolled HTTP/1.1 accept loop on top of
+`Std.Internal.Async.TCP`. 4.31 ships a real `Std.Http.Server` with
+graceful shutdown, connection limits, `100-continue` handling, and
+proper async lifecycle — strictly more than what we wrote. We now
+sit on top of it.
+
+The public API stays:
+
+```
+LeanTea.Net.Server.serve port host handler
+```
+
+…where `handler : LeanTea.Net.Http.Request → IO LeanTea.Net.Http.Response`
+keeps the original shape. The conversion between our
+`Request`/`Response` (raw bytes, lowercased header array) and Std's
+strongly-typed `Std.Http.{Request, Response}` happens in this
+file. Anything more advanced (streaming bodies, Std's
+`ContextAsync`-aware handlers) belongs at the Std layer; this
+module is just the shim. -/
 
 namespace LeanTea.Net.Server
 
 open LeanTea.Net.Http
 open Std.Async
 open Std.Net
-open Std.Async.TCP
-
-private partial def recvAll (client : Socket.Client) (acc : ByteArray) : IO ByteArray := do
-  match splitHeaders acc with
-  | some (headersStr, bodySoFar) =>
-    -- Derive content-length from headers (case-insensitive lookup).
-    let lower := headersStr.toLower
-    let cl := match lower.splitOn "content-length:" with
-      | _ :: rest :: _ =>
-        let v := (rest.takeWhile (· != '\r')).toString.trim
-        v.toNat?.getD 0
-      | _ => 0
-    if bodySoFar.size ≥ cl then
-      return acc
-    let chunk ← (client.recv? 4096).block
-    match chunk with
-    | some b => recvAll client (acc ++ b)
-    | none   => return acc
-  | none =>
-    let chunk ← (client.recv? 4096).block
-    match chunk with
-    | some b => recvAll client (acc ++ b)
-    | none   => return acc
-
-private def handleConn (handler : Handler) (client : Socket.Client) : IO Unit := do
-  try
-    let raw ← recvAll client .empty
-    let body : ByteArray :=
-      match baFindSeq raw CRLFCRLF with
-      | some h => raw.extract (h + 4) raw.size
-      | none   => .empty
-    let resp ← match parseRequest raw body with
-      | some req =>
-        try
-          handler req
-        catch e =>
-          pure (Response.serverError s!"handler: {e}")
-      | none => pure Response.badRequest
-    let bytes := resp.toBytes
-    (client.send bytes).block
-    (client.shutdown).block
-  catch e =>
-    IO.eprintln s!"conn error: {e}"
-
-partial def serveLoop (server : Socket.Server) (handler : Handler) : IO Unit := do
-  let client ← (server.accept).block
-  handleConn handler client
-  serveLoop server handler
-
-/-- Parse a dotted IPv4 string ("127.0.0.1") into a `Std.Net.IPv4Addr`.
-    Returns `0.0.0.0` if parsing fails. -/
+open Std.Http
+open Std.Http.Server
+
+/-! ## Request adapter: Std → our `Request` -/
+
+private partial def drainStream (s : Body.Stream) (acc : ByteArray) : Async ByteArray := do
+  match ← s.recv with
+  | none       => return acc
+  | some chunk => drainStream s (acc ++ chunk.data)
+
+/-- Std's `URI.Query.toString` emits a leading `?`. Our public
+    `Request.query` carries the raw `k=v&k=v` body without it
+    (matching how the previous hand-rolled parser populated the
+    field), so strip the prefix here. -/
+private def queryStrip (s : String) : String :=
+  if s.startsWith "?" then (s.drop 1).toString else s
+
+private def pathAndQueryOf (target : RequestTarget) : String × String :=
+  match target with
+  | .originForm path query =>
+    let p : String := toString path
+    let q : String := match query with
+                      | some q => queryStrip (toString q)
+                      | none   => ""
+    (p, q)
+  | .absoluteForm uri =>
+    let p : String := toString uri.path
+    let q : String := queryStrip (toString uri.query)
+    (p, q)
+  | .authorityForm a => (toString a, "")
+  | .asteriskForm    => ("*", "")
+
+/-- Std's `Header.Name.toString` is the canonical PascalCase form;
+    our existing parser populated header names as lowercase, and
+    `Request.header?` compares against `name.toLower`. Preserve that
+    invariant by reading `n.value` (the underlying lowercased
+    representation) directly. -/
+private def headersToPairs (h : Headers) : Array (String × String) :=
+  h.toArray.map fun (n, v) => (n.value, v.value)
+
+/-- Convert a Std request (with stream body) into our raw record.
+    Drains the body up front so handlers see a complete `ByteArray`. -/
+def fromStd (req : Std.Http.Request Body.Stream) : Async LeanTea.Net.Http.Request := do
+  let (path, query) := pathAndQueryOf req.line.uri
+  let body ← drainStream req.body .empty
+  return {
+    method  := toString req.line.method,
+    path,
+    query,
+    headers := headersToPairs req.line.headers,
+    body
+  }
+
+/-! ## Response adapter: our `Response` → Std -/
+
+private def statusOfNat (n : Nat) : Status :=
+  (Status.ofCode none n.toUInt16).getD .ok
+
+private def headersFromPairs (pairs : Array (String × String)) : Headers := Id.run do
+  let mut h := Headers.empty
+  for (k, v) in pairs do
+    h := h.insert! k v
+  return h
+
+/-- Convert our raw response into a Std response with a `Body.Full`
+    payload (the bytes the handler computed). -/
+def toStd (resp : LeanTea.Net.Http.Response) : Async (Std.Http.Response Body.Any) := do
+  let head : Response.Head := {
+    status  := statusOfNat resp.status,
+    version := .v11,
+    headers := headersFromPairs resp.headers
+  }
+  let full ← Body.Full.ofByteArray resp.body
+  return { line := head, body := .ofBody full, extensions := .empty }
+
+/-! ## Handler bridge -/
+
+private structure LegacyHandler where
+  inner : LeanTea.Net.Http.Handler
+
+instance : Std.Http.Server.Handler LegacyHandler where
+  ResponseBody := Body.Any
+  onRequest h req := do
+    let our ← fromStd req
+    /- `IO → ContextAsync` is a MonadLift instance in Std.Async,
+       so we can simply `← h.inner our` without an explicit lift. -/
+    let resp ← h.inner our
+    toStd resp
+
+/-! ## IPv4 helper -/
+
 def parseIPv4 (s : String) : IPv4Addr :=
   let zero : IPv4Addr := ⟨#v[0, 0, 0, 0]⟩
   match (s.splitOn ".").map (·.toNat?.getD 0) with
   | [a, b, c, d] => ⟨#v[a.toUInt8, b.toUInt8, c.toUInt8, d.toUInt8]⟩
   | _ => zero
 
+/-- Run an HTTP server on `port` / `host` with the given
+    LeanTEA-shaped handler. Blocks until the underlying
+    `Std.Http.Server` is shut down. -/
 def serve (port : UInt16 := 8001) (host : String := "0.0.0.0")
     (handler : Handler) : IO Unit := do
-  let server ← Socket.Server.mk
   let addr : SocketAddress := .v4 {
     addr := parseIPv4 host,
     port := port
   }
-  server.bind addr
-  server.listen 64
   IO.eprintln s!"serving on http://{host}:{port}/"
-  serveLoop server handler
+  Async.block do
+    let server ← Std.Http.Server.serve addr (LegacyHandler.mk handler) {}
+    server.waitShutdown
 
 end LeanTea.Net.Server