module arch.node.engines.logging_behaviour;

import arch.node.engines.logging_messages open;
import arch.node.engines.logging_config open;
import arch.node.engines.logging_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 LoggingActionArgument := Unit;

LoggingActionArguments : Type := List LoggingActionArgument;

LoggingAction : Type :=
  Action
    LoggingCfg
    LoggingLocalState
    LoggingMailboxState
    LoggingTimerHandle
    LoggingActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

LoggingActionInput : Type :=
  ActionInput
    LoggingCfg
    LoggingLocalState
    LoggingMailboxState
    LoggingTimerHandle
    LoggingActionArguments
    Anoma.Msg;

LoggingActionEffect : Type :=
  ActionEffect
    LoggingLocalState
    LoggingMailboxState
    LoggingTimerHandle
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

LoggingActionExec : Type :=
  ActionExec
    LoggingCfg
    LoggingLocalState
    LoggingMailboxState
    LoggingTimerHandle
    LoggingActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

appendLogAction (input : LoggingActionInput) : Option LoggingActionEffect :=
  let
    env := ActionInput.env input;
    trigger := ActionInput.trigger input;
  in case getEngineMsgFromTimestampedTrigger trigger of
       | some EngineMsg.mk@{
                msg := Anoma.PreMsg.MsgLogging (LoggingMsg.Append AppendValue.mk@{
                                                                    value := value;
                                                                  });
              } :=
         let
           currentLogbook :=
             LoggingLocalState.logbook (EngineEnv.localState env);
           newLogbook := value :: currentLogbook;
         in some
           ActionEffect.mk@{
             env :=
               env@EngineEnv{localState := LoggingLocalState.mk@{
                                             logbook := newLogbook;
                                           }};
             msgs := [];
             timers := [];
             engines := [];
           }
       | _ := none;

appendLogActionLabel : LoggingActionExec := ActionExec.Seq [appendLogAction];

LoggingGuard : Type :=
  Guard
    LoggingCfg
    LoggingLocalState
    LoggingMailboxState
    LoggingTimerHandle
    LoggingActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

LoggingGuardOutput : Type :=
  GuardOutput
    LoggingCfg
    LoggingLocalState
    LoggingMailboxState
    LoggingTimerHandle
    LoggingActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

LoggingGuardEval : Type :=
  GuardEval
    LoggingCfg
    LoggingLocalState
    LoggingMailboxState
    LoggingTimerHandle
    LoggingActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

appendLogGuard
  (trigger : LoggingTimestampedTrigger)
  (cfg : EngineCfg LoggingCfg)
  (env : LoggingEnv)
  : Option LoggingGuardOutput :=
  case getEngineMsgFromTimestampedTrigger trigger of
    | some EngineMsg.mk@{
             msg := Anoma.PreMsg.MsgLogging (LoggingMsg.Append _);
           } :=
      some
        GuardOutput.mk@{
          action := appendLogActionLabel;
          args := [];
        }
    | _ := none;

LoggingBehaviour : Type :=
  EngineBehaviour
    LoggingCfg
    LoggingLocalState
    LoggingMailboxState
    LoggingTimerHandle
    LoggingActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

loggingBehaviour : LoggingBehaviour :=
  EngineBehaviour.mk@{
    guards := GuardEval.First [appendLogGuard];
  };