Fields

• fEnv :: !(SEnv Sort)

  top-level fixpoint env

• 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

• 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

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

• scheck :: !Bool

  Check Strata (?)

• 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 :: !GhcInfo
   
• dataConTys :: ![(Var, SpecType)]

  Refined Types of Data Constructors

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)

• fargs :: !(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)

• holes :: !HEnv

  Types with holes, will need refreshing

• lcs :: !LConstraint

  Logical Constraints

• aenv :: !(HashMap Var Symbol)

  axiom environment maps reflected Haskell functions to the logical functions

• cerr :: !(Maybe (TError SpecType))

  error that should be reported at the user , cgCfg :: !Config -- ^ top-level config options

• cgInfo :: !GhcInfo

  top-level GhcInfo

• cgVar :: !(Maybe Var)

  top level function being checked

Fields

• feBinds :: !IBindEnv

  Integer Keys for Fixpoint Environment

• feEnv :: !(SEnv Sort)

  Fixpoint Environment

• feIdEnv :: !(SEnv BindId)

  Map from Symbol to current BindId

Fields

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

Fields

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