module arch.node.engines.naming_behaviour;

import Stdlib.Data.Set as Set;

import prelude open;
import arch.node.types.messages open;
import arch.node.types.engine open;
import arch.node.types.identities open;
import arch.node.engines.naming_messages open;
import arch.node.engines.naming_config open;
import arch.node.engines.naming_environment open;
import arch.node.types.anoma as Anoma open;

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

type NamingActionArgument := | NamingActionArgumentReplyTo ReplyTo;

NamingActionArguments : Type := List NamingActionArgument;

NamingAction : Type :=
  Action
    NamingCfg
    NamingLocalState
    NamingMailboxState
    NamingTimerHandle
    NamingActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

NamingActionInput : Type :=
  ActionInput
    NamingCfg
    NamingLocalState
    NamingMailboxState
    NamingTimerHandle
    NamingActionArguments
    Anoma.Msg;

NamingActionEffect : Type :=
  ActionEffect
    NamingLocalState
    NamingMailboxState
    NamingTimerHandle
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

NamingActionExec : Type :=
  ActionExec
    NamingCfg
    NamingLocalState
    NamingMailboxState
    NamingTimerHandle
    NamingActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

resolveNameAction (input : NamingActionInput) : Option NamingActionEffect :=
  let
    env := ActionInput.env input;
    cfg := ActionInput.cfg input;
    tt := ActionInput.trigger input;
    localState := EngineEnv.localState env;
    identityName :=
      case getEngineMsgFromTimestampedTrigger tt of
        | some EngineMsg.mk@{
                 msg := Anoma.PreMsg.MsgNaming (NamingMsg.ResolveNameRequest req);
               } := some (RequestResolveName.identityName req)
        | _ := none;
  in case identityName of
       | some name :=
         let
           matchingEvidence :=
             Set.filter
               \{evidence :=
                 isEqual
                   (Ord.compare
                     (IdentityNameEvidence.identityName evidence)
                     name)}
               (NamingLocalState.evidenceStore localState);
           identities :=
             Set.fromList
               (map
                 \{evidence := IdentityNameEvidence.externalIdentity evidence}
                 (Set.toList matchingEvidence));
           responseMsg :=
             ReplyResolveName.mkReplyResolveName@{
               externalIdentities := identities;
               err := none;
             };
         in case getEngineMsgFromTimestampedTrigger tt of {
              | some emsg :=
                some
                  ActionEffect.mk@{
                    env := env;
                    msgs :=
                      [
                        EngineMsg.mk@{
                          sender := getEngineIDFromEngineCfg cfg;
                          target := EngineMsg.sender emsg;
                          mailbox := some 0;
                          msg :=
                            Anoma.PreMsg.MsgNaming
                              (NamingMsg.ResolveNameReply responseMsg);
                        };
                      ];
                    timers := [];
                    engines := [];
                  }
              | _ := none
            }
       | _ := none;

submitNameEvidenceAction
  (input : NamingActionInput) : Option NamingActionEffect :=
  let
    env := ActionInput.env input;
    cfg := ActionInput.cfg input;
    tt := ActionInput.trigger input;
    localState := EngineEnv.localState env;
    evidence :=
      case getEngineMsgFromTimestampedTrigger tt of
        | some EngineMsg.mk@{
                 msg := Anoma.PreMsg.MsgNaming (NamingMsg.SubmitNameEvidenceRequest req);
               } := some (RequestSubmitNameEvidence.evidence req)
        | _ := none;
  in case evidence of
       | some ev :=
         let
           isValid := verifyEvidence ev;
           alreadyExists :=
             case isValid of
               | true :=
                 isElement
                   \{a b := a && b}
                   true
                   (map
                     \{e := isEqual (Ord.compare e ev)}
                     (Set.toList (NamingLocalState.evidenceStore localState)))
               | false := false;
           newEnv :=
             case isValid && not alreadyExists of
               | true :=
                 env@EngineEnv{localState := localState@NamingLocalState{evidenceStore := Set.insert
                   ev
                   (NamingLocalState.evidenceStore localState)}}
               | false := env;
           responseMsg :=
             ReplySubmitNameEvidence.mkReplySubmitNameEvidence@{
               err :=
                 case isValid of
                   | false := some "Invalid evidence"
                   | true :=
                     case alreadyExists of
                       | true := some "Evidence already exists"
                       | false := none;
             };
         in case getEngineMsgFromTimestampedTrigger tt of {
              | some emsg :=
                some
                  ActionEffect.mk@{
                    env := newEnv;
                    msgs :=
                      [
                        EngineMsg.mk@{
                          sender := getEngineIDFromEngineCfg cfg;
                          target := EngineMsg.sender emsg;
                          mailbox := some 0;
                          msg :=
                            Anoma.PreMsg.MsgNaming
                              (NamingMsg.SubmitNameEvidenceReply responseMsg);
                        };
                      ];
                    timers := [];
                    engines := [];
                  }
              | _ := none
            }
       | _ := none;

