module tutorial.engines.template_minimum_behaviour;

import tutorial.engines.template_minimum_messages open;
import tutorial.engines.template_minimum_config open;
import tutorial.engines.template_minimum_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;

TemplateMinimumActionArguments : Type := Unit;

TemplateMinimumAction : Type :=
  Action
    TemplateMinimumLocalCfg
    TemplateMinimumLocalState
    TemplateMinimumMailboxState
    TemplateMinimumTimerHandle
    TemplateMinimumActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

TemplateMinimumActionInput : Type :=
  ActionInput
    TemplateMinimumLocalCfg
    TemplateMinimumLocalState
    TemplateMinimumMailboxState
    TemplateMinimumTimerHandle
    TemplateMinimumActionArguments
    Anoma.Msg;

TemplateMinimumActionEffect : Type :=
  ActionEffect
    TemplateMinimumLocalState
    TemplateMinimumMailboxState
    TemplateMinimumTimerHandle
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

TemplateMinimumActionExec : Type :=
  ActionExec
    TemplateMinimumLocalCfg
    TemplateMinimumLocalState
    TemplateMinimumMailboxState
    TemplateMinimumTimerHandle
    TemplateMinimumActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

exampleReplyAction
  (input : TemplateMinimumActionInput) : Option TemplateMinimumActionEffect :=
  TODO;

{-
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.MsgTemplateMinimum (TemplateMinimumMsgExampleRequest 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.MsgTemplateMinimum
(TemplateMinimumMsgExampleReply
(ok mkExampleReplyOk@{
argOne := ExampleRequest.argOne req;
}));
}
];
timers := [];
engines := [];
}
| _ := none
-}
exampleReplyActionLabel : TemplateMinimumActionExec :=
  ActionExec.Seq [exampleReplyAction];

TemplateMinimumGuard : Type :=
  Guard
    TemplateMinimumLocalCfg
    TemplateMinimumLocalState
    TemplateMinimumMailboxState
    TemplateMinimumTimerHandle
    TemplateMinimumActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

TemplateMinimumGuardOutput : Type :=
  GuardOutput
    TemplateMinimumLocalCfg
    TemplateMinimumLocalState
    TemplateMinimumMailboxState
    TemplateMinimumTimerHandle
    TemplateMinimumActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

TemplateMinimumGuardEval : Type :=
  GuardEval
    TemplateMinimumLocalCfg
    TemplateMinimumLocalState
    TemplateMinimumMailboxState
    TemplateMinimumTimerHandle
    TemplateMinimumActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

exampleReplyGuard
  (trigger : TemplateMinimumTimestampedTrigger)
  (cfg : TemplateMinimumCfg)
  (env : TemplateMinimumEnv)
  : Option TemplateMinimumGuardOutput :=
  case getEngineMsgFromTimestampedTrigger trigger of
    | some EngineMsg.mk@{
             msg := Anoma.PreMsg.MsgTemplateMinimum (TemplateMinimumMsg.ExampleRequest req);
             sender := mkPair none _;
           } -- from local engines only (NodeID is none)
    :=
      some
        GuardOutput.mk@{
          action := exampleReplyActionLabel;
          args := unit;
        }
    | _ := none;

TemplateMinimumBehaviour : Type :=
  EngineBehaviour
    TemplateMinimumLocalCfg
    TemplateMinimumLocalState
    TemplateMinimumMailboxState
    TemplateMinimumTimerHandle
    TemplateMinimumActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

module template_minimum_behaviour_example;
  
  exTemplateMinimumBehaviour : TemplateMinimumBehaviour :=
    EngineBehaviour.mk@{
      guards := GuardEval.First [exampleReplyGuard];
    };
end;