module tutorial.engines.template_messages;

import prelude open;

Template Messages¶

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

Message interface¶

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

Message sequence diagrams¶

ExampleRequest and 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

Message types¶

TemplateMsgJustHi¶

Lorem ipsum dolor sit amet, consectetur adipiscing elit.

ExampleRequest¶

Example request.

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

ExampleReply¶

Reply to an ExampleRequest.

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

type ExampleReplyError :=
  | ExampleErrorOne
  | ExampleErrorTwo;

ExampleReply : Type := Result ExampleReplyError ExampleReplyOk;

TemplateMsg¶

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

Engine components¶

• Template Configuration
• Template Environment
• Template Behaviour