Language.Haskell.Liquid.Constraint

This module defines the representation of Subtyping and WF Constraints, and the code for syntax-directed constraint generation.

Constraint information output by generator

data CGInfo

Constructors

CGInfo

Fields

hsCs :: ![SubC]

subtyping constraints over RType

hsWfs :: ![WfC]

wellformedness constraints over RType

sCs :: ![SubC]

additional stratum constrains for let bindings

fixCs :: ![FixSubC]

subtyping over Sort (post-splitting)

isBind :: ![Bool]

tracks constraints that come from let-bindings

fixWfs :: ![FixWfC]

wellformedness constraints over Sort (post-splitting)

globals :: !FEnv

? global measures

freshIndex :: !Integer

counter for generating fresh KVars

binds :: !BindEnv

set of environment binders

annotMap :: !(AnnInfo (Annot SpecType))

source-position annotation map

tyConInfo :: !(HashMap TyCon RTyCon)

information about type-constructors

specQuals :: ![Qualifier]

? qualifiers in source files

specDecr :: ![(Var, [Int])]

? FIX THIS

termExprs :: !(HashMap Var [Expr])

Terminating Metrics for Recursive functions

specLVars :: !(HashSet Var)

Set of variables to ignore for termination checking

specLazy :: !(HashSet Var)

? FIX THIS

tyConEmbed :: !(TCEmb TyCon)

primitive Sorts into which TyCons should be embedded

kuts :: !Kuts

Fixpoint Kut variables (denoting "back-edges"/recursive KVars)

lits :: ![(Symbol, Sort)]

? FIX THIS

tcheck :: !Bool

Check Termination (?)

scheck :: !Bool

Check Strata (?)

trustghc :: !Bool

Trust ghc auto generated bindings

pruneRefs :: !Bool

prune unsorted refinements

logErrors :: ![TError SpecType]

Errors during coontraint generation

kvProf :: !KVProf

Profiling distribution of KVars

recCount :: !Int

number of recursive functions seen (for benchmarks)

Instances

NFData CGInfo

PPrint CGInfo

Function that does the actual generation

generateConstraints :: GhcInfo -> CGInfo

Project Constraints to Fixpoint Format

cgInfoFInfo :: CGInfo -> FInfo Cinfo

cgInfoFInfoBot :: CGInfo -> FInfo Cinfo

cgInfoFInfoKvars :: CGInfo -> [Symbol] -> FInfo Cinfo

KVars in constraints, for debug/profile purposes