Optimize Elaboration

[vrindisbacher]

@ranjitjhala, this one is from the liquid-fixpoint origin but has the same changes as #735

(copying over notes)

A few changes are implemented here:

• Delaying use of applyExpr in elab until after all the elaboration has taken place.
• Separate type Visitor and type Folder into two separate structures.
• Additionally, ditch using the State monad for folding and replace it with the Reader monad - similar to what is implemented for CheckM
• Ripping out a redundant unifyExpr. This seemed to be re-traversing the expression tree and creating type substitutions by unifying sorts that were already unified in elabEAppSort.

[RJ: All of these together yield massive speedups for some flux benchmarks]

[ranjitjhala]

Thanks @vrindisbacher -- seems to give some nice improvements in the LH benchmarks too!

[vrindisbacher]

Awesome!