diff --git a/crates/epiphany-testkit/DECISIONS.md b/crates/epiphany-testkit/DECISIONS.md index fc6e6bb..9cd041f 100644 --- a/crates/epiphany-testkit/DECISIONS.md +++ b/crates/epiphany-testkit/DECISIONS.md @@ -317,3 +317,38 @@ specifies a text syntax must not misprint that syntax. from its `\setmonofont`, which makes this the house convention rather than a new one; the three companions that still enable it have no listing content the feature would touch. + +### 0.5.0: what starting the implementation found + +The grammar could not derive an ordinary pitched note. `value` had **no +alternative for a sequence**, though `req:textproj:value-projection` clause 5 +required one. Adding it exposed why it had been missing: a sequence whose first +element is a fieldless variant is *shape-identical* to a struct, and `()` is both +the empty sequence and the absent option. Both collisions are reachable from the +first pitched note in any score — `PitchedEvent` carries `articulations` and +`ornaments` (sequences over the zero-field `ArticulationMark` / `OrnamentMark`) +beside an optional `DynamicMark`. + +**The collision is irreducible without new syntax, and new syntax buys nothing.** +`req:textproj:strict-parse` already obliges a parser to reject "a duplicate in a +set-typed field" — which it cannot do without knowing the field is set-typed. A +parser consults the schema either way. Spending `(seq …)` or `[…]` to remove a +*shape* ambiguity, while leaving the schema dependency that syntax was meant to +remove, lengthens every line and simplifies no tool. **User ratified +schema-directed** (`req:textproj:schema-directed`), so `value` collapses to +`"(" value* ")"` or a leaf — all that shape can honestly say — and the +requirement assigns meaning by expected type. + +Three consequences, now stated: a struct with no fields is the bare symbol, as a +fieldless variant is; a **byte string is not a sequence** (where the binary form +writes a length-prefixed run of bytes — an opaque extension payload, a +`SoundConfiguration` — the projection writes a byte string, never a list of +integers); and the grammar's repetitions carry a notation rule, adjacent elements +separated by exactly one space, without which `"(transpose (" bytes* ") "` spelled +two targets as one undelimited run of hex. + +The checker gained `value_admits_a_bare_list_and_claims_no_shape_it_cannot_distinguish`, +mutation-verified two ways: restoring the 0.4.0 `value` production, and stripping +the `schema-directed` citations. A grammar that claims to distinguish a struct +from a sequence would be lying, so the test asserts the symbol-headed alternative +is **absent**. diff --git a/crates/epiphany-testkit/tests/text_projection_grammar.rs b/crates/epiphany-testkit/tests/text_projection_grammar.rs index 6407daf..aa941e8 100644 --- a/crates/epiphany-testkit/tests/text_projection_grammar.rs +++ b/crates/epiphany-testkit/tests/text_projection_grammar.rs @@ -19,6 +19,12 @@ //! 4. The escape rule excludes the four codepoints //! `req:textproj:string-escapes` requires a writer to escape — the //! contradiction that 0.4.0 fixed. +//! 5. `value` admits a bare parenthesised list. Without it the grammar cannot +//! derive a sequence, so it cannot derive an ordinary pitched note — the +//! omission 0.5.0 fixed. And it must *not* re-introduce a symbol-headed +//! struct alternative: shape does not distinguish a struct from a sequence, +//! and `req:textproj:schema-directed` says so rather than pretending +//! otherwise. use std::collections::{BTreeSet, VecDeque}; @@ -413,6 +419,42 @@ fn the_escape_grammar_agrees_with_the_escape_requirement() { ); } +/// `value` must admit a bare parenthesised list, or the grammar cannot derive any +/// sequence — a `PitchedEvent`'s `articulations` among them, which makes an +/// ordinary `insert-event` line underivable. It must equally *not* carry a +/// symbol-headed struct alternative: a sequence whose first element is a fieldless +/// variant has exactly that shape, so a grammar claiming to tell them apart would +/// be lying. `req:textproj:schema-directed` carries the distinction instead. +#[test] +fn value_admits_a_bare_list_and_claims_no_shape_it_cannot_distinguish() { + let block = uncommented(production_block("value")); + let alts: Vec = block + .split('|') + .map(|a| a.split_whitespace().collect::>().join(" ")) + .collect(); + + assert!( + alts.iter().any(|a| a == "\"(\" value* \")\""), + "`value` must admit a bare parenthesised list, else no sequence is \ + derivable; alternatives were {alts:?}" + ); + assert!( + !alts.iter().any(|a| a.contains("symbol \" \" value*")), + "`value` must not claim to distinguish a struct from a sequence by shape; \ + alternatives were {alts:?}" + ); + + // The requirement that carries the distinction must exist and be cited where + // it is relied on: the value rule, the strict-parse rule, and the grammar. + assert!(SPEC.contains("\\label{req:textproj:schema-directed}")); + let citations = SPEC.matches("req:textproj:schema-directed").count(); + assert!( + citations >= 4, + "expected the label plus citations from the value rule, strict parsing \ + and the grammar; found {citations}" + ); +} + /// The mono font must not apply TeX ligatures. `tlig` rewrites `\"` as a right /// curly quote and `--` as an en dash, so the grammar -- which delimits terminals /// with U+0022 and builds escapes from U+005C -- would render characters other diff --git a/spec/text_projection.pdf b/spec/text_projection.pdf index 51e57f5..c6af7fd 100644 Binary files a/spec/text_projection.pdf and b/spec/text_projection.pdf differ diff --git a/spec/text_projection.tex b/spec/text_projection.tex index ccccb8d..35cb8d3 100644 --- a/spec/text_projection.tex +++ b/spec/text_projection.tex @@ -229,7 +229,7 @@ {\Large\scshape\color{epiphanyslate}Text Projection}\\[6pt] {\large\itshape\color{epiphanyslate}A companion to the Core Specification}\\[14pt] {\color{epiphanygold}\rule{3in}{0.8pt}}\\[24pt] - {\normalsize\color{epiphanyink}Version 0.4.0 --- Derived ordering, and an escape grammar that matches its requirement}\\[4pt] + {\normalsize\color{epiphanyink}Version 0.5.0 --- The projection is schema-directed, and the grammar says only what shape can say}\\[4pt] {\small\color{epiphanyslate}Normative for the text form it defines} \vfill \end{titlepage} @@ -627,6 +627,50 @@ Chapter~5 --- an \texttt{Event}, a \texttt{Pitch}, a \texttt{Region}, a states one rule for turning any of them into text, and the shapes stay where they are ratified. +\begin{requirement} + \label{req:textproj:schema-directed} + The projection is \textbf{schema-directed}. At every position a reader knows + the type it expects, from the ratified schema and from the position itself, + exactly as the binary decoder does. The grammar of + Chapter~\ref{ch:grammar} describes the \emph{shape} of the text; it is not a + standalone unambiguous language, and a reader \MUSTNOT{} attempt to recover a + value's type from its shape. + + Three consequences follow, and a reader resolves each by the type it expects: + + \begin{itemize} + \item \texttt{()} is the empty sequence, and it is the absent option. + \item A bare symbol is a fieldless variant, and it is a struct with no + fields. + \item A parenthesised list whose first element is a symbol is a struct, and + it is a sequence whose first element is a symbol. + \end{itemize} +\end{requirement} + +\begin{rationale} + This states what the ratified rules already require rather than adding a new + constraint. A struct is \texttt{( \ldots)} and a sequence is + a parenthesised list of its elements; a sequence whose first element is a + fieldless variant is therefore shape-identical to a struct. The collision is + \emph{irreducible} without new syntax, and it is reachable from the first + pitched note a score contains: a \texttt{PitchedEvent} carries + \texttt{articulations} and \texttt{ornaments}, sequences of a zero-field + \texttt{ArticulationMark} and \texttt{OrnamentMark}, alongside an optional + \texttt{DynamicMark} --- so one \texttt{insert-event} line holds an empty + sequence and an absent option, both spelled \texttt{()}, and a two-element + sequence spelled like a two-field struct. + + Making the text standalone-unambiguous would buy nothing, because + Requirement~\ref{req:textproj:strict-parse} already obliges a parser to reject + ``a duplicate in a set-typed field'' --- which it cannot do without knowing that + the field is set-typed. The parser consults the schema either way. Spending + syntax to remove a shape ambiguity, while leaving the schema dependency it was + meant to remove, would make every line longer and no tool simpler. + + The binary form is schema-directed for the same reason and pays the same price: + its bytes do not say what they are either. +\end{rationale} + \begin{requirement} \label{req:textproj:value-projection} A canonical value is projected thus: @@ -636,7 +680,9 @@ are ratified. the type name is the core specification's name in lower-case hyphenated form and the fields appear \emph{positionally}, in the order that specification's ratified listing declares them. Field names are not - written. + written. A struct with \emph{no} fields is the bare symbol + \texttt{}, as a fieldless variant is; it encodes to no bytes in + the binary form and carries no value here. \item A \textbf{newtype} --- a struct of exactly one unnamed field --- is projected as that field alone, with no wrapper. This mirrors the binary form, in which a newtype delegates to its field and adds no bytes. @@ -648,10 +694,17 @@ are ratified. \item A \textbf{sequence}, \textbf{set}, or \textbf{map} is a parenthesised list of its elements, \emph{in the order the binary form writes them}, except where Requirement~\ref{req:textproj:derived-ordering} applies; a - map entry is \texttt{( )}. The projection invents no ordering - of its own, and a set that the binary form writes strictly increasing is - written strictly increasing here + map entry is \texttt{( )}. An empty one is \texttt{()}, which + Requirement~\ref{req:textproj:schema-directed} distinguishes from an absent + option by the expected type. The projection invents no ordering of its own, + and a set that the binary form writes strictly increasing is written + strictly increasing here (Requirement~\ref{req:textproj:strict-parse}). + + A \textbf{byte string} is not a sequence. Where the binary form writes a + length-prefixed run of bytes rather than a counted sequence of elements --- + an opaque extension payload, a \texttt{SoundConfiguration} --- the + projection writes a byte string, not a list of integers. \item \textbf{Leaves.} An identifier or hash is a byte string. An integer is an integer. A boolean is \texttt{true} or \texttt{false}. Canonical text is a quoted string. A rational is \texttt{(ratio )}, @@ -804,6 +857,10 @@ are ratified. Accepting non-canonical text and normalizing it \emph{is} accepting it, and does not satisfy this requirement. + + Rejecting a duplicate in a set-typed field requires knowing that the field is + set-typed. A parser therefore reads the schema + (Requirement~\ref{req:textproj:schema-directed}); shape alone never suffices. \end{requirement} \begin{rationale} @@ -834,6 +891,12 @@ are ratified. \label{ch:grammar} \begin{lstlisting} +; Notation. X* is zero or more X, X? is zero or one. Within a line, adjacent +; elements of a repetition are separated by exactly one U+0020, and an empty +; repetition contributes nothing -- so "(" value* ")" spells () when empty. The +; line productions below carry their own trailing LF, and are simply +; concatenated. LF is U+000A. Terminals are quoted; U+XXXX names a codepoint. + projection ::= header document lineage? profile* extension* canonical-base? blob* envelope* @@ -931,7 +994,10 @@ reassign-entry ::= "(" bytes " " ratio ")" ; event id, musical position ; --- Values and leaves. -value ::= "(" symbol " " value* ")" ; req:textproj:value-projection +; A struct, a sequence, a set, a map and an option all have this one shape. The +; reader tells them apart by the type it expects, never by the shape: +; req:textproj:schema-directed. Meaning is req:textproj:value-projection. +value ::= "(" value* ")" | symbol | bytes | integer | bool | string | ratio | option option ::= "()" | "(some " value ")" ratio ::= "(ratio " integer " " integer ")" @@ -1120,6 +1186,32 @@ absorb it, exactly as the binary decoder does. name; the checks it replaced were anchored to a column, and a reflow would have silently switched them off. The 0.3.0 claim of a ``machine-checked'' grammar was true of one run and of nothing durable. Still no implementation. \\ + \today & Chapters 3, 5 & 0.5.0 --- Found by starting the implementation: the + grammar could not derive an ordinary pitched note. + + \emph{The projection is schema-directed} + (\texttt{req:textproj:schema-directed}), and now says so. \texttt{value} had no + alternative for a sequence at all, though clause~5 required one; and once + added, a sequence whose first element is a fieldless variant is + shape-identical to a struct, while \texttt{()} is both the empty sequence and + the absent option. Both collisions are reachable from the first pitched note in + any score --- \texttt{PitchedEvent} carries \texttt{articulations} and + \texttt{ornaments} over zero-field marks, beside an optional + \texttt{DynamicMark}. The collision is irreducible without new syntax, and new + syntax would buy nothing: + \texttt{req:textproj:strict-parse} already obliges a parser to reject a + duplicate in a set-typed field, which it cannot do without the schema. So + \texttt{value} now collapses to \texttt{"(" value* ")"} or a leaf --- all shape + can honestly say --- and the requirement assigns meaning by expected type. + + \emph{Three consequences, stated.} A struct with no fields is the bare symbol, + as a fieldless variant is. A byte string is not a sequence: where the binary + form writes a length-prefixed run of bytes, so does the projection, never a + list of integers. And the grammar's repetitions now carry a notation rule --- + adjacent elements are separated by exactly one space --- without which + \texttt{"(transpose (" bytes* ") "} spelled two targets as one run of hex. + + Still no implementation; this is what the first day of writing it found. \\ \bottomrule \end{longtable}