module arch.node.engines.signs_for_behaviour;

import prelude open;
import Stdlib.Data.Set as Set;
import arch.node.types.messages open;
import arch.node.types.engine open;
import arch.node.types.identities open;
import arch.node.engines.signs_for_environment open;
import arch.node.engines.signs_for_messages open;
import arch.node.engines.signs_for_config open;
import arch.node.types.anoma as Anoma open;

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

type SignsForActionArgument := | SignsForActionArgumentReplyTo ReplyTo;

SignsForActionArguments : Type := List SignsForActionArgument;

SignsForAction : Type :=
  Action
    SignsForCfg
    SignsForLocalState
    SignsForMailboxState
    SignsForTimerHandle
    SignsForActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

SignsForActionInput : Type :=
  ActionInput
    SignsForCfg
    SignsForLocalState
    SignsForMailboxState
    SignsForTimerHandle
    SignsForActionArguments
    Anoma.Msg;

SignsForActionEffect : Type :=
  ActionEffect
    SignsForLocalState
    SignsForMailboxState
    SignsForTimerHandle
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

SignsForActionExec : Type :=
  ActionExec
    SignsForCfg
    SignsForLocalState
    SignsForMailboxState
    SignsForTimerHandle
    SignsForActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

signsForQueryAction
  (input : SignsForActionInput) : Option SignsForActionEffect :=
  let
    env := ActionInput.env input;
    cfg := ActionInput.cfg input;
    tt := ActionInput.trigger input;
    localState := EngineEnv.localState env;
  in case getEngineMsgFromTimestampedTrigger tt of
       | some EngineMsg.mk@{
                msg := Anoma.PreMsg.MsgSignsFor (SignsForMsg.SignsForRequest (RequestSignsFor.mkRequestSignsFor externalIdentityA externalIdentityB));
                sender := msgSender;
              } :=
         let
           hasEvidence :=
             isElement
               \{a b := a && b}
               true
               (map
                 \{evidence :=
                   isEqual
                       (Ord.compare
                         (SignsForEvidence.fromIdentity evidence)
                         externalIdentityA)
                     && isEqual
                       (Ord.compare
                         (SignsForEvidence.toIdentity evidence)
                         externalIdentityB)}
                 (Set.toList (SignsForLocalState.evidenceStore localState)));
           responseMsg :=
             ReplySignsFor.mkReplySignsFor@{
               signsFor := hasEvidence;
               err := none;
             };
         in some
           ActionEffect.mk@{
             env := env;
             msgs :=
               [
                 EngineMsg.mk@{
                   sender := getEngineIDFromEngineCfg cfg;
                   target := msgSender;
                   mailbox := some 0;
                   msg :=
                     Anoma.PreMsg.MsgSignsFor
                       (SignsForMsg.SignsForReply responseMsg);
                 };
               ];
             timers := [];
             engines := [];
           }
       | _ := none;

submitEvidenceAction
  (input : SignsForActionInput) : Option SignsForActionEffect :=
  let
    env := ActionInput.env input;
    cfg := ActionInput.cfg input;
    tt := ActionInput.trigger input;
    localState := EngineEnv.localState env;
  in case getEngineMsgFromTimestampedTrigger tt of
       | some EngineMsg.mk@{
                msg := Anoma.PreMsg.MsgSignsFor (SignsForMsg.SubmitSignsForEvidenceRequest (RequestSubmitSignsForEvidence.mkRequestSubmitSignsForEvidence evidence));
                sender := msgSender;
              } :=
         case verifyEvidence evidence of {
           | true :=
             let
               alreadyExists :=
                 isElement
                   \{a b := a && b}
                   true
                   (map
                     \{e := isEqual (Ord.compare e evidence)}
                     (Set.toList
                       (SignsForLocalState.evidenceStore localState)));
             in case alreadyExists of {
                  | true :=
                    let
                      responseMsg :=
                        ReplySubmitSignsForEvidence.mkReplySubmitSignsForEvidence@{
                          err := some "Evidence already exists.";
                        };
                    in some
                      ActionEffect.mk@{
                        env := env;
                        msgs :=
                          [
                            EngineMsg.mk@{
                              sender := getEngineIDFromEngineCfg cfg;
                              target := msgSender;
                              mailbox := some 0;
                              msg :=
                                Anoma.PreMsg.MsgSignsFor
                                  (SignsForMsg.SubmitSignsForEvidenceReply
                                    responseMsg);
                            };
                          ];
                        timers := [];
                        engines := [];
                      }
                  | false :=
                    let
                      newEvidenceStore :=
                        Set.insert
                          evidence
                          (SignsForLocalState.evidenceStore localState);
                      updatedLocalState :=
                        localState@SignsForLocalState{evidenceStore := newEvidenceStore};
                      newEnv := env@EngineEnv{localState := updatedLocalState};
                      responseMsg :=
                        ReplySubmitSignsForEvidence.mkReplySubmitSignsForEvidence@{
                          err := none;
                        };
                    in some
                      ActionEffect.mk@{
                        env := newEnv;
                        msgs :=
                          [
                            EngineMsg.mk@{
                              sender := getEngineIDFromEngineCfg cfg;
                              target := msgSender;
                              mailbox := some 0;
                              msg :=
                                Anoma.PreMsg.MsgSignsFor
                                  (SignsForMsg.SubmitSignsForEvidenceReply
                                    responseMsg);
                            };
                          ];
                        timers := [];
                        engines := [];
                      }
                }
           | false :=
             let
               responseMsg :=
                 ReplySubmitSignsForEvidence.mkReplySubmitSignsForEvidence@{
                   err := some "Invalid evidence provided.";
                 };
             in some
               ActionEffect.mk@{
                 env := env;
                 msgs :=
                   [
                     EngineMsg.mk@{
                       sender := getEngineIDFromEngineCfg cfg;
                       target := msgSender;
                       mailbox := some 0;
                       msg :=
                         Anoma.PreMsg.MsgSignsFor
                           (SignsForMsg.SubmitSignsForEvidenceReply
                             responseMsg);
                     };
                   ];
                 timers := [];
                 engines := [];
               }
         }
       | _ := none;

queryEvidenceAction
  (input : SignsForActionInput) : Option SignsForActionEffect :=
  let
    env := ActionInput.env input;
    cfg := ActionInput.cfg input;
    tt := ActionInput.trigger input;
    localState := EngineEnv.localState env;
  in case getEngineMsgFromTimestampedTrigger tt of
       | some EngineMsg.mk@{
                msg := Anoma.PreMsg.MsgSignsFor (SignsForMsg.QuerySignsForEvidenceRequest (RequestQuerySignsForEvidence.mkRequestQuerySignsForEvidence externalIdentity));
                sender := msgSender;
              } :=
         let
           relevantEvidence :=
             Set.filter
               \{evidence :=
                 isEqual
                     (Ord.compare
                       (SignsForEvidence.fromIdentity evidence)
                       externalIdentity)
                   || isEqual
                     (Ord.compare
                       (SignsForEvidence.toIdentity evidence)
                       externalIdentity)}
               (SignsForLocalState.evidenceStore localState);
           responseMsg :=
             ReplyQuerySignsForEvidence.mkReplyQuerySignsForEvidence@{
               externalIdentity := externalIdentity;
               evidence := relevantEvidence;
               err := none;
             };
         in some
           ActionEffect.mk@{
             env := env;
             msgs :=
               [
                 EngineMsg.mk@{
                   sender := getEngineIDFromEngineCfg cfg;
                   target := msgSender;
                   mailbox := some 0;
                   msg :=
                     Anoma.PreMsg.MsgSignsFor
                       (SignsForMsg.QuerySignsForEvidenceReply responseMsg);
                 };
               ];
             timers := [];
             engines := [];
           }
       | _ := none;

signsForQueryActionLabel : SignsForActionExec :=
  ActionExec.Seq [signsForQueryAction];

submitEvidenceActionLabel : SignsForActionExec :=
  ActionExec.Seq [submitEvidenceAction];

queryEvidenceActionLabel : SignsForActionExec :=
  ActionExec.Seq [queryEvidenceAction];

SignsForGuard : Type :=
  Guard
    SignsForCfg
    SignsForLocalState
    SignsForMailboxState
    SignsForTimerHandle
    SignsForActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

SignsForGuardOutput : Type :=
  GuardOutput
    SignsForCfg
    SignsForLocalState
    SignsForMailboxState
    SignsForTimerHandle
    SignsForActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

SignsForGuardEval : Type :=
  GuardEval
    SignsForCfg
    SignsForLocalState
    SignsForMailboxState
    SignsForTimerHandle
    SignsForActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

signsForQueryGuard
  (tt : TimestampedTrigger SignsForTimerHandle Anoma.Msg)
  (cfg : EngineCfg SignsForCfg)
  (env : SignsForEnv)
  : Option SignsForGuardOutput :=
  case getEngineMsgFromTimestampedTrigger tt of
    | some EngineMsg.mk@{
             msg := Anoma.PreMsg.MsgSignsFor (SignsForMsg.SignsForRequest _);
           } :=
      some
        GuardOutput.mk@{
          action := signsForQueryActionLabel;
          args := [];
        }
    | _ := none;

submitEvidenceGuard
  (tt : TimestampedTrigger SignsForTimerHandle Anoma.Msg)
  (cfg : EngineCfg SignsForCfg)
  (env : SignsForEnv)
  : Option SignsForGuardOutput :=
  case getEngineMsgFromTimestampedTrigger tt of
    | some EngineMsg.mk@{
             msg := Anoma.PreMsg.MsgSignsFor (SignsForMsg.SubmitSignsForEvidenceRequest _);
           } :=
      some
        GuardOutput.mk@{
          action := submitEvidenceActionLabel;
          args := [];
        }
    | _ := none;

queryEvidenceGuard
  (tt : TimestampedTrigger SignsForTimerHandle Anoma.Msg)
  (cfg : EngineCfg SignsForCfg)
  (env : SignsForEnv)
  : Option SignsForGuardOutput :=
  case getEngineMsgFromTimestampedTrigger tt of
    | some EngineMsg.mk@{
             msg := Anoma.PreMsg.MsgSignsFor (SignsForMsg.QuerySignsForEvidenceRequest _);
           } :=
      some
        GuardOutput.mk@{
          action := queryEvidenceActionLabel;
          args := [];
        }
    | _ := none;

SignsForBehaviour : Type :=
  EngineBehaviour
    SignsForCfg
    SignsForLocalState
    SignsForMailboxState
    SignsForTimerHandle
    SignsForActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

signsForBehaviour : SignsForBehaviour :=
  EngineBehaviour.mk@{
    guards :=
      GuardEval.First
        [signsForQueryGuard; submitEvidenceGuard; queryEvidenceGuard];
  };