module tutorial.engines.template_messages;

import prelude open;

Template Messages¶

These are the messages that the Template engine can receive/respond to.

Message interface¶

TemplateMsgJustHi¶

Lorem ipsum dolor sit amet, consectetur adipiscing elit.

TemplateMsgExampleRequest ExampleRequest¶

Example request.

type ExampleRequest : Type :=
  mkExampleRequest@{
    argOne : Nat;
    argTwo : Nat;
  };

TemplateMsgExampleReply ExampleReply¶

Reply to an ExampleRequest.

ExampleReplyOk¶

Example OK reply.

type ExampleReplyOk : Type := mkExampleReplyOk@{argOne : Nat};

ExampleReplyError¶

Example error reply.

type ExampleReplyError : Type :=
  | ExampleErrorOne
  | ExampleErrorTwo;

ExampleReply¶

ExampleReply : Type := Result ExampleReplyError ExampleReplyOk;

TemplateMsg¶

type TemplateMsg :=
  | TemplateMsgJustHi
  | TemplateMsgExampleRequest ExampleRequest
  | TemplateMsgExampleReply ExampleReply;

Sequence Diagrams¶

ExampleRequest & ExampleReply¶

Lorem ipsum dolor sit amet, consectetur adipiscing elit. Sed ut purus eget sapien. Nulla facilisi.

sequenceDiagram
    participant TemplateClient
    participant Template

    TemplateClient ->> Template: ExampleRequest
    Template ->> TemplateClient: ExampleReplyOk

    TemplateClient ->> Template: ExampleRequest
    Template ->> TemplateClient: ExampleReplyErrorOne