Fields

• gsTySigs :: ![(Var, LocSpecType)]

  Asserted Reftypes

• gsAsmSigs :: ![(Var, LocSpecType)]

  Assumed Reftypes

• gsInSigs :: ![(Var, LocSpecType)]

  Auto generated Signatures

• gsCtors :: ![(Var, LocSpecType)]

  Data Constructor Measure Sigs

• gsLits :: ![(Symbol, LocSpecType)]

  Literals/Constants e.g. datacons: EQ, GT, string lits: "zombie",...

• gsMeas :: ![(Symbol, LocSpecType)]

  Measure Types eg. len :: [a] -> Int

• gsInvariants :: ![(Maybe Var, LocSpecType)]

  Data Type Invariants that came from the definition of var measure eg. forall a. {v: [a] | len(v) >= 0}

• gsIaliases :: ![(LocSpecType, LocSpecType)]

  Data Type Invariant Aliases

• gsDconsP :: ![Located DataCon]

  Predicated Data-Constructors e.g. see testsposMap.hs

• gsTconsP :: ![(TyCon, TyConP)]

  Predicated Type-Constructors eg. see testsposMap.hs

• gsFreeSyms :: ![(Symbol, Var)]

  List of Symbol free in spec and corresponding GHC var eg. (Cons, Cons#7uz) from testsposex1.hs

• gsTcEmbeds :: TCEmb TyCon

  How to embed GHC Tycons into fixpoint sorts e.g. "embed Set as Set_set" from includeDataSet.spec

• gsQualifiers :: ![Qualifier]

  Qualifiers in Source/Spec files e.g testsposqualTest.hs

• gsADTs :: ![DataDecl]

  ADTs extracted from Haskell 'data' definitions

• gsTgtVars :: ![Var]

  Top-level Binders To Verify (empty means ALL binders)

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

  Lexicographically ordered size witnesses for termination

• gsTexprs :: ![(Var, [Located Expr])]

  Lexicographically ordered expressions for termination

• gsNewTypes :: ![(TyCon, LocSpecType)]

  Mapping of 'newtype' type constructors with their refined types.

• gsLvars :: !(HashSet Var)

  Variables that should be checked in the environment they are used

• gsLazy :: !(HashSet Var)

  Binders to IGNORE during termination checking

• gsAutosize :: !(HashSet TyCon)

  Binders to IGNORE during termination checking

• gsAutoInst :: !(HashMap Var (Maybe Int))

  Binders to expand with automatic axiom instances maybe with specified fuel

• gsConfig :: !Config

  Configuration Options

• gsExports :: !NameSet

  Names exported by the module being verified

• gsMeasures :: [Measure SpecType DataCon]
   
• gsTyconEnv :: HashMap TyCon RTyCon
   
• gsDicts :: DEnv Var SpecType

  Dictionary Environment

• gsAxioms :: [AxiomEq]

  Axioms from reflected functions

• gsReflects :: [Var]

  Binders for reflected functions

• gsLogicMap :: LogicMap
   
• gsProofType :: Maybe Type
   
• gsRTAliases :: !RTEnv

  Refinement type aliases