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;

syntax alias MailboxOneOne := Nat;
syntax alias MailboxTwoOne := String;
syntax alias MailboxTwoTwo := Bool;

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

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

type TemplateMailboxState :=
  | TemplateMailboxStateFirstKind FirstKindMailboxState
  | TemplateMailboxStateSecondKind SecondKindMailboxState;

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

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

syntax alias ArgOne := Nat;

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

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

type TemplateTimerHandle :=
  | TemplateTimerHandleFirstOption FirstOptionTimerHandle
  | TemplateTimerHandleSecondOption SecondOptionTimerHandle;

TemplateTimestampedTrigger : Type :=
  TimestampedTrigger TemplateTimerHandle Anoma.Msg;

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

module template_environment_example;
  
  exTemplateEnv : TemplateEnv :=
    mkEngineEnv@{
      localState :=
        mkTemplateLocalState@{
          taskQueue :=
            mkCustomData@{
              word := "taskQueue";
            };
        };
      mailboxCluster := Map.empty;
      acquaintances := Set.empty;
      timers := [];
    };
end;