Skip to main content

Module enumerate

Module enumerate 

Source
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§

EnumOptions
Knobs for the enumeration search.
FixpointResult
The outcome of repairing a graph to a fixpoint.
RepairSolution
A repair the enumeration driver found and verified.

Functions§

candidates
Existing terms in data that satisfy a hole’s constraint, plus a fresh node where minting is allowed — truncated to cap. 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 from data, while gating is evaluated against context (which should contain data; pass data again when there is no separate shapes graph) — so a candidate typed with a subclass of a required class clears the gate. The enumeration dual of crate::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 ΔG is gated (introduces nothing) and strictly reduces the violation count, so the loop terminates.