Documentation

Fields

tySigs :: ![(Var, Located SpecType)]

Asserted Reftypes eg. see include/Prelude.spec

asmSigs :: ![(Var, Located SpecType)]

Assumed Reftypes

ctors :: ![(Var, Located SpecType)]

Data Constructor Measure Sigs eg. (:) :: a -> xs:[a] -> {v: Int | v = 1 + len(xs) }

meas :: ![(Symbol, Located SpecType)]

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

invariants :: ![Located SpecType]

Data Type Invariants eg. forall a. {v: [a] | len(v) >= 0}

ialiases :: ![(Located SpecType, Located SpecType)]

Data Type Invariant Aliases

dconsP :: ![(DataCon, DataConP)]

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

tconsP :: ![(TyCon, TyConP)]

Predicated Type-Constructors eg. see testsposMap.hs

freeSyms :: ![(Symbol, Var)]

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

tcEmbeds :: TCEmb TyCon

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

qualifiers :: ![Qualifier]

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

tgtVars :: ![Var]

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

decr :: ![(Var, [Int])]

Lexicographically ordered size witnesses for termination

texprs :: ![(Var, [Expr])]

Lexicographically ordered expressions for termination

lvars :: !(HashSet Var)

Variables that should be checked in the environment they are used

lazy :: !(HashSet Var)

Binders to IGNORE during termination checking

autosize :: !(HashSet TyCon)

Binders to IGNORE during termination checking

config :: !Config

Configuration Options

exports :: !NameSet

Names exported by the module being verified

measures :: [Measure SpecType DataCon]

 

tyconEnv :: HashMap TyCon RTyCon

 

dicts :: DEnv Var SpecType

Dictionary Environment