search

nick8325 / quickspec

Equational laws for free
BSD 3-Clause "New" or "Revised" License
250 stars 24 forks source link

Feature request: "what does this equal?" mode #59

Open isovector opened 4 years ago

isovector commented 4 years ago

I'm looking for optimizations for a certain expensive term in my program. It'd be great if I could ask QuickSpec to generate terms as usual and tell me if any of them are equal to this thing.

Eg, my expensive term is both (gate ef1 g1) (gate ef2 g2), so I'd like to be able to add something to the signature like:

searchFor $ \ef1 g1 ef2 g2 -> both (gate ef1 g1) (gate ef2 g2)

such that the only things QS reports are equivalent expressions.

isovector commented 4 years ago

Right now I approximate this by putting everything in series, and then afterwards add an equivalent constructor for this. This has a few problems; one of which is that it spends most of its time finding laws in the background that I don't care about, and then usually such equivalent terms are not small.