module tutorial.engines.template_behaviour;

import tutorial.engines.template_messages open;
import tutorial.engines.template_config open;
import tutorial.engines.template_environment 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;

syntax alias Val := Nat;

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

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

type TemplateActionArgument :=
  | One FirstArgument
  | Two SecondArgument;

TemplateActionArguments : Type := List TemplateActionArgument;

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

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

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

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

justHiAction (input : TemplateActionInput) : Option TemplateActionEffect :=
  let
    env := ActionInput.env input;
    args := ActionInput.args input;
  in case args of
       | TemplateActionArgument.Two SecondArgument.mk@{data := data} :: _ :=
         some
           ActionEffect.mk@{
             env :=
               env@EngineEnv{localState := TemplateLocalState.mk@{
                                             taskQueue :=
                                               CustomData.mkCustomData@{
                                                 word := data;
                                               };
                                           }};
             msgs := [];
             timers := [];
             engines := [];
           }
       | _ := none;

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 EngineMsg.mk@{
                msg := Anoma.PreMsg.MsgTemplate (TemplateMsg.ExampleRequest req);
                sender := sender;
                target := target;
                mailbox := mailbox;
              } :=
         some
           ActionEffect.mk@{
             env := env;
             msgs :=
               [
                 EngineMsg.mk@{
                   sender := getEngineIDFromEngineCfg cfg;
                   target := sender;
                   mailbox := some 0;
                   msg :=
                     Anoma.PreMsg.MsgTemplate
                       (TemplateMsg.ExampleReply
                         (ok
                           ExampleReplyOk.mkExampleReplyOk@{
                             argOne := ExampleRequest.argOne req;
                           }));
                 };
               ];
             timers := [];
             engines := [];
           }
       | _ := none;

justHiActionLabel : TemplateActionExec := ActionExec.Seq [justHiAction];

exampleReplyActionLabel : TemplateActionExec :=
  ActionExec.Seq [exampleReplyAction];

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

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

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

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

justHiGuard
  (trigger : TemplateTimestampedTrigger)
  (cfg : TemplateCfg)
  (env : TemplateEnv)
  : Option TemplateGuardOutput :=
  let
    emsg := getEngineMsgFromTimestampedTrigger trigger;
  in case emsg of
       | some EngineMsg.mk@{
                msg := Anoma.PreMsg.MsgTemplate TemplateMsg.JustHi;
              } :=
         some
           GuardOutput.mk@{
             action := justHiActionLabel;
             args :=
               [
                 TemplateActionArgument.Two
                   SecondArgument.mk@{
                     data := "Hello World!";
                   };
               ];
           }
       | _ := none;

exampleReplyGuard
  (trigger : TemplateTimestampedTrigger)
  (cfg : TemplateCfg)
  (env : TemplateEnv)
  : Option TemplateGuardOutput :=
  case getEngineMsgFromTimestampedTrigger trigger of
    | some EngineMsg.mk@{
             msg := Anoma.PreMsg.MsgTemplate (TemplateMsg.ExampleRequest req);
             sender := mkPair none _;
           } -- from local engines only (NodeID is none)
    :=
      some
        GuardOutput.mk@{
          action := exampleReplyActionLabel;
          args := [];
        }
    | _ := none;

TemplateBehaviour : Type :=
  EngineBehaviour
    TemplateLocalCfg
    TemplateLocalState
    TemplateMailboxState
    TemplateTimerHandle
    TemplateActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

module template_behaviour_example;
  
  exTemplateBehaviour : TemplateBehaviour :=
    EngineBehaviour.mk@{
      guards := GuardEval.First [justHiGuard; exampleReplyGuard];
    };
end;