module arch.node.engines.local_key_value_storage_behaviour;

import arch.node.engines.local_key_value_storage_messages open;
import arch.node.engines.local_key_value_storage_config open;
import arch.node.engines.local_key_value_storage_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 LocalKVStorageActionArgument := | LocalKVStorageReplyTo EngineID;

LocalKVStorageActionArguments : Type := List LocalKVStorageActionArgument;

LocalKVStorageAction : Type :=
  Action
    LocalKVStorageCfg
    LocalKVStorageLocalState
    LocalKVStorageMailboxState
    LocalKVStorageTimerHandle
    LocalKVStorageActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

LocalKVStorageActionInput : Type :=
  ActionInput
    LocalKVStorageCfg
    LocalKVStorageLocalState
    LocalKVStorageMailboxState
    LocalKVStorageTimerHandle
    LocalKVStorageActionArguments
    Anoma.Msg;

LocalKVStorageActionEffect : Type :=
  ActionEffect
    LocalKVStorageLocalState
    LocalKVStorageMailboxState
    LocalKVStorageTimerHandle
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

LocalKVStorageActionExec : Type :=
  ActionExec
    LocalKVStorageCfg
    LocalKVStorageLocalState
    LocalKVStorageMailboxState
    LocalKVStorageTimerHandle
    LocalKVStorageActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

getValueAction
  (input : LocalKVStorageActionInput) : Option LocalKVStorageActionEffect :=
  let
    env := ActionInput.env input;
    cfg := ActionInput.cfg input;
    local := EngineEnv.localState env;
    storage := LocalKVStorageLocalState.storage local;
    trigger := ActionInput.trigger input;
  in case getEngineMsgFromTimestampedTrigger trigger of
       | some emsg :=
         case emsg of {
           | mkEngineMsg@{
               msg := Anoma.MsgLocalKVStorage (LocalKVStorageMsgGetValueRequest req);
             } :=
             some
               mkActionEffect@{
                 env := env;
                 msgs :=
                   [
                     mkEngineMsg@{
                       sender := getEngineIDFromEngineCfg cfg;
                       target := EngineMsg.sender emsg;
                       mailbox := some 0;
                       msg :=
                         Anoma.MsgLocalKVStorage
                           (LocalKVStorageMsgGetValueReply
                             mkGetValueKVStoreReply@{
                               key := GetValueKVStoreRequest.key req;
                               value :=
                                 fromOption
                                   (Map.lookup
                                     (GetValueKVStoreRequest.key req)
                                     storage)
                                   "";
                             });
                     };
                   ];
                 timers := [];
                 engines := [];
               }
           | _ := none
         }
       | _ := none;

setValueAction
  (input : LocalKVStorageActionInput) : Option LocalKVStorageActionEffect :=
  let
    env := ActionInput.env input;
    cfg := ActionInput.cfg input;
    local := EngineEnv.localState env;
    storage := LocalKVStorageLocalState.storage local;
    trigger := ActionInput.trigger input;
    newTime := advanceTime (LocalKVStorageLocalState.localClock local);
  in case getEngineMsgFromTimestampedTrigger trigger of
       | some emsg :=
         case emsg of {
           | mkEngineMsg@{
               msg := Anoma.MsgLocalKVStorage (LocalKVStorageMsgSetValueRequest req);
             } :=
             let
               key := SetValueKVStoreRequest.key req;
               value := SetValueKVStoreRequest.value req;
               newStorage := Map.insert key value storage;
               newLocal :=
                 local@LocalKVStorageLocalState{
                   storage := newStorage;
                   localClock := newTime;
                 };
               newEnv := env@EngineEnv{localState := newLocal};
               responseMsg :=
                 mkEngineMsg@{
                   sender := getEngineIDFromEngineCfg cfg;
                   target := EngineMsg.sender emsg;
                   mailbox := some 0;
                   msg :=
                     Anoma.MsgLocalKVStorage
                       (LocalKVStorageMsgSetValueReply
                         mkSetValueKVStoreReply@{
                           key := key;
                           success := true;
                         });
                 };
               notificationMsg :=
                 \{target :=
                   mkEngineMsg@{
                     sender := getEngineIDFromEngineCfg cfg;
                     target := target;
                     mailbox := some 0;
                     msg :=
                       Anoma.MsgLocalKVStorage
                         (LocalKVStorageMsgValueChanged
                           mkValueChangedKVStore@{
                             key := key;
                             value := value;
                             timestamp := newTime;
                           });
                   }};
               notificationMsgs :=
                 map notificationMsg (getNotificationTargets key);
             in some
               mkActionEffect@{
                 env := newEnv;
                 msgs := responseMsg :: notificationMsgs;
                 timers := [];
                 engines := [];
               }
           | _ := none
         }
       | _ := none;

