Refactoring incremental homomorphism search #84
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Conceptually cleaner implementation of incremental hom search. Furthermore, this introduces a data structure
IHS
to manage multiple patterns, multiple rules, and multiple states being tracked. This also generalizes the previous implementation by being able to handle non-monic matches appropriately.There are two algorithms: one based purely on the structure of an adhesive category and another (more efficient) that presumes one has complements. C-Sets do have complements, so we definitely want to have the latter, but the former is important to support to. In the case of a single rewrite, the relation between these two approaches is clear and we can have just one algorithm (with a special optimization built in). It still remains how to view the batch algorithm with complements as a special case/optimization of the adhesive batch algorithm. The code would become much simpler if we could do this.
TODO
Before merging, it will be useful to support: