ucsd-progsys/liquid-fixpoint — pull request #26 by ranjitjhala (2013-11-21 21:54:53+00:00)
Title: Lazy Instantiation

Rather than instatiating up front, wait till later. Gives some non-trivial speed bumps for the solver.
Idea was to only instantiate quals with symbols that appear in a non-trivial manner in the LHS of
constraints where the K appears on the RHS.

Problem, need to instantiate even with non-trivial vars, as quals like

isBin(v) => q

may hold (and may be required) even if no information holds for variables in q.

Still, non-trivial gains simply by skipping the crazy step where we check if EACH Kvar is well
formed in EACH environment that it appears in (!!!) instead of anything to do with lazy instantiation.
Problem: this leads to malformed environments -- because of crazy renaming bugs during constraint
generation.

(Yet another case of an expensive run-time check masking a serious bug.)

Need to fix constraint generation but since this branch is done for now, leaving it as such...

(Probably could simplify by just using master and SKIPPING the monstrous env-validity check in `refine-sort`?)

?