module arch.node.engines.local_time_series_storage_environment;

import prelude open;
import arch.node.engines.local_time_series_storage_messages open;
import arch.node.types.engine open;
import arch.node.types.messages open;
import arch.node.types.identities open;
import arch.node.types.anoma_message as Anoma open;

syntax alias LocalTSStorageMailboxState := Unit;
syntax alias Database := String;
-- Abstract DB type

axiom updateDB : Database -> TSStorageDBQuery -> TSStorageDBData -> Database;

axiom queryDB : Database -> TSStorageDBQuery -> Option TSStorageDBData;

axiom getNotificationTargets : TSStorageDBQuery -> List EngineID;

axiom advanceTime : EpochTimestamp -> EpochTimestamp;

type LocalTSStorageLocalState :=
  mkLocalTSStorageLocalState@{
    db : Database;
    localClock : EpochTimestamp;
  };

syntax alias LocalTSStorageTimerHandle := Unit;

LocalTSStorageTimestampedTrigger : Type :=
  TimestampedTrigger LocalTSStorageTimerHandle Anoma.Msg;

LocalTSStorageEnv : Type :=
  EngineEnv
    LocalTSStorageLocalState
    LocalTSStorageMailboxState
    LocalTSStorageTimerHandle
    Anoma.Msg;

module local_ts_storage_environment_example;
  
  localTSStorageEnv : LocalTSStorageEnv :=
    mkEngineEnv@{
      localState :=
        mkLocalTSStorageLocalState@{
          db := "";
          localClock := 0;
        };
      mailboxCluster := Map.empty;
      acquaintances := Set.empty;
      timers := [];
    };
end;