Notes on the predecessor function

[elegios]

Two approaches, broadly speaking:

• Precompute all the predecessor lists (a 2d matrix, indexed by the int repr of a state). Presumably type Int[][|state|] (where |state| is the number of values in the type state).
• Pass around a buffer that is filled at runtime with the predecessors of a single state.

Both approaches need to deal with different states having different numbers of predecessors, one way or another.

Both approaches can use the following basic approach when working with set builder notation:

• Find all unknown variables in the patterns.
• Check all possible combinations of values for those variables.
• Filter by the predicates.

We believe that non-linear patterns are beneficial for reading and probably also make the simple implementation more efficient. E.g.:
[a, as..., ] -> [as..., b, ] is ok and means that the same (sub-)sequence appears on both sides. Alternatively we could try handling = predicates, since they cut down the search space drastically. We still don't like using previously bound things in patterns, e.g.,

let foo = 42
[foo, 2] -> [1, 1]

should shadow foo (probably with a warning).

Both approaches (though especially the runtime one) could probably benefit from interfacing with an SMT solver. Ideally we'd ask, at compile time, what values could possibly satisfy the predicates, so we only have to range over those. In some of the cases we have this should cut the number of values to check from 16 (per state) to 1. For the static approach this likely only helps with time/space taken to compile a model but the runtime version would have significantly less work to do.

The runtime version still needs a max number of predecessors, to pre-allocate the buffer, and the easiest way to obtain this is to just precompute all the predecessor sets, thus we think it's better to start with the static approach and maybe do something better later.

It's possible that the approaches could be mixed, some transitions are pre-computed and put in lists and some computed at runtime, with a (ideally simple) check for which transition we're currently considering. Deciding between these could be decision points.