From 3f5d717ec3da51c700ff85d21f8a03d66015ed5e Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 16 Sep 2026 21:21:07 +0000 Subject: [PATCH] feat(language): math can be layered onto a model built elsewhere MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A layer reads what another model holds and adds math of its own. It reads a column through `given_variables:`, which #507 added, and now the dual of a row family through `given_constraints:` — a frame and nothing else, because the body is the owner's and a sense written here would be a claim no file could check. `dual(balance)` is the only place one may be named, and the frame is what gives the reported expression its dimensions. The program carries both groups, apart from the ones it builds. That is the distinction a builder needs and nothing else can supply: `variables` is a column to create, `given_variables` is a column to bind. Creating one instead of binding it would be a second column nothing else refers to, in a model that solves and is wrong. `reading.md` states the three things a consumer owes them: bind each name, check the frame, and refuse what it cannot bind. So `to_program` no longer refuses a file that reads what it does not build. That rule fitted a library, where `merge` folds each given declaration into the file that introduces it; a layer has nothing to fold into. What replaces it is a note from `advice`, under a third kind, naming each declaration a consumer has to bind. The two tests that asserted the refusal now asserts what the program carries instead. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01CA5v9XJvgYViUHP7hSiKPU --- docs/about/limits.md | 11 +- docs/howto/compose.md | 6 +- docs/reference/language/declarations.md | 41 ++++- docs/reference/language/file.md | 4 +- docs/reference/language/index.md | 2 +- docs/reference/language/reading.md | 38 ++++ schema/math-spec.schema.json | 40 +++- src/math_spec/advice.py | 31 +++- src/math_spec/composition.py | 2 +- src/math_spec/dimensions.py | 2 +- src/math_spec/errors.py | 2 +- src/math_spec/lowering.py | 34 +--- src/math_spec/model.py | 35 +++- src/math_spec/program.py | 23 +++ src/math_spec/resolution.py | 5 +- src/math_spec/typesetting/symbols.py | 3 +- src/math_spec/typesetting/walk.py | 7 + tests/test_advice.py | 23 ++- tests/test_given.py | 235 ++++++++++++++++++++++++ tests/test_given_variables.py | 127 ------------- tests/test_reading_page.py | 2 +- 21 files changed, 492 insertions(+), 181 deletions(-) create mode 100644 tests/test_given.py delete mode 100644 tests/test_given_variables.py diff --git a/docs/about/limits.md b/docs/about/limits.md index b487646b..39f7f6f1 100644 --- a/docs/about/limits.md +++ b/docs/about/limits.md @@ -199,8 +199,15 @@ A template reads the coupling surface it is written against, and declares that column under `given_variables:`. So a template loads on its own, and prints as math on its own, which is what it could not do while a fragment was a file the loader had to refuse. `merge` folds each given declaration into the one that -introduces it, and a program carries none of them: a build makes every column it -holds. +introduces it, so a composed library carries none. + +A layer over a model this language never sees — one built through linopy, say — +has nothing to fold into. There the declaration stays, and the program carries +the name and the frame for a consumer to bind, under +[what a program does not build](../reference/language/reading.md#what-a-program-does-not-build). +`given_constraints:` is the same fact about a row family: `dual(balance)` prices +what the base model settles, and the file says how many duals there are and what +indexes them. The verb is built to collide, so every collision the caller did not ask for is refused. An entry naming some fields of a declaration the base does not have is diff --git a/docs/howto/compose.md b/docs/howto/compose.md index bbac34bd..4d152430 100644 --- a/docs/howto/compose.md +++ b/docs/howto/compose.md @@ -62,9 +62,9 @@ compose: `override(merge({…}), {…})`. expression: sum(gen_p * gen_cost) ``` - The template loads on its own, and it prints as math on its own. What it - cannot do is lower: a program builds every column it carries, and this file - says the opposite about `flow`. + The template loads on its own, and it prints as math on its own. Lowering + it gives a program that names `flow` as a column to bind rather than build, + which is what a layer over another model wants; a library merges instead. 3. **Merge the templates you need.** Each fragment is given a name, and that name is what a refusal calls it. diff --git a/docs/reference/language/declarations.md b/docs/reference/language/declarations.md index 857a0172..9d87d250 100644 --- a/docs/reference/language/declarations.md +++ b/docs/reference/language/declarations.md @@ -152,18 +152,43 @@ An expression reads a given variable as it reads any other, so `at(flow, by=gen_port)` lands on the generator frame and the dim algebra checks it at load. -**A file with a `given_variables` block does not lower.** A program builds -every column it carries, and this file says the opposite about one of its own: - -```text -this file reads a variable it does not introduce: 'flow'. A program builds every column it carries, so compose the file with the ones that declare them first — to_program(merge({...})). The file loads and prints on its own either way. -``` - [`merge`](../../howto/compose.md) folds each given declaration into the -declaration that introduces it, so a composed model carries none of them. The +declaration that introduces it, so a composed library carries none of them. The folded declaration is the introducer's, and what the reader stated has to agree with it. +Where nothing in this language introduces the column — a layer over a model +built in Python — the declaration stays, and the program carries it for a +consumer to bind. See +[what a program does not build](reading.md#what-a-program-does-not-build). + +## `given_constraints` + +A given constraint is a row family this file reads the dual of and another +model builds. It is what lets a layer price something the base model settles. + +```yaml +given_constraints: + balance: + dims: [snapshot, bus] + description: the host model clears each bus +expressions: + price: + expression: dual(balance) +``` + +| Field | | | +| ------------- | ------------------------------------------------- | -------------- | +| `dims` | required. The dimensions the row family runs over | | +| `description` | free text | default `null` | + +There is no `expression`, because nothing here builds the row, and no `sense`. +The dual comes back from whoever solved the model, under that model's own +convention, and a sense written here would be a claim no file could check. + +`dual(name)` is the only place a given row family may be named, and the frame +is what gives the reported expression its dimensions. + ## `constraints` One block is one rule. The name of the block is the name of the constraint, and diff --git a/docs/reference/language/file.md b/docs/reference/language/file.md index 25b951aa..fe2ab7c7 100644 --- a/docs/reference/language/file.md +++ b/docs/reference/language/file.md @@ -5,8 +5,8 @@ SPDX-License-Identifier: CC-BY-4.0 # File shape -A model file is a YAML mapping with **eleven declaration keys**, plus -`version` and `description`. Any subset of the eleven is accepted. +A model file is a YAML mapping with **twelve declaration keys**, plus +`version` and `description`. Any subset of the twelve is accepted. | Key | | | ----------------- | ------------------------------------------------------------------------------------------------------------------- | diff --git a/docs/reference/language/index.md b/docs/reference/language/index.md index d9576803..a7afd034 100644 --- a/docs/reference/language/index.md +++ b/docs/reference/language/index.md @@ -46,7 +46,7 @@ message that names the fix. These ten rules are what it checks. | # | Rule | | | --- | ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | --------------------------------------------------------------- | -| 1 | A file has eleven declaration keys, plus `version` and `description`. A key the schema does not know is refused, with the nearest valid key named: `boundz` → `bounds`. | [File shape](file.md) | +| 1 | A file has twelve declaration keys, plus `version` and `description`. A key the schema does not know is refused, with the nearest valid key named: `boundz` → `bounds`. | [File shape](file.md) | | 2 | Everything that can be checked without data is checked when the file loads. | [Errors](errors.md) | | 3 | Every name is declared once. A parameter and a dimension both called `snapshot` is refused, and the message names both lines. | [Names](expressions.md#name-resolution) | | 4 | Where a name may stand depends on what it is. A dimension may follow `over=` or `along=`, and may not be multiplied: `dispatch * snapshot` is refused, because `snapshot` is an axis and not a column of numbers. | [Names](expressions.md#name-resolution) | diff --git a/docs/reference/language/reading.md b/docs/reference/language/reading.md index d546b5ff..795e8b4e 100644 --- a/docs/reference/language/reading.md +++ b/docs/reference/language/reading.md @@ -116,6 +116,44 @@ tree, so a boolean literal stands at a mask's root or nowhere. A tree with an unresolved leaf is refused. A `Region`'s `when` arrives as a `Mask` too. The node classes live in `math_spec.program`. +## What a program does not build + +`program.given_variables` and `program.given_constraints` name what the model +reads and does not build. Every other group is a build instruction — a column +for each entry of `variables`, a row family for each entry of `constraints`. +These two are the opposite: a name to look up in the model this one is layered +onto. + +```python +layer = to_program( + { + 'dimensions': {'snapshot': {'dtype': 'int'}, 'bus': {'dtype': 'str'}}, + 'given_variables': {'p': {'dims': ['snapshot', 'bus']}}, + 'given_constraints': {'balance': {'dims': ['snapshot', 'bus']}}, + 'parameters': {'rate': {'dims': ['bus']}}, + 'constraints': {'cap': {'dims': [], 'expression': 'sum(p * rate) <= 100'}}, + 'expressions': {'price': {'expression': 'dual(balance)'}}, + } +) + +sorted(layer.variables) # [] +sorted(layer.given_variables) # ['p'] +layer.given_constraints['balance'].dims # ('snapshot', 'bus') +``` + +A consumer that builds a program does three things with them: + +1. **Bind each name** to a column or a row family the host model already holds. +2. **Check the frame.** `dims` is what the file claims about the shape, and it + is the one claim a binder can settle. +3. **Refuse what it cannot bind, and name it.** Building a column of its own + instead would be a second column nothing else refers to, and the model would + solve and be wrong. + +A consumer with no host to bind against refuses a program whose two groups are +not both empty. [`merge`](../../howto/compose.md) is what empties them wherever +a file in this language introduces the declaration. + ## Asking what a program uses `program.footprint` says which of the language's constructs one model uses. It diff --git a/schema/math-spec.schema.json b/schema/math-spec.schema.json index 33e30974..dc4f1473 100644 --- a/schema/math-spec.schema.json +++ b/schema/math-spec.schema.json @@ -216,6 +216,36 @@ "title": "ExpressionCase", "type": "object" }, + "GivenConstraintBlock": { + "additionalProperties": false, + "description": "A row family this file reads the dual of and does not build.\n\nThe frame says how many duals there are and what indexes them, which is\nwhat ``dual()`` needs and all this file can answer. There is no\n``expression:``: the body is the owner's, and nothing here builds a row.", + "properties": { + "description": { + "anyOf": [ + { + "type": "string" + }, + { + "type": "null" + } + ], + "default": null, + "title": "Description" + }, + "dims": { + "items": { + "type": "string" + }, + "title": "Dims", + "type": "array" + } + }, + "required": [ + "dims" + ], + "title": "GivenConstraintBlock", + "type": "object" + }, "GivenVariableBlock": { "additionalProperties": false, "description": "A variable this file reads and does not introduce.\n\nThe frame is what every load-time pass asks of a variable, and it is all\nthis file can answer: whoever introduces the column owns its bounds and its\nmask, and a second spelling of either here would be a second home for one\nfact. :func:`~math_spec.composition.merge` folds the declaration into the\none that introduces it, so a composed model carries none of these.", @@ -676,7 +706,7 @@ }, "$schema": "https://json-schema.org/draft/2020-12/schema", "additionalProperties": false, - "description": "The declared math \u2014 one YAML file, or one dict, validated. Nothing here has seen data.\n\nA ``Spec`` that exists has passed the whole language: constructing one by\nany route \u2014 ``to_spec``, :meth:`model_validate`, the constructor \u2014 runs\nevery load-time check, expansion and expression pass included, and raises\n:class:`~math_spec.errors.LanguageError` on a model the language refuses.\nHolding one is the proof, so nothing downstream checks it again.\n\nThe API is the eleven declaration sections plus ``version`` and\n``description``, and two ways back out: :meth:`to_dict` for the model as\ndata, :meth:`to_yaml` for the file a reviewer reads. Everything else on\nthis class is pydantic's, not a contract this package keeps.", + "description": "The declared math \u2014 one YAML file, or one dict, validated. Nothing here has seen data.\n\nA ``Spec`` that exists has passed the whole language: constructing one by\nany route \u2014 ``to_spec``, :meth:`model_validate`, the constructor \u2014 runs\nevery load-time check, expansion and expression pass included, and raises\n:class:`~math_spec.errors.LanguageError` on a model the language refuses.\nHolding one is the proof, so nothing downstream checks it again.\n\nThe API is the twelve declaration sections plus ``version`` and\n``description``, and two ways back out: :meth:`to_dict` for the model as\ndata, :meth:`to_yaml` for the file a reviewer reads. Everything else on\nthis class is pydantic's, not a contract this package keeps.", "properties": { "constraints": { "additionalProperties": { @@ -714,6 +744,14 @@ "title": "Expressions", "type": "object" }, + "given_constraints": { + "additionalProperties": { + "$ref": "#/$defs/GivenConstraintBlock" + }, + "default": {}, + "title": "Given Constraints", + "type": "object" + }, "given_variables": { "additionalProperties": { "$ref": "#/$defs/GivenVariableBlock" diff --git a/src/math_spec/advice.py b/src/math_spec/advice.py index 910478db..7f119e68 100644 --- a/src/math_spec/advice.py +++ b/src/math_spec/advice.py @@ -33,11 +33,34 @@ def advice(model: str | Path | dict[str, Any] | Spec | Program) -> tuple[Advice, answer alike. Returns: - The never-an-axis advice in declaration order, then the unboundedness - advice; ``str()`` of each is its sentence. + The never-an-axis advice in declaration order, then what the model + reads and does not build, then the unboundedness advice; ``str()`` of + each is its sentence. """ program = to_program(model) - return tuple(_never_an_axis(program) + unbounded_notes(program)) + return tuple(_never_an_axis(program) + _given(program) + unbounded_notes(program)) + + +def _given(program: Program) -> list[Advice]: + """One note per declaration the program reads and does not build. + + A note rather than a refusal, because both readings are a model somebody + meant: a template is composed with the file that introduces the column, and + a layer is bound to the model it is laid onto. What neither is, is a model + a consumer can build alone, and the consumer is the one that can tell which + it is holding. + """ + return [ + Advice( + 'given', + name, + f"{kind} '{name}' is read here and built elsewhere: a consumer binds it to the model this " + f'one is layered onto, and refuses where it cannot. A template is composed instead, and ' + f'merge() folds it into the file that introduces it.', + ) + for kind, group in (('variable', program.given_variables), ('row family', program.given_constraints)) + for name in group + ] def _never_an_axis(program: Program) -> list[Advice]: @@ -50,6 +73,8 @@ def _never_an_axis(program: Program) -> list[Advice]: reached: set[str] = set() for declaration in (*program.parameters.values(), *program.variables.values(), *program.constraints.values()): reached.update(declaration.dims) + reached.update(dim for given in program.given_variables.values() for dim in given.dims) + reached.update(dim for given in program.given_constraints.values() for dim in given.dims) reached |= _produced_axes(program) reached |= {dim for lk in program.relations.values() for dim in lk.dims} diff --git a/src/math_spec/composition.py b/src/math_spec/composition.py index 715bcaa6..4d09092b 100644 --- a/src/math_spec/composition.py +++ b/src/math_spec/composition.py @@ -73,7 +73,7 @@ #: The declarations a file reads and does not introduce. Peers must agree #: about one, and :func:`merge` folds it into the declaration that introduces #: it, so a composed library carries none. -GIVEN_SECTIONS = ('given_variables',) +GIVEN_SECTIONS = ('given_variables', 'given_constraints') #: Every section keyed by declaration name. ``objective`` is one declaration #: rather than a mapping of them, and is laid over field by field beside these. diff --git a/src/math_spec/dimensions.py b/src/math_spec/dimensions.py index d7e773f8..38b95c84 100644 --- a/src/math_spec/dimensions.py +++ b/src/math_spec/dimensions.py @@ -97,7 +97,7 @@ def _dims( raise AssertionError(msg) if isinstance(node, DualNode): - return frozenset(schema.constraints[node.constraint].dims) + return frozenset({**schema.constraints, **schema.given_constraints}[node.constraint].dims) if isinstance(node, FunctionCallNode): return _dims_call(node, schema, context) diff --git a/src/math_spec/errors.py b/src/math_spec/errors.py index 1c467ae9..686c63d5 100644 --- a/src/math_spec/errors.py +++ b/src/math_spec/errors.py @@ -18,7 +18,7 @@ #: Which pass an :class:`Advice` comes from. Closed, like the operator set: a #: consumer filtering on it can enumerate every value. -AdviceKind = Literal['never-an-axis', 'unbounded'] +AdviceKind = Literal['never-an-axis', 'unbounded', 'given'] ADVICE_KINDS = frozenset(get_args(AdviceKind)) diff --git a/src/math_spec/lowering.py b/src/math_spec/lowering.py index 58d0c0dd..25348d8e 100644 --- a/src/math_spec/lowering.py +++ b/src/math_spec/lowering.py @@ -34,12 +34,11 @@ VariableNode, ) from math_spec.dimensions import dims_of -from math_spec.errors import LanguageError from math_spec.piecewise import declaration_of, derivations_of, expand_piecewise from math_spec.validation import to_spec if TYPE_CHECKING: - from collections.abc import Callable, Mapping + from collections.abc import Callable from pathlib import Path from typing import Any @@ -78,32 +77,11 @@ def to_program(spec: str | Path | dict[str, Any] | Spec | program.Program) -> pr Raises: SchemaError: The file is not a valid model. LanguageError: A construct outside the language, named with its - rewrite, or a file that reads variables it does not introduce. + rewrite. """ if isinstance(spec, program.Program): return spec - schema = to_spec(spec) - if schema.given_variables: - raise LanguageError(_unintroduced_message(schema.given_variables)) - return lower_program(expand_piecewise(schema)) - - -def _unintroduced_message(given: Mapping[str, Any]) -> str: - """The refusal for lowering a fragment, which is a model no build can finish. - - A program is what a consumer builds and solves, so every column in one is a - column something introduces. A fragment states the opposite about some of - its own, which is why it is composed before it is lowered — and why it - still loads and still prints, both of which read the model rather than - build it. - """ - named = ', '.join(f"'{name}'" for name in sorted(given)) - noun = 'a variable' if len(given) == 1 else 'variables' - return ( - f'this file reads {noun} it does not introduce: {named}. A program builds every column it ' - f'carries, so compose the file with the ones that declare them first — ' - f'to_program(merge({{...}})). The file loads and prints on its own either way.' - ) + return lower_program(expand_piecewise(to_spec(spec))) def lower_program(expanded: _ExpandedSpec) -> program.Program: @@ -187,6 +165,10 @@ def lower_program(expanded: _ExpandedSpec) -> program.Program: expressions[name] = program.ExpressionDeclaration( _Lowering(expanded, f"named expression '{name}'").expr(ast), in_math=name in resolved.read_by_the_math ) + given_variables = {name: program.GivenDeclaration(tuple(g.dims)) for name, g in expanded.given_variables.items()} + given_constraints = { + name: program.GivenDeclaration(tuple(g.dims)) for name, g in expanded.given_constraints.items() + } return program.Program( parameters=parameters, variables=variables, @@ -196,6 +178,8 @@ def lower_program(expanded: _ExpandedSpec) -> program.Program: sos=sos, piecewise={name: declaration_of(ex) for name, ex in expanded.expanded_piecewise.items()}, named_expressions=expressions, + given_variables=given_variables, + given_constraints=given_constraints, ) diff --git a/src/math_spec/model.py b/src/math_spec/model.py index 2c355765..fd32cc1c 100644 --- a/src/math_spec/model.py +++ b/src/math_spec/model.py @@ -308,6 +308,20 @@ def _absence_needs_a_mask(self) -> VariableBlock: return self +class GivenConstraintBlock(_StrictBlock): + """A row family this file reads the dual of and does not build. + + The frame says how many duals there are and what indexes them, which is + what ``dual()`` needs and all this file can answer. There is no + ``expression:``: the body is the owner's, and nothing here builds a row. + """ + + _label: ClassVar[str] = 'a given constraint declaration' + + dims: list[str] + description: str | None = None + + class GivenVariableBlock(_StrictBlock): """A variable this file reads and does not introduce. @@ -710,7 +724,7 @@ class Spec(_StrictBlock): :class:`~math_spec.errors.LanguageError` on a model the language refuses. Holding one is the proof, so nothing downstream checks it again. - The API is the eleven declaration sections plus ``version`` and + The API is the twelve declaration sections plus ``version`` and ``description``, and two ways back out: :meth:`to_dict` for the model as data, :meth:`to_yaml` for the file a reviewer reads. Everything else on this class is pydantic's, not a contract this package keeps. @@ -746,6 +760,9 @@ class Spec(_StrictBlock): #: empty again once :func:`~math_spec.composition.merge` has folded each one #: into the declaration that introduces it. given_variables: dict[str, GivenVariableBlock] = {} + #: The row families this file reads the dual of and does not build + #: (:class:`GivenConstraintBlock`). Empty in a file that stands alone. + given_constraints: dict[str, GivenConstraintBlock] = {} def relations_of(self, dimension: str) -> dict[str, RelationBlock]: """The relations with a column over *dimension*, by name.""" @@ -830,11 +847,26 @@ def _validate_references(self) -> Spec: *self._relation_targets(), *self._bound_names(), *self._sos_shapes(), + *self._given_constraint_collisions(), ] if errors: raise ValueError('\n'.join(errors)) return self + def _given_constraint_collisions(self) -> Iterator[str]: + """A row family is either built here or given, never both. + + Constraint names sit outside the flat namespace :meth:`_name_collisions` + walks — ``dual()``'s argument is the only position that reads them — so + this is the one place the two constraint sections meet. + """ + for name in self.given_constraints: + if name in self.constraints: + yield ( + f"Given constraint '{name}' is also declared under 'constraints:'. A row family is " + f'either built by this file or given to it — drop one of the two.' + ) + def _name_collisions(self) -> Iterator[str]: """A name is declared once, and never as a built-in operator.""" kinds: list[tuple[str, Iterable[str]]] = [ @@ -869,6 +901,7 @@ def _frame_dimensions(self) -> Iterator[str]: *(('Parameter', name, p.dims) for name, p in self.parameters.items()), *(('Variable', name, v.dims) for name, v in self.variables.items()), *(('Given variable', name, g.dims) for name, g in self.given_variables.items()), + *(('Given constraint', name, g.dims) for name, g in self.given_constraints.items()), *(('Constraint', name, c.dims) for name, c in self.constraints.items()), *(('Named expression', name, e.dims or []) for name, e in self.expressions.items()), ] diff --git a/src/math_spec/program.py b/src/math_spec/program.py index f9cf87ce..6661ebf4 100644 --- a/src/math_spec/program.py +++ b/src/math_spec/program.py @@ -63,6 +63,7 @@ 'FanIn', 'FirstOf', 'Footprint', + 'GivenDeclaration', 'GroupSum', 'Increasing', 'LastOf', @@ -752,6 +753,21 @@ class VariableDeclaration: absence: VariableAbsence = 'undefined' +@dataclass(frozen=True) +class GivenDeclaration: + """A column or a row family this program reads and does not build. + + The frame is the whole declaration, because it is the whole of what the + file knows: whoever introduces the column owns its bounds, and whoever + builds the row owns its body. A consumer looks the name up in the model it + is layering onto, checks the frame against what it finds, and refuses what + it cannot bind — building a column of its own here would silently be a + second column nothing else names. + """ + + dims: tuple[str, ...] + + @dataclass(frozen=True) class ConstraintDeclaration: """``lhs sense rhs`` for each coord combination of ``dims``. @@ -968,6 +984,13 @@ class Program: #: named expression is outside the language is refused by every verb that #: reads the file rather than only by the one that reads the expression. named_expressions: Mapping[str, ExpressionDeclaration] = Sealed({}) + #: The columns this program reads and does not build. A consumer binds each + #: to a column the model it is layered onto already holds; nothing here + #: emits one, so a build reads :attr:`variables` and never this. + given_variables: Mapping[str, GivenDeclaration] = Sealed({}) + #: The row families this program reads the dual of and does not build, + #: bound the same way and read back after the solve. + given_constraints: Mapping[str, GivenDeclaration] = Sealed({}) def __post_init__(self) -> None: """Seal every group, so a program handed out cannot be written to.""" diff --git a/src/math_spec/resolution.py b/src/math_spec/resolution.py index 59ab79bc..f1a6ccaa 100644 --- a/src/math_spec/resolution.py +++ b/src/math_spec/resolution.py @@ -144,7 +144,7 @@ def of(cls, schema: Spec) -> Namespace: **{p: tuple(pd.dims) for p, pd in schema.parameters.items()}, **{v: tuple(vd.dims) for v, vd in {**schema.variables, **schema.given_variables}.items()}, }, - schema.constraints, + {**schema.constraints, **schema.given_constraints}, ) def kind(self, name: str) -> DeclarationKind | None: @@ -190,7 +190,8 @@ def unknown_constraint(self, name: str, context: str, *, formals: Iterable[str] return ( f"{context}: dual({name}): '{name}' is not a declared constraint{also}.\n" f' Constraints: {sorted(self.constraints)}\n' - f"Check for typos, or declare '{name}' under 'constraints:'." + f"Check for typos, or declare '{name}' — under 'constraints:' if this file builds the row, " + f"or under 'given_constraints:' if it reads the dual of one somebody else built." ) diff --git a/src/math_spec/typesetting/symbols.py b/src/math_spec/typesetting/symbols.py index 24125212..e1620939 100644 --- a/src/math_spec/typesetting/symbols.py +++ b/src/math_spec/typesetting/symbols.py @@ -129,7 +129,7 @@ def __init__(self, schema: _ExpandedSpec, fmt: Format, table: SymbolTable) -> No #: overrides it. self.constraint: dict[str, str] = { name: table.names[name] if name in table.names else _derive_name_symbol(name, declared, fmt, given=True) - for name in schema.constraints + for name in (*schema.constraints, *schema.given_constraints) } self.index: dict[str, str] = {} @@ -245,6 +245,7 @@ def checked_against(self, schema: _ExpandedSpec) -> SymbolTable: | set(schema.given_variables) | set(schema.expressions) | set(schema.constraints) + | set(schema.given_constraints) ) errors = [ *(_unknown_entry(d, 'dimensions', dims) for d in {*self.indices, *self.sets} - dims), diff --git a/src/math_spec/typesetting/walk.py b/src/math_spec/typesetting/walk.py index bc7142c3..cd220821 100644 --- a/src/math_spec/typesetting/walk.py +++ b/src/math_spec/typesetting/walk.py @@ -865,6 +865,13 @@ def glossaries(self, noticed: Noticed) -> list[Glossary]: given = [ self._entry(self.symbols.name[g], f'{fmt.mono(g)}{self._over(list(block.dims))}', block.description) for g, block in self.schema.given_variables.items() + ] + [ + self._entry( + self.symbols.constraint[g], + f'{fmt.mono(g)}{self._over(list(block.dims))}, a row family this file reads the dual of', + block.description, + ) + for g, block in self.schema.given_constraints.items() ] definitions = [ self._entry(self.symbols.name[e], f'{fmt.mono(e)}{self._over(self.frames[e])}', block.description) diff --git a/tests/test_advice.py b/tests/test_advice.py index a95b20e8..da6cea8f 100644 --- a/tests/test_advice.py +++ b/tests/test_advice.py @@ -66,7 +66,28 @@ def test_both_kinds_of_note_come_through_the_one_door(): assert [(n.kind, n.subject) for n in notes] == [('never-an-axis', 'h'), ('unbounded', 'p')], ( 'the never-an-axis advice comes first, then the unboundedness advice' ) - assert {n.kind for n in notes} == ADVICE_KINDS, 'every kind a consumer can pin against is one this file produces' + + +#: A model whose only note is the third kind: `flow` is a column this file +#: reads and whatever it is layered onto builds. `p` is bounded on both sides +#: and every dimension is indexed, so neither other pass has anything to say. +READS_A_COLUMN = { + 'dimensions': {'g': {'dtype': 'str'}}, + 'given_variables': {'flow': {'dims': ['g']}}, + 'variables': {'p': {'dims': ['g'], 'bounds': {'lower': 0, 'upper': 1}}}, + 'constraints': {'tie': {'dims': ['g'], 'expression': 'p == flow'}}, +} + + +def test_a_column_read_and_not_built_is_advised(): + (note,) = advice(READS_A_COLUMN) + assert (note.kind, note.subject) == ('given', 'flow') + assert 'binds it to the model' in str(note), 'the note says whose job the column is' + + +def test_every_kind_a_consumer_can_pin_against_is_produced_here(): + kinds = {note.kind for note in (*advice(BOTH_KINDS), *advice(READS_A_COLUMN))} + assert kinds == ADVICE_KINDS, 'every kind a consumer can pin against is one these fixtures produce' def _written(model: dict, tmp_path: Path) -> Path: diff --git a/tests/test_given.py b/tests/test_given.py new file mode 100644 index 00000000..7a30f910 --- /dev/null +++ b/tests/test_given.py @@ -0,0 +1,235 @@ +# SPDX-FileCopyrightText: math-spec Contributors +# +# SPDX-License-Identifier: MIT + +"""What a file reads and does not build: a column, and a row family. + +Two readings, and each is a model somebody meant. A **template** reads a column +the file beside it introduces, and `merge` folds the two together, so the +composed model carries neither the declaration nor any trace of it. A **layer** +reads a column, or the dual of a row family, that a model outside the language +holds — linopy's, say — and there is nothing to fold into, so the program +carries the name and the frame and a consumer binds them. + +What both need is that the file stands on its own: it loads, and it prints as +math, without the thing that owns what it reads. +""" + +from __future__ import annotations + +import pytest + +from math_spec import FORMATS, LanguageError, advice, merge, to_markdown, to_program, to_spec, typeset + +#: One component template: it pins the flow at its own port, and the column it +#: pins belongs to the surface fragment below. +SUPPLY = { + 'description': 'A fleet of generators, each on one port.', + 'dimensions': {'snapshot': {'dtype': 'int'}, 'port': {'dtype': 'str'}, 'generator': {'dtype': 'str'}}, + 'relations': {'gen_port': {'key': 'generator', 'value': 'port'}}, + 'given_variables': {'flow': {'dims': ['snapshot', 'port'], 'description': 'what a port puts into its bus'}}, + 'parameters': {'gen_cost': {'dims': ['generator']}, 'gen_p_max': {'dims': ['generator']}}, + 'variables': {'gen_p': {'dims': ['snapshot', 'generator'], 'bounds': {'lower': 0, 'upper': 'gen_p_max'}}}, + 'constraints': {'gen_injects': {'dims': ['snapshot', 'generator'], 'expression': 'at(flow, by=gen_port) == gen_p'}}, + 'objective': {'sense': 'minimize', 'expression': 'sum(gen_p * gen_cost)'}, +} + +#: The fragment that owns `flow`, with the bounds and the balance that go with it. +SURFACE = { + 'dimensions': {'snapshot': {'dtype': 'int'}, 'port': {'dtype': 'str'}, 'bus': {'dtype': 'str'}}, + 'relations': {'port_bus': {'key': 'port', 'value': 'bus'}}, + 'variables': {'flow': {'dims': ['snapshot', 'port'], 'bounds': {'lower': -1000, 'upper': 1000}}}, + 'constraints': {'balance': {'dims': ['snapshot', 'bus'], 'expression': 'sum(flow, by=port_bus) == 0'}}, +} + + +def test_a_fragment_that_says_what_it_reads_loads_on_its_own(): + spec = to_spec(SUPPLY) + assert sorted(spec.given_variables) == ['flow'], 'the column it reads is a declaration like any other' + assert sorted(spec.variables) == ['gen_p'], 'and it is not one of the columns this file introduces' + + +@pytest.mark.parametrize('fmt', sorted(FORMATS)) +def test_a_fragment_prints_as_math_in_every_format(fmt): + """The improvement the section exists for: the unit you share is the unit you can read.""" + assert typeset(SUPPLY, fmt), f'{fmt} rendered nothing' + + +def test_the_given_column_prints_under_its_own_heading(): + printed = to_markdown(SUPPLY) + assert '#### Given' in printed, 'the legend says which symbols the file does not introduce' + assert '`flow`' in printed.split('#### Given')[1] + + +def test_a_program_carries_the_column_it_reads_apart_from_the_ones_it_builds(): + """The distinction a builder needs: create this column, or bind it to one the host already holds.""" + program = to_program(SUPPLY) + assert sorted(program.variables) == ['gen_p'], 'a build reads this group and creates a column for each' + assert sorted(program.given_variables) == ['flow'], 'and binds each of these to a column it is given' + assert program.given_variables['flow'].dims == ('snapshot', 'port'), 'the frame is what a binder checks' + + +def test_the_advice_says_which_columns_a_consumer_has_to_bind(): + (note,) = [note for note in advice(SUPPLY) if note.kind == 'given'] + assert note.subject == 'flow' + + +def test_merging_folds_the_given_declaration_into_the_one_that_introduces_it(): + composed = merge({'surface': SURFACE, 'supply': SUPPLY}) + assert 'given_variables' not in composed, 'the expectation is spent once the column is in the composition' + spec = to_spec(composed) + assert sorted(spec.variables) == ['flow', 'gen_p'] + assert spec.variables['flow'].bounds.lower == -1000, "the introducer's declaration is the one that survives" + assert sorted(to_program(spec).variables) == ['flow', 'gen_p'], 'a composed library lowers like any model' + + +def test_a_given_declaration_may_say_less_than_the_introducer(): + """Bounds are the owner's, so the reader states the frame and stops.""" + assert 'bounds' not in SUPPLY['given_variables']['flow'] + assert to_spec(merge({'surface': SURFACE, 'supply': SUPPLY})).variables['flow'].bounds.upper == 1000 + + +def test_a_given_declaration_that_disagrees_with_the_introducer_is_refused(): + misread = {**SUPPLY, 'given_variables': {'flow': {'dims': ['snapshot', 'generator']}}} + with pytest.raises(LanguageError) as raised: + merge({'surface': SURFACE, 'supply': misread}) + message = str(raised.value) + assert "'supply'" in message and "'surface'" in message, 'both sides of a disagreement are named' + + +def test_two_fragments_must_read_one_column_the_same_way(): + other = { + 'dimensions': {'snapshot': {'dtype': 'int'}, 'port': {'dtype': 'str'}}, + 'given_variables': {'flow': {'dims': ['port']}}, + } + with pytest.raises(LanguageError, match=r'say different things about given variable'): + merge({'supply': SUPPLY, 'other': other}) + + +def test_a_name_both_introduced_and_given_in_one_file_is_refused(): + both = {**SUPPLY, 'variables': {**SUPPLY['variables'], 'flow': {'dims': ['snapshot', 'port']}}} + with pytest.raises(LanguageError, match=r"'flow'"): + to_spec(both) + + +@pytest.mark.parametrize( + ('block', 'says'), + [ + pytest.param({'dims': ['snapshot', 'nowhere']}, 'nowhere', id='a-frame-over-an-undeclared-dimension'), + pytest.param({'dims': ['snapshot', 'snapshot']}, 'twice', id='a-frame-naming-one-dimension-twice'), + pytest.param({'dims': ['snapshot'], 'bounds': {'lower': 0}}, 'bounds', id='bounds-the-owner-holds'), + pytest.param({'dims': ['snapshot'], 'where': 'gen_cost > 0'}, 'where', id='a-mask-the-owner-holds'), + ], +) +def test_a_given_declaration_is_refused_where_it_oversteps(block, says): + with pytest.raises(LanguageError) as raised: + to_spec({**SUPPLY, 'given_variables': {'flow': block}}) + assert says in str(raised.value) + + +def test_an_expression_reads_a_given_column_as_it_reads_any_other(): + """Resolution and the dim algebra see one namespace, so `at(flow, by=gen_port)` lands on the generator frame.""" + spec = to_spec(SUPPLY) + assert spec.constraints['gen_injects'].dims == ['snapshot', 'generator'] + + +#: A layer over a model this language never sees: it reads a column and the +#: dual of a row family, and adds one constraint of its own. +LAYER = { + 'description': 'A carbon cap laid over a model that already exists.', + 'dimensions': {'snapshot': {'dtype': 'int'}, 'bus': {'dtype': 'str'}}, + 'given_variables': {'p': {'dims': ['snapshot', 'bus']}}, + 'given_constraints': {'balance': {'dims': ['snapshot', 'bus'], 'description': 'the host clears each bus'}}, + 'parameters': {'rate': {'dims': ['bus']}}, + 'constraints': {'cap': {'dims': [], 'expression': 'sum(p * rate) <= 100'}}, + 'expressions': {'price': {'expression': 'dual(balance)'}}, +} + + +def test_a_dual_may_name_a_row_family_this_file_does_not_build(): + spec = to_spec(LAYER) + assert sorted(spec.given_constraints) == ['balance'] + assert sorted(spec.constraints) == ['cap'], 'the row families it builds are its own, and that is not one' + + +def test_the_program_carries_the_row_family_a_consumer_binds(): + program = to_program(LAYER) + assert sorted(program.given_constraints) == ['balance'] + assert program.given_constraints['balance'].dims == ('snapshot', 'bus'), 'the frame is what a binder checks' + + +def test_the_dual_takes_its_frame_from_the_given_declaration(): + """Without the frame the reported expression has no dims, and nothing downstream could shape it.""" + assert to_markdown(LAYER).count(r'\lambda_{\mathrm{balance},t,b}') == 1 + + +def test_a_given_row_family_prints_under_the_given_heading(): + given = to_markdown(LAYER).split('#### Given')[1] + assert '`balance`' in given + assert 'reads the dual of' in given, 'the legend says what the file may do with it' + + +def test_a_row_family_both_built_and_given_is_refused(): + both = {**LAYER, 'constraints': {**LAYER['constraints'], 'balance': {'dims': [], 'expression': 'sum(p) >= 0'}}} + with pytest.raises(LanguageError, match=r"'balance'.*either built by this file or given to it"): + to_spec(both) + + +def test_a_dual_naming_nothing_says_where_to_declare_it(): + mistyped = {**LAYER, 'expressions': {'price': {'expression': 'dual(balnce)'}}} + with pytest.raises(LanguageError) as raised: + to_spec(mistyped) + message = str(raised.value) + assert "'constraints:'" in message and "'given_constraints:'" in message, ( + 'the message names both places the row family could be declared' + ) + + +@pytest.mark.parametrize( + ('block', 'says'), + [ + pytest.param({'dims': [], 'expression': 'sum(p) >= 0'}, 'expression', id='a-body-the-owner-holds'), + pytest.param({'dims': [], 'sense': '<='}, 'sense', id='a-sense-nothing-here-could-check'), + ], +) +def test_a_given_row_family_is_refused_where_it_oversteps(block, says): + with pytest.raises(LanguageError) as raised: + to_spec({**LAYER, 'given_constraints': {'balance': block}}) + assert says in str(raised.value) + + +def test_merging_folds_a_row_family_into_the_file_that_builds_it(): + builder = { + 'dimensions': {'snapshot': {'dtype': 'int'}, 'bus': {'dtype': 'str'}}, + 'variables': {'p': {'dims': ['snapshot', 'bus'], 'bounds': {'lower': 0}}}, + 'constraints': {'balance': {'dims': ['snapshot', 'bus'], 'expression': 'p >= 0'}}, + } + composed = merge({'builder': builder, 'layer': LAYER}) + assert 'given_constraints' not in composed and 'given_variables' not in composed + program = to_program(composed) + assert sorted(program.constraints) == ['balance', 'cap'] + assert not program.given_constraints, 'nothing is left for a consumer to bind' + + +def test_the_advice_names_every_declaration_a_consumer_has_to_bind(): + subjects = {(note.subject) for note in advice(LAYER) if note.kind == 'given'} + assert subjects == {'p', 'balance'}, 'both the column and the row family are named' + + +#: `port` is named by nothing but the given column's frame, and `bus` by +#: nothing but the given row family's, so each is in use only through a +#: declaration this file does not build. +REACHED_ONLY_BY_A_GIVEN_FRAME = { + 'dimensions': {'g': {'dtype': 'str'}, 'port': {'dtype': 'str'}, 'bus': {'dtype': 'str'}}, + 'given_variables': {'flow': {'dims': ['port']}}, + 'given_constraints': {'balance': {'dims': ['bus']}}, + 'variables': {'p': {'dims': ['g'], 'bounds': {'lower': 0, 'upper': 1}}}, + 'constraints': {'tie': {'dims': ['g'], 'expression': 'p >= sum(flow, over=port)'}}, + 'expressions': {'price': {'expression': 'dual(balance)'}}, +} + + +def test_a_dimension_only_a_given_declaration_indexes_is_in_use(): + """The never-an-axis pass reads the frames a build emits, and these two are in neither.""" + unreached = {note.subject for note in advice(REACHED_ONLY_BY_A_GIVEN_FRAME) if note.kind == 'never-an-axis'} + assert not unreached, 'a dimension a given column or row family is indexed by is used' diff --git a/tests/test_given_variables.py b/tests/test_given_variables.py deleted file mode 100644 index 35ec45a7..00000000 --- a/tests/test_given_variables.py +++ /dev/null @@ -1,127 +0,0 @@ -# SPDX-FileCopyrightText: math-spec Contributors -# -# SPDX-License-Identifier: MIT - -"""A file that reads a column it does not introduce, and still stands on its own. - -The point of the section is what a template could not do before it: load, and -print as math, without the file that owns the column. What it may not do is -lower — a program builds every column it carries — so the two doors this pins -open and shut in the same breath: `to_spec` and the typesetter take a fragment, -`to_program` refuses one and names the composition that fixes it. -""" - -from __future__ import annotations - -import pytest - -from math_spec import FORMATS, LanguageError, merge, to_markdown, to_program, to_spec, typeset - -#: One component template: it pins the flow at its own port, and the column it -#: pins belongs to the surface fragment below. -SUPPLY = { - 'description': 'A fleet of generators, each on one port.', - 'dimensions': {'snapshot': {'dtype': 'int'}, 'port': {'dtype': 'str'}, 'generator': {'dtype': 'str'}}, - 'relations': {'gen_port': {'key': 'generator', 'value': 'port'}}, - 'given_variables': {'flow': {'dims': ['snapshot', 'port'], 'description': 'what a port puts into its bus'}}, - 'parameters': {'gen_cost': {'dims': ['generator']}, 'gen_p_max': {'dims': ['generator']}}, - 'variables': {'gen_p': {'dims': ['snapshot', 'generator'], 'bounds': {'lower': 0, 'upper': 'gen_p_max'}}}, - 'constraints': {'gen_injects': {'dims': ['snapshot', 'generator'], 'expression': 'at(flow, by=gen_port) == gen_p'}}, - 'objective': {'sense': 'minimize', 'expression': 'sum(gen_p * gen_cost)'}, -} - -#: The fragment that owns `flow`, with the bounds and the balance that go with it. -SURFACE = { - 'dimensions': {'snapshot': {'dtype': 'int'}, 'port': {'dtype': 'str'}, 'bus': {'dtype': 'str'}}, - 'relations': {'port_bus': {'key': 'port', 'value': 'bus'}}, - 'variables': {'flow': {'dims': ['snapshot', 'port'], 'bounds': {'lower': -1000, 'upper': 1000}}}, - 'constraints': {'balance': {'dims': ['snapshot', 'bus'], 'expression': 'sum(flow, by=port_bus) == 0'}}, -} - - -def test_a_fragment_that_says_what_it_reads_loads_on_its_own(): - spec = to_spec(SUPPLY) - assert sorted(spec.given_variables) == ['flow'], 'the column it reads is a declaration like any other' - assert sorted(spec.variables) == ['gen_p'], 'and it is not one of the columns this file introduces' - - -@pytest.mark.parametrize('fmt', sorted(FORMATS)) -def test_a_fragment_prints_as_math_in_every_format(fmt): - """The improvement the section exists for: the unit you share is the unit you can read.""" - assert typeset(SUPPLY, fmt), f'{fmt} rendered nothing' - - -def test_the_given_column_prints_under_its_own_heading(): - printed = to_markdown(SUPPLY) - assert '#### Given' in printed, 'the legend says which symbols the file does not introduce' - assert '`flow`' in printed.split('#### Given')[1] - - -def test_a_program_refuses_a_file_that_reads_what_it_does_not_introduce(): - with pytest.raises(LanguageError, match=r"reads a variable it does not introduce: 'flow'"): - to_program(SUPPLY) - - -def test_the_refusal_names_the_composition_that_fixes_it(): - with pytest.raises(LanguageError) as raised: - to_program(SUPPLY) - assert 'merge(' in str(raised.value), 'a message names the rewrite, and here the rewrite is a verb' - - -def test_merging_folds_the_given_declaration_into_the_one_that_introduces_it(): - composed = merge({'surface': SURFACE, 'supply': SUPPLY}) - assert 'given_variables' not in composed, 'the expectation is spent once the column is in the composition' - spec = to_spec(composed) - assert sorted(spec.variables) == ['flow', 'gen_p'] - assert spec.variables['flow'].bounds.lower == -1000, "the introducer's declaration is the one that survives" - assert sorted(to_program(spec).variables) == ['flow', 'gen_p'], 'a composed library lowers like any model' - - -def test_a_given_declaration_may_say_less_than_the_introducer(): - """Bounds are the owner's, so the reader states the frame and stops.""" - assert 'bounds' not in SUPPLY['given_variables']['flow'] - assert to_spec(merge({'surface': SURFACE, 'supply': SUPPLY})).variables['flow'].bounds.upper == 1000 - - -def test_a_given_declaration_that_disagrees_with_the_introducer_is_refused(): - misread = {**SUPPLY, 'given_variables': {'flow': {'dims': ['snapshot', 'generator']}}} - with pytest.raises(LanguageError) as raised: - merge({'surface': SURFACE, 'supply': misread}) - message = str(raised.value) - assert "'supply'" in message and "'surface'" in message, 'both sides of a disagreement are named' - - -def test_two_fragments_must_read_one_column_the_same_way(): - other = { - 'dimensions': {'snapshot': {'dtype': 'int'}, 'port': {'dtype': 'str'}}, - 'given_variables': {'flow': {'dims': ['port']}}, - } - with pytest.raises(LanguageError, match=r'say different things about given variable'): - merge({'supply': SUPPLY, 'other': other}) - - -def test_a_name_both_introduced_and_given_in_one_file_is_refused(): - both = {**SUPPLY, 'variables': {**SUPPLY['variables'], 'flow': {'dims': ['snapshot', 'port']}}} - with pytest.raises(LanguageError, match=r"'flow'"): - to_spec(both) - - -@pytest.mark.parametrize( - ('block', 'says'), - [ - pytest.param({'dims': ['snapshot', 'nowhere']}, 'nowhere', id='a-frame-over-an-undeclared-dimension'), - pytest.param({'dims': ['snapshot', 'snapshot']}, 'twice', id='a-frame-naming-one-dimension-twice'), - pytest.param({'dims': ['snapshot'], 'bounds': {'lower': 0}}, 'bounds', id='bounds-the-owner-holds'), - pytest.param({'dims': ['snapshot'], 'where': 'gen_cost > 0'}, 'where', id='a-mask-the-owner-holds'), - ], -) -def test_a_given_declaration_is_refused_where_it_oversteps(block, says): - with pytest.raises(LanguageError) as raised: - to_spec({**SUPPLY, 'given_variables': {'flow': block}}) - assert says in str(raised.value) - - -def test_an_expression_reads_a_given_column_as_it_reads_any_other(): - """Resolution and the dim algebra see one namespace, so `at(flow, by=gen_port)` lands on the generator frame.""" - spec = to_spec(SUPPLY) - assert spec.constraints['gen_injects'].dims == ['snapshot', 'generator'] diff --git a/tests/test_reading_page.py b/tests/test_reading_page.py index 0117f308..35b1179a 100644 --- a/tests/test_reading_page.py +++ b/tests/test_reading_page.py @@ -55,6 +55,6 @@ def test_the_page_shows_the_declarations_the_expansion_emits(tmp_path, monkeypat exec(compile(code, str(PAGE), 'exec'), namespace) claims.extend(_claims(code)) - assert len(claims) == 10, 'every `expression # value` line on the page is checked; one without one is not' + assert len(claims) == 13, 'every `expression # value` line on the page is checked; one without one is not' for expression, claimed in claims: assert eval(expression, namespace) == claimed, f'reading.md says `{expression}` is {claimed}'