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 EngineMsg.mk@{
                msg := Anoma.PreMsg.MsgLocalTSStorage (LocalTSStorageMsg.GetRequest request);
                sender := sender;
              } :=
         let
           result :=
             queryDB
               (LocalTSStorageLocalState.db local)
               (GetDataTSStorageDBRequest.query request);
         in case result of {
              | some data :=
                some
                  ActionEffect.mk@{
                    env := env;
                    msgs :=
                      [
                        EngineMsg.mk@{
                          sender := getEngineIDFromEngineCfg cfg;
                          target := sender;
                          mailbox := some 0;
                          msg :=
                            Anoma.PreMsg.MsgLocalTSStorage
                              (LocalTSStorageMsg.GetReply
                                GetDataTSStorageDBReply.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 EngineMsg.mk@{
                msg := Anoma.PreMsg.MsgLocalTSStorage (LocalTSStorageMsg.RecordRequest 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 := LocalTSStorageLocalState.mk@{
                                                  db := newDb;
                                                  localClock := newTime;
                                                }};
                  responseMsg :=
                    EngineMsg.mk@{
                      sender := getEngineIDFromEngineCfg cfg;
                      target := sender;
                      mailbox := some 0;
                      msg :=
                        Anoma.PreMsg.MsgLocalTSStorage
                          (LocalTSStorageMsg.DeleteReply
                            DeleteDataTSStorageDBReply.mkDeleteDataTSStorageDBReply@{
                              query := query;
                              success := true;
                            });
                    };
                  notificationMsg :=
                    \{target :=
                      EngineMsg.mk@{
                        sender := getEngineIDFromEngineCfg cfg;
                        target := target;
                        mailbox := some 0;
                        msg :=
                          Anoma.PreMsg.MsgLocalTSStorage
                            (LocalTSStorageMsg.DataChanged
                              DataChangedTSStorageDB.mkDataChangedTSStorageDB@{
                                query := query;
                                data := value;
                                timestamp := newTime;
                              });
                      }};
                  notificationMsgs :=
                    map notificationMsg (getNotificationTargets query);
                in some
                  ActionEffect.mk@{
                    env := newEnv;
                    msgs := responseMsg :: notificationMsgs;
                    timers := [];
                    engines := [];
                  }
              | none :=
                some
                  ActionEffect.mk@{
                    env := env;
                    msgs :=
                      [
                        EngineMsg.mk@{
                          sender := getEngineIDFromEngineCfg cfg;
                          target := sender;
                          mailbox := some 0;
                          msg :=
                            Anoma.PreMsg.MsgLocalTSStorage
                              (LocalTSStorageMsg.RecordReply
                                RecordDataTSStorageDBReply.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 EngineMsg.mk@{
                msg := Anoma.PreMsg.MsgLocalTSStorage (LocalTSStorageMsg.DeleteRequest 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 := LocalTSStorageLocalState.mk@{
                                                  db := newDb;
                                                  localClock := newTime;
                                                }};
                  responseMsg :=
                    EngineMsg.mk@{
                      sender := getEngineIDFromEngineCfg cfg;
                      target := sender;
                      mailbox := some 0;
                      msg :=
                        Anoma.PreMsg.MsgLocalTSStorage
                          (LocalTSStorageMsg.DeleteReply
                            DeleteDataTSStorageDBReply.mkDeleteDataTSStorageDBReply@{
                              query := query;
                              success := true;
                            });
                    };
                  notificationMsg :=
                    \{target :=
                      EngineMsg.mk@{
                        sender := getEngineIDFromEngineCfg cfg;
                        target := target;
                        mailbox := some 0;
                        msg :=
                          Anoma.PreMsg.MsgLocalTSStorage
                            (LocalTSStorageMsg.DataChanged
                              DataChangedTSStorageDB.mkDataChangedTSStorageDB@{
                                query := query;
                                data := value;
                                timestamp := newTime;
                              });
                      }};
                  notificationMsgs :=
                    map notificationMsg (getNotificationTargets query);
                in some
                  ActionEffect.mk@{
                    env := newEnv;
                    msgs := responseMsg :: notificationMsgs;
                    timers := [];
                    engines := [];
                  }
              | none :=
                some
                  ActionEffect.mk@{
                    env := env;
                    msgs :=
                      [
                        EngineMsg.mk@{
                          sender := getEngineIDFromEngineCfg cfg;
                          target := sender;
                          mailbox := some 0;
                          msg :=
                            Anoma.PreMsg.MsgLocalTSStorage
                              (LocalTSStorageMsg.DeleteReply
                                DeleteDataTSStorageDBReply.mkDeleteDataTSStorageDBReply@{
                                  query := query;
                                  success := false;
                                });
                        };
                      ];
                    timers := [];
                    engines := [];
                  }
            }
       | _ := none;

getDataActionLabel : LocalTSStorageActionExec := ActionExec.Seq [getDataAction];

recordDataActionLabel : LocalTSStorageActionExec :=
  ActionExec.Seq [recordDataAction];

deleteDataActionLabel : LocalTSStorageActionExec :=
  ActionExec.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 EngineMsg.mk@{
             msg := Anoma.PreMsg.MsgLocalTSStorage (LocalTSStorageMsg.GetRequest _);
           } :=
      some
        GuardOutput.mk@{
          action := getDataActionLabel;
          args := [];
        }
    | _ := none;

recordDataGuard
  (trigger : LocalTSStorageTimestampedTrigger)
  (cfg : EngineCfg LocalTSStorageCfg)
  (env : LocalTSStorageEnv)
  : Option LocalTSStorageGuardOutput :=
  case getEngineMsgFromTimestampedTrigger trigger of
    | some EngineMsg.mk@{
             msg := Anoma.PreMsg.MsgLocalTSStorage (LocalTSStorageMsg.RecordRequest _);
           } :=
      some
        GuardOutput.mk@{
          action := recordDataActionLabel;
          args := [];
        }
    | _ := none;

deleteDataGuard
  (trigger : LocalTSStorageTimestampedTrigger)
  (cfg : EngineCfg LocalTSStorageCfg)
  (env : LocalTSStorageEnv)
  : Option LocalTSStorageGuardOutput :=
  case getEngineMsgFromTimestampedTrigger trigger of
    | some EngineMsg.mk@{
             msg := Anoma.PreMsg.MsgLocalTSStorage (LocalTSStorageMsg.DeleteRequest _);
           } :=
      some
        GuardOutput.mk@{
          action := deleteDataActionLabel;
          args := [];
        }
    | _ := none;

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

localTSStorageBehaviour : LocalTSStorageBehaviour :=
  EngineBehaviour.mk@{
    guards := GuardEval.First [getDataGuard; recordDataGuard; deleteDataGuard];
  };