Safe Haskell	Safe-Inferred
Language	Haskell98

Language.Haskell.Liquid.Constraint.Types

Contents

Constraint Generation Monad
Constraint information
Constraint Generation Environment
Logical constraints (FIXME: related to bounds?)
Fixpoint environment
Hole Environment
Subtyping Constraints
Well-formedness Constraints
Invariants
Aliases?

Synopsis

type CG = State CGInfo
data CGInfo = CGInfo {
- fEnv :: !(SEnv Sort)
- hsCs :: ![SubC]
- hsWfs :: ![WfC]
- fixCs :: ![FixSubC]
- fixWfs :: ![FixWfC]
- freshIndex :: !Integer
- binds :: !FixBindEnv
- ebinds :: ![BindId]
- annotMap :: !(AnnInfo (Annot SpecType))
- tyConInfo :: !TyConMap
- newTyEnv :: !(HashMap TyCon SpecType)
- termExprs :: !(HashMap Var [Located Expr])
- specLVars :: !(HashSet Var)
- specLazy :: !(HashSet Var)
- specTmVars :: !(HashSet Var)
- autoSize :: !(HashSet TyCon)
- tyConEmbed :: !(TCEmb TyCon)
- kuts :: !Kuts
- kvPacks :: ![HashSet KVar]
- cgLits :: !(SEnv Sort)
- cgConsts :: !(SEnv Sort)
- cgADTs :: ![DataDecl]
- tcheck :: !Bool
- cgiTypeclass :: !Bool
- pruneRefs :: !Bool
- logErrors :: ![Error]
- kvProf :: !KVProf
- recCount :: !Int
- bindSpans :: HashMap BindId SrcSpan
- allowHO :: !Bool
- ghcI :: !TargetInfo
- dataConTys :: ![(Var, SpecType)]
- unsorted :: !Templates
}
data CGEnv = CGE {
- cgLoc :: !SpanStack
- renv :: !REnv
- syenv :: !(SEnv Var)
- denv :: !RDEnv
- litEnv :: !(SEnv Sort)
- constEnv :: !(SEnv Sort)
- fenv :: !FEnv
- recs :: !(HashSet Var)
- invs :: !RTyConInv
- rinvs :: !RTyConInv
- ial :: !RTyConIAl
- grtys :: !REnv
- assms :: !REnv
- intys :: !REnv
- emb :: TCEmb TyCon
- tgEnv :: !TagEnv
- tgKey :: !(Maybe TagKey)
- trec :: !(Maybe (HashMap Symbol SpecType))
- lcb :: !(HashMap Symbol CoreExpr)
- forallcb :: !(HashMap Var Expr)
- holes :: !HEnv
- lcs :: !LConstraint
- cerr :: !(Maybe (TError SpecType))
- cgInfo :: !TargetInfo
- cgVar :: !(Maybe Var)
}
newtype LConstraint = LC [[(Symbol, SpecType)]]
data FEnv = FE {
- feBinds :: !IBindEnv
- feEnv :: !(SEnv Sort)
- feIdEnv :: !(SEnv BindId)
}
initFEnv :: [(Symbol, Sort)] -> FEnv
insertsFEnv :: FEnv -> [((Symbol, Sort), BindId)] -> FEnv
data HEnv
fromListHEnv :: [Symbol] -> HEnv
elemHEnv :: Symbol -> HEnv -> Bool
data SubC
- = SubC {
  - senv :: !CGEnv
  - lhs :: !SpecType
  - rhs :: !SpecType
  }
- | SubR {
  - senv :: !CGEnv
  - oblig :: !Oblig
  - ref :: !RReft
  }
type FixSubC = SubC Cinfo
subVar :: FixSubC -> Maybe Var
data WfC = WfC !CGEnv !SpecType
type FixWfC = WfC Cinfo
type RTyConInv = HashMap RTyCon [RInv]
mkRTyConInv :: [(Maybe Var, Located SpecType)] -> RTyConInv
addRTyConInv :: RTyConInv -> SpecType -> SpecType
addRInv :: RTyConInv -> (Var, SpecType) -> (Var, SpecType)
type RTyConIAl = HashMap RTyCon [RInv]
mkRTyConIAl :: [(a, Located SpecType)] -> RTyConInv
removeInvariant :: CGEnv -> CoreBind -> (CGEnv, RTyConInv)
restoreInvariant :: CGEnv -> RTyConInv -> CGEnv
makeRecInvariants :: CGEnv -> [Var] -> CGEnv
getTemplates :: CG Templates
getLocation :: CGEnv -> SrcSpan

Constraint Generation Monad

type CG = State CGInfo Source #

Constraint information

data CGInfo Source #

Generation: Types ---------------------------------------------------------

Constructors

CGInfo

Fields

fEnv :: !(SEnv Sort)
top-level fixpoint env
hsCs :: ![SubC]
subtyping constraints over RType
hsWfs :: ![WfC]
wellformedness constraints over RType
fixCs :: ![FixSubC]
subtyping over Sort (post-splitting)
fixWfs :: ![FixWfC]
wellformedness constraints over Sort (post-splitting)
freshIndex :: !Integer
counter for generating fresh KVars
binds :: !FixBindEnv
set of environment binders
ebinds :: ![BindId]
existentials
annotMap :: !(AnnInfo (Annot SpecType))
source-position annotation map
tyConInfo :: !TyConMap
information about type-constructors
newTyEnv :: !(HashMap TyCon SpecType)
Mapping of new type type constructors with their refined types.
termExprs :: !(HashMap Var [Located Expr])
Terminating Metrics for Recursive functions
specLVars :: !(HashSet Var)
Set of variables to ignore for termination checking
specLazy :: !(HashSet Var)
"Lazy binders", skip termination checking
specTmVars :: !(HashSet Var)
Binders that FAILED struct termination check that MUST be checked
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)
kvPacks :: ![HashSet KVar]
Fixpoint "packs" of correlated kvars
cgLits :: !(SEnv Sort)
Global symbols in the refinement logic
cgConsts :: !(SEnv Sort)
Distinct constant symbols in the refinement logic
cgADTs :: ![DataDecl]
ADTs extracted from Haskell 'data' definitions
tcheck :: !Bool
Check Termination (?)
cgiTypeclass :: !Bool
Enable typeclass support
pruneRefs :: !Bool
prune unsorted refinements
logErrors :: ![Error]
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
allowHO :: !Bool
ghcI :: !TargetInfo
dataConTys :: ![(Var, SpecType)]
Refined Types of Data Constructors
unsorted :: !Templates
Potentially unsorted expressions

Instances

Instances details

NFData CGInfo Source #
Instance details Defined in Language.Haskell.Liquid.Constraint.Types Methods rnf :: CGInfo -> () #
PPrint CGInfo Source #
Instance details Defined in Language.Haskell.Liquid.Constraint.Types Methods pprintTidy :: Tidy -> CGInfo -> Doc # pprintPrec :: Int -> Tidy -> CGInfo -> Doc #
Freshable CG Integer Source #	This is all hardwiring stuff to CG ----------------------------------------
Instance details Defined in Language.Haskell.Liquid.Constraint.Fresh Methods fresh :: CG Integer Source # true :: Bool -> Integer -> CG Integer Source # refresh :: Bool -> Integer -> CG Integer Source #

Constraint Generation Environment

data CGEnv Source #

Constructors

CGE

Fields

cgLoc :: !SpanStack
Location in original source file
renv :: !REnv
SpecTypes for Bindings in scope
syenv :: !(SEnv Var)
Map from free Symbols (e.g. datacons) to Var
denv :: !RDEnv
Dictionary Environment
litEnv :: !(SEnv Sort)
Global literals
constEnv :: !(SEnv Sort)
Distinct literals
fenv :: !FEnv
Fixpoint Environment
recs :: !(HashSet Var)
recursive defs being processed (for annotations)
invs :: !RTyConInv
Datatype invariants
rinvs :: !RTyConInv
Datatype recursive invariants: ignored in the base case assumed in rec call
ial :: !RTyConIAl
Datatype checkable invariants
grtys :: !REnv
Top-level variables with (assert)-guarantees to verify
assms :: !REnv
Top-level variables with assumed types
intys :: !REnv
Top-level variables with auto generated internal 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 (c.f. LAZYVARs)
forallcb :: !(HashMap Var Expr)
Polymorhic let bindings
holes :: !HEnv
Types with holes, will need refreshing
lcs :: !LConstraint
Logical Constraints
cerr :: !(Maybe (TError SpecType))
error that should be reported at the user
cgInfo :: !TargetInfo
top-level TargetInfo
cgVar :: !(Maybe Var)
top level function being checked

Instances

Instances details

Show CGEnv Source #
Instance details Defined in Language.Haskell.Liquid.Constraint.Types Methods showsPrec :: Int -> CGEnv -> ShowS # show :: CGEnv -> String # showList :: [CGEnv] -> ShowS #
NFData CGEnv Source #
Instance details Defined in Language.Haskell.Liquid.Constraint.Types Methods rnf :: CGEnv -> () #
PPrint CGEnv Source #
Instance details Defined in Language.Haskell.Liquid.Constraint.Types Methods pprintTidy :: Tidy -> CGEnv -> Doc # pprintPrec :: Int -> Tidy -> CGEnv -> Doc #
HasConfig CGEnv Source #
Instance details Defined in Language.Haskell.Liquid.Constraint.Types Methods getConfig :: CGEnv -> Config Source #

Logical constraints (FIXME: related to bounds?)

newtype LConstraint Source #

Constructors

LC [[(Symbol, SpecType)]]

Instances

Instances details

Monoid LConstraint Source #
Instance details Defined in Language.Haskell.Liquid.Constraint.Types Methods mempty :: LConstraint # mappend :: LConstraint -> LConstraint -> LConstraint # mconcat :: [LConstraint] -> LConstraint #
Semigroup LConstraint Source #
Instance details Defined in Language.Haskell.Liquid.Constraint.Types Methods (<>) :: LConstraint -> LConstraint -> LConstraint # sconcat :: NonEmpty LConstraint -> LConstraint # stimes :: Integral b => b -> LConstraint -> LConstraint #

Fixpoint environment

data FEnv Source #

Fixpoint Environment ------------------------------------------------------

Constructors

FE
Fields feBinds :: !IBindEnv Integer Keys for Fixpoint Environment feEnv :: !(SEnv Sort) Fixpoint Environment feIdEnv :: !(SEnv BindId) Map from Symbol to current BindId

Instances

Instances details

NFData FEnv Source #
Instance details Defined in Language.Haskell.Liquid.Constraint.Types Methods rnf :: FEnv -> () #

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

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

Hole Environment

data HEnv Source #

Helper Types: HEnv --------------------------------------------------------

fromListHEnv :: [Symbol] -> HEnv Source #

elemHEnv :: Symbol -> HEnv -> Bool Source #

Subtyping Constraints

data SubC Source #

Subtyping Constraints -----------------------------------------------------

Constructors

SubC
Fields senv :: !CGEnv lhs :: !SpecType rhs :: !SpecType
SubR
Fields senv :: !CGEnv oblig :: !Oblig ref :: !RReft

Instances

Instances details

NFData SubC Source #
Instance details Defined in Language.Haskell.Liquid.Constraint.Types Methods rnf :: SubC -> () #
PPrint SubC Source #
Instance details Defined in Language.Haskell.Liquid.Constraint.Types Methods pprintTidy :: Tidy -> SubC -> Doc # pprintPrec :: Int -> Tidy -> SubC -> Doc #

type FixSubC = SubC Cinfo Source #

subVar :: FixSubC -> Maybe Var Source #

Well-formedness Constraints

data WfC Source #

Constructors

WfC !CGEnv !SpecType

Instances

Instances details

NFData WfC Source #
Instance details Defined in Language.Haskell.Liquid.Constraint.Types Methods rnf :: WfC -> () #
PPrint WfC Source #
Instance details Defined in Language.Haskell.Liquid.Constraint.Types Methods pprintTidy :: Tidy -> WfC -> Doc # pprintPrec :: Int -> Tidy -> WfC -> Doc #

type FixWfC = WfC Cinfo Source #

Invariants

type RTyConInv = HashMap RTyCon [RInv] Source #

mkRTyConInv :: [(Maybe Var, Located SpecType)] -> RTyConInv Source #

addRTyConInv :: RTyConInv -> SpecType -> SpecType Source #

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

Aliases?

type RTyConIAl = HashMap RTyCon [RInv] Source #

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

removeInvariant :: CGEnv -> CoreBind -> (CGEnv, RTyConInv) Source #

restoreInvariant :: CGEnv -> RTyConInv -> CGEnv Source #

makeRecInvariants :: CGEnv -> [Var] -> CGEnv Source #

getTemplates :: CG Templates Source #

getLocation :: CGEnv -> SrcSpan Source #