module arch.node.engines.net_registry_environment;

import arch.node.engines.net_registry_messages open;
import arch.node.types.basics open;
import arch.node.types.engine open;
import arch.node.types.messages open;
import arch.node.types.identities open;
import arch.node.types.anoma_message as Anoma open;

Network Registry Environment¶

Overview¶

The Engine environment of the engine.

Mailbox state¶

NetworkRegistryMailboxState¶

NetworkRegistryMailboxState : Type := Unit;

Local state¶

NetworkRegistryLocalState¶

type NetworkRegistryLocalState := mkNetworkRegistryLocalState;

Timer handles¶

NetworkRegistryTimerHandle¶

NetworkRegistryTimerHandle : Type := Unit;

NetworkRegistryTimestampedTrigger¶

NetworkRegistryTimestampedTrigger : Type :=
  TimestampedTrigger NetworkRegistryTimerHandle Anoma.Msg;

Engine Environment¶

NetworkRegistryEnv¶

NetworkRegistryEnv : Type :=
  EngineEnv
    NetworkRegistryLocalState
    NetworkRegistryMailboxState
    NetworkRegistryTimerHandle
    Anoma.Msg;

Instantiation¶

exNetworkRegistryEnv : NetworkRegistryEnv :=
  mkEngineEnv@{
    localState := mkNetworkRegistryLocalState;
    mailboxCluster := Map.empty;
    acquaintances := Set.empty;
    timers := [];
  };