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.utils 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);
             } :=
             let
               responseMsg :=
                 Anoma.MsgLocalKVStorage
                   (LocalKVStorageMsgGetValueReply
                     mkGetValueKVStoreReply@{
                       key := GetValueKVStoreRequest.key req;
                       value :=
                         fromOption
                           (Map.lookup (GetValueKVStoreRequest.key req) storage)
                           "";
                     });
             in some
               (defaultReplyActionEffect
                 env
                 cfg
                 (EngineMsg.sender emsg)
                 responseMsg)
           | _ := 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 :=
                   defaultReplyMsg
                     cfg
                     target
                     (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 :=
                   defaultReplyMsg
                     cfg
                     target
                     (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];
  };