Language.Haskell.Liquid.Constraint.Types

Constraint Generation Monad

type CG = State CGInfo

Constraint information

data CGInfo

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 :: !BindEnv

  set of environment binders

• ebinds :: ![BindId]

  existentials

• annotMap :: !(AnnInfo (Annot SpecType))

  source-position annotation map

• holesMap :: !(HashMap Var (HoleInfo (CGInfo, CGEnv) SpecType))

  information for ghc hole expressions

• tyConInfo :: !TyConMap

  information about type-constructors

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

  ^ Lexicographic order of decreasing args (DEPRECATED)

• 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 (?)

• 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

NFData CGInfo

Defined in Language.Haskell.Liquid.Constraint.Types

Methods

rnf :: CGInfo -> ()

PPrint CGInfo

Defined in Language.Haskell.Liquid.Constraint.Types

Methods

pprintTidy :: Tidy -> CGInfo -> Doc

pprintPrec :: Int -> Tidy -> CGInfo -> Doc

Freshable CG Integer

This is all hardwiring stuff to CG ----------------------------------------

Defined in Language.Haskell.Liquid.Constraint.Fresh

Methods

fresh :: CG Integer

true :: Integer -> CG Integer

refresh :: Integer -> CG Integer

Constraint Generation Environment

data CGEnv

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

Show CGEnv

Defined in Language.Haskell.Liquid.Constraint.Types

Methods

showsPrec :: Int -> CGEnv -> ShowS

show :: CGEnv -> String

showList :: [CGEnv] -> ShowS

NFData CGEnv

Defined in Language.Haskell.Liquid.Constraint.Types

Methods

rnf :: CGEnv -> ()

PPrint CGEnv

Defined in Language.Haskell.Liquid.Constraint.Types

Methods

pprintTidy :: Tidy -> CGEnv -> Doc

pprintPrec :: Int -> Tidy -> CGEnv -> Doc

HasConfig CGEnv

Defined in Language.Haskell.Liquid.Constraint.Types

Methods

getConfig :: CGEnv -> Config

Logical constraints (FIXME: related to bounds?)

data LConstraint

Constructors

LC [[(Symbol, SpecType)]]

Instances

Semigroup LConstraint

Defined in Language.Haskell.Liquid.Constraint.Types

Methods

(<>) :: LConstraint -> LConstraint -> LConstraint

sconcat :: NonEmpty LConstraint -> LConstraint

stimes :: Integral b => b -> LConstraint -> LConstraint

Monoid LConstraint

Defined in Language.Haskell.Liquid.Constraint.Types

Methods

mempty :: LConstraint

mappend :: LConstraint -> LConstraint -> LConstraint

mconcat :: [LConstraint] -> LConstraint

Fixpoint environment

data FEnv

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

NFData FEnv

Defined in Language.Haskell.Liquid.Constraint.Types

Methods

rnf :: FEnv -> ()

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

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

Hole Environment

data HEnv

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

fromListHEnv :: [Symbol] -> HEnv

elemHEnv :: Symbol -> HEnv -> Bool

Subtyping Constraints

data SubC

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

Constructors

SubC

Fields

• senv :: !CGEnv
• lhs :: !SpecType
• rhs :: !SpecType

SubR

Fields

• senv :: !CGEnv
• oblig :: !Oblig
• ref :: !RReft

Instances

NFData SubC

Defined in Language.Haskell.Liquid.Constraint.Types

Methods

rnf :: SubC -> ()

PPrint SubC

Defined in Language.Haskell.Liquid.Constraint.Types

Methods

pprintTidy :: Tidy -> SubC -> Doc

pprintPrec :: Int -> Tidy -> SubC -> Doc

type FixSubC = SubC Cinfo

subVar :: FixSubC -> Maybe Var

Well-formedness Constraints

data WfC

Constructors

WfC !CGEnv !SpecType

Instances

NFData WfC

Defined in Language.Haskell.Liquid.Constraint.Types

Methods

rnf :: WfC -> ()

PPrint WfC

Defined in Language.Haskell.Liquid.Constraint.Types

Methods

pprintTidy :: Tidy -> WfC -> Doc

pprintPrec :: Int -> Tidy -> WfC -> Doc

type FixWfC = WfC Cinfo

Invariants

type RTyConInv = HashMap RTyCon [RInv]

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

addRTyConInv :: RTyConInv -> SpecType -> SpecType

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

Aliases?

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