module arch.node.engines.router_behaviour;

import arch.node.engines.router_messages open;
import arch.node.engines.router_config open;
import arch.node.engines.router_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;

RouterActionArguments : Type := Unit;

RouterAction : Type :=
  Action
    RouterLocalCfg
    RouterLocalState
    RouterMailboxState
    RouterTimerHandle
    RouterActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

RouterActionInput : Type :=
  ActionInput
    RouterLocalCfg
    RouterLocalState
    RouterMailboxState
    RouterTimerHandle
    RouterActionArguments
    Anoma.Msg;

RouterActionEffect : Type :=
  ActionEffect
    RouterLocalState
    RouterMailboxState
    RouterTimerHandle
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

RouterActionExec : Type :=
  ActionExec
    RouterLocalCfg
    RouterLocalState
    RouterMailboxState
    RouterTimerHandle
    RouterActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

exampleReplyAction (input : RouterActionInput) : Option RouterActionEffect :=
  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.MsgRouter (RouterMsgExampleRequest 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.MsgRouter
(RouterMsgExampleReply
(ok mkExampleReplyOk@{
argOne := ExampleRequest.argOne req;
}));
}
];
timers := [];
eng ines := [];
}
| _ := none
-}
exampleReplyActionLabel : RouterActionExec :=
  ActionExec.Seq [exampleReplyAction];

RouterGuard : Type :=
  Guard
    RouterLocalCfg
    RouterLocalState
    RouterMailboxState
    RouterTimerHandle
    RouterActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

RouterGuardOutput : Type :=
  GuardOutput
    RouterLocalCfg
    RouterLocalState
    RouterMailboxState
    RouterTimerHandle
    RouterActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

RouterGuardEval : Type :=
  GuardEval
    RouterLocalCfg
    RouterLocalState
    RouterMailboxState
    RouterTimerHandle
    RouterActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

exampleReplyGuard
  (trigger : RouterTimestampedTrigger)
  (cfg : RouterCfg)
  (env : RouterEnv)
  : Option RouterGuardOutput := TODO;

{-
case getEngineMsgFromTimestampedTrigger trigger of {
| some EngineMsg.mk@{
msg := Anoma.PreMsg.MsgRouter (RouterMsgExampleRequest req);
sender := mkPair none _; -- from local engines only (NodeID is none)
} := some GuardOutput.mk@{
action := exampleReplyActionLabel;
args := [];
}
| _ := none
-}
RouterBehaviour : Type :=
  EngineBehaviour
    RouterLocalCfg
    RouterLocalState
    RouterMailboxState
    RouterTimerHandle
    RouterActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

module router_behaviour_example;
  
  exRouterBehaviour : RouterBehaviour :=
    EngineBehaviour.mk@{
      guards := GuardEval.First [exampleReplyGuard];
    };

end;