Make the Bind iterator for AND goals fair develop
authorCassie Jones <code@witchoflight.com>
Mon, 17 Feb 2020 16:52:12 +0000 (17:52 +0100)
committerCassie Jones <code@witchoflight.com>
Mon, 17 Feb 2020 16:58:58 +0000 (17:58 +0100)
commit5d75f416c773f9371bbdfb1f91292b84dbc183c2
tree5e22095197ef314f96be0eba54a64a2f5b0e0125
parentf6eb4b2e9c660fbb8293ad9d6ea83a0c1fa7868c
Make the Bind iterator for AND goals fair

Given and(goal_a, goal_b), previously if goal_b could produce an
infinite number of solutions, then goal_a wouldn't get a chance to move
on the to previous. It was doing a sort of dependent Cartesian product
where it would take one step on goal_a in order to find the context for
goal_b, and then completely exhaust goal_b in that context.

Now, we do a diagonal search, keeping a vector of searches in goal_b,
and asking goal_a for a new context each time we loop back around to the
beginning. If goal_a is exhausted, we stop adding new searches, and if
any of the searches in goal_b is exhausted, we remove it from the list
of searches to iterate over.

Some specific things to note: we respect yields in goal_a, so that a
diverging goal_a doesn't get stuck and instead will repeatedly yield,
letting the rest of the program continue its search, interleaved
elsewhere.

This changes performance, making the large Peano addition slower.
src/lib.rs
src/main.rs