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

• 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

Instances

HasConfig GhcSpec

Methods

getConfig :: GhcSpec -> Config

patternFlag :: GhcSpec -> Bool

higherOrderFlag :: GhcSpec -> Bool

pruneFlag :: GhcSpec -> Bool

expandFlag :: GhcSpec -> Bool

hasOpt :: GhcSpec -> (Config -> Bool) -> Bool

totalityCheck :: GhcSpec -> Bool

terminationCheck :: GhcSpec -> Bool

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

Lifted Spec

loadLiftedSpec :: Config -> FilePath -> IO BareSpec

saveLiftedSpec :: FilePath -> ModName -> BareSpec -> IO ()