Language.Haskell.Liquid.Bare

This module contains the functions that convert from descriptions of symbols, names and types (over freshly parsed bare Strings), to representations connected to GHC vars, names, and types. The actual representations of bare and real (refinement) types are all in RefType -- they are different instances of RType

Documentation

data GhcSpec

The following is the overall type for specifications obtained from parsing the target source and dependent libraries

Constructors

SP

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

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

Instances

PPrint GhcSpec

makeGhcSpec :: Config -> ModName -> [CoreBind] -> [Var] -> [Var] -> NameSet -> HscEnv -> Either Error LogicMap -> [(ModName, BareSpec)] -> IO GhcSpec