Body.Full

A body backed by a fixed ByteArray. The first call to recv returns the full byte array as a single chunk; subsequent calls return none (end-of-stream). Closing the body marks it closed. resetInPlace resets state to ready so the body can be read again.

structure Std.Http.Body.Full : Type

A body backed by a fixed ByteArray.

Unlike Body.Stream, a Full body is replayable: resetInPlace resets the state to ready so the same body can be read again.

• data : ByteArray
• state : Std.Mutex State

instance Std.Http.Body.instNonemptyFull : Nonempty Full

def Std.Http.Body.Full.ofByteArray (data : ByteArray) : Async.Async Full

Creates a Full body from a ByteArray.

Equations

• Std.Http.Body.Full.ofByteArray data = do let state ← liftM (Std.Mutex.new Std.Http.Body.Full.State.ready✝) pure { data := data, state := state }

def Std.Http.Body.Full.ofString (data : String) : Async.Async Full

Creates a Full body from a String.

Equations

• Std.Http.Body.Full.ofString data = do let state ← liftM (Std.Mutex.new Std.Http.Body.Full.State.ready✝) pure { data := data.toUTF8, state := state }

def Std.Http.Body.Full.recv (full : Full) : Async.Async (Option Chunk)

Receives the body data. Returns the full byte array on the first call as a single chunk, then none on all subsequent calls until the cursor is reset.

Equations

• full.recv = (Std.Http.Body.Full.state✝ full).atomically (Std.Http.Body.Full.takeChunk✝ full)

def Std.Http.Body.Full.close (full : Full) : Async.Async Unit

Closes the body, discarding any unconsumed data.

Equations

• full.close = (Std.Http.Body.Full.state✝ full).atomically (set Std.Http.Body.Full.State.closed✝)

def Std.Http.Body.Full.isClosed (full : Full) : Async.Async Bool

Returns true when the body has been closed or consumed.

Equations

• full.isClosed = (Std.Http.Body.Full.state✝ full).atomically do let __do_lift ← get pure (__do_lift != Std.Http.Body.Full.State.ready✝)

def Std.Http.Body.Full.getKnownSize (full : Full) : Async.Async (Option Length)

Returns the known size of the remaining data. Returns some (.fixed n) with the byte count if not yet consumed, some (.fixed 0) otherwise.

Equations

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

def Std.Http.Body.Full.tryRecv (full : Full) : Async.Async (Option (Option Chunk))

Non-blocking receive. Full bodies are always in-memory, so data is always immediately available. Returns some chunk on first call, some none (EOF) once consumed or closed.

Equations

• full.tryRecv = do let __do_lift ← (Std.Http.Body.Full.state✝ full).atomically (Std.Http.Body.Full.takeChunk✝ full) pure (some __do_lift)

def Std.Http.Body.Full.recvSelector (full : Full) : Async.Selector (Option Chunk)

Selector that immediately resolves to the remaining chunk (or EOF).

Equations

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

def Std.Http.Body.Full.resetInPlace (full : Full) : Async.Async Unit

Resets the cursor to position zero so the body can be re-read from the start. Since Full.data is always preserved in the struct, this always works regardless of whether close was previously called (e.g. by the connection loop after EOF).

Equations

• full.resetInPlace = (Std.Http.Body.Full.state✝ full).atomically (set Std.Http.Body.Full.State.ready✝)

@[instance_reducible]

instance Std.Http.Body.instFull : Body Full

Equations

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

@[instance_reducible]

instance Std.Http.Body.instReplayableFull : Replayable Full

Full is replayable: resetInPlace resets the cursor to zero so the body can be re-read from the start.

Equations

• Std.Http.Body.instReplayableFull = { resetInPlace := Std.Http.Body.Full.resetInPlace }

@[instance_reducible]

instance Std.Http.Body.instCoeFullAny : Coe Full Any

Equations

• Std.Http.Body.instCoeFullAny = { coe := Std.Http.Body.Any.ofReplayableBody }

@[instance_reducible]

instance Std.Http.Body.instCoeResponseFullAny : Coe (Response Full) (Response Any)

Equations

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

@[instance_reducible]

