Persistent structure-based term identifiers

[samcowger]

This adds a field to STApp-constructed Terms to store the hash of the TermF they encompass, giving shared terms a readily-available, (relatively) unique identifier based solely on the shape/structure of their subterms. The goal of this is to provide terms with a persistent, concise reference that does not change between SAW invocations.

In doing this, I changed the Hashable and Eq instances to leverage this field. Before, Hashable was implemented solely in terms of stAppIndex, which was basically guaranteed unique for any single SAW invocation. Now, Hashable is implemented solely in terms of this stored hash. This slightly increases the possibility of term hash collisions, but I believe the likelihood of collisions is no worse than that of automatically-derived instances. RFC: should we now handwrite a Hashable instance for TermF to mitigate this risk somewhat?

One use case for this (which this PR does not implement, but which a future PR will) is to allow users to print terms with memoization based on these references, rather than based on mercurially-unique integer tags. This would help users to maintain context in larger, heavily-memoized terms (e.g. a proof goal) as users enter and exit SAW REPLs and proof subshells in the process of proof development.

[samcowger]

One alternative to the approach implemented here, if there is substantial concern about changing the Hashable instance, would be to define a parallel class, say Hashable', whose only purpose would be to provide a structure-based hash in tandem with the current index-based hash, and implement it on the Term and its subordinate types. We would still need to modify the representation of STApp Terms to cache this hash, but could otherwise leave the Hashable and Eq instances unchanged.

[eddywestbrook]

While you are changing the Term datatype, please add a haddock description to it to explain the design concepts associated with it, including: that the STApp constructor implements hash-consing (maybe put a pointer to Wikipedia or something to explain the concept?) using the stAppIndex field; that the stAppIndex field is always meant to be unique; that the stAppTermF field "ties the knot" for the TermF data-type (it would be great if you could dig up a reference for this style of datatype functor, but it's fine if you can't); and that the stAppHash and stAppFreeVars fields cache the free variables and hash values of the term.

[samcowger]

While you are changing the Term datatype, please add a haddock description to it to explain the design concepts associated with it, including: that the STApp constructor implements hash-consing (maybe put a pointer to Wikipedia or something to explain the concept?) using the stAppIndex field; that the stAppIndex field is always meant to be unique; that the stAppTermF field "ties the knot" for the TermF data-type (it would be great if you could dig up a reference for this style of datatype functor, but it's fine if you can't); and that the stAppHash and stAppFreeVars fields cache the free variables and hash values of the term.

Can do!

[eddywestbrook]

Excellent, thanks for adding those haddocks!