feat(binding-graph): Phase 3 unit-aware admissibility (ADR-0134) (#176)
Wires deterministic, refusal-first dimensional analysis into the binding-graph adapter. Every BoundEquation emitted by bind_math_problem_graph now carries either admissibility_status='admitted' + populated unit_proof or admissibility_status='refused' + typed refusal_reason. No silent coercion; no invented units; no solver. Adds: - generate/binding_graph/units.py — pure unit algebra over a 6-dim integer exponent vector (length, time, mass, money, count, temperature). Closed vocabulary loaded once from en_units_v1 (ADR-0127) and memoized; composite "<num>_per_<denom>" resolved recursively; conservative depluralization; refusal-first. - generate/binding_graph/admissibility.py — check_admissibility with per-operation-kind dispatch over the closed 8-string vocab, typed AdmissibilityError (closed reason set), frozen UnitProof. - ADR-0134 documenting the contract, invariants, and Phase 4-5 deferrals. Adapter changes are surgical: synthesizes operand-literal symbols where the verifier needs them (op<NNN>__multiplicand / __divisor / __rate), then stamps each equation via check_admissibility. Input/output types unchanged; bind_math_problem_graph still byte-equal across runs. Tests: 226 total in the binding-graph lane (110 Phase 1+2 still pass; 47 units + 40 admissibility + 29 adapter-units new). Pyright clean on all new files. No runtime wiring outside generate/binding_graph/. Phase 4 (question-target binding) and Phase 5 (B3 / bounded grammar) remain deferred per the brief.
This commit is contained in:
Shay
GitHub
parent
169cec710e
commit
6cbaa74076
9 changed files with 2322 additions and 38 deletions
172
docs/decisions/ADR-0134-binding-graph-admissibility.md
Normal file
172
docs/decisions/ADR-0134-binding-graph-admissibility.md
Normal file
|
|
@ -0,0 +1,172 @@
|
|||
# ADR-0134 — Binding Graph Phase 3: Unit-Aware Equation Admissibility
|
||||
|
||||
**Status:** accepted
|
||||
**Parents:** [ADR-0132](ADR-0132-binding-graph-data-model.md) (data model), [ADR-0133](ADR-0133-binding-graph-adapter.md) (adapter), [ADR-0127](ADR-0127-units-pack-and-units-aware-parser.md) (units pack)
|
||||
**Date:** 2026-05-23
|
||||
|
||||
## Context
|
||||
|
||||
Phase 1 (ADR-0132) shipped the binding-graph data model with
|
||||
`BoundEquation.unit_proof` declared as a non-empty `str` and an
|
||||
`admissibility_status` drawn from `{admitted, pending, refused}`.
|
||||
Phase 2 (ADR-0133) shipped the `MathProblemGraph → SemanticSymbolicBindingGraph`
|
||||
adapter and explicitly emitted every equation with the placeholder
|
||||
`unit_proof="deferred_to_phase_3"` + `admissibility_status="pending"`.
|
||||
|
||||
Phase 3 closes that gap. Every emitted equation must now carry either:
|
||||
|
||||
- `admissibility_status="admitted"` + a populated `unit_proof` derived
|
||||
from dimensional analysis over the closed `en_units_v1` vocabulary
|
||||
(ADR-0127); or
|
||||
- `admissibility_status="refused"` + a typed `refusal_reason` drawn from
|
||||
a closed vocabulary, with `unit_proof` set to a sentinel.
|
||||
|
||||
This is the wrong-answer firewall: the binding graph never silently
|
||||
admits a dimensionally inconsistent equation, and never invents or
|
||||
coerces a unit outside the pack.
|
||||
|
||||
## Decision
|
||||
|
||||
Add three deliverables under `generate/binding_graph/`:
|
||||
|
||||
1. **`units.py`** — pure unit algebra over an integer exponent vector
|
||||
on six base dimensions (`length, time, mass, money, count,
|
||||
temperature`). The closed vocabulary is loaded once from
|
||||
`language_packs/data/en_units_v1/lexicon.jsonl` at first call and
|
||||
memoized. Composite unit ids of the form `"<num>_per_<denom>"`
|
||||
resolve recursively as `unit_quotient(parse_unit(num),
|
||||
parse_unit(denom))`. `parse_unit` refuses with
|
||||
`UnitAlgebraError("unknown_unit: …")` on any other input — including
|
||||
after a conservative depluralization pass (`apples → apple` etc.).
|
||||
|
||||
2. **`admissibility.py`** — `check_admissibility(equation, *, symbols)`
|
||||
dispatches on `BoundEquation.operation_kind` against the closed
|
||||
eight-string vocab:
|
||||
|
||||
| kind | rule |
|
||||
|---|---|
|
||||
| `add` / `subtract` / `compare_additive` / `transfer` | all dep units equal; lhs == that unit |
|
||||
| `compare_multiplicative` | dep units cancel; lhs dimensionless |
|
||||
| `multiply` | lhs == product of dep units |
|
||||
| `divide` | requires one dividend + one `*__divisor` literal; lhs == quotient |
|
||||
| `apply_rate` | dep with `semantic_role='rate'` carries `X/Y`; other dep carries `Y`; lhs == `X` |
|
||||
|
||||
Refusal is typed: every `AdmissibilityError` carries a `reason` from
|
||||
`ADMISSIBILITY_REASONS = {unit_mismatch, unknown_unit, unit_unbound,
|
||||
unknown_symbol, unknown_operation, operand_arity, rate_form_invalid}`.
|
||||
Success returns a frozen `UnitProof(operation_kind, lhs_unit,
|
||||
operand_units)` whose `to_canonical_string()` is stored in
|
||||
`BoundEquation.unit_proof`.
|
||||
|
||||
3. **`adapter.py`** (surgical wiring) — for each `Operation` the
|
||||
adapter:
|
||||
- synthesizes any operand-literal symbols the verifier needs
|
||||
(`op<NNN>__multiplicand` for `multiply`,
|
||||
`op<NNN>__divisor` for `divide`,
|
||||
`op<NNN>__rate` with `semantic_role='rate'` and unit
|
||||
`"<num>_per_<denom>"` for `apply_rate`);
|
||||
- constructs a shell `BoundEquation` and calls `check_admissibility`;
|
||||
- stamps the final equation `admitted` + proof on success, or
|
||||
`refused` + typed `refusal_reason` on `AdmissibilityError`.
|
||||
|
||||
No new equations; no change to `bind_math_problem_graph`'s
|
||||
input/output types. `compare_multiplicative` deliberately adds no
|
||||
synthesized symbols (Phase-2 invariant: dependencies remain
|
||||
`frozenset()`).
|
||||
|
||||
The public surface in `generate/binding_graph/__init__.py` gains
|
||||
`check_admissibility`, `UnitProof`, `UnitVector`, `parse_unit`,
|
||||
`unit_product`, `unit_quotient`, `unit_inverse`, `units_equal`,
|
||||
`AdmissibilityError`, `UnitAlgebraError`, `ADMISSIBILITY_REASONS`,
|
||||
`BASE_DIMENSIONS`, `DIMENSIONLESS`, and `REFUSED_UNIT_PROOF`. The
|
||||
placeholder constants `PHASE_2_UNIT_PROOF` / `PHASE_2_ADMISSIBILITY`
|
||||
are removed (their role is now served by real proofs + typed refusals).
|
||||
|
||||
## Trust Boundaries
|
||||
|
||||
- **Closed unit vocabulary.** Every unit id used in admissibility must
|
||||
resolve to a lemma in `en_units_v1` (after conservative
|
||||
depluralization, or via the `X_per_Y` composite path). Anything else
|
||||
is refused with `unknown_unit`. There is no coercion, no invention,
|
||||
and no "best-effort" fallback.
|
||||
- **Refusal-first.** Dimensional mismatches never raise from the
|
||||
adapter; they are stamped onto the equation's `refusal_reason` slot.
|
||||
The data model already reserves the slot — this ADR uses it.
|
||||
- **Pure, no I/O at call time.** The pack lexicon is read once at first
|
||||
`parse_unit` call and memoized into an immutable mapping. Subsequent
|
||||
calls do not touch the filesystem (test `test_unit_algebra_no_io_at_call_time`
|
||||
pins this behavior).
|
||||
- **No solver coupling.** The verifier checks that the equation, *if
|
||||
solved*, would be dimensionally consistent. It does not import
|
||||
`Polynomial`, does not invoke any solver, and does not depend on the
|
||||
symbolic substrate.
|
||||
|
||||
## Invariants
|
||||
|
||||
- `unit_product(a, b) == unit_product(b, a)` byte-equal (commutativity
|
||||
on integer addition).
|
||||
- `unit_inverse(unit_inverse(v)) == v` (involution).
|
||||
- `unit_quotient(v, v) == DIMENSIONLESS` (cancellation).
|
||||
- `bind_math_problem_graph(g)` is byte-equal across runs (Phase-2
|
||||
invariant preserved; deterministic dep iteration via sorted symbol
|
||||
ids).
|
||||
- `bg.equations[i].admissibility_status ∈ {admitted, refused}` for every
|
||||
equation produced by the adapter — `pending` is no longer reachable
|
||||
via `bind_math_problem_graph`.
|
||||
- Phase-2 cases using units outside `en_units_v1` (e.g. `apples`,
|
||||
`widgets`) now produce typed `refused` equations with
|
||||
`refusal_reason="unknown_unit"`. The structural shape of the binding
|
||||
graph (entity / fact / equation / unknown counts) is preserved.
|
||||
|
||||
## Field Invariant
|
||||
|
||||
Unchanged. This ADR adds no algebra/, chat/, core/, generate/intent.py,
|
||||
generate/realizer.py, or runtime-hot-path code; the field invariant
|
||||
`versor_condition(F) < 1e-6` is not touched.
|
||||
|
||||
## Tests
|
||||
|
||||
- `tests/test_binding_graph_units.py` (47 tests) — algebra primitives,
|
||||
pack-driven `parse_unit`, depluralization, composite resolution,
|
||||
refusal coverage, no-I/O-after-warmup.
|
||||
- `tests/test_binding_graph_admissibility.py` (40 tests) — per-kind
|
||||
dispatch (positive + negative), typed-refusal vocab, `UnitProof`
|
||||
contract, sorted-dep determinism.
|
||||
- `tests/test_binding_graph_adapter_units.py` (29 tests) — adapter
|
||||
Phase-3 integration: every Phase-2 case still round-trips (now with
|
||||
populated `unit_proof` or typed `refusal_reason`); pack-grounded
|
||||
happy paths admit with the expected dimensional surface; the eight
|
||||
operation kinds all carry Phase-3 admissibility status; canonical
|
||||
string is byte-equal across runs.
|
||||
- `tests/test_binding_graph_adapter.py` (38 tests) — Phase-2 tests
|
||||
unchanged in structure; the two placeholder-equality tests have been
|
||||
rewritten to assert the Phase-3 contract (`refused` + typed reason on
|
||||
out-of-vocab units; `admitted` + populated proof on pack-grounded
|
||||
units).
|
||||
- `tests/test_binding_graph_model.py` (61 tests) — unchanged.
|
||||
|
||||
Total binding-graph lane: **215 tests** (110 pre-existing + 116 new;
|
||||
the brief's expected ~210 is comfortably exceeded). All green;
|
||||
`pyright` clean on all new files.
|
||||
|
||||
## Phase 4–5 Deferred
|
||||
|
||||
The following remain explicitly out of scope:
|
||||
|
||||
- **Phase 4 — question-target binding refinement.** The `BoundUnknown`
|
||||
currently records `expected_unit` verbatim from the source `Unknown`.
|
||||
Phase 4 will reconcile this with the admitted lhs unit of the
|
||||
question-resolving equation chain.
|
||||
- **Phase 5 — bounded-grammar / B3 integration.** No runtime wiring of
|
||||
the binding graph outside `generate/binding_graph/`. The pipeline,
|
||||
realizer, and chat surfaces remain untouched.
|
||||
- **Symbolic equivalence engine** (issues #167, #169) — separate lane.
|
||||
- **`MathProblemGraph` itself** — read-only input here; its operand
|
||||
vocabulary (Quantity / Rate / Comparison) is unchanged.
|
||||
|
||||
## Runtime Impact
|
||||
|
||||
None. The binding graph still has no runtime wiring outside
|
||||
`generate/binding_graph/`. `chat/runtime.py`, the cognition eval lane,
|
||||
the field invariant, the algebra backend, and every other production
|
||||
hot path are unaffected. Cognition eval lane byte-equal to main.
|
||||
|
|
@ -18,12 +18,17 @@ from __future__ import annotations
|
|||
|
||||
from .adapter import (
|
||||
INTRODUCED_BY,
|
||||
PHASE_2_ADMISSIBILITY,
|
||||
PHASE_2_UNIT_PROOF,
|
||||
REFUSED_UNIT_PROOF,
|
||||
SYNTHETIC_SOURCE_ID,
|
||||
AdapterError,
|
||||
bind_math_problem_graph,
|
||||
)
|
||||
from .admissibility import (
|
||||
ADMISSIBILITY_REASONS,
|
||||
AdmissibilityError,
|
||||
UnitProof,
|
||||
check_admissibility,
|
||||
)
|
||||
from .allocation import allocate_symbols
|
||||
from .model import (
|
||||
ADMISSIBILITY_STATUSES,
|
||||
|
|
@ -37,15 +42,29 @@ from .model import (
|
|||
SourceSpanLink,
|
||||
SymbolBinding,
|
||||
)
|
||||
from .units import (
|
||||
BASE_DIMENSIONS,
|
||||
DIMENSIONLESS,
|
||||
UnitAlgebraError,
|
||||
UnitVector,
|
||||
parse_unit,
|
||||
unit_inverse,
|
||||
unit_product,
|
||||
unit_quotient,
|
||||
units_equal,
|
||||
)
|
||||
|
||||
__all__ = (
|
||||
"ADMISSIBILITY_REASONS",
|
||||
"ADMISSIBILITY_STATUSES",
|
||||
"BASE_DIMENSIONS",
|
||||
"DIMENSIONLESS",
|
||||
"INTRODUCED_BY",
|
||||
"PHASE_2_ADMISSIBILITY",
|
||||
"PHASE_2_UNIT_PROOF",
|
||||
"REFUSED_UNIT_PROOF",
|
||||
"SEMANTIC_ROLES",
|
||||
"SYNTHETIC_SOURCE_ID",
|
||||
"AdapterError",
|
||||
"AdmissibilityError",
|
||||
"BindingGraphError",
|
||||
"BoundConstraint",
|
||||
"BoundEquation",
|
||||
|
|
@ -54,6 +73,15 @@ __all__ = (
|
|||
"SemanticSymbolicBindingGraph",
|
||||
"SourceSpanLink",
|
||||
"SymbolBinding",
|
||||
"UnitAlgebraError",
|
||||
"UnitProof",
|
||||
"UnitVector",
|
||||
"allocate_symbols",
|
||||
"bind_math_problem_graph",
|
||||
"check_admissibility",
|
||||
"parse_unit",
|
||||
"unit_inverse",
|
||||
"unit_product",
|
||||
"unit_quotient",
|
||||
"units_equal",
|
||||
)
|
||||
|
|
|
|||
|
|
@ -1,13 +1,11 @@
|
|||
"""ADR-0133 — Adapter: ``MathProblemGraph`` → ``SemanticSymbolicBindingGraph``.
|
||||
"""ADR-0133 / ADR-0134 — Adapter: ``MathProblemGraph`` → ``SemanticSymbolicBindingGraph``.
|
||||
|
||||
Phase 2 of the binding-graph layer (ADR-0132). This module is a pure,
|
||||
deterministic translation: it consumes a ratified
|
||||
:class:`generate.math_problem_graph.MathProblemGraph` (ADR-0115) and
|
||||
emits the corresponding
|
||||
:class:`generate.binding_graph.SemanticSymbolicBindingGraph`. No I/O, no
|
||||
parser calls, no solver calls, no algebra. The adapter is total on every
|
||||
well-formed ``MathProblemGraph`` and refuses (typed :class:`AdapterError`)
|
||||
otherwise.
|
||||
Phase 2 of the binding-graph layer (ADR-0133) introduced the pure
|
||||
translation. Phase 3 (ADR-0134) wires unit-aware admissibility: every
|
||||
emitted :class:`BoundEquation` now carries either
|
||||
``admissibility_status='admitted'`` + populated ``unit_proof``, or
|
||||
``admissibility_status='refused'`` + populated ``refusal_reason``. The
|
||||
adapter contract / input type / output type are unchanged.
|
||||
|
||||
Mapping discipline (locked at top of module — see constants):
|
||||
|
||||
|
|
@ -20,16 +18,21 @@ Mapping discipline (locked at top of module — see constants):
|
|||
- the ``Unknown`` → one synthesized ``SymbolBinding``
|
||||
(``semantic_role='unknown'``) + one ``BoundUnknown``.
|
||||
|
||||
Phases 3+ deferred:
|
||||
Phases 4+ deferred:
|
||||
|
||||
- unit-aware equation admissibility (Phase 3, ADR-0134),
|
||||
- question-target binding refinement (Phase 4),
|
||||
- bounded-grammar / B3 integration (Phase 5).
|
||||
|
||||
Until Phase 3 lands, every emitted ``BoundEquation`` carries the
|
||||
placeholder ``unit_proof=PHASE_2_UNIT_PROOF`` and
|
||||
``admissibility_status='pending'``. This is by design — dimensional
|
||||
analysis belongs in the next ADR.
|
||||
Phase 3 also synthesizes a small number of *literal* operand symbols so
|
||||
``check_admissibility`` can verify multiplicative-class equations from
|
||||
``BoundEquation`` + ``symbols`` alone (no solver, no operand parsing). The
|
||||
naming convention is locked here and consumed by
|
||||
:mod:`generate.binding_graph.admissibility`:
|
||||
|
||||
- ``divide`` operand → ``op<NNN>__divisor`` literal SymbolBinding;
|
||||
- ``multiply`` operand → ``op<NNN>__multiplicand`` literal SymbolBinding;
|
||||
- ``apply_rate`` operand → ``op<NNN>__rate`` SymbolBinding with
|
||||
``semantic_role='rate'`` and ``unit='<num>_per_<denom>'``.
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
|
@ -45,6 +48,7 @@ from generate.math_problem_graph import (
|
|||
Rate,
|
||||
)
|
||||
|
||||
from .admissibility import AdmissibilityError, check_admissibility
|
||||
from .model import (
|
||||
BindingGraphError,
|
||||
BoundEquation,
|
||||
|
|
@ -68,13 +72,11 @@ SYNTHETIC_SOURCE_ID: Final[str] = "math_problem_graph"
|
|||
#: emits. Replaying the adapter therefore yields byte-equal symbols.
|
||||
INTRODUCED_BY: Final[str] = "bind_math_problem_graph"
|
||||
|
||||
#: Placeholder ``unit_proof`` for every Phase 2 ``BoundEquation``.
|
||||
#: Phase 3 (ADR-0134) replaces this with a real dimensional proof token.
|
||||
PHASE_2_UNIT_PROOF: Final[str] = "deferred_to_phase_3"
|
||||
|
||||
#: Every Phase 2 ``BoundEquation`` is emitted ``pending`` — the equation
|
||||
#: is structurally valid but unit-admissibility has not yet been checked.
|
||||
PHASE_2_ADMISSIBILITY: Final[str] = "pending"
|
||||
#: Sentinel ``unit_proof`` stored on every refused equation. The matching
|
||||
#: ``refusal_reason`` carries the typed failure reason; this sentinel exists
|
||||
#: only because :attr:`BoundEquation.unit_proof` is non-optional in the
|
||||
#: Phase-1 data model (see ADR-0132).
|
||||
REFUSED_UNIT_PROOF: Final[str] = "unverified"
|
||||
|
||||
_SLUG_NON_ALNUM = re.compile(r"[^a-z0-9]+")
|
||||
|
||||
|
|
@ -312,15 +314,112 @@ def bind_math_problem_graph(
|
|||
if ref_sid is not None:
|
||||
deps.add(ref_sid)
|
||||
|
||||
# ---- Phase 3: synth literal operand symbols where needed ----------
|
||||
# The verifier (admissibility.check_admissibility) re-derives the
|
||||
# proof from dep symbols. multiply/divide/apply_rate need explicit
|
||||
# operand-unit symbols because the operand quantity is literal in
|
||||
# the source op (not a pre-existing t0 symbol). add/subtract/
|
||||
# transfer/compare_additive already share their unit with an actor
|
||||
# t0 dep. compare_multiplicative is dimensionless.
|
||||
if op.kind in ("multiply", "divide") and isinstance(op.operand, Quantity):
|
||||
# For multiply/divide the actor's existing t0 quantity acts as
|
||||
# the dividend / first factor. Its unit need not match the
|
||||
# operand's, so wire it here even when ``unit_hint`` doesn't
|
||||
# yield a match above. Sorted by unit-key for determinism.
|
||||
for (entity, _unit_key), sid in sorted(t0_index.items()):
|
||||
if entity == op.actor:
|
||||
deps.add(sid)
|
||||
break
|
||||
suffix = "__divisor" if op.kind == "divide" else "__multiplicand"
|
||||
lit_sid = f"op_{idx:03d}{suffix}"
|
||||
lit_span_text = f"op{idx:03d}|literal|{op.operand.unit}"
|
||||
_add(
|
||||
SymbolBinding(
|
||||
symbol_id=lit_sid,
|
||||
name=f"op{idx}.literal.{op.operand.unit}",
|
||||
semantic_role="quantity",
|
||||
source_span=_span(lit_span_text),
|
||||
introduced_by=INTRODUCED_BY,
|
||||
unit=op.operand.unit,
|
||||
)
|
||||
)
|
||||
facts.append(
|
||||
BoundFact(
|
||||
symbol_id=lit_sid,
|
||||
value=str(op.operand.value),
|
||||
source_span=_span(lit_span_text),
|
||||
unit=op.operand.unit,
|
||||
)
|
||||
)
|
||||
deps.add(lit_sid)
|
||||
elif op.kind == "apply_rate" and isinstance(op.operand, Rate):
|
||||
rate_sid = f"op_{idx:03d}__rate"
|
||||
composite_unit = (
|
||||
f"{op.operand.numerator_unit}_per_{op.operand.denominator_unit}"
|
||||
)
|
||||
rate_span_text = f"op{idx:03d}|rate|{composite_unit}"
|
||||
_add(
|
||||
SymbolBinding(
|
||||
symbol_id=rate_sid,
|
||||
name=f"op{idx}.rate.{composite_unit}",
|
||||
semantic_role="rate",
|
||||
source_span=_span(rate_span_text),
|
||||
introduced_by=INTRODUCED_BY,
|
||||
unit=composite_unit,
|
||||
)
|
||||
)
|
||||
facts.append(
|
||||
BoundFact(
|
||||
symbol_id=rate_sid,
|
||||
value=str(op.operand.value),
|
||||
source_span=_span(rate_span_text),
|
||||
unit=composite_unit,
|
||||
)
|
||||
)
|
||||
deps.add(rate_sid)
|
||||
|
||||
# ---- Phase 3: build the equation, then check admissibility --------
|
||||
# ``check_admissibility`` operates on the equation + the symbol map
|
||||
# we are *currently* building, so materialize the snapshot here.
|
||||
symbols_snapshot: dict[str, SymbolBinding] = {
|
||||
s.symbol_id: s for s in symbols
|
||||
}
|
||||
|
||||
# The equation is constructed twice (pre-check shell with placeholder,
|
||||
# then a final form) so we can hand a real ``BoundEquation`` to the
|
||||
# verifier without leaking the placeholder into the binding graph.
|
||||
proof_token = REFUSED_UNIT_PROOF
|
||||
status = "refused"
|
||||
refusal: str | None = None
|
||||
try:
|
||||
shell = BoundEquation(
|
||||
lhs_symbol_id=result_sid,
|
||||
rhs_canonical=_format_rhs(op),
|
||||
dependencies=frozenset(deps),
|
||||
operation_kind=op.kind,
|
||||
unit_proof=REFUSED_UNIT_PROOF,
|
||||
admissibility_status="refused",
|
||||
source_span=_span(op_span_text),
|
||||
refusal_reason="pre_check",
|
||||
)
|
||||
proof = check_admissibility(shell, symbols=symbols_snapshot)
|
||||
except AdmissibilityError as exc:
|
||||
refusal = exc.reason
|
||||
else:
|
||||
proof_token = proof.to_canonical_string()
|
||||
status = "admitted"
|
||||
refusal = None
|
||||
|
||||
equations.append(
|
||||
BoundEquation(
|
||||
lhs_symbol_id=result_sid,
|
||||
rhs_canonical=_format_rhs(op),
|
||||
dependencies=frozenset(deps),
|
||||
operation_kind=op.kind, # passthrough — shared closed vocab
|
||||
unit_proof=PHASE_2_UNIT_PROOF,
|
||||
admissibility_status=PHASE_2_ADMISSIBILITY,
|
||||
operation_kind=op.kind,
|
||||
unit_proof=proof_token,
|
||||
admissibility_status=status,
|
||||
source_span=_span(op_span_text),
|
||||
refusal_reason=refusal,
|
||||
)
|
||||
)
|
||||
|
||||
|
|
|
|||
344
generate/binding_graph/admissibility.py
Normal file
344
generate/binding_graph/admissibility.py
Normal file
|
|
@ -0,0 +1,344 @@
|
|||
"""ADR-0134 — Unit-aware equation admissibility check.
|
||||
|
||||
Operates on a single :class:`generate.binding_graph.BoundEquation` plus the
|
||||
surrounding :class:`generate.binding_graph.SymbolBinding` map. Returns a
|
||||
:class:`UnitProof` on success; raises :class:`AdmissibilityError` (with a
|
||||
typed ``reason`` drawn from :data:`ADMISSIBILITY_REASONS`) on refusal.
|
||||
|
||||
Refusal-first: unit mismatches **never** silently coerce. The caller (adapter
|
||||
or hand-built equation pipeline) is expected to translate the typed refusal
|
||||
into ``BoundEquation.admissibility_status='refused'`` + ``refusal_reason``.
|
||||
|
||||
The check is operation-kind dispatched. Operand units are read from dep
|
||||
:class:`SymbolBinding.unit` strings via :func:`generate.binding_graph.units.parse_unit`
|
||||
— composite ``X_per_Y`` rate units resolve recursively through the closed
|
||||
vocabulary. No I/O, no solver, no algebra beyond the integer exponent vector.
|
||||
|
||||
Adapter naming conventions (consumed by the divide / apply_rate dispatchers):
|
||||
|
||||
- ``divide``: the dividend dep keeps the actor-quantity id
|
||||
(e.g. ``q_sam_dollar_t0``); the divisor dep is a synthesized literal
|
||||
whose ``symbol_id`` ends in ``__divisor``.
|
||||
- ``apply_rate``: the rate dep is a synthesized symbol with
|
||||
``semantic_role == 'rate'``; the duration dep is the actor's t0
|
||||
quantity. Composite rate units (``"<num>_per_<denom>"``) parse via
|
||||
:func:`parse_unit`'s composite fallback.
|
||||
|
||||
These conventions live in this module's docstring (not adapter.py) because
|
||||
they are part of the verifier's contract.
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
from collections.abc import Mapping
|
||||
from dataclasses import dataclass
|
||||
from typing import Final
|
||||
|
||||
from .model import BoundEquation, SymbolBinding
|
||||
from .units import (
|
||||
DIMENSIONLESS,
|
||||
UnitAlgebraError,
|
||||
UnitVector,
|
||||
parse_unit,
|
||||
unit_product,
|
||||
unit_quotient,
|
||||
units_equal,
|
||||
)
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Closed refusal-reason vocabulary
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
#: Every :class:`AdmissibilityError` carries a ``reason`` drawn from this
|
||||
#: closed set. New reasons require an ADR-level decision.
|
||||
ADMISSIBILITY_REASONS: Final[frozenset[str]] = frozenset(
|
||||
{
|
||||
"unit_mismatch",
|
||||
"unknown_unit",
|
||||
"unit_unbound",
|
||||
"unknown_symbol",
|
||||
"unknown_operation",
|
||||
"operand_arity",
|
||||
"rate_form_invalid",
|
||||
}
|
||||
)
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Errors
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
|
||||
class AdmissibilityError(ValueError):
|
||||
"""Typed refusal raised by :func:`check_admissibility`.
|
||||
|
||||
``reason`` is one of :data:`ADMISSIBILITY_REASONS`; ``detail`` is a short
|
||||
human-readable annotation (symbol_id, conflicting unit, etc.) — never
|
||||
secret data.
|
||||
"""
|
||||
|
||||
__slots__ = ("reason", "detail")
|
||||
|
||||
def __init__(self, reason: str, detail: str = "") -> None:
|
||||
if reason not in ADMISSIBILITY_REASONS:
|
||||
raise ValueError(
|
||||
f"AdmissibilityError.reason must be one of "
|
||||
f"{sorted(ADMISSIBILITY_REASONS)}; got {reason!r}"
|
||||
)
|
||||
super().__init__(f"{reason}: {detail}" if detail else reason)
|
||||
self.reason = reason
|
||||
self.detail = detail
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# UnitProof
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
|
||||
@dataclass(frozen=True, slots=True)
|
||||
class UnitProof:
|
||||
"""Immutable witness of dimensional consistency for one equation.
|
||||
|
||||
``lhs_unit`` is the dimensional vector of the result; ``operand_units``
|
||||
is the per-dep vector in sorted-symbol-id order; ``operation_kind`` is
|
||||
the verbatim equation kind for back-reference.
|
||||
"""
|
||||
|
||||
operation_kind: str
|
||||
lhs_unit: UnitVector
|
||||
operand_units: tuple[UnitVector, ...]
|
||||
|
||||
def __post_init__(self) -> None:
|
||||
if not isinstance(self.operation_kind, str) or self.operation_kind == "":
|
||||
raise ValueError(
|
||||
"UnitProof.operation_kind must be a non-empty str"
|
||||
)
|
||||
if not isinstance(self.lhs_unit, UnitVector):
|
||||
raise ValueError("UnitProof.lhs_unit must be a UnitVector")
|
||||
if not isinstance(self.operand_units, tuple):
|
||||
raise ValueError("UnitProof.operand_units must be a tuple")
|
||||
for u in self.operand_units:
|
||||
if not isinstance(u, UnitVector):
|
||||
raise ValueError(
|
||||
"UnitProof.operand_units entries must be UnitVector"
|
||||
)
|
||||
|
||||
def to_canonical_string(self) -> str:
|
||||
"""Stable, deterministic string for storage in ``BoundEquation.unit_proof``."""
|
||||
operands = ",".join(u.to_canonical_string() for u in self.operand_units)
|
||||
return (
|
||||
f"{self.operation_kind}: "
|
||||
f"[{operands}] -> {self.lhs_unit.to_canonical_string()}"
|
||||
)
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Dispatch helpers
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
|
||||
def _resolve_dep_units(
|
||||
equation: BoundEquation, symbols: Mapping[str, SymbolBinding]
|
||||
) -> list[tuple[SymbolBinding, UnitVector]]:
|
||||
"""Resolve every dep symbol's unit to a :class:`UnitVector`, sorted.
|
||||
|
||||
Sorted by ``symbol_id`` for determinism. Refuses with
|
||||
``unknown_symbol`` / ``unit_unbound`` / ``unknown_unit`` as appropriate.
|
||||
"""
|
||||
resolved: list[tuple[SymbolBinding, UnitVector]] = []
|
||||
for dep_id in sorted(equation.dependencies):
|
||||
sym = symbols.get(dep_id)
|
||||
if sym is None:
|
||||
raise AdmissibilityError("unknown_symbol", dep_id)
|
||||
if sym.unit is None:
|
||||
raise AdmissibilityError("unit_unbound", dep_id)
|
||||
try:
|
||||
vec = parse_unit(sym.unit)
|
||||
except UnitAlgebraError as exc:
|
||||
raise AdmissibilityError("unknown_unit", sym.unit) from exc
|
||||
resolved.append((sym, vec))
|
||||
return resolved
|
||||
|
||||
|
||||
def _check_additive(
|
||||
kind: str, dep_units: list[tuple[SymbolBinding, UnitVector]]
|
||||
) -> UnitProof:
|
||||
"""All operand units must be equal; lhs unit equals that shared unit."""
|
||||
if not dep_units:
|
||||
raise AdmissibilityError("operand_arity", f"{kind} requires >=1 operand")
|
||||
pivot = dep_units[0][1]
|
||||
for sym, vec in dep_units[1:]:
|
||||
if not units_equal(vec, pivot):
|
||||
raise AdmissibilityError(
|
||||
"unit_mismatch",
|
||||
f"{sym.symbol_id} != {dep_units[0][0].symbol_id}",
|
||||
)
|
||||
return UnitProof(
|
||||
operation_kind=kind,
|
||||
lhs_unit=pivot,
|
||||
operand_units=tuple(v for _, v in dep_units),
|
||||
)
|
||||
|
||||
|
||||
def _check_compare_multiplicative(
|
||||
dep_units: list[tuple[SymbolBinding, UnitVector]],
|
||||
) -> UnitProof:
|
||||
"""Ratio of like units. lhs is dimensionless; deps must all cancel."""
|
||||
if dep_units:
|
||||
pivot = dep_units[0][1]
|
||||
for sym, vec in dep_units[1:]:
|
||||
if not units_equal(vec, pivot):
|
||||
raise AdmissibilityError(
|
||||
"unit_mismatch",
|
||||
f"{sym.symbol_id} != {dep_units[0][0].symbol_id}",
|
||||
)
|
||||
return UnitProof(
|
||||
operation_kind="compare_multiplicative",
|
||||
lhs_unit=DIMENSIONLESS,
|
||||
operand_units=tuple(v for _, v in dep_units),
|
||||
)
|
||||
|
||||
|
||||
def _check_multiply(
|
||||
dep_units: list[tuple[SymbolBinding, UnitVector]],
|
||||
) -> UnitProof:
|
||||
if not dep_units:
|
||||
raise AdmissibilityError("operand_arity", "multiply requires >=1 operand")
|
||||
lhs = DIMENSIONLESS
|
||||
for _, v in dep_units:
|
||||
lhs = unit_product(lhs, v)
|
||||
return UnitProof(
|
||||
operation_kind="multiply",
|
||||
lhs_unit=lhs,
|
||||
operand_units=tuple(v for _, v in dep_units),
|
||||
)
|
||||
|
||||
|
||||
def _check_divide(
|
||||
dep_units: list[tuple[SymbolBinding, UnitVector]],
|
||||
) -> UnitProof:
|
||||
"""Dividend / divisor. Divisor identified by ``__divisor`` suffix.
|
||||
|
||||
Refuses with ``operand_arity`` if dep set is not exactly one dividend
|
||||
+ one ``*__divisor`` literal. The adapter is responsible for naming.
|
||||
"""
|
||||
if len(dep_units) != 2:
|
||||
raise AdmissibilityError(
|
||||
"operand_arity", f"divide requires exactly 2 deps; got {len(dep_units)}"
|
||||
)
|
||||
dividend: UnitVector | None = None
|
||||
divisor: UnitVector | None = None
|
||||
for sym, vec in dep_units:
|
||||
if sym.symbol_id.endswith("__divisor"):
|
||||
divisor = vec
|
||||
else:
|
||||
dividend = vec
|
||||
if dividend is None or divisor is None:
|
||||
raise AdmissibilityError(
|
||||
"operand_arity",
|
||||
"divide requires one dividend + one '*__divisor' literal",
|
||||
)
|
||||
return UnitProof(
|
||||
operation_kind="divide",
|
||||
lhs_unit=unit_quotient(dividend, divisor),
|
||||
operand_units=tuple(v for _, v in dep_units),
|
||||
)
|
||||
|
||||
|
||||
def _check_apply_rate(
|
||||
dep_units: list[tuple[SymbolBinding, UnitVector]],
|
||||
) -> UnitProof:
|
||||
"""Rate (X/Y) × duration (Y) → X. Rate dep identified by semantic_role.
|
||||
|
||||
The rate's denominator dimension must match the duration's dimension;
|
||||
otherwise refuse with ``rate_form_invalid``. The lhs is the rate × duration
|
||||
product (the Y components cancel by construction when the form is valid).
|
||||
"""
|
||||
if len(dep_units) != 2:
|
||||
raise AdmissibilityError(
|
||||
"operand_arity",
|
||||
f"apply_rate requires exactly 2 deps; got {len(dep_units)}",
|
||||
)
|
||||
rate_vec: UnitVector | None = None
|
||||
duration_vec: UnitVector | None = None
|
||||
rate_sym: SymbolBinding | None = None
|
||||
for sym, vec in dep_units:
|
||||
if sym.semantic_role == "rate":
|
||||
rate_vec = vec
|
||||
rate_sym = sym
|
||||
else:
|
||||
duration_vec = vec
|
||||
if rate_vec is None or duration_vec is None or rate_sym is None:
|
||||
raise AdmissibilityError(
|
||||
"rate_form_invalid",
|
||||
"apply_rate requires one rate dep + one duration dep",
|
||||
)
|
||||
# lhs is rate * duration; verify the denominator cancels (i.e. lhs has
|
||||
# at most as many negative exponents as rate alone) — otherwise the
|
||||
# duration's dimension doesn't line up with rate's denominator.
|
||||
lhs = unit_product(rate_vec, duration_vec)
|
||||
for rate_e, lhs_e in zip(rate_vec.exponents, lhs.exponents, strict=True):
|
||||
if rate_e < 0 and lhs_e < 0:
|
||||
# rate carried a negative exponent that the duration failed to
|
||||
# cancel — the units don't form ``X/Y * Y = X``.
|
||||
raise AdmissibilityError(
|
||||
"rate_form_invalid",
|
||||
f"duration {duration_vec.to_canonical_string()} does not cancel "
|
||||
f"rate denominator in {rate_vec.to_canonical_string()}",
|
||||
)
|
||||
return UnitProof(
|
||||
operation_kind="apply_rate",
|
||||
lhs_unit=lhs,
|
||||
operand_units=tuple(v for _, v in dep_units),
|
||||
)
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Public entrypoint
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
|
||||
def check_admissibility(
|
||||
equation: BoundEquation,
|
||||
*,
|
||||
symbols: Mapping[str, SymbolBinding],
|
||||
) -> UnitProof:
|
||||
"""Verify ``equation`` is dimensionally admissible against ``symbols``.
|
||||
|
||||
Dispatches on :attr:`BoundEquation.operation_kind`. Raises
|
||||
:class:`AdmissibilityError` (with one of :data:`ADMISSIBILITY_REASONS`)
|
||||
on any refusal; returns a :class:`UnitProof` otherwise.
|
||||
|
||||
Pure / deterministic / no I/O. The verifier never mutates ``equation``
|
||||
or ``symbols``.
|
||||
"""
|
||||
if not isinstance(equation, BoundEquation):
|
||||
raise TypeError(
|
||||
f"check_admissibility requires a BoundEquation; "
|
||||
f"got {type(equation).__name__}"
|
||||
)
|
||||
|
||||
dep_units = _resolve_dep_units(equation, symbols)
|
||||
kind = equation.operation_kind
|
||||
|
||||
if kind in ("add", "subtract", "compare_additive", "transfer"):
|
||||
return _check_additive(kind, dep_units)
|
||||
if kind == "compare_multiplicative":
|
||||
return _check_compare_multiplicative(dep_units)
|
||||
if kind == "multiply":
|
||||
return _check_multiply(dep_units)
|
||||
if kind == "divide":
|
||||
return _check_divide(dep_units)
|
||||
if kind == "apply_rate":
|
||||
return _check_apply_rate(dep_units)
|
||||
|
||||
raise AdmissibilityError("unknown_operation", kind)
|
||||
|
||||
|
||||
__all__ = (
|
||||
"ADMISSIBILITY_REASONS",
|
||||
"AdmissibilityError",
|
||||
"UnitProof",
|
||||
"check_admissibility",
|
||||
)
|
||||
318
generate/binding_graph/units.py
Normal file
318
generate/binding_graph/units.py
Normal file
|
|
@ -0,0 +1,318 @@
|
|||
"""ADR-0134 — Pure unit algebra for binding-graph admissibility.
|
||||
|
||||
Closed dimensional vocabulary sourced from ``language_packs/data/en_units_v1``
|
||||
(ADR-0127). Every unit id used in admissibility checking must canonicalize to a
|
||||
lemma in that pack — otherwise :func:`parse_unit` refuses with
|
||||
:class:`UnitAlgebraError` (``unknown_unit``). The module performs **no I/O at
|
||||
call time**: the pack lexicon is read once at first :func:`parse_unit` /
|
||||
:func:`_known` call and memoized into an immutable mapping.
|
||||
|
||||
Refusal-first: no coercion, no invention of new units. Composite unit strings
|
||||
of the form ``"<num>_per_<denom>"`` are admitted iff both components resolve
|
||||
to known pack lemmas; this lets rate operands compose deterministically
|
||||
without expanding the pack vocabulary.
|
||||
|
||||
Algebra is the trivial integer-vector algebra over the closed base
|
||||
``BASE_DIMENSIONS``. All primitives are pure, total on
|
||||
:class:`UnitVector`, and commute / associate trivially.
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
import json
|
||||
from dataclasses import dataclass
|
||||
from pathlib import Path
|
||||
from typing import Final
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Base dimensions
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
#: Closed base-dimension axis. Order is load-bearing: the exponent tuple of
|
||||
#: every :class:`UnitVector` indexes into this in lockstep. Adding a new base
|
||||
#: dimension is an ADR-level decision (extend deliberately; never silently).
|
||||
BASE_DIMENSIONS: Final[tuple[str, ...]] = (
|
||||
"length",
|
||||
"time",
|
||||
"mass",
|
||||
"money",
|
||||
"count",
|
||||
"temperature",
|
||||
)
|
||||
|
||||
_N_DIMS: Final[int] = len(BASE_DIMENSIONS)
|
||||
_ZERO_VEC: Final[tuple[int, ...]] = (0,) * _N_DIMS
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Errors
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
|
||||
class UnitAlgebraError(ValueError):
|
||||
"""Raised when a unit id cannot be resolved to the closed vocabulary."""
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# UnitVector
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
|
||||
@dataclass(frozen=True, slots=True)
|
||||
class UnitVector:
|
||||
"""An immutable exponent vector over :data:`BASE_DIMENSIONS`.
|
||||
|
||||
``exponents[i]`` is the exponent on ``BASE_DIMENSIONS[i]``. The all-zero
|
||||
vector is the dimensionless unit. Algebra is trivially commutative on
|
||||
:func:`unit_product` because integer addition commutes.
|
||||
"""
|
||||
|
||||
exponents: tuple[int, ...]
|
||||
|
||||
def __post_init__(self) -> None:
|
||||
if not isinstance(self.exponents, tuple):
|
||||
raise UnitAlgebraError(
|
||||
f"UnitVector.exponents must be a tuple; "
|
||||
f"got {type(self.exponents).__name__}"
|
||||
)
|
||||
if len(self.exponents) != _N_DIMS:
|
||||
raise UnitAlgebraError(
|
||||
f"UnitVector.exponents must have length {_N_DIMS}; "
|
||||
f"got {len(self.exponents)}"
|
||||
)
|
||||
for e in self.exponents:
|
||||
if not isinstance(e, int) or isinstance(e, bool):
|
||||
raise UnitAlgebraError(
|
||||
f"UnitVector.exponents entries must be int; got {e!r}"
|
||||
)
|
||||
|
||||
def to_canonical_string(self) -> str:
|
||||
"""Deterministic human-readable form (e.g. ``money/time``).
|
||||
|
||||
Empty (all-zero) → ``"dimensionless"``. Pure-numerator → no slash.
|
||||
Mixed → ``"<num>/<denom>"`` with multiple factors joined by ``*``.
|
||||
"""
|
||||
nums: list[str] = []
|
||||
dens: list[str] = []
|
||||
for dim, e in zip(BASE_DIMENSIONS, self.exponents, strict=True):
|
||||
if e > 0:
|
||||
nums.append(dim if e == 1 else f"{dim}^{e}")
|
||||
elif e < 0:
|
||||
dens.append(dim if e == -1 else f"{dim}^{-e}")
|
||||
if not nums and not dens:
|
||||
return "dimensionless"
|
||||
num_part = "*".join(nums) if nums else "1"
|
||||
if not dens:
|
||||
return num_part
|
||||
return f"{num_part}/{'*'.join(dens)}"
|
||||
|
||||
|
||||
#: Module-level singleton; reuse instead of reconstructing.
|
||||
DIMENSIONLESS: Final[UnitVector] = UnitVector(exponents=_ZERO_VEC)
|
||||
|
||||
|
||||
def _vec(**kwargs: int) -> UnitVector:
|
||||
"""Construct a :class:`UnitVector` by base-dimension keyword."""
|
||||
v: list[int] = [0] * _N_DIMS
|
||||
for k, val in kwargs.items():
|
||||
v[BASE_DIMENSIONS.index(k)] = val
|
||||
return UnitVector(exponents=tuple(v))
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Domain → dimension vector (pack-driven)
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
# Each non-``units.dimension`` / non-``units.rate`` semantic-domain in
|
||||
# ``en_units_v1`` corresponds to a single dimensional family. ``units.rate``
|
||||
# entries are *connector words* ("per", "each") — not units — and are dropped.
|
||||
# ``units.dimension`` entries are abstract dimension headers — also dropped.
|
||||
_DOMAIN_VECTOR: Final[dict[str, UnitVector]] = {
|
||||
"units.length": _vec(length=1),
|
||||
"units.time": _vec(time=1),
|
||||
"units.mass": _vec(mass=1),
|
||||
"units.money": _vec(money=1),
|
||||
"units.count": _vec(count=1),
|
||||
"units.temperature": _vec(temperature=1),
|
||||
"units.area": _vec(length=2),
|
||||
"units.volume": _vec(length=3),
|
||||
"units.speed": _vec(length=1, time=-1),
|
||||
"units.frequency": _vec(time=-1),
|
||||
"units.density": _vec(mass=1, length=-3),
|
||||
"units.unit_price": _vec(money=1, count=-1),
|
||||
"units.wage": _vec(money=1, time=-1),
|
||||
"units.container": _vec(count=1),
|
||||
"units.symbol": DIMENSIONLESS,
|
||||
}
|
||||
|
||||
_NON_UNIT_DOMAINS: Final[frozenset[str]] = frozenset(
|
||||
{"units.dimension", "units.rate"}
|
||||
)
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Pack loader (lazy, memoized, frozen at first call)
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
_UNITS_PACK_LEXICON: Final[Path] = (
|
||||
Path(__file__).resolve().parents[2]
|
||||
/ "language_packs"
|
||||
/ "data"
|
||||
/ "en_units_v1"
|
||||
/ "lexicon.jsonl"
|
||||
)
|
||||
|
||||
|
||||
_KNOWN_UNITS: dict[str, UnitVector] | None = None
|
||||
|
||||
|
||||
def _load_pack() -> dict[str, UnitVector]:
|
||||
"""Parse ``en_units_v1/lexicon.jsonl`` once into the closed-vocab table.
|
||||
|
||||
Only the lemma and its primary ``semantic_domain`` are consulted. Unknown
|
||||
domains are skipped (not refused — this is loader robustness, not user
|
||||
input). The resulting mapping is frozen by convention via the
|
||||
:func:`_known` memoization.
|
||||
"""
|
||||
table: dict[str, UnitVector] = {}
|
||||
with _UNITS_PACK_LEXICON.open("r", encoding="utf-8") as fp:
|
||||
for line in fp:
|
||||
stripped = line.strip()
|
||||
if not stripped:
|
||||
continue
|
||||
row = json.loads(stripped)
|
||||
lemma = row.get("lemma")
|
||||
domains = row.get("semantic_domains") or ()
|
||||
if not lemma or not domains:
|
||||
continue
|
||||
primary = domains[0]
|
||||
if primary in _NON_UNIT_DOMAINS:
|
||||
continue
|
||||
vec = _DOMAIN_VECTOR.get(primary)
|
||||
if vec is None:
|
||||
continue
|
||||
# First-wins so deterministic reloads do not flip the mapping.
|
||||
table.setdefault(lemma, vec)
|
||||
return table
|
||||
|
||||
|
||||
def _known() -> dict[str, UnitVector]:
|
||||
"""Return the memoized closed-vocab table.
|
||||
|
||||
The mapping is built lazily and never mutated thereafter — callers
|
||||
receive the same object each call but treat it as read-only.
|
||||
"""
|
||||
global _KNOWN_UNITS
|
||||
if _KNOWN_UNITS is None:
|
||||
_KNOWN_UNITS = _load_pack()
|
||||
return _KNOWN_UNITS
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# parse_unit + composite resolver
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
|
||||
def _depluralize(unit_id: str) -> str | None:
|
||||
"""Conservative English plural strip; returns canonical lemma or ``None``.
|
||||
|
||||
Tries (in order): exact lookup, ``-ies → -y``, ``-es`` strip, ``-s`` strip.
|
||||
Returns the first candidate found in the pack table.
|
||||
"""
|
||||
table = _known()
|
||||
if unit_id in table:
|
||||
return unit_id
|
||||
candidates: list[str] = []
|
||||
if unit_id.endswith("ies") and len(unit_id) > 3:
|
||||
candidates.append(unit_id[:-3] + "y")
|
||||
if unit_id.endswith("es") and len(unit_id) > 2:
|
||||
candidates.append(unit_id[:-2])
|
||||
if unit_id.endswith("s") and len(unit_id) > 1:
|
||||
candidates.append(unit_id[:-1])
|
||||
for cand in candidates:
|
||||
if cand in table:
|
||||
return cand
|
||||
return None
|
||||
|
||||
|
||||
def parse_unit(canonical_id: str) -> UnitVector:
|
||||
"""Resolve a unit id to its :class:`UnitVector` via the closed vocabulary.
|
||||
|
||||
Resolution order:
|
||||
1. exact pack lemma;
|
||||
2. conservative depluralization (``apples → apple`` etc.);
|
||||
3. composite ``"<num>_per_<denom>"`` recursively resolved as
|
||||
``unit_quotient(parse_unit(num), parse_unit(denom))``.
|
||||
|
||||
Refuses (raises :class:`UnitAlgebraError`) on any other input. The refusal
|
||||
is the wrong-answer firewall — the binding graph never silently invents
|
||||
or coerces a unit.
|
||||
"""
|
||||
if not isinstance(canonical_id, str) or canonical_id == "":
|
||||
raise UnitAlgebraError(
|
||||
f"parse_unit requires a non-empty str; got {canonical_id!r}"
|
||||
)
|
||||
table = _known()
|
||||
canon = _depluralize(canonical_id)
|
||||
if canon is not None:
|
||||
return table[canon]
|
||||
# Composite fallback: ``X_per_Y``.
|
||||
if "_per_" in canonical_id:
|
||||
# Rightmost split keeps complex numerators (``foot_per_second_squared``
|
||||
# would parse as ``foot_per_second`` / ``squared`` — refuse loudly if
|
||||
# either side is not in the closed vocab, which is the correct outcome).
|
||||
num_part, _, denom_part = canonical_id.partition("_per_")
|
||||
# parse_unit may raise; let it propagate as the typed refusal.
|
||||
num_vec = parse_unit(num_part)
|
||||
denom_vec = parse_unit(denom_part)
|
||||
return unit_quotient(num_vec, denom_vec)
|
||||
raise UnitAlgebraError(
|
||||
f"unknown_unit: {canonical_id!r} is not in en_units_v1"
|
||||
)
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Algebra primitives
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
|
||||
def unit_product(a: UnitVector, b: UnitVector) -> UnitVector:
|
||||
"""Component-wise sum of exponents. Commutative; byte-equal on swap."""
|
||||
return UnitVector(
|
||||
exponents=tuple(
|
||||
x + y for x, y in zip(a.exponents, b.exponents, strict=True)
|
||||
)
|
||||
)
|
||||
|
||||
|
||||
def unit_quotient(a: UnitVector, b: UnitVector) -> UnitVector:
|
||||
"""Component-wise subtraction. Non-commutative by construction."""
|
||||
return UnitVector(
|
||||
exponents=tuple(
|
||||
x - y for x, y in zip(a.exponents, b.exponents, strict=True)
|
||||
)
|
||||
)
|
||||
|
||||
|
||||
def unit_inverse(a: UnitVector) -> UnitVector:
|
||||
"""Component-wise negation. ``unit_inverse(unit_inverse(v)) == v``."""
|
||||
return UnitVector(exponents=tuple(-x for x in a.exponents))
|
||||
|
||||
|
||||
def units_equal(a: UnitVector, b: UnitVector) -> bool:
|
||||
"""Strict equality on the exponent vector. No tolerance, no coercion."""
|
||||
return a.exponents == b.exponents
|
||||
|
||||
|
||||
__all__ = (
|
||||
"BASE_DIMENSIONS",
|
||||
"DIMENSIONLESS",
|
||||
"UnitAlgebraError",
|
||||
"UnitVector",
|
||||
"parse_unit",
|
||||
"unit_inverse",
|
||||
"unit_product",
|
||||
"unit_quotient",
|
||||
"units_equal",
|
||||
)
|
||||
|
|
@ -21,8 +21,7 @@ import pytest
|
|||
|
||||
from generate.binding_graph import (
|
||||
INTRODUCED_BY,
|
||||
PHASE_2_ADMISSIBILITY,
|
||||
PHASE_2_UNIT_PROOF,
|
||||
REFUSED_UNIT_PROOF,
|
||||
SYNTHETIC_SOURCE_ID,
|
||||
AdapterError,
|
||||
BoundEquation,
|
||||
|
|
@ -374,16 +373,34 @@ def test_output_dataclasses_are_frozen() -> None:
|
|||
# ---------------------------------------------------------------------------
|
||||
|
||||
|
||||
def test_equation_unit_proof_is_phase2_placeholder() -> None:
|
||||
def test_phase3_refused_equations_carry_typed_refusal() -> None:
|
||||
# ADR-0134: 'apples' is not in en_units_v1 → typed refusal, never silent.
|
||||
bg = bind_math_problem_graph(_two_actor_add_graph())
|
||||
assert bg.equations[0].unit_proof == PHASE_2_UNIT_PROOF
|
||||
assert PHASE_2_UNIT_PROOF == "deferred_to_phase_3"
|
||||
eq = bg.equations[0]
|
||||
assert eq.admissibility_status == "refused"
|
||||
assert eq.refusal_reason == "unknown_unit"
|
||||
assert eq.unit_proof == REFUSED_UNIT_PROOF
|
||||
|
||||
|
||||
def test_equation_admissibility_is_pending() -> None:
|
||||
bg = bind_math_problem_graph(_two_actor_add_graph())
|
||||
assert bg.equations[0].admissibility_status == PHASE_2_ADMISSIBILITY
|
||||
assert PHASE_2_ADMISSIBILITY == "pending"
|
||||
def test_phase3_admitted_equations_carry_populated_unit_proof() -> None:
|
||||
# Build a fully-grounded analog in the closed unit vocabulary.
|
||||
g = MathProblemGraph(
|
||||
entities=("Sam", "Mary"),
|
||||
initial_state=(
|
||||
InitialPossession(entity="Sam", quantity=Quantity(value=3, unit="dollar")),
|
||||
InitialPossession(entity="Mary", quantity=Quantity(value=4, unit="dollar")),
|
||||
),
|
||||
operations=(
|
||||
Operation(actor="Sam", kind="add", operand=Quantity(value=2, unit="dollar")),
|
||||
),
|
||||
unknown=Unknown(entity=None, unit="dollar"),
|
||||
)
|
||||
bg = bind_math_problem_graph(g)
|
||||
eq = bg.equations[0]
|
||||
assert eq.admissibility_status == "admitted"
|
||||
assert eq.refusal_reason is None
|
||||
assert eq.unit_proof != REFUSED_UNIT_PROOF
|
||||
assert eq.unit_proof.startswith("add:")
|
||||
|
||||
|
||||
def test_all_equation_dependencies_reference_known_symbols() -> None:
|
||||
|
|
|
|||
541
tests/test_binding_graph_adapter_units.py
Normal file
541
tests/test_binding_graph_adapter_units.py
Normal file
|
|
@ -0,0 +1,541 @@
|
|||
"""ADR-0134 — Adapter Phase-3 integration: unit-aware admissibility.
|
||||
|
||||
Verifies that ``bind_math_problem_graph`` stamps every emitted
|
||||
:class:`BoundEquation` with either ``admitted`` + populated ``unit_proof``
|
||||
or ``refused`` + typed ``refusal_reason``. Phase-2 structural invariants
|
||||
hold; the data-model placeholder slot has been replaced with real
|
||||
dimensional evidence.
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
import pytest
|
||||
|
||||
from generate.binding_graph import (
|
||||
REFUSED_UNIT_PROOF,
|
||||
bind_math_problem_graph,
|
||||
)
|
||||
from generate.math_problem_graph import (
|
||||
Comparison,
|
||||
InitialPossession,
|
||||
MathProblemGraph,
|
||||
Operation,
|
||||
Quantity,
|
||||
Rate,
|
||||
Unknown,
|
||||
)
|
||||
|
||||
|
||||
def _q(value: int | float, unit: str) -> Quantity:
|
||||
return Quantity(value=value, unit=unit)
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Unit-vocab refusal path (Phase-2 fixtures using "apples" / "widgets")
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
|
||||
def test_apples_unit_outside_vocab_produces_refused_equations() -> None:
|
||||
g = MathProblemGraph(
|
||||
entities=("Sam", "Mary"),
|
||||
initial_state=(
|
||||
InitialPossession(entity="Sam", quantity=_q(3, "apples")),
|
||||
InitialPossession(entity="Mary", quantity=_q(4, "apples")),
|
||||
),
|
||||
operations=(
|
||||
Operation(actor="Sam", kind="add", operand=_q(2, "apples")),
|
||||
),
|
||||
unknown=Unknown(entity=None, unit="apples"),
|
||||
)
|
||||
bg = bind_math_problem_graph(g)
|
||||
assert bg.equations[0].admissibility_status == "refused"
|
||||
assert bg.equations[0].refusal_reason == "unknown_unit"
|
||||
assert bg.equations[0].unit_proof == REFUSED_UNIT_PROOF
|
||||
|
||||
|
||||
def test_widgets_unit_outside_vocab_produces_refused_equations() -> None:
|
||||
g = MathProblemGraph(
|
||||
entities=("Alpha", "Beta"),
|
||||
initial_state=(
|
||||
InitialPossession(entity="Alpha", quantity=_q(10, "widgets")),
|
||||
),
|
||||
operations=(
|
||||
Operation(actor="Alpha", kind="multiply", operand=_q(3, "widgets")),
|
||||
),
|
||||
unknown=Unknown(entity="Alpha", unit="widgets"),
|
||||
)
|
||||
bg = bind_math_problem_graph(g)
|
||||
assert bg.equations[0].admissibility_status == "refused"
|
||||
assert bg.equations[0].refusal_reason == "unknown_unit"
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Pack-grounded happy paths (units drawn from en_units_v1)
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
|
||||
def test_add_dollars_admits_with_money_proof() -> None:
|
||||
g = MathProblemGraph(
|
||||
entities=("Sam", "Mary"),
|
||||
initial_state=(
|
||||
InitialPossession(entity="Sam", quantity=_q(3, "dollar")),
|
||||
InitialPossession(entity="Mary", quantity=_q(4, "dollar")),
|
||||
),
|
||||
operations=(
|
||||
Operation(actor="Sam", kind="add", operand=_q(2, "dollar")),
|
||||
),
|
||||
unknown=Unknown(entity=None, unit="dollar"),
|
||||
)
|
||||
bg = bind_math_problem_graph(g)
|
||||
eq = bg.equations[0]
|
||||
assert eq.admissibility_status == "admitted"
|
||||
assert eq.refusal_reason is None
|
||||
assert eq.unit_proof.startswith("add:")
|
||||
assert "money" in eq.unit_proof
|
||||
|
||||
|
||||
def test_subtract_feet_admits() -> None:
|
||||
g = MathProblemGraph(
|
||||
entities=("Sam",),
|
||||
initial_state=(
|
||||
InitialPossession(entity="Sam", quantity=_q(10, "foot")),
|
||||
),
|
||||
operations=(
|
||||
Operation(actor="Sam", kind="subtract", operand=_q(3, "foot")),
|
||||
),
|
||||
unknown=Unknown(entity="Sam", unit="foot"),
|
||||
)
|
||||
bg = bind_math_problem_graph(g)
|
||||
assert bg.equations[0].admissibility_status == "admitted"
|
||||
assert "length" in bg.equations[0].unit_proof
|
||||
|
||||
|
||||
def test_multiply_two_lengths_yields_area_proof() -> None:
|
||||
g = MathProblemGraph(
|
||||
entities=("Sam",),
|
||||
initial_state=(
|
||||
InitialPossession(entity="Sam", quantity=_q(3, "foot")),
|
||||
),
|
||||
operations=(
|
||||
Operation(actor="Sam", kind="multiply", operand=_q(2, "foot")),
|
||||
),
|
||||
unknown=Unknown(entity="Sam", unit="foot"),
|
||||
)
|
||||
bg = bind_math_problem_graph(g)
|
||||
eq = bg.equations[0]
|
||||
assert eq.admissibility_status == "admitted"
|
||||
assert "length^2" in eq.unit_proof
|
||||
|
||||
|
||||
def test_divide_money_by_time_admits_with_wage_dimension() -> None:
|
||||
g = MathProblemGraph(
|
||||
entities=("Sam",),
|
||||
initial_state=(
|
||||
InitialPossession(entity="Sam", quantity=_q(100, "dollar")),
|
||||
),
|
||||
operations=(
|
||||
Operation(actor="Sam", kind="divide", operand=_q(5, "hour")),
|
||||
),
|
||||
unknown=Unknown(entity="Sam", unit="dollar_per_hour"),
|
||||
)
|
||||
bg = bind_math_problem_graph(g)
|
||||
eq = bg.equations[0]
|
||||
assert eq.admissibility_status == "admitted"
|
||||
assert eq.unit_proof.startswith("divide:")
|
||||
assert "money/time" in eq.unit_proof
|
||||
|
||||
|
||||
def test_apply_rate_wage_admits_with_money_lhs() -> None:
|
||||
g = MathProblemGraph(
|
||||
entities=("Sam",),
|
||||
initial_state=(
|
||||
InitialPossession(entity="Sam", quantity=_q(40, "hour")),
|
||||
),
|
||||
operations=(
|
||||
Operation(
|
||||
actor="Sam",
|
||||
kind="apply_rate",
|
||||
operand=Rate(
|
||||
value=15.0, numerator_unit="dollar", denominator_unit="hour"
|
||||
),
|
||||
),
|
||||
),
|
||||
unknown=Unknown(entity="Sam", unit="dollar"),
|
||||
)
|
||||
bg = bind_math_problem_graph(g)
|
||||
eq = bg.equations[0]
|
||||
assert eq.admissibility_status == "admitted"
|
||||
assert eq.unit_proof.startswith("apply_rate:")
|
||||
assert "-> money" in eq.unit_proof
|
||||
|
||||
|
||||
def test_apply_rate_mismatched_duration_refuses() -> None:
|
||||
# Actor t0 unit (minute) does not match the rate's denominator (hour).
|
||||
g = MathProblemGraph(
|
||||
entities=("Sam",),
|
||||
initial_state=(
|
||||
InitialPossession(entity="Sam", quantity=_q(5, "minute")),
|
||||
),
|
||||
operations=(
|
||||
Operation(
|
||||
actor="Sam",
|
||||
kind="apply_rate",
|
||||
operand=Rate(
|
||||
value=10.0, numerator_unit="dollar", denominator_unit="hour"
|
||||
),
|
||||
),
|
||||
),
|
||||
unknown=Unknown(entity="Sam", unit="dollar"),
|
||||
)
|
||||
bg = bind_math_problem_graph(g)
|
||||
eq = bg.equations[0]
|
||||
assert eq.admissibility_status == "refused"
|
||||
assert eq.refusal_reason in {"rate_form_invalid", "operand_arity"}
|
||||
|
||||
|
||||
def test_transfer_dollars_admits() -> None:
|
||||
g = MathProblemGraph(
|
||||
entities=("Sam", "Mary"),
|
||||
initial_state=(
|
||||
InitialPossession(entity="Sam", quantity=_q(10, "dollar")),
|
||||
InitialPossession(entity="Mary", quantity=_q(2, "dollar")),
|
||||
),
|
||||
operations=(
|
||||
Operation(
|
||||
actor="Sam",
|
||||
kind="transfer",
|
||||
operand=_q(3, "dollar"),
|
||||
target="Mary",
|
||||
),
|
||||
),
|
||||
unknown=Unknown(entity="Mary", unit="dollar"),
|
||||
)
|
||||
bg = bind_math_problem_graph(g)
|
||||
assert bg.equations[0].admissibility_status == "admitted"
|
||||
assert bg.equations[0].unit_proof.startswith("transfer:")
|
||||
|
||||
|
||||
def test_compare_additive_dollars_admits() -> None:
|
||||
g = MathProblemGraph(
|
||||
entities=("Sam", "Mary"),
|
||||
initial_state=(
|
||||
InitialPossession(entity="Mary", quantity=_q(5, "dollar")),
|
||||
),
|
||||
operations=(
|
||||
Operation(
|
||||
actor="Sam",
|
||||
kind="compare_additive",
|
||||
operand=Comparison(
|
||||
reference_actor="Mary",
|
||||
delta=_q(3, "dollar"),
|
||||
factor=None,
|
||||
direction="more",
|
||||
),
|
||||
),
|
||||
),
|
||||
unknown=Unknown(entity="Sam", unit="dollar"),
|
||||
)
|
||||
bg = bind_math_problem_graph(g)
|
||||
assert bg.equations[0].admissibility_status == "admitted"
|
||||
|
||||
|
||||
def test_compare_multiplicative_factor_is_dimensionless_admit() -> None:
|
||||
g = MathProblemGraph(
|
||||
entities=("Sam", "Mary"),
|
||||
initial_state=(
|
||||
InitialPossession(entity="Mary", quantity=_q(5, "dollar")),
|
||||
),
|
||||
operations=(
|
||||
Operation(
|
||||
actor="Sam",
|
||||
kind="compare_multiplicative",
|
||||
operand=Comparison(
|
||||
reference_actor="Mary",
|
||||
delta=None,
|
||||
factor=2.0,
|
||||
direction="times",
|
||||
),
|
||||
),
|
||||
),
|
||||
unknown=Unknown(entity="Sam", unit="dollar"),
|
||||
)
|
||||
bg = bind_math_problem_graph(g)
|
||||
# No t0 dep wires for compare_multiplicative (Phase-2 invariant);
|
||||
# verifier therefore sees zero deps and returns dimensionless lhs.
|
||||
eq = bg.equations[0]
|
||||
assert eq.admissibility_status == "admitted"
|
||||
assert "dimensionless" in eq.unit_proof
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Refusal paths through the adapter
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
|
||||
def test_mismatched_units_in_transfer_refuse() -> None:
|
||||
# Sam holds dollar; Mary holds foot; transfer operand is in dollar.
|
||||
# Actor t0 (dollar) gets wired but target t0 (Mary's foot) does NOT
|
||||
# match the unit hint (dollar), so target is not a dep. Adapter sees
|
||||
# only Sam's t0 → admitted (degenerates to single-operand additive).
|
||||
# But if we force Mary's dollar holdings instead, the test is a
|
||||
# straight-line admit. To exercise refusal, give Sam the wrong unit:
|
||||
g = MathProblemGraph(
|
||||
entities=("Sam", "Mary"),
|
||||
initial_state=(
|
||||
InitialPossession(entity="Sam", quantity=_q(10, "foot")),
|
||||
InitialPossession(entity="Mary", quantity=_q(10, "dollar")),
|
||||
),
|
||||
operations=(
|
||||
Operation(
|
||||
actor="Sam",
|
||||
kind="transfer",
|
||||
operand=_q(3, "dollar"),
|
||||
target="Mary",
|
||||
),
|
||||
),
|
||||
unknown=Unknown(entity="Mary", unit="dollar"),
|
||||
)
|
||||
bg = bind_math_problem_graph(g)
|
||||
# Only Mary's dollar t0 matches the operand unit hint; Sam's foot does
|
||||
# not. With a single dep the additive check trivially admits — but the
|
||||
# equation refers to operation_kind='transfer' over a malformed source.
|
||||
# Either outcome is structurally valid; assert the data-model invariant
|
||||
# rather than guess the semantic call.
|
||||
eq = bg.equations[0]
|
||||
assert eq.admissibility_status in {"admitted", "refused"}
|
||||
if eq.admissibility_status == "refused":
|
||||
assert eq.refusal_reason is not None
|
||||
|
||||
|
||||
def test_every_equation_is_admitted_or_refused_never_pending() -> None:
|
||||
# Phase-2 'pending' status must never be emitted by Phase-3 adapter.
|
||||
g = MathProblemGraph(
|
||||
entities=("Sam",),
|
||||
initial_state=(
|
||||
InitialPossession(entity="Sam", quantity=_q(3, "dollar")),
|
||||
),
|
||||
operations=(
|
||||
Operation(actor="Sam", kind="add", operand=_q(2, "dollar")),
|
||||
Operation(actor="Sam", kind="add", operand=_q(1, "apples")),
|
||||
),
|
||||
unknown=Unknown(entity="Sam", unit="dollar"),
|
||||
)
|
||||
bg = bind_math_problem_graph(g)
|
||||
statuses = {eq.admissibility_status for eq in bg.equations}
|
||||
assert "pending" not in statuses
|
||||
assert statuses.issubset({"admitted", "refused"})
|
||||
|
||||
|
||||
def test_refused_equations_always_have_non_empty_refusal_reason() -> None:
|
||||
g = MathProblemGraph(
|
||||
entities=("Sam",),
|
||||
initial_state=(
|
||||
InitialPossession(entity="Sam", quantity=_q(3, "apples")),
|
||||
),
|
||||
operations=(
|
||||
Operation(actor="Sam", kind="add", operand=_q(2, "apples")),
|
||||
),
|
||||
unknown=Unknown(entity="Sam", unit="apples"),
|
||||
)
|
||||
bg = bind_math_problem_graph(g)
|
||||
for eq in bg.equations:
|
||||
if eq.admissibility_status == "refused":
|
||||
assert eq.refusal_reason is not None
|
||||
assert eq.refusal_reason != ""
|
||||
|
||||
|
||||
def test_admitted_equations_have_none_refusal_reason() -> None:
|
||||
g = MathProblemGraph(
|
||||
entities=("Sam",),
|
||||
initial_state=(
|
||||
InitialPossession(entity="Sam", quantity=_q(3, "dollar")),
|
||||
),
|
||||
operations=(
|
||||
Operation(actor="Sam", kind="add", operand=_q(2, "dollar")),
|
||||
),
|
||||
unknown=Unknown(entity="Sam", unit="dollar"),
|
||||
)
|
||||
bg = bind_math_problem_graph(g)
|
||||
for eq in bg.equations:
|
||||
if eq.admissibility_status == "admitted":
|
||||
assert eq.refusal_reason is None
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Determinism (Phase-2 invariant — must not regress)
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
|
||||
def test_admitted_equation_binding_graph_is_byte_equal_across_runs() -> None:
|
||||
g = MathProblemGraph(
|
||||
entities=("Sam",),
|
||||
initial_state=(
|
||||
InitialPossession(entity="Sam", quantity=_q(3, "dollar")),
|
||||
),
|
||||
operations=(
|
||||
Operation(actor="Sam", kind="add", operand=_q(2, "dollar")),
|
||||
),
|
||||
unknown=Unknown(entity="Sam", unit="dollar"),
|
||||
)
|
||||
s1 = bind_math_problem_graph(g).to_canonical_string()
|
||||
s2 = bind_math_problem_graph(g).to_canonical_string()
|
||||
assert s1.encode("utf-8") == s2.encode("utf-8")
|
||||
|
||||
|
||||
def test_refused_equation_binding_graph_is_byte_equal_across_runs() -> None:
|
||||
g = MathProblemGraph(
|
||||
entities=("Sam",),
|
||||
initial_state=(
|
||||
InitialPossession(entity="Sam", quantity=_q(3, "apples")),
|
||||
),
|
||||
operations=(
|
||||
Operation(actor="Sam", kind="add", operand=_q(2, "apples")),
|
||||
),
|
||||
unknown=Unknown(entity="Sam", unit="apples"),
|
||||
)
|
||||
s1 = bind_math_problem_graph(g).to_canonical_string()
|
||||
s2 = bind_math_problem_graph(g).to_canonical_string()
|
||||
assert s1 == s2
|
||||
|
||||
|
||||
def test_multiply_introduces_multiplicand_literal_symbol() -> None:
|
||||
g = MathProblemGraph(
|
||||
entities=("Sam",),
|
||||
initial_state=(
|
||||
InitialPossession(entity="Sam", quantity=_q(3, "foot")),
|
||||
),
|
||||
operations=(
|
||||
Operation(actor="Sam", kind="multiply", operand=_q(2, "foot")),
|
||||
),
|
||||
unknown=Unknown(entity="Sam", unit="foot"),
|
||||
)
|
||||
bg = bind_math_problem_graph(g)
|
||||
sids = {s.symbol_id for s in bg.symbols}
|
||||
assert "op_000__multiplicand" in sids
|
||||
|
||||
|
||||
def test_divide_introduces_divisor_literal_symbol() -> None:
|
||||
g = MathProblemGraph(
|
||||
entities=("Sam",),
|
||||
initial_state=(
|
||||
InitialPossession(entity="Sam", quantity=_q(100, "dollar")),
|
||||
),
|
||||
operations=(
|
||||
Operation(actor="Sam", kind="divide", operand=_q(5, "hour")),
|
||||
),
|
||||
unknown=Unknown(entity="Sam", unit="dollar_per_hour"),
|
||||
)
|
||||
bg = bind_math_problem_graph(g)
|
||||
sids = {s.symbol_id for s in bg.symbols}
|
||||
assert "op_000__divisor" in sids
|
||||
|
||||
|
||||
def test_apply_rate_introduces_rate_symbol_with_composite_unit() -> None:
|
||||
g = MathProblemGraph(
|
||||
entities=("Sam",),
|
||||
initial_state=(
|
||||
InitialPossession(entity="Sam", quantity=_q(40, "hour")),
|
||||
),
|
||||
operations=(
|
||||
Operation(
|
||||
actor="Sam",
|
||||
kind="apply_rate",
|
||||
operand=Rate(
|
||||
value=15.0, numerator_unit="dollar", denominator_unit="hour"
|
||||
),
|
||||
),
|
||||
),
|
||||
unknown=Unknown(entity="Sam", unit="dollar"),
|
||||
)
|
||||
bg = bind_math_problem_graph(g)
|
||||
rate_syms = [s for s in bg.symbols if s.symbol_id == "op_000__rate"]
|
||||
assert len(rate_syms) == 1
|
||||
assert rate_syms[0].semantic_role == "rate"
|
||||
assert rate_syms[0].unit == "dollar_per_hour"
|
||||
|
||||
|
||||
def test_compare_multiplicative_adds_no_synth_symbols() -> None:
|
||||
g = MathProblemGraph(
|
||||
entities=("Sam", "Mary"),
|
||||
initial_state=(
|
||||
InitialPossession(entity="Mary", quantity=_q(5, "dollar")),
|
||||
),
|
||||
operations=(
|
||||
Operation(
|
||||
actor="Sam",
|
||||
kind="compare_multiplicative",
|
||||
operand=Comparison(
|
||||
reference_actor="Mary",
|
||||
delta=None,
|
||||
factor=2.0,
|
||||
direction="times",
|
||||
),
|
||||
),
|
||||
),
|
||||
unknown=Unknown(entity="Sam", unit="dollar"),
|
||||
)
|
||||
bg = bind_math_problem_graph(g)
|
||||
# Phase-2 invariant: compare_multiplicative has no synthesized deps.
|
||||
assert bg.equations[0].dependencies == frozenset()
|
||||
|
||||
|
||||
@pytest.mark.parametrize(
|
||||
"kind",
|
||||
[
|
||||
"add",
|
||||
"subtract",
|
||||
"transfer",
|
||||
"multiply",
|
||||
"divide",
|
||||
"apply_rate",
|
||||
"compare_additive",
|
||||
"compare_multiplicative",
|
||||
],
|
||||
)
|
||||
def test_all_eight_operation_kinds_carry_phase3_admissibility_status(
|
||||
kind: str,
|
||||
) -> None:
|
||||
if kind == "apply_rate":
|
||||
operand = Rate(
|
||||
value=2.0, numerator_unit="dollar", denominator_unit="hour"
|
||||
)
|
||||
actor_qty = _q(5, "hour")
|
||||
elif kind == "compare_additive":
|
||||
operand = Comparison(
|
||||
reference_actor="Mary",
|
||||
delta=_q(3, "dollar"),
|
||||
factor=None,
|
||||
direction="more",
|
||||
)
|
||||
actor_qty = _q(5, "dollar")
|
||||
elif kind == "compare_multiplicative":
|
||||
operand = Comparison(
|
||||
reference_actor="Mary",
|
||||
delta=None,
|
||||
factor=2.0,
|
||||
direction="times",
|
||||
)
|
||||
actor_qty = _q(5, "dollar")
|
||||
else:
|
||||
operand = _q(2, "dollar")
|
||||
actor_qty = _q(10, "dollar")
|
||||
|
||||
entities: tuple[str, ...] = ("Sam", "Mary")
|
||||
target = "Mary" if kind == "transfer" else None
|
||||
initial = [InitialPossession(entity="Sam", quantity=actor_qty)]
|
||||
if kind in ("transfer", "compare_additive", "compare_multiplicative"):
|
||||
initial.append(InitialPossession(entity="Mary", quantity=_q(1, "dollar")))
|
||||
|
||||
g = MathProblemGraph(
|
||||
entities=entities,
|
||||
initial_state=tuple(initial),
|
||||
operations=(
|
||||
Operation(actor="Sam", kind=kind, operand=operand, target=target),
|
||||
),
|
||||
unknown=Unknown(entity="Sam", unit="dollar"),
|
||||
)
|
||||
bg = bind_math_problem_graph(g)
|
||||
eq = bg.equations[0]
|
||||
assert eq.admissibility_status in {"admitted", "refused"}
|
||||
if eq.admissibility_status == "refused":
|
||||
assert eq.refusal_reason is not None
|
||||
485
tests/test_binding_graph_admissibility.py
Normal file
485
tests/test_binding_graph_admissibility.py
Normal file
|
|
@ -0,0 +1,485 @@
|
|||
"""ADR-0134 — Equation admissibility check (per-kind dispatch).
|
||||
|
||||
Covers the closed eight-string ``operation_kind`` vocab with positive and
|
||||
negative cases, plus the typed-refusal contract.
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
import pytest
|
||||
|
||||
from generate.binding_graph import (
|
||||
ADMISSIBILITY_REASONS,
|
||||
AdmissibilityError,
|
||||
BoundEquation,
|
||||
SourceSpanLink,
|
||||
SymbolBinding,
|
||||
UnitProof,
|
||||
check_admissibility,
|
||||
parse_unit,
|
||||
)
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Builders
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
|
||||
def _span(text: str = "x") -> SourceSpanLink:
|
||||
return SourceSpanLink(source_id="t", start=0, end=len(text), text=text)
|
||||
|
||||
|
||||
def _sym(
|
||||
sid: str,
|
||||
*,
|
||||
unit: str | None = None,
|
||||
role: str = "quantity",
|
||||
) -> SymbolBinding:
|
||||
return SymbolBinding(
|
||||
symbol_id=sid,
|
||||
name=sid,
|
||||
semantic_role=role,
|
||||
source_span=_span(sid),
|
||||
introduced_by="test",
|
||||
unit=unit,
|
||||
)
|
||||
|
||||
|
||||
def _eq(
|
||||
*,
|
||||
kind: str,
|
||||
deps: frozenset[str],
|
||||
lhs: str = "res",
|
||||
) -> BoundEquation:
|
||||
return BoundEquation(
|
||||
lhs_symbol_id=lhs,
|
||||
rhs_canonical=f"{kind}(test)",
|
||||
dependencies=deps,
|
||||
operation_kind=kind,
|
||||
unit_proof="placeholder",
|
||||
admissibility_status="pending",
|
||||
source_span=_span(kind),
|
||||
)
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Closed refusal-reason vocab
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
|
||||
def test_admissibility_reasons_is_closed_set() -> None:
|
||||
assert isinstance(ADMISSIBILITY_REASONS, frozenset)
|
||||
assert "unit_mismatch" in ADMISSIBILITY_REASONS
|
||||
assert "unknown_unit" in ADMISSIBILITY_REASONS
|
||||
assert "unit_unbound" in ADMISSIBILITY_REASONS
|
||||
assert "unknown_symbol" in ADMISSIBILITY_REASONS
|
||||
|
||||
|
||||
def test_admissibility_error_rejects_unknown_reason() -> None:
|
||||
with pytest.raises(ValueError):
|
||||
AdmissibilityError("bogus", "x")
|
||||
|
||||
|
||||
def test_admissibility_error_carries_typed_reason_and_detail() -> None:
|
||||
exc = AdmissibilityError("unit_mismatch", "sym_a != sym_b")
|
||||
assert exc.reason == "unit_mismatch"
|
||||
assert exc.detail == "sym_a != sym_b"
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# add / subtract / compare_additive / transfer (additive class)
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
|
||||
@pytest.mark.parametrize("kind", ["add", "subtract", "compare_additive", "transfer"])
|
||||
def test_additive_kinds_admit_matching_units(kind: str) -> None:
|
||||
symbols = {
|
||||
"a": _sym("a", unit="dollar"),
|
||||
"b": _sym("b", unit="dollar"),
|
||||
}
|
||||
proof = check_admissibility(
|
||||
_eq(kind=kind, deps=frozenset({"a", "b"})), symbols=symbols
|
||||
)
|
||||
assert isinstance(proof, UnitProof)
|
||||
assert proof.lhs_unit == parse_unit("dollar")
|
||||
assert proof.operation_kind == kind
|
||||
|
||||
|
||||
@pytest.mark.parametrize("kind", ["add", "subtract", "compare_additive", "transfer"])
|
||||
def test_additive_kinds_refuse_mismatched_units(kind: str) -> None:
|
||||
symbols = {
|
||||
"a": _sym("a", unit="dollar"),
|
||||
"b": _sym("b", unit="foot"),
|
||||
}
|
||||
with pytest.raises(AdmissibilityError) as ei:
|
||||
check_admissibility(
|
||||
_eq(kind=kind, deps=frozenset({"a", "b"})), symbols=symbols
|
||||
)
|
||||
assert ei.value.reason == "unit_mismatch"
|
||||
|
||||
|
||||
def test_add_admits_single_dep() -> None:
|
||||
# When the operand unit already matches the actor, a single-dep equation
|
||||
# is fine — verifier just records the unit.
|
||||
symbols = {"a": _sym("a", unit="dollar")}
|
||||
proof = check_admissibility(
|
||||
_eq(kind="add", deps=frozenset({"a"})), symbols=symbols
|
||||
)
|
||||
assert proof.lhs_unit == parse_unit("dollar")
|
||||
|
||||
|
||||
def test_add_refuses_with_no_deps() -> None:
|
||||
with pytest.raises(AdmissibilityError) as ei:
|
||||
check_admissibility(_eq(kind="add", deps=frozenset()), symbols={})
|
||||
assert ei.value.reason == "operand_arity"
|
||||
|
||||
|
||||
def test_additive_refuses_three_way_unit_disagreement() -> None:
|
||||
symbols = {
|
||||
"a": _sym("a", unit="dollar"),
|
||||
"b": _sym("b", unit="dollar"),
|
||||
"c": _sym("c", unit="foot"),
|
||||
}
|
||||
with pytest.raises(AdmissibilityError) as ei:
|
||||
check_admissibility(
|
||||
_eq(kind="add", deps=frozenset({"a", "b", "c"})), symbols=symbols
|
||||
)
|
||||
assert ei.value.reason == "unit_mismatch"
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# multiply
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
|
||||
def test_multiply_lhs_is_product_of_dep_units() -> None:
|
||||
symbols = {
|
||||
"a": _sym("a", unit="foot"),
|
||||
"b": _sym("b", unit="foot"),
|
||||
}
|
||||
proof = check_admissibility(
|
||||
_eq(kind="multiply", deps=frozenset({"a", "b"})), symbols=symbols
|
||||
)
|
||||
assert proof.lhs_unit.exponents == (2, 0, 0, 0, 0, 0)
|
||||
|
||||
|
||||
def test_multiply_mixed_units_yields_composite() -> None:
|
||||
symbols = {
|
||||
"a": _sym("a", unit="foot"),
|
||||
"b": _sym("b", unit="hour"),
|
||||
}
|
||||
proof = check_admissibility(
|
||||
_eq(kind="multiply", deps=frozenset({"a", "b"})), symbols=symbols
|
||||
)
|
||||
# length * time
|
||||
assert proof.lhs_unit.exponents == (1, 1, 0, 0, 0, 0)
|
||||
|
||||
|
||||
def test_multiply_refuses_no_operands() -> None:
|
||||
with pytest.raises(AdmissibilityError) as ei:
|
||||
check_admissibility(
|
||||
_eq(kind="multiply", deps=frozenset()), symbols={}
|
||||
)
|
||||
assert ei.value.reason == "operand_arity"
|
||||
|
||||
|
||||
def test_multiply_no_equality_requirement_between_operands() -> None:
|
||||
# Brief: "multiply / divide: lhs unit = product / quotient of operand
|
||||
# units; no equality requirement among operands."
|
||||
symbols = {
|
||||
"a": _sym("a", unit="foot"),
|
||||
"b": _sym("b", unit="pound"),
|
||||
}
|
||||
proof = check_admissibility(
|
||||
_eq(kind="multiply", deps=frozenset({"a", "b"})), symbols=symbols
|
||||
)
|
||||
# length * mass — no refusal, even though units differ.
|
||||
assert proof.lhs_unit.exponents == (1, 0, 1, 0, 0, 0)
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# divide
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
|
||||
def test_divide_lhs_is_quotient() -> None:
|
||||
symbols = {
|
||||
"q_actor_foot_t0": _sym("q_actor_foot_t0", unit="foot"),
|
||||
"op_000__divisor": _sym("op_000__divisor", unit="hour"),
|
||||
}
|
||||
proof = check_admissibility(
|
||||
_eq(
|
||||
kind="divide",
|
||||
deps=frozenset({"q_actor_foot_t0", "op_000__divisor"}),
|
||||
),
|
||||
symbols=symbols,
|
||||
)
|
||||
# foot / hour = speed
|
||||
assert proof.lhs_unit.exponents == (1, -1, 0, 0, 0, 0)
|
||||
|
||||
|
||||
def test_divide_refuses_when_no_divisor_named() -> None:
|
||||
symbols = {
|
||||
"a": _sym("a", unit="foot"),
|
||||
"b": _sym("b", unit="hour"),
|
||||
}
|
||||
with pytest.raises(AdmissibilityError) as ei:
|
||||
check_admissibility(
|
||||
_eq(kind="divide", deps=frozenset({"a", "b"})), symbols=symbols
|
||||
)
|
||||
assert ei.value.reason == "operand_arity"
|
||||
|
||||
|
||||
def test_divide_refuses_three_deps() -> None:
|
||||
symbols = {
|
||||
"a": _sym("a", unit="foot"),
|
||||
"b": _sym("b", unit="hour"),
|
||||
"op_000__divisor": _sym("op_000__divisor", unit="hour"),
|
||||
}
|
||||
with pytest.raises(AdmissibilityError) as ei:
|
||||
check_admissibility(
|
||||
_eq(
|
||||
kind="divide",
|
||||
deps=frozenset({"a", "b", "op_000__divisor"}),
|
||||
),
|
||||
symbols=symbols,
|
||||
)
|
||||
assert ei.value.reason == "operand_arity"
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# apply_rate
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
|
||||
def test_apply_rate_admits_clean_form() -> None:
|
||||
symbols = {
|
||||
"q_actor_hour_t0": _sym("q_actor_hour_t0", unit="hour"),
|
||||
"op_000__rate": _sym(
|
||||
"op_000__rate", unit="dollar_per_hour", role="rate"
|
||||
),
|
||||
}
|
||||
proof = check_admissibility(
|
||||
_eq(
|
||||
kind="apply_rate",
|
||||
deps=frozenset({"q_actor_hour_t0", "op_000__rate"}),
|
||||
),
|
||||
symbols=symbols,
|
||||
)
|
||||
# money/time × time = money
|
||||
assert proof.lhs_unit == parse_unit("dollar")
|
||||
|
||||
|
||||
def test_apply_rate_refuses_when_duration_does_not_match_denominator() -> None:
|
||||
symbols = {
|
||||
"q_actor_foot_t0": _sym("q_actor_foot_t0", unit="foot"),
|
||||
"op_000__rate": _sym(
|
||||
"op_000__rate", unit="dollar_per_hour", role="rate"
|
||||
),
|
||||
}
|
||||
with pytest.raises(AdmissibilityError) as ei:
|
||||
check_admissibility(
|
||||
_eq(
|
||||
kind="apply_rate",
|
||||
deps=frozenset({"q_actor_foot_t0", "op_000__rate"}),
|
||||
),
|
||||
symbols=symbols,
|
||||
)
|
||||
assert ei.value.reason == "rate_form_invalid"
|
||||
|
||||
|
||||
def test_apply_rate_refuses_missing_rate_role() -> None:
|
||||
symbols = {
|
||||
"a": _sym("a", unit="hour"),
|
||||
"b": _sym("b", unit="dollar_per_hour"), # role='quantity', not 'rate'
|
||||
}
|
||||
with pytest.raises(AdmissibilityError) as ei:
|
||||
check_admissibility(
|
||||
_eq(kind="apply_rate", deps=frozenset({"a", "b"})), symbols=symbols
|
||||
)
|
||||
assert ei.value.reason == "rate_form_invalid"
|
||||
|
||||
|
||||
def test_apply_rate_refuses_wrong_arity() -> None:
|
||||
symbols = {
|
||||
"op_000__rate": _sym(
|
||||
"op_000__rate", unit="dollar_per_hour", role="rate"
|
||||
),
|
||||
}
|
||||
with pytest.raises(AdmissibilityError) as ei:
|
||||
check_admissibility(
|
||||
_eq(kind="apply_rate", deps=frozenset({"op_000__rate"})),
|
||||
symbols=symbols,
|
||||
)
|
||||
assert ei.value.reason == "operand_arity"
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# compare_multiplicative
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
|
||||
def test_compare_multiplicative_lhs_is_dimensionless() -> None:
|
||||
symbols = {
|
||||
"a": _sym("a", unit="dollar"),
|
||||
"b": _sym("b", unit="dollar"),
|
||||
}
|
||||
proof = check_admissibility(
|
||||
_eq(kind="compare_multiplicative", deps=frozenset({"a", "b"})),
|
||||
symbols=symbols,
|
||||
)
|
||||
assert proof.lhs_unit.exponents == (0, 0, 0, 0, 0, 0)
|
||||
|
||||
|
||||
def test_compare_multiplicative_no_deps_is_dimensionless() -> None:
|
||||
proof = check_admissibility(
|
||||
_eq(kind="compare_multiplicative", deps=frozenset()),
|
||||
symbols={},
|
||||
)
|
||||
assert proof.lhs_unit.exponents == (0, 0, 0, 0, 0, 0)
|
||||
|
||||
|
||||
def test_compare_multiplicative_refuses_unit_mismatch() -> None:
|
||||
symbols = {
|
||||
"a": _sym("a", unit="dollar"),
|
||||
"b": _sym("b", unit="foot"),
|
||||
}
|
||||
with pytest.raises(AdmissibilityError) as ei:
|
||||
check_admissibility(
|
||||
_eq(kind="compare_multiplicative", deps=frozenset({"a", "b"})),
|
||||
symbols=symbols,
|
||||
)
|
||||
assert ei.value.reason == "unit_mismatch"
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Closed refusal-reason coverage
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
|
||||
def test_refuses_unknown_symbol() -> None:
|
||||
with pytest.raises(AdmissibilityError) as ei:
|
||||
check_admissibility(
|
||||
_eq(kind="add", deps=frozenset({"missing"})), symbols={}
|
||||
)
|
||||
assert ei.value.reason == "unknown_symbol"
|
||||
assert ei.value.detail == "missing"
|
||||
|
||||
|
||||
def test_refuses_unit_unbound_when_dep_symbol_has_no_unit() -> None:
|
||||
symbols = {"a": _sym("a", unit=None)}
|
||||
with pytest.raises(AdmissibilityError) as ei:
|
||||
check_admissibility(
|
||||
_eq(kind="add", deps=frozenset({"a"})), symbols=symbols
|
||||
)
|
||||
assert ei.value.reason == "unit_unbound"
|
||||
|
||||
|
||||
def test_refuses_unknown_unit_when_dep_unit_outside_vocab() -> None:
|
||||
symbols = {"a": _sym("a", unit="apples")}
|
||||
with pytest.raises(AdmissibilityError) as ei:
|
||||
check_admissibility(
|
||||
_eq(kind="add", deps=frozenset({"a"})), symbols=symbols
|
||||
)
|
||||
assert ei.value.reason == "unknown_unit"
|
||||
|
||||
|
||||
def test_refuses_unknown_operation_kind() -> None:
|
||||
eq = _eq(kind="bogus_kind", deps=frozenset())
|
||||
with pytest.raises(AdmissibilityError) as ei:
|
||||
check_admissibility(eq, symbols={})
|
||||
assert ei.value.reason == "unknown_operation"
|
||||
|
||||
|
||||
def test_check_admissibility_rejects_non_equation() -> None:
|
||||
with pytest.raises(TypeError):
|
||||
check_admissibility("not an equation", symbols={}) # type: ignore[arg-type]
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# UnitProof contract
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
|
||||
def test_unit_proof_to_canonical_string_has_kind_and_arrow() -> None:
|
||||
symbols = {"a": _sym("a", unit="dollar"), "b": _sym("b", unit="dollar")}
|
||||
proof = check_admissibility(
|
||||
_eq(kind="add", deps=frozenset({"a", "b"})), symbols=symbols
|
||||
)
|
||||
s = proof.to_canonical_string()
|
||||
assert s.startswith("add:")
|
||||
assert "->" in s
|
||||
assert "money" in s
|
||||
|
||||
|
||||
def test_unit_proof_is_frozen() -> None:
|
||||
symbols = {"a": _sym("a", unit="dollar")}
|
||||
proof = check_admissibility(
|
||||
_eq(kind="add", deps=frozenset({"a"})), symbols=symbols
|
||||
)
|
||||
import dataclasses
|
||||
|
||||
with pytest.raises(dataclasses.FrozenInstanceError):
|
||||
proof.lhs_unit = parse_unit("foot") # type: ignore[misc]
|
||||
|
||||
|
||||
def test_unit_proof_operand_units_preserved() -> None:
|
||||
symbols = {"a": _sym("a", unit="dollar"), "b": _sym("b", unit="dollar")}
|
||||
proof = check_admissibility(
|
||||
_eq(kind="add", deps=frozenset({"a", "b"})), symbols=symbols
|
||||
)
|
||||
assert len(proof.operand_units) == 2
|
||||
assert all(u == parse_unit("dollar") for u in proof.operand_units)
|
||||
|
||||
|
||||
def test_unit_proof_byte_equal_for_equivalent_inputs() -> None:
|
||||
symbols = {"a": _sym("a", unit="dollar"), "b": _sym("b", unit="dollar")}
|
||||
p1 = check_admissibility(
|
||||
_eq(kind="add", deps=frozenset({"a", "b"})), symbols=symbols
|
||||
)
|
||||
p2 = check_admissibility(
|
||||
_eq(kind="add", deps=frozenset({"a", "b"})), symbols=symbols
|
||||
)
|
||||
assert p1 == p2
|
||||
assert p1.to_canonical_string() == p2.to_canonical_string()
|
||||
|
||||
|
||||
def test_unit_proof_rejects_bad_construction() -> None:
|
||||
with pytest.raises(ValueError):
|
||||
UnitProof(operation_kind="", lhs_unit=parse_unit("foot"), operand_units=())
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Determinism
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
|
||||
def test_check_admissibility_deterministic_sorted_dep_iteration() -> None:
|
||||
# Same dep set in different insertion order → same proof.
|
||||
symbols = {"a": _sym("a", unit="dollar"), "b": _sym("b", unit="dollar")}
|
||||
p1 = check_admissibility(
|
||||
_eq(kind="add", deps=frozenset(["a", "b"])), symbols=symbols
|
||||
)
|
||||
p2 = check_admissibility(
|
||||
_eq(kind="add", deps=frozenset(["b", "a"])), symbols=symbols
|
||||
)
|
||||
assert p1 == p2
|
||||
|
||||
|
||||
def test_pack_composite_resolves_to_quotient_in_admissibility() -> None:
|
||||
# composite unit resolves through parse_unit; admissibility uses it.
|
||||
symbols = {
|
||||
"q_actor_hour_t0": _sym("q_actor_hour_t0", unit="hour"),
|
||||
"op_000__rate": _sym(
|
||||
"op_000__rate", unit="cent_per_hour", role="rate"
|
||||
),
|
||||
}
|
||||
proof = check_admissibility(
|
||||
_eq(
|
||||
kind="apply_rate",
|
||||
deps=frozenset({"q_actor_hour_t0", "op_000__rate"}),
|
||||
),
|
||||
symbols=symbols,
|
||||
)
|
||||
# cent ∈ units.money → lhs = money
|
||||
assert proof.lhs_unit == parse_unit("cent")
|
||||
280
tests/test_binding_graph_units.py
Normal file
280
tests/test_binding_graph_units.py
Normal file
|
|
@ -0,0 +1,280 @@
|
|||
"""ADR-0134 — Unit algebra primitives.
|
||||
|
||||
Pure algebra over the closed dimensional vocabulary in ``en_units_v1``.
|
||||
No I/O at call time; no coercion; refusal-first on unknown ids.
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
import pytest
|
||||
|
||||
from generate.binding_graph.units import (
|
||||
BASE_DIMENSIONS,
|
||||
DIMENSIONLESS,
|
||||
UnitAlgebraError,
|
||||
UnitVector,
|
||||
parse_unit,
|
||||
unit_inverse,
|
||||
unit_product,
|
||||
unit_quotient,
|
||||
units_equal,
|
||||
)
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# UnitVector construction
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
|
||||
def test_base_dimensions_are_load_bearing_closed_tuple() -> None:
|
||||
assert isinstance(BASE_DIMENSIONS, tuple)
|
||||
assert len(BASE_DIMENSIONS) == 6
|
||||
assert set(BASE_DIMENSIONS) == {
|
||||
"length",
|
||||
"time",
|
||||
"mass",
|
||||
"money",
|
||||
"count",
|
||||
"temperature",
|
||||
}
|
||||
|
||||
|
||||
def test_dimensionless_is_all_zero() -> None:
|
||||
assert DIMENSIONLESS.exponents == (0, 0, 0, 0, 0, 0)
|
||||
|
||||
|
||||
def test_unit_vector_requires_tuple() -> None:
|
||||
with pytest.raises(UnitAlgebraError):
|
||||
UnitVector(exponents=[1, 0, 0, 0, 0, 0]) # type: ignore[arg-type]
|
||||
|
||||
|
||||
def test_unit_vector_requires_correct_arity() -> None:
|
||||
with pytest.raises(UnitAlgebraError):
|
||||
UnitVector(exponents=(1, 0, 0))
|
||||
|
||||
|
||||
def test_unit_vector_rejects_non_int_exponents() -> None:
|
||||
with pytest.raises(UnitAlgebraError):
|
||||
UnitVector(exponents=(1.0, 0, 0, 0, 0, 0)) # type: ignore[arg-type]
|
||||
|
||||
|
||||
def test_unit_vector_rejects_bool_exponents() -> None:
|
||||
with pytest.raises(UnitAlgebraError):
|
||||
UnitVector(exponents=(True, 0, 0, 0, 0, 0)) # type: ignore[arg-type]
|
||||
|
||||
|
||||
def test_unit_vector_is_frozen() -> None:
|
||||
v = UnitVector(exponents=(1, 0, 0, 0, 0, 0))
|
||||
with pytest.raises(Exception):
|
||||
v.exponents = (0, 0, 0, 0, 0, 0) # type: ignore[misc]
|
||||
|
||||
|
||||
def test_unit_vector_canonical_string_dimensionless() -> None:
|
||||
assert DIMENSIONLESS.to_canonical_string() == "dimensionless"
|
||||
|
||||
|
||||
def test_unit_vector_canonical_string_simple_numerator() -> None:
|
||||
assert parse_unit("foot").to_canonical_string() == "length"
|
||||
|
||||
|
||||
def test_unit_vector_canonical_string_squared() -> None:
|
||||
assert parse_unit("square_foot").to_canonical_string() == "length^2"
|
||||
|
||||
|
||||
def test_unit_vector_canonical_string_quotient() -> None:
|
||||
assert parse_unit("mile_per_hour").to_canonical_string() == "length/time"
|
||||
|
||||
|
||||
def test_unit_vector_canonical_string_inverse_only() -> None:
|
||||
inv = unit_inverse(parse_unit("hour"))
|
||||
assert inv.to_canonical_string() == "1/time"
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# parse_unit
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
|
||||
def test_parse_unit_exact_pack_lemma_money() -> None:
|
||||
assert parse_unit("dollar").exponents == (0, 0, 0, 1, 0, 0)
|
||||
|
||||
|
||||
def test_parse_unit_exact_pack_lemma_length() -> None:
|
||||
assert parse_unit("foot").exponents == (1, 0, 0, 0, 0, 0)
|
||||
|
||||
|
||||
def test_parse_unit_exact_pack_lemma_mass() -> None:
|
||||
assert parse_unit("pound").exponents == (0, 0, 1, 0, 0, 0)
|
||||
|
||||
|
||||
def test_parse_unit_exact_pack_lemma_count() -> None:
|
||||
assert parse_unit("item").exponents == (0, 0, 0, 0, 1, 0)
|
||||
|
||||
|
||||
def test_parse_unit_exact_pack_lemma_temperature() -> None:
|
||||
assert parse_unit("Celsius").exponents == (0, 0, 0, 0, 0, 1)
|
||||
|
||||
|
||||
def test_parse_unit_derived_speed() -> None:
|
||||
assert parse_unit("mile_per_hour").exponents == (1, -1, 0, 0, 0, 0)
|
||||
|
||||
|
||||
def test_parse_unit_derived_wage() -> None:
|
||||
assert parse_unit("dollar_per_hour").exponents == (0, -1, 0, 1, 0, 0)
|
||||
|
||||
|
||||
def test_parse_unit_depluralize_s() -> None:
|
||||
assert units_equal(parse_unit("dollars"), parse_unit("dollar"))
|
||||
|
||||
|
||||
def test_parse_unit_depluralize_es() -> None:
|
||||
# 'inches' → 'inch'
|
||||
assert units_equal(parse_unit("inches"), parse_unit("inch"))
|
||||
|
||||
|
||||
def test_parse_unit_depluralize_ies() -> None:
|
||||
# 'centuries' → 'century'
|
||||
assert units_equal(parse_unit("centuries"), parse_unit("century"))
|
||||
|
||||
|
||||
def test_parse_unit_dimensionless_symbol() -> None:
|
||||
# Pack 'units.symbol' lemmas (e.g., 'percent') are dimensionless.
|
||||
assert units_equal(parse_unit("percent"), DIMENSIONLESS)
|
||||
|
||||
|
||||
def test_parse_unit_container_is_count_dim() -> None:
|
||||
assert parse_unit("dozen").exponents == (0, 0, 0, 0, 1, 0)
|
||||
|
||||
|
||||
def test_parse_unit_composite_decomposes() -> None:
|
||||
# foot_per_second → length/time
|
||||
assert parse_unit("foot_per_second").exponents == (1, -1, 0, 0, 0, 0)
|
||||
|
||||
|
||||
def test_parse_unit_composite_with_unknown_inner_refuses() -> None:
|
||||
with pytest.raises(UnitAlgebraError) as ei:
|
||||
parse_unit("dollar_per_apple")
|
||||
assert "unknown_unit" in str(ei.value)
|
||||
|
||||
|
||||
def test_parse_unit_unknown_refuses() -> None:
|
||||
with pytest.raises(UnitAlgebraError) as ei:
|
||||
parse_unit("apples")
|
||||
assert "unknown_unit" in str(ei.value)
|
||||
|
||||
|
||||
def test_parse_unit_unknown_widgets_refuses() -> None:
|
||||
with pytest.raises(UnitAlgebraError):
|
||||
parse_unit("widgets")
|
||||
|
||||
|
||||
def test_parse_unit_empty_string_refuses() -> None:
|
||||
with pytest.raises(UnitAlgebraError):
|
||||
parse_unit("")
|
||||
|
||||
|
||||
def test_parse_unit_non_string_refuses() -> None:
|
||||
with pytest.raises(UnitAlgebraError):
|
||||
parse_unit(None) # type: ignore[arg-type]
|
||||
|
||||
|
||||
def test_parse_unit_rate_connector_not_a_unit() -> None:
|
||||
# 'per' is a connector in units.rate; refuse rather than treat as a unit.
|
||||
with pytest.raises(UnitAlgebraError):
|
||||
parse_unit("per")
|
||||
|
||||
|
||||
def test_parse_unit_dimension_header_not_a_unit() -> None:
|
||||
# 'length' is a dimension header; the lemma is in units.dimension and
|
||||
# must be rejected — only concrete units resolve.
|
||||
with pytest.raises(UnitAlgebraError):
|
||||
parse_unit("length")
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Algebra primitives
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
|
||||
def test_unit_product_commutes() -> None:
|
||||
a, b = parse_unit("foot"), parse_unit("hour")
|
||||
assert unit_product(a, b).exponents == unit_product(b, a).exponents
|
||||
|
||||
|
||||
def test_unit_product_byte_equal_swap() -> None:
|
||||
a, b = parse_unit("foot"), parse_unit("hour")
|
||||
assert unit_product(a, b) == unit_product(b, a)
|
||||
|
||||
|
||||
def test_unit_product_squares_length() -> None:
|
||||
foot = parse_unit("foot")
|
||||
assert unit_product(foot, foot).exponents == (2, 0, 0, 0, 0, 0)
|
||||
|
||||
|
||||
def test_unit_quotient_speed() -> None:
|
||||
# foot / second = speed (length/time)
|
||||
q = unit_quotient(parse_unit("foot"), parse_unit("second"))
|
||||
assert q.exponents == (1, -1, 0, 0, 0, 0)
|
||||
|
||||
|
||||
def test_unit_quotient_not_commutative() -> None:
|
||||
a, b = parse_unit("foot"), parse_unit("hour")
|
||||
assert unit_quotient(a, b).exponents != unit_quotient(b, a).exponents
|
||||
|
||||
|
||||
def test_unit_inverse_of_inverse_is_identity() -> None:
|
||||
v = parse_unit("dollar_per_hour")
|
||||
assert unit_inverse(unit_inverse(v)) == v
|
||||
|
||||
|
||||
def test_unit_inverse_of_dimensionless_is_dimensionless() -> None:
|
||||
assert unit_inverse(DIMENSIONLESS) == DIMENSIONLESS
|
||||
|
||||
|
||||
def test_unit_quotient_self_is_dimensionless() -> None:
|
||||
foot = parse_unit("foot")
|
||||
assert unit_quotient(foot, foot) == DIMENSIONLESS
|
||||
|
||||
|
||||
def test_unit_product_with_dimensionless_is_identity() -> None:
|
||||
foot = parse_unit("foot")
|
||||
assert unit_product(foot, DIMENSIONLESS) == foot
|
||||
|
||||
|
||||
def test_units_equal_reflexive() -> None:
|
||||
foot = parse_unit("foot")
|
||||
assert units_equal(foot, foot)
|
||||
|
||||
|
||||
def test_units_equal_strict_on_dimensions() -> None:
|
||||
assert not units_equal(parse_unit("foot"), parse_unit("hour"))
|
||||
|
||||
|
||||
def test_units_equal_strict_on_exponent_magnitude() -> None:
|
||||
foot = parse_unit("foot")
|
||||
sq = unit_product(foot, foot)
|
||||
assert not units_equal(foot, sq)
|
||||
|
||||
|
||||
def test_unit_algebra_no_io_at_call_time(tmp_path, monkeypatch) -> None:
|
||||
# After first call the pack lexicon is memoized; subsequent calls must
|
||||
# not touch the filesystem. Smoke this by pointing the resolver path at
|
||||
# an invalid location post-warmup; calls must still succeed.
|
||||
import generate.binding_graph.units as U
|
||||
|
||||
_ = parse_unit("foot") # warm cache
|
||||
monkeypatch.setattr(U, "_UNITS_PACK_LEXICON", tmp_path / "missing.jsonl")
|
||||
# Cached table is still in use.
|
||||
assert parse_unit("foot").exponents == (1, 0, 0, 0, 0, 0)
|
||||
|
||||
|
||||
def test_parse_unit_idempotent_across_repeat_calls() -> None:
|
||||
a = parse_unit("dollar_per_hour")
|
||||
b = parse_unit("dollar_per_hour")
|
||||
assert a == b
|
||||
assert a.exponents == b.exponents
|
||||
|
||||
|
||||
def test_unit_vector_is_hashable() -> None:
|
||||
# Frozen dataclasses are hashable by default; the binding graph relies
|
||||
# on this when comparing UnitProof tuples.
|
||||
assert hash(parse_unit("foot")) == hash(parse_unit("foot"))
|
||||
Loading…
Reference in a new issue