instance Std.Http.Body.instCoeContextAsyncResponseFullAny : Coe (Async.ContextAsync (Response Full)) (Async.ContextAsync (Response Any))

Equations

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

@[instance_reducible]

instance Std.Http.Body.instCoeAsyncResponseFullContextAsyncAny : Coe (Async.Async (Response Full)) (Async.ContextAsync (Response Any))

Equations

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

def Std.Http.Request.Builder.fromBytes (builder : Builder) (content : ByteArray) : Async.Async (Request Body.Full)

Builds a request body from raw bytes without setting any headers. Use bytes instead if you want Content-Type: application/octet-stream set automatically.

Equations

• builder.fromBytes content = do let __do_lift ← Std.Http.Body.Full.ofByteArray content pure (builder.body __do_lift)

def Std.Http.Request.Builder.bytes (builder : Builder) (content : ByteArray) : Async.Async (Request Body.Full)

Builds a request with a binary body. Sets Content-Type: application/octet-stream. Use fromBytes instead if you need to set a different Content-Type or none at all.

Equations

• builder.bytes content = (builder.header Std.Http.Header.Name.contentType (Std.Http.Header.Value.ofString! "application/octet-stream")).fromBytes content

def Std.Http.Request.Builder.text (builder : Builder) (content : String) : Async.Async (Request Body.Full)

Builds a request with a text body. Sets Content-Type: text/plain; charset=utf-8.

Equations

• builder.text content = (builder.header Std.Http.Header.Name.contentType (Std.Http.Header.Value.ofString! "text/plain; charset=utf-8")).fromBytes content.toUTF8

def Std.Http.Request.Builder.json (builder : Builder) (content : String) : Async.Async (Request Body.Full)

Builds a request with a JSON body. Sets Content-Type: application/json.

Equations

• builder.json content = (builder.header Std.Http.Header.Name.contentType (Std.Http.Header.Value.ofString! "application/json")).fromBytes content.toUTF8

def Std.Http.Request.Builder.html (builder : Builder) (content : String) : Async.Async (Request Body.Full)

Builds a request with an HTML body. Sets Content-Type: text/html; charset=utf-8.

Equations

• builder.html content = (builder.header Std.Http.Header.Name.contentType (Std.Http.Header.Value.ofString! "text/html; charset=utf-8")).fromBytes content.toUTF8

def Std.Http.Response.Builder.fromBytes (builder : Builder) (content : ByteArray) : Async.Async (Response Body.Full)

Builds a response body from raw bytes without setting any headers. Use bytes instead if you want Content-Type: application/octet-stream set automatically.

Equations

• builder.fromBytes content = do let __do_lift ← Std.Http.Body.Full.ofByteArray content pure (builder.body __do_lift)

def Std.Http.Response.Builder.bytes (builder : Builder) (content : ByteArray) : Async.Async (Response Body.Full)

Builds a response with a binary body. Sets Content-Type: application/octet-stream. Use fromBytes instead if you need to set a different Content-Type or none at all.

Equations

• builder.bytes content = (builder.header Std.Http.Header.Name.contentType (Std.Http.Header.Value.ofString! "application/octet-stream")).fromBytes content

def Std.Http.Response.Builder.text (builder : Builder) (content : String) : Async.Async (Response Body.Full)

Builds a response with a text body. Sets Content-Type: text/plain; charset=utf-8.

Equations

• builder.text content = (builder.header Std.Http.Header.Name.contentType (Std.Http.Header.Value.ofString! "text/plain; charset=utf-8")).fromBytes content.toUTF8

def Std.Http.Response.Builder.json (builder : Builder) (content : String) : Async.Async (Response Body.Full)

Builds a response with a JSON body. Sets Content-Type: application/json.

Equations

• builder.json content = (builder.header Std.Http.Header.Name.contentType (Std.Http.Header.Value.ofString! "application/json")).fromBytes content.toUTF8

def Std.Http.Response.Builder.html (builder : Builder) (content : String) : Async.Async (Response Body.Full)

Builds a response with an HTML body. Sets Content-Type: text/html; charset=utf-8.

Equations

• builder.html content = (builder.header Std.Http.Header.Name.contentType (Std.Http.Header.Value.ofString! "text/html; charset=utf-8")).fromBytes content.toUTF8