deleteValueAction
  (input : LocalKVStorageActionInput) : Option LocalKVStorageActionEffect :=
  let
    env := ActionInput.env input;
    cfg := ActionInput.cfg input;
    local := EngineEnv.localState env;
    storage := LocalKVStorageLocalState.storage local;
    trigger := ActionInput.trigger input;
    newTime := advanceTime (LocalKVStorageLocalState.localClock local);
  in case getEngineMsgFromTimestampedTrigger trigger of
       | some emsg :=
         case emsg of {
           | mkEngineMsg@{
               msg := Anoma.MsgLocalKVStorage (LocalKVStorageMsgDeleteValueRequest req);
             } :=
             let
               key := DeleteValueKVStoreRequest.key req;
               newStorage := Map.delete key storage;
               newLocal :=
                 local@LocalKVStorageLocalState{
                   storage := newStorage;
                   localClock := newTime;
                 };
               newEnv := env@EngineEnv{localState := newLocal};
               responseMsg :=
                 mkEngineMsg@{
                   sender := getEngineIDFromEngineCfg cfg;
                   target := EngineMsg.sender emsg;
                   mailbox := some 0;
                   msg :=
                     Anoma.MsgLocalKVStorage
                       (LocalKVStorageMsgDeleteValueReply
                         mkDeleteValueKVStoreReply@{
                           key := key;
                           success := true;
                         });
                 };
               notificationMsg :=
                 \{target :=
                   mkEngineMsg@{
                     sender := getEngineIDFromEngineCfg cfg;
                     target := target;
                     mailbox := some 0;
                     msg :=
                       Anoma.MsgLocalKVStorage
                         (LocalKVStorageMsgValueChanged
                           mkValueChangedKVStore@{
                             key := key;
                             value := "";
                             timestamp := newTime;
                           });
                   }};
               notificationMsgs :=
                 map notificationMsg (getNotificationTargets key);
             in some
               mkActionEffect@{
                 env := newEnv;
                 msgs := responseMsg :: notificationMsgs;
                 timers := [];
                 engines := [];
               }
           | _ := none
         }
       | _ := none;

getValueActionLabel : LocalKVStorageActionExec := Seq [getValueAction];

setValueActionLabel : LocalKVStorageActionExec := Seq [setValueAction];

deleteValueActionLabel : LocalKVStorageActionExec := Seq [deleteValueAction];

LocalKVStorageGuard : Type :=
  Guard
    LocalKVStorageCfg
    LocalKVStorageLocalState
    LocalKVStorageMailboxState
    LocalKVStorageTimerHandle
    LocalKVStorageActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

LocalKVStorageGuardOutput : Type :=
  GuardOutput
    LocalKVStorageCfg
    LocalKVStorageLocalState
    LocalKVStorageMailboxState
    LocalKVStorageTimerHandle
    LocalKVStorageActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

LocalKVStorageGuardEval : Type :=
  GuardEval
    LocalKVStorageCfg
    LocalKVStorageLocalState
    LocalKVStorageMailboxState
    LocalKVStorageTimerHandle
    LocalKVStorageActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

getValueGuard
  (trigger : LocalKVStorageTimestampedTrigger)
  (cfg : EngineCfg LocalKVStorageCfg)
  (env : LocalKVStorageEnv)
  : Option LocalKVStorageGuardOutput :=
  case getEngineMsgFromTimestampedTrigger trigger of
    | some mkEngineMsg@{
             msg := Anoma.MsgLocalKVStorage (LocalKVStorageMsgGetValueRequest _);
           } :=
      some
        mkGuardOutput@{
          action := getValueActionLabel;
          args := [];
        }
    | _ := none;

setValueGuard
  (trigger : LocalKVStorageTimestampedTrigger)
  (cfg : EngineCfg LocalKVStorageCfg)
  (env : LocalKVStorageEnv)
  : Option LocalKVStorageGuardOutput :=
  case getEngineMsgFromTimestampedTrigger trigger of
    | some mkEngineMsg@{
             msg := Anoma.MsgLocalKVStorage (LocalKVStorageMsgSetValueRequest _);
           } :=
      some
        mkGuardOutput@{
          action := setValueActionLabel;
          args := [];
        }
    | _ := none;

deleteValueGuard
  (trigger : LocalKVStorageTimestampedTrigger)
  (cfg : EngineCfg LocalKVStorageCfg)
  (env : LocalKVStorageEnv)
  : Option LocalKVStorageGuardOutput :=
  case getEngineMsgFromTimestampedTrigger trigger of
    | some mkEngineMsg@{
             msg := Anoma.MsgLocalKVStorage (LocalKVStorageMsgDeleteValueRequest _);
           } :=
      some
        mkGuardOutput@{
          action := deleteValueActionLabel;
          args := [];
        }
    | _ := none;

LocalKVStorageBehaviour : Type :=
  EngineBehaviour
    LocalKVStorageCfg
    LocalKVStorageLocalState
    LocalKVStorageMailboxState
    LocalKVStorageTimerHandle
    LocalKVStorageActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

localKVStorageBehaviour : LocalKVStorageBehaviour :=
  mkEngineBehaviour@{
    guards := First [getValueGuard; setValueGuard; deleteValueGuard];
  };