From 97da44b7115664cae51e0d7bf2247b31e4cd4763 Mon Sep 17 00:00:00 2001 From: Felix Bumann Date: Sun, 20 Sep 2026 14:34:48 +0000 Subject: [PATCH 1/2] refactor(program): a direction carries what a consumer reads, not the check the loader makes `Direction.is_single_valued` is a module-private function in resolution.py. It is the discriminator between `at` and `sum(by=)`, it has two callers in one function, and no consumer asks it: a program's node type already says which operator a call became. The refusal table in docs/about/what-counts-as-public-api.md refuses a function whose answer a declaration could give. The `Predicate` union said it was what a lowered mask's root is built of. That is false. It also holds `ArithmeticComparison`, which lowering rewrites into an `ExpressionComparison`, so a consumer walking a program meets every other member and never that one. The comment and the reading page now say so. docs/reference/reading.md: n 52, avg 14.9, median 13, over25 7. The long sentences all predate this change; the two added are 11 and 9 words. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01MKUDdoyCtxHXm5Gcuze24W --- docs/reference/reading.md | 4 +++- src/math_spec/program.py | 13 +++++-------- src/math_spec/resolution.py | 13 +++++++++++-- 3 files changed, 19 insertions(+), 11 deletions(-) diff --git a/docs/reference/reading.md b/docs/reference/reading.md index bf580cba..236a4ea1 100644 --- a/docs/reference/reading.md +++ b/docs/reference/reading.md @@ -87,7 +87,9 @@ node's operands, and `where_children()` walks a predicate's. `walk()` yields every node under an expression, parents first. `walk_regions()` yields each node with the `cases:` regions it stands inside, outermost first. -Every `where` arrives as a `Mask`. Its `.root` is the resolved predicate. The +Every `where` arrives as a `Mask`. Its `.root` is the resolved predicate. One +member of the `Predicate` union never reaches you. Lowering rewrites every +`ArithmeticComparison` into an `ExpressionComparison`. The mask also answers four questions: - `.conjuncts` flattens the `AND` spine, and stops at an `OR` or a `NOT`. diff --git a/src/math_spec/program.py b/src/math_spec/program.py index ee27dc63..ea15cac5 100644 --- a/src/math_spec/program.py +++ b/src/math_spec/program.py @@ -266,7 +266,7 @@ class Pullback: The dims ``direction`` consumes go and the dims it produces arrive, one value per coordinate because the read takes value columns at a key the - result fixes (``Direction.is_single_valued``). The join fans out, many + result fixes, which the loader checks. The join fans out, many produced tuples sharing one consumed tuple — at each coordinate of the joined columns, which the operand carries and the result keeps. """ @@ -499,11 +499,6 @@ def produced_dims(self) -> tuple[str, ...]: def joined_dims(self) -> tuple[str, ...]: return tuple(self.dim(role) for role in self.joined) - @property - def is_single_valued(self) -> bool: - """Whether the read is one value per coordinate: the key lies inside what is fixed.""" - return set(self.relation.key) <= {*self.joined, *self.produced} - @dataclass(frozen=True) class Partition: @@ -1268,8 +1263,10 @@ class Or: right: Predicate -#: Every resolved predicate node — what a lowered mask's ``root`` is built of. -#: The parser's ``Unresolved*`` nodes are not members: they live with the +#: Every resolved predicate node. A lowered mask's ``root`` holds every member +#: but :class:`ArithmeticComparison`, which lowering rewrites into an +#: :class:`ExpressionComparison`, so a consumer walking a program never meets +#: one. The parser's ``Unresolved*`` nodes are not members: they live with the #: grammar in :mod:`math_spec._where_parser`, and resolution rewrites them away #: before anything here is asked. Predicate = ( diff --git a/src/math_spec/resolution.py b/src/math_spec/resolution.py index 6e0826f7..b04e9c6a 100644 --- a/src/math_spec/resolution.py +++ b/src/math_spec/resolution.py @@ -251,6 +251,15 @@ def names_in(value: ArithmeticNode) -> tuple[str, ...]: return value.names if isinstance(value, NameListNode) else () +def _is_single_valued(direction: Direction) -> bool: + """Whether the read gives one value per coordinate: the relation's key lies inside what the call fixes. + + The discriminator between ``at`` and ``sum(by=)``, and the only stage that + asks: a program's node type says which one a call became. + """ + return set(direction.relation.key) <= {*direction.joined, *direction.produced} + + def mask_of(node: Predicate | None) -> Mask | None: """The mask a declaration carries for a resolved where: ``None`` where there is none, or where every row passes.""" if node is None or (isinstance(node, BooleanLiteral) and node.value): @@ -627,14 +636,14 @@ def _direction( return None joined = tuple(r for r in shape.key if r not in from_roles and r not in into_roles) direction = Direction(name, shape, from_roles, into_roles, joined) - if not forward and not direction.is_single_valued: + if not forward and not _is_single_valued(direction): self.errors.append( f"{context}: {call}: at reads one value per coordinate, and '{name}' is not single-valued in " f'{list(from_roles)} at the columns the call lands on ({[*into_roles, *joined]}) — its key is ' f'{list(shape.key)}. Key the table by the columns the call lands on, or read the other way.' ) return None - if forward and direction.is_single_valued: + if forward and _is_single_valued(direction): self.errors.append( f'{context}: {call}: this sum lands on the key {list(shape.key)}, so each coordinate has one ' f"term and nothing is added up — that is a read, which is at()'s. Write " From 8c02f9f63d63fe050d19b1a158427b2fc2cc1102 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 20 Sep 2026 20:41:29 +0000 Subject: [PATCH 2/2] chore(resolution): the single-valued test is a local of the one call that asks it Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01JJfEUsCDtwXuXV8CANCHuR --- src/math_spec/resolution.py | 14 +++----------- 1 file changed, 3 insertions(+), 11 deletions(-) diff --git a/src/math_spec/resolution.py b/src/math_spec/resolution.py index b04e9c6a..c8e10bae 100644 --- a/src/math_spec/resolution.py +++ b/src/math_spec/resolution.py @@ -251,15 +251,6 @@ def names_in(value: ArithmeticNode) -> tuple[str, ...]: return value.names if isinstance(value, NameListNode) else () -def _is_single_valued(direction: Direction) -> bool: - """Whether the read gives one value per coordinate: the relation's key lies inside what the call fixes. - - The discriminator between ``at`` and ``sum(by=)``, and the only stage that - asks: a program's node type says which one a call became. - """ - return set(direction.relation.key) <= {*direction.joined, *direction.produced} - - def mask_of(node: Predicate | None) -> Mask | None: """The mask a declaration carries for a resolved where: ``None`` where there is none, or where every row passes.""" if node is None or (isinstance(node, BooleanLiteral) and node.value): @@ -635,15 +626,16 @@ def _direction( ) return None joined = tuple(r for r in shape.key if r not in from_roles and r not in into_roles) + single_valued = set(shape.key) <= {*into_roles, *joined} direction = Direction(name, shape, from_roles, into_roles, joined) - if not forward and not _is_single_valued(direction): + if not forward and not single_valued: self.errors.append( f"{context}: {call}: at reads one value per coordinate, and '{name}' is not single-valued in " f'{list(from_roles)} at the columns the call lands on ({[*into_roles, *joined]}) — its key is ' f'{list(shape.key)}. Key the table by the columns the call lands on, or read the other way.' ) return None - if forward and _is_single_valued(direction): + if forward and single_valued: self.errors.append( f'{context}: {call}: this sum lands on the key {list(shape.key)}, so each coordinate has one ' f"term and nothing is added up — that is a read, which is at()'s. Write "