| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Fixpoint.Solver.Eliminate
Description
This module exports a single function that computes the dependency
information needed to eliminate non-cut KVars, and then transitively
collapse the resulting constraint dependencies.
See the type of SolverInfo for details.
Synopsis
- solverInfo :: Config -> SInfo a -> SolverInfo a
Documentation
solverInfo :: Config -> SInfo a -> SolverInfo a Source #
solverInfo constructs a SolverInfo comprising the Solution and various
indices needed by the worklist-based refinement loop
Computes the set of cut and non-cut kvars, computes the hypotheses common to all of the usage sites of each kvar, then initializes the solutions of the non-cut KVars (in the sHyp field).
This is part of the implementation of the FUSION algorithm described in:
"Local Refinement Typing", ICFP 2017, https://ranjitjhala.github.io/static/local_refinement_typing.pdf