module anomian;

import arch.node.types.basics open public;
import arch.node.types.identities open;
import arch.node.types.messages open hiding {EngineMsg; mkEngineMsg; Mailbox};

type EngineStatus :=
  | Running
  | Dead
  | Suspended;

syntax alias EnglishPayload := String;
syntax alias FrenchPayload := String;
syntax alias SpanishPayload := String;

type AnomianMsgInterface :=
  | AnomianMsgEnglish@{
      msg : EnglishPayload;
    }
  | AnomianMsgFrench@{
      msg : FrenchPayload;
    };

type JordanMsgInterface :=
  | JordanMsgEnglish@{
      msg : EnglishPayload;
    }
  | JordanMsgSpanish@{
      msg : SpanishPayload;
    };

helloAnomian : AnomianMsgInterface :=
  AnomianMsgEnglish@{
    msg := "Hello!";
  };

type MsgInterface :=
  | MsgAnomian AnomianMsgInterface
  | MsgJordan JordanMsgInterface;

syntax alias Timeout := Nat;

type CommunicationPattern :=
  | FireAndForget
  | RequestReply@{
      timeout : Option Timeout;
    }
  | PubSub;

type EngineMsgKind :=
  | Request
  | Reply
  | Notify;

type EngineCfg C :=
  mkEngineCfg@{
    parent : Option EngineID;
    name : EngineName;
    node : NodeID;
    cfg : C;
  };

axiom localhost : NodeID;

simpleConfig : EngineCfg Unit :=
  mkEngineCfg@{
    parent := none;
    name := "Anomian";
    node := localhost;
    cfg := unit;
  };

-- no specific configuration
JordanID : EngineID := mkPair (some localhost) "Jordan9121";

AnomianID : EngineID := mkPair (some localhost) "Anomian184";

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

jordanToAnomian : EngineMsg MsgInterface :=
  mkEngineMsg@{
    sender := JordanID;
    target := AnomianID;
    mailbox := some 1;
    pattern :=
      RequestReply@{
        timeout := none;
      };
    kind := Request;
    msg :=
      MsgAnomian
        AnomianMsgEnglish@{
          msg := "What is the meaning of life?";
        };
  };

anomianToJordan : EngineMsg MsgInterface :=
  mkEngineMsg@{
    sender := AnomianID;
    target := JordanID;
    mailbox := some 1;
    pattern := FireAndForget;
    kind := Reply;
    msg :=
      MsgJordan
        JordanMsgEnglish@{
          msg := "The meaning of life is 42.";
        };
  };

type Mailbox S M :=
  mkMailbox@{
    messages : List (EngineMsg M);
    -- TODO: Should be a queue?
    mailboxState : Option S;
  };

MailboxCluster (S M : Type) : Type := Map MailboxID (Mailbox S M);

AddressBook : Type := Set EngineName;

type EngineEnv S Msg :=
  mkEngineEnv@{
    state : S;
    mailbox : MailboxCluster S Msg;
    acq : AddressBook;
  };

axiom ReturnSomething : Type;

Handler (M S : Type) : Type := M -> EngineEnv S M -> ReturnSomething;

syntax alias TimeTrigger := Nat;

type Effect S E M :=
  | SendMsg@{
      msg : EngineMsg M;
    }
  | UpdateState@{
      state : S;
    }
  | SpawnEngine@{
      engine : E;
    }
  | Chain@{
      effects : List (Effect S E M);
    }
  | Schedule@{
      trigger : TimeTrigger;
      action : Effect S E M;
    };

Guard (S M C R : Type) : Type :=
  EngineMsg M -> EngineEnv S M -> EngineCfg C -> Option R;

isSatisfied
  {S M C R}
  (guard : Guard S M C R)
  (msg : EngineMsg M)
  (env : EngineEnv S M)
  (cfg : EngineCfg C)
  : Bool :=
  case guard msg env cfg of
    | none := false
    | some _ := true;

type GuardStrategy :=
  | FirstGuard
  | LastGuard
  | OneGuard
  | UniqueGuard
  -- checks that it is the only one that is triggered
  | AllGuards;

type GuardEval S M C R :=
  mkGuardEval@{
    guards : List (Guard S M C R);
    strategy : GuardStrategy;
  };

EngineBehaviour (S E M C R : Type) : Type := GuardEval S M C R -> Effect S E M;

type Engine (S E M C R : Type) :=
  mkEngine@{
    status : EngineStatus;
    cfg : EngineCfg C;
    state : EngineEnv S M;
    behavior : EngineBehaviour S E M C R;
  };