search

ucsd-progsys / liquidhaskell

Liquid Types For Haskell
BSD 3-Clause "New" or "Revised" License
1.2k stars 139 forks source link

Tame the dissemination of measure equations in constraints #2005

Open facundominguez opened 2 years ago

facundominguez commented 2 years ago

Currently if a measure is in scope, every time a data constructor appears in a constraint, an equation for that constructor and measure will be added to the environment of that constraint.

This means that the amount of equations added by having measures in scope is

 amount_of_data_constructor_occurrences x ​amount_of_measures_that_mention_the_data_constructor

Many times, though, a measure being in scope doesn't mean that the measure is relevant to the verification of every constraint in the module, which results in a lot of useless equations being added. This requires in turn more communication with the SMT solver, and it compounds badly with PLE, which will then try to unfold any function applications used in the equations.

Adding these (most-of-the-time) irrelevant equations buries the interesting equations that the user might care about inspecting in LH dumps when verification fails.

Lastly adding a measure in one of the transitively imported modules can slowdown or affect verification of previously passing constraints.

I propose here that we implement a flag --no-automatic-measure-spicing (name suggestions welcome) that stops LH from adding measures everywhere like this. If the user wants a measure to be spiced in the constraints of a module, she can write:

{-@ use_measure f @-}

where f is a measure in scope.

And furthermore, if the user wants to use a measure only in the constraints of a particular function, she can write:

{-@ use_measure g f @-}

where g is a function in the current module, and f is a measure in scope.

Note that this proposal affects only LH, not how PLE treats measures. But PLE could take advantage of this later on. At one point we tried handling measures as reflected functions in PLE and this was too slow when LH generated so many measure equations. It showed up in a test tests/benchmarks/sf/Lists.hs. But we could consider this strategy again when --no-automatic-measure-spicing is in effect.

facundominguez commented 2 years ago

One possible refinement of this idea is to not add measure equations to the constraints if ple is enabled, since ple will add those equations anyway as it discovers the data constructors in the candidate expressions.