Uniquify all Sprite preterms in separate step prior elaboration

[janvrany]

Yet another attempt to fix #139.

This PR α-renames all variables in a separate step prior elaboration.
It is similar to PR #197 but differ in several ways:

• perform renaming as a separate step, not as part of [Chk-Lam].
• renames all lets, not just function parameter binds
• renames everything in single top-down traversal.

[shingarov]

I wonder if this can be somehow integrated with AlphaRenamer. Which leads us to further zoom in attention to things like #194 , which is just one manifestation of a more general issue, that in the upstream Sprite, there is a hierarchy of Exprs parallel to that in Fixpoint. For example, there are EVar and EApp etc in Fixpoint, and there are EVar and EApp etc in Sprite (and in the Sprite namespace the former are called F.EVar etc because of import qualified Language.Fixpoint.Types as F). Actually it's even worse: in Fixpoint itself there is duplication between the "fixpoint names" (F.*) and "horn names" (H.*). In addition to datatype names, there is similar duplication of function names.

In Smalltalk, most of the time we follow the convention that if some a is duplicated in Sprite and Fixpoint, the Fixpoint thing (F.a) is called a in Smalltalk, and the Sprite a is called Λa in Smalltalk. See, for example, Object>>predReft, or SInfo>>eliminatingSolverInfo.

But sometimes it's too unbearable to lug all this parallelism through the whole codebase. There is, for example, PInt ("literal integer constant"). I just don't bother distinguishing between the Sprite and the Fixpoint PInt. One day a hero will be born who will clean all this mess.

[janvrany]

I wonder if this can be somehow integrated with AlphaRenamer.

I was thinking the same but after digging deeper I decided not to, not now anyways. It seemed more than I could chew.

One day a hero will be born who will clean all this mess.

Yeah, and hopefully soon else a mere hero won't suffice. And gods are even scarcer to come by than heroes.

[janvrany]

Closing as resolved via 3ac081f and #283