Formal grammar

This is the canonical formal specification of Carve. It is layered because no single grammar notation can express indentation, fence matching, document-wide resolution and canonical writing together.

Layer	Content	Formalism
PART 0	Line layout: indentation, container prefixes, lazy continuation	Machine-readable transition table plus deterministic line algorithm
PARTS 1-8	Block and inline productions	EBNF + declared guard notation (lookahead, lookbehind classes, where counting guards)
PART 9	Semantic constraints a context-free production cannot carry	Operational semantics, with interruption and ownership tables published as data
PART 9R	Whole-document resolution (references, footnotes, crossrefs, numbering)	Two-pass rules over declared symbol tables
PART 10	HTML serialization	Tree-transform conventions
PART 11	Canonical source writer (carve fmt): round-trip invariants and the escaping rule	Invariants over parse/fmt + a decision procedure
PART 12	AST serialization: the JSON shape a parsed document exchanges as	Reference-implementation field names + a round-trip invariant

Why layers instead of one grammar?

Some Carve constraints are not expressible in context-free EBNF. Structured tables cover closed state transitions and capability matrices; operational clauses cover the remaining algorithms.

Specification sources

The editable normative sources are split by processing phase under resources/spec/. The modules follow the processing pipeline:

Source	Responsibility
00-preamble.ebnf	Notation, precedence and normativity
01-layout.ebnf	Input normalization and layout automaton
02-document.ebnf to 12-precedence.ebnf	Document, block, inline and lexical productions
13-semantics-foundations.ebnf to 17-semantics-unicode-controls.ebnf	Operational semantics, split by concern
18-resolution.ebnf	Whole-document resolution
19-html-serialization.ebnf	HTML serialization
20-writer-invariants.ebnf to 22-writer-targets.ebnf	Canonical and non-HTML writers
23-ast-foundations.ebnf to 25-ast-extensions.ebnf	AST wire contract

resources/grammar.ebnf is generated by concatenating those modules. It remains available for tools that require one file, but it is not edited directly.

The adjacent structured artifacts make closed rule sets inspectable without parsing English prose:

• layout-transitions.json defines every ownership boundary transition.
• paragraph-interruption.json partitions interrupting and non-interrupting constructs.
• target-capabilities.json records cross-target preservation behavior.
• rules.json assigns stable identifiers and an implementation scope to every normative clause. The generated normative rule index provides focused views without making any rule optional.

Run npm run spec:check and npm run spec:rules:check after editing the specification.

Executable checks

Three derived artifacts execute the core specification:

Spec layer	Executable artifact
PART 0 layout automaton + list/quote structure	scripts/spec/layout.mjs
PART 3 inline grammar	resources/carve-core.ohm (Ohm/PEG)
PART 9R resolution + PART 10 serialization	scripts/spec/html.mjs

npm run core:check
npm run grammar:reach

core:check compares the derived pipeline with every reviewed corpus pair. grammar:reach checks that the corpus exercises every reachable production and pins the remainder in resources/grammar-corpus-coverage.txt, which fails both on a newly unreached production and on a stale entry a new document now covers. These tools expose disagreements; they do not override normative clauses. The review policy for clauses, checkers, and generated goldens lives in CONTRIBUTING.md.

Implementations should match this grammar. The case study explains the design rationale, the parsing ambiguities page covers parsing edge cases, and the examples show the expected HTML output for each construct.

The generated single-file grammar remains available at resources/grammar.ebnf. It is intentionally not embedded into this page: the aggregate is a generated tool input, not a readable introduction.