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:

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.
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>}.

Most directives come in three presentations that render the same underlying definition differently: -source emits raw SpecTec source, -latex typesets it as LaTeX math, and -prose generates English. The -source and -latex forms are wrapped in collapsible blocks that only appear in the HTML backend.

Directive type	Key format	What it renders
`syntax`	syntax name	BNF grammar block for that production
`relation-title-{source,latex,prose}`	relation name	Relation signature (declaration only)
`func-title-{source,latex,prose}`	function name	Function signature (declaration only)
`rulegroup-{source,latex,prose}`	`RelName/rulegroup`	A rulegroup (its rules, with premises and conclusion)
`func-{source,latex,prose}`	function name	Full auxiliary function definitions (clauses)
`table-{source,latex,prose}`	table name	A table definition
`rulegroup-dispatch-prose`	`RelName/rulegroup`	Prose for a dispatch rulegroup (prose only)
`rulegroup-prose-else`	`RelName/rulegroup`	Prose for a rulegroup with an `otherwise` rule (prose only)

The -latex presentation renders to an AsciiDoc latexmath block, so the HTML backend needs a math renderer such as MathJax or KaTeX to typeset it (see the worked example below). The two prose-only rulegroup variants have no -source or -latex counterpart; they exist to phrase dispatching and otherwise-style rulegroups in a way the plain rulegroup-prose renderer would not.

A ${syntax: ...} directive accepts multiple space-separated names and emits them all in a single grammar block; the relation-title-*, func-title-*, and table-* directives likewise accept several space-separated names.

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 seven directives: one syntax directive for the grammar, and one source/latex/prose triple 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-latex: Statement_ok/conditionalStatement}
${rulegroup-prose: Statement_ok/conditionalStatement}

=== Runtime Evaluation

${rulegroup-source: Statement_eval/conditionalStatement}
${rulegroup-latex: 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:

Click to view the specification 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-latex directive renders the same rulegroup as a typeset inference rule instead of prose.

Click to view the mathematical definition

\[ {\displaystyle \frac{\begin{array}{r@{\quad}l} {\scriptstyle\mathtt{(1)}} & \mathsf{scope}\,\mathsf{TC} \mathrel{\vdash} \mathsf{expression} : \mathsf{BOOL} \\ {\scriptstyle\mathtt{(2)}} & \mathsf{TC} \mathrel{\vdash} {\mathsf{blockStatement}}_{\mathsf{then}} \\ {\scriptstyle\mathtt{(3)}} & \mathsf{TC} \mathrel{\vdash} {\mathsf{blockStatement}}_{\mathsf{else}} \end{array}}{\mathsf{scope}\,\mathsf{TC} \mathrel{\vdash} \mathsf{IF}\,\left(\mathsf{expression}\right)\,{\mathsf{blockStatement}}_{\mathsf{then}}\,\mathsf{ELSE}\,{\mathsf{blockStatement}}_{\mathsf{else}} \mathrel{\dashv} \mathsf{TC}}} \]

The three numbered premises are the same ones you saw in the source block: the condition must type as BOOL, and each branch must be well-typed. Unlike rulegroup-prose, this presentation takes no prose_in/prose_out hints; it renders straight from the relation’s notation.

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:

scope TC |- IF `( expression `) blockStatement_then ELSE blockStatement_else -| %:

Let scope TC |- expression : typeIR.
Let!_type baseTypeIR be typeIR.
Check that baseTypeIR is BOOL.
If TC |- blockStatement_then holds:
1. If TC |- blockStatement_else holds:
  1. Result in TC.

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:

Typing IF `( expression `) blockStatement_then ELSE blockStatement_else, under context TC at scope:

Let typeIR be the result of typing expression, under context TC at scope.
Let!_type baseTypeIR be typeIR.
Check that baseTypeIR is BOOL.
If blockStatement_then is well-typed under context TC:
1. If blockStatement_else is well-typed under context TC: the result is context TC.

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:

Runtime evaluation of IF `( expression `) blockStatement_then ELSE blockStatement_else, under context EC at scope:

Let value be the result of evaluating expression, under context EC at scope.
If value is equal to true:
1. Let context EC₁ be the result of runtime evaluation of blockStatement_then, under context EC.
2. The result is context EC₁.
Else if value is equal to false:
1. Let context EC₁ be the result of runtime evaluation of blockStatement_else, under context EC.
2. The result is context EC₁.

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.