module arch.node.net.router_messages;

import arch.node.net.router_types open;
import arch.node.net.transport_types open;
import arch.node.net.node_proxy_messages open;
import arch.node.net.pub_sub_topic_messages open;
import arch.node.types.basics open;
import arch.node.types.identities open;
import arch.node.types.messages open;

Router Messages¶

Message interface¶

RouterMsgNodeSend¶

Send a message to a Node Proxy. If it does not exist yet, the Router spawns a new instance beforehand.

type NodeOutMsg M :=
  mkNodeOutMsg@{
    prefs : TransportPrefs;
    expiry : Time;
    msg : EngineMsg M;
  };

RouterMsgTopicForward¶

Forward a TopicMsg to the corresponding Pub/Sub Topic. If the topic does not exist, the message is dropped. This happens when there are no subscribers.

RouterMsgNodeConnectRequest¶

Request to establish a connection to a remote node.

The Router spawns a new Node Proxy if it does not exist yet, and sets the connection permanence of the Node Proxy via MsgNodeProxySetPermanence.

type NodeConnectRequest :=
  mkNodeConnectRequest@{
    node_id : NodeID;
    permanent : Bool;
  };

NodeConnectReply¶

Reply to a NodeConnectRequest.

NodeConnectReplyOk¶

Example OK reply.

type NodeConnectReplyOk : Type :=
  mkExampleReplyOk@{
    argOne : Nat;
  };

NodeConnectReplyError¶

Example error reply.

type NodeConnectReplyError : Type :=
  | NodeConnectReplyErrorUnknown
  | NodeConnectReplyErrorDenied;

NodeConnectReply¶

NodeConnectReply : Type := Result NodeConnectReplyError NodeConnectReplyOk;

RouterMsgTopicSub TopicSub¶

Allow local engines to subscribe to a Pub/Sub Topic if a TopicAdvert is known for the topic.

The Router forwards the TopicSub message to the Pub/Sub Topic engine instance responsible for the topic. If necessary, it spawns a new Pub/Sub Topic engine instance beforehand.

type RouterSub :=
  mkRouterSub@{
    topic_id : TopicID;
  };

topic_id

Topic ID.

RouterMsgTopicUnsub TopicUnsub¶

Allow local engines to unsubscribe from a Pub/Sub Topic if the topic exists.

The Router forwards the TopicUnsub message to the Pub/Sub Topic.

type RouterTopicUnsub :=
  mkRouterTopicsub@{
    topic_id : TopicID;
  };

topic_id

Topic ID.

RouterMsgNodeAdvert NodeAdvert¶

Node advertisement update.

RouterMsgTopicAdvert TopicAdvert¶

Topic advertisement update.

RouterMsg¶

All Router engine messages.

type RouterMsg M :=
  | RouterMsgNodeSend (NodeOutMsg M)
  | RouterMsgTopicForward TopicMsg
  | RouterMsgNodeConnectRequest NodeConnectRequest
  | RouterMsgNodeAdvert NodeAdvert
  | RouterMsgTopicAdvert TopicAdvert;