Text Projection 0.6.0: the operation vocabulary is grammar-directed
Scoping the operation layer surfaced a contradiction the companion had never resolved. `req:textproj:value-projection` is a mechanical rule over structs, enums and newtypes; the Grammar chapter separately spells out `envelope`, `stamp`, `causal`, `payload`, `kind` and their sub-vocabularies. The two disagree. Under the value rule an operation would read `(insert-event (insert-event-op #x0a <event>))`, because an `*Op` record is a named-field struct and so not a transparent newtype. `req:textproj:operation-vocabulary` rules for the grammar, which is what the companion already implied: the value rule's own preamble scopes itself to the values an operation *embeds*, and the `value` nonterminal marks where it applies. If the rule governed the vocabulary too, the grammar's productions would be redundant and partly wrong. An operation kind therefore inlines its payload record, and the requirement says why rather than asserting it: the record exists so each variant can name a type, and the binary form adds no bytes for it -- `OperationKind`'s encoding writes the tag and delegates. A wrapper that adds no bytes adds no text. That is the same argument clause 2 makes for newtype transparency, applied one level out. Also removes a second name for one type. `transpose-interval` inlined its interval as `(interval <d> <c>)` while `TranspositionInterval` projects as `(transposition-interval <d> <c>)` at every `value` position. The production now delegates to `value` and the special case is gone. Two new checker tests lock both, bringing that gate to nine. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This commit is contained in:
parent
b6728da5c6
commit
4ded63a583
|
|
@ -26,6 +26,11 @@
|
|||
//! struct alternative: shape does not distinguish a struct from a sequence,
|
||||
//! and `req:textproj:schema-directed` says so rather than pretending
|
||||
//! otherwise.
|
||||
//! 6. The Chapter 6 operation vocabulary is explicitly grammar-directed, and
|
||||
//! the requirement carrying that boundary is cited at both reliance points.
|
||||
//! 7. `transpose-interval` takes target bytes followed by a `value`; `interval`
|
||||
//! is not allowed to become a grammar production parallel to the canonical
|
||||
//! `TranspositionInterval` value spelling.
|
||||
|
||||
use std::collections::{BTreeSet, VecDeque};
|
||||
|
||||
|
|
@ -297,6 +302,69 @@ fn the_kind_productions_are_the_operation_vocabulary() {
|
|||
);
|
||||
}
|
||||
|
||||
/// The operation grammar is the authority for Chapter 6 vocabulary; the
|
||||
/// mechanical Chapter-5 value rule begins only where a production says `value`.
|
||||
/// The two places that rely on that boundary must cite the requirement rather
|
||||
/// than leaving implementors to infer it from the grammar's shape.
|
||||
#[test]
|
||||
fn the_operation_vocabulary_requirement_is_cited_where_it_applies() {
|
||||
const LABEL: &str = "req:textproj:operation-vocabulary";
|
||||
assert!(
|
||||
SPEC.contains(&format!("\\label{{{LABEL}}}")),
|
||||
"the grammar/value boundary must be a labeled normative requirement"
|
||||
);
|
||||
|
||||
let operation_preamble = grammar()
|
||||
.split_once("; --- Operation kinds")
|
||||
.expect("the grammar introduces its operation kinds")
|
||||
.1
|
||||
.split_once("\nkind")
|
||||
.expect("the operation preamble precedes the `kind` production")
|
||||
.0;
|
||||
assert!(
|
||||
operation_preamble.contains(LABEL),
|
||||
"the operation-kind grammar must cite `{LABEL}` at the point it relies \
|
||||
on the grammar/value boundary"
|
||||
);
|
||||
|
||||
let after_grammar = SPEC
|
||||
.split_once(grammar())
|
||||
.expect("the specification contains the located grammar")
|
||||
.1;
|
||||
let grammar_explanation = after_grammar
|
||||
.split_once("\\chapter{A Worked Example}")
|
||||
.expect("the grammar chapter precedes the worked example")
|
||||
.0;
|
||||
assert!(
|
||||
grammar_explanation.contains(LABEL),
|
||||
"the prose explaining why Chapter-5 field lists are not restated must \
|
||||
cite `{LABEL}`"
|
||||
);
|
||||
}
|
||||
|
||||
/// `TranspositionInterval` is a Chapter-5 value with the canonical
|
||||
/// `(transposition-interval ...)` spelling. Giving `transpose-interval` a second,
|
||||
/// inline `(interval ...)` spelling creates two names for one type; defining an
|
||||
/// `interval` nonterminal merely moves that same special case behind another
|
||||
/// production head.
|
||||
#[test]
|
||||
fn transpose_interval_delegates_to_value_without_an_interval_production() {
|
||||
let kind = uncommented(production_block("kind"))
|
||||
.split_whitespace()
|
||||
.collect::<Vec<_>>()
|
||||
.join(" ");
|
||||
assert!(
|
||||
kind.contains("\"(transpose-interval (\" bytes* \") \" value \")\""),
|
||||
"`transpose-interval` must take target bytes followed by exactly one \
|
||||
Chapter-5 `value`; the `kind` production reads: {kind}"
|
||||
);
|
||||
assert!(
|
||||
!defined(grammar()).contains("interval"),
|
||||
"`interval` must not be a production head: TranspositionInterval uses \
|
||||
the ordinary `value` projection"
|
||||
);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn the_chunk_kind_productions_are_the_chunk_vocabulary() {
|
||||
let expected: BTreeSet<String> = (0u8..=8)
|
||||
|
|
|
|||
Binary file not shown.
|
|
@ -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.5.0 --- The projection is schema-directed, and the grammar says only what shape can say}\\[4pt]
|
||||
{\normalsize\color{epiphanyink}Version 0.6.0 --- The operation vocabulary is grammar-directed; values enter exactly where named}\\[4pt]
|
||||
{\small\color{epiphanyslate}Normative for the text form it defines}
|
||||
\vfill
|
||||
\end{titlepage}
|
||||
|
|
@ -627,6 +627,24 @@ 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:operation-vocabulary}
|
||||
The core specification's Chapter~6 operation vocabulary --- the envelope, its
|
||||
stamp and causal context, the payload, the operation kinds, and their
|
||||
sub-vocabularies --- \MUST{} be projected by the productions of
|
||||
Chapter~\ref{ch:grammar}, not by
|
||||
Requirement~\ref{req:textproj:value-projection}. The value-projection
|
||||
rule governs exactly the \texttt{value} positions those productions contain,
|
||||
and no other positions.
|
||||
|
||||
An operation kind's payload record \MUST{} be inlined into its production. The
|
||||
record exists so each variant can name a type; it is not a modelling
|
||||
distinction, and the binary form agrees: \texttt{OperationKind}'s encoding
|
||||
writes the kind tag and then delegates to the record, adding no bytes for the
|
||||
wrapper. It adds no text here either, for the same reason clause~2 of
|
||||
Requirement~\ref{req:textproj:value-projection} makes a newtype transparent.
|
||||
\end{requirement}
|
||||
|
||||
\begin{requirement}
|
||||
\label{req:textproj:schema-directed}
|
||||
The projection is \textbf{schema-directed}. At every position a reader knows
|
||||
|
|
@ -946,9 +964,11 @@ action ::= "accept-loser" | "keep-winner" | "dismiss"
|
|||
| "(registered " bytes ")"
|
||||
policy ::= "strict-inverse" | "best-effort" | "cascade"
|
||||
|
||||
; --- Operation kinds. Fields are the Operation Catalog's payload schema,
|
||||
; --- positionally, in declaration order. Embedded Chapter-5 values follow
|
||||
; --- req:textproj:value-projection and are written <value> below.
|
||||
; --- Operation kinds inline their payload records as required by
|
||||
; --- req:textproj:operation-vocabulary. Fields are the Operation Catalog's
|
||||
; --- payload schema, positionally, in declaration order. Embedded Chapter-5
|
||||
; --- values occur only at <value> positions and follow
|
||||
; --- req:textproj:value-projection.
|
||||
|
||||
kind ::= "(insert-event " bytes " " value ")"
|
||||
| "(delete-event " bytes " " tuplet-comp ")"
|
||||
|
|
@ -981,8 +1001,7 @@ kind ::= "(insert-event " bytes " " value ")"
|
|||
| "(set-staff-layout " bytes " " option " " option " " bool ")"
|
||||
| "(create-repeat-structure " value ")"
|
||||
| "(delete-repeat-structure " bytes ")"
|
||||
| "(transpose-interval (" bytes* ") (interval " integer
|
||||
" " integer "))"
|
||||
| "(transpose-interval (" bytes* ") " value ")"
|
||||
|
||||
tuplet-comp ::= "not-in-tuplet" | "(replace-with-rest " value ")"
|
||||
| "(rewrite-tuplets (" bytes* "))"
|
||||
|
|
@ -1030,9 +1049,11 @@ derived-but-unwritten, and said so; that gap is closed. Barriers and affected
|
|||
object kinds are byte strings, because the bundle holds them opaquely and the
|
||||
projection interprets nothing the bundle does not.
|
||||
|
||||
The one thing still \emph{read} rather than restated is a Chapter-5 value's field
|
||||
list, and that is deliberate: Requirement~\ref{req:textproj:value-projection} is a
|
||||
rule applied to the core specification's ratified listings, not a copy of them.
|
||||
At exactly the \texttt{value} positions delimited by
|
||||
Requirement~\ref{req:textproj:operation-vocabulary}, the one thing still
|
||||
\emph{read} rather than restated is a Chapter-5 value's field list. That is
|
||||
deliberate: Requirement~\ref{req:textproj:value-projection} is a rule applied to
|
||||
the core specification's ratified listings, not a copy of them.
|
||||
A rule cannot drift from what it reads. An implementation that projects a value's
|
||||
fields in an order other than the declaration order disagrees with the core
|
||||
specification, not with this document.
|
||||
|
|
@ -1061,7 +1082,7 @@ fifth, over a compacted base and one embedded image --- projects to six lines:
|
|||
(profile full (0 1 0) (constraints 67108864 (retention 1 () true)))
|
||||
(canonical-base #x1f8b... #x00 1 full (schema 0 1) #x0000...)
|
||||
(blob "image/png" () #x89504e47...)
|
||||
(envelope #x00000000000000070000000000000001 #x00000000000000000000000011223344 (stamp 42 7 #x00000000000000070000000000000001) (causal ((#x0000000000000001 3)) (#x00000000000000020000000000000009)) (some #x00000000000000070000000000000005) (primitive (transpose-interval (#x00000000000000070000000000000001 #x00000000000000070000000000000002) (interval 4 7))))
|
||||
(envelope #x00000000000000070000000000000001 #x00000000000000000000000011223344 (stamp 42 7 #x00000000000000070000000000000001) (causal ((#x0000000000000001 3)) (#x00000000000000020000000000000009)) (some #x00000000000000070000000000000005) (primitive (transpose-interval (#x00000000000000070000000000000001 #x00000000000000070000000000000002) (transposition-interval 4 7))))
|
||||
\end{lstlisting}
|
||||
|
||||
The envelope's targets are a \emph{set}: strictly increasing, no duplicates
|
||||
|
|
@ -1212,6 +1233,21 @@ absorb it, exactly as the binary decoder does.
|
|||
\texttt{"(transpose (" bytes* ") "} spelled two targets as one run of hex.
|
||||
|
||||
Still no implementation; this is what the first day of writing it found. \\
|
||||
\today & Chapters 3, 5, 6 & 0.6.0 --- The operation vocabulary is
|
||||
grammar-directed, and the boundary is now normative
|
||||
(\texttt{req:textproj:operation-vocabulary}). The envelope, stamp, causal
|
||||
context, payload, operation kinds, and their sub-vocabularies follow the
|
||||
grammar's productions; \texttt{req:textproj:value-projection} applies exactly
|
||||
at the \texttt{value} positions those productions name. Operation-kind payload
|
||||
records are inlined because they name variant types but add neither a binary
|
||||
wrapper nor a modelling distinction.
|
||||
|
||||
\texttt{transpose-interval} now takes its target byte strings followed by one
|
||||
\texttt{value}. Its \texttt{TranspositionInterval} therefore has the same
|
||||
\texttt{(transposition-interval ...)} spelling it has at every other value
|
||||
position, and the grammar has no special \texttt{interval} production. The
|
||||
committed grammar gate locks the requirement, its reliance-point citations,
|
||||
and that absence. \\
|
||||
\bottomrule
|
||||
\end{longtable}
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue