module arch.node.engines.wall_clock_behaviour;

import arch.node.engines.wall_clock_messages open;
import arch.node.engines.wall_clock_config open;
import arch.node.engines.wall_clock_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;

type MessageFrom :=
  mkMessageFrom@{
    whoAsked : Option EngineID;
    mailbox : Option MailboxID;
  };

type WallClockActionArgument := | WallClockActionArgumentFrom MessageFrom;

WallClockActionArguments : Type := List WallClockActionArgument;

WallClockAction : Type :=
  Action
    WallClockCfg
    WallClockLocalState
    WallClockMailboxState
    WallClockTimerHandle
    WallClockActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

WallClockActionInput : Type :=
  ActionInput
    WallClockCfg
    WallClockLocalState
    WallClockMailboxState
    WallClockTimerHandle
    WallClockActionArguments
    Anoma.Msg;

WallClockActionEffect : Type :=
  ActionEffect
    WallClockLocalState
    WallClockMailboxState
    WallClockTimerHandle
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

WallClockActionExec : Type :=
  ActionExec
    WallClockCfg
    WallClockLocalState
    WallClockMailboxState
    WallClockTimerHandle
    WallClockActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

getTimeAction (input : WallClockActionInput) : Option WallClockActionEffect :=
  let
    cfg := ActionInput.cfg input;
    env := ActionInput.env input;
    trigger := ActionInput.trigger input;
    currentTime := WallClockLocalState.currentTime (EngineEnv.localState env);
    newTime := advanceTime currentTime;
  in case getEngineMsgFromTimestampedTrigger trigger of
       | some emsg :=
         some
           mkActionEffect@{
             env :=
               env@EngineEnv{localState := mkWallClockLocalState@{
                                             currentTime := newTime;
                                           }};
             msgs :=
               [
                 mkEngineMsg@{
                   sender := getEngineIDFromEngineCfg cfg;
                   target := EngineMsg.sender emsg;
                   mailbox := some 0;
                   msg :=
                     Anoma.MsgWallClock
                       (WallClockGetTimeResult
                         mkTimeResult@{
                           epochTime := newTime;
                         });
                 };
               ];
             timers := [];
             engines := [];
           }
       | _ := none;

getTimeActionLabel : WallClockActionExec := Seq [getTimeAction];

WallClockGuard : Type :=
  Guard
    WallClockCfg
    WallClockLocalState
    WallClockMailboxState
    WallClockTimerHandle
    WallClockActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

WallClockGuardOutput : Type :=
  GuardOutput
    WallClockCfg
    WallClockLocalState
    WallClockMailboxState
    WallClockTimerHandle
    WallClockActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

WallClockGuardEval : Type :=
  GuardEval
    WallClockCfg
    WallClockLocalState
    WallClockMailboxState
    WallClockTimerHandle
    WallClockActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

getTimeGuard
  (trigger : TimestampedTrigger WallClockTimerHandle Anoma.Msg)
  (cfg : EngineCfg WallClockCfg)
  (env : WallClockEnv)
  : Option WallClockGuardOutput :=
  case getEngineMsgFromTimestampedTrigger trigger of
    | some mkEngineMsg@{msg := Anoma.MsgWallClock WallClockGetTime} :=
      some
        mkGuardOutput@{
          action := getTimeActionLabel;
          args := [];
        }
    | _ := none;

WallClockBehaviour : Type :=
  EngineBehaviour
    WallClockCfg
    WallClockLocalState
    WallClockMailboxState
    WallClockTimerHandle
    WallClockActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

wallClockBehaviour : WallClockBehaviour :=
  mkEngineBehaviour@{
    guards := First [getTimeGuard];
  };