@[reducible, inline]

abbrev Std.Http.Internal.Test.TestHandler : Type

Equations

• Std.Http.Internal.Test.TestHandler = (Std.Http.Request Std.Http.Body.Stream → Std.Async.ContextAsync (Std.Http.Response Std.Http.Body.Any))

@[implicit_reducible]

instance Std.Http.Internal.Test.instHandlerTestHandler : Server.Handler TestHandler

Equations

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

def Std.Http.Internal.Test.defaultConfig : Config

Default config for server tests. Short lingering timeout, no Date header.

Equations

• Std.Http.Internal.Test.defaultConfig = { lingeringTimeout := 1000, generateDate := false }

def Std.Http.Internal.Test.runGroup (name : String) (tests : IO Unit) : IO Unit

Run tests and wrap any failure message with the group name. Use as #eval runGroup "Topic" do ....

Equations

• Std.Http.Internal.Test.runGroup name tests = tryCatch tests fun (e : IO.Error) => throw (IO.userError (toString "[" ++ toString name ++ toString "]\n" ++ toString e))

def Std.Http.Internal.Test.check (name raw : String) (handler : TestHandler) (expect : ByteArray → IO Unit) (config : Config := defaultConfig) : IO Unit

Create a fresh mock connection, send raw, and run assertions.

Equations

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

def Std.Http.Internal.Test.checkClose (name raw : String) (handler : TestHandler) (expect : ByteArray → IO Unit) (config : Config := defaultConfig) : IO Unit

Like check but closes the client channel before running the server. Use for tests involving truncated input or silent-close (EOF-triggered behavior).

Equations

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

def Std.Http.Internal.Test.checkTimed (name : String) (ms : Nat := 2000) (raw : String) (handler : TestHandler) (expect : ByteArray → IO Unit) (config : Config := defaultConfig) : IO Unit

Like check wrapped in a wall-clock timeout. Required when the test involves streaming, async timers, or keep-alive behavior.

Equations

• Std.Http.Internal.Test.checkTimed name ms raw handler expect config = Std.Http.Internal.Test.withTimeout✝ name ms (Std.Http.Internal.Test.check name raw handler expect config)

def Std.Http.Internal.Test.assertStatus (response : ByteArray) (prefix_ : String) : IO Unit

Assert the response starts with prefix_ (e.g. "HTTP/1.1 200").

Equations

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

def Std.Http.Internal.Test.assertExact (response : ByteArray) (expected : String) : IO Unit

Assert the response is byte-for-byte equal to expected. Use sparingly — prefer assertStatus + assertContains for 200 responses.

Equations

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

def Std.Http.Internal.Test.assertContains (response : ByteArray) (needle : String) : IO Unit

Assert needle appears anywhere in the response.

Equations

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

def Std.Http.Internal.Test.assertAbsent (response : ByteArray) (needle : String) : IO Unit

Assert needle does NOT appear in the response.

Equations

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

def Std.Http.Internal.Test.assertResponseCount (response : ByteArray) (n : Nat) : IO Unit

Assert the response contains exactly n occurrences of "HTTP/1.1 ".

Equations

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

def Std.Http.Internal.Test.r400 : String

Equations

• Std.Http.Internal.Test.r400 = "HTTP/1.1 400 Bad Request\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"

def Std.Http.Internal.Test.r408 : String

Equations

• Std.Http.Internal.Test.r408 = "HTTP/1.1 408 Request Timeout\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"

def Std.Http.Internal.Test.r413 : String

Equations

• Std.Http.Internal.Test.r413 = "HTTP/1.1 413 Content Too Large\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"

def Std.Http.Internal.Test.r417 : String

Equations

• Std.Http.Internal.Test.r417 = "HTTP/1.1 417 Expectation Failed\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"

def Std.Http.Internal.Test.r431 : String

Equations

• Std.Http.Internal.Test.r431 = "HTTP/1.1 431 Request Header Fields Too Large\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"

def Std.Http.Internal.Test.r505 : String

Equations

• Std.Http.Internal.Test.r505 = "HTTP/1.1 505 HTTP Version Not Supported\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"

def Std.Http.Internal.Test.okHandler : TestHandler

Always respond 200 "ok" without reading the request body.

Equations

• Std.Http.Internal.Test.okHandler x✝ = do let a ← liftM (Std.Http.Response.ok.text "ok") pure { line := a.line, body := Std.Http.Body.Any.ofBody a.body, extensions := a.extensions }

def Std.Http.Internal.Test.echoHandler : TestHandler

Read the full request body and echo it back as text/plain.

Equations

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

def Std.Http.Internal.Test.uriHandler : TestHandler

Respond 200 with the request URI as the body.

Equations

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

def Std.Http.Internal.Test.mkGet (path : String := "/") (extra : String := "") : String

Minimal GET request. extra is appended as raw header lines (each ending with \x0d\n) before the blank line.

Equations

• Std.Http.Internal.Test.mkGet path extra = toString "GET " ++ toString path ++ toString " HTTP/1.1\x0d\nHost: example.com\x0d\n" ++ toString extra ++ toString "\x0d\n"

def Std.Http.Internal.Test.mkGetClose (path : String := "/") : String

GET with Connection: close.

Equations

• Std.Http.Internal.Test.mkGetClose path = Std.Http.Internal.Test.mkGet path "Connection: close\x0d\n"

def Std.Http.Internal.Test.mkPost (path body : String) (extra : String := "") : String

POST with a fixed Content-Length body. extra is appended before the blank line.

Equations

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

def Std.Http.Internal.Test.mkChunked (path chunkedBody : String) (extra : String := "") : String

POST with Transfer-Encoding: chunked. chunkedBody is the pre-formatted body (use chunk + chunkEnd to build it).

Equations

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

def Std.Http.Internal.Test.chunk (data : String) : String

Format a single chunk: <hex-size>\x0d\n<data>\x0d\n.

Equations

• Std.Http.Internal.Test.chunk data = toString (String.ofList (Nat.toDigits 16 data.toUTF8.size)) ++ toString "\x0d\n" ++ toString data ++ toString "\x0d\n"

def Std.Http.Internal.Test.chunkEnd : String

The terminal zero-chunk that ends a chunked body.

Equations

• Std.Http.Internal.Test.chunkEnd = "0\x0d\n\x0d\n"