diff --git a/docs/about/limits.md b/docs/about/limits.md index a95a0fb3..91eb2395 100644 --- a/docs/about/limits.md +++ b/docs/about/limits.md @@ -112,22 +112,28 @@ second kind. `min_up_time` is a column the model already binds, so `sum_back(window=min_up_time)` reads the width off the column and you ship no window mask. +Checking a column is neither. `p_min <= p_max` is a rule two consumers must not +answer differently, so the rule is +[language](../reference/language/assumptions.md) and the check is the +consumer's. The file states the predicate, and whoever binds the numbers runs +it. + ## Deliberate non-primitives What has been asked for and refused, with the reason and what to write instead. That another tool has a feature is not by itself a reason to add it. -| Request | Why refused | Instead | -| ------------------------------------------------------------------------ | ------------------------------------------------------------------------------------------------------------------------------------------ | ---------------------------------------------------------------------------------------------------------------------------------- | -| Resampling, clustering, file IO, unit conversion | not math | do it in data preparation, and pass a parameter | -| Unit checking at load | a `unit: MW` on a parameter is a claim that nothing checks against the column, and it needs a grammar of units the language then maintains | convert to one unit system in data preparation, and name it in the `description:` | -| Array operations such as `merge` and `reindex` | there is no end to them | data preparation | -| Helpers for one domain, such as `reduce_carrier_dim` | writes one field's vocabulary into the language | a component library of macros over the operators that exist | -| A vocabulary for tracked metrics: `impacts:`, `effects:`, a `costs` axis | a named expression already does this | an `impact` dimension and one named expression. Cap it with a constraint, weight it in the objective, read it back after the solve | -| `**` with a variable in the base or the exponent | the exponent would decide the degree, and `to_spec` reads no data | `x * x` for a square. `**` over parameters and numbers is allowed | -| Normalisation, `x / sum(x)` | dividing by a variable is not a polynomial, and no solver takes it | write the ratio as a constraint, or fix the denominator | -| An `if`, a loop, or declarations that depend on the data | `to_spec` could no longer read the file without the data | `where:` masks and `dims:` dimensions. A tool may loop over models | -| A Python API for building models | the model is the file you review and diff | YAML, or a `dict` with the same keys ([below](#composition-component-libraries)) | +| Request | Why refused | Instead | +| ------------------------------------------------------------------------ | ------------------------------------------------------------------------------------------------------------------------------------------ | ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| Resampling, clustering, file IO, unit conversion | not math | do it in data preparation, and pass a parameter | +| Unit checking at load | a `unit: MW` on a parameter is a claim that nothing checks against the column, and it needs a grammar of units the language then maintains | convert to one unit system in data preparation, and name it in the `description:`. A range the data has to meet is an [`assumptions:`](../reference/language/assumptions.md) entry | +| Array operations such as `merge` and `reindex` | there is no end to them | data preparation | +| Helpers for one domain, such as `reduce_carrier_dim` | writes one field's vocabulary into the language | a component library of macros over the operators that exist | +| A vocabulary for tracked metrics: `impacts:`, `effects:`, a `costs` axis | a named expression already does this | an `impact` dimension and one named expression. Cap it with a constraint, weight it in the objective, read it back after the solve | +| `**` with a variable in the base or the exponent | the exponent would decide the degree, and `to_spec` reads no data | `x * x` for a square. `**` over parameters and numbers is allowed | +| Normalisation, `x / sum(x)` | dividing by a variable is not a polynomial, and no solver takes it | write the ratio as a constraint, or fix the denominator | +| An `if`, a loop, or declarations that depend on the data | `to_spec` could no longer read the file without the data | `where:` masks and `dims:` dimensions. A tool may loop over models | +| A Python API for building models | the model is the file you review and diff | YAML, or a `dict` with the same keys ([below](#composition-component-libraries)) | ## Composition (component libraries) diff --git a/docs/examples/commitment.md b/docs/examples/commitment.md index 901182f9..20e026e6 100644 --- a/docs/examples/commitment.md +++ b/docs/examples/commitment.md @@ -79,6 +79,16 @@ constraints: dispatch - shift(dispatch, along=snapshot, offset=1, edge=0) <= ramp_limit * previous_status + start_up_limit * (1 - previous_status) +assumptions: + output_floor_fits_under_the_cap: + holds: "min_output <= capacity" + where: "committable" + description: >- + `lower` and `upper` hold one dispatch between them, so a floor above the + cap makes a running unit infeasible rather than expensive. A unit that + cannot be switched off is held to its floor in every snapshot, so the + check is the committable ones'. + objective: sense: minimize expression: sum(dispatch * cost) @@ -178,6 +188,14 @@ $`\mathrm{pos}(t)`$ denotes where index $`t`$ sits along its dimension's own ord ```math \mathit{status}_{t,g} \in \{0, 1\} \qquad \forall\, t \in \mathcal{T},\ g \in \mathcal{G} ``` + +#### Assumptions + +**`output_floor_fits_under_the_cap`** + +```math +\mathrm{min\_output}_{g} \le \mathrm{capacity}_{g} \qquad \forall\, g \in \mathcal{G} \,:\, \mathrm{committable}_{g} +``` Regenerate with `pixi run python -m tools.gallery`. diff --git a/docs/reference/language/assumptions.md b/docs/reference/language/assumptions.md new file mode 100644 index 00000000..35ae4280 --- /dev/null +++ b/docs/reference/language/assumptions.md @@ -0,0 +1,131 @@ + + +# Assumptions + +`assumptions:` states what the model expects of the data it is bound to. The +language reads no data, so it checks nothing here. It types the predicate, +carries it on the program, and prints it in the +[typeset document](../typeset.md). The consumer that binds the numbers runs +each one, and refuses the data that fails it. + +```yaml +dimensions: + generator: { dtype: str } +parameters: + p_min: { dims: [generator] } + p_max: { dims: [generator] } +variables: + p: + dims: [generator] + bounds: { lower: p_min, upper: p_max } +constraints: + cap: + dims: [generator] + expression: p <= p_max +objective: + sense: minimize + expression: sum(p, over=generator) +assumptions: + bounds_do_not_cross: "p_min <= p_max" +``` + +$$\mathrm{p}^{\mathrm{min}}_{g} \le \mathrm{p}^{\mathrm{max}}_{g} \qquad \forall\thinspace g \in \mathcal{G}$$ + +## The entry + +An entry is one where string, or a mapping once it carries more than the +predicate. + +| Field | | | +| ------------- | ----------------------------------------------------------------------------- | -------------- | +| `holds` | required. The predicate, in the [where grammar](expressions.md#where-strings) | | +| `where` | which coordinates it is checked at, in the same grammar | default `null` | +| `description` | why the rule is there. A refusal quotes it | default `null` | + +`bounds_do_not_cross: "p_min <= p_max"` above is the short form of +`bounds_do_not_cross: { holds: "p_min <= p_max" }`. + +A `description:` says why the rule is there. The sentence a consumer refuses +with quotes it, so a failure names the columns and the reason. + +There is no `dims:`. The predicate holds at every coordinate of the product of +the dimensions its two masks name. A predicate narrower than that broadcasts, +as it does in any `where`. + +## What a predicate may say + +Everything the [where grammar](expressions.md#where-strings) admits, which +includes arithmetic on either side: + +```yaml +dimensions: + snapshot: { dtype: int } + generator: { dtype: str } +parameters: + eta: { dims: [generator] } + p_max: { dims: [generator] } + peak: { dims: [] } + load: { dims: [snapshot] } + ramp_limit: { dims: [] } +variables: + p: + dims: [snapshot, generator] + bounds: { lower: 0, upper: p_max } +constraints: + meet_load: + dims: [snapshot] + expression: sum(p, over=generator) == load +objective: + sense: minimize + expression: sum(p) +assumptions: + efficiency_is_a_fraction: "eta > 0 AND eta <= 1" + peak_is_reachable: "sum(p_max, over=generator) >= peak" + ramps_are_gentle: + holds: "load - shift(load, along=snapshot, offset=1, edge=0) <= ramp_limit" + where: "position(snapshot) > 0" + description: the first snapshot has no predecessor to ramp from +``` + +A `where:` narrows which coordinates are checked. A parameter supplied only +where it applies takes one, so the rows it has no value at are not held to the +predicate. + +## What the loader refuses + +**A predicate the connectives already decide.** It reads no data, so it is +either a claim about nothing or a claim no data can meet: + +> `Assumption 'sound'`: the predicate `'c > 0 OR true'` folds to true, so it +> assumes nothing of the data. Delete it, or name a parameter it constrains. + +A `where:` the connectives decide is refused the same way: one that folds to +true narrows nothing, and one that folds to false checks the entry on no row. + +**A variable.** An assumption is about the numbers the caller binds, and a +variable is what the solver decides from them: + +> `Assumption 'sound'`: variable `'p'` stands in what the assumption assumes, +> and an assumption is about the data — a variable is what the solver decides +> from it. Name a parameter, or state the rule as a constraint. + +A rule that binds a decision is a [constraint](declarations.md#constraints). +A constraint whose sides carry no variable is refused, and its message names +this section. + +## What a curve assumes + +A [`piecewise:`](piecewise.md) block puts its own conditions on the numbers. +Its breakpoints increase along the curve, and the shape is the one its +`method:` is exact for. The language derives both from the method, not from +anything the file writes, and carries them beside the written ones under the +name a refusal quotes. A `method: convex` block called `curve` adds +`curve increasing` and `curve curvature`. + +Both kinds print under one _Assumptions_ heading, because a reader checking +the data against the document checks all of them. +[Reading a loaded model](../reading.md#what-the-data-has-to-satisfy) says how +a consumer runs them. diff --git a/docs/reference/language/expressions.md b/docs/reference/language/expressions.md index e785e38c..57b3e5fa 100644 --- a/docs/reference/language/expressions.md +++ b/docs/reference/language/expressions.md @@ -75,7 +75,8 @@ Position decides which kinds of name are legal: A bare word in the value of a keyword argument is a name to resolve, which is why `wrap` is quoted. A keyword's key is never a name. -Constraints sit outside the flat namespace, so a model may name a constraint +Constraints and assumptions sit outside the flat namespace, because no +expression names either, so a model may name a constraint or an assumption after a variable. The objective has no name at all. ## How dimensions combine diff --git a/docs/reference/language/file.md b/docs/reference/language/file.md index f27062a3..2e52c196 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 **ten declaration keys**, plus `version` -and `description`. Any subset of the ten is accepted. +A model file is a YAML mapping with **eleven declaration keys**, plus +`version` and `description`. Any subset of the eleven is accepted. | Key | | | ------------- | ------------------------------------------------------------------------------------------------- | @@ -20,6 +20,7 @@ and `description`. Any subset of the ten is accepted. | `macros` | templates that take arguments ([macros](named.md#macros)) | | `piecewise` | piecewise-linear curves ([piecewise](piecewise.md)) | | `sos` | special-ordered sets ([sos](piecewise.md#sos)) | +| `assumptions` | what the model expects of its data ([assumptions](assumptions.md)) | A file with no `objective` is a **feasibility problem**: it asks whether the constraints can all be met. diff --git a/docs/reference/language/index.md b/docs/reference/language/index.md index 07454afa..bab5b195 100644 --- a/docs/reference/language/index.md +++ b/docs/reference/language/index.md @@ -42,7 +42,7 @@ That file is a complete model. The pages below give the exact rules. | | | | ----------------------------------------------------------------------- | ------------------------------------------------------------------------- | -| [File shape](file.md) | the ten keys, `version` and `description` | +| [File shape](file.md) | the eleven keys, `version` and `description` | | [Dimensions](dimensions.md) | the axes | | [Relations](relations.md) | the maps from one axis onto another | | [Parameters, variables, constraints and the objective](declarations.md) | the four blocks that carry the math | @@ -51,6 +51,7 @@ That file is a complete model. The pages below give the exact rules. | [Operators](operators.md) | `sum`, `sum_back`, `at` and `shift` | | [Absence and `where`](absence.md) | which rows are built, and which are not | | [Piecewise curves and SOS](piecewise.md) | `piecewise:` and `sos:` | +| [Assumptions](assumptions.md) | what the model expects of the data it is bound to | | [Errors and limits](errors.md) | what fails when, and what the language will not express | ## The ten rules @@ -60,7 +61,7 @@ message that names the fix. These are the rules it checks. | # | Rule | | | --- | --------------------------------------------------------------------------------------------------------------------------------------------------------------------- | --------------------------------------------------------------- | -| 1 | A file has ten declaration keys, plus `version` and `description`. An unknown key is refused, with the nearest valid key named. | [File shape](file.md) | +| 1 | A file has eleven declaration keys, plus `version` and `description`. An unknown key is refused, with the nearest valid key named. | [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. | [Names](expressions.md#name-resolution) | | 4 | Where a name may stand depends on what it is. A dimension follows `over=` or `along=`, and is never multiplied. | [Names](expressions.md#name-resolution) | diff --git a/docs/reference/language/piecewise.md b/docs/reference/language/piecewise.md index 92e84a85..3551257b 100644 --- a/docs/reference/language/piecewise.md +++ b/docs/reference/language/piecewise.md @@ -57,6 +57,12 @@ is what the rest of the model sees, and what the The breakpoint order is the declared order of `over`. A curve whose breakpoints decrease in that order is refused when the data binds. +Every condition this page says is checked "when the data binds" is an +[assumption](assumptions.md). The language derives each one from the `method:` +rather than from anything the file writes, carries it beside the assumptions +the file did write, and prints both under one heading. The consumer that binds +the numbers runs them. + !!! warning "A values parameter short of a row does not build a shorter curve" The missing row reads as a breakpoint at the origin, and the table is diff --git a/docs/reference/notation.md b/docs/reference/notation.md index e3395367..c2f4a61c 100644 --- a/docs/reference/notation.md +++ b/docs/reference/notation.md @@ -45,6 +45,7 @@ dimensions: zone: { dtype: str } season: { dtype: str } technology: { dtype: str } + bp: { dtype: int } # the breakpoint axis the two curves run along relations: gen_bus: { key: generator, values: bus } @@ -69,6 +70,10 @@ parameters: lead: { dims: [generator], dtype: int } budget: { dims: [] } # scalar: the legend says so rather than printing an empty product growth: { dims: [] } # the base of a power; the exponent is `lead`, a column + bp_x: { dims: [bp] } # the masked curve's x-axis, and the parameter its mask is derived from + bp_y: { dims: [bp] } + heat_x: { dims: [bp] } # the whole-axis curve, bounded the other way + heat_y: { dims: [bp] } ``` #### Sets @@ -81,6 +86,7 @@ parameters: | $`\mathcal{Z}`$ | index $`z`$ — `zone` with $`\mathrm{zone\_of}: \mathcal{B} \to \mathcal{Z},\ \mathrm{area\_of}: \mathcal{B} \to \mathcal{Z},\ \mathrm{gen\_zone}: \mathcal{G} \times \mathcal{T} \to \mathcal{Z}`$ | | $`\mathcal{S}`$ | index $`s`$ — `season` with $`\mathrm{season\_of}: \mathcal{T} \to \mathcal{S}`$ | | $`\mathcal{E}`$ | index $`e`$ — `technology` with $`\mathrm{gen\_bt}: \mathcal{G} \to \mathcal{B} \times \mathcal{E}`$ | +| $`\mathcal{A}`$ | index $`a`$ — `bp` | #### Parameters @@ -98,6 +104,13 @@ parameters: | $`\mathrm{lead}`$ | `lead` over $`\mathcal{G}`$ | | $`\mathrm{budget}`$ | `budget` (scalar) | | $`\mathrm{growth}`$ | `growth` (scalar) | +| $`\mathrm{bp\_x}`$ | `bp_x` over $`\mathcal{A}`$ | +| $`\mathrm{bp\_y}`$ | `bp_y` over $`\mathcal{A}`$ | +| $`\mathrm{heat}^{\mathrm{x}}`$ | `heat_x` over $`\mathcal{A}`$ | +| $`\mathrm{heat}^{\mathrm{y}}`$ | `heat_y` over $`\mathcal{A}`$ | +| $`\mathrm{fuel}^{\mathrm{curve,points}}`$ | `fuel_curve_points` over $`\mathcal{A}`$ — where 'bp\_x' has a row, and so where the curve runs | +| $`\mathrm{fuel}^{\mathrm{curve,starts}}`$ | `fuel_curve_starts` over $`\mathcal{A}`$ — the first breakpoint of each curve | +| $`\mathrm{fuel}^{\mathrm{curve,ends}}`$ | `fuel_curve_ends` over $`\mathcal{A}`$ — the last breakpoint of each curve | #### Variables @@ -113,6 +126,10 @@ parameters: | $`\mathit{reserve}`$ | `reserve` (scalar) | | $`\mathit{headroom}`$ | `headroom` (scalar) | | $`\mathit{weight}`$ | `weight` over $`\mathcal{T} \times \mathcal{G}`$ | +| $`p^{\mathrm{bp}}`$ | `p_bp` over $`\mathcal{T}`$ | +| $`\mathit{fuel}`$ | `fuel` over $`\mathcal{T}`$ | +| $`q^{\mathrm{bp}}`$ | `q_bp` over $`\mathcal{T}`$ | +| $`\mathit{heat}`$ | `heat` over $`\mathcal{T}`$ | #### Definitions @@ -974,6 +991,62 @@ weight: 0 \le \mathit{weight}_{t,g} \le 1 \qquad \forall\, t \in \mathcal{T},\ g \in \mathcal{G} ``` +#### `p_bp` + +the masked curve's x link + +```yaml +p_bp: + dims: [snapshot] + bounds: { lower: 0, upper: 100 } +``` + +```math +0 \le p^{\mathrm{bp}}_{t} \le 100 \qquad \forall\, t \in \mathcal{T} +``` + +#### `fuel` + +its y link, bounded above, which is what makes the curve a convex one + +```yaml +fuel: + dims: [snapshot] + bounds: { lower: 0 } +``` + +```math +\mathit{fuel}_{t} \ge 0 \qquad \forall\, t \in \mathcal{T} +``` + +#### `q_bp` + +the whole-axis curve's x link + +```yaml +q_bp: + dims: [snapshot] + bounds: { lower: 0, upper: 100 } +``` + +```math +0 \le q^{\mathrm{bp}}_{t} \le 100 \qquad \forall\, t \in \mathcal{T} +``` + +#### `heat` + +its y link, bounded below, so that curve is concave + +```yaml +heat: + dims: [snapshot] + bounds: { lower: 0 } +``` + +```math +\mathit{heat}_{t} \ge 0 \qquad \forall\, t \in \mathcal{T} +``` + ### Curves, as what they expand to A curve is sugar: what prints is the formulation it expands to, which is the math the solver receives. One row per `method:`, each from the model named under it, so the symbols in this section are that model's. @@ -1114,6 +1187,16 @@ cost_curve: 0 \le \lambda_{t,g,b} \le 1 \qquad \forall\, t \in \mathcal{T},\ g \in \mathcal{G},\ b \in \mathcal{B} ``` +What the method assumes of the numbers bound to it: + +```math +\mathrm{x}_{g,b - 1} < \mathrm{x}_{g,b} \qquad \forall\, g \in \mathcal{G},\ b \in \mathcal{B} +``` + +```math +\mathrm{y}_{g,b} \text{ is a convex or concave function of } \mathrm{x}_{g,b} \text{ along } b \qquad \forall\, g \in \mathcal{G} +``` + #### `cost_curve` **`method: lp`** — no weights at all — one row per segment line, plus the two rows holding the domain, in `examples/piecewise_lp.yaml`. @@ -1149,6 +1232,20 @@ cost_curve: \mathit{dispatch}_{t,g} \le \mathrm{x}_{g,b} \qquad \forall\, t \in \mathcal{T},\ g \in \mathcal{G},\ b \in \mathcal{B} \,:\, \mathrm{pos}(b) = \lvert \mathcal{B} \rvert - 1 ``` +What the method assumes of the numbers bound to it: + +```math +\mathrm{x}_{g,b - 1} < \mathrm{x}_{g,b} \qquad \forall\, g \in \mathcal{G},\ b \in \mathcal{B} +``` + +```math +\mathrm{y}_{g,b} \text{ is a convex function of } \mathrm{x}_{g,b} \text{ along } b \qquad \forall\, g \in \mathcal{G} +``` + +```math +\lvert \mathcal{B} \rvert \ge 2 +``` + ### Sets carried to the solver #### `adjacent` @@ -1165,4 +1262,108 @@ adjacent: ```math \left( \mathit{weight}_{t,g} \right)_{g \in \mathcal{G}} \in \mathrm{SOS}2 \qquad \forall\, t \in \mathcal{T} ``` + +### What the data has to satisfy + +#### `bounds_do_not_cross` + +two parameters, which is arithmetic like any other + +```yaml +bounds_do_not_cross: "p_min <= p_max" +``` + +```math +\mathrm{p}^{\mathrm{min}}_{g} \le \mathrm{p}^{\mathrm{max}}_{g} \qquad \forall\, g \in \mathcal{G} +``` + +#### `efficiency_is_a_fraction` + +a connective, so the line has no relation to align on + +```yaml +efficiency_is_a_fraction: "eta > 0 AND eta <= 1" +``` + +```math +\mathrm{eta}_{g} > 0 \wedge \mathrm{eta}_{g} \le 1 \qquad \forall\, g \in \mathcal{G} +``` + +#### `lead_times_are_short` + +one parameter against a literal + +```yaml +lead_times_are_short: "lead <= 3" +``` + +```math +\mathrm{lead}_{g} \le 3 \qquad \forall\, g \in \mathcal{G} +``` + +#### `zones_agree` + +two maps into one set, compared row by row + +```yaml +zones_agree: "zone_of == area_of" +``` + +```math +\mathrm{zone\_of}(b) = \mathrm{area\_of}(b) \qquad \forall\, b \in \mathcal{B} +``` + +#### `budget_covers_the_peak` + +a reduction on a side, leaving nothing to quantify + +```yaml +budget_covers_the_peak: "sum(p_max, over=generator) >= budget" +``` + +```math +\sum_{g \in \mathcal{G}} \mathrm{p}^{\mathrm{max}}_{g} \ge \mathrm{budget} +``` + +#### `ramps_are_gentle` + +a translation inside arithmetic, and a position keeping the vacated row out + +```yaml +ramps_are_gentle: + holds: "load - shift(load, along=snapshot, offset=1, edge=0) <= budget" + where: "position(snapshot) > 0" +``` + +```math +\mathrm{load}_{t,b} - \mathrm{load}_{t \boxminus_{0} 1,b} \le \mathrm{budget} \qquad \forall\, t \in \mathcal{T},\ b \in \mathcal{B} \,:\, \mathrm{pos}(t) > 0 +``` + +#### `flexible_units_have_headroom` + +a bare bool parameter as the where + +```yaml +flexible_units_have_headroom: + holds: "p_min < p_max" + where: "is_flexible" +``` + +```math +\mathrm{p}^{\mathrm{min}}_{g} < \mathrm{p}^{\mathrm{max}}_{g} \qquad \forall\, g \in \mathcal{G} \,:\, \mathrm{is\_flexible}_{g} +``` + +#### `northern_demand_is_real` + +a relation comparison as the where, over a frame two dims wide + +```yaml +northern_demand_is_real: + holds: "load >= 0" + where: "zone_of == 'north'" +``` + +```math +\mathrm{load}_{t,b} \ge 0 \qquad \forall\, t \in \mathcal{T},\ b \in \mathcal{B} \,:\, \mathrm{zone\_of}(b) = \text{'}\mathrm{north}\text{'} +``` diff --git a/docs/reference/reading.md b/docs/reference/reading.md index de490c89..88bec8d5 100644 --- a/docs/reference/reading.md +++ b/docs/reference/reading.md @@ -45,6 +45,10 @@ piecewise: - [p, bp_x] - [cost, bp_y, ">="] method: convex +assumptions: + cost_is_never_negative: + holds: "bp_y >= 0" + description: a negative cost is a gain the objective would chase constraints: target: dims: [] @@ -73,11 +77,34 @@ on a `Program`, it returns the same object unchanged. | building rows, as a solver backend or a second front end does | `Program` | Every declaration is there, and resolved | | reading the file, for `macros:`, `description:`, or a link as it was written | `Spec` | A program keeps a curve's facts | -`program.piecewise` keeps what the block assumed about the numbers, such as -"the breakpoints in `bp_x` increase", as a `checks` tuple. The engine, which has -the numbers, runs each check, and `check_message` gives it the sentence to -raise. `ParameterDeclaration.derivation` says how a parameter is filled, and -`None` means the engine binds it from its data. +`program.piecewise` keeps the curve: its breakpoint dimension, its method and +its values parameters. `ParameterDeclaration.derivation` says how a parameter +is filled, and `None` means the engine binds it from its data. + +## What the data has to satisfy + +`program.assumptions` holds every fact the numbers have to meet, by the name a +refusal quotes. The engine, which has the numbers, runs each one and raises +`assumption_message` where it fails: + +```python +from math_spec.program import Holds, assumption_message + +sorted(program.assumptions) # ['cost_is_never_negative', 'curve curvature', 'curve increasing'] +isinstance(program.assumptions['curve increasing'], Holds) # False +message = assumption_message('curve increasing', program.assumptions['curve increasing']) +message # "piecewise 'curve': method: convex requires strictly increasing breakpoints in 'bp_x' along 'bp'" +written = assumption_message('cost_is_never_negative', program.assumptions['cost_is_never_negative']) +written # "assumption 'cost_is_never_negative' does not hold for the data bound to 'bp_y' — a negative cost is a gain the objective would chase" +``` + +Two kinds stand in that mapping. A `Holds` carries what the file wrote under +`assumptions:`: the `predicate`, the `where` it is checked under, and the +`description` the sentence quotes. +The rest carry what a `piecewise:` block's method implies about its +breakpoints — `Increasing`, `Curved`, `AtLeastTwo` and `Contiguous` — each +naming the block it came from. The union is closed, so a kind added later is a +type error at your match rather than a case you silently skip. ## Nodes and masks diff --git a/docs/reference/typeset.md b/docs/reference/typeset.md index c118753a..b7f27551 100644 --- a/docs/reference/typeset.md +++ b/docs/reference/typeset.md @@ -47,6 +47,10 @@ a flag. - The model's `description:` opens the document. - A `piecewise:` block prints as the variables and constraints it expands into. +- An [`assumptions:`](language/assumptions.md) entry prints under an + **Assumptions** heading, last, beside what each curve assumes of its + breakpoints. A model that assumes nothing of its data prints no such + heading. - A [named expression](language/named.md) prints its symbol where it is used and its body once, under a **Definitions** heading, in declaration order. A `cases:` block and a [reported entry](language/named.md#reported-expressions) @@ -74,8 +78,8 @@ dimension, parameter and variable. ## Printing one declaration on its own `typeset_declaration` returns the line the document prints for one named -expression, constraint or variable, with its quantifier and without a document, -a label, a number or math delimiters: +expression, constraint, assumption or variable, with its quantifier and without +a document, a label, a number or math delimiters: ```python ms.typeset_declaration('model.yaml', 'spend', 'latex') @@ -97,9 +101,9 @@ A line on its own has no _Definitions_ section beside it, so the plain named expressions it uses are substituted. A cased expression prints by symbol, and a second call with its name prints its block. -A name that is none of the three kinds is refused with the near miss. A name that -is both a constraint and a variable is refused too, because one line can print -only one of them. +A name that is none of the four kinds is refused with the near miss. A name +declared as two of them, such as a constraint and a variable, is refused too, +because one line can print only one of them. ## Symbol tables diff --git a/examples/commitment.yaml b/examples/commitment.yaml index 770ba19e..bba313ee 100644 --- a/examples/commitment.yaml +++ b/examples/commitment.yaml @@ -67,6 +67,16 @@ constraints: dispatch - shift(dispatch, along=snapshot, offset=1, edge=0) <= ramp_limit * previous_status + start_up_limit * (1 - previous_status) +assumptions: + output_floor_fits_under_the_cap: + holds: "min_output <= capacity" + where: "committable" + description: >- + `lower` and `upper` hold one dispatch between them, so a floor above the + cap makes a running unit infeasible rather than expensive. A unit that + cannot be switched off is held to its floor in every snapshot, so the + check is the committable ones'. + objective: sense: minimize expression: sum(dispatch * cost) diff --git a/mkdocs.yml b/mkdocs.yml index ccc32aff..91cc7a4d 100644 --- a/mkdocs.yml +++ b/mkdocs.yml @@ -52,6 +52,7 @@ nav: - Named expressions and macros: reference/language/named.md - Operators: reference/language/operators.md - Piecewise curves and SOS: reference/language/piecewise.md + - Assumptions: reference/language/assumptions.md - Absence and where: reference/language/absence.md - Errors and limits: reference/language/errors.md - Every construct, as math: reference/notation.md diff --git a/schema/math-spec.schema.json b/schema/math-spec.schema.json index 450866fc..f309ca64 100644 --- a/schema/math-spec.schema.json +++ b/schema/math-spec.schema.json @@ -1,5 +1,51 @@ { "$defs": { + "AssumptionBlock": { + "anyOf": [ + { + "additionalProperties": false, + "description": "What the model assumes of its data: a predicate every coordinate it is checked at has to satisfy.\n\nWritten in YAML as a bare where string, or as a mapping once it carries a\n``where:`` or a ``description:``, and serialised back to whichever form it\nwas written in::\n\n assumptions:\n efficiency_is_a_fraction: \"efficiency > 0 AND efficiency <= 1\"\n bounds_do_not_cross:\n holds: \"p_min <= p_max\"\n where: \"p_min\"\n description: a unit with no minimum is unconstrained below\n\nThe language decides nothing about the numbers, so the consumer binding\nthe data checks it, and refuses the data where it does not hold.", + "properties": { + "description": { + "anyOf": [ + { + "type": "string" + }, + { + "type": "null" + } + ], + "default": null, + "title": "Description" + }, + "holds": { + "title": "Holds", + "type": "string" + }, + "where": { + "anyOf": [ + { + "type": "string" + }, + { + "type": "null" + } + ], + "default": null, + "title": "Where" + } + }, + "required": [ + "holds" + ], + "title": "AssumptionBlock", + "type": "object" + }, + { + "type": "string" + } + ] + }, "BoundsBlock": { "additionalProperties": false, "description": "Variable bounds \u2014 each side is a number or parameter name.\n\nAn omitted bound leaves the variable unbounded on that side, not\nimplicitly non-negative.", @@ -636,8 +682,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\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 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. 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 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.", "properties": { + "assumptions": { + "additionalProperties": { + "$ref": "#/$defs/AssumptionBlock" + }, + "default": {}, + "title": "Assumptions", + "type": "object" + }, "constraints": { "additionalProperties": { "$ref": "#/$defs/ConstraintBlock" diff --git a/src/math_spec/lowering.py b/src/math_spec/lowering.py index 66b48e5a..226f9c4c 100644 --- a/src/math_spec/lowering.py +++ b/src/math_spec/lowering.py @@ -35,7 +35,7 @@ VariableNode, ) from math_spec.dimensions import dims_of -from math_spec.piecewise import declaration_of, derivations_of, expand_piecewise +from math_spec.piecewise import assumptions_of, declaration_of, derivations_of, expand_piecewise from math_spec.validation import to_spec if TYPE_CHECKING: @@ -164,10 +164,28 @@ def lower_program(expanded: _ExpandedSpec) -> program.Program: relations=resolved.relations, sos=sos, piecewise={name: declaration_of(ex) for name, ex in expanded.expanded_piecewise.items()}, + assumptions=_assumptions(expanded), expressions=expressions, ) +def _assumptions(expanded: _ExpandedSpec) -> dict[str, program.Assumption]: + """Everything the data has to satisfy, the file's entries first and each block's behind them. + + One mapping rather than two, because a consumer binding data checks them + all the same way and refuses in the same words. + """ + assumptions: dict[str, program.Assumption] = {} + for name, (holds, where) in expanded.resolved.assumptions.items(): + lowering = _Lowering(expanded, f"assumption '{name}'") + predicate = lowering.mask(holds) + assert predicate is not None, 'a predicate that admits every row was refused as deciding nothing' + assumptions[name] = program.Holds(predicate, lowering.mask(where), expanded.assumptions[name].description) + for block, ex in expanded.expanded_piecewise.items(): + assumptions.update(assumptions_of(block, ex)) + return assumptions + + # --------------------------------------------------------------------------- # expression lowering # --------------------------------------------------------------------------- diff --git a/src/math_spec/model.py b/src/math_spec/model.py index 91b9a91c..8c739953 100644 --- a/src/math_spec/model.py +++ b/src/math_spec/model.py @@ -476,6 +476,58 @@ def _as_written(self) -> str | dict[str, object]: return {'expression': self.expression, 'description': self.description} +class AssumptionBlock(_StrictBlock): + """What the model assumes of its data: a predicate every coordinate it is checked at has to satisfy. + + Written in YAML as a bare where string, or as a mapping once it carries a + ``where:`` or a ``description:``, and serialised back to whichever form it + was written in:: + + assumptions: + efficiency_is_a_fraction: "efficiency > 0 AND efficiency <= 1" + bounds_do_not_cross: + holds: "p_min <= p_max" + where: "p_min" + description: a unit with no minimum is unconstrained below + + The language decides nothing about the numbers, so the consumer binding + the data checks it, and refuses the data where it does not hold. + """ + + _label: ClassVar[str] = 'an assumption declaration' + + #: The predicate, in the where grammar. It holds at every coordinate of + #: its own frame that ``where`` admits. + holds: str + #: Which coordinates it is checked at, in the same grammar; absent means every one. + where: str | None = None + #: Why the rule is there, in the author's words. The sentence a consumer + #: refuses with quotes it. + description: str | None = None + + @model_validator(mode='before') + @classmethod + def _from_string(cls, data: object) -> object: + return {'holds': data} if isinstance(data, str) else data + + @classmethod + @override + def __get_pydantic_json_schema__(cls, core_schema: CoreSchema, handler: GetJsonSchemaHandler) -> dict[str, object]: + """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, object]: + if self.where is None and self.description is None: + return self.holds + written: dict[str, object] = {'holds': self.holds} + if self.where is not None: + written['where'] = self.where + if self.description is not None: + written['description'] = self.description + return written + + class PiecewiseLink(_StrictBlock): """One link of a piecewise block: an expression pinned to a values curve. @@ -693,7 +745,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 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. Everything else on this class is pydantic's, not a contract this package keeps. @@ -724,6 +776,7 @@ class Spec(_StrictBlock): macros: dict[str, MacroBlock] = {} piecewise: dict[str, PiecewiseBlock] = {} sos: dict[str, SosBlock] = {} + assumptions: dict[str, AssumptionBlock] = {} def relations_of(self, dimension: str) -> dict[str, RelationBlock]: """The relations with a column over *dimension*, by name.""" diff --git a/src/math_spec/piecewise.py b/src/math_spec/piecewise.py index c6c68799..72c18766 100644 --- a/src/math_spec/piecewise.py +++ b/src/math_spec/piecewise.py @@ -64,29 +64,38 @@ def _curvature_required(pw: PiecewiseBlock) -> Curvature | None: def declaration_of(expanded: ExpandedPiecewise) -> PiecewiseDeclaration: - """The facts of one expanded block, as a program carries them. + """The curve of one expanded block, as a program carries it.""" + pw = expanded.block + return PiecewiseDeclaration( + over=pw.over, + method=pw.method, + breakpoints=tuple(link.values for link in pw.links), + ) + + +def assumptions_of(block: str, expanded: ExpandedPiecewise) -> dict[str, Check]: + """What *block* assumes of its numbers, by the name the document prints and a refusal quotes. A curve has an x-axis only where two links tie it, so the increasing condition — and the shape it is checked with — exist only there; ``lp`` alone needs a segment to state a line for; a mask must be one run. + + The space in each name is what keeps these apart from the file's own + ``assumptions:`` entries in one mapping: a declaration is named as an + expression writes it, so no file can write one of these. """ pw = expanded.block - checks: list[Check] = [] + checks: dict[str, Check] = {} 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[f'{block} increasing'] = Increasing(block, pw.method, x.values, pw.over) + checks[f'{block} curvature'] = Curved(block, pw.method, x.values, y.values, pw.over, curvature) if pw.method == 'lp': - checks.append(AtLeastTwo(pw.over, expanded.points)) + checks[f'{block} breakpoints'] = AtLeastTwo(block, pw.over, expanded.points) if expanded.points is not None: - checks.append(Contiguous(expanded.points, _nominated(pw))) - return PiecewiseDeclaration( - over=pw.over, - method=pw.method, - breakpoints=tuple(link.values for link in pw.links), - checks=tuple(checks), - ) + checks[f'{block} points'] = Contiguous(block, expanded.points, _nominated(pw)) + return checks def derivations_of(block: str, expanded: ExpandedPiecewise) -> dict[str, Derivation]: diff --git a/src/math_spec/program.py b/src/math_spec/program.py index 0bff4351..af43ca40 100644 --- a/src/math_spec/program.py +++ b/src/math_spec/program.py @@ -43,6 +43,7 @@ 'Add', 'And', 'ArithmeticComparison', + 'Assumption', 'AtLeastTwo', 'BooleanLiteral', 'Cases', @@ -68,6 +69,7 @@ 'FirstOf', 'Footprint', 'GroupSum', + 'Holds', 'Increasing', 'LastOf', 'Mask', @@ -108,8 +110,8 @@ 'VariableDefined', 'VariableDomain', 'WindowSum', + 'assumption_message', 'carries_variable', - 'check_message', 'children', 'divisor_parameters', 'fan_in', @@ -579,10 +581,51 @@ class LastOf: Derivation = MaskOf | FirstOf | LastOf +@dataclass(frozen=True) +class PiecewiseDeclaration: + """A ``piecewise:`` block, kept as the facts a consumer binding its data reads. + + The expansion lowered the links into constraints and emitted the + parameters it needs — each of those says how it is filled, on its own + :attr:`ParameterDeclaration.derivation`. What the block assumes of its + numbers is an :data:`Assumption` like any other, under + :attr:`Program.assumptions`; what is left here is the curve. + + Attributes: + over: The breakpoint dimension. + method: How the weights are restricted. + breakpoints: The links' values parameters, in link order. + """ + + over: str + method: _model.PiecewiseMethod + breakpoints: tuple[str, ...] + + +@dataclass(frozen=True) +class Holds: + """A predicate the file states of its data, under the name it wrote in ``assumptions:``. + + ``predicate`` is true at every coordinate of its frame — the product of + every dim the two masks name — that ``where`` admits, a missing row + reading as false as it does in any mask. Nothing here is decidable at + load: both sides are the data's, which is why the consumer binding it + checks. + """ + + predicate: Mask + where: Mask | None = None + #: What the file wrote under ``description:``. The refusal quotes it: the + #: names alone say which columns are wrong, and not why the rule is there. + description: str | None = None + + @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.""" + block: str + method: _model.PiecewiseMethod parameter: str over: str @@ -591,10 +634,12 @@ class Increasing: class Curved: """*y* over *x* bends, along *over*, the way *curvature* says. - That is the shape the method is exact for. ``either`` is the hull's - weaker condition: any single bend, so only a mixed curve fails it. + That is the shape *method* is exact for. ``either`` is the hull's weaker + condition: any single bend, so only a mixed curve fails it. """ + block: str + method: _model.PiecewiseMethod x: str y: str over: str @@ -605,6 +650,7 @@ class Curved: class AtLeastTwo: """Each curve has at least two breakpoints — every position along *over*, or those *mask* admits.""" + block: str over: str mask: str | None @@ -613,75 +659,66 @@ class AtLeastTwo: class Contiguous: """*mask* admits one consecutive run of at least one breakpoint per curve.""" + block: str mask: str #: The breakpoint parameter the mask was derived from, where it was — the #: name the file wrote, and the one a refusal names. 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`. +#: What a ``piecewise:`` block assumes of the numbers it is bound to, each +#: naming the block whose expansion derived it. The file writes none of these: +#: the method implies them, which is why each carries the method its sentence +#: quotes. Check = Increasing | Curved | AtLeastTwo | Contiguous - -@dataclass(frozen=True) -class PiecewiseDeclaration: - """A ``piecewise:`` block, kept as the facts a consumer binding its data reads. - - The expansion lowered the links into constraints and emitted the - parameters it needs — each of those says how it is filled, on its own - :attr:`ParameterDeclaration.derivation`. What is left here is the curve - and what the block assumes of it. - - Attributes: - over: The breakpoint dimension. - method: How the weights are restricted. - breakpoints: The links' values parameters, in link order. - checks: What the block assumes of the numbers, each carrying its own - subjects, for the consumer holding them to check. - """ - - over: str - method: _model.PiecewiseMethod - breakpoints: tuple[str, ...] - checks: tuple[Check, ...] +#: One fact about the data a consumer has to check before it solves — the +#: file's own under :class:`Holds`, and a curve's under :data:`Check`. The data +#: decides whether each holds, so the language names the condition with its +#: subjects and its sentence (:func:`assumption_message`), and the consumer +#: holding the numbers checks. Closed, like :data:`Derivation`. +Assumption = Holds | 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 assumption_message(name: str, assumption: Assumption) -> str: + """The sentence a consumer raises when the data bound to *assumption*, called *name*, fails it. The language's own wording, so every consumer refuses in the same words; - a consumer appends what it saw. + a consumer appends the coordinates it saw. Where the file wrote a + ``description:``, it trails the sentence, since the author said there why + the rule is there. """ - ctx = f"piecewise '{block}'" - match check: - case Increasing(parameter, over): + match assumption: + case Holds(predicate, _, description): + read = ', '.join(f"'{n}'" for n in sorted(predicate.names_read)) + sentence = f"assumption '{name}' does not hold for the data bound to {read}" + return f'{sentence} — {description}' if description else sentence + case Increasing(block, method, parameter, over): return ( - f"{ctx}: method: {pw.method} requires strictly increasing breakpoints in '{parameter}' along '{over}'" + f"piecewise '{block}': method: {method} requires strictly increasing breakpoints in " + f"'{parameter}' along '{over}'" ) - case Curved(x, y, over, curvature): + case Curved(block, method, x, y, over, curvature): 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"piecewise '{block}': 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(): + case AtLeastTwo(block): return ( - f'{ctx}: 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"piecewise '{block}': method: lp needs at least two breakpoints per curve — the method *is* its " + f'segment 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): + case Contiguous(block, mask, values): return ( - f"{ctx}: 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." + f"piecewise '{block}': points: '{values if values is not None else mask}' must mark a consecutive " + f'run of at least one breakpoint per curve — the chord row joins a breakpoint to the one before ' + f"it, and the domain rows sit on the curve's own first and last." ) case _: - assert_never(check) + assert_never(assumption) @dataclass(frozen=True) @@ -931,6 +968,12 @@ class Program: #: Each ``piecewise:`` block the file wrote, as facts — see #: :class:`PiecewiseDeclaration`. piecewise: Mapping[str, PiecewiseDeclaration] = Sealed({}) + #: What the data has to satisfy for the answer to mean anything, by the + #: name a refusal quotes: every ``assumptions:`` entry the file wrote, then + #: what each ``piecewise:`` block's method assumes of its breakpoints. The + #: language decides none of it, so the consumer binding the data checks + #: each and refuses with :func:`assumption_message`. + assumptions: Mapping[str, Assumption] = Sealed({}) #: Declared ``expressions:``, lowered, each saying whether the math reads #: it. None builds a row of its own — one the math reads is inlined where #: it is read — but all are lowered with the program, so a file whose diff --git a/src/math_spec/resolution.py b/src/math_spec/resolution.py index 8d4a7e11..119c471f 100644 --- a/src/math_spec/resolution.py +++ b/src/math_spec/resolution.py @@ -188,6 +188,13 @@ class ResolvedConstraint(NamedTuple): where: Mask | None +class ResolvedAssumption(NamedTuple): + """One assumption's typed halves: the predicate it states, and the mask it is checked under.""" + + holds: Mask + where: Mask | None + + @dataclass(frozen=True) class Resolved: """Every expression and where string of one schema, typed once at load. @@ -212,6 +219,8 @@ class Resolved: relations: Each relation's columns and key, as declared — the one copy, which every :class:`~math_spec.program.Direction` and :class:`~math_spec.program.Partition` in the trees holds. + assumptions: Each ``assumptions:`` entry's predicate and the mask it + is checked under. """ expressions: dict[str, CasesNode | DefinitionNode] @@ -219,6 +228,7 @@ class Resolved: constraints: dict[str, ResolvedConstraint] objective: ArithmeticNode | None relations: dict[str, RelationDeclaration] + assumptions: dict[str, ResolvedAssumption] @cached_property def read_by_the_math(self) -> frozenset[str]: diff --git a/src/math_spec/typesetting/__init__.py b/src/math_spec/typesetting/__init__.py index 7bbdadd8..8f6919f5 100644 --- a/src/math_spec/typesetting/__init__.py +++ b/src/math_spec/typesetting/__init__.py @@ -168,7 +168,7 @@ def typeset_declaration( """Render one declaration as the bare line the document prints for it. The line the whole-model render prints for it — a named expression's - definition, a constraint, or a variable's domain, quantifier included — + definition, a constraint, an assumption, or a variable's domain, quantifier included — with no document, label, equation number or math delimiters around it, for a math context the caller lays out: a docstring, a table cell. A line on its own has no Definitions section beside it, so the plain named @@ -177,7 +177,7 @@ def typeset_declaration( Args: model: Anything :func:`math_spec.to_spec` accepts. - name: A named expression, constraint or variable the model declares. + name: A named expression, constraint, assumption or variable the model declares. fmt: What spells the math — a key of :data:`FORMATS`. symbols: How names print; see :func:`typeset`. inline_expressions: Substitute the plain named expressions the line uses, so it @@ -191,20 +191,27 @@ def typeset_declaration( Raises: ValueError: *fmt* names no format. LanguageError: A model that does not compile; it does not print. - SchemaError: *name* is declared as none of the three, or as two — a + SchemaError: *name* is declared as none of the four, or as two — a constraint may share a variable's name; or a symbol table entry names nothing in the model. """ walk = _walk(model, fmt, symbols, inline_expressions=inline_expressions) schema = walk.schema - kinds = {'named expression': schema.expressions, 'constraint': schema.constraints, 'variable': schema.variables} + kinds = { + 'named expression': schema.expressions, + 'constraint': schema.constraints, + 'assumption': schema.assumptions, + 'variable': schema.variables, + } found = [kind for kind, group in kinds.items() if name in group] if not found: everything = {n for group in kinds.values() for n in group} - msg = f"'{name}' is not a named expression, constraint or variable. {did_you_mean(name, everything)}" + msg = ( + f"'{name}' is not a named expression, constraint, assumption or variable. {did_you_mean(name, everything)}" + ) raise SchemaError(msg) if len(found) > 1: - msg = f"'{name}' is both a {found[0]} and a {found[1]}, and one line prints one of them — rename one." + msg = f"'{name}' is declared twice, as {found[0]} and as {found[1]}, and one line prints one of them — rename one." raise SchemaError(msg) return walk.format.equation(walk.line(name)) diff --git a/src/math_spec/typesetting/format.py b/src/math_spec/typesetting/format.py index a0bedfb5..80612b69 100644 --- a/src/math_spec/typesetting/format.py +++ b/src/math_spec/typesetting/format.py @@ -223,6 +223,10 @@ def cardinality(self, inner: str) -> str: def fraction(self, numerator: str, denominator: str) -> str: ... + def set_of(self, members: str, condition: str) -> str: + """A set by comprehension: ``{ k ∈ K : condition }``.""" + ... + def summation(self, domain: str, body: str) -> str: ... def cases(self, arms: list[tuple[str, str]]) -> str: diff --git a/src/math_spec/typesetting/latex.py b/src/math_spec/typesetting/latex.py index d09c3ff2..3e3296f5 100644 --- a/src/math_spec/typesetting/latex.py +++ b/src/math_spec/typesetting/latex.py @@ -98,6 +98,9 @@ def cardinality(self, inner: str) -> str: def fraction(self, numerator: str, denominator: str) -> str: return rf'\frac{{{numerator}}}{{{denominator}}}' + def set_of(self, members: str, condition: str) -> str: + return rf'\{{ {members} {self.operators["such_that"]} {condition} \}}' + def cases(self, arms: list[tuple[str, str]]) -> str: rows = self.cases_row.join(f'{value} & {condition}' for value, condition in arms) return rf'\begin{{cases}} {rows} \end{{cases}}' diff --git a/src/math_spec/typesetting/typst.py b/src/math_spec/typesetting/typst.py index 55c34c7f..d83a1aeb 100644 --- a/src/math_spec/typesetting/typst.py +++ b/src/math_spec/typesetting/typst.py @@ -106,6 +106,9 @@ def cardinality(self, inner: str) -> str: def fraction(self, numerator: str, denominator: str) -> str: return f'frac({numerator}, {denominator})' + def set_of(self, members: str, condition: str) -> str: + return f'{{{members} {self.operators["such_that"]} {condition}}}' + def cases(self, arms: list[tuple[str, str]]) -> str: return 'cases({})'.format(self.cases_row.join(f'{value} & {condition}' for value, condition in arms)) diff --git a/src/math_spec/typesetting/walk.py b/src/math_spec/typesetting/walk.py index 2413c3c6..75a5c52e 100644 --- a/src/math_spec/typesetting/walk.py +++ b/src/math_spec/typesetting/walk.py @@ -35,14 +35,20 @@ VariableNode, ) from math_spec.dimensions import dims_of +from math_spec.piecewise import assumptions_of from math_spec.program import ( And, ArithmeticComparison, + AtLeastTwo, BooleanLiteral, + Check, + Contiguous, + Curved, DimensionComparison, DimensionPosition, Direction, ExpressionComparison, + Increasing, Mask, Not, Or, @@ -61,7 +67,7 @@ import datetime from collections.abc import Iterable, Mapping - from math_spec.model import RelationBlock, SosBlock, _ExpandedSpec + from math_spec.model import ExpandedPiecewise, RelationBlock, SosBlock, _ExpandedSpec from math_spec.typesetting.format import Format from math_spec.typesetting.symbols import Symbols @@ -75,6 +81,17 @@ #: a comparison sits above the connectives and is bracketed under none. _WHERE_PRECEDENCE = {'or': 0, 'and': 1, 'comparison': 2, 'not': 3} +#: The predicates that are one relation between two sides, which a line may +#: align on the way it aligns a constraint. +AlignedComparison = ( + ParameterComparison + | ArithmeticComparison + | DimensionComparison + | DimensionPosition + | RelationComparison + | RelationPairComparison +) + _PREDICATES: dict[PredicateOperator, OperatorName] = { '==': 'equal', '!=': 'ne', @@ -581,45 +598,14 @@ def _where(self, node: Predicate, ctx: _Context) -> tuple[str, int]: comparison, ) - if isinstance(node, ParameterComparison): - left = ctx.indexed(self.symbols.name[node.name], list(node.dims)) - return f'{left} {self._op(_PREDICATES[node.op])} {self._literal(node.value)}', comparison - - if isinstance(node, ArithmeticComparison): - left, right = self._expression(node.left, ctx), self._expression(node.right, ctx) - return f'{left} {self._op(_PREDICATES[node.op])} {right}', comparison + if isinstance(node, AlignedComparison): + left, right = self.sides(node, ctx) + return f'{left} {right}', comparison if isinstance(node, ExpressionComparison): msg = 'a lowered comparison reached the typesetter; it prints the resolved tree, which lowering rebuilds.' raise AssertionError(msg) - if isinstance(node, DimensionComparison): - if isinstance(node.value, int | float): - self.noticed.numeric_coordinates.add(node.name) - return ( - f'{ctx.subscript(node.name)} {self._op(_PREDICATES[node.op])} {self._literal(node.value)}', - comparison, - ) - - if isinstance(node, DimensionPosition): - grouping = ( - None - if node.partition is None - else self._tuple([self._value_read(node.partition.name, c, ctx) for c in node.partition.group]) - ) - place = self._position(ctx.subscript(node.name), grouping) - ordinal = self._ordinal(node.name, node.position, grouping) - return f'{place} {self._op(_PREDICATES[node.op])} {ordinal}', comparison - - if isinstance(node, RelationComparison): - applied = self._value_read(node.name, node.column, ctx) - return f'{applied} {self._op(_PREDICATES[node.op])} {self._literal(node.value)}', comparison - - if isinstance(node, RelationPairComparison): - left = self._value_read(node.name, node.column, ctx) - right = self._value_read(node.other, node.other_column, ctx) - return f'{left} {self._op(_PREDICATES[node.op])} {right}', comparison - if isinstance(node, RelationDefined): return self._relation_row(node.name, self._frame_key(node.name, ctx)), comparison @@ -641,6 +627,37 @@ def _where(self, node: Predicate, ctx: _Context) -> tuple[str, int]: assert_never(node) + def sides(self, node: AlignedComparison, ctx: _Context) -> tuple[str, str]: + """One comparison as its two sides, the relation symbol leading the right. + + Split so that a line whose whole predicate is one comparison aligns on + the relation, as a constraint does. + """ + if isinstance(node, ParameterComparison): + left, right = ctx.indexed(self.symbols.name[node.name], list(node.dims)), self._literal(node.value) + elif isinstance(node, ArithmeticComparison): + left, right = self._expression(node.left, ctx), self._expression(node.right, ctx) + elif isinstance(node, DimensionComparison): + if isinstance(node.value, int | float): + self.noticed.numeric_coordinates.add(node.name) + left, right = ctx.subscript(node.name), self._literal(node.value) + elif isinstance(node, DimensionPosition): + grouping = ( + None + if node.partition is None + else self._tuple([self._value_read(node.partition.name, c, ctx) for c in node.partition.group]) + ) + left = self._position(ctx.subscript(node.name), grouping) + right = self._ordinal(node.name, node.position, grouping) + elif isinstance(node, RelationComparison): + left, right = self._value_read(node.name, node.column, ctx), self._literal(node.value) + elif isinstance(node, RelationPairComparison): + left = self._value_read(node.name, node.column, ctx) + right = self._value_read(node.other, node.other_column, ctx) + else: + assert_never(node) + return left, f'{self._op(_PREDICATES[node.op])} {right}' + def _literal(self, value: float | str | datetime.date) -> str: return self._number(value) if isinstance(value, int | float) else self.format.quoted(str(value)) @@ -690,6 +707,7 @@ def equations(self) -> tuple[list[tuple[str, list[Line]]], Noticed]: ('Subject to', self._constraints()), ('Definitions', self._definitions()), ('Variable domains', self._variables()), + ('Assumptions', self._assumptions()), ] return sections, self.noticed @@ -764,15 +782,17 @@ def definition(self, name: str) -> Line: ) def line(self, name: str) -> Line: - """The one line *name* prints as: a named expression's definition, a constraint, or a variable's domain. + """The one line *name* prints as: a named expression, a constraint, an assumption, or a variable's domain. - *name* is one of the three; :func:`~math_spec.typesetting.typeset_declaration` + *name* is one of the four; :func:`~math_spec.typesetting.typeset_declaration` refuses the rest, and a constraint sharing a variable's name. """ if name in self.schema.expressions: return self.definition(name) if name in self.schema.constraints: return self._constraint(name) + if name in self.schema.assumptions: + return self._assumption(name) return self._variable(name) def _arms(self, node: CasesNode, ctx: _Context) -> list[tuple[str, str]]: @@ -844,6 +864,103 @@ def _sos(self, name: str, block: SosBlock, ctx: _Context) -> Line: condition=self._quantifier([d for d in dims if d != block.over], ''), ) + # -- assumptions ------------------------------------------------------- + + def _assumptions(self) -> list[Line]: + """What the model assumes of its data, in the order a program carries it. + + A curve's conditions are the language's own, derived from the method + rather than written (:func:`~math_spec.piecewise.assumptions_of`), and + they print here beside the file's: the reader sees every condition the + data is held to, whoever stated it. + """ + lines = [self._assumption(name) for name in self.schema.assumptions] + for block, expanded in self.schema.expanded_piecewise.items(): + lines += [self._derived(name, expanded, check) for name, check in assumptions_of(block, expanded).items()] + return lines + + def _assumption(self, name: str) -> Line: + """One ``assumptions:`` entry: the predicate over the frame both its masks name, under its ``where``.""" + holds, where = self.schema.resolved.assumptions[name] + frame = self._sorted(holds.dims | (where.dims if where is not None else frozenset())) + ctx = self._context(frame) + if isinstance(holds.root, AlignedComparison): + left, right = self.sides(holds.root, ctx) + else: + left, right = self._predicate(holds.root, ctx), '' + return Line(label=name, left=left, right=right, condition=self._quantifier(frame, self._condition(ctx, where))) + + def _derived(self, name: str, expanded: ExpandedPiecewise, check: Check) -> Line: + """One condition a curve puts on its breakpoints, as the line a reader checks the data against. + + The strictly increasing x-axis is an inequality between neighbours, + printed with the plain translation whose vacated first row is absent. + The shape a method is exact for is prose, as a paper writes it, since + "convex or concave" is no one inequality. The two conditions on a + ``points:`` mask are stated of the set the mask admits. + """ + match check: + case Increasing(_, _, parameter, over): + frame = self._sorted(frozenset(self.schema.parameters[parameter].dims)) + ctx = self._context(frame) + previous = ctx.translated(over, _Step(1, 'plain')) + condition = '' + if (mask := expanded.points) is not None: + admitted = ParameterDefined(mask, tuple(self.schema.parameters[mask].dims)) + condition = self.format.joined( + [self._predicate(admitted, ctx), self._predicate(admitted, previous)], self._op('and') + ) + return Line( + label=name, + left=self._parameter(parameter, previous), + right=f'{self._op("lt")} {self._parameter(parameter, ctx)}', + condition=self._quantifier(frame, condition), + ) + case Curved(_, _, x, y, over, curvature): + dims = frozenset(self.schema.parameters[x].dims) | frozenset(self.schema.parameters[y].dims) + ctx = self._context(self._sorted(dims)) + shape = 'convex or concave' if curvature == 'either' else curvature + return Line( + label=name, + left=self._parameter(y, ctx), + right=( + f'{self.format.prose(f" is a {shape} function of ")} {self._parameter(x, ctx)} ' + f'{self.format.prose(" along ")} {self.symbols.index[over]}' + ), + condition=self._quantifier(self._sorted(dims - {over}), ''), + ) + case AtLeastTwo(_, over, mask): + members, frame = self.symbols.set[over], self._sorted(frozenset()) + if mask is not None: + members, frame = self._admitted(mask, over) + return Line( + label=name, + left=self.format.cardinality(members), + right=f'{self._op("ge")} {self._number(2)}', + condition=self._quantifier(frame, ''), + ) + case Contiguous(_, mask, _): + members, frame = self._admitted(mask, expanded.block.over) + return Line( + label=name, + left=members, + right=self.format.prose(' is one run of consecutive breakpoints'), + condition=self._quantifier(frame, ''), + ) + assert_never(check) + + def _admitted(self, mask: str, over: str) -> tuple[str, list[str]]: + """The breakpoints *mask* admits along *over* as a set, and the frame that set is one of per curve.""" + dims = frozenset(self.schema.parameters[mask].dims) + frame = self._sorted(dims - {over}) + ctx = self._context([*frame, over]) + admitted = self._predicate(ParameterDefined(mask, tuple(self.schema.parameters[mask].dims)), ctx) + return self.format.set_of(self._membership(over), admitted), frame + + def _parameter(self, name: str, ctx: _Context) -> str: + """A parameter's symbol, indexed by its own dims.""" + return ctx.indexed(self.symbols.name[name], list(self.schema.parameters[name].dims)) + def _bound(self, ctx: _Context, value: float | str) -> str: if isinstance(value, str): return ctx.indexed(self.symbols.name[value], list(self.schema.parameters[value].dims)) diff --git a/src/math_spec/validation.py b/src/math_spec/validation.py index 4b9ecb7c..626931f6 100644 --- a/src/math_spec/validation.py +++ b/src/math_spec/validation.py @@ -38,10 +38,11 @@ from math_spec.expansion import expand, parse_and_expand, parse_template from math_spec.model import Spec from math_spec.operators import BUILTINS, call_shape_error, unknown_operator_message -from math_spec.program import BooleanLiteral +from math_spec.program import BooleanLiteral, Mask, VariableDefined from math_spec.resolution import ( Namespace, Resolved, + ResolvedAssumption, ResolvedConstraint, mask_of, names_in, @@ -52,7 +53,7 @@ if TYPE_CHECKING: from pathlib import Path - from math_spec.model import ExpressionBlock + from math_spec.model import AssumptionBlock, ExpressionBlock from math_spec.program import Predicate @@ -162,10 +163,15 @@ def validate_expressions(schema: Spec) -> Resolved: schema.objective.expression, ns, 'The objective', errors, comparison=False, ceiling=2 ) + assumptions: dict[str, ResolvedAssumption] = {} + for aname, adef in schema.assumptions.items(): + if (assumption := _assumption(aname, adef, ns, errors)) is not None: + assumptions[aname] = assumption + if errors: raise SchemaError(_once(errors)) - resolved = Resolved(expressions, variables, constraints, objective, ns.relations) + resolved = Resolved(expressions, variables, constraints, objective, ns.relations, assumptions) check_schema(schema, resolved) return resolved @@ -203,6 +209,62 @@ def _named(name: str, block: ExpressionBlock, ns: Namespace, errors: list[str]) return CasesNode(name, (*arms, CaseArm('otherwise', None, fallback))) +def _assumption(name: str, block: AssumptionBlock, ns: Namespace, errors: list[str]) -> ResolvedAssumption | None: + """One ``assumptions:`` entry typed, or ``None`` once anything in it failed. + + A predicate the connectives decide is refused: one that folds to true + assumes nothing, and one that folds to false refuses every dataset. A + variable is refused too, since an assumption is about the data and a + variable is what the solver decides from it. + """ + context = f"Assumption '{name}'" + found = len(errors) + holds = resolve_where_text(block.holds, ns, context, errors) + where = resolve_where_text(block.where, ns, f'{context}, where', errors) + if isinstance(holds, BooleanLiteral): + errors.append(_decided_assumption(context, block.holds, value=holds.value)) + if isinstance(where, BooleanLiteral): + assert block.where is not None, 'a where the file did not write resolves to nothing' + errors.append(_decided_where(context, block.where, value=where.value)) + for mask, part in ((holds, 'assumes'), (where, 'is checked where')): + if mask is None or isinstance(mask, BooleanLiteral): + continue + errors.extend( + f"{context}: variable '{atom.name}' stands in what the assumption {part}, and an assumption is " + f'about the data — a variable is what the solver decides from it. Name a parameter, or state the ' + f'rule as a constraint.' + for atom in Mask(mask).atoms + if isinstance(atom, VariableDefined) + ) + if len(errors) > found: + return None + assert holds is not None, 'a where string that read to nothing appended an error' + return ResolvedAssumption(Mask(holds), mask_of(where)) + + +def _decided_assumption(context: str, text: str, *, value: bool) -> str: + """The refusal for a predicate the connectives already decided, whose data is never read.""" + if value: + return ( + f'{context}: the predicate {text!r} folds to true, so it assumes nothing of the data. ' + f'Delete it, or name a parameter it constrains.' + ) + return ( + f'{context}: the predicate {text!r} folds to false, so it holds on no data at all. ' + f'Delete it, or write the predicate the data can satisfy.' + ) + + +def _decided_where(context: str, text: str, *, value: bool) -> str: + """The refusal for a ``where`` the connectives already decided, which narrows nothing or everything.""" + if value: + return f'{context}: the where {text!r} folds to true, so it narrows nothing. Delete the where.' + return ( + f'{context}: the where {text!r} folds to false, so the assumption is checked on no row. ' + f'Delete the entry, or write the where the data can satisfy.' + ) + + def _constant_arm(context: str, *, value: bool) -> str: """The refusal for a case arm whose mask the connectives already decided. @@ -288,7 +350,7 @@ def _check_expression( f'Got: {expression!r}\n' f'A constraint is a claim about a decision, and a comparison of numbers and parameters ' f'is settled before the solve — no consumer builds a row for it. Name the variable it should ' - f'bound, or drop the declaration and check the fact where the data is prepared.' + f'bound, or state the fact under `assumptions:`, where the consumer binding the data checks it.' ) return None return resolved diff --git a/tests/test_lowering.py b/tests/test_lowering.py index ad90102c..99185599 100644 --- a/tests/test_lowering.py +++ b/tests/test_lowering.py @@ -37,6 +37,7 @@ ExpressionComparison, Footprint, GroupSum, + Holds, Mask, Multiply, Negate, @@ -55,6 +56,7 @@ Translate, Variable, WindowSum, + assumption_message, children, divisor_parameters, fan_in, @@ -430,6 +432,53 @@ def test_a_comparison_of_expressions_lowers_to_program_expressions_on_both_sides ) +def test_assumptions_carry_the_file_s_entries_and_the_curves_behind_them(): + """One mapping holds every fact about the data, so a consumer binding it has one loop and one refusal. + + The file's entries come first, in the order it wrote them; each + ``piecewise:`` block's conditions follow under the name a refusal quotes. + """ + program = to_program(EXAMPLES / 'piecewise_lp.yaml') + written = [name for name, a in program.assumptions.items() if isinstance(a, Holds)] + derived = [name for name, a in program.assumptions.items() if not isinstance(a, Holds)] + + assert list(program.assumptions) == [*written, *derived], 'the file first, then what the methods imply' + assert derived == ['cost_curve increasing', 'cost_curve curvature', 'cost_curve breakpoints'], ( + 'an lp curve over a whole axis assumes three things of its breakpoints' + ) + + +def test_an_assumption_lowers_both_of_its_masks(): + """The predicate and the ``where`` are rebuilt on program expressions, as every other mask is.""" + program = to_program(override(SHAPES_MODEL, assumptions={'sound': {'holds': 'c <= 0.5 * k', 'where': 'flag'}})) + assumption = program.assumptions['sound'] + + assert assumption == Holds( + Mask(ExpressionComparison(Parameter('c'), '<=', Multiply(Constant(0.5), Parameter('k')), ('g',))), + Mask(ParameterDefined('flag', ('g',))), + ), 'the arithmetic side is a program expression, and the where is the mask the file wrote' + assert assumption_message('sound', assumption) == ( + "assumption 'sound' does not hold for the data bound to 'c', 'k'" + ), 'the refusal names what the consumer bound, so it can say which column is wrong' + + +def test_an_assumption_refuses_in_the_words_the_file_wrote(): + """``description:`` reached no consumer: the block held it and neither the program nor the sentence did. + + The names alone say which columns are wrong. What the author wrote says + why the rule is there, which is what the reader of a refusal needs, so + the sentence quotes it where the file wrote one. + """ + reason = 'a shape with no room between its bounds cannot be cut' + program = to_program(override(SHAPES_MODEL, assumptions={'sound': {'holds': 'c <= k', 'description': reason}})) + assumption = program.assumptions['sound'] + + assert assumption.description == reason, 'the program carries it, so a consumer needs no second read of the file' + assert assumption_message('sound', assumption) == ( + f"assumption 'sound' does not hold for the data bound to 'c', 'k' \N{EM DASH} {reason}" + ), 'the sentence trails what the author wrote' + + def test_a_cased_side_reads_the_data_its_regions_are_decided_by(): """`names_read` promised every parameter and relation the sides read, and dropped the `when:` of a cased entry: the walk descends a `Cases` by its values alone.""" diff --git a/tests/test_piecewise.py b/tests/test_piecewise.py index d951b26a..536988e2 100644 --- a/tests/test_piecewise.py +++ b/tests/test_piecewise.py @@ -29,7 +29,7 @@ Increasing, LastOf, MaskOf, - check_message, + assumption_message, ) from tests.fixtures import DISPATCH_MODEL, override, raw_of, schema_of @@ -378,7 +378,7 @@ def test_a_gate_that_is_not_a_variable_is_refused(activity, match): @pytest.mark.parametrize(('raw', 'expected'), _CURVATURE_CASES) def test_a_method_names_the_curvature_it_is_exact_for(raw, expected): """The consumer holding the breakpoints checks the shape; this says what to check for.""" - answer = next((c.curvature for c in to_program(raw).piecewise['cost_curve'].checks if isinstance(c, Curved)), None) + answer = next((c.curvature for c in to_program(raw).assumptions.values() if isinstance(c, Curved)), None) assert answer == expected assert answer is None or answer in CURVATURES, ( f'{answer!r} is not one of the curvatures the package publishes, so a consumer ' @@ -423,30 +423,40 @@ def test_a_file_supplied_mask_derives_nothing(): ) assert program.parameters['reach'].derivation is None, 'the file declared it, so the caller binds it' - assert Contiguous('reach', None) in program.piecewise['cost_curve'].checks, ( + assert program.assumptions['cost_curve points'] == Contiguous('cost_curve', 'reach', None), ( 'the mask is still one the data has to make contiguous, with no values parameter behind it' ) -def test_a_block_is_kept_as_the_checks_a_consumer_binding_it_runs(): - """Every condition a curve puts on its data arrives carrying its own subjects.""" - curve = to_program(LP_MASKED).piecewise['cost_curve'] +def test_a_block_assumes_of_its_data_what_the_method_implies(): + """Every condition a curve puts on its data stands with the file's own, carrying its own subjects.""" + program = to_program(LP_MASKED) - 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'), - AtLeastTwo('bp', 'cost_curve_points'), - Contiguous('cost_curve_points', 'bp_x'), + assert program.piecewise['cost_curve'].breakpoints == ('bp_x', 'bp_y'), 'the values parameters, in link order' + assert program.assumptions == { + 'cost_curve increasing': Increasing('cost_curve', 'lp', 'bp_x', 'bp'), + 'cost_curve curvature': Curved('cost_curve', 'lp', 'bp_x', 'bp_y', 'bp', 'convex'), + 'cost_curve breakpoints': AtLeastTwo('cost_curve', 'bp', 'cost_curve_points'), + 'cost_curve points': Contiguous('cost_curve', 'cost_curve_points', 'bp_x'), }, 'an lp curve with a mask assumes all four, each against the names the file wrote' - plain = to_program(raw_of(NONCONVEX_YAML)).piecewise['cost_curve'] - assert plain.checks == (), 'adjacency over a whole curve is exact for any shape, and masks nothing' + plain = to_program(raw_of(NONCONVEX_YAML)) + assert plain.assumptions == {}, 'adjacency over a whole curve is exact for any shape, and masks nothing' + + +def test_a_curves_conditions_cannot_collide_with_a_written_assumption(): + """The two kinds share one mapping, and the space in a derived name is what keeps them apart. + + A declaration is named the way an expression writes it, so a file cannot + write `cost_curve increasing` and quietly replace the curve's own. + """ + with pytest.raises(LanguageError, match="'cost_curve increasing' is not a name"): + to_program(override(LP, assumptions={'cost_curve increasing': 'bp_x > 0'})) @pytest.mark.parametrize('kind', get_args(Check), ids=lambda k: k.__name__) def test_every_check_has_a_sentence(kind): - curve = to_program(LP_MASKED).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':") + found = [(n, c) for n, c in to_program(LP_MASKED).assumptions.items() if isinstance(c, kind)] + assert found, 'the fixture is the block that assumes everything' + name, check = found[0] + assert assumption_message(name, check).startswith("piecewise 'cost_curve':") diff --git a/tests/test_reading_page.py b/tests/test_reading_page.py index 60725ac6..57453ba0 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) == 12, 'every `expression # value` line on the page is checked; one without one is not' + assert len(claims) == 16, '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}' diff --git a/tests/test_validation.py b/tests/test_validation.py index eece7bf6..b1790d02 100644 --- a/tests/test_validation.py +++ b/tests/test_validation.py @@ -1244,6 +1244,95 @@ def test_the_at_a_sum_landing_on_the_key_names_is_one_the_language_takes(self): _schema(objective={'expression': f'sum({rewrite})'}) +class TestAssumptions: + """What an ``assumptions:`` entry may state, and what the load refuses. + + Everything here is about the data, so nothing in it is decided at load but + the shape of the predicate: the entry is refused where the connectives + already settle it, and where it names a variable, which is what the solver + decides rather than what the caller binds. + """ + + @pytest.mark.parametrize( + ('entry', 'fragments'), + [ + pytest.param( + 'c > 0 OR true', + ('folds to true', 'assumes nothing of the data'), + id='a-predicate-that-is-always-true', + ), + pytest.param( + 'false AND c > 0', + ('folds to false', 'holds on no data at all'), + id='a-predicate-that-is-always-false', + ), + pytest.param( + 'p', + ("variable 'p' stands in what the assumption assumes",), + id='a-variable-in-the-predicate', + ), + pytest.param( + {'holds': 'c > 0', 'where': 'p'}, + ("variable 'p' stands in what the assumption is checked where",), + id='a-variable-in-the-where', + ), + pytest.param( + {'holds': 'c > 0', 'where': 'false'}, + ('folds to false', 'checked on no row'), + id='a-where-that-is-always-false', + ), + pytest.param( + {'holds': 'c > 0', 'where': 'p AND false'}, + ('folds to false', 'checked on no row'), + id='a-where-that-hides-a-variable-behind-a-fold', + ), + pytest.param( + {'holds': 'c > 0', 'where': 'flag OR true'}, + ('folds to true', 'narrows nothing'), + id='a-where-that-is-always-true', + ), + pytest.param( + 'c > tag', + ("'tag' is declared dtype: str, and an expression is arithmetic",), + id='a-label-parameter-on-a-side', + ), + pytest.param('nope > 0', ("'nope' not found",), id='an-unknown-name'), + ], + ) + def test_an_entry_the_language_refuses(self, entry, fragments): + message = _refusal(assumptions={'sound': entry}) + assert "Assumption 'sound'" in message + for fragment in fragments: + assert fragment in message + + @pytest.mark.parametrize( + 'entry', + [ + pytest.param('c <= k', id='two-parameters'), + pytest.param('c <= 0.5 * k', id='arithmetic-on-a-side'), + pytest.param('sum(c, over=g) >= k', id='a-reduction-on-a-side'), + pytest.param("lk == 'north' AND c > 0", id='a-relation-and-a-connective'), + pytest.param({'holds': 'c > 0', 'where': 'flag'}, id='a-where-of-its-own'), + pytest.param({'holds': 'c > 0', 'description': 'costs are positive'}, id='a-description'), + ], + ) + def test_an_entry_the_language_admits(self, entry): + spec = _schema(assumptions={'sound': entry}) + assert set(spec.assumptions) == {'sound'}, 'the entry loads under the name the file wrote' + + def test_an_entry_round_trips_as_the_form_it_was_written_in(self): + """A bare string stays one, and a mapping keeps only the keys it carried.""" + spec = _schema(assumptions={'plain': 'c > 0', 'masked': {'holds': 'c > 0', 'where': 'flag'}}) + assert spec.to_dict()['assumptions'] == {'plain': 'c > 0', 'masked': {'holds': 'c > 0', 'where': 'flag'}}, ( + 'neither form gains a key the file did not write' + ) + + def test_a_variable_free_comparison_is_pointed_at_assumptions_rather_than_at_data_prep(self): + """The refusal named nowhere to put the fact until this section existed.""" + message = _refusal(constraints={'cap': {'dims': ['g'], 'expression': 'c <= 1'}}) + assert '`assumptions:`' in message, 'the refusal names the section that now holds such a fact' + + class TestTheFrontDoor: def test_a_list_of_models_is_not_a_model(self): """Composition is Python's, not the file's (#30) — and the refusal is the package's own, so the CLI's one except catches it.""" diff --git a/tests/typesetting/golden/latex.out b/tests/typesetting/golden/latex.out index 3c711fa9..80745fd2 100644 --- a/tests/typesetting/golden/latex.out +++ b/tests/typesetting/golden/latex.out @@ -15,6 +15,7 @@ \item[{$\mathcal{Z}$}] index $z$ --- \texttt{zone} with $\mathrm{zone\_of}: \mathcal{B} \to \mathcal{Z},\ \mathrm{area\_of}: \mathcal{B} \to \mathcal{Z},\ \mathrm{gen\_zone}: \mathcal{G} \times \mathcal{T} \to \mathcal{Z}$ \item[{$\mathcal{S}$}] index $s$ --- \texttt{season} with $\mathrm{season\_of}: \mathcal{T} \to \mathcal{S}$ \item[{$\mathcal{E}$}] index $e$ --- \texttt{technology} with $\mathrm{gen\_bt}: \mathcal{G} \to \mathcal{B} \times \mathcal{E}$ +\item[{$\mathcal{A}$}] index $a$ --- \texttt{bp} \end{description} \paragraph{Parameters} @@ -31,6 +32,13 @@ \item[{$\mathrm{lead}$}] \texttt{lead} over $\mathcal{G}$ \item[{$\mathrm{budget}$}] \texttt{budget} (scalar) \item[{$\mathrm{growth}$}] \texttt{growth} (scalar) +\item[{$\mathrm{bp\_x}$}] \texttt{bp\_x} over $\mathcal{A}$ +\item[{$\mathrm{bp\_y}$}] \texttt{bp\_y} over $\mathcal{A}$ +\item[{$\mathrm{heat}^{\mathrm{x}}$}] \texttt{heat\_x} over $\mathcal{A}$ +\item[{$\mathrm{heat}^{\mathrm{y}}$}] \texttt{heat\_y} over $\mathcal{A}$ +\item[{$\mathrm{fuel}^{\mathrm{curve,points}}$}] \texttt{fuel\_curve\_points} over $\mathcal{A}$ --- where 'bp\_x' has a row, and so where the curve runs +\item[{$\mathrm{fuel}^{\mathrm{curve,starts}}$}] \texttt{fuel\_curve\_starts} over $\mathcal{A}$ --- the first breakpoint of each curve +\item[{$\mathrm{fuel}^{\mathrm{curve,ends}}$}] \texttt{fuel\_curve\_ends} over $\mathcal{A}$ --- the last breakpoint of each curve \end{description} \paragraph{Variables} @@ -45,6 +53,10 @@ \item[{$\mathit{reserve}$}] \texttt{reserve} (scalar) \item[{$\mathit{headroom}$}] \texttt{headroom} (scalar) \item[{$\mathit{weight}$}] \texttt{weight} over $\mathcal{T} \times \mathcal{G}$ +\item[{$p^{\mathrm{bp}}$}] \texttt{p\_bp} over $\mathcal{T}$ +\item[{$\mathit{fuel}$}] \texttt{fuel} over $\mathcal{T}$ +\item[{$q^{\mathrm{bp}}$}] \texttt{q\_bp} over $\mathcal{T}$ +\item[{$\mathit{heat}$}] \texttt{heat} over $\mathcal{T}$ \end{description} \paragraph{Definitions} @@ -118,7 +130,13 @@ \text{margin} && p_{t,g} & \le \mathrm{p}^{\mathrm{max}}_{g} && \forall\, t \in \mathcal{T},\ g \in \mathcal{G} \,:\, \mathrm{p}^{\mathrm{max}}_{g} - \mathrm{p}^{\mathrm{min}}_{g} > \frac{\mathrm{cost}_{g}}{2} \\ \text{ramped} && \mathit{slack}_{t} & \le \mathrm{load}_{t,b} && \forall\, t \in \mathcal{T},\ b \in \mathcal{B} \,:\, \mathrm{load}_{t,b} - \mathrm{load}_{t \boxminus_{0} 1,b} \le \mathrm{zone\_cap}_{\mathrm{zone\_of}(b)} \wedge \mathrm{pos}(t) > 0 \\ \text{covered} && \sum_{t \in \mathcal{T},\ g \in \mathcal{G}} p_{t,g} & \le \mathrm{budget} && \text{where } \sum_{g \in \mathcal{G}} \mathrm{p}^{\mathrm{max}}_{g} \ge \mathrm{budget} \\ -\text{capped} && p_{t,g} & \le \mathrm{p}^{\mathrm{max}}_{g} && \forall\, t \in \mathcal{T},\ g \in \mathcal{G} \,:\, \mathrm{spend}^{\mathrm{cap}}_{g} > 0 \vee \neg \mathrm{is\_flexible}_{g} +\text{capped} && p_{t,g} & \le \mathrm{p}^{\mathrm{max}}_{g} && \forall\, t \in \mathcal{T},\ g \in \mathcal{G} \,:\, \mathrm{spend}^{\mathrm{cap}}_{g} > 0 \vee \neg \mathrm{is\_flexible}_{g} \\ +\text{fuel\_curve\_chord} && \mathit{fuel}_{t} \cdot \left( \mathrm{bp\_x}_{a} - \mathrm{bp\_x}_{a \boxminus_{0} 1} \right) & \ge \left( \mathrm{bp\_y}_{a} - \mathrm{bp\_y}_{a \boxminus_{0} 1} \right) \cdot \left( p^{\mathrm{bp}}_{t} - \mathrm{bp\_x}_{a} \right) + \mathrm{bp\_y}_{a} \cdot \left( \mathrm{bp\_x}_{a} - \mathrm{bp\_x}_{a \boxminus_{0} 1} \right) && \forall\, t \in \mathcal{T},\ a \in \mathcal{A} \,:\, \mathrm{fuel}^{\mathrm{curve,points}}_{a} \wedge \neg \mathrm{fuel}^{\mathrm{curve,starts}}_{a} \\ +\text{fuel\_curve\_domain\_lo} && p^{\mathrm{bp}}_{t} & \ge \mathrm{bp\_x}_{a} && \forall\, t \in \mathcal{T},\ a \in \mathcal{A} \,:\, \mathrm{fuel}^{\mathrm{curve,starts}}_{a} \\ +\text{fuel\_curve\_domain\_hi} && p^{\mathrm{bp}}_{t} & \le \mathrm{bp\_x}_{a} && \forall\, t \in \mathcal{T},\ a \in \mathcal{A} \,:\, \mathrm{fuel}^{\mathrm{curve,ends}}_{a} \\ +\text{heat\_curve\_chord} && \mathit{heat}_{t} \cdot \left( \mathrm{heat}^{\mathrm{x}}_{a} - \mathrm{heat}^{\mathrm{x}}_{a \boxminus_{0} 1} \right) & \le \left( \mathrm{heat}^{\mathrm{y}}_{a} - \mathrm{heat}^{\mathrm{y}}_{a \boxminus_{0} 1} \right) \cdot \left( q^{\mathrm{bp}}_{t} - \mathrm{heat}^{\mathrm{x}}_{a} \right) + \mathrm{heat}^{\mathrm{y}}_{a} \cdot \left( \mathrm{heat}^{\mathrm{x}}_{a} - \mathrm{heat}^{\mathrm{x}}_{a \boxminus_{0} 1} \right) && \forall\, t \in \mathcal{T},\ a \in \mathcal{A} \,:\, \mathrm{pos}(a) \neq 0 \\ +\text{heat\_curve\_domain\_lo} && q^{\mathrm{bp}}_{t} & \ge \mathrm{heat}^{\mathrm{x}}_{a} && \forall\, t \in \mathcal{T},\ a \in \mathcal{A} \,:\, \mathrm{pos}(a) = 0 \\ +\text{heat\_curve\_domain\_hi} && q^{\mathrm{bp}}_{t} & \le \mathrm{heat}^{\mathrm{x}}_{a} && \forall\, t \in \mathcal{T},\ a \in \mathcal{A} \,:\, \mathrm{pos}(a) = \lvert \mathcal{A} \rvert - 1 \end{align} \paragraph{Definitions} @@ -142,7 +160,30 @@ \text{reserve} && \mathit{reserve} & \ge 0 \\ \text{headroom} && \mathit{headroom} & \ge 0 && \text{where } \mathrm{budget} \text{ is defined} \\ \text{weight} && 0 \le \mathit{weight}_{t,g} & \le 1 && \forall\, t \in \mathcal{T},\ g \in \mathcal{G} \\ -\text{weight sos} && \left( \mathit{weight}_{t,g} \right)_{g \in \mathcal{G}} & \in \mathrm{SOS}2 && \forall\, t \in \mathcal{T} +\text{weight sos} && \left( \mathit{weight}_{t,g} \right)_{g \in \mathcal{G}} & \in \mathrm{SOS}2 && \forall\, t \in \mathcal{T} \\ +\text{p\_bp} && 0 \le p^{\mathrm{bp}}_{t} & \le 100 && \forall\, t \in \mathcal{T} \\ +\text{fuel} && \mathit{fuel}_{t} & \ge 0 && \forall\, t \in \mathcal{T} \\ +\text{q\_bp} && 0 \le q^{\mathrm{bp}}_{t} & \le 100 && \forall\, t \in \mathcal{T} \\ +\text{heat} && \mathit{heat}_{t} & \ge 0 && \forall\, t \in \mathcal{T} +\end{align} + +\paragraph{Assumptions} +\begin{align} +\text{bounds\_do\_not\_cross} && \mathrm{p}^{\mathrm{min}}_{g} & \le \mathrm{p}^{\mathrm{max}}_{g} && \forall\, g \in \mathcal{G} \\ +\text{efficiency\_is\_a\_fraction} && \mathrm{eta}_{g} > 0 \wedge \mathrm{eta}_{g} \le 1 & && \forall\, g \in \mathcal{G} \\ +\text{lead\_times\_are\_short} && \mathrm{lead}_{g} & \le 3 && \forall\, g \in \mathcal{G} \\ +\text{zones\_agree} && \mathrm{zone\_of}(b) & = \mathrm{area\_of}(b) && \forall\, b \in \mathcal{B} \\ +\text{budget\_covers\_the\_peak} && \sum_{g \in \mathcal{G}} \mathrm{p}^{\mathrm{max}}_{g} & \ge \mathrm{budget} \\ +\text{ramps\_are\_gentle} && \mathrm{load}_{t,b} - \mathrm{load}_{t \boxminus_{0} 1,b} & \le \mathrm{budget} && \forall\, t \in \mathcal{T},\ b \in \mathcal{B} \,:\, \mathrm{pos}(t) > 0 \\ +\text{flexible\_units\_have\_headroom} && \mathrm{p}^{\mathrm{min}}_{g} & < \mathrm{p}^{\mathrm{max}}_{g} && \forall\, g \in \mathcal{G} \,:\, \mathrm{is\_flexible}_{g} \\ +\text{northern\_demand\_is\_real} && \mathrm{load}_{t,b} & \ge 0 && \forall\, t \in \mathcal{T},\ b \in \mathcal{B} \,:\, \mathrm{zone\_of}(b) = \text{'}\mathrm{north}\text{'} \\ +\text{fuel\_curve increasing} && \mathrm{bp\_x}_{a - 1} & < \mathrm{bp\_x}_{a} && \forall\, a \in \mathcal{A} \,:\, \mathrm{fuel}^{\mathrm{curve,points}}_{a} \wedge \mathrm{fuel}^{\mathrm{curve,points}}_{a - 1} \\ +\text{fuel\_curve curvature} && \mathrm{bp\_y}_{a} & \text{ is a convex function of } \mathrm{bp\_x}_{a} \text{ along } a \\ +\text{fuel\_curve breakpoints} && \lvert \{ a \in \mathcal{A} \,:\, \mathrm{fuel}^{\mathrm{curve,points}}_{a} \} \rvert & \ge 2 \\ +\text{fuel\_curve points} && \{ a \in \mathcal{A} \,:\, \mathrm{fuel}^{\mathrm{curve,points}}_{a} \} & \text{ is one run of consecutive breakpoints} \\ +\text{heat\_curve increasing} && \mathrm{heat}^{\mathrm{x}}_{a - 1} & < \mathrm{heat}^{\mathrm{x}}_{a} && \forall\, a \in \mathcal{A} \\ +\text{heat\_curve curvature} && \mathrm{heat}^{\mathrm{y}}_{a} & \text{ is a concave function of } \mathrm{heat}^{\mathrm{x}}_{a} \text{ along } a \\ +\text{heat\_curve breakpoints} && \lvert \mathcal{A} \rvert & \ge 2 \end{align} \end{document} diff --git a/tests/typesetting/golden/markdown.out b/tests/typesetting/golden/markdown.out index 225d22ac..2b26c904 100644 --- a/tests/typesetting/golden/markdown.out +++ b/tests/typesetting/golden/markdown.out @@ -12,6 +12,7 @@ every character a notation escapes, set as text: link\_to, 100% & \#1 costs \$5 | $`\mathcal{Z}`$ | index $`z`$ — `zone` with $`\mathrm{zone\_of}: \mathcal{B} \to \mathcal{Z},\ \mathrm{area\_of}: \mathcal{B} \to \mathcal{Z},\ \mathrm{gen\_zone}: \mathcal{G} \times \mathcal{T} \to \mathcal{Z}`$ | | $`\mathcal{S}`$ | index $`s`$ — `season` with $`\mathrm{season\_of}: \mathcal{T} \to \mathcal{S}`$ | | $`\mathcal{E}`$ | index $`e`$ — `technology` with $`\mathrm{gen\_bt}: \mathcal{G} \to \mathcal{B} \times \mathcal{E}`$ | +| $`\mathcal{A}`$ | index $`a`$ — `bp` | #### Parameters @@ -29,6 +30,13 @@ every character a notation escapes, set as text: link\_to, 100% & \#1 costs \$5 | $`\mathrm{lead}`$ | `lead` over $`\mathcal{G}`$ | | $`\mathrm{budget}`$ | `budget` (scalar) | | $`\mathrm{growth}`$ | `growth` (scalar) | +| $`\mathrm{bp\_x}`$ | `bp_x` over $`\mathcal{A}`$ | +| $`\mathrm{bp\_y}`$ | `bp_y` over $`\mathcal{A}`$ | +| $`\mathrm{heat}^{\mathrm{x}}`$ | `heat_x` over $`\mathcal{A}`$ | +| $`\mathrm{heat}^{\mathrm{y}}`$ | `heat_y` over $`\mathcal{A}`$ | +| $`\mathrm{fuel}^{\mathrm{curve,points}}`$ | `fuel_curve_points` over $`\mathcal{A}`$ — where 'bp\_x' has a row, and so where the curve runs | +| $`\mathrm{fuel}^{\mathrm{curve,starts}}`$ | `fuel_curve_starts` over $`\mathcal{A}`$ — the first breakpoint of each curve | +| $`\mathrm{fuel}^{\mathrm{curve,ends}}`$ | `fuel_curve_ends` over $`\mathcal{A}`$ — the last breakpoint of each curve | #### Variables @@ -44,6 +52,10 @@ every character a notation escapes, set as text: link\_to, 100% & \#1 costs \$5 | $`\mathit{reserve}`$ | `reserve` (scalar) | | $`\mathit{headroom}`$ | `headroom` (scalar) | | $`\mathit{weight}`$ | `weight` over $`\mathcal{T} \times \mathcal{G}`$ | +| $`p^{\mathrm{bp}}`$ | `p_bp` over $`\mathcal{T}`$ | +| $`\mathit{fuel}`$ | `fuel` over $`\mathcal{T}`$ | +| $`q^{\mathrm{bp}}`$ | `q_bp` over $`\mathcal{T}`$ | +| $`\mathit{heat}`$ | `heat` over $`\mathcal{T}`$ | #### Definitions @@ -329,6 +341,42 @@ p_{t,g} \le \mathrm{p}^{\mathrm{max}}_{g} \qquad \forall\, t \in \mathcal{T},\ g p_{t,g} \le \mathrm{p}^{\mathrm{max}}_{g} \qquad \forall\, t \in \mathcal{T},\ g \in \mathcal{G} \,:\, \mathrm{spend}^{\mathrm{cap}}_{g} > 0 \vee \neg \mathrm{is\_flexible}_{g} ``` +**`fuel_curve_chord`** + +```math +\mathit{fuel}_{t} \cdot \left( \mathrm{bp\_x}_{a} - \mathrm{bp\_x}_{a \boxminus_{0} 1} \right) \ge \left( \mathrm{bp\_y}_{a} - \mathrm{bp\_y}_{a \boxminus_{0} 1} \right) \cdot \left( p^{\mathrm{bp}}_{t} - \mathrm{bp\_x}_{a} \right) + \mathrm{bp\_y}_{a} \cdot \left( \mathrm{bp\_x}_{a} - \mathrm{bp\_x}_{a \boxminus_{0} 1} \right) \qquad \forall\, t \in \mathcal{T},\ a \in \mathcal{A} \,:\, \mathrm{fuel}^{\mathrm{curve,points}}_{a} \wedge \neg \mathrm{fuel}^{\mathrm{curve,starts}}_{a} +``` + +**`fuel_curve_domain_lo`** + +```math +p^{\mathrm{bp}}_{t} \ge \mathrm{bp\_x}_{a} \qquad \forall\, t \in \mathcal{T},\ a \in \mathcal{A} \,:\, \mathrm{fuel}^{\mathrm{curve,starts}}_{a} +``` + +**`fuel_curve_domain_hi`** + +```math +p^{\mathrm{bp}}_{t} \le \mathrm{bp\_x}_{a} \qquad \forall\, t \in \mathcal{T},\ a \in \mathcal{A} \,:\, \mathrm{fuel}^{\mathrm{curve,ends}}_{a} +``` + +**`heat_curve_chord`** + +```math +\mathit{heat}_{t} \cdot \left( \mathrm{heat}^{\mathrm{x}}_{a} - \mathrm{heat}^{\mathrm{x}}_{a \boxminus_{0} 1} \right) \le \left( \mathrm{heat}^{\mathrm{y}}_{a} - \mathrm{heat}^{\mathrm{y}}_{a \boxminus_{0} 1} \right) \cdot \left( q^{\mathrm{bp}}_{t} - \mathrm{heat}^{\mathrm{x}}_{a} \right) + \mathrm{heat}^{\mathrm{y}}_{a} \cdot \left( \mathrm{heat}^{\mathrm{x}}_{a} - \mathrm{heat}^{\mathrm{x}}_{a \boxminus_{0} 1} \right) \qquad \forall\, t \in \mathcal{T},\ a \in \mathcal{A} \,:\, \mathrm{pos}(a) \neq 0 +``` + +**`heat_curve_domain_lo`** + +```math +q^{\mathrm{bp}}_{t} \ge \mathrm{heat}^{\mathrm{x}}_{a} \qquad \forall\, t \in \mathcal{T},\ a \in \mathcal{A} \,:\, \mathrm{pos}(a) = 0 +``` + +**`heat_curve_domain_hi`** + +```math +q^{\mathrm{bp}}_{t} \le \mathrm{heat}^{\mathrm{x}}_{a} \qquad \forall\, t \in \mathcal{T},\ a \in \mathcal{A} \,:\, \mathrm{pos}(a) = \lvert \mathcal{A} \rvert - 1 +``` + #### Definitions **`spend_cap`** @@ -428,3 +476,119 @@ p_{t,g} \le \mathrm{p}^{\mathrm{max}}_{g} \qquad \forall\, t \in \mathcal{T},\ g ```math \left( \mathit{weight}_{t,g} \right)_{g \in \mathcal{G}} \in \mathrm{SOS}2 \qquad \forall\, t \in \mathcal{T} ``` + +**`p_bp`** + +```math +0 \le p^{\mathrm{bp}}_{t} \le 100 \qquad \forall\, t \in \mathcal{T} +``` + +**`fuel`** + +```math +\mathit{fuel}_{t} \ge 0 \qquad \forall\, t \in \mathcal{T} +``` + +**`q_bp`** + +```math +0 \le q^{\mathrm{bp}}_{t} \le 100 \qquad \forall\, t \in \mathcal{T} +``` + +**`heat`** + +```math +\mathit{heat}_{t} \ge 0 \qquad \forall\, t \in \mathcal{T} +``` + +#### Assumptions + +**`bounds_do_not_cross`** + +```math +\mathrm{p}^{\mathrm{min}}_{g} \le \mathrm{p}^{\mathrm{max}}_{g} \qquad \forall\, g \in \mathcal{G} +``` + +**`efficiency_is_a_fraction`** + +```math +\mathrm{eta}_{g} > 0 \wedge \mathrm{eta}_{g} \le 1 \qquad \forall\, g \in \mathcal{G} +``` + +**`lead_times_are_short`** + +```math +\mathrm{lead}_{g} \le 3 \qquad \forall\, g \in \mathcal{G} +``` + +**`zones_agree`** + +```math +\mathrm{zone\_of}(b) = \mathrm{area\_of}(b) \qquad \forall\, b \in \mathcal{B} +``` + +**`budget_covers_the_peak`** + +```math +\sum_{g \in \mathcal{G}} \mathrm{p}^{\mathrm{max}}_{g} \ge \mathrm{budget} +``` + +**`ramps_are_gentle`** + +```math +\mathrm{load}_{t,b} - \mathrm{load}_{t \boxminus_{0} 1,b} \le \mathrm{budget} \qquad \forall\, t \in \mathcal{T},\ b \in \mathcal{B} \,:\, \mathrm{pos}(t) > 0 +``` + +**`flexible_units_have_headroom`** + +```math +\mathrm{p}^{\mathrm{min}}_{g} < \mathrm{p}^{\mathrm{max}}_{g} \qquad \forall\, g \in \mathcal{G} \,:\, \mathrm{is\_flexible}_{g} +``` + +**`northern_demand_is_real`** + +```math +\mathrm{load}_{t,b} \ge 0 \qquad \forall\, t \in \mathcal{T},\ b \in \mathcal{B} \,:\, \mathrm{zone\_of}(b) = \text{'}\mathrm{north}\text{'} +``` + +**`fuel_curve increasing`** + +```math +\mathrm{bp\_x}_{a - 1} < \mathrm{bp\_x}_{a} \qquad \forall\, a \in \mathcal{A} \,:\, \mathrm{fuel}^{\mathrm{curve,points}}_{a} \wedge \mathrm{fuel}^{\mathrm{curve,points}}_{a - 1} +``` + +**`fuel_curve curvature`** + +```math +\mathrm{bp\_y}_{a} \text{ is a convex function of } \mathrm{bp\_x}_{a} \text{ along } a +``` + +**`fuel_curve breakpoints`** + +```math +\lvert \{ a \in \mathcal{A} \,:\, \mathrm{fuel}^{\mathrm{curve,points}}_{a} \} \rvert \ge 2 +``` + +**`fuel_curve points`** + +```math +\{ a \in \mathcal{A} \,:\, \mathrm{fuel}^{\mathrm{curve,points}}_{a} \} \text{ is one run of consecutive breakpoints} +``` + +**`heat_curve increasing`** + +```math +\mathrm{heat}^{\mathrm{x}}_{a - 1} < \mathrm{heat}^{\mathrm{x}}_{a} \qquad \forall\, a \in \mathcal{A} +``` + +**`heat_curve curvature`** + +```math +\mathrm{heat}^{\mathrm{y}}_{a} \text{ is a concave function of } \mathrm{heat}^{\mathrm{x}}_{a} \text{ along } a +``` + +**`heat_curve breakpoints`** + +```math +\lvert \mathcal{A} \rvert \ge 2 +``` diff --git a/tests/typesetting/golden/model.yaml b/tests/typesetting/golden/model.yaml index 43de710a..15004aab 100644 --- a/tests/typesetting/golden/model.yaml +++ b/tests/typesetting/golden/model.yaml @@ -19,6 +19,7 @@ dimensions: zone: { dtype: str } season: { dtype: str } technology: { dtype: str } + bp: { dtype: int } # the breakpoint axis the two curves run along relations: gen_bus: { key: generator, values: bus } @@ -43,6 +44,10 @@ parameters: lead: { dims: [generator], dtype: int } budget: { dims: [] } # scalar: the legend says so rather than printing an empty product growth: { dims: [] } # the base of a power; the exponent is `lead`, a column + bp_x: { dims: [bp] } # the masked curve's x-axis, and the parameter its mask is derived from + bp_y: { dims: [bp] } + heat_x: { dims: [bp] } # the whole-axis curve, bounded the other way + heat_y: { dims: [bp] } variables: p: # both bounds, and a where with all three connectives @@ -77,6 +82,33 @@ variables: weight: # the family a sos runs along dims: [snapshot, generator] bounds: { lower: 0, upper: 1 } + p_bp: # the masked curve's x link + dims: [snapshot] + bounds: { lower: 0, upper: 100 } + fuel: # its y link, bounded above, which is what makes the curve a convex one + dims: [snapshot] + bounds: { lower: 0 } + q_bp: # the whole-axis curve's x link + dims: [snapshot] + bounds: { lower: 0, upper: 100 } + heat: # its y link, bounded below, so that curve is concave + dims: [snapshot] + bounds: { lower: 0 } + +piecewise: + fuel_curve: # an lp curve masked by one of its own breakpoints: every condition a method puts on data + over: bp + method: lp + points: bp_x + links: + - [p_bp, bp_x] + - [fuel, bp_y, ">="] + heat_curve: # the same method bounded the other way over a whole axis: a concave curve, and no mask + over: bp + method: lp + links: + - [q_bp, heat_x] + - [heat, heat_y, "<="] sos: adjacent: # at most two adjacent members nonzero, one set per snapshot @@ -246,6 +278,23 @@ constraints: where: "spend_cap > 0 OR NOT is_flexible" expression: p <= p_max +assumptions: # what the data has to satisfy for the answer to mean anything + bounds_do_not_cross: "p_min <= p_max" # two parameters, which is arithmetic like any other + efficiency_is_a_fraction: "eta > 0 AND eta <= 1" # a connective, so the line has no relation to align on + lead_times_are_short: "lead <= 3" # one parameter against a literal + zones_agree: "zone_of == area_of" # two maps into one set, compared row by row + budget_covers_the_peak: "sum(p_max, over=generator) >= budget" # a reduction on a side, leaving nothing to quantify + ramps_are_gentle: # a translation inside arithmetic, and a position keeping the vacated row out + holds: "load - shift(load, along=snapshot, offset=1, edge=0) <= budget" + where: "position(snapshot) > 0" + flexible_units_have_headroom: # a bare bool parameter as the where + holds: "p_min < p_max" + where: "is_flexible" + description: a unit that cannot be turned down needs somewhere to go + northern_demand_is_real: # a relation comparison as the where, over a frame two dims wide + holds: "load >= 0" + where: "zone_of == 'north'" + 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 diff --git a/tests/typesetting/golden/typst.out b/tests/typesetting/golden/typst.out index 97bf944c..9771b28f 100644 --- a/tests/typesetting/golden/typst.out +++ b/tests/typesetting/golden/typst.out @@ -10,6 +10,7 @@ every character a notation escapes, set as text: link\_to, 100% & \#1 costs \$5 / $cal(Z)$: index $z$ --- `zone` with $upright("zone_of"): cal(B) arrow.r cal(Z), upright("area_of"): cal(B) arrow.r cal(Z), upright("gen_zone"): cal(G) times cal(T) arrow.r cal(Z)$ / $cal(S)$: index $s$ --- `season` with $upright("season_of"): cal(T) arrow.r cal(S)$ / $cal(E)$: index $e$ --- `technology` with $upright("gen_bt"): cal(G) arrow.r cal(B) times cal(E)$ +/ $cal(A)$: index $a$ --- `bp` == Parameters / $upright("p")^(upright("max"))$: `p_max` over $cal(G)$ @@ -24,6 +25,13 @@ every character a notation escapes, set as text: link\_to, 100% & \#1 costs \$5 / $upright("lead")$: `lead` over $cal(G)$ / $upright("budget")$: `budget` (scalar) / $upright("growth")$: `growth` (scalar) +/ $upright("bp_x")$: `bp_x` over $cal(A)$ +/ $upright("bp_y")$: `bp_y` over $cal(A)$ +/ $upright("heat")^(upright("x"))$: `heat_x` over $cal(A)$ +/ $upright("heat")^(upright("y"))$: `heat_y` over $cal(A)$ +/ $upright("fuel")^(upright("curve,points"))$: `fuel_curve_points` over $cal(A)$ --- where 'bp\_x' has a row, and so where the curve runs +/ $upright("fuel")^(upright("curve,starts"))$: `fuel_curve_starts` over $cal(A)$ --- the first breakpoint of each curve +/ $upright("fuel")^(upright("curve,ends"))$: `fuel_curve_ends` over $cal(A)$ --- the last breakpoint of each curve == Variables / $p$: `p` over $cal(T) times cal(G)$ @@ -36,6 +44,10 @@ every character a notation escapes, set as text: link\_to, 100% & \#1 costs \$5 / $italic("reserve")$: `reserve` (scalar) / $italic("headroom")$: `headroom` (scalar) / $italic("weight")$: `weight` over $cal(T) times cal(G)$ +/ $p^(upright("bp"))$: `p_bp` over $cal(T)$ +/ $italic("fuel")$: `fuel` over $cal(T)$ +/ $q^(upright("bp"))$: `q_bp` over $cal(T)$ +/ $italic("heat")$: `heat` over $cal(T)$ == Definitions / $upright("spend")^(upright("cap"))$: `spend_cap` over $cal(G)$ @@ -105,7 +117,13 @@ $ upright("budgeted") & italic("spend")_(t) & <= upright("budget") & forall t in upright("margin") & p_(t,g) & <= upright("p")^(upright("max"))_(g) & forall t in cal(T), g in cal(G) colon upright("p")^(upright("max"))_(g) - upright("p")^(upright("min"))_(g) > frac(upright("cost")_(g), 2) \ upright("ramped") & italic("slack")_(t) & <= upright("load")_(t,b) & forall t in cal(T), b in cal(B) colon upright("load")_(t,b) - upright("load")_(t minus.square_(0) 1,b) <= upright("zone_cap")_(upright("zone_of")(b)) and upright("pos")(t) > 0 \ upright("covered") & sum_(t in cal(T), g in cal(G)) p_(t,g) & <= upright("budget") & upright("where ") sum_(g in cal(G)) upright("p")^(upright("max"))_(g) >= upright("budget") \ - upright("capped") & p_(t,g) & <= upright("p")^(upright("max"))_(g) & forall t in cal(T), g in cal(G) colon upright("spend")^(upright("cap"))_(g) > 0 or not upright("is_flexible")_(g) $ + upright("capped") & p_(t,g) & <= upright("p")^(upright("max"))_(g) & forall t in cal(T), g in cal(G) colon upright("spend")^(upright("cap"))_(g) > 0 or not upright("is_flexible")_(g) \ + upright("fuel_curve_chord") & italic("fuel")_(t) dot (upright("bp_x")_(a) - upright("bp_x")_(a minus.square_(0) 1)) & >= (upright("bp_y")_(a) - upright("bp_y")_(a minus.square_(0) 1)) dot (p^(upright("bp"))_(t) - upright("bp_x")_(a)) + upright("bp_y")_(a) dot (upright("bp_x")_(a) - upright("bp_x")_(a minus.square_(0) 1)) & forall t in cal(T), a in cal(A) colon upright("fuel")^(upright("curve,points"))_(a) and not upright("fuel")^(upright("curve,starts"))_(a) \ + upright("fuel_curve_domain_lo") & p^(upright("bp"))_(t) & >= upright("bp_x")_(a) & forall t in cal(T), a in cal(A) colon upright("fuel")^(upright("curve,starts"))_(a) \ + upright("fuel_curve_domain_hi") & p^(upright("bp"))_(t) & <= upright("bp_x")_(a) & forall t in cal(T), a in cal(A) colon upright("fuel")^(upright("curve,ends"))_(a) \ + upright("heat_curve_chord") & italic("heat")_(t) dot (upright("heat")^(upright("x"))_(a) - upright("heat")^(upright("x"))_(a minus.square_(0) 1)) & <= (upright("heat")^(upright("y"))_(a) - upright("heat")^(upright("y"))_(a minus.square_(0) 1)) dot (q^(upright("bp"))_(t) - upright("heat")^(upright("x"))_(a)) + upright("heat")^(upright("y"))_(a) dot (upright("heat")^(upright("x"))_(a) - upright("heat")^(upright("x"))_(a minus.square_(0) 1)) & forall t in cal(T), a in cal(A) colon upright("pos")(a) != 0 \ + upright("heat_curve_domain_lo") & q^(upright("bp"))_(t) & >= upright("heat")^(upright("x"))_(a) & forall t in cal(T), a in cal(A) colon upright("pos")(a) = 0 \ + upright("heat_curve_domain_hi") & q^(upright("bp"))_(t) & <= upright("heat")^(upright("x"))_(a) & forall t in cal(T), a in cal(A) colon upright("pos")(a) = abs(cal(A)) - 1 $ == Definitions #set math.equation(numbering: "(1)") @@ -127,4 +145,26 @@ $ upright("p") & upright("p")^(upright("min"))_(g) <= p_(t,g) & <= upright("p")^ upright("reserve") & italic("reserve") & >= 0 \ 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) $ + upright("weight sos") & (italic("weight")_(t,g))_(g in cal(G)) & in upright("SOS")2 & forall t in cal(T) \ + upright("p_bp") & 0 <= p^(upright("bp"))_(t) & <= 100 & forall t in cal(T) \ + upright("fuel") & italic("fuel")_(t) & >= 0 & forall t in cal(T) \ + upright("q_bp") & 0 <= q^(upright("bp"))_(t) & <= 100 & forall t in cal(T) \ + upright("heat") & italic("heat")_(t) & >= 0 & forall t in cal(T) $ + +== Assumptions +#set math.equation(numbering: "(1)") +$ upright("bounds_do_not_cross") & upright("p")^(upright("min"))_(g) & <= upright("p")^(upright("max"))_(g) & forall g in cal(G) \ + upright("efficiency_is_a_fraction") & upright("eta")_(g) > 0 and upright("eta")_(g) <= 1 & & forall g in cal(G) \ + upright("lead_times_are_short") & upright("lead")_(g) & <= 3 & forall g in cal(G) \ + upright("zones_agree") & upright("zone_of")(b) & = upright("area_of")(b) & forall b in cal(B) \ + upright("budget_covers_the_peak") & sum_(g in cal(G)) upright("p")^(upright("max"))_(g) & >= upright("budget") \ + upright("ramps_are_gentle") & upright("load")_(t,b) - upright("load")_(t minus.square_(0) 1,b) & <= upright("budget") & forall t in cal(T), b in cal(B) colon upright("pos")(t) > 0 \ + upright("flexible_units_have_headroom") & upright("p")^(upright("min"))_(g) & < upright("p")^(upright("max"))_(g) & forall g in cal(G) colon upright("is_flexible")_(g) \ + upright("northern_demand_is_real") & upright("load")_(t,b) & >= 0 & forall t in cal(T), b in cal(B) colon upright("zone_of")(b) = upright("'north'") \ + upright("fuel_curve increasing") & upright("bp_x")_(a - 1) & < upright("bp_x")_(a) & forall a in cal(A) colon upright("fuel")^(upright("curve,points"))_(a) and upright("fuel")^(upright("curve,points"))_(a - 1) \ + upright("fuel_curve curvature") & upright("bp_y")_(a) & upright(" is a convex function of ") upright("bp_x")_(a) upright(" along ") a \ + upright("fuel_curve breakpoints") & abs({a in cal(A) colon upright("fuel")^(upright("curve,points"))_(a)}) & >= 2 \ + upright("fuel_curve points") & {a in cal(A) colon upright("fuel")^(upright("curve,points"))_(a)} & upright(" is one run of consecutive breakpoints") \ + upright("heat_curve increasing") & upright("heat")^(upright("x"))_(a - 1) & < upright("heat")^(upright("x"))_(a) & forall a in cal(A) \ + upright("heat_curve curvature") & upright("heat")^(upright("y"))_(a) & upright(" is a concave function of ") upright("heat")^(upright("x"))_(a) upright(" along ") a \ + upright("heat_curve breakpoints") & abs(cal(A)) & >= 2 $ diff --git a/tests/typesetting/test_declaration.py b/tests/typesetting/test_declaration.py index d1872884..409331cd 100644 --- a/tests/typesetting/test_declaration.py +++ b/tests/typesetting/test_declaration.py @@ -127,11 +127,15 @@ def test_a_body_naming_another_expression_inlines_it_on_its_own_and_names_it_in_ @pytest.mark.parametrize( ('name', 'match'), [ - pytest.param('spent', r"'spent' is not a named expression, constraint or variable.*spend", id='a-near-miss'), + pytest.param( + 'spent', + r"'spent' is not a named expression, constraint, assumption or variable.*spend", + id='a-near-miss', + ), pytest.param('objective', r"'objective' is not a named expression", id='the-objective-has-no-name'), ], ) -def test_a_name_declared_as_none_of_the_three_is_refused(name: str, match: str): +def test_a_name_declared_as_none_of_the_four_is_refused(name: str, match: str): with pytest.raises(SchemaError, match=match): typeset_declaration(PLAIN, name, 'latex') @@ -139,7 +143,7 @@ def test_a_name_declared_as_none_of_the_three_is_refused(name: str, match: str): def test_a_name_shared_by_a_constraint_and_a_variable_is_refused_rather_than_guessed(): """Constraints sit outside the flat namespace, so the model admits the pair; one line prints one of them.""" model = override(PLAIN, **{'constraints.p': {'dims': ['snapshot', 'generator'], 'expression': 'p <= 1'}}) - with pytest.raises(SchemaError, match="'p' is both a constraint and a variable"): + with pytest.raises(SchemaError, match="'p' is declared twice, as constraint and as variable"): typeset_declaration(model, 'p', 'latex') diff --git a/tests/typesetting/test_golden.py b/tests/typesetting/test_golden.py index a23e7220..5229a1c4 100644 --- a/tests/typesetting/test_golden.py +++ b/tests/typesetting/test_golden.py @@ -129,6 +129,10 @@ def _rendered_trees() -> Iterator[object]: for mask in resolved.variables.values(): if mask is not None: yield mask.root + for holds, where in resolved.assumptions.values(): + yield holds.root + if where is not None: + yield where.root yield from resolved.expressions.values() @@ -203,6 +207,7 @@ def test_the_golden_model_calls_every_operator_in_the_language(): "msg = f'{context}: expected a comparison, got {type(node).__name__}'", 'raise AssertionError(msg)', 'assert_never(node)', + 'assert_never(check)', 'if block is None:', 'return []', } @@ -228,7 +233,7 @@ def test_the_golden_model_reaches_every_line_of_the_walk(tmp_path: Path): 'to_latex(model)\n' 'to_latex(model, inline_expressions=True)\n' 'spec = to_spec(model)\n' - 'for name in (*spec.expressions, *spec.constraints, *spec.variables):\n' + 'for name in (*spec.expressions, *spec.constraints, *spec.assumptions, *spec.variables):\n' " typeset_declaration(model, name, 'latex')\n" ) subprocess.run( diff --git a/tests/typesetting/test_walk.py b/tests/typesetting/test_walk.py index 8653c5f3..ef87e10e 100644 --- a/tests/typesetting/test_walk.py +++ b/tests/typesetting/test_walk.py @@ -13,11 +13,11 @@ from math_spec.errors import LanguageError from math_spec.piecewise import expand_piecewise -from math_spec.typesetting import FORMATS, SymbolTable, to_latex, typeset +from math_spec.typesetting import FORMATS, SymbolTable, to_latex, typeset, typeset_declaration from math_spec.typesetting.format import OPERATOR_NAMES from math_spec.typesetting.symbols import Symbols, _derive_name_symbol, chosen_expressions from math_spec.validation import to_spec -from tests.fixtures import DISPATCH_MODEL, OPERATOR_PROBES, override +from tests.fixtures import DISPATCH_MODEL, EXAMPLES, OPERATOR_PROBES, override from tests.typesetting import golden from tests.typesetting.fixtures import EVERY_FORMAT, LATEX @@ -835,3 +835,36 @@ def test_a_comparison_of_expressions_prints_as_the_arithmetic_it_is(name: Format p_max = fmt.subscript(fmt.superscript(fmt.upright('p'), fmt.upright('max')), ['g']) cost = fmt.subscript(fmt.upright('cost'), ['g']) assert f'{cost} {fmt.operators["le"]} {fmt.fraction(p_max, "2")}' in text + + +@EVERY_FORMAT +def test_an_assumption_prints_under_its_own_heading(name: FormatName, fmt: Format): + """What the data is held to prints with the math, because a reader checking it reads the same document.""" + model = override(DISPATCH_MODEL, assumptions={'costs_are_positive': 'cost > 0'}) + text = typeset(model, name, legend=False) + section = text[text.index('Assumptions') :] + assert fmt.subscript(fmt.upright('cost'), ['g']) in section + assert f'{fmt.operators["gt"]} 0' in section, 'the line aligns on the relation, which leads the right side' + assert 'Assumptions' not in typeset(DISPATCH_MODEL, name, legend=False), ( + 'a model that assumes nothing of its data prints no heading for it' + ) + + +@EVERY_FORMAT +def test_a_curve_prints_what_its_method_assumes_of_the_breakpoints(name: FormatName, fmt: Format): + """The conditions a method implies are the data's too, so they print where the written ones do. + + ``convex`` is exact for a curve that bends once either way, which is no + single inequality — so that one is prose, as a paper writes it. + """ + text = typeset(EXAMPLES / 'piecewise.yaml', name, legend=False) + assert fmt.prose(' is a convex or concave function of ') in text + assert fmt.operators['lt'] in text, 'the x-axis is strictly increasing between neighbours' + + +def test_an_assumption_is_a_declaration_a_line_may_be_asked_for(): + """`typeset_declaration` prints one line for a name; an assumption is now one of the names it takes.""" + model = override(DISPATCH_MODEL, assumptions={'costs_are_positive': 'cost > 0'}) + assert typeset_declaration(model, 'costs_are_positive', 'latex') == ( + r'\mathrm{cost}_{g} > 0 \qquad \forall\, g \in \mathcal{G}' + ) diff --git a/tools/gallery.py b/tools/gallery.py index 14a4a1ec..74fba0f5 100644 --- a/tools/gallery.py +++ b/tools/gallery.py @@ -111,6 +111,7 @@ def declared_block(path: Path) -> str: equation = equations(_section(page, 'Subject to')) definition = equations(_section(page[page.index('#### Objective') :], 'Definitions')) if model.expressions else {} domains = _section(page, 'Variable domains').strip() + assumption = equations(_section(page, 'Assumptions')) if model.assumptions else {} parts = [legend, f'### Objective\n\n```yaml\n{declaration(text, "objective")}\n```\n\n{objective}'] for name, block in model.constraints.items(): parts.append( @@ -124,6 +125,10 @@ def declared_block(path: Path) -> str: for name in model.expressions ) parts.append(domains) + parts.extend( + f'### `{name}`\n\n```yaml\n{declaration(text, "assumptions", name)}\n```\n\n{assumption[name]}' + for name in model.assumptions + ) return '\n\n'.join(parts) diff --git a/tools/notation.py b/tools/notation.py index affe89ef..ef5cd382 100644 --- a/tools/notation.py +++ b/tools/notation.py @@ -57,6 +57,7 @@ 'variables': 'Variable domains', 'piecewise': 'Curves, as what they expand to', 'sos': 'Sets carried to the solver', + 'assumptions': 'What the data has to satisfy', } @@ -227,7 +228,11 @@ def _curves() -> list[str]: caption = ( f'**`method: {method}`** \N{EM DASH} {PIECEWISE_METHODS[method]}, in `{source.relative_to(ROOT)}`.' ) + derived = [math for label, math in printed.items() if label.startswith(f'{block.name} ')] + assumed = '\n\n'.join(['What the method assumes of the numbers bound to it:', *derived]) if derived else '' rows.append(row.replace('\n\n', f'\n\n{caption}\n\n{_table_shown(table)}', 1)) + if assumed: + rows.append(assumed) return rows