Expand description
The enumeration reference driver (docs/07-repair-drivers.md §4) and the
candidates helper (docs/06-repair.md §3.3).
This is the simplest driver: it walks the RepairTree’s finite choices —
Any branches, Repeat counts, and per-hole candidate terms drawn from the
data graph (reuse) or minted fresh — and returns the first plan whose ΔG
passes the gate. It is primarily a correctness check on the
IR and the gate; it cannot invent novel literals (those holes are filled only
by reuse).
Like every driver, it decides nothing the library doesn’t expose: it only
composes [instantiate], candidates, and gate.
Structs§
- Enum
Options - Knobs for the enumeration search.
- Fixpoint
Result - The outcome of repairing a graph to a fixpoint.
- Repair
Solution - A repair the enumeration driver found and verified.
Functions§
- candidates
- Existing terms in
datathat satisfy a hole’s constraint, plus a fresh node where minting is allowed — truncated tocap. The contract places no requirement on where a binding comes from; this is the reuse-first default. - enumerate_
repair - Search for the first sound, progress-making repair of
tree. Reuse candidates are drawn fromdata, while gating is evaluated againstcontext(which should containdata; passdataagain when there is no separate shapes graph) — so a candidate typed with a subclass of a required class clears the gate. The enumeration dual ofcrate::validate_with_context. - repair_
to_ fixpoint - The reference fixpoint driver (
docs/07-repair-drivers.md§1): witness → synthesize → enumerate → gate → apply, re-witnessing after each accepted repair until the graph conforms or no focus admits a sound, progress-making repair. Each acceptedΔGis gated (introduces nothing) and strictly reduces the violation count, so the loop terminates.