Generating Prose Specification

The chapters up to this point have walked through every part of the Nano-P4 specification as it lives in .watsup files. P4-SpecTec can do more than run programs against a spec: it can also render the spec into human-readable English prose, formatted as AsciiDoc, ready to be compiled into HTML or PDF. As a concrete example of what the output looks like, the P4-SpecTec team publishes a spliced HTML document generated from the mechanized P4 spec.

This chapter introduces the splice workflow and shows it in action on the Nano-P4 conditional statement.

What Splicing Does

Splicing is a two-step process:

1. You write a skeleton document: a normal AsciiDoc file with special directive placeholders such as ${syntax: conditionalStatement} or ${rulegroup-prose: Statement_eval/conditionalStatement}. These are not AsciiDoc constructs; they are recognized only by P4-SpecTec.
2. You run nano-p4spectec splice, which reads your .watsup spec files, extracts the relevant definitions, and replaces every placeholder in the skeleton with the rendered content.

The result is a complete AsciiDoc document. Compile it with Asciidoctor to produce HTML or PDF.

Directive Reference

Each directive has the form ${<type>: <key>}.

A ${syntax: ...} directive accepts multiple space-separated names and emits them all in a single grammar block.

Running the Splice Command

nano-p4spectec exposes the splice subcommand:

nano-p4spectec splice <spec-files...> -splice <skeleton.adoc> -out <output.adoc>

To splice multiple skeleton files in one pass, repeat -splice/-out pairs as needed:

nano-p4spectec splice nano-p4/spec \
  -splice nano-p4/docs/sections-skeleton/conditional.adoc -out conditional.adoc \
  -splice nano-p4/docs/sections-skeleton/parser.adoc      -out parser.adoc

For Nano-P4, pass the spec files from nano-p4/spec/:

nano-p4spectec splice nano-p4/spec \
  -splice nano-p4/docs/sections-skeleton/conditional-statement.adoc \
  -out conditional-statement-spliced.adoc

A Worked Example: Conditional Statement

Below is a minimal skeleton for the conditional statement section. It uses five directives: one syntax directive for the grammar, and one source/prose pair each for the type-checking and runtime-evaluation rules.

conditional-statement.adoc (skeleton):

[#sec-conditional-statement]
== Conditional Statement

The conditional statement is Nano-P4's sole branching construct. Unlike C or
Java, where any non-zero integer is truthy, P4 (and Nano-P4) require the
condition to be a Boolean expression. Both branches are always required; there
is no optional `else`.

${syntax: conditionalStatement}

=== Type Checking

${rulegroup-source: Statement_ok/conditionalStatement}
${rulegroup-prose: Statement_ok/conditionalStatement}

=== Runtime Evaluation

${rulegroup-source: Statement_eval/conditionalStatement}
${rulegroup-prose: Statement_eval/conditionalStatement}

After running nano-p4spectec splice,

nano-p4spectec splice nano-p4/spec \
  -splice nano-p4/docs/sections-skeleton/conditional-statement.adoc \
  -out conditional-statement-spliced.adoc

each placeholder is replaced. The syntax directive expands to a BNF grammar block:

conditionalStatement
   : IF `( expression ) blockStatement ELSE blockStatement
   ;

The rulegroup-source directive produces a collapsible block (visible only in the HTML backend) showing the raw SpecTec source:

rulegroup Statement_ok/conditionalStatement:
  rule Statement_ok/conditionalStatement:
  scope TC |- IF `( expression `) blockStatement_then ELSE blockStatement_else -| TC
 -- Expr_ok: scope TC |- expression : BOOL
 -- Block_ok: TC |- blockStatement_then
 -- Block_ok: TC |- blockStatement_else

The rulegroup-prose directive produces auto-generated English steps. Without any prose hints on the relations, the output uses raw SpecTec notation in the cross-references:

The cross-references are legible, but the link text is just a rendering of the relation’s notation rather than natural English. The prose_in and prose_out hints on the relation definition control this. For example, adding:

relation Expr_ok:
  scope typingContext |- expression : typeIR
  hint(input %0 %1 %2)
  hint(prose_in "typing" %2#", under context" %1 "at" %0)
  hint(prose_out %3)

tells the renderer how to describe what Expr_ok computes:

• prose_in controls the link text in Let X be the result of <link>[...] steps, replacing the raw SpecTec notation with natural English. The %N placeholders refer to the relation’s arguments by index. The # operator fuses two adjacent pieces without inserting a space between them, so %2#", under context" produces expression, under context rather than expression , under context.
• prose_out names the variable on the left-hand side of Let X be.... With hint(prose_out %3), the renderer picks up typeIR (the fourth argument) and produces Let typeIR be the result of .... For relations whose output is a context, writing hint(prose_out "context" %3) prepends the label, giving Let context EC_1 be... instead of a bare Let EC_1 be.... Without prose_out, the step collapses to a bare Let xref:Expr_ok[...] with no named output variable.

With prose_in/prose_out hints added to Expr_ok, Statement_ok, Block_ok, Expr_eval, Statement_eval, and Block_eval, the prose becomes:

For Block_ok, which is a hold relation (no output), prose_true and prose_false are used instead of prose_in/prose_out:

relation Block_ok:
  typingContext |- blockStatement
  hint(input %0 %1)
  hint(prose_true %1 "is well-typed under context" %0)
  hint(prose_false %1 "is not well-typed under context" %0)

This controls the phrasing of If ... holds branches: prose_true gives the text when the relation holds, prose_false when it does not.

For the runtime evaluation, the output with hints is:

The hints are defined in 5.01-typing-relation.watsup and 8.01-eval-relation.watsup.

This matches the two-rule structure you saw in Section 5.4: evaluate the condition, then dispatch to the appropriate branch.

Generating an HTML Spec File

Once spliced, compile the AsciiDoc output with Asciidoctor:

asciidoctor -o conditional-statement.html conditional-statement-spliced.adoc

For an HTML document that shows the collapsible source blocks, you need the backend-html5 attribute (which Asciidoctor sets by default when targeting HTML5). The ifdef::backend-html5[] guards in the spliced output are resolved at compile time, so they only appear in the HTML output, not in PDF.

The skeleton file lives in the nano-spec repository at nano-p4/docs/sections-skeleton/conditional-statement.adoc. You can reproduce the full HTML output by running:

./nano-p4spectec splice nano-p4/spec \
  -splice nano-p4/docs/sections-skeleton/conditional-statement.adoc \
  -out out/conditional-statement.adoc
asciidoctor -o out/conditional-statement.html out/conditional-statement.adoc

The prose hints used throughout this chapter live on the prose branch of the nano-spec repository. Check out that branch to find the sample spec with the prose annotations already applied to 5.01-typing-relation.watsup and 8.01-eval-relation.watsup.