Binary to apply search patterns to disjunction of configurations

[dwightguth]

Right now, the llvm backend is capable of search if you don't specify any search pattern. However, it is a nontrivial effort to make a tool to deal with search patterns on the llvm backend because the search patterns are dynamically generated by user input after the semantics has been installed on the machine, but currently the only way to match a pattern in the llvm backend is to compile some code to do it.

Since this step ought not to take very much time, being pure matching with no function evaluation or rewrite steps, I propose that we get the haskell backend to perform this step, similar to how the haskell backend makes use of binaries generated by the llvm backend in order to do unparsing.

What we need is a tool that takes as input:

1. A disjunction of concrete terms
2. A search pattern in the same format that the haskell backend normally receives search patterns

And produces as output a disjunction of conjunctions, #Bottom, or #Top, depending on circumstances, where the result is a disjunction of substitutions of the variables in the search pattern, in the same format that the haskell backend normally outputs when performing a search.

This isn't very high priority and isn't blocking anything (in particular it's lower priority than the iele lto packaging issue), but it is required to mark some parts of the k grant as completed.

[ana-pantilie]

@dwightguth Do you have any input examples for this tool?