Delay applyExpr until after elaboration

[vrindisbacher]

There are a few changes I'm hoping to implement here. There are:

1. delaying use of applyExpr in elab until after all the elaboration has taken place.
2. delaying use of apply in elab until after all the elaboration has taken place - hoping to use union find to do this. See the PoC implementation here.
3. 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

The reasons for these changes are performance hang ups when passing large queries to fixpoint. We noticed that a significant amount of time is being spent in elab - and we suspect it's due to the exponential nature of using apply and applyExpr. Additionally, we observed that trans and fold in the type visitors and folders were taking up a massive amount of memory. By "specializing" the visitor not to have an accumulator we reduced the memory footprint on certain queries by ~ half.

As of now, changes 1 and 3 are implemented and I'm working on 2. Just 1 and 3 cut down the time fixpoint takes on large queries by ~ 1/3.

[ranjitjhala]

let me check this works with the LH tests too...

[vrindisbacher]

Sounds good - fwiw I also ran the flux tests with this version and everything passed.

[nilehmann]

I'm trying to rationalize the correctness of this change.

I think you can delay the substitution of sort variables as long as you don't structurally match on sorts, i.e., you don't make decisions based on the structure of sorts (which may have solved variables that should be considered in the decision). Presumably, elaboration shouldn't be making decisions based on the structure of sorts in the expression being elaborated so this change sounds fine...

...except that you structurally match on sorts when printing expressions for errors. For example, I think this changes the behavior of this line

liquid-fixpoint/src/Language/Fixpoint/SortCheck.hs

Line 586 in ac79d5c

!s <- checkIteTy g p e1' e2' s1 s2

because checkIteTy prints the expressions (with pending substitutions) in case of an error. However, I have the impression that this always has been wrong and errors may print expressions with sorts variables that have already been solved.

unrelated and out of curiosity: do the changes in strictness have any impact? the constructors of Expr are already marked as strict

[vrindisbacher]

Ah ya you're right - I suppose you could use applyExpr in the error case of checkIteTy. e..g errIte e1 e2 t1 t2 -> errIte (applyExp theta e1) (applyExp theta e2) t1 t2?

[vrindisbacher]

I think there are some bugs in Foldable. Working them out now.

[facundominguez]

Hello! Is there a description available of the problem that this contribution is addressing? I don't promise to review, but it would be helpful for future reference nonetheless.

[vrindisbacher]

Hello! Is there a description available of the problem that this contribution is addressing? I don't promise to review, but it would be helpful for future reference nonetheless.

I just updated the description with some details. Let me know if you have questions / if I can provide additional details.