queryNameEvidenceAction
  (input : NamingActionInput) : Option NamingActionEffect :=
  let
    env := ActionInput.env input;
    cfg := ActionInput.cfg input;
    tt := ActionInput.trigger input;
    localState := EngineEnv.localState env;
    externalIdentity :=
      case getEngineMsgFromTimestampedTrigger tt of
        | some EngineMsg.mk@{
                 msg := Anoma.PreMsg.MsgNaming (NamingMsg.QueryNameEvidenceRequest req);
               } := some (RequestQueryNameEvidence.externalIdentity req)
        | _ := none;
  in case externalIdentity of
       | some extId :=
         let
           relevantEvidence :=
             Set.filter
               \{evidence :=
                 isEqual
                   (Ord.compare
                     (IdentityNameEvidence.externalIdentity evidence)
                     extId)}
               (NamingLocalState.evidenceStore localState);
           responseMsg :=
             ReplyQueryNameEvidence.mkReplyQueryNameEvidence@{
               externalIdentity := extId;
               evidence := relevantEvidence;
               err := none;
             };
         in case getEngineMsgFromTimestampedTrigger tt of {
              | some emsg :=
                some
                  ActionEffect.mk@{
                    env := env;
                    msgs :=
                      [
                        EngineMsg.mk@{
                          sender := getEngineIDFromEngineCfg cfg;
                          target := EngineMsg.sender emsg;
                          mailbox := some 0;
                          msg :=
                            Anoma.PreMsg.MsgNaming
                              (NamingMsg.QueryNameEvidenceReply responseMsg);
                        };
                      ];
                    timers := [];
                    engines := [];
                  }
              | _ := none
            }
       | _ := none;

resolveNameActionLabel : NamingActionExec := ActionExec.Seq [resolveNameAction];

submitNameEvidenceActionLabel : NamingActionExec :=
  ActionExec.Seq [submitNameEvidenceAction];

queryNameEvidenceActionLabel : NamingActionExec :=
  ActionExec.Seq [queryNameEvidenceAction];

NamingGuard : Type :=
  Guard
    NamingCfg
    NamingLocalState
    NamingMailboxState
    NamingTimerHandle
    NamingActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

NamingGuardOutput : Type :=
  GuardOutput
    NamingCfg
    NamingLocalState
    NamingMailboxState
    NamingTimerHandle
    NamingActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

NamingGuardEval : Type :=
  GuardEval
    NamingCfg
    NamingLocalState
    NamingMailboxState
    NamingTimerHandle
    NamingActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

resolveNameGuard
  (tt : TimestampedTrigger NamingTimerHandle Anoma.Msg)
  (cfg : EngineCfg NamingCfg)
  (env : NamingEnv)
  : Option NamingGuardOutput :=
  case getEngineMsgFromTimestampedTrigger tt of
    | some EngineMsg.mk@{
             msg := Anoma.PreMsg.MsgNaming (NamingMsg.ResolveNameRequest _);
           } :=
      some
        GuardOutput.mk@{
          action := resolveNameActionLabel;
          args := [];
        }
    | _ := none;

submitNameEvidenceGuard
  (tt : TimestampedTrigger NamingTimerHandle Anoma.Msg)
  (cfg : EngineCfg NamingCfg)
  (env : NamingEnv)
  : Option NamingGuardOutput :=
  case getEngineMsgFromTimestampedTrigger tt of
    | some EngineMsg.mk@{
             msg := Anoma.PreMsg.MsgNaming (NamingMsg.SubmitNameEvidenceRequest _);
           } :=
      some
        GuardOutput.mk@{
          action := submitNameEvidenceActionLabel;
          args := [];
        }
    | _ := none;

queryNameEvidenceGuard
  (tt : TimestampedTrigger NamingTimerHandle Anoma.Msg)
  (cfg : EngineCfg NamingCfg)
  (env : NamingEnv)
  : Option NamingGuardOutput :=
  case getEngineMsgFromTimestampedTrigger tt of
    | some EngineMsg.mk@{
             msg := Anoma.PreMsg.MsgNaming (NamingMsg.QueryNameEvidenceRequest _);
           } :=
      some
        GuardOutput.mk@{
          action := queryNameEvidenceActionLabel;
          args := [];
        }
    | _ := none;

NamingBehaviour : Type :=
  EngineBehaviour
    NamingCfg
    NamingLocalState
    NamingMailboxState
    NamingTimerHandle
    NamingActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

namingBehaviour : NamingBehaviour :=
  EngineBehaviour.mk@{
    guards :=
      GuardEval.First
        [resolveNameGuard; submitNameEvidenceGuard; queryNameEvidenceGuard];
  };