Body.Full

A body backed by a fixed ByteArray held in a Mutex.

The byte array is consumed at most once: the first call to recv atomically takes the data and returns it as a single chunk; subsequent calls return none (end-of-stream). Closing the body discards any unconsumed data.

structure Std.Http.Body.Full : Type

A body backed by a fixed, mutex-protected ByteArray.

The data is consumed on the first read. Once consumed (or explicitly closed), the body behaves as a closed, empty channel.

• state : Std.Mutex (Option ByteArray)

instance Std.Http.Body.instNonemptyFull : Nonempty Full

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

Creates a Full body from a ByteArray.

Equations

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

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

Creates a Full body from a String.

Equations

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

def Std.Http.Body.Full.recv (full : Full) : Internal.IO.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.

Equations

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

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

Closes the body, discarding any unconsumed data.

Equations

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

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

Returns true when the data has been consumed or the body has been closed.

Equations

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

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

Returns the known size of the remaining data. Returns some (.fixed n) with the current byte count, or some (.fixed 0) if the body has already been consumed or closed.

Equations

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

def Std.Http.Body.Full.recvSelector (full : Full) : Internal.IO.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.

@[implicit_reducible]

instance Std.Http.Body.instFull : Body Full

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

• Std.Http.Body.instCoeResponseFullAny = { coe := fun (f : Std.Http.Response Std.Http.Body.Full) => { line := f.line, body := Std.Http.Body.Any.ofBody f.body, extensions := f.extensions } }

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance Std.Http.Body.instCoeAsyncResponseFullContextAsyncAny : Coe (Internal.IO.Async.Async (Response Full)) (Internal.IO.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) : Internal.IO.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) : Internal.IO.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) : Internal.IO.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) : Internal.IO.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) : Internal.IO.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) : Internal.IO.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) : Internal.IO.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) : Internal.IO.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) : Internal.IO.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) : Internal.IO.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