diff --git a/docs/reference/language/declarations.md b/docs/reference/language/declarations.md index caca3045..d02914f5 100644 --- a/docs/reference/language/declarations.md +++ b/docs/reference/language/declarations.md @@ -207,3 +207,46 @@ different models, and the bracket is the difference. A second objective is unsayable rather than checked — the schema holds one block. Weight several goals into one expression. + +## `checks` + +A condition the **data** must satisfy for the model to mean what it says. It +builds no row and changes no answer; it is the sentence a reader has to believe +about the table before believing the constraints above it. + +```yaml +parameters: + CVaR_omega: { dims: [] } + Link_efficiency: { dims: [link] } +checks: + omega_is_a_share: "CVaR_omega >= 0 AND CVaR_omega <= 1" + efficiency_is_a_share: + holds: "Link_efficiency > 0 AND Link_efficiency <= 1" + description: a link delivers some of what it takes, and no more +``` + +| Field | | | +| ------------- | ---------------------------------------------------------------------- | -------------- | +| `holds` | required — a `where` predicate ([where](expressions.md#where-strings)) | | +| `description` | free text | default `null` | + +Written as a bare string wherever it carries no description, like a named +expression. + +**There is no `foreach`.** A check is asked at every coordinate the names in it +span — `Link_efficiency` over `link` is one question per link, and a scalar +parameter is one question — so the frame is read off the predicate rather than +declared beside it. + +**Nothing here checks it.** No file determines whether a table satisfies a +condition, so the language states it and the consumer binding the data raises +it, in the language's own words — `check_message` is the sentence, and the +`description:` is its second half, which is why a check is the one declaration +whose prose reaches the program +([reading a loaded model](reading.md)). What _is_ decided at load is that the +condition is one data could break: a predicate the connectives settle to +`True` checks nothing and one that settles to `False` refuses every table, and +both are load errors naming the rewrite. So is a predicate reading a variable, +which has no value before the solve. + +A check prints, under **Data conditions**, as the predicate it is — last, and [droppable](../typeset.md#options) for a page about the math alone. diff --git a/docs/reference/language/file.md b/docs/reference/language/file.md index 187fcf00..023b4353 100644 --- a/docs/reference/language/file.md +++ b/docs/reference/language/file.md @@ -20,6 +20,7 @@ and `description`: | `macros` | parameterised templates ([macros](expressions.md#macros)) | | `piecewise` | piecewise-linear curves ([piecewise](piecewise.md)) | | `sos` | special-ordered sets ([sos](piecewise.md#sos)) | +| `checks` | conditions the bound data must satisfy ([checks](declarations.md#checks)) | Any subset is accepted, `objective` included: a file with none is a **feasibility problem**, and the answer is whether the constraints can be met diff --git a/docs/reference/language/reading.md b/docs/reference/language/reading.md index 6bcca9d1..490334ca 100644 --- a/docs/reference/language/reading.md +++ b/docs/reference/language/reading.md @@ -89,12 +89,19 @@ with nothing to see. `Program` is a different type from `Spec`, so that mistake is one the signature refuses rather than one the numbers report. **A program cannot answer what the file wrote.** It has no `macros:`, no -`description:`, and no link expression — those are the `Spec`'s, and +link expression, and no `description:` — bar one, below — so those are the +`Spec`'s, and rendering has to be handed what `to_spec` returned. The projection runs one way on purpose. What it keeps of a `piecewise:` block is `program.piecewise`: which parameters carry the curve, and what the block assumes of the numbers as a `checks` tuple — each check carrying the names it is about, so the consumer holding the numbers runs it, with `check_message` for the sentence to raise. +`program.checks` is the same vocabulary where the _file_ wrote the condition +rather than a curve implying it: one `Holds` per +[`checks:`](declarations.md#checks) block, carrying the resolved predicate, the +dims it is asked over, and — the one prose a program keeps — the block's own +`description:`, because there it is not documentation but the second half of +the sentence `check_message` returns. What the expansion emitted is answered where it is asked instead: a `ParameterDeclaration.derivation` says how that parameter is filled, and `None` means the caller binds it. diff --git a/docs/reference/typeset.md b/docs/reference/typeset.md index de3c9b7d..b11e500f 100644 --- a/docs/reference/typeset.md +++ b/docs/reference/typeset.md @@ -39,6 +39,7 @@ The three functions take the same keywords; the CLI spells each as a flag. | `symbols` | `--symbols FILE` | how names should print — [below](#symbol-tables). Default: derived | | `standalone` | `--standalone` | emit a document that compiles, rather than a fragment to include. Default: fragment | | `legend` | `--no-legend` | the sets / parameters / variables table above the math. Default: on | +| `checks` | `--no-checks` | the data conditions the model declares, below the math. Default: on | | `numbered` | `--no-numbers` | number the equations. Default: on | `-o FILE` writes to a file instead of stdout. @@ -51,6 +52,10 @@ that is the math the solver receives. Where the math translates an index — what the notation for it means, so a reader meets no symbol the page has not defined. +A [`checks:`](language/declarations.md#checks) block prints last, under **Data +conditions** — a condition on the _input_ rather than a row a solver holds, so +`--no-checks` leaves a page about the math alone. + A model that does not compile does not print: typesetting runs the same load-time checks everything else does. diff --git a/examples/pypsa_stochastic.yaml b/examples/pypsa_stochastic.yaml index 015b86fb..37811050 100644 --- a/examples/pypsa_stochastic.yaml +++ b/examples/pypsa_stochastic.yaml @@ -202,3 +202,16 @@ objective: sum(Generator_p_nom_ext * Generator_capital_cost) + (1 - CVaR_omega) * sum(scenario_weight * scenario_opex, over=scenario) + CVaR_omega * CVaR + +checks: + omega_is_a_share: + holds: "CVaR_omega >= 0 AND CVaR_omega <= 1" + description: >- + the objective blends the expectation and the tail at `omega` and + `1 - omega`, so outside [0, 1] it is an extrapolation of the two rather + than a mix of them + tail_probability_is_one_or_more: + holds: "CVaR_inv_tail >= 1" + description: >- + `1 / (1 - alpha)` for a probability `alpha`, so below one the CVaR row + prices the tail at less than its own expectation diff --git a/schema/math-spec.schema.json b/schema/math-spec.schema.json index 6c45b96f..04d21218 100644 --- a/schema/math-spec.schema.json +++ b/schema/math-spec.schema.json @@ -30,6 +30,40 @@ "title": "BoundsBlock", "type": "object" }, + "CheckBlock": { + "anyOf": [ + { + "additionalProperties": false, + "description": "A condition the data must satisfy for the model to mean what it says.\n\nWritten in YAML as a bare string, or as a mapping once it carries a\n``description:`` \u2014 and serialised back to whichever form it was written in,\nso a round trip through :meth:`Spec.to_yaml` reproduces the file::\n\n checks:\n omega_is_a_share: \"CVaR_omega >= 0 AND CVaR_omega <= 1\"\n efficiency_is_a_share:\n holds: \"Link_efficiency > 0 AND Link_efficiency <= 1\"\n description: a link delivers some of what it takes, and no more\n\n``holds:`` is a ``where`` predicate, read over the dims the names in it\ncarry. It builds no row: a consumer holding the data refuses a model whose\ntable breaks it, in the language's own words\n(:func:`~math_spec.program.check_message`).", + "properties": { + "description": { + "anyOf": [ + { + "type": "string" + }, + { + "type": "null" + } + ], + "default": null, + "title": "Description" + }, + "holds": { + "title": "Holds", + "type": "string" + } + }, + "required": [ + "holds" + ], + "title": "CheckBlock", + "type": "object" + }, + { + "type": "string" + } + ] + }, "ConstraintBlock": { "additionalProperties": false, "description": "A declared constraint: one rule, over one frame.", @@ -552,8 +586,16 @@ }, "$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\nThe API is the ten 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. In goes through\n``to_spec``, which raises\n:class:`~math_spec.errors.LanguageError` on a model the language refuses.\n\nEverything else on this class is pydantic's, not a contract this package\nkeeps \u2014 ``model_json_schema()`` describes the shape pydantic validates\nrather than the language (checked in for editors as\n``schema/math_spec.schema.json``), and ``model_construct()`` skips validation\nentirely, so a ``Spec`` is valid when it was built the normal way.", + "description": "The declared math \u2014 one YAML file, or one dict, validated. Nothing here has seen data.\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. In goes through\n``to_spec``, which raises\n:class:`~math_spec.errors.LanguageError` on a model the language refuses.\n\nEverything else on this class is pydantic's, not a contract this package\nkeeps \u2014 ``model_json_schema()`` describes the shape pydantic validates\nrather than the language (checked in for editors as\n``schema/math_spec.schema.json``), and ``model_construct()`` skips validation\nentirely, so a ``Spec`` is valid when it was built the normal way.", "properties": { + "checks": { + "additionalProperties": { + "$ref": "#/$defs/CheckBlock" + }, + "default": {}, + "title": "Checks", + "type": "object" + }, "constraints": { "additionalProperties": { "$ref": "#/$defs/ConstraintBlock" diff --git a/src/math_spec/__main__.py b/src/math_spec/__main__.py index 4fd183f6..d7c8c881 100644 --- a/src/math_spec/__main__.py +++ b/src/math_spec/__main__.py @@ -36,6 +36,7 @@ def parser() -> argparse.ArgumentParser: verb.add_argument('--symbols', help='sidecar YAML saying how names should print') verb.add_argument('--standalone', action='store_true', help='emit a compilable document') verb.add_argument('--no-legend', action='store_true', help='omit the sets/parameters/variables table') + verb.add_argument('--no-checks', action='store_true', help='omit the data conditions the model declares') verb.add_argument('--no-numbers', action='store_true', help='leave the equations unnumbered') return front @@ -61,6 +62,7 @@ def main(argv: list[str] | None = None) -> int: symbols=args.symbols, standalone=args.standalone, legend=not args.no_legend, + checks=not args.no_checks, numbered=not args.no_numbers, ) if args.out: diff --git a/src/math_spec/dimensions.py b/src/math_spec/dimensions.py index 327c9ab3..ed4200bc 100644 --- a/src/math_spec/dimensions.py +++ b/src/math_spec/dimensions.py @@ -464,6 +464,31 @@ def check_schema(schema: Spec) -> None: ) +def where_dims(node: WhereNode | None, schema: Spec) -> frozenset[str]: + """The dims a resolved predicate reads. + + A ``where:`` is checked *against* a declared frame; a ``checks:`` block has + no frame of its own, so its rows are exactly the coordinates its names + span, and this is what says which those are. + """ + if node is None or isinstance(node, BooleanLiteralNode): + return frozenset() + if isinstance(node, (ParameterDefinedNode, ParameterComparisonNode)): + return frozenset(schema.parameters[node.name].dims) + if isinstance(node, VariableDefinedNode): + return frozenset(schema.variables[node.name].foreach) + if isinstance(node, (DimensionComparisonNode, DimensionPositionNode)): + return frozenset({node.name}) + if isinstance(node, (LookupComparisonNode, LookupPairComparisonNode, LookupDefinedNode)): + return frozenset({node.over}) + if isinstance(node, NotNode): + return where_dims(node.operand, schema) + if isinstance(node, (AndNode, OrNode)): + return where_dims(node.left, schema) | where_dims(node.right, schema) + msg = f'{type(node).__name__} reached the dim reader unresolved.' + raise AssertionError(msg) + + def _check_where_dims( node: WhereNode | None, schema: Spec, diff --git a/src/math_spec/lowering.py b/src/math_spec/lowering.py index 2e04350b..58bf0897 100644 --- a/src/math_spec/lowering.py +++ b/src/math_spec/lowering.py @@ -32,7 +32,7 @@ from typing import TYPE_CHECKING, Literal, assert_never, cast import math_spec.program as program -from math_spec.dimensions import dims_of +from math_spec.dimensions import dims_of, where_dims from math_spec.errors import LanguageError from math_spec.expression_parser import ( ArithmeticNode, @@ -187,6 +187,7 @@ def lower_program(schema: _ExpandedSpec) -> program.Program: for sname, sdef in expanded.sos.items() } expressions = {name: _lower_expression(expanded, ns, name) for name in expanded.expressions} + checks = {name: _lower_check(expanded, ns, name) for name in expanded.checks} return program.Program( parameters=parameters, variables=variables, @@ -196,9 +197,18 @@ def lower_program(schema: _ExpandedSpec) -> program.Program: sos=sos, piecewise={name: declaration_of(ex) for name, ex in expanded.expanded_piecewise.items()}, named_expressions=expressions, + checks=checks, ) +def _lower_check(schema: _ExpandedSpec, ns: Namespace, name: str) -> program.Holds: + """Resolve the check *name* and read the coordinates it is asked at off its own names.""" + block = schema.checks[name] + holds = where_of(block.holds, ns, f"check '{name}'") + assert holds is not None, 'load-time validation refuses a check that holds whatever the data says' + return program.Holds(holds, tuple(sorted(where_dims(holds, schema))), block.description) + + def _lower_expression(schema: _ExpandedSpec, ns: Namespace, name: str) -> program.ExpressionNode: """Compile the named expression *name* into a program expression. diff --git a/src/math_spec/model.py b/src/math_spec/model.py index efda499c..792c5eb5 100644 --- a/src/math_spec/model.py +++ b/src/math_spec/model.py @@ -352,6 +352,48 @@ def _as_written(self) -> str | dict[str, str]: return {'expression': self.expression, 'description': self.description} +class CheckBlock(_StrictBlock): + """A condition the data must satisfy for the model to mean what it says. + + Written in YAML as a bare string, or as a mapping once it carries a + ``description:`` — and serialised back to whichever form it was written in, + so a round trip through :meth:`Spec.to_yaml` reproduces the file:: + + checks: + omega_is_a_share: "CVaR_omega >= 0 AND CVaR_omega <= 1" + efficiency_is_a_share: + holds: "Link_efficiency > 0 AND Link_efficiency <= 1" + description: a link delivers some of what it takes, and no more + + ``holds:`` is a ``where`` predicate, read over the dims the names in it + carry. It builds no row: a consumer holding the data refuses a model whose + table breaks it, in the language's own words + (:func:`~math_spec.program.check_message`). + """ + + _label: ClassVar[str] = 'a check' + + holds: str + description: str | None = None + + @model_validator(mode='before') + @classmethod + def _from_string(cls, data: Any) -> Any: + return {'holds': data} if isinstance(data, str) else data + + @classmethod + @override + def __get_pydantic_json_schema__(cls, core_schema: CoreSchema, handler: GetJsonSchemaHandler) -> JsonSchemaValue: + """The published schema admits the bare string the one-line form is written as.""" + return _also_written_as(core_schema, handler, {'type': 'string'}) + + @model_serializer + def _as_written(self) -> str | dict[str, str]: + if self.description is None: + return self.holds + return {'holds': self.holds, 'description': self.description} + + class PiecewiseLink(_StrictBlock): """One link of a piecewise block: an expression pinned to a values curve. @@ -582,7 +624,7 @@ def _is_absent(value: Any) -> bool: class Spec(_StrictBlock): """The declared math — one YAML file, or one dict, validated. Nothing here has seen data. - The API is the ten declaration sections plus ``version`` and + The API is the eleven 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. In goes through ``to_spec``, which raises @@ -620,6 +662,7 @@ class Spec(_StrictBlock): macros: dict[str, MacroBlock] = {} piecewise: dict[str, PiecewiseBlock] = {} sos: dict[str, SosBlock] = {} + checks: dict[str, CheckBlock] = {} def targeted_of(self, dimension: str) -> dict[str, str]: """The groupable lookups over *dimension*: name -> the dim they map into.""" diff --git a/src/math_spec/piecewise.py b/src/math_spec/piecewise.py index e46ac16a..99bff4b2 100644 --- a/src/math_spec/piecewise.py +++ b/src/math_spec/piecewise.py @@ -101,8 +101,8 @@ def declaration_of(expanded: ExpandedPiecewise) -> PiecewiseDeclaration: curvature = _curvature_required(pw) if curvature is not None: x, y = pw.curve - checks.append(Increasing(x.values, pw.over)) - checks.append(Curved(x.values, y.values, pw.over, curvature)) + checks.append(Increasing(x.values, pw.over, pw.method)) + checks.append(Curved(x.values, y.values, pw.over, curvature, pw.method)) if pw.method == 'lp': checks.append(AtLeastTwo(pw.over, expanded.points)) if expanded.points is not None: diff --git a/src/math_spec/program.py b/src/math_spec/program.py index 5fcdc062..a0271f76 100644 --- a/src/math_spec/program.py +++ b/src/math_spec/program.py @@ -98,6 +98,7 @@ 'FirstOf', 'Footprint', 'GroupSum', + 'Holds', 'Increasing', 'LastOf', 'LookupDeclaration', @@ -558,10 +559,11 @@ class LastOf: @dataclass(frozen=True) class Increasing: - """*parameter* is strictly increasing along *over* within each curve — the x-axis a method sorts by.""" + """*parameter* is strictly increasing along *over* within each curve — the x-axis *method* sorts by.""" parameter: str over: str + method: _model.PiecewiseMethod @dataclass(frozen=True) @@ -576,6 +578,7 @@ class Curved: y: str over: str curvature: _model.Curvature + method: _model.PiecewiseMethod @dataclass(frozen=True) @@ -596,11 +599,36 @@ class Contiguous: values: str | None -#: What a ``piecewise:`` block assumes of the numbers it is bound to. The data -#: decides whether each holds, so the language names the condition with its -#: subjects and its sentence (:func:`check_message`), and the consumer holding -#: the numbers checks. Closed, like :data:`Derivation`. -Check = Increasing | Curved | AtLeastTwo | Contiguous +@dataclass(frozen=True) +class Holds: + """The predicate a ``checks:`` block declares, read over *dims*. + + The only member the file writes: the others are what a ``piecewise:`` + block's own shape assumes. + + Attributes: + holds: The condition, resolved. Never a literal: one the data cannot + decide is refused at load. + dims: The coordinates it is asked at, from the names in the predicate — + a check has no frame to declare, so its rows are the ones it spans, + and empty dims are one question rather than none. + description: The file's own sentence, or ``None``. The one place a + program keeps prose: for every other declaration a description is + for the typeset page, and here it is the second half of the + refusal a consumer raises (:func:`check_message`). + """ + + holds: WhereNode + dims: tuple[str, ...] + description: str | None = None + + +#: A condition on the numbers a model is bound to — what a ``piecewise:`` +#: block assumes of its curve, and what a ``checks:`` block declares outright. +#: The data decides whether each holds, so the language names the condition +#: with its subjects and its sentence (:func:`check_message`), and the consumer +#: holding the numbers checks. Closed, like :data:`Derivation`. +Check = Increasing | Curved | AtLeastTwo | Contiguous | Holds @dataclass(frozen=True) @@ -626,37 +654,46 @@ class PiecewiseDeclaration: checks: tuple[Check, ...] -def check_message(block: str, pw: PiecewiseDeclaration, check: Check) -> str: - """The sentence a consumer raises when the data bound to *block* fails *check*. +def check_message(context: str, check: Check) -> str: + """The sentence a consumer raises when the data fails *check*. The language's own wording, so every consumer refuses in the same words; a consumer appends what it saw. + + Args: + context: What is being checked, as a refusal names it — ``piecewise + 'cost_curve'`` for a block's own assumption, ``check 'weights'`` + for one the file declares. + check: The condition that failed. """ - ctx = f"piecewise '{block}'" match check: - case Increasing(parameter, over): + case Increasing(parameter, over, method): return ( - f"{ctx}: method: {pw.method} requires strictly increasing breakpoints in '{parameter}' along '{over}'" + f"{context}: method: {method} requires strictly increasing breakpoints in '{parameter}' along '{over}'" ) - case Curved(x, y, over, curvature): + case Curved(x, y, over, curvature, method): shape = 'a single bend' if curvature == 'either' else f'a {curvature} curve' return ( - f"{ctx}: method: {pw.method} is exact only for {shape}, and '{y}' over '{x}' along " + f"{context}: method: {method} is exact only for {shape}, and '{y}' over '{x}' along " f"'{over}' is not one, so the answer is wrong rather than loose. Use method: adjacency " f'or sos2, which take a curve of any shape.' ) case AtLeastTwo(): return ( - f'{ctx}: method: lp needs at least two breakpoints per curve — the method *is* its segment ' + f'{context}: method: lp needs at least two breakpoints per curve — the method *is* its segment ' f'lines, so a curve with no segment states nothing and leaves the bounded link on its own ' f'bound. Use method: adjacency, sos2 or convex, which pin it to the points it does have.' ) case Contiguous(mask, values): return ( - f"{ctx}: points: '{values if values is not None else mask}' must mark a consecutive run of at " + f"{context}: points: '{values if values is not None else mask}' must mark a consecutive run of at " f'least one breakpoint per curve — the chord row joins a breakpoint to the one before it, and ' f"the domain rows sit on the curve's own first and last." ) + case Holds(description=None): + return f'{context}: the data does not satisfy it' + case Holds(description=description): + return f'{context}: the data does not satisfy it — {description}' case _: assert_never(check) @@ -814,6 +851,10 @@ 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, ExpressionNode] = MappingProxyType({}) + #: Each ``checks:`` block the file wrote. Not part of the program a solver + #: sees either — a check builds no row — but carried with it, because the + #: consumer that binds the data is the only one that can answer one. + checks: Mapping[str, Holds] = MappingProxyType({}) def __post_init__(self) -> None: """Seal every group, so a program handed out cannot be written to. diff --git a/src/math_spec/typesetting/__init__.py b/src/math_spec/typesetting/__init__.py index aaa393c1..3cfd4e11 100644 --- a/src/math_spec/typesetting/__init__.py +++ b/src/math_spec/typesetting/__init__.py @@ -73,6 +73,7 @@ def typeset( symbols: str | Path | Mapping[str, Any] | SymbolTable | None = None, standalone: bool = False, legend: bool = True, + checks: bool = True, numbered: bool = True, ) -> str: """Render *model*'s math in *fmt*. @@ -87,6 +88,9 @@ def typeset( legend: Prepend the sets/parameters/variables table. The model's own ``description:`` opens the document either way — it is what the file says it is, not a symbol table. + checks: Append the data conditions the model declares. They are + conditions on the *input*, not rows a solver holds, so a page + about the math alone leaves them out. numbered: Number the equations. Returns: @@ -108,6 +112,8 @@ def typeset( ('Subject to', walk.constraints()), ('Variable domains', walk.variables()), ] + if checks: + sections.append(('Data conditions', walk.checks())) rendered = [fmt.section(title, fmt.equations(lines, numbered=numbered)) for title, lines in sections if lines] blocks = [fmt.note(fmt.escape(schema.description))] if schema.description else [] diff --git a/src/math_spec/typesetting/walk.py b/src/math_spec/typesetting/walk.py index 2905c1f8..07cd4adf 100644 --- a/src/math_spec/typesetting/walk.py +++ b/src/math_spec/typesetting/walk.py @@ -15,7 +15,7 @@ from dataclasses import dataclass, field, replace from typing import TYPE_CHECKING, assert_never -from math_spec.dimensions import dims_of +from math_spec.dimensions import dims_of, where_dims from math_spec.expression_parser import ( ArithmeticNode, BinaryOperatorNode, @@ -663,6 +663,29 @@ def _sorted(self, dims: frozenset[str]) -> list[str]: # -- legend ------------------------------------------------------------ + def checks(self) -> list[Line]: + """One line per ``checks:`` block — a condition on the data, not a row. + + It prints as the predicate it is, quantified over the coordinates its + own names span: the reader believing the constraints above has to + believe these of the table first. + """ + lines = [] + for name, block in self.schema.checks.items(): + node = where_of(block.holds, self.namespace, f"check '{name}'") + assert node is not None, 'load-time validation refuses a check that holds whatever the data says' + dims = sorted(where_dims(node, self.schema)) + ctx = self.context(frame=dims) + lines.append( + Line( + label=name, + left=self.where(node, ctx), + right='', + condition=self.quantifier(dims, ''), + ) + ) + return lines + def glossaries(self) -> list[Glossary]: fmt = self.format sets = [ diff --git a/src/math_spec/validation.py b/src/math_spec/validation.py index 1021bd83..0d6f5228 100644 --- a/src/math_spec/validation.py +++ b/src/math_spec/validation.py @@ -28,10 +28,18 @@ UnaryOperatorNode, VariableNode, ) -from math_spec.model import Spec +from math_spec.model import CheckBlock, Spec from math_spec.operators import BUILTINS, unknown_operator_message -from math_spec.resolution import Namespace, resolve_expression, resolve_where -from math_spec.where_parser import parse_where +from math_spec.resolution import Namespace, resolve_expression, resolve_where, where_of +from math_spec.where_parser import ( + AndNode, + BooleanLiteralNode, + NotNode, + OrNode, + VariableDefinedNode, + WhereNode, + parse_where, +) def to_spec(model: str | Path | dict[str, Any] | Spec) -> Spec: @@ -111,6 +119,9 @@ def validate_expressions(schema: Spec) -> None: if schema.objective is not None: _check_expression(schema.objective.expression, schema, ns, 'The objective', errors, comparison=False, ceiling=2) + for kname, kdef in schema.checks.items(): + _check_check(kname, kdef, ns, errors) + if errors: raise SchemaError('\n'.join(errors)) @@ -163,6 +174,49 @@ def _check_expression( errors.append(str(e)) +def _check_check(name: str, block: CheckBlock, ns: Namespace, errors: list[str]) -> None: + """A check is a predicate over data alone, and one that data cannot decide is a mistake the file can see. + + Folding is what makes the second half reachable: ``where_of`` reduces a + predicate the connectives settle to a literal, so a check no table can + fail arrives as ``None`` and one no table can pass as ``False``. + """ + context = f"Check '{name}'" + try: + folded = where_of(block.holds, ns, context) + except ValueError as e: + errors.append(_prefixed(context, e)) + return + if variables := sorted(_variables_in(folded)): + errors.append( + f'{context}: reads variable(s) {variables}, and a check is a condition on the data, ' + f'settled before any variable has a value. Test the parameters the variable is ' + f'built from, or make it a constraint.' + ) + return + if folded is None: + errors.append( + f'{context}: holds at every coordinate whatever the data says, so it checks nothing. ' + f'Write the condition the data could break, or drop the check.' + ) + elif isinstance(folded, BooleanLiteralNode): + errors.append( + f'{context}: no data satisfies it, so every table is refused. Write the condition ' + f'the data could meet, or drop the check.' + ) + + +def _variables_in(node: WhereNode | None) -> set[str]: + """Every variable a predicate reads — empty for one that reads only data.""" + if isinstance(node, VariableDefinedNode): + return {node.name} + if isinstance(node, NotNode): + return _variables_in(node.operand) + if isinstance(node, (AndNode, OrNode)): + return _variables_in(node.left) | _variables_in(node.right) + return set() + + def _check_where( text: str | None, ns: Namespace, diff --git a/tests/test_lowering.py b/tests/test_lowering.py index 492fd192..527d6e7a 100644 --- a/tests/test_lowering.py +++ b/tests/test_lowering.py @@ -23,7 +23,7 @@ import pytest -from math_spec import LanguageError, Spec +from math_spec import LanguageError, Spec, to_program, to_spec from math_spec.expression_parser import FunctionCallNode, NumberNode from math_spec.lowering import _Lowering, lower_program from math_spec.piecewise import expand_piecewise @@ -47,6 +47,7 @@ Translate, Variable, Window, + check_message, divisor_parameters, fan_in, quotients, @@ -677,3 +678,40 @@ def test_a_dimension_carries_the_dtype_its_labels_are_checked_against(): assert program.dimension('t').dtype == 'int', 'a declared dtype reaches the plan' assert program.dimension('g').dtype == 'str', "and the schema's default does too, rather than nothing" + + +def test_a_check_lowers_to_the_predicate_and_the_coordinates_it_is_asked_at(): + program = to_program( + override( + SMALL_MODEL, + checks={'share': 'c > 0 AND c <= 1', 'scale': 'k >= 1'}, + ) + ) + assert list(program.checks) == ['share', 'scale'], 'checks come back in the order the file wrote them' + assert program.checks['share'].dims == ('g',), "the frame is read off the predicate's own names" + assert program.checks['scale'].dims == (), 'a scalar condition is one question, not none' + assert program.checks['share'].holds == where_of('c > 0 AND c <= 1', Namespace.of(to_spec(SMALL_MODEL)), 'x') + + +def test_a_check_builds_no_row(): + raw = override(SMALL_MODEL, constraints={'cap': {'foreach': ['g'], 'expression': 'p <= c'}}) + without = to_program(raw) + with_check = to_program(override(raw, checks={'share': 'c > 0'})) + assert with_check.constraints == without.constraints + assert with_check.expressions == without.expressions, 'a check is not among the expressions a solver sees' + + +def test_a_declared_check_and_a_piecewise_one_share_a_sentence(): + program = to_program(override(SMALL_MODEL, checks={'share': 'c > 0'})) + assert check_message("check 'share'", program.checks['share']) == "check 'share': the data does not satisfy it" + + +def test_a_checks_description_reaches_the_program_because_it_is_half_the_refusal(): + """The one prose a program keeps: a consumer reading only the program prints why the condition matters.""" + program = to_program( + override(SMALL_MODEL, checks={'share': {'holds': 'c > 0', 'description': 'a price of zero is a free good'}}) + ) + assert program.checks['share'].description == 'a price of zero is a free good' + assert check_message("check 'share'", program.checks['share']) == ( + "check 'share': the data does not satisfy it — a price of zero is a free good" + ) diff --git a/tests/test_piecewise.py b/tests/test_piecewise.py index 50be3b79..936ad9de 100644 --- a/tests/test_piecewise.py +++ b/tests/test_piecewise.py @@ -371,8 +371,8 @@ def test_a_block_is_kept_as_the_checks_a_consumer_binding_it_runs(): assert curve.breakpoints == ('bp_x', 'bp_y'), 'the values parameters, in link order' assert set(curve.checks) == { - Increasing('bp_x', 'bp'), - Curved('bp_x', 'bp_y', 'bp', 'convex'), + Increasing('bp_x', 'bp', 'lp'), + Curved('bp_x', 'bp_y', 'bp', 'convex', 'lp'), AtLeastTwo('bp', 'cost_curve_points'), Contiguous('cost_curve_points', 'bp_x'), }, 'an lp curve with a mask assumes all four, each against the names the file wrote' @@ -383,7 +383,13 @@ def test_a_block_is_kept_as_the_checks_a_consumer_binding_it_runs(): @pytest.mark.parametrize('kind', get_args(Check), ids=lambda k: k.__name__) def test_every_check_has_a_sentence(kind): + """The union is what a consumer dispatches on, so a member with no sentence is one every consumer words for itself. + + Both provenances are swept: a block assumes the first four of its curve, + and the file declares the fifth. + """ curve = to_program(override(LP, **{'piecewise.cost_curve.points': 'bp_x'})).piecewise['cost_curve'] - check = next((c for c in curve.checks if isinstance(c, kind)), None) - assert check is not None, 'the fixture is the block that assumes everything' - assert check_message('cost_curve', curve, check).startswith("piecewise 'cost_curve':") + declared = to_program(override(LP, checks={'positive': 'bp_x > 0'})).checks + found = [c for c in (*curve.checks, *declared.values()) if isinstance(c, kind)] + assert found, 'no fixture here produces this check, so nothing holds its sentence to the language' + assert check_message("piecewise 'cost_curve'", found[0]).startswith("piecewise 'cost_curve':") diff --git a/tests/test_validation.py b/tests/test_validation.py index 221780ca..8c92f0b2 100644 --- a/tests/test_validation.py +++ b/tests/test_validation.py @@ -594,3 +594,83 @@ def test_a_default_is_written_out_and_an_absence_is_not(self): assert 'upper' in written['variables']['p']['bounds'] and 'where' not in written['variables']['p'], ( 'a null and an infinite bound say nothing, so they are not written' ) + + +class TestChecks: + """A `checks:` block states a condition on the data; what the file can decide is decided at load.""" + + @pytest.mark.parametrize( + ('holds', 'fragments'), + [ + pytest.param( + 'nope > 0', + ("Check 'k1'", "'nope' not found"), + id='an-unknown-name', + ), + pytest.param( + 'p', + ("Check 'k1'", "reads variable(s) ['p']", 'make it a constraint'), + id='a-variable', + ), + pytest.param( + 'c > 0 AND p', + ("Check 'k1'", "reads variable(s) ['p']"), + id='a-variable-under-a-connective', + ), + pytest.param( + 'True', + ("Check 'k1'", 'checks nothing'), + id='a-condition-every-table-passes', + ), + pytest.param( + 'c > 0 OR True', + ("Check 'k1'", 'checks nothing'), + id='a-condition-the-connectives-settle-true', + ), + pytest.param( + 'False', + ("Check 'k1'", 'no data satisfies it'), + id='a-condition-no-table-passes', + ), + pytest.param( + 'c > 0 AND False', + ("Check 'k1'", 'no data satisfies it'), + id='a-condition-the-connectives-settle-false', + ), + ], + ) + def test_a_check_the_file_can_refute_is_refused_at_load(self, holds, fragments): + with pytest.raises(LanguageError) as exc: + _schema(checks={'k1': holds}) + for fragment in fragments: + assert fragment in str(exc.value) + + @pytest.mark.parametrize( + 'holds', + [ + pytest.param('c > 0', id='over-a-dimension'), + pytest.param('k >= 1', id='scalar'), + pytest.param('c > 0 AND c <= 1', id='a-conjunction'), + pytest.param('flag', id='a-boolean-parameter'), + pytest.param('tag != "wind"', id='a-label-space'), + pytest.param('NOT flag OR c > 0', id='a-connective-the-data-decides'), + ], + ) + def test_a_condition_the_data_decides_loads(self, holds): + assert _schema(checks={'k1': holds}).checks['k1'].holds == holds + + def test_a_check_is_written_as_a_bare_string_or_a_mapping(self): + schema = _schema( + checks={'bare': 'c > 0', 'described': {'holds': 'k >= 1', 'description': 'the scale is positive'}} + ) + assert schema.checks['bare'].description is None + assert schema.checks['described'].description == 'the scale is positive' + + def test_a_check_round_trips_through_yaml_in_the_form_it_was_written(self): + schema = _schema( + checks={'bare': 'c > 0', 'described': {'holds': 'k >= 1', 'description': 'the scale is positive'}} + ) + assert to_spec(parse_yaml(schema.to_yaml())).to_dict() == schema.to_dict() + assert parse_yaml(schema.to_yaml())['checks']['bare'] == 'c > 0', ( + 'a check with no description serialises back to the bare string it was written as' + ) diff --git a/tests/typesetting/golden/latex.out b/tests/typesetting/golden/latex.out index bd0090ca..ddf3a2c0 100644 --- a/tests/typesetting/golden/latex.out +++ b/tests/typesetting/golden/latex.out @@ -113,4 +113,10 @@ \text{weight sos} && \left( \mathit{weight}_{t,g} \right)_{g \in \mathcal{G}} & \in \mathrm{SOS}2 && \forall\, t \in \mathcal{T} \end{align} +\paragraph{Data conditions} +\begin{align} +\text{availability\_is\_a\_share} && \mathrm{p}^{\mathrm{max}}_{g} > 0 \wedge \mathrm{eta}_{g} \le 1 & && \forall\, g \in \mathcal{G} \\ +\text{the\_budget\_is\_real} && \mathrm{budget} \ge 0 +\end{align} + \end{document} diff --git a/tests/typesetting/golden/markdown.out b/tests/typesetting/golden/markdown.out index f7eb4410..bb24e235 100644 --- a/tests/typesetting/golden/markdown.out +++ b/tests/typesetting/golden/markdown.out @@ -222,3 +222,13 @@ $$0 \le \mathit{weight}_{t,g} \le 1 \qquad \forall\thinspace t \in \mathcal{T},\ **`weight sos`** $$\left( \mathit{weight}_{t,g} \right)_{g \in \mathcal{G}} \in \mathrm{SOS}2 \qquad \forall\thinspace t \in \mathcal{T}$$ + +#### Data conditions + +**`availability_is_a_share`** + +$$\mathrm{p}^{\mathrm{max}}_{g} > 0 \wedge \mathrm{eta}_{g} \le 1 \qquad \forall\thinspace g \in \mathcal{G}$$ + +**`the_budget_is_real`** + +$$\mathrm{budget} \ge 0$$ diff --git a/tests/typesetting/golden/model.yaml b/tests/typesetting/golden/model.yaml index eec16c95..60ad2af4 100644 --- a/tests/typesetting/golden/model.yaml +++ b/tests/typesetting/golden/model.yaml @@ -183,3 +183,9 @@ constraints: objective: # a sense, a product of two variables, a power over two parameters, a power of one of those, and the summations a scalar objective spells out beside two scalar terms sense: maximize expression: sum(p * cost) + sum(p * p * cost) + sum(p * cost * growth ** lead) + sum(p * (growth ** lead) ** 2) + sum(p * p_max) - reserve + -headroom + +checks: # a condition on the data, printing under its own heading — one over a dimension, one scalar + availability_is_a_share: + holds: "p_max > 0 AND eta <= 1" + description: a generator with no headroom is a row that decides nothing, and no unit gains energy + the_budget_is_real: "budget >= 0" # scalar, so the line carries no quantifier at all diff --git a/tests/typesetting/golden/typst.out b/tests/typesetting/golden/typst.out index a4cc2645..136f34a0 100644 --- a/tests/typesetting/golden/typst.out +++ b/tests/typesetting/golden/typst.out @@ -99,3 +99,8 @@ $ upright("p") & upright("p")^(upright("min"))_(g) <= p_(t,g) & <= upright("p")^ upright("headroom") & italic("headroom") & >= 0 & upright("where ") upright("budget") upright(" is defined") \ upright("weight") & 0 <= italic("weight")_(t,g) & <= 1 & forall t in cal(T), g in cal(G) \ upright("weight sos") & (italic("weight")_(t,g))_(g in cal(G)) & in upright("SOS")2 & forall t in cal(T) $ + +== Data conditions +#set math.equation(numbering: "(1)") +$ upright("availability_is_a_share") & upright("p")^(upright("max"))_(g) > 0 and upright("eta")_(g) <= 1 & & forall g in cal(G) \ + upright("the_budget_is_real") & upright("budget") >= 0 $ diff --git a/tests/typesetting/test_cli.py b/tests/typesetting/test_cli.py index 923b47c7..6745e2e7 100644 --- a/tests/typesetting/test_cli.py +++ b/tests/typesetting/test_cli.py @@ -163,3 +163,15 @@ def test_no_verb_binds_data(): for name, verb in _verbs().items(): flags = {option for action in verb._actions for option in action.option_strings} assert not (flags & banned), f'{name} binds data: {sorted(flags & banned)}' + + +def test_each_section_switch_drops_its_own_section(capsys): + """`--no-legend` and `--no-checks` are the two the front offers, and neither reaches the other's section.""" + assert front.main(['markdown', MODEL, '--no-checks']) == 0 + without_checks = capsys.readouterr().out + assert front.main(['markdown', MODEL, '--no-legend']) == 0 + without_legend = capsys.readouterr().out + + assert 'Data conditions' not in without_checks + assert 'Parameters' in without_checks, 'the legend is still there' + assert 'Data conditions' in without_legend, 'the checks are still there' diff --git a/tests/typesetting/test_walk.py b/tests/typesetting/test_walk.py index 91ae13c4..ea959f77 100644 --- a/tests/typesetting/test_walk.py +++ b/tests/typesetting/test_walk.py @@ -723,3 +723,31 @@ def test_a_string_value_in_a_where_prints_as_a_quoted_label(fmt: Format): text = typeset(model, fmt, legend=False) assert fmt.quoted('gas_ccgt') in text, 'a string value prints through the quoted seam' assert fmt.prose('gas_ccgt') not in text, 'a string value is data, never words inside math' + + +@EVERY_FORMAT +def test_a_check_prints_as_the_predicate_under_its_own_heading(fmt: Format): + """A construct the loader admits, the typesetter renders — and a data + condition is a mathematical statement, so it reads as one rather than as a + note beside the model.""" + model = override(DISPATCH_MODEL, checks={'costs_are_priced': 'cost > 0'}) + text = typeset(model, fmt, legend=False) + assert 'Data conditions' in text + assert fmt.operators['forall'] in text.split('Data conditions')[1], ( + 'a check over a dimension is quantified over the coordinates its own names span' + ) + + +@EVERY_FORMAT +def test_a_model_with_no_checks_prints_no_heading_for_them(fmt: Format): + assert 'Data conditions' not in typeset(DISPATCH_MODEL, fmt, legend=False) + + +@EVERY_FORMAT +def test_the_data_conditions_are_left_out_on_request(fmt: Format): + """They are conditions on the input rather than rows a solver holds, so a page about the math alone drops them.""" + model = override(DISPATCH_MODEL, checks={'costs_are_priced': 'cost > 0'}) + assert 'Data conditions' not in typeset(model, fmt, legend=False, checks=False) + assert typeset(model, fmt, legend=False, checks=False) == typeset(DISPATCH_MODEL, fmt, legend=False), ( + 'dropping the section leaves the math byte-identical to the same model without checks' + )