feat(language): a where may compare arithmetic over parameters, so an assumption can say what a formula has to satisfy

docs/reference/language/declarations.md

@@ -267,6 +267,11 @@ Three rules say what an assumption means:
 - **Two parameters may be compared.** `p_min <= p_max` reads the two coordinate
   by coordinate, the narrower one at every coordinate of the wider. Both are
   numbers, or both share a dtype. A number against a label is refused.
+- **Either side may be arithmetic.** `p_min <= 0.5 * p_max`,
+  `sum(p_max, over=generator) >= peak` and
+  `p_max <= at(bus_cap, by=bus_of)` are each one assumption, read as an
+  [expression](expressions.md#arithmetic-in-a-comparison) is: macros and named
+  expressions expand, `shift` names its `edge=`, and a variable is refused.
 
 A predicate that names a variable is refused, because an assumption is about
 the data and a variable is what the solver decides from it. State a rule about

docs/reference/language/expressions.md

@@ -157,10 +157,11 @@ A `where:` is a boolean mask, and true means "this coordinate exists".
 ```text
 where_expr ::= atom | "NOT" where_expr | where_expr ("AND"|"OR") where_expr
             |  "(" where_expr ")"
-atom       ::= NAME | NAME COMPARATOR value | POSITION COMPARATOR INTEGER
-            |  "True" | "False"
+atom       ::= NAME | NAME COMPARATOR value | expression COMPARATOR expression
+            |  POSITION COMPARATOR INTEGER | "True" | "False"
 COMPARATOR ::= "<=" | ">=" | "==" | "!=" | "<" | ">"
 value      ::= NUMBER | QUOTED | NAME_OR_STRING
+expression ::= the arithmetic grammar above, with no variable and no dual in it
 POSITION   ::= "position" "(" NAME [ "," "by" "=" NAME ] ")"
 QUOTED     ::= "'" chars "'" | '"' chars '"'
 ```
@@ -176,6 +177,7 @@ QUOTED     ::= "'" chars "'" | '"' chars '"'
 | `name OP value`                  | lookup                           | A filter on the lookup's value, so the `over` dimension has to be in the frame. A null compares false                                                                                                                                                                                               |
 | `name OP name`                   | two parameters                   | Coordinate by coordinate, the narrower one read at every coordinate of the wider. Both are numbers, or both share a dtype. A null on either side compares false                                                                                                                                     |
 | `name OP name`                   | two lookups                      | Legal only where both lookups are over the same dimension and into the same dimension. `from != to` excludes a self-loop                                                                                                                                                                            |
+| `expression OP expression`       | arithmetic over parameters       | Coordinate by coordinate, over every dimension either side carries. A macro and a named expression expand as in an expression, and every operator keeps its rule, so a `shift` names its `edge=`. A side with no value at a coordinate compares false                                               |
 | `position(name) OP i`            | dimension                        | Where the row sits along the dimension's own order. `0` is first, and a negative number counts from the end                                                                                                                                                                                         |
 | `position(name, by=lookup) OP i` | a dimension and a lookup over it | The same, counted within each group the lookup makes                                                                                                                                                                                                                                                |
 | `AND` `OR` `NOT`                 | —                                | Case-insensitive. `NOT` binds tighter than `AND`, and `AND` tighter than `OR`                                                                                                                                                                                                                       |
@@ -217,6 +219,39 @@ so do two lookups that share both ends: over one dimension they are two columns
 of one table, and into one dimension they draw from one label set. Comparing two
 dimensions is not in the language. Precompute a boolean parameter instead.
 
+### Arithmetic in a comparison
+
+Either side of a comparison may be an expression: `p_min <= 0.5 * p_max`,
+`sum(p_max, over=generator) >= peak`, `p_max <= at(bus_cap, by=bus_of)`. The
+side is read exactly as an [expression](#expressions) is, so a macro
+and a named expression expand into it and every operator keeps its own rule.
+Two things an expression may carry are refused here, because a mask is built
+before either exists: a variable, and a `dual()`.
+
+A comparison of expressions is checked over every dimension either side
+carries. A side whose value is absent at a coordinate compares false there, as
+a null does in every other comparison; under a summing operator the absent
+term is one fewer. A `shift` says what its vacated positions hold, as it does
+everywhere, so a comparison against the previous row names an `edge=` and a
+`where:` on the position keeps the first row out:
+
+```yaml
+dimensions:
+  snapshot: { dtype: int }
+parameters:
+  load: { dims: [snapshot] }
+  ramp: { dims: [] }
+assumptions:
+  load_ramps_within_limit:
+    holds: "load - shift(load, over=snapshot, offset=1, edge=0) <= ramp"
+    where: "position(snapshot) > 0"
+```
+
+A case `when:` that compares expressions cannot be proved apart from its
+neighbours before the data arrives, so it is refused there with the rewrite:
+compare one parameter against a literal or another parameter, or precompute
+the test as a boolean parameter.
+
 ### `position()`
 
 `position(dim)` is where the row sits along the dimension's own order, which is

docs/reference/language/reading.md

@@ -114,6 +114,11 @@ questions that every engine would otherwise work out for itself:
 - `.atoms` gives its leaves, with the connectives removed.
 - `.dims` gives the dimensions the mask is read at.
 
+A comparison of expressions arrives as an `ExpressionComparisonNode`, whose two
+sides are program expressions like a constraint's, and whose `dims` are every
+dimension either side carries. Its `names_read` are every parameter and lookup
+the sides read, the lookup a grouping joins through included.
+
 A predicate you build yourself answers the same four questions: wrap it in `Mask`,
 or build it there with `~`, `&` and `|`. A mask folds as it is built: a double
 negation cancels, and a `True` or `False` is absorbed rather than buried in the

docs/reference/notation.md

@@ -127,6 +127,7 @@ parameters:
 
 | Symbol | Meaning |
 |---|---|
+| $`\mathrm{spend}^{\mathrm{cap}}`$ | `spend_cap` over $`\mathcal{G}`$ |
 | $`\mathit{spend}`$ | `spend` over $`\mathcal{T}`$ — what a snapshot's dispatch costs |
 | $`\mathit{lcoe}`$ | `lcoe` (scalar) |
 | $`\mathit{marginal\_price}`$ | `marginal_price` over $`\mathcal{T} \times \mathcal{B}`$ |
@@ -595,8 +596,35 @@ never:
 \mathit{slack}_{t} \ge 0 \qquad \forall\, t \in \mathcal{T} \,:\, \bot
 ```
 
+#### `margin`
+
+a mask comparing two expressions, which prints as the arithmetic it is
+
+```yaml
+margin:
+  dims: [snapshot, generator]
+  where: "p_max - p_min > cost / 2"
+  expression: p <= p_max
+```
+
+```math
+p_{t,g} \le \mathrm{p}^{\mathrm{max}}_{g} \qquad \forall\, t \in \mathcal{T},\ g \in \mathcal{G} \,:\, \mathrm{p}^{\mathrm{max}}_{g} - \mathrm{p}^{\mathrm{min}}_{g} > \frac{\mathrm{cost}_{g}}{2}
+```
+
 ### Definitions
 
+#### `spend_cap`
+
+a data-only entry, so a where or an assumption may compare it
+
+```yaml
+spend_cap: cost * 2
+```
+
+```math
+\mathrm{spend}^{\mathrm{cap}}_{g} = \mathrm{cost}_{g} \cdot 2 \qquad \forall\, g \in \mathcal{G}
+```
+
 #### `spend`
 
 a plain named expression: its symbol prints where it is used, its body once as a definition
@@ -875,6 +903,56 @@ flexible_units_are_cheap: "NOT is_flexible OR cost <= budget"
 \neg \mathrm{is\_flexible}_{g} \vee \mathrm{cost}_{g} \le \mathrm{budget} \qquad \forall\, g \in \mathcal{G}
 ```
 
+#### `floor_is_half_the_capacity`
+
+arithmetic on a side, which reads as an expression does
+
+```yaml
+floor_is_half_the_capacity: "p_min <= 0.5 * p_max"
+```
+
+```math
+\mathrm{p}^{\mathrm{min}}_{g} \le 0.5 \cdot \mathrm{p}^{\mathrm{max}}_{g} \qquad \forall\, g \in \mathcal{G}
+```
+
+#### `load_ramps_within_the_zone_cap`
+
+a translation under a comparison names its edge, and the where keeps the vacated row out
+
+```yaml
+load_ramps_within_the_zone_cap:
+  holds: "load - shift(load, over=snapshot, offset=1, edge=0) <= at(zone_cap, by=zone_of)"
+  where: "position(snapshot) > 0"
+```
+
+```math
+\mathrm{load}_{t,b} - \mathrm{load}_{t \boxminus_{0} 1,b} \le \mathrm{zone\_cap}_{\mathrm{zone\_of}(b)} \qquad \forall\, t \in \mathcal{T},\ b \in \mathcal{B} \,:\, \mathrm{pos}(t) > 0
+```
+
+#### `fleet_covers_the_budget`
+
+a reduction on a side, so the frame is what is left
+
+```yaml
+fleet_covers_the_budget: "sum(p_max, over=generator) >= budget"
+```
+
+```math
+\sum_{g \in \mathcal{G}} \mathrm{p}^{\mathrm{max}}_{g} \ge \mathrm{budget}
+```
+
+#### `cheap_when_spent`
+
+an expressions: entry on a side, read by the name the file gave it
+
+```yaml
+cheap_when_spent: "spend_cap > 0 OR NOT is_flexible"
+```
+
+```math
+\mathrm{spend}^{\mathrm{cap}}_{g} > 0 \vee \neg \mathrm{is\_flexible}_{g} \qquad \forall\, g \in \mathcal{G}
+```
+
 ### 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.

src/math_spec/_expression_parser.py

@@ -349,8 +349,12 @@ def with_children(node: ArithmeticNode, recurse: Callable[[ArithmeticNode], Arit
 # ---------------------------------------------------------------------------
 
 
-def _build_grammar() -> pp.ParserElement:
-    """``inf`` is a ``pp.Keyword`` rather than a ``pp.Literal``, which would match the prefix of ``inflow``."""
+def _build_grammar() -> tuple[pp.ParserElement, pp.ParserElement]:
+    """The arithmetic grammar, and the expression grammar that puts one comparison over it.
+
+    ``inf`` is a ``pp.Keyword`` rather than a ``pp.Literal``, which would
+    match the prefix of ``inflow``.
+    """
     arith = pp.Forward()
 
     inf_literal = (pp.Keyword('.inf') | pp.Keyword('inf')).set_parse_action(lambda: NumberNode(float('inf')))
@@ -386,9 +390,10 @@ def _build_grammar() -> pp.ParserElement:
     arith <<= add_sub
 
     comparator = pp.one_of(list(get_args(ComparisonOperator)))
-    return (arith + pp.Optional(comparator + arith)).set_parse_action(
+    expression = (arith + pp.Optional(comparator + arith)).set_parse_action(
         lambda t: ComparisonNode(t[1], t[0], t[2]) if len(t) == 3 else t[0]
     )
+    return arith, expression
 
 
 def _make_func_call(tokens: pp.ParseResults) -> FunctionCallNode:
@@ -421,7 +426,9 @@ def _make_power(tokens: pp.ParseResults) -> Any:
     return items[0] if len(items) == 1 else BinaryOperatorNode('**', items[0], items[2])
 
 
-_GRAMMAR = _build_grammar()
+#: The arithmetic half on its own, for the where grammar to put a predicate's
+#: comparator over — one grammar for what a side may say, wherever it stands.
+ARITHMETIC, _GRAMMAR = _build_grammar()
 
 
 #: How deep a tree the language admits. Every pass over an expression recurses,

src/math_spec/_where_parser.py

@@ -15,12 +15,23 @@
 
 import pyparsing as pp
 
-from math_spec._expression_parser import NAME, REAL, parse_text
+from math_spec._expression_parser import (
+    ARITHMETIC,
+    NAME,
+    REAL,
+    FunctionCallNode,
+    NameNode,
+    NumberNode,
+    UnaryOperatorNode,
+    children,
+    parse_text,
+)
 from math_spec.program import AndNode, BooleanLiteralNode, NotNode, OrNode, PredicateOperator, where_children
 
 if TYPE_CHECKING:
     from collections.abc import Callable
 
+    from math_spec._expression_parser import ArithmeticNode
     from math_spec.program import WhereNode
 
 # ---------------------------------------------------------------------------
@@ -49,6 +60,19 @@ class UnresolvedComparisonNode:
     quoted: bool = False
 
 
+@dataclass(frozen=True)
+class UnresolvedExpressionComparisonNode:
+    """``expression <op> expression``, both sides still the bare parse — ``resolution.py`` types and judges them.
+
+    The grammar reaches for this only where a side is more than one name or
+    literal, so the simpler forms keep their own nodes and their own rules.
+    """
+
+    left: ArithmeticNode
+    op: PredicateOperator
+    right: ArithmeticNode
+
+
 @dataclass(frozen=True)
 class UnresolvedPositionNode:
     """``position(dim[, by=lookup]) <op> i`` before the names are checked; ``resolution.py`` types it."""
@@ -61,7 +85,9 @@ class UnresolvedPositionNode:
 
 #: What resolution rewrites away on the where side — the three nodes whose
 #: left-hand side is still a name the schema has not been asked about.
-UnresolvedWhereNode = UnresolvedNameNode | UnresolvedComparisonNode | UnresolvedPositionNode
+UnresolvedWhereNode = (
+    UnresolvedNameNode | UnresolvedComparisonNode | UnresolvedExpressionComparisonNode | UnresolvedPositionNode
+)
 
 
 # ---------------------------------------------------------------------------
@@ -82,6 +108,31 @@ def _position_comparison(tokens: pp.ParseResults) -> UnresolvedPositionNode:
     return UnresolvedPositionNode(str(dimension), op, at, None if by is None else str(by))
 
 
+def _is_plain(node: ArithmeticNode) -> bool:
+    """Whether *node* is one name or one signed number — a side the simpler comparison forms own."""
+    if isinstance(node, UnaryOperatorNode):
+        return isinstance(node.operand, NumberNode)
+    return isinstance(node, NameNode | NumberNode)
+
+
+def _reads_arithmetic(tokens: pp.ParseResults) -> bool:
+    """Whether a comparison needs the expression form at all.
+
+    Two plain sides are ``name <op> literal`` or ``name <op> name``, and a
+    ``position(...)`` call against a plain side is the position form; each of
+    those has a node of its own, so this form stands aside for them.
+    """
+    left, _, right = tokens
+    if _is_plain(left) and _is_plain(right):
+        return False
+    return not (isinstance(left, FunctionCallNode) and left.name == 'position' and _is_plain(right))
+
+
+def _expression_comparison(tokens: pp.ParseResults) -> UnresolvedExpressionComparisonNode:
+    left, op, right = tokens
+    return UnresolvedExpressionComparisonNode(left, op, right)
+
+
 def _comparison(tokens: pp.ParseResults) -> UnresolvedComparisonNode:
     """``name <op> literal`` off the tokens the grammar captured, the quoted marker turned into a flag."""
     name, op, value = tokens
@@ -93,8 +144,11 @@ def _build_where_grammar() -> pp.ParserElement:
     """Build the pyparsing grammar for where strings.
 
     Both quote characters are accepted because YAML already owns one of them.
-    ``NOT`` binds tightest, then ``AND``, then ``OR``. ``position(...)`` leads
-    the alternation, since ``position`` would otherwise be read as a bare name.
+    ``NOT`` binds tightest, then ``AND``, then ``OR``. The three comparison
+    forms are matched longest-first, so ``p > 2 * q`` is not cut short at
+    ``p > 2``; the expression form stands aside for the two plain shapes
+    (:func:`_reads_arithmetic`), so ``p > 0`` keeps the node its dtype rule
+    is written for.
     """
     where_expr = pp.Forward()
 
@@ -121,14 +175,16 @@ def _build_where_grammar() -> pp.ParserElement:
     position_comparison = (position_call + comparator + position).set_parse_action(_position_comparison)
 
     comparison = (name + comparator + (number | quoted | name)).set_parse_action(_comparison)
+    expression_comparison = (
+        (ARITHMETIC + comparator + ARITHMETIC).add_condition(_reads_arithmetic).add_parse_action(_expression_comparison)
+    )
     # pyrefly: ignore[implicit-any-lambda]
     existence = name.copy().set_parse_action(lambda t: UnresolvedNameNode(t[0]))
 
     atom = (
         true_lit
         | false_lit
-        | position_comparison
-        | comparison
+        | (position_comparison ^ comparison ^ expression_comparison)
         | existence
         | (pp.Suppress('(') + where_expr + pp.Suppress(')'))
     )
@@ -192,6 +248,17 @@ def _named_rewrite(text: str, loc: int) -> str | None:
 )
 
 
+def _nested(node: Any) -> tuple[Any, ...]:
+    """What a where string nests through: a connective's operands, and the arithmetic under a comparison of expressions."""
+    if isinstance(node, UnresolvedExpressionComparisonNode):
+        return (node.left, node.right)
+    if isinstance(node, UnresolvedWhereNode):
+        return ()
+    if isinstance(node, AndNode | OrNode | NotNode | BooleanLiteralNode):
+        return where_children(node)
+    return children(node)
+
+
 @lru_cache(maxsize=4096)
 def parse_where(text: str) -> WhereNode | UnresolvedWhereNode:
     """Parse a where string into an AST, its leaves still unresolved.
@@ -208,5 +275,5 @@ def parse_where(text: str) -> WhereNode | UnresolvedWhereNode:
     """
     return cast(
         'WhereNode | UnresolvedWhereNode',
-        parse_text(_WHERE_GRAMMAR, text, 'where string', _named_rewrite, where_children, _DEEP_REWRITE),
+        parse_text(_WHERE_GRAMMAR, text, 'where string', _named_rewrite, _nested, _DEEP_REWRITE),
     )