module arch.node.engines.shard_environment;

import prelude open;
import arch.node.engines.shard_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 ShardMailboxState := Unit;

type ReadStatus :=
  mkReadStatus@{
    hasBeenRead : Bool;
    isEager : Bool;
    executor : EngineID;
  };

type WriteStatus KVSDatum :=
  mkWriteStatus@{
    data : Option KVSDatum;
    mayWrite : Bool;
  };

type KeyAccess KVSDatum :=
  mkKeyAccess@{
    readStatus : Option ReadStatus;
    writeStatus : Option (WriteStatus KVSDatum);
  };

type DAGStructure KVSKey KVSDatum :=
  mkDAGStructure@{
    keyAccesses : Map KVSKey (Map TxFingerprint (KeyAccess KVSDatum));
    heardAllReads : TxFingerprint;
    heardAllWrites : TxFingerprint;
  };

type ShardLocalState KVSKey KVSDatum :=
  mk@{
    dagStructure : DAGStructure KVSKey KVSDatum;
    anchors : List NarwhalBlock;
  };

syntax alias ShardTimerHandle := Unit;

ShardEnv (KVSKey KVSDatum : Type) : Type :=
  EngineEnv
    (ShardLocalState KVSKey KVSDatum)
    ShardMailboxState
    ShardTimerHandle
    Anoma.Msg;

module shard_environment_example;
  
  shardEnv : ShardEnv String String :=
    EngineEnv.mk@{
      localState :=
        ShardLocalState.mk@{
          dagStructure :=
            DAGStructure.mkDAGStructure@{
              keyAccesses := Map.empty;
              heardAllReads := 0;
              heardAllWrites := 0;
            };
          anchors := [];
        };
      mailboxCluster := Map.empty;
      acquaintances := Set.empty;
      timers := [];
    };
end;