When using quickspec to find laws useful for optimization, it's helpful to look for laws only of a particular shape.
For example, my both function grows quickly in the size of its argument. I'd like to be able to find ways of distributing other combinators through it. Quickspec will happily find lots of laws for both:
...
22. choose x (both y (star y)) = both (star y) (choose x y)
23. both (char x) (lookahead (char y)) = both (char x) (char y)
24. star (both x (star (char y))) = star (both x (optional (char y)))
25. both (cat x y) (cat x z) = cat x (both y z)
26. both (cat x x) (cat y x) = cat (both x y) x
27. both (cat x y) (choose z y) = both (optional z) (cat x y)
28. choose (both x y) (both x z) = both x (choose y z)
29. both x (cat (both x y) z) = cat (both x y) z
...
of particular interest here are 23 and 25 because they simplify arguments to both. Unfortunately, they are awash in a million other laws for both, which makes it hard to skim for these ones.
I'd be amazing to have a way to have QuickSpec help me find laws like these more easily.
When using quickspec to find laws useful for optimization, it's helpful to look for laws only of a particular shape.
For example, my
bothfunction grows quickly in the size of its argument. I'd like to be able to find ways of distributing other combinators through it. Quickspec will happily find lots of laws forboth:of particular interest here are 23 and 25 because they simplify arguments to
both. Unfortunately, they are awash in a million other laws forboth, which makes it hard to skim for these ones.I'd be amazing to have a way to have QuickSpec help me find laws like these more easily.