For the curious, this was an attempt to change the way context
matching works. Currently, when matching a pattern, if 'hole' is
encountered, the match succeeds and the result just includes the term
at that point. This means that when matching (in-hole p1 p2), p1
generally returns multiple results and then those results are thinned
out by matching p2 against the thing actually at the hole.
Instead, one could pass along the function that does the matching and
then, when matching a hole pattern, it could decide right at that
point whether or not the match works.
This seems like it would be a win overall, but it interferes with
caching. Specifically, most reduction systems have lots of rules
that all begin
(--> (in-hole E ...) ...)
and, in the strategy first described above, that matching can be cached.
But in the second, it cannot. Overall, this turns out to be a slight
lose in the current version of Redex. Maybe if other things change, however,
this tradeoff will change.
Revert "IN PROGRESS: more context speedup attempt"
This reverts commit 0134b8753d.
Revert "IN PROGRESS: a possible speed up attempt; match the thing in the hole before returning the context matches instead of afterwards"
This reverts commit 11059e2b5c.
b068d9583c