Update Hashable Term instance so alphaEquiv t1 t2 implies hash t1 == hash t2

[m-yac]

The Hashable class requires that if two elements are equal, then they have the same hash. I noticed that the current Hashable instance for Term did not satisfy this in two ways:

1. Variable names: Lambda "x" t u would have a different hash than Lambda "y" t u, even though they are equal (since equality of Terms is alphaEquiv)
2. STApp vs. Unshared: STApp { stAppTermF = t } would have a different hash than Unshared t, even though they are equal (since, as above, equality of Terms is alphaEquiv, and alphaEquiv does not differentiate between the two constructors if they have equal TermF representations)

This PR resolves both of these issues: the first by defining a manual Hashable (TermF e) instance, and the second by removing the combine 0x00000000 and combine 0x55555555 parts of the Hashable Term instance which differentiated the STApp and Unshared constructors.

I noticed that some of this was already discussed in #1830 – in particular Andrei left a comment with an optimization to alphaEquiv that can be made if the first change above was implemented. Since I did the latter, I included that optimization.

[RyanGlScott]

Consider adding some unit tests for the properties you are trying to establish in the saw-core test suite.

[m-yac]

Thanks for the comments @RyanGlScott! I added some more commentary in the places you asked – let me know if you think more would be better, or if I need to clarify something.

I will definitely add some unit tests when I get a chance.

[samcowger]

I've just noticed that Eq on TermF es is not implemented in terms of alpha equivalence, it's merely derived. Do you think that's worth changing in this PR, so that equivalence of Terms and TermF es is more unified?

[eddywestbrook]

I've just noticed that Eq on TermF es is not implemented in terms of alpha equivalence, it's merely derived. Do you think that's worth changing in this PR, so that equivalence of Terms and TermF es is more unified?

Ooh, good catch! Yes, Eq on TermF should use alphaEquiv. It looks like the way alphaEquiv is defined in fact defines local equality functions for TermF and FlatTermF, but doesn't export them as the equality functions for those types. That should be fixed.

Also, 100% yes to @RyanGlScott's suggestion! Please add tests for these properties!