module arch.node.types.engine_behaviour;

import arch.node.types.basics open;
import arch.node.types.messages open;
import arch.node.types.identities open;
import arch.node.types.engine_config open;
import arch.node.types.engine_environment open;

Action (C S B H A AM AC AE : Type) : Type :=
  (input : ActionInput C S B H A AM) -> Option (ActionEffect S B H AM AC AE);

type ActionInput C S B H A AM :=
  mk@{
    args : A;
    cfg : EngineCfg C;
    env : EngineEnv S B H AM;
    trigger : TimestampedTrigger H AM;
  };

type ActionEffect S B H AM AC AE :=
  mk@{
    env : EngineEnv S B H AM;
    msgs : List (EngineMsg AM);
    timers : List (Timer H);
    engines : List (Pair AC AE);
  };

type ActionExec C S B H A AM AC AE := | Seq (List (Action C S B H A AM AC AE));

Guard (C S B H A AM AC AE : Type) : Type :=
  (trigger : TimestampedTrigger H AM)
    -> (cfg : EngineCfg C)
    -> (env : EngineEnv S B H AM)
    -> Option (GuardOutput C S B H A AM AC AE);

type GuardOutput C S B H A AM AC AE :=
  mk@{
    action : ActionExec C S B H A AM AC AE;
    args : A;
  };

type GuardEval C S B H A AM AC AE :=
  | First (List (Guard C S B H A AM AC AE))
  | Any (List (Guard C S B H A AM AC AE));

type EngineBehaviour C S B H A AM AC AE :=
  mk@{
    guards : GuardEval C S B H A AM AC AE;
  };