Language.Haskell.Liquid.Constraint.Types

Documentation

data CGEnv

Constructors

CGE

Fields

loc :: !SrcSpan

Location in original source file

renv :: !REnv

SpecTypes for Bindings in scope

syenv :: !(SEnv Var)

Map from free Symbols (e.g. datacons) to Var , penv :: !(F.SEnv PrType) -- ^ PrTypes for top-level bindings (merge with renv)

denv :: !RDEnv

Dictionary Environment

fenv :: !FEnv

Fixpoint Environment

recs :: !(HashSet Var)

recursive defs being processed (for annotations)

invs :: !RTyConInv

Datatype invariants

ial :: !RTyConIAl

Datatype checkable invariants

grtys :: !REnv

Top-level variables with (assert)-guarantees to verify

assms :: !REnv

Top-level variables with assumed types

emb :: TCEmb TyCon

How to embed GHC Tycons into fixpoint sorts

tgEnv :: !TagEnv

Map from top-level binders to fixpoint tag

tgKey :: !(Maybe TagKey)

Current top-level binder

trec :: !(Maybe (HashMap Symbol SpecType))

Type of recursive function with decreasing constraints

lcb :: !(HashMap Symbol CoreExpr)

Let binding that have not been checked

holes :: !HEnv

Types with holes, will need refreshing

lcs :: !LConstraint

Logical Constraints

Instances

Show CGEnv

NFData CGEnv

PPrint CGEnv

data LConstraint

Constructors

LC [[(Symbol, SpecType)]]

Instances

Monoid LConstraint

data SubC

Constructors

SubC

Fields

senv :: !CGEnv

lhs :: !SpecType

rhs :: !SpecType

SubR

Fields

senv :: !CGEnv

oblig :: !Oblig

ref :: !RReft

Instances

NFData SubC

PPrint SubC

SubStratum SubC

data WfC

Constructors

WfC !CGEnv !SpecType

Instances

NFData WfC

PPrint WfC

type FixSubC = SubC Cinfo

type FixWfC = WfC Cinfo

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)

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

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

autoSize :: !(HashSet TyCon)

? 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 constraint generation

kvProf :: !KVProf

Profiling distribution of KVars

recCount :: !Int

number of recursive functions seen (for benchmarks)

bindSpans :: HashMap BindId SrcSpan

Source Span associated with Fixpoint Binder

Instances

NFData CGInfo

PPrint CGInfo

pprCGInfo :: t -> Doc

newtype HEnv

Constructors

HEnv (HashSet Symbol)

fromListHEnv :: [Symbol] -> HEnv

elemHEnv :: Symbol -> HEnv -> Bool

type RTyConInv = HashMap RTyCon [SpecType]

type RTyConIAl = HashMap RTyCon [SpecType]

mkRTyConInv :: [Located SpecType] -> RTyConInv

mkRTyConIAl :: [(a, Located SpecType)] -> RTyConInv

addRTyConInv :: RTyConInv -> SpecType -> SpecType

addRInv :: RTyConInv -> (Var, SpecType) -> (Var, SpecType)

conjoinInvariantShift :: RType RTyCon tv RReft -> SpecType -> RType RTyCon tv RReft

conjoinInvariant :: RType RTyCon tv RReft -> SpecType -> RType RTyCon tv RReft

grapBindsWithType :: RType RTyCon RTyVar r -> CGEnv -> [Symbol]

toListREnv :: REnv -> [(Symbol, SpecType)]

filterREnv :: (SpecType -> Bool) -> REnv -> REnv

fromListREnv :: [(Symbol, SpecType)] -> REnv

deleteREnv :: Symbol -> REnv -> REnv

insertREnv :: Symbol -> SpecType -> REnv -> REnv

lookupREnv :: Symbol -> REnv -> Maybe SpecType

memberREnv :: Symbol -> REnv -> Bool

data FEnv

Constructors

FE

Fields

fe_binds :: !IBindEnv

Integer Keys for Fixpoint Environment

fe_env :: !(SEnv Sort)

Fixpoint Environment

Instances

NFData FEnv

insertFEnv :: FEnv -> ((Symbol, Sort), BindId) -> FEnv

insertsFEnv :: FEnv -> [((Symbol, Sort), BindId)] -> FEnv

initFEnv :: [(Symbol, Sort)] -> FEnv