Module repeat 

Repeating a step until it says it is done: the driver of every loop that runs until a condition holds — a worklist rewritten until nothing is left to rewrite (the next split, merge or imprint found and made, until none is found), a march stepped on until it arrives or leaves, passes over a list until one changes nothing.

What a step does, and when the work is done, are the caller’s. The solver promises the bound: at most most steps, each taken once and in order, and an explicit Repeated::Exhausted when every one of them was taken and none said it was done. Running out is never read as done: a caller that can do nothing else with an unfinished run says so with Repeated::done or Repeated::done_or.

repeat is the driver; rewrite is its worklist form (find the next rewrite, make it, search again), and resolve its form for passes over a list, which needs no budget: it ends by its own count.

Enums

Repeated

How a run of steps ended.

Step

What one step said.

Functions

repeat

Takes step until it says Step::Done, at most most times. step keeps the state of the work itself, since every step is taken once, in order.

resolve

Resolves items in passes, each trying every item still unresolved, in order, until all are or a pass resolves none: what is left then never will be, and comes back, in order, with what its last try said. A try may depend on what the tries before it resolved, in this pass or an earlier one — that is what a later pass is for. Every pass but the last resolves one item at least, so it ends after as many passes as there are items, and one more.

rewrite

Rewrites state until nothing is left to rewrite: find looks for the next rewrite in it, apply makes the one found, and the search starts over from the state that leaves — a rewrite changes what there is to find. At most most searches, the last of which, in a run that is done, finds nothing; done with how many rewrites were made.