module arch.node.engines.signs_for_behaviour;

import prelude open;
import arch.node.utils open;
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 mkEngineMsg@{
                msg := Anoma.MsgSignsFor (MsgSignsForRequest (mkRequestSignsFor externalIdentityA externalIdentityB));
                sender := msgSender;
              } :=
         let
           hasEvidence :=
             isElement
               \{a b := a && b}
               true
               (map
                 \{evidence :=
                   isEqual
                       (Ord.cmp
                         (SignsForEvidence.fromIdentity evidence)
                         externalIdentityA)
                     && isEqual
                       (Ord.cmp
                         (SignsForEvidence.toIdentity evidence)
                         externalIdentityB)}
                 (Set.toList (SignsForLocalState.evidenceStore localState)));
           responseMsg :=
             Anoma.MsgSignsFor
               (MsgSignsForReply
                 mkReplySignsFor@{
                   signsFor := hasEvidence;
                   err := none;
                 });
         in some (defaultReplyActionEffect env cfg msgSender responseMsg)
       | _ := 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 mkEngineMsg@{
                msg := Anoma.MsgSignsFor (MsgSubmitSignsForEvidenceRequest (mkRequestSubmitSignsForEvidence evidence));
                sender := msgSender;
              } :=
         case verifyEvidence evidence of {
           | true :=
             let
               alreadyExists :=
                 isElement
                   \{a b := a && b}
                   true
                   (map
                     \{e := isEqual (Ord.cmp e evidence)}
                     (Set.toList
                       (SignsForLocalState.evidenceStore localState)));
             in case alreadyExists of {
                  | true :=
                    let
                      responseMsg :=
                        Anoma.MsgSignsFor
                          (MsgSubmitSignsForEvidenceReply
                            mkReplySubmitSignsForEvidence@{
                              err := some "Evidence already exists.";
                            });
                    in some
                      (defaultReplyActionEffect env cfg msgSender responseMsg)
                  | false :=
                    let
                      newEvidenceStore :=
                        Set.insert
                          evidence
                          (SignsForLocalState.evidenceStore localState);
                      updatedLocalState :=
                        localState@SignsForLocalState{evidenceStore := newEvidenceStore};
                      newEnv := env@EngineEnv{localState := updatedLocalState};
                      responseMsg :=
                        Anoma.MsgSignsFor
                          (MsgSubmitSignsForEvidenceReply
                            mkReplySubmitSignsForEvidence@{
                              err := none;
                            });
                    in some
                      (defaultReplyActionEffect
                        newEnv
                        cfg
                        msgSender
                        responseMsg)
                }
           | false :=
             let
               responseMsg :=
                 Anoma.MsgSignsFor
                   (MsgSubmitSignsForEvidenceReply
                     mkReplySubmitSignsForEvidence@{
                       err := some "Invalid evidence provided.";
                     });
             in some (defaultReplyActionEffect env cfg msgSender responseMsg)
         }
       | _ := 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 mkEngineMsg@{
                msg := Anoma.MsgSignsFor (MsgQuerySignsForEvidenceRequest (mkRequestQuerySignsForEvidence externalIdentity));
                sender := msgSender;
              } :=
         let
           relevantEvidence :=
             AVLTree.filter
               \{evidence :=
                 isEqual
                     (Ord.cmp
                       (SignsForEvidence.fromIdentity evidence)
                       externalIdentity)
                   || isEqual
                     (Ord.cmp
                       (SignsForEvidence.toIdentity evidence)
                       externalIdentity)}
               (SignsForLocalState.evidenceStore localState);
           responseMsg :=
             Anoma.MsgSignsFor
               (MsgQuerySignsForEvidenceReply
                 mkReplyQuerySignsForEvidence@{
                   externalIdentity := externalIdentity;
                   evidence := relevantEvidence;
                   err := none;
                 });
         in some (defaultReplyActionEffect env cfg msgSender responseMsg)
       | _ := none;

signsForQueryActionLabel : SignsForActionExec := Seq [signsForQueryAction];

submitEvidenceActionLabel : SignsForActionExec := Seq [submitEvidenceAction];

queryEvidenceActionLabel : SignsForActionExec := 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 mkEngineMsg@{msg := Anoma.MsgSignsFor (MsgSignsForRequest _)} :=
      some
        mkGuardOutput@{
          action := signsForQueryActionLabel;
          args := [];
        }
    | _ := none;

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

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

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

signsForBehaviour : SignsForBehaviour :=
  mkEngineBehaviour@{
    guards :=
      First [signsForQueryGuard; submitEvidenceGuard; queryEvidenceGuard];
  };