idris-lang/Idris-dev — pull request #1507 by bmsherman (2014-09-02 00:28:39+00:00)
Title: Symmetry of equality (and small fix) for :search

I've made three relatively orthogonal changes to the :search code:

- I've added "flipping of equality" as another "edit" that can be made in :search. For example, the type of `plusAssociative`,
```Idris
left + (centre + right) = (left + centre) + right
```
can be modified to
```Idris
(left + centre) + right = left + (centre + right)
```
so you can search either way and still get the result. There is a small penalty for this change, so even in the case that there are two types which differ only in the flipping of the equality, the non-flipped type will be shown first. This addresses issue https://github.com/idris-lang/Idris-dev/issues/1350.

- I've fixed a small error in :search that's been present for a while. It took me a while to discover this error, because the error was usually producing the right results! (for the wrong reasons...). So I have removed a cause of spurious results.

- I've refactored the code. Most of the code is involved with matching two types: I think of them as the left-hand and right-hand side. In a lot of cases, I had duplicated code for the "left-hand" case and "right-hand" case. I've tried to clean up the code to allow that pattern to be abstracted out. So there's less code duplication, and the code is somewhat cleaner as well. I've also tried to reduce the amount of name shadowing.