Documentation

Strips from all the constraint environments the bindings that are irrelevant for their respective constraints.

Environment reduction has the following stages.

Stage 1) Compute the binding dependencies of each constraint ignoring KVars.

A binding is a dependency of a constraint if it is mentioned in the lhs, or the rhs of the constraint, or in a binding that is a dependency, or in a define or match clause that is mentioned in the lhs or rhs or another binding dependency, or if it appears in the environment of the constraint and can't be discarded as trivial (see dropIrrelevantBindings).

Stage 2) Compute the binding dependencies of KVars.

A binding is a dependency of a KVar K1 if it is a dependency of a constraint in which the K1 appears, or if it is a dependency of another KVar appearing in a constraint in which K1 appears.

Stage 3) Drop from the environment of each constraint the bindings that aren't dependencies of the constraint, or that aren't dependencies of any KVar appearing in the constraint.

Note on SInfo:

This function can be changed to work on SInfo rather than FInfo. However, this causes some tests to fail. At least:

liquid-fixpointtestsproof/rewrite.fq testsimportclient/ReflectClient4a.hs

lhs bindings are numbered with the highest numbers when FInfo is converted to SInfo. Environment reduction, however, rehashes the binding identifiers and lhss could end up with a lower numbering. For most of the tests, this doesn't seem to make a difference, but it causes the two tests referred above to fail.

See #473 for more discussion.

Simplifies bindings in constraint environments.

It runs mergeDuplicatedBindings and simplifyBooleanRefts on the environment of each constraint.

If 'inlineANFBindings cfg' is on, also runs undoANFAndVV to inline lq_anf bindings.

dropLikelyIrrelevantBindings ss env is like dropIrrelevantBindings but drops bindings that could potentially be necessary to validate a constraint.

This function drops any bindings in the reachable set of symbols of ss. See relatedSymbols.

A constraint might be rendered unverifiable if the verification depends on the environment being inconsistent. For instance, suppose the constraint is a < 0 and we call this function like

dropLikelyIrrelevantBindings ["a"] [a : { v | v > 0 }, b : { v | false }]
  == [a : { v | v > 0 }]

The binding for b is dropped since it is not otherwise related to a, making the corresponding constraint unverifiable.

Bindings refered only from match or define clauses will be dropped as well.

Symbols starting with a capital letter will be dropped too, as these are usually global identifiers with either uninteresting or known types.

Inlines bindings given by srLookup in the given expression if they appear in equalities.

Given a binding like a : { v | v = e1 && e2 } and an expression ... e0 = a ..., this function produces the expression ... e0 = e1 ... if v does not appear free in e1.

... e0 = (a : s) ... is equally transformed to ... e0 = (e1 : s) ...

Given a binding like a : { v | v = e1 } and an expression ... a ..., this function produces the expression ... e1 ... if v does not appear free in e1.

Inlines bindings in env in the given SortedReft.

If the environment contains duplicated bindings, they are combined with conjunctions.

This means that [ a : {v | P v }, a : {z | Q z }, b : {v | S v} ] is combined into [ a : {v | P v && Q v }, b : {v | S v} ]

If a symbol has two bindings with different sorts, none of the bindings for that symbol are merged.

Transforms bindings of the form {v:bool | v && P v} into {v:Bool | v && P true}, and bindings of the form {v:bool | ~v && P v} into {v:bool | ~v && P false}.

Only yields the modified bindings.

Like undoANF but also inlines VV bindings

This function is used to produced the prettified output, and the user can request to use it in the verification pipeline with --inline-anf-bindings. However, using it in the verification pipeline causes some tests in liquidhaskell to blow up.

Note: This function simplifies.

Like substBindings but specialized for ANF bindings.

Only bindings with prefix lq_anf$... might be inlined.