Juvix imports

module arch.node.engines.template_behaviour;

import arch.node.engines.template_messages open;
import arch.node.engines.template_config open;
import arch.node.engines.template_environment open;
import prelude open;
import arch.node.types.basics open;
import arch.node.types.identities open;
import arch.node.types.messages open;
import arch.node.types.engine open;
import arch.node.types.anoma as Anoma open;

Template Behaviour¶

Overview¶

A template engine acts in the ways described on this page. The action labels correspond to the actions that can be performed by the engine. Using the action labels, we describe the effects of the actions.

Action arguments¶

The action arguments are set by a guard and passed to the action function as part of the GuardOutput.

Auxiliary Juvix code

syntax alias Val := Nat;

`TemplateActionArgumentOne FirstArgument`¶

type FirstArgument := mkFirstArgument@{data : Val};

Arguments

data:: is the value of the action argument.

`TemplateActionArgumentTwo SecondArgument`¶

type SecondArgument := mkSecondArgument@{data : String};

Arguments

data:: is the value of the action argument.

`TemplateActionArgument`¶

type TemplateActionArgument :=
  | TemplateActionArgumentOne FirstArgument
  | TemplateActionArgumentTwo SecondArgument;

`TemplateActionArguments`¶

TemplateActionArguments : Type := List TemplateActionArgument;

Actions¶

Auxiliary Juvix code

`TemplateAction`¶

TemplateAction : Type :=
  Action
    TemplateLocalCfg
    TemplateLocalState
    TemplateMailboxState
    TemplateTimerHandle
    TemplateActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

`TemplateActionInput`¶

TemplateActionInput : Type :=
  ActionInput
    TemplateLocalCfg
    TemplateLocalState
    TemplateMailboxState
    TemplateTimerHandle
    TemplateActionArguments
    Anoma.Msg;

`TemplateActionEffect`¶

TemplateActionEffect : Type :=
  ActionEffect
    TemplateLocalState
    TemplateMailboxState
    TemplateTimerHandle
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

`TemplateActionExec`¶

TemplateActionExec : Type :=
  ActionExec
    TemplateLocalCfg
    TemplateLocalState
    TemplateMailboxState
    TemplateTimerHandle
    TemplateActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

`justHiAction`¶

Action description.

State update: Update state with the data set by justHiGuard.
Messages to be sent: No messages are added to the send queue.
Engines to be spawned: No engine is created by this action.
Timer updates: No timers are set or cancelled.
Acquaintance updates: None.

justHiAction (input : TemplateActionInput) : Option TemplateActionEffect :=
  let
    env := ActionInput.env input;
    args := ActionInput.args input;
  in case args of
       | TemplateActionArgumentTwo mkSecondArgument@{data := data} :: _ :=
         some
           mkActionEffect@{
             env :=
               env@EngineEnv{localState := mkTemplateLocalState@{
                                             taskQueue :=
                                               mkCustomData@{
                                                 word := data;
                                               };
                                           }};
             msgs := [];
             timers := [];
             engines := [];
           }
       | _ := none;

`exampleReplyAction`¶

Respond with a TemplateMsgExampleResponse.

State update: The state remains unchanged.
Messages to be sent: A TemplateMsgExampleReply message with the data set by exampleReplyGuard.
Engines to be spawned: No engine is created by this action.
Timer updates: No timers are set or cancelled.

exampleReplyAction
  (input : TemplateActionInput) : Option TemplateActionEffect :=
  let
    cfg := ActionInput.cfg input;
    env := ActionInput.env input;
    trigger := ActionInput.trigger input;
    args := ActionInput.args input;
  in case getEngineMsgFromTimestampedTrigger trigger of
       | some mkEngineMsg@{
                msg := Anoma.MsgTemplate (TemplateMsgExampleRequest req);
                sender := sender;
                target := target;
                mailbox := mailbox;
              } :=
         some
           mkActionEffect@{
             env := env;
             msgs :=
               [
                 mkEngineMsg@{
                   sender := getEngineIDFromEngineCfg cfg;
                   target := sender;
                   mailbox := some 0;
                   msg :=
                     Anoma.MsgTemplate
                       (TemplateMsgExampleReply
                         (ok
                           mkExampleReplyOk@{
                             argOne := ExampleRequest.argOne req;
                           }));
                 };
               ];
             timers := [];
             engines := [];
           }
       | _ := none;

Action Labels¶

`justHiActionLabel`¶

justHiActionLabel : TemplateActionExec := Seq [justHiAction];

`exampleReplyActionLabel`¶

exampleReplyActionLabel : TemplateActionExec := Seq [exampleReplyAction];

`doBothActionLabel`¶

doBothActionLabel : TemplateActionExec := Seq [justHiAction; exampleReplyAction];

Guards¶

Auxiliary Juvix code

`TemplateGuard`¶

TemplateGuard : Type :=
  Guard
    TemplateLocalCfg
    TemplateLocalState
    TemplateMailboxState
    TemplateTimerHandle
    TemplateActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

`TemplateGuardOutput`¶

TemplateGuardOutput : Type :=
  GuardOutput
    TemplateLocalCfg
    TemplateLocalState
    TemplateMailboxState
    TemplateTimerHandle
    TemplateActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

`TemplateGuardEval`¶

TemplateGuardEval : Type :=
  GuardEval
    TemplateLocalCfg
    TemplateLocalState
    TemplateMailboxState
    TemplateTimerHandle
    TemplateActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

`justHiGuard`¶

Guard description (optional).

Condition: Message type is TemplateMsgJustHi.

justHiGuard
  (trigger : TemplateTimestampedTrigger)
  (cfg : TemplateCfg)
  (env : TemplateEnv)
  : Option TemplateGuardOutput :=
  let
    emsg := getEngineMsgFromTimestampedTrigger trigger;
  in case emsg of
       | some mkEngineMsg@{msg := Anoma.MsgTemplate TemplateMsgJustHi} :=
         some
           mkGuardOutput@{
             action := justHiActionLabel;
             args :=
               [
                 TemplateActionArgumentTwo
                   mkSecondArgument@{
                     data := "Hello World!";
                   };
               ];
           }
       | _ := none;

`exampleReplyGuard`¶

Guard description (optional).

Condition: Message type is TemplateMsgExampleRequest.

exampleReplyGuard
  (trigger : TemplateTimestampedTrigger)
  (cfg : TemplateCfg)
  (env : TemplateEnv)
  : Option TemplateGuardOutput :=
  case getEngineMsgFromTimestampedTrigger trigger of
    | some mkEngineMsg@{
             msg := Anoma.MsgTemplate (TemplateMsgExampleRequest req);
             sender := mkPair none _;
           } :=
      some
        mkGuardOutput@{
          action := exampleReplyActionLabel;
          args := [];
        }
    | _ := none;

The Template behaviour¶