Connection

This module defines Server.Connection, a structure used to handle a single HTTP connection with possibly multiple requests.

structure Std.Http.Server.RemoteAddr : Type

Represents the remote address of a client connection.

• addr : Net.SocketAddress

  The socket address of the remote client.

@[implicit_reducible]

instance Std.Http.Server.instTypeNameRemoteAddr : TypeName RemoteAddr

Equations

• Std.Http.Server.instTypeNameRemoteAddr = Std.Http.Server.inst✝

@[implicit_reducible]

instance Std.Http.Server.instToStringRemoteAddr : ToString RemoteAddr

Equations

• Std.Http.Server.instToStringRemoteAddr = { toString := fun (addr : Std.Http.Server.RemoteAddr) => toString addr.addr }

structure Std.Http.Server.Connection (α : Type) : Type

A single HTTP connection.

• socket : α

  The client connection.

• machine : Protocol.H1.Machine Protocol.H1.Direction.receiving

  The processing machine for HTTP/1.1.

• extensions : Extensions

  Extensions to attach to each request (e.g., remote address).

def Std.Http.Server.serveConnection {t σ : Type} [Transport t] [Handler σ] (client : t) (handler : σ) (config : Config) (extensions : Extensions := Extensions.empty) : Async.ContextAsync Unit

Handles request/response processing for a single connection using an Async handler. The library-level entry point for running a server is Server.serve. This function can be used with a TCP.Socket or any other type that implements Transport to build custom server loops.

Example

-- Create a TCP socket server instance
let server ← Socket.Server.mk
server.bind addr
server.listen backlog

-- Enter an infinite loop to handle incoming client connections
while true do
  let client ← server.accept
  background (serveConnection client handler config)

Equations

• One or more equations did not get rendered due to their size.