module tutorial.engines.template_environment;

import tutorial.engines.template_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;

Template Environment¶

Overview¶

The Engine environment of the engine.

Mailbox state¶

syntax alias MailboxOneOne := Nat;

syntax alias MailboxTwoOne := String;

syntax alias MailboxTwoTwo := Bool;

TemplateMailboxStateFirstKind FirstKindMailboxState¶

type FirstKindMailboxState :=
  mkFirstKindMailboxState@{
    fieldOne : MailboxOneOne;
  };

This is one family of mailbox states without much complexity.

TemplateMailboxStateSecondKind SecondKindMailboxState¶

type SecondKindMailboxState :=
  mkSecondKindMailboxState@{
    fieldOne : MailboxTwoOne;
    fieldTwo : MailboxTwoTwo;
  };

Lorem ipsum dolor sit amet, consectetur adipiscing elit.

TemplateMailboxState¶

type TemplateMailboxState :=
  | TemplateMailboxStateFirstKind FirstKindMailboxState
  | TemplateMailboxStateSecondKind SecondKindMailboxState;

Local state¶

type CustomData :=
  mkCustomData@{
    word : String;
  };

TemplateLocalState¶

type TemplateLocalState :=
  mk@{
    taskQueue : CustomData;
  };

Timer handles¶

syntax alias ArgOne := Nat;

TemplateTimerHandleFirstOption FirstOptionTimerHandle¶

type FirstOptionTimerHandle :=
  mkFirstOptionTimerHandle@{
    argOne : ArgOne;
  };

Lorem ipsum dolor sit amet, consectetur adipiscing elit. The following code is an example of this case.

TemplateTimerHandleSecondOption SecondOptionTimerHandle¶

type SecondOptionTimerHandle :=
  mkSecondOptionTimerHandle@{
    argOne : String;
    argTwo : Bool;
  };

TemplateTimerHandle¶

type TemplateTimerHandle :=
  | TemplateTimerHandleFirstOption FirstOptionTimerHandle
  | TemplateTimerHandleSecondOption SecondOptionTimerHandle;

TemplateTimestampedTrigger¶

TemplateTimestampedTrigger : Type :=
  TimestampedTrigger TemplateTimerHandle Anoma.Msg;

Engine Environment¶

TemplateEnv¶

TemplateEnv : Type :=
  EngineEnv
    TemplateLocalState
    TemplateMailboxState
    TemplateTimerHandle
    Anoma.Msg;

Instantiation¶

exTemplateEnv : TemplateEnv :=
  EngineEnv.mk@{
    localState :=
      TemplateLocalState.mk@{
        taskQueue :=
          CustomData.mkCustomData@{
            word := "taskQueue";
          };
      };
    mailboxCluster := Map.empty;
    acquaintances := Set.empty;
    timers := [];
  };