module arch.node.engines.executor_environment;

import prelude open;
import arch.node.types.messages open;
import arch.node.types.identities open;
import arch.node.types.engine_environment open;
import arch.node.engines.executor_messages open;
import arch.node.types.anoma_message as Anoma open;

trait
type Runnable KVSKey KVSDatum Executable ProgramState :=
  mkRunnable@{
    executeStep
      : Executable
        -> ProgramState
        -> Pair KVSKey KVSDatum
        -> Result
          String
          (Pair ProgramState (List (Either KVSKey (Pair KVSKey KVSDatum))));
    halted : ProgramState -> Bool;
    startingState : ProgramState;
  };

syntax alias ExecutorMailboxState := Unit;

type ExecutorLocalState KVSKey KVSDatum ProgramState :=
  mkExecutorLocalState@{
    program_state : ProgramState;
    completed_reads : Map KVSKey KVSDatum;
    completed_writes : Map KVSKey KVSDatum;
  };

syntax alias ExecutorTimerHandle := Unit;

ExecutorEnv (KVSKey KVSDatum ProgramState : Type) : Type :=
  EngineEnv
    (ExecutorLocalState KVSKey KVSDatum ProgramState)
    ExecutorMailboxState
    ExecutorTimerHandle
    Anoma.Msg;

module executor_environment_example;
  
  executorEnv {KVSKey KVSDatum} : ExecutorEnv KVSKey KVSDatum String :=
    mkEngineEnv@{
      localState :=
        mkExecutorLocalState@{
          program_state := "";
          completed_reads := Map.empty;
          completed_writes := Map.empty;
        };
      mailboxCluster := Map.empty;
      acquaintances := Set.empty;
      timers := [];
    };
end;