refactor(program): the declaration vocabularies have one home, so a program cannot spell one differently from the file

[FBumann]

Prompt: "Check the latest 4 open issues. CLosable? Otherwise implement them as PRs"

Note

The following content was generated by AI.

program.py derives its four vocabulary Literals from math_spec.model instead of spelling them a second time, the two by=-list claims that had no home here get one in tests/test_parser.py, and the boundary claim #209 offers to decline is declined in writing. Closes #209.

The fourteenth claim: the second home is removed, not fenced

test_architecture.py::test_every_program_vocabulary_matches_the_one_the_language_validates predicted its own end — "the day the program is declared where the vocabularies are, each of these becomes an import". It becomes an import here:

DimensionDtype = _model.DimensionDtype
ParameterDtype = _model.ParameterDtype
VariableAbsence = _model.VariableAbsence
VariableType = _model.VariableDomain

The comment's first option — keep both spellings and add four set(get_args(...)) == set(...) assertions — is the weaker one, and measurably so: typing interns identical Literals, so program.VariableAbsence is model.VariableAbsence was already True on origin/main with the two written out separately. A fence that passes for the wrong reason is not a fence.

What the removal buys, run on both trees with 'semicontinuous' added to model.VariableDomain alone:

tree	get_args(model.VariableDomain)	get_args(program.VariableType)
origin/main	('continuous', 'integer', 'binary', 'semicontinuous')	('continuous', 'binary', 'integer')
this branch	('continuous', 'integer', 'binary', 'semicontinuous')	('continuous', 'integer', 'binary', 'semicontinuous')

(Mutation reverted; the tree here is unmutated.)

The four names stay on math_spec.program's surface — it is the only module math_spec.__all__ exports, so it is where a consumer reaches a vocabulary — and they stay documented assignments rather than a bare re-import, because test_public_surface.py::test_the_program_module_exports_everything_it_defines reads the module's defined names from source and an import is not one. The prose that made each vocabulary make sense moved to model.py, beside the members.

VariableType is still the program's name for VariableDomain. Renaming the field is a separate decision (#157's), not this one.

The eleven claims: where each lives now

Eight were reported as already having homes here, and all eight check out on origin/main:

claim	home
a sum over an undeclared name	test_validation.py an-unknown-name-in-a-constraint, sum-over-typo
by= where the operand lacks over	test_dimensions.py sum-requires-the-grouped-dim
which error a mismatched lookup earns	test_validation.py by-lookup-typo, by-names-a-dimension
a per-entity offset with no edge=	test_dimensions.py::TestTheEdgeRulesAreDecidedAtLoad::test_a_named_offset_with_no_edge_is_refused_by_to_spec
one grouping consumes one dimension	test_validation.py by-lookups-over-different-dimensions
by= onto a dim already carried	test_dimensions.py sum-into-a-dim-the-operand-already-carries

Two did not, and are added here — test_a_list_the_language_cannot_read_is_refused_at_load and test_a_list_is_only_legal_in_a_kwarg_value. Both are grammar claims, so they land in tests/test_parser.py as one table of seven refusals (a trailing comma, an empty list, a missing comma, an unclosed bracket, a list as a positional argument, as a term, and as the whole expression) plus the well-formed by=[a, b] beside it. expression_parser.py states the rule in a docstring and nothing held it.

The remaining five are the shape claims, in #215 (#212).

The two boundary claims, declined

test_a_program_outside_the_language_is_rejected and test_the_eager_lane_holds_every_program_to_the_boundary both hand-built a malformed Program and expected check() to refuse it. #209 says declining is a fine answer if it is written down as one, so it is written down, in program.py's module docstring:

A program is trusted by construction: to_program is the only thing that builds one, and nothing checks one assembled by hand. The language's refusals happen at load, where the file and its author are, and a program put together some other way is outside that guarantee rather than inside a pass restating it.

test_program_check.py, the second of the two deleted modules, covered a consumer verb this package does not have; advice is the verb that crossed, and tests/test_advice.py is its home.

Verification

pixi run ci green (lint, 767 tests, docs-build, compile-tex).

Not done

VariableType → VariableDomain on the program, and the variable_type field with it: one name for one vocabulary is right, and it is a rename downstream sees, so it belongs with #157 rather than smuggled in here.

[read-the-docs-community]

Documentation build overview

📚 math-spec | 🛠️ Build #34275865 | 📁 Comparing 743d0c7 against latest (4fc50e6)

  🔍 Preview build  

3 files changed

± reference/math_spec/advice/index.html
± reference/math_spec/boundedness/index.html
± reference/math_spec/program/index.html