module arch.node.engines.commitment_behaviour;

import prelude open;
import arch.system.identity.identity open;
import arch.node.engines.commitment_messages open;
import arch.node.engines.commitment_config open;
import arch.node.engines.commitment_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;

type ReplyTo :=
  mkReplyTo@{
    whoAsked : Option EngineID;
    mailbox : Option MailboxID;
  };

type CommitmentActionArgument := | CommitmentActionArgumentReplyTo ReplyTo;

CommitmentActionArguments : Type := List CommitmentActionArgument;

CommitmentAction : Type :=
  Action
    CommitmentLocalCfg
    CommitmentLocalState
    CommitmentMailboxState
    CommitmentTimerHandle
    CommitmentActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

CommitmentActionInput : Type :=
  ActionInput
    CommitmentLocalCfg
    CommitmentLocalState
    CommitmentMailboxState
    CommitmentTimerHandle
    CommitmentActionArguments
    Anoma.Msg;

CommitmentActionEffect : Type :=
  ActionEffect
    CommitmentLocalState
    CommitmentMailboxState
    CommitmentTimerHandle
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

CommitmentActionExec : Type :=
  ActionExec
    CommitmentLocalCfg
    CommitmentLocalState
    CommitmentMailboxState
    CommitmentTimerHandle
    CommitmentActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

commitAction (input : CommitmentActionInput) : Option CommitmentActionEffect :=
  let
    env := ActionInput.env input;
    cfg := ActionInput.cfg input;
    tt := ActionInput.trigger input;
  in case getEngineMsgFromTimestampedTrigger tt of
       | some emsg :=
         case emsg of {
           | EngineMsg.mk@{
               msg := Anoma.Msg.Commitment (CommitmentMsg.Request request);
             } :=
             let
               signedData :=
                 Signer.sign
                   (CommitmentLocalCfg.signer (EngineCfg.cfg cfg))
                   (CommitmentLocalCfg.backend (EngineCfg.cfg cfg))
                   (RequestCommitment.data request);
               responseMsg :=
                 ReplyCommitment.mkReplyCommitment@{
                   commitment := signedData;
                   err := none;
                 };
             in some
               ActionEffect.mk@{
                 env := env;
                 msgs :=
                   [
                     EngineMsg.mk@{
                       sender := getEngineIDFromEngineCfg cfg;
                       target := EngineMsg.sender emsg;
                       mailbox := some 0;
                       msg :=
                         Anoma.Msg.Commitment (CommitmentMsg.Reply responseMsg);
                     };
                   ];
                 timers := [];
                 engines := [];
               }
           | _ := none
         }
       | _ := none;

commitActionLabel : CommitmentActionExec := ActionExec.Seq [commitAction];

CommitmentGuard : Type :=
  Guard
    CommitmentLocalCfg
    CommitmentLocalState
    CommitmentMailboxState
    CommitmentTimerHandle
    CommitmentActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

CommitmentGuardOutput : Type :=
  GuardOutput
    CommitmentLocalCfg
    CommitmentLocalState
    CommitmentMailboxState
    CommitmentTimerHandle
    CommitmentActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

CommitmentGuardEval : Type :=
  GuardEval
    CommitmentLocalCfg
    CommitmentLocalState
    CommitmentMailboxState
    CommitmentTimerHandle
    CommitmentActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

commitGuard
  (tt : TimestampedTrigger CommitmentTimerHandle Anoma.Msg)
  (cfg : CommitmentCfg)
  (env : CommitmentEnv)
  : Option CommitmentGuardOutput :=
  case getEngineMsgFromTimestampedTrigger tt of
    | some EngineMsg.mk@{
             msg := Anoma.Msg.Commitment (CommitmentMsg.Request _);
           } :=
      some
        GuardOutput.mk@{
          action := commitActionLabel;
          args := [];
        }
    | _ := none;

CommitmentBehaviour : Type :=
  EngineBehaviour
    CommitmentLocalCfg
    CommitmentLocalState
    CommitmentMailboxState
    CommitmentTimerHandle
    CommitmentActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

commitmentBehaviour : CommitmentBehaviour :=
  EngineBehaviour.mk@{
    guards := GuardEval.First [commitGuard];
  };