module arch.node.engines.logging_environment;

import prelude open;
import arch.node.engines.logging_messages 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;

Logging Environment¶

Overview¶

The logging environment maintains the state necessary for recording logs locally on the physical machine.

Mailbox state types¶

LoggingMailboxState¶

syntax alias LoggingMailboxState := Unit;

The logging engine does not require complex mailbox states.

Local state¶

LoggingLocalState¶

type LoggingLocalState :=
  mkLoggingLocalState@{
    logbook : List String;
  };

Timer handles¶

LoggingTimerHandle¶

syntax alias LoggingTimerHandle := Unit;

LoggingTimestampedTrigger¶

LoggingTimestampedTrigger : Type :=
  TimestampedTrigger LoggingTimerHandle Anoma.Msg;

The Logging Environment¶

LoggingEnv¶

LoggingEnv : Type :=
  EngineEnv LoggingLocalState LoggingMailboxState LoggingTimerHandle Anoma.Msg;

Instantiation¶

loggingEnv : LoggingEnv :=
  mkEngineEnv@{
    localState :=
      mkLoggingLocalState@{
        logbook := [];
      };
    mailboxCluster := Map.empty;
    acquaintances := Set.empty;
    timers := [];
  };