Fields

• measures :: ![Measure ty bndr]

  User-defined properties for ADTs

• asmSigs :: ![(LocSymbol, ty)]

  Assumed (unchecked) types; including reflected signatures

• sigs :: ![(LocSymbol, ty)]

  Imported functions and types

• localSigs :: ![(LocSymbol, ty)]

  Local type signatures

• reflSigs :: ![(LocSymbol, ty)]

  Reflected type signatures

• invariants :: ![ty]

  Data type invariants

• ialiases :: ![(ty, ty)]

  Data type invariants to be checked

• imports :: ![Symbol]

  Loaded spec module names

• dataDecls :: ![DataDecl]

  Predicated data definitions

• newtyDecls :: ![DataDecl]

  Predicated new type definitions

• includes :: ![FilePath]

  Included qualifier files

• aliases :: ![RTAlias Symbol BareType]

  RefType aliases

• ealiases :: ![RTAlias Symbol Expr]

  Expression aliases

• embeds :: !(TCEmb LocSymbol)

  GHC-Tycon-to-fixpoint Tycon map

• qualifiers :: ![Qualifier]

  Qualifiers in source/spec files

• decr :: ![(LocSymbol, [Int])]

  Information on decreasing arguments

• lvars :: ![LocSymbol]

  Variables that should be checked in the environment they are used

• lazy :: !(HashSet LocSymbol)

  Ignore Termination Check in these Functions , axioms :: !(S.HashSet LocSymbol) -- ^ Binders to turn into SMT axioms

• reflects :: !(HashSet LocSymbol)

  Binders to reflect

• autois :: !(HashMap LocSymbol (Maybe Int))

  Automatically instantiate axioms in these Functions with maybe specified fuel

• hmeas :: !(HashSet LocSymbol)

  Binders to turn into measures using haskell definitions

• hbounds :: !(HashSet LocSymbol)

  Binders to turn into bounds using haskell definitions

• inlines :: !(HashSet LocSymbol)

  Binders to turn into logic inline using haskell definitions

• autosize :: !(HashSet LocSymbol)

  Type Constructors that get automatically sizing info

• pragmas :: ![Located String]

  Command-line configurations passed in through source

• cmeasures :: ![Measure ty ()]

  Measures attached to a type-class

• imeasures :: ![Measure ty bndr]

  Mappings from (measure,type) -> measure

• classes :: ![RClass ty]

  Refined Type-Classes

• termexprs :: ![(LocSymbol, [Located Expr])]

  Terminating Conditions for functions

• rinstance :: ![RInstance ty]
   
• dvariance :: ![(LocSymbol, [Variance])]

  ? Where do these come from ?!

• bounds :: !(RRBEnv ty)
   
• defs :: !(HashMap LocSymbol Symbol)

  Temporary (?) hack to deal with dictionaries in specifications see testsposNatClass.hs

• axeqs :: ![AxiomEq]

  AxiomEqualities used for Proof-By-Evaluation

Fields

• ctorMap :: HashMap Symbol [Def ty ctor]
   
• measMap :: HashMap LocSymbol (Measure ty ctor)
   
• cmeasMap :: HashMap LocSymbol (Measure ty ())
   
• imeas :: ![Measure ty ctor]