Skip to main content

send

In a local protocol, a message leaving the component the statement is written in. The statement names what is sent and where it goes.

component Radar;
component CommandPost;

message struct TrackReport {
    track_id: uint32;
    bearing_deg: float32;
}

local protocol Sweep in Radar {
    send any TrackReport to CommandPost;
}

Payloads​

The payload takes one of the following forms, followed by the connection clause and a semicolon.

  • An expression sends that value.
  • any T sends some value of T, without saying which.
  • any name: T where pred sends some value of T that satisfies pred.
  • let pattern: T binds what is sent, so later statements can refer to it. It also takes a where.

The message type is message data: a non-abstract message struct, or a message variant. In the expression form, the expression's type is what has to be message data.

component Radar;
component CommandPost;

message struct TrackReport {
    track_id: uint32;
    bearing_deg: float32;
}

message struct Ack {
    track_id: uint32;
}

local protocol Sweep in Radar {
    send TrackReport { track_id = 7; bearing_deg = 91.5; } to CommandPost;
    send any TrackReport to CommandPost;
    send any report: TrackReport where report.bearing_deg >= 0.0 to CommandPost;
    send let sent: TrackReport to CommandPost;
    recv any ack: Ack assuming ack.track_id == sent.track_id from CommandPost;
}

Predicates​

A where predicate is what the sender guarantees about the value it puts on the wire, and its type is bit.

  • The predicate is a promise, not a filter. any report: TrackReport where pred may produce any value of the type satisfying pred, so whatever consumes it has to be correct for all of them and not for one convenient witness.
  • The name bound before the colon is in scope in the predicate, and nowhere else.
  • The predicate is the counterpart of the receiver's assuming: the pair is what makes an exchange compatible or not.
  • Neither type checking nor evaluation is affected by a predicate.

Errors​

Sending a type that has no wire form​

Only a message struct or a message variant crosses a connection.

component Radar;
component CommandPost;

struct TrackReport {
    track_id: uint32;
}

local protocol Sweep in Radar {
    send any TrackReport to CommandPost;   // error: message-data-type
}

A where predicate that is not bit​

component Radar;
component CommandPost;

message struct TrackReport {
    track_id: uint32;
}

local protocol Sweep in Radar {
    send any report: TrackReport where report.track_id to CommandPost;   // error: send-predicate-type
}
  • recv — the matching statement at the other end.
  • exch — both halves written as one global statement.
  • connection — the from/to/on clause every message statement carries.
  • struct — the message modifier that gives a type a wire form.