Juvix imports

module arch.node.engines.template_environment;

import prelude open;
import arch.node.engines.template_messages open;
import arch.node.types.engine_environment open;

Template Environment¶

Overview¶

Lorem ipsum dolor sit amet, consectetur adipiscing elit.

Mailbox state types¶

Auxiliary Juvix code

syntax alias MailboxOneOne := Nat;

syntax alias MailboxTwoOne := String;

syntax alias MailboxTwoTwo := Bool;

TemplateMailboxState constructors¶

TemplateMailboxStateFirstKind FirstKindMailboxState

type FirstKindMailboxState := mkFirstKindMailboxState {fieldOne : MailboxOneOne};

This is one family of mailbox states without much complexity.

fieldOne: Lorem ipsum dolor sit amet, consectetur adipiscing elit.

TemplateMailboxStateSecondKind SecondKindMailboxState

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

Lorem ipsum dolor sit amet, consectetur adipiscing elit.

fieldOne: Lorem ipsum dolor sit amet, consectetur adipiscing elit.
fieldTwo: Lorem ipsum dolor sit amet, consectetur adipiscing elit.

TemplateMailboxState¶

type TemplateMailboxState :=
  | TemplateMailboxStateFirstKind FirstKindMailboxState
  | TemplateMailboxStateSecondKind SecondKindMailboxState;

Local state¶

Auxiliary Juvix code

Lorem ipsum dolor sit amet, consectetur adipiscing elit.

type CustomData := mkCustomData {word : String};

word: Lorem ipsum dolor sit amet, consectetur adipiscing elit.

TemplateLocalState¶

type TemplateLocalState := mkTemplateLocalState {taskQueue : CustomData};

Timer handles¶

Auxiliary Juvix code

syntax alias ArgOne := Nat;

TemplateTimerHandle constructors¶

FirstOptionTimerHandle

type FirstOptionTimerHandle := mkFirstOptionTimerHandle {argOne : ArgOne};

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

argOne: Lorem ipsum dolor sit amet, consectetur adipiscing elit.

SecondOptionTimerHandle

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

argOne: Lorem ipsum dolor sit amet, consectetur adipiscing elit.
argTwo: Lorem ipsum dolor sit amet, consectetur adipiscing elit.

TemplateTimerHandle¶

type TemplateTimerHandle :=
  | TemplateTimerHandleFirstOption FirstOptionTimerHandle
  | TemplateTimerHandleSecondOption SecondOptionTimerHandle;

The Template Environment¶

TemplateEnvironment¶

TemplateEnvironment : Type :=
  EngineEnvironment TemplateLocalState TemplateMailboxState TemplateTimerHandle;

Instantiation¶

templateEnvironment : TemplateEnvironment :=
  mkEngineEnvironment@{
    name := "template";
    localState :=
      mkTemplateLocalState@{
        taskQueue :=
          mkCustomData@{
            word := "taskQueue"
          }
      };
    mailboxCluster := Map.empty;
    acquaintances := Set.empty;
    timers := []
  };