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

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

 

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

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

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 axiomatized Haskell functions to the logical functions

cerr :: !(Maybe (TError SpecType))

error that should be reported at the user

Fields

feBinds :: !IBindEnv

Integer Keys for Fixpoint Environment

feEnv :: !(SEnv Sort)

Fixpoint Environment

Fields

senv :: !CGEnv

 

lhs :: !SpecType

 

rhs :: !SpecType

 

Fields

senv :: !CGEnv

 

oblig :: !Oblig

 

ref :: !RReft