DiscrTree-accelerated pattern matching

Stream: metaprogramming / tactics

[Geoffrey Irving]

Say I have a large number of (pattern, function) pairs, something like [(Q($a + $b), fun a b => …), (Q(exp $z), fun z => …)]. If the list is known, one could write this as an explicit pattern match. What’s the right way to do if I have a large number of (pattern, function) pairs constructed programmatically, and want DiscrTree acceleration?

[Jovan Gerbscheid]

You can make a discrimination tree where you index the patterns (with the variables as metavariables). Then when matching with some expression, you look up the expression in the discrimination tree, which gives you a short list of candidates. And then you check each of those candidates in the usual way with unification. You could use my RefinedDiscrTree, but I presume that the patterns are going to be quite simple, so then the default DiscrTree should do the job just as well.

[Jovan Gerbscheid]

If the patterns have a particular order in which they need to be tried, then you should be careful to remember for each pattern what the index is, so that you can put them back in the original order after the DiscrTree lookup.

[Geoffrey Irving]

Thanks, that makes sense!