module arch.node.types.messages;

import prelude open public;
import arch.node.types.basics open;
import arch.node.types.crypto open;
import arch.node.types.identities open;

syntax alias EngineMsgID := Digest;

type Mailbox S M :=
  mkMailbox@{
    messages : List (EngineMsg M);
    mailboxState : Option S;
  };

syntax alias MailboxID := Nat;

type EngineMsg M :=
  mkEngineMsg@{
    sender : EngineID;
    target : EngineID;
    mailbox : Option MailboxID;
    msg : M;
  };

type Timer H :=
  mkTimer@{
    time : Time;
    handle : H;
  };

type Trigger H M :=
  | MessageArrived@{
      msg : EngineMsg M;
    }
  | Elapsed@{
      timers : List (Timer H);
    };

getEngineMsgFromTrigger {H M} (tr : Trigger H M) : Option (EngineMsg M) :=
  case tr of
    | MessageArrived@{msg} := some msg
    | Elapsed@{} := none;

getMsgFromTrigger {H M} (tr : Trigger H M) : Option M :=
  case tr of
    | MessageArrived@{msg} := some (EngineMsg.msg msg)
    | Elapsed@{} := none;

getSenderFromTrigger {H M} (tr : Trigger H M) : Option EngineID :=
  case tr of
    | MessageArrived@{msg} := some (EngineMsg.sender msg)
    | Elapsed@{} := none;

getTargetFromTrigger {H M} (tr : Trigger H M) : Option EngineID :=
  case tr of
    | MessageArrived@{msg} := some (EngineMsg.target msg)
    | Elapsed@{} := none;

type TimestampedTrigger H M :=
  mkTimestampedTrigger@{
    time : Time;
    trigger : Trigger H M;
  };

getEngineMsgFromTimestampedTrigger
  {H M} (tr : TimestampedTrigger H M) : Option (EngineMsg M) :=
  getEngineMsgFromTrigger (TimestampedTrigger.trigger tr);

getMsgFromTimestampedTrigger {H M} (tr : TimestampedTrigger H M) : Option M :=
  getMsgFromTrigger (TimestampedTrigger.trigger tr);

getSenderFromTimestampedTrigger
  {H M} (tr : TimestampedTrigger H M) : Option EngineID :=
  getSenderFromTrigger (TimestampedTrigger.trigger tr);

getTargetFromTimestampedTrigger
  {H M} (tr : TimestampedTrigger H M) : Option EngineID :=
  getTargetFromTrigger (TimestampedTrigger.trigger tr);