feat(incremental): the Derived trait, Eager and the differential harness (improvise-t8ow)
Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze
This commit is contained in:
committed by
Edward Langley
parent
069d56bd9f
commit
c0e6bd8f33
@@ -0,0 +1,74 @@
|
||||
# `improvise-incremental`: the reasoning
|
||||
|
||||
`crates/improvise-incremental` is ADR 009 step 2 (improvise-t8ow, epic improvise-bw4p): the
|
||||
plug. It holds the `Derived` trait, `Eager` (today's evaluator behind it) and the
|
||||
differential harness every later backend is checked with. There is no incremental backend
|
||||
here, the evaluator is untouched and no existing crate changed. The decisions are the ADR's
|
||||
(`context/adr/009-incremental-evaluation.md`, clause 2). The evidence for each test is in
|
||||
`context/test-evidence/improvise-incremental.md`.
|
||||
|
||||
## The shape
|
||||
|
||||
| item | what it is |
|
||||
|---|---|
|
||||
| `Derived` | the two things the evaluator reads: `value(key, agg)` and `raw_fold(partial)` |
|
||||
| `Eager` | an owned `Model` plus its None categories; every answer is a call into `Model` |
|
||||
| `Maintained` | a `Derived` that is told each `Edit`; `Eager` is one |
|
||||
| `Edit` | one model mutation as data (set, clear, add or remove a formula, set a measure's aggregation) |
|
||||
| `probes`, `Probe` | every question worth asking of a model, and a way to put it to any backend |
|
||||
| `differential` | runs one edit sequence on a candidate and on `Eager`, comparing every probe at every step |
|
||||
| `Divergence`, `Report` | what a failure names (step, probe, both answers) and what a pass compared |
|
||||
|
||||
## Interpretations
|
||||
|
||||
Clause 2 names the trait and says what it carries ("the formula result at a key, and the raw
|
||||
fold of the cells that match a partial key") and nothing else. These are the readings taken.
|
||||
|
||||
1. **`Derived` lives in this crate, not in improvise-core.** The ADR says improvise-core
|
||||
"gains a trait". Putting it there changes an existing crate's source, which this step does
|
||||
not do. Nothing is lost: the seam crate depends on core and core never on `zset`, which is
|
||||
the clause's actual constraint. Moving the trait into core, when the evaluator is made to
|
||||
read through it, is a move of one file.
|
||||
2. **Two methods, the minimum.** `value(key, agg)` is the formula result at a key, or the cell
|
||||
as stored or folded; `raw_fold(partial)` is the fold of matching stored cells. `agg` is
|
||||
`Aggregation`, the evaluator's own type, because exact and over-hidden reads differ and
|
||||
the harness must be able to ask both. Collapsed-group `covers`, totals and occupancy are
|
||||
not in the trait: nothing reads them through it yet, and a method with no caller is
|
||||
designed blind. The ADR's differential test compares "every drawn cell, total and occupancy
|
||||
count"; those enter with the steps that maintain them.
|
||||
3. **`Eager::raw_fold` is `evaluate_aggregated(partial, OverHidden)`.** The evaluator's raw
|
||||
fold (`aggregate_raw`, `aggregate_cell_values`) is private to core, and wrapping without
|
||||
editing core leaves the public path. The two agree for a partial that names no formula
|
||||
target and no collapsed group, which is what the harness probes. For a partial that does
|
||||
name a formula target the cache answers instead, so `raw_fold` is not "never a formula"
|
||||
there. Step 3 should expose the raw fold from core when it moves the evaluator behind the
|
||||
trait, and `Eager` should call that.
|
||||
4. **`Eager` recomputes formulas after every edit.** Production does it in `rebuild_layout`
|
||||
(`Model::recompute_formulas(none_cats)`), and an over-hidden read of a formula cell reads
|
||||
the cache it fills. So `Eager` carries the None categories of the view it stands for and
|
||||
recomputes under them after each edit, as a layout rebuild does.
|
||||
5. **`Edit` is the vocabulary of the harness, not of the wire.** Five variants, each one
|
||||
public `Model` call. A later step adds variants for what it maintains (an item added, a
|
||||
category removed); the harness does not care which.
|
||||
6. **Values agree by float rules with every NaN one value** (`same_value`), the rule clause 3
|
||||
states for cell deltas. A NaN answer is not a divergence from itself. Signed zero compares
|
||||
equal, so a later `ExactSum` cannot be told from eager's sum by the sign of a zero here;
|
||||
clause 8 has its own property test for that.
|
||||
7. **No `zset` dependency yet.** The brief and the ADR name it, but nothing in this step uses
|
||||
a Z-set, and an unused dependency is noise. It arrives with the first backend, as the
|
||||
cell delta of step 3.
|
||||
|
||||
## What the harness checks
|
||||
|
||||
`differential(model, none_cats, candidate, edits)` builds `Eager` over a clone of the model,
|
||||
applies each edit to both, and after step 0 and after every edit asks both every probe. A
|
||||
probe set is derived from the post-edit model: each stored key, each partial of one and each
|
||||
formula cell over them under both aggregations, plus the raw fold of every partial. The key an
|
||||
edit names is probed too, so a cleared cell is asked about after it is gone. The first
|
||||
disagreement is returned as a `Divergence` whose message reads
|
||||
`divergence at step N: <probe>: eager <a> != candidate <b>`. A pass returns a `Report` of how
|
||||
many states and answers were compared, so a run that compared nothing shows as zero.
|
||||
|
||||
The corpus the tests use is `examples/demo.improv` and `web/demo.improv`, loaded through
|
||||
`improvise_io::persistence::load`, every view's None categories in turn, plus a hand-built
|
||||
model with formulas, text and mixed values.
|
||||
Reference in New Issue
Block a user