emit

Writing a projected protocol out as Gleam source.

pacta/protocol/graph turns a specification into one flattened state graph per participant. This turns a graph into a module a project can compile, which is the step that connects the specification layer to pacta/session/core and pacta/protocol_machine.

Why there is a generator at all

A two-party protocol that runs once can be written by hand as a nested type, and session/core’s markers are built for exactly that. A protocol that repeats cannot: expressing it needs an alias defined in terms of itself, and Gleam rejects that outright. So a repeating protocol has to become a set of named positions with edges between them, and there is no way to write those names down that also tells the compiler what each name stands for.

A generated module says it instead. Each position becomes an uninhabited type, and each position gets one function unfolding it into the session/core shape the protocol says it has:

pub type AtWaiting
pub type AtServing

pub fn at_waiting(
  channel: Channel(AtWaiting, msg),
) -> Channel(core.Recv(String, AtServing), msg) {
  core.unchecked_position(channel)
}

Unfolding is one level deep, and the continuation is the next flat name, so the cycle that defeats the alias never forms. Everything downstream is ordinary: core.receive on the unfolded channel hands back a Channel(AtServing, msg), and protocol_machine.accept takes it just as happily, because what it wants is a Recv and that is what unfolding produced.

What it costs

core.unchecked_position is a hole, and this is the module that needs it. Its own documentation says what the hole is worth; the part that belongs here is that a generated module is the whole reason it is public, and that nothing at the type level distinguishes a generated call from a hand-written one. What makes the generated ones sound is that the shape was read off a graph graph.compile had already checked, and that check is where the guarantee actually lives.

Positions are uninhabited and their unfolding functions are the only way past them, so a channel at a generated position still cannot go anywhere the protocol does not allow. The hole is one function, in one place, and the rest of the surface is as tight as the hand-written one.

Checking rather than writing

review compares what the emitter would write against what is on disk, which is the shape a CI step wants: regenerate, and fail if the result differs from what was committed. It compares content and not layout, so running gleam format over generated files does not make them stale.

Limits

The emitted module contains positions and their unfoldings, and nothing else. It does not pick a gen_statem tag for each position, because how coarse those should be is a decision about the machine rather than about the protocol, and it does not name the wire type, because this layer never sees one. Payload types are the strings the specification carried, resolved by the specification’s imports lines.

Types

Module

</>

One generated module.

name is the Gleam module path, so atm/customer is what an importing module writes and what path turns into a file name. Which source root it sits under is deliberately not decided here: src/ is the answer for a protocol a project ships, and the wrong one for a protocol only its tests use.

pub type Module {
  Module(name: String, source: String)
}

Constructors

```
Module(name: String, source: String)
```

Review

</>

One module, and what its file had to say.

pub type Review {
  Review(module: Module, status: Status)
}

Constructors

```
Review(module: Module, status: Status)
```

Status

</>

What a file on disk says about a module that should have been generated.

pub type Status {
  Current
  Absent
  Different
}

Constructors

```
Current
```
The file is there and says what the emitter would say.
```
Absent
```
There is no file for it.
```
Different
```
The file is there and says something else.

Values

agreed

</>

pub fn agreed(reviews: List(Review)) -> Bool

Whether every reviewed module is current.

describe

</>

pub fn describe(review: Review) -> String

A reviewed module in one line, for a CI step to print.

module

</>

pub fn module(
  protocol: spec.Protocol,
  for role: String,
  under prefix: String,
) -> Result(Module, graph.Error)

Write one participant’s module.

Unlike modules this projects without validating the whole specification first, matching graph.project. Prefer modules unless there is a reason to want one participant in isolation.

modules

</>

pub fn modules(
  protocol: spec.Protocol,
  under prefix: String,
) -> Result(List(Module), graph.Error)

Write every participant’s module.

prefix is a module path the generated modules go under, so a prefix of "myapp/protocols" and a protocol named atm produce myapp/protocols/atm/customer. Pass "" to put them at the root.

The protocol is checked first, so anything graph.compile rejects comes back here rather than being written out.

Example

let assert Ok([customer, teller]) = emit.modules(atm(), under: "banking")
let assert "banking/atm/customer" = customer.name

path

</>

pub fn path(module: Module, in root: String) -> String

Where a module’s file belongs, under a source root.

Example

let assert "src/banking/atm/customer.gleam" = emit.path(customer, in: "src")

review

</>

pub fn review(
  modules: List(Module),
  against read: fn(Module) -> Result(String, Nil),
) -> List(Review)

Compare generated modules against what is already on disk.

read is handed a module and returns the contents of its file, or Error(Nil) if there is no file. Keeping the reading outside means this stays a pure function, and means the caller decides where generated modules live rather than being told.

Comparison ignores layout, so a generated file that has been through gleam format still counts as Current. What it does not ignore is a change in what the module says.

Example

let assert Ok(wanted) = emit.modules(atm(), under: "banking")

let read = fn(module) {
  simplifile.read(emit.path(module, in: "src"))
  |> result.replace_error(Nil)
}

case emit.agreed(emit.review(wanted, against: read)) {
  True -> Ok(Nil)
  False -> Error("protocol modules are out of date, regenerate them")
}