module arch.node.engines.local_time_series_storage_behaviour;

import arch.node.engines.local_time_series_storage_messages open;
import arch.node.engines.local_time_series_storage_config open;
import arch.node.engines.local_time_series_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 LocalTSStorageActionArgument := Unit;

LocalTSStorageActionArguments : Type := List LocalTSStorageActionArgument;

LocalTSStorageAction : Type :=
  Action
    LocalTSStorageCfg
    LocalTSStorageLocalState
    LocalTSStorageMailboxState
    LocalTSStorageTimerHandle
    LocalTSStorageActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

LocalTSStorageActionInput : Type :=
  ActionInput
    LocalTSStorageCfg
    LocalTSStorageLocalState
    LocalTSStorageMailboxState
    LocalTSStorageTimerHandle
    LocalTSStorageActionArguments
    Anoma.Msg;

LocalTSStorageActionEffect : Type :=
  ActionEffect
    LocalTSStorageLocalState
    LocalTSStorageMailboxState
    LocalTSStorageTimerHandle
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

LocalTSStorageActionExec : Type :=
  ActionExec
    LocalTSStorageCfg
    LocalTSStorageLocalState
    LocalTSStorageMailboxState
    LocalTSStorageTimerHandle
    LocalTSStorageActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

getDataAction
  (input : LocalTSStorageActionInput) : Option LocalTSStorageActionEffect :=
  let
    env := ActionInput.env input;
    trigger := ActionInput.trigger input;
    cfg := ActionInput.cfg input;
    local := EngineEnv.localState env;
  in case getEngineMsgFromTimestampedTrigger trigger of
       | some mkEngineMsg@{
                msg := Anoma.MsgLocalTSStorage (LocalTSStorageMsgGetRequest request);
                sender := sender;
              } :=
         let
           result :=
             queryDB
               (LocalTSStorageLocalState.db local)
               (GetDataTSStorageDBRequest.query request);
         in case result of {
              | some data :=
                some
                  mkActionEffect@{
                    env := env;
                    msgs :=
                      [
                        mkEngineMsg@{
                          sender := getEngineIDFromEngineCfg cfg;
                          target := sender;
                          mailbox := some 0;
                          msg :=
                            Anoma.MsgLocalTSStorage
                              (LocalTSStorageMsgGetReply
                                mkGetDataTSStorageDBReply@{
                                  query :=
                                    GetDataTSStorageDBRequest.query request;
                                  data := data;
                                });
                        };
                      ];
                    timers := [];
                    engines := [];
                  }
              | none := none
            }
       | _ := none;

recordDataAction
  (input : LocalTSStorageActionInput) : Option LocalTSStorageActionEffect :=
  let
    env := ActionInput.env input;
    trigger := ActionInput.trigger input;
    cfg := ActionInput.cfg input;
    local := EngineEnv.localState env;
    newTime := advanceTime (LocalTSStorageLocalState.localClock local);
  in case getEngineMsgFromTimestampedTrigger trigger of
       | some mkEngineMsg@{
                msg := Anoma.MsgLocalTSStorage (LocalTSStorageMsgRecordRequest request);
                sender := sender;
              } :=
         let
           query := RecordDataTSStorageDBRequest.query request;
           db := LocalTSStorageLocalState.db local;
           data := queryDB db query;
         in case data of {
              | some value :=
                let
                  newDb := updateDB db query value;
                  newEnv :=
                    env@EngineEnv{localState := mkLocalTSStorageLocalState@{
                                                  db := newDb;
                                                  localClock := newTime;
                                                }};
                  responseMsg :=
                    mkEngineMsg@{
                      sender := getEngineIDFromEngineCfg cfg;
                      target := sender;
                      mailbox := some 0;
                      msg :=
                        Anoma.MsgLocalTSStorage
                          (LocalTSStorageMsgDeleteReply
                            mkDeleteDataTSStorageDBReply@{
                              query := query;
                              success := true;
                            });
                    };
                  notificationMsg :=
                    \{target :=
                      mkEngineMsg@{
                        sender := getEngineIDFromEngineCfg cfg;
                        target := target;
                        mailbox := some 0;
                        msg :=
                          Anoma.MsgLocalTSStorage
                            (LocalTSStorageMsgDataChanged
                              mkDataChangedTSStorageDB@{
                                query := query;
                                data := value;
                                timestamp := newTime;
                              });
                      }};
                  notificationMsgs :=
                    map notificationMsg (getNotificationTargets query);
                in some
                  mkActionEffect@{
                    env := newEnv;
                    msgs := responseMsg :: notificationMsgs;
                    timers := [];
                    engines := [];
                  }
              | none :=
                some
                  mkActionEffect@{
                    env := env;
                    msgs :=
                      [
                        mkEngineMsg@{
                          sender := getEngineIDFromEngineCfg cfg;
                          target := sender;
                          mailbox := some 0;
                          msg :=
                            Anoma.MsgLocalTSStorage
                              (LocalTSStorageMsgRecordReply
                                mkRecordDataTSStorageDBReply@{
                                  query := query;
                                  success := false;
                                });
                        };
                      ];
                    timers := [];
                    engines := [];
                  }
            }
       | _ := none;

deleteDataAction
  (input : LocalTSStorageActionInput) : Option LocalTSStorageActionEffect :=
  let
    env := ActionInput.env input;
    trigger := ActionInput.trigger input;
    cfg := ActionInput.cfg input;
    local := EngineEnv.localState env;
    newTime := advanceTime (LocalTSStorageLocalState.localClock local);
  in case getEngineMsgFromTimestampedTrigger trigger of
       | some mkEngineMsg@{
                msg := Anoma.MsgLocalTSStorage (LocalTSStorageMsgDeleteRequest request);
                sender := sender;
              } :=
         let
           query := DeleteDataTSStorageDBRequest.query request;
           db := LocalTSStorageLocalState.db local;
           data := queryDB db query;
         in case data of {
              | some value :=
                let
                  newDb := updateDB db query "";
                  newEnv :=
                    env@EngineEnv{localState := mkLocalTSStorageLocalState@{
                                                  db := newDb;
                                                  localClock := newTime;
                                                }};
                  responseMsg :=
                    mkEngineMsg@{
                      sender := getEngineIDFromEngineCfg cfg;
                      target := sender;
                      mailbox := some 0;
                      msg :=
                        Anoma.MsgLocalTSStorage
                          (LocalTSStorageMsgDeleteReply
                            mkDeleteDataTSStorageDBReply@{
                              query := query;
                              success := true;
                            });
                    };
                  notificationMsg :=
                    \{target :=
                      mkEngineMsg@{
                        sender := getEngineIDFromEngineCfg cfg;
                        target := target;
                        mailbox := some 0;
                        msg :=
                          Anoma.MsgLocalTSStorage
                            (LocalTSStorageMsgDataChanged
                              mkDataChangedTSStorageDB@{
                                query := query;
                                data := value;
                                timestamp := newTime;
                              });
                      }};
                  notificationMsgs :=
                    map notificationMsg (getNotificationTargets query);
                in some
                  mkActionEffect@{
                    env := newEnv;
                    msgs := responseMsg :: notificationMsgs;
                    timers := [];
                    engines := [];
                  }
              | none :=
                some
                  mkActionEffect@{
                    env := env;
                    msgs :=
                      [
                        mkEngineMsg@{
                          sender := getEngineIDFromEngineCfg cfg;
                          target := sender;
                          mailbox := some 0;
                          msg :=
                            Anoma.MsgLocalTSStorage
                              (LocalTSStorageMsgDeleteReply
                                mkDeleteDataTSStorageDBReply@{
                                  query := query;
                                  success := false;
                                });
                        };
                      ];
                    timers := [];
                    engines := [];
                  }
            }
       | _ := none;

getDataActionLabel : LocalTSStorageActionExec := Seq [getDataAction];

recordDataActionLabel : LocalTSStorageActionExec := Seq [recordDataAction];

deleteDataActionLabel : LocalTSStorageActionExec := Seq [deleteDataAction];

LocalTSStorageGuard : Type :=
  Guard
    LocalTSStorageCfg
    LocalTSStorageLocalState
    LocalTSStorageMailboxState
    LocalTSStorageTimerHandle
    LocalTSStorageActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

LocalTSStorageGuardOutput : Type :=
  GuardOutput
    LocalTSStorageCfg
    LocalTSStorageLocalState
    LocalTSStorageMailboxState
    LocalTSStorageTimerHandle
    LocalTSStorageActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

LocalTSStorageGuardEval : Type :=
  GuardEval
    LocalTSStorageCfg
    LocalTSStorageLocalState
    LocalTSStorageMailboxState
    LocalTSStorageTimerHandle
    LocalTSStorageActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

getDataGuard
  (trigger : LocalTSStorageTimestampedTrigger)
  (cfg : EngineCfg LocalTSStorageCfg)
  (env : LocalTSStorageEnv)
  : Option LocalTSStorageGuardOutput :=
  case getEngineMsgFromTimestampedTrigger trigger of
    | some mkEngineMsg@{
             msg := Anoma.MsgLocalTSStorage (LocalTSStorageMsgGetRequest _);
           } :=
      some
        mkGuardOutput@{
          action := getDataActionLabel;
          args := [];
        }
    | _ := none;

recordDataGuard
  (trigger : LocalTSStorageTimestampedTrigger)
  (cfg : EngineCfg LocalTSStorageCfg)
  (env : LocalTSStorageEnv)
  : Option LocalTSStorageGuardOutput :=
  case getEngineMsgFromTimestampedTrigger trigger of
    | some mkEngineMsg@{
             msg := Anoma.MsgLocalTSStorage (LocalTSStorageMsgRecordRequest _);
           } :=
      some
        mkGuardOutput@{
          action := recordDataActionLabel;
          args := [];
        }
    | _ := none;

deleteDataGuard
  (trigger : LocalTSStorageTimestampedTrigger)
  (cfg : EngineCfg LocalTSStorageCfg)
  (env : LocalTSStorageEnv)
  : Option LocalTSStorageGuardOutput :=
  case getEngineMsgFromTimestampedTrigger trigger of
    | some mkEngineMsg@{
             msg := Anoma.MsgLocalTSStorage (LocalTSStorageMsgDeleteRequest _);
           } :=
      some
        mkGuardOutput@{
          action := deleteDataActionLabel;
          args := [];
        }
    | _ := none;

LocalTSStorageBehaviour : Type :=
  EngineBehaviour
    LocalTSStorageCfg
    LocalTSStorageLocalState
    LocalTSStorageMailboxState
    LocalTSStorageTimerHandle
    LocalTSStorageActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

localTSStorageBehaviour : LocalTSStorageBehaviour :=
  mkEngineBehaviour@{
    guards := First [getDataGuard; recordDataGuard; deleteDataGuard];
  };