Safe Haskell	None
Language	Haskell98

Language.Haskell.Liquid.Types.Specs

Contents

Different types of specifications
Gathering information about a module
TargetSpec
BareSpec
LiftedSpec
Tracking dependencies
Predicates on spec types
Other types
Legacy data structures
Provisional compatibility exports & optics

Description

This module contains the top-level structures that hold information about specifications.

Synopsis

data TargetInfo = TargetInfo {
- giSrc :: !TargetSrc
- giSpec :: !TargetSpec
}
data TargetSrc = TargetSrc {
- giIncDir :: !FilePath
- giTarget :: !FilePath
- giTargetMod :: !ModName
- giCbs :: ![CoreBind]
- gsTcs :: ![TyCon]
- gsCls :: !(Maybe [ClsInst])
- giDerVars :: !(HashSet Var)
- giImpVars :: ![Var]
- giDefVars :: ![Var]
- giUseVars :: ![Var]
- gsExports :: !(HashSet StableName)
- gsFiTcs :: ![TyCon]
- gsFiDcs :: ![(Symbol, DataCon)]
- gsPrimTcs :: ![TyCon]
- gsQualImps :: !QImports
- gsAllImps :: !(HashSet Symbol)
- gsTyThings :: ![TyThing]
}
data TargetSpec = TargetSpec {
- gsSig :: !GhcSpecSig
- gsQual :: !GhcSpecQual
- gsData :: !GhcSpecData
- gsName :: !GhcSpecNames
- gsVars :: !GhcSpecVars
- gsTerm :: !GhcSpecTerm
- gsRefl :: !GhcSpecRefl
- gsLaws :: !GhcSpecLaws
- gsImps :: ![(Symbol, Sort)]
- gsConfig :: !Config
}
newtype BareSpec = MkBareSpec {
- getBareSpec :: Spec LocBareType LocSymbol
}
data LiftedSpec = LiftedSpec {
- liftedMeasures :: HashSet (Measure LocBareType LocSymbol)
- liftedImpSigs :: HashSet (Symbol, Sort)
- liftedExpSigs :: HashSet (Symbol, Sort)
- liftedAsmSigs :: HashSet (LocSymbol, LocBareType)
- liftedSigs :: HashSet (LocSymbol, LocBareType)
- liftedInvariants :: HashSet (Maybe LocSymbol, LocBareType)
- liftedIaliases :: HashSet (LocBareType, LocBareType)
- liftedImports :: HashSet Symbol
- liftedDataDecls :: HashSet DataDecl
- liftedNewtyDecls :: HashSet DataDecl
- liftedAliases :: HashSet (Located (RTAlias Symbol BareType))
- liftedEaliases :: HashSet (Located (RTAlias Symbol Expr))
- liftedEmbeds :: TCEmb LocSymbol
- liftedQualifiers :: HashSet Qualifier
- liftedDecr :: HashSet (LocSymbol, [Int])
- liftedLvars :: HashSet LocSymbol
- liftedAutois :: HashMap LocSymbol (Maybe Int)
- liftedAutosize :: HashSet LocSymbol
- liftedCmeasures :: HashSet (Measure LocBareType ())
- liftedImeasures :: HashSet (Measure LocBareType LocSymbol)
- liftedClasses :: HashSet (RClass LocBareType)
- liftedClaws :: HashSet (RClass LocBareType)
- liftedRinstance :: HashSet (RInstance LocBareType)
- liftedIlaws :: HashSet (RILaws LocBareType)
- liftedDvariance :: HashSet (LocSymbol, [Variance])
- liftedBounds :: RRBEnv LocBareType
- liftedDefs :: HashMap LocSymbol Symbol
- liftedAxeqs :: HashSet Equation
}
newtype StableModule = StableModule {
- unStableModule :: Module
}
toStableModule :: Module -> StableModule
renderModule :: Module -> String
newtype TargetDependencies = TargetDependencies {
- getDependencies :: HashMap StableModule LiftedSpec
}
dropDependency :: StableModule -> TargetDependencies -> TargetDependencies
isPLEVar :: TargetSpec -> Var -> Bool
isExportedVar :: TargetSrc -> Var -> Bool
data QImports = QImports {
- qiModules :: !(HashSet Symbol)
- qiNames :: !(HashMap Symbol [Symbol])
}
data Spec ty bndr = Spec {
- measures :: ![Measure ty bndr]
- impSigs :: ![(Symbol, Sort)]
- expSigs :: ![(Symbol, Sort)]
- asmSigs :: ![(LocSymbol, ty)]
- sigs :: ![(LocSymbol, ty)]
- localSigs :: ![(LocSymbol, ty)]
- reflSigs :: ![(LocSymbol, ty)]
- invariants :: ![(Maybe LocSymbol, ty)]
- ialiases :: ![(ty, ty)]
- imports :: ![Symbol]
- dataDecls :: ![DataDecl]
- newtyDecls :: ![DataDecl]
- includes :: ![FilePath]
- aliases :: ![Located (RTAlias Symbol BareType)]
- ealiases :: ![Located (RTAlias Symbol Expr)]
- embeds :: !(TCEmb LocSymbol)
- qualifiers :: ![Qualifier]
- decr :: ![(LocSymbol, [Int])]
- lvars :: !(HashSet LocSymbol)
- lazy :: !(HashSet LocSymbol)
- rewrites :: !(HashSet LocSymbol)
- rewriteWith :: !(HashMap LocSymbol [LocSymbol])
- fails :: !(HashSet LocSymbol)
- reflects :: !(HashSet LocSymbol)
- autois :: !(HashMap LocSymbol (Maybe Int))
- hmeas :: !(HashSet LocSymbol)
- hbounds :: !(HashSet LocSymbol)
- inlines :: !(HashSet LocSymbol)
- ignores :: !(HashSet LocSymbol)
- autosize :: !(HashSet LocSymbol)
- pragmas :: ![Located String]
- cmeasures :: ![Measure ty ()]
- imeasures :: ![Measure ty bndr]
- classes :: ![RClass ty]
- claws :: ![RClass ty]
- termexprs :: ![(LocSymbol, [Located Expr])]
- rinstance :: ![RInstance ty]
- ilaws :: ![RILaws ty]
- dvariance :: ![(LocSymbol, [Variance])]
- bounds :: !(RRBEnv ty)
- defs :: !(HashMap LocSymbol Symbol)
- axeqs :: ![Equation]
}
data GhcSpecVars = SpVar {
- gsTgtVars :: ![Var]
- gsIgnoreVars :: !(HashSet Var)
- gsLvars :: !(HashSet Var)
- gsCMethods :: ![Var]
}
data GhcSpecSig = SpSig {
- gsTySigs :: ![(Var, LocSpecType)]
- gsAsmSigs :: ![(Var, LocSpecType)]
- gsRefSigs :: ![(Var, LocSpecType)]
- gsInSigs :: ![(Var, LocSpecType)]
- gsNewTypes :: ![(TyCon, LocSpecType)]
- gsDicts :: !(DEnv Var LocSpecType)
- gsMethods :: ![(Var, MethodType LocSpecType)]
- gsTexprs :: ![(Var, LocSpecType, [Located Expr])]
}
data GhcSpecNames = SpNames {
- gsFreeSyms :: ![(Symbol, Var)]
- gsDconsP :: ![Located DataCon]
- gsTconsP :: ![TyConP]
- gsTcEmbeds :: !(TCEmb TyCon)
- gsADTs :: ![DataDecl]
- gsTyconEnv :: !TyConMap
}
data GhcSpecTerm = SpTerm {
- gsStTerm :: !(HashSet Var)
- gsAutosize :: !(HashSet TyCon)
- gsLazy :: !(HashSet Var)
- gsFail :: !(HashSet (Located Var))
- gsDecr :: ![(Var, [Int])]
- gsNonStTerm :: !(HashSet Var)
}
data GhcSpecRefl = SpRefl {
- gsAutoInst :: !(HashMap Var (Maybe Int))
- gsHAxioms :: ![(Var, LocSpecType, Equation)]
- gsImpAxioms :: ![Equation]
- gsMyAxioms :: ![Equation]
- gsReflects :: ![Var]
- gsLogicMap :: !LogicMap
- gsWiredReft :: ![Var]
- gsRewrites :: HashSet (Located Var)
- gsRewritesWith :: HashMap Var [Var]
}
data GhcSpecLaws = SpLaws {
- gsLawDefs :: ![(Class, [(Var, LocSpecType)])]
- gsLawInst :: ![LawInstance]
}
data GhcSpecData = SpData {
- gsCtors :: ![(Var, LocSpecType)]
- gsMeas :: ![(Symbol, LocSpecType)]
- gsInvariants :: ![(Maybe Var, LocSpecType)]
- gsIaliases :: ![(LocSpecType, LocSpecType)]
- gsMeasures :: ![Measure SpecType DataCon]
- gsUnsorted :: ![UnSortedExpr]
}
data GhcSpecQual = SpQual {
- gsQualifiers :: ![Qualifier]
- gsRTAliases :: ![Located SpecRTAlias]
}
type BareDef = Def LocBareType LocSymbol
type BareMeasure = Measure LocBareType LocSymbol
type SpecMeasure = Measure LocSpecType DataCon
type VarOrLocSymbol = Either Var LocSymbol
data LawInstance = LawInstance {
- lilName :: Class
- liSupers :: [LocSpecType]
- lilTyArgs :: [LocSpecType]
- lilEqus :: [(VarOrLocSymbol, (VarOrLocSymbol, Maybe LocSpecType))]
- lilPos :: SrcSpan
}
data GhcSrc = Src {
- _giIncDir :: !FilePath
- _giTarget :: !FilePath
- _giTargetMod :: !ModName
- _giCbs :: ![CoreBind]
- _gsTcs :: ![TyCon]
- _gsCls :: !(Maybe [ClsInst])
- _giDerVars :: !(HashSet Var)
- _giImpVars :: ![Var]
- _giDefVars :: ![Var]
- _giUseVars :: ![Var]
- _gsExports :: !(HashSet StableName)
- _gsFiTcs :: ![TyCon]
- _gsFiDcs :: ![(Symbol, DataCon)]
- _gsPrimTcs :: ![TyCon]
- _gsQualImps :: !QImports
- _gsAllImps :: !(HashSet Symbol)
- _gsTyThings :: ![TyThing]
}
data GhcSpec = SP {
- _gsSig :: !GhcSpecSig
- _gsQual :: !GhcSpecQual
- _gsData :: !GhcSpecData
- _gsName :: !GhcSpecNames
- _gsVars :: !GhcSpecVars
- _gsTerm :: !GhcSpecTerm
- _gsRefl :: !GhcSpecRefl
- _gsLaws :: !GhcSpecLaws
- _gsImps :: ![(Symbol, Sort)]
- _gsConfig :: !Config
- _gsLSpec :: !(Spec LocBareType LocSymbol)
}
targetSrcIso :: Iso' GhcSrc TargetSrc
targetSpecGetter :: Getter GhcSpec (TargetSpec, LiftedSpec)
bareSpecIso :: Iso' (Spec LocBareType LocSymbol) BareSpec
liftedSpecGetter :: Getter (Spec LocBareType LocSymbol) LiftedSpec
unsafeFromLiftedSpec :: LiftedSpec -> Spec LocBareType LocSymbol

Different types of specifications

There are different types or "flavours" for a specification, depending on its lifecycle. The main goal is always the same, i.e. refining the Haskell types and produce a final statement (i.e. safe or unsafe) about the input program. In order to do so, a specification is transformed in the way described by this picture:

    +---------------+                                +-------------------+
    |   BareSpec    |                                |                   |  checked by liquid/liquidOne
    |               |                    ------------|    TargetSpec     |----------------------------- ..
    |(input module) |                   /            |                   |
    +---------------+  makeTargetSpec  /             +-------------------+
           +         -----------------/
    +---------------+                 \              +-------------------+
    | {LiftedSpec}  |                  \             |                   |    serialised on disk
    |               |                   -------------|    LiftedSpec     |----------------------------- ..
    |(dependencies) |                                |                   |
    +---------------+                                +-------------------+
          ^                                                    |
          |                   used-as                          |
          +----------------------------------------------------+

More specifically, we distinguish:

BareSpec - is the specification obtained by parsing the Liquid annotations of the input Haskell file. It typically contains information about the associated input Haskell module, with the exceptions of assumptions that can refer to functions defined in other modules.
LiftedSpec - is the specification we obtain by "lifting" the BareSpec. Most importantly, a LiftedSpec gets serialised on disk and becomes a dependency for the verification of other BareSpecs.

Lifting in this context consist of:

Perform name-resolution (e.g. make all the relevant GHC's Vars qualified, resolve GHC's Names, etc);
Strip the final LiftedSpec with information which are relevant (read: local) to just the input BareSpec. An example would be local signatures, used to annotate internal, auxiliary functions within a Module;
Strip termination checks, which are required (if specified) for a BareSpec but not for the LiftedSpec.

TargetSpec - is the specification we actually use for refinement, and is conceptually an "augmented" BareSpec. You can create a TargetSpec by calling makeTargetSpec.

In order to produce these spec types we have to gather information about the module being compiled by using the GHC API and retain enough context of the compiled Module in order to be able to construct the types introduced aboves. The rest of this module introduced also these intermediate structures.

The following is the overall type for specifications obtained from parsing the target source and dependent libraries. IMPORTANT: A TargetInfo is what is checked by LH itself and it NEVER contains the LiftedSpec, because the checking happens only on the BareSpec of the target module.

data TargetInfo #

Constructors

TargetInfo
Fields giSrc :: !TargetSrc The `TargetSrc` of the module being checked. giSpec :: !TargetSpec The `TargetSpec` of the module being checked.

Instances

Instances details

Show TargetInfo #
Instance details Defined in Language.Haskell.Liquid.GHC.Interface Methods showsPrec :: Int -> TargetInfo -> ShowS # show :: TargetInfo -> String # showList :: [TargetInfo] -> ShowS #
PPrint TargetInfo #
Instance details Defined in Language.Haskell.Liquid.GHC.Interface Methods pprintTidy :: Tidy -> TargetInfo -> Doc # pprintPrec :: Int -> Tidy -> TargetInfo -> Doc #
HasConfig TargetInfo #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods getConfig :: TargetInfo -> Config #

Gathering information about a module

data TargetSrc #

The TargetSrc type is a collection of all the things we know about a module being currently checked. It include things like the name of the module, the list of CoreBinds, the TyCons declared in this module (that includes TyCons for classes), typeclass instances and so and so forth. It might be consider a sort of ModGuts embellished with LH-specific information (for example, giDefVars are populated with datacons from the module plus the let vars derived from the A-normalisation).

Constructors

TargetSrc

Fields

giIncDir :: !FilePath
Path for LH include/prelude directory
giTarget :: !FilePath
Source file for module
giTargetMod :: !ModName
Name for module
giCbs :: ![CoreBind]
Source Code
gsTcs :: ![TyCon]
All used Type constructors
gsCls :: !(Maybe [ClsInst])
Class instances?
giDerVars :: !(HashSet Var)
Binders created by GHC eg dictionaries
giImpVars :: ![Var]
Binders that are _read_ in module (but not defined?)
giDefVars :: ![Var]
(Top-level) binders that are _defined_ in module
giUseVars :: ![Var]
Binders that are _read_ in module
gsExports :: !(HashSet StableName)
Names exported by the module being verified
gsFiTcs :: ![TyCon]
Family instance TyCons
gsFiDcs :: ![(Symbol, DataCon)]
Family instance DataCons
gsPrimTcs :: ![TyCon]
Primitive GHC TyCons (from TysPrim.primTyCons)
gsQualImps :: !QImports
Map of qualified imports
gsAllImps :: !(HashSet Symbol)
Set of _all_ imported modules
gsTyThings :: ![TyThing]
All the TyThings known to GHC

TargetSpec

data TargetSpec #

A TargetSpec is what we actually check via LiquidHaskell. It is created as part of mkTargetSpec alongside the LiftedSpec. It shares a similar structure with a BareSpec, but manipulates and transforms the data in preparation to the checking process.

Constructors

TargetSpec
Fields gsSig :: !GhcSpecSig gsQual :: !GhcSpecQual gsData :: !GhcSpecData gsName :: !GhcSpecNames gsVars :: !GhcSpecVars gsTerm :: !GhcSpecTerm gsRefl :: !GhcSpecRefl gsLaws :: !GhcSpecLaws gsImps :: ![(Symbol, Sort)] Imported Environment gsConfig :: !Config

Instances

Instances details

PPrint TargetSpec #	Pretty Printing -----------------------------------------------------------
Instance details Defined in Language.Haskell.Liquid.GHC.Interface Methods pprintTidy :: Tidy -> TargetSpec -> Doc # pprintPrec :: Int -> Tidy -> TargetSpec -> Doc #
HasConfig TargetSpec #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods getConfig :: TargetSpec -> Config #

BareSpec

newtype BareSpec #

A BareSpec is the spec we derive by parsing the Liquid Haskell annotations of a single file. As such, it contains things which are relevant for validation and lifting; it contains things like the pragmas the user defined, the termination condition (if termination-checking is enabled) and so on and so forth. Crucially, as a BareSpec is still subject to "preflight checks", it may contain duplicates (e.g. duplicate measures, duplicate type declarations etc.) and therefore most of the fields for a BareSpec are lists, so that we can report these errors to the end user: it would be an error to silently ignore the duplication and leave the duplicate resolution to whichever Eq instance is implemented for the relevant field.

Also, a BareSpec has not yet been subject to name resolution, so it may refer to undefined or out-of-scope entities.

Constructors

MkBareSpec
Fields getBareSpec :: Spec LocBareType LocSymbol

Instances

Instances details

Show BareSpec #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods showsPrec :: Int -> BareSpec -> ShowS # show :: BareSpec -> String # showList :: [BareSpec] -> ShowS #
Generic BareSpec #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Associated Types type Rep BareSpec :: Type -> Type # Methods from :: BareSpec -> Rep BareSpec x # to :: Rep BareSpec x -> BareSpec #
Semigroup BareSpec #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods (<>) :: BareSpec -> BareSpec -> BareSpec # sconcat :: NonEmpty BareSpec -> BareSpec # stimes :: Integral b => b -> BareSpec -> BareSpec #
Monoid BareSpec #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods mempty :: BareSpec # mappend :: BareSpec -> BareSpec -> BareSpec # mconcat :: [BareSpec] -> BareSpec #
Binary BareSpec #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods put :: BareSpec -> Put # get :: Get BareSpec # putList :: [BareSpec] -> Put #
type Rep BareSpec #
Instance details Defined in Language.Haskell.Liquid.Types.Specs type Rep BareSpec = D1 ('MetaData "BareSpec" "Language.Haskell.Liquid.Types.Specs" "liquidhaskell-0.8.10.1-inplace" 'True) (C1 ('MetaCons "MkBareSpec" 'PrefixI 'True) (S1 ('MetaSel ('Just "getBareSpec") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Spec LocBareType LocSymbol))))

LiftedSpec

data LiftedSpec #

A LiftedSpec is derived from an input BareSpec and a set of its dependencies. The general motivations for lifting a spec are (a) name resolution, (b) the fact that some info is only relevant for checking the body of functions but does not need to be exported, e.g. termination measures, or the fact that a type signature was assumed. A LiftedSpec is what we serialise on disk and what the clients should will be using.

What we do not have compared to a BareSpec:

The localSigs, as it's not necessary/visible to clients;
The includes, as they are probably not reachable for clients anyway;
The reflSigs, they are now just "normal" signatures;
The lazy, we don't do termination checking in lifted specs;
The reflects, the reflection has already happened at this point;
The hmeas, we have already turned these into measures at this point;
The hbounds, ditto as hmeas;
The inlines, ditto as hmeas;
The ignores, ditto as hmeas;
The pragmas, we can't make any use of this information for lifted specs;
The termexprs, we don't do termination checking in lifted specs;

Apart from less fields, a LiftedSpec replaces all instances of lists with sets, to enforce duplicate detection and removal on what we serialise on disk.

Constructors

LiftedSpec

Fields

liftedMeasures :: HashSet (Measure LocBareType LocSymbol)
User-defined properties for ADTs
liftedImpSigs :: HashSet (Symbol, Sort)
Imported variables types
liftedExpSigs :: HashSet (Symbol, Sort)
Exported variables types
liftedAsmSigs :: HashSet (LocSymbol, LocBareType)
Assumed (unchecked) types; including reflected signatures
liftedSigs :: HashSet (LocSymbol, LocBareType)
Imported functions and types
liftedInvariants :: HashSet (Maybe LocSymbol, LocBareType)
Data type invariants; the Maybe is the generating measure
liftedIaliases :: HashSet (LocBareType, LocBareType)
Data type invariants to be checked
liftedImports :: HashSet Symbol
Loaded spec module names
liftedDataDecls :: HashSet DataDecl
Predicated data definitions
liftedNewtyDecls :: HashSet DataDecl
Predicated new type definitions
liftedAliases :: HashSet (Located (RTAlias Symbol BareType))
RefType aliases
liftedEaliases :: HashSet (Located (RTAlias Symbol Expr))
Expression aliases
liftedEmbeds :: TCEmb LocSymbol
GHC-Tycon-to-fixpoint Tycon map
liftedQualifiers :: HashSet Qualifier
Qualifiers in source/spec files
liftedDecr :: HashSet (LocSymbol, [Int])
Information on decreasing arguments
liftedLvars :: HashSet LocSymbol
Variables that should be checked in the environment they are used
liftedAutois :: HashMap LocSymbol (Maybe Int)
Automatically instantiate axioms in these Functions with maybe specified fuel
liftedAutosize :: HashSet LocSymbol
Type Constructors that get automatically sizing info
liftedCmeasures :: HashSet (Measure LocBareType ())
Measures attached to a type-class
liftedImeasures :: HashSet (Measure LocBareType LocSymbol)
Mappings from (measure,type) -> measure
liftedClasses :: HashSet (RClass LocBareType)
Refined Type-Classes
liftedClaws :: HashSet (RClass LocBareType)
Refined Type-Classe Laws
liftedRinstance :: HashSet (RInstance LocBareType)
liftedIlaws :: HashSet (RILaws LocBareType)
liftedDvariance :: HashSet (LocSymbol, [Variance])
? Where do these come from ?!
liftedBounds :: RRBEnv LocBareType
liftedDefs :: HashMap LocSymbol Symbol
Temporary (?) hack to deal with dictionaries in specifications see testsposNatClass.hs
liftedAxeqs :: HashSet Equation
Equalities used for Proof-By-Evaluation

Instances

Instances details

Eq LiftedSpec #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods (==) :: LiftedSpec -> LiftedSpec -> Bool # (/=) :: LiftedSpec -> LiftedSpec -> Bool #
Show LiftedSpec #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods showsPrec :: Int -> LiftedSpec -> ShowS # show :: LiftedSpec -> String # showList :: [LiftedSpec] -> ShowS #
Generic LiftedSpec #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Associated Types type Rep LiftedSpec :: Type -> Type # Methods from :: LiftedSpec -> Rep LiftedSpec x # to :: Rep LiftedSpec x -> LiftedSpec #
Binary LiftedSpec #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods put :: LiftedSpec -> Put # get :: Get LiftedSpec # putList :: [LiftedSpec] -> Put #
Hashable LiftedSpec #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods hashWithSalt :: Int -> LiftedSpec -> Int hash :: LiftedSpec -> Int
type Rep LiftedSpec #
Instance details Defined in Language.Haskell.Liquid.Types.Specs type Rep LiftedSpec = D1 ('MetaData "LiftedSpec" "Language.Haskell.Liquid.Types.Specs" "liquidhaskell-0.8.10.1-inplace" 'False) (C1 ('MetaCons "LiftedSpec" 'PrefixI 'True) ((((S1 ('MetaSel ('Just "liftedMeasures") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet (Measure LocBareType LocSymbol))) :: (S1 ('MetaSel ('Just "liftedImpSigs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet (Symbol, Sort))) :: S1 ('MetaSel ('Just "liftedExpSigs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet (Symbol, Sort))))) :: ((S1 ('MetaSel ('Just "liftedAsmSigs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet (LocSymbol, LocBareType))) :: S1 ('MetaSel ('Just "liftedSigs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet (LocSymbol, LocBareType)))) :: (S1 ('MetaSel ('Just "liftedInvariants") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet (Maybe LocSymbol, LocBareType))) :: S1 ('MetaSel ('Just "liftedIaliases") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet (LocBareType, LocBareType)))))) :: ((S1 ('MetaSel ('Just "liftedImports") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet Symbol)) :: (S1 ('MetaSel ('Just "liftedDataDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet DataDecl)) :: S1 ('MetaSel ('Just "liftedNewtyDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet DataDecl)))) :: ((S1 ('MetaSel ('Just "liftedAliases") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet (Located (RTAlias Symbol BareType)))) :: S1 ('MetaSel ('Just "liftedEaliases") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet (Located (RTAlias Symbol Expr))))) :: (S1 ('MetaSel ('Just "liftedEmbeds") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TCEmb LocSymbol)) :: S1 ('MetaSel ('Just "liftedQualifiers") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet Qualifier)))))) :: (((S1 ('MetaSel ('Just "liftedDecr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet (LocSymbol, [Int]))) :: (S1 ('MetaSel ('Just "liftedLvars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet LocSymbol)) :: S1 ('MetaSel ('Just "liftedAutois") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap LocSymbol (Maybe Int))))) :: ((S1 ('MetaSel ('Just "liftedAutosize") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet LocSymbol)) :: S1 ('MetaSel ('Just "liftedCmeasures") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet (Measure LocBareType ())))) :: (S1 ('MetaSel ('Just "liftedImeasures") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet (Measure LocBareType LocSymbol))) :: S1 ('MetaSel ('Just "liftedClasses") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet (RClass LocBareType)))))) :: ((S1 ('MetaSel ('Just "liftedClaws") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet (RClass LocBareType))) :: (S1 ('MetaSel ('Just "liftedRinstance") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet (RInstance LocBareType))) :: S1 ('MetaSel ('Just "liftedIlaws") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet (RILaws LocBareType))))) :: ((S1 ('MetaSel ('Just "liftedDvariance") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet (LocSymbol, [Variance]))) :: S1 ('MetaSel ('Just "liftedBounds") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (RRBEnv LocBareType))) :: (S1 ('MetaSel ('Just "liftedDefs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap LocSymbol Symbol)) :*: S1 ('MetaSel ('Just "liftedAxeqs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet Equation))))))))

Tracking dependencies

newtype StableModule #

A newtype wrapper around a Module which:

Allows a Module to be serialised (i.e. it has a Binary instance)
It tries to use stable comparison and equality under the hood.

Constructors

StableModule
Fields unStableModule :: Module

Instances

Instances details

Eq StableModule #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods (==) :: StableModule -> StableModule -> Bool # (/=) :: StableModule -> StableModule -> Bool #
Ord StableModule #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods compare :: StableModule -> StableModule -> Ordering # (<) :: StableModule -> StableModule -> Bool # (<=) :: StableModule -> StableModule -> Bool # (>) :: StableModule -> StableModule -> Bool # (>=) :: StableModule -> StableModule -> Bool # max :: StableModule -> StableModule -> StableModule # min :: StableModule -> StableModule -> StableModule #
Show StableModule #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods showsPrec :: Int -> StableModule -> ShowS # show :: StableModule -> String # showList :: [StableModule] -> ShowS #
Generic StableModule #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Associated Types type Rep StableModule :: Type -> Type # Methods from :: StableModule -> Rep StableModule x # to :: Rep StableModule x -> StableModule #
Binary StableModule #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods put :: StableModule -> Put # get :: Get StableModule # putList :: [StableModule] -> Put #
Hashable StableModule #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods hashWithSalt :: Int -> StableModule -> Int hash :: StableModule -> Int
type Rep StableModule #
Instance details Defined in Language.Haskell.Liquid.Types.Specs type Rep StableModule = D1 ('MetaData "StableModule" "Language.Haskell.Liquid.Types.Specs" "liquidhaskell-0.8.10.1-inplace" 'True) (C1 ('MetaCons "StableModule" 'PrefixI 'True) (S1 ('MetaSel ('Just "unStableModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Module)))

toStableModule :: Module -> StableModule #

Converts a Module into a StableModule.

renderModule :: Module -> String #

newtype TargetDependencies #

The target dependencies that concur to the creation of a TargetSpec and a LiftedSpec.

Constructors

TargetDependencies
Fields getDependencies :: HashMap StableModule LiftedSpec

Instances

Instances details

Eq TargetDependencies #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods (==) :: TargetDependencies -> TargetDependencies -> Bool # (/=) :: TargetDependencies -> TargetDependencies -> Bool #
Show TargetDependencies #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods showsPrec :: Int -> TargetDependencies -> ShowS # show :: TargetDependencies -> String # showList :: [TargetDependencies] -> ShowS #
Generic TargetDependencies #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Associated Types type Rep TargetDependencies :: Type -> Type # Methods from :: TargetDependencies -> Rep TargetDependencies x # to :: Rep TargetDependencies x -> TargetDependencies #
Semigroup TargetDependencies #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods (<>) :: TargetDependencies -> TargetDependencies -> TargetDependencies # sconcat :: NonEmpty TargetDependencies -> TargetDependencies # stimes :: Integral b => b -> TargetDependencies -> TargetDependencies #
Monoid TargetDependencies #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods mempty :: TargetDependencies # mappend :: TargetDependencies -> TargetDependencies -> TargetDependencies # mconcat :: [TargetDependencies] -> TargetDependencies #
Binary TargetDependencies #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods put :: TargetDependencies -> Put # get :: Get TargetDependencies # putList :: [TargetDependencies] -> Put #
type Rep TargetDependencies #
Instance details Defined in Language.Haskell.Liquid.Types.Specs type Rep TargetDependencies = D1 ('MetaData "TargetDependencies" "Language.Haskell.Liquid.Types.Specs" "liquidhaskell-0.8.10.1-inplace" 'True) (C1 ('MetaCons "TargetDependencies" 'PrefixI 'True) (S1 ('MetaSel ('Just "getDependencies") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap StableModule LiftedSpec))))

dropDependency :: StableModule -> TargetDependencies -> TargetDependencies #

Drop the given StableModule from the dependencies.

Predicates on spec types

isPLEVar :: TargetSpec -> Var -> Bool #

Returns True if the input Var is a PLE one.

isExportedVar :: TargetSrc -> Var -> Bool #

Returns True if the input Var was exported in the module the input TargetSrc represents.

Other types

data QImports #

QImports is a map of qualified imports.

Constructors

QImports
Fields qiModules :: !(HashSet Symbol) All the modules that are imported qualified qiNames :: !(HashMap Symbol [Symbol]) Map from qualification to full module name

Instances

Instances details

Show QImports #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods showsPrec :: Int -> QImports -> ShowS # show :: QImports -> String # showList :: [QImports] -> ShowS #

data Spec ty bndr #

A generic Spec type, polymorphic over the inner choice of type and binder.

Constructors

Spec

Fields

measures :: ![Measure ty bndr]
User-defined properties for ADTs
impSigs :: ![(Symbol, Sort)]
Imported variables types
expSigs :: ![(Symbol, Sort)]
Exported variables types
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 :: ![(Maybe LocSymbol, ty)]
Data type invariants; the Maybe is the generating measure
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 :: ![Located (RTAlias Symbol BareType)]
RefType aliases
ealiases :: ![Located (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 :: !(HashSet LocSymbol)
Variables that should be checked in the environment they are used
lazy :: !(HashSet LocSymbol)
Ignore Termination Check in these Functions
rewrites :: !(HashSet LocSymbol)
Theorems turned into rewrite rules
rewriteWith :: !(HashMap LocSymbol [LocSymbol])
Definitions using rewrite rules
fails :: !(HashSet LocSymbol)
These Functions should be unsafe
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
ignores :: !(HashSet LocSymbol)
Binders to ignore during checking; that is DON't check the corebind.
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
claws :: ![RClass ty]
Refined Type-Classe Laws
termexprs :: ![(LocSymbol, [Located Expr])]
Terminating Conditions for functions
rinstance :: ![RInstance ty]
ilaws :: ![RILaws 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 :: ![Equation]
Equalities used for Proof-By-Evaluation

Instances

Instances details

Qualify BareSpec #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareSpec -> BareSpec #
Qualify ModSpecs #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> ModSpecs -> ModSpecs #
(PPrint ty, PPrint bndr, Show ty) => Show (Spec ty bndr) #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods showsPrec :: Int -> Spec ty bndr -> ShowS # show :: Spec ty bndr -> String # showList :: [Spec ty bndr] -> ShowS #
Generic (Spec ty bndr) #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Associated Types type Rep (Spec ty bndr) :: Type -> Type # Methods from :: Spec ty bndr -> Rep (Spec ty bndr) x # to :: Rep (Spec ty bndr) x -> Spec ty bndr #
Semigroup (Spec ty bndr) #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods (<>) :: Spec ty bndr -> Spec ty bndr -> Spec ty bndr # sconcat :: NonEmpty (Spec ty bndr) -> Spec ty bndr # stimes :: Integral b => b -> Spec ty bndr -> Spec ty bndr #
Monoid (Spec ty bndr) #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods mempty :: Spec ty bndr # mappend :: Spec ty bndr -> Spec ty bndr -> Spec ty bndr # mconcat :: [Spec ty bndr] -> Spec ty bndr #
Binary (Spec LocBareType LocSymbol) #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods put :: Spec LocBareType LocSymbol -> Put # get :: Get (Spec LocBareType LocSymbol) # putList :: [Spec LocBareType LocSymbol] -> Put #
(Show ty, Show bndr, PPrint ty, PPrint bndr) => PPrint (Spec ty bndr) #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods pprintTidy :: Tidy -> Spec ty bndr -> Doc # pprintPrec :: Int -> Tidy -> Spec ty bndr -> Doc #
type Rep (Spec ty bndr) #
Instance details Defined in Language.Haskell.Liquid.Types.Specs type Rep (Spec ty bndr) = D1 ('MetaData "Spec" "Language.Haskell.Liquid.Types.Specs" "liquidhaskell-0.8.10.1-inplace" 'False) (C1 ('MetaCons "Spec" 'PrefixI 'True) (((((S1 ('MetaSel ('Just "measures") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Measure ty bndr]) :: S1 ('MetaSel ('Just "impSigs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(Symbol, Sort)])) :: (S1 ('MetaSel ('Just "expSigs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(Symbol, Sort)]) :: (S1 ('MetaSel ('Just "asmSigs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(LocSymbol, ty)]) :: S1 ('MetaSel ('Just "sigs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(LocSymbol, ty)])))) :: ((S1 ('MetaSel ('Just "localSigs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(LocSymbol, ty)]) :: S1 ('MetaSel ('Just "reflSigs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(LocSymbol, ty)])) :: (S1 ('MetaSel ('Just "invariants") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(Maybe LocSymbol, ty)]) :: (S1 ('MetaSel ('Just "ialiases") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(ty, ty)]) :: S1 ('MetaSel ('Just "imports") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Symbol]))))) :: (((S1 ('MetaSel ('Just "dataDecls") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [DataDecl]) :: S1 ('MetaSel ('Just "newtyDecls") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [DataDecl])) :: (S1 ('MetaSel ('Just "includes") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [FilePath]) :: (S1 ('MetaSel ('Just "aliases") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Located (RTAlias Symbol BareType)]) :: S1 ('MetaSel ('Just "ealiases") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Located (RTAlias Symbol Expr)])))) :: ((S1 ('MetaSel ('Just "embeds") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (TCEmb LocSymbol)) :: (S1 ('MetaSel ('Just "qualifiers") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Qualifier]) :: S1 ('MetaSel ('Just "decr") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(LocSymbol, [Int])]))) :: (S1 ('MetaSel ('Just "lvars") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol)) :: (S1 ('MetaSel ('Just "lazy") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol)) :: S1 ('MetaSel ('Just "rewrites") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol))))))) :: ((((S1 ('MetaSel ('Just "rewriteWith") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashMap LocSymbol [LocSymbol])) :: S1 ('MetaSel ('Just "fails") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol))) :: (S1 ('MetaSel ('Just "reflects") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol)) :: (S1 ('MetaSel ('Just "autois") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashMap LocSymbol (Maybe Int))) :: S1 ('MetaSel ('Just "hmeas") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol))))) :: ((S1 ('MetaSel ('Just "hbounds") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol)) :: S1 ('MetaSel ('Just "inlines") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol))) :: (S1 ('MetaSel ('Just "ignores") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol)) :: (S1 ('MetaSel ('Just "autosize") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol)) :: S1 ('MetaSel ('Just "pragmas") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Located String]))))) :: (((S1 ('MetaSel ('Just "cmeasures") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Measure ty ()]) :: S1 ('MetaSel ('Just "imeasures") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Measure ty bndr])) :: (S1 ('MetaSel ('Just "classes") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [RClass ty]) :: (S1 ('MetaSel ('Just "claws") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [RClass ty]) :: S1 ('MetaSel ('Just "termexprs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(LocSymbol, [Located Expr])])))) :: ((S1 ('MetaSel ('Just "rinstance") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [RInstance ty]) :: (S1 ('MetaSel ('Just "ilaws") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [RILaws ty]) :: S1 ('MetaSel ('Just "dvariance") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(LocSymbol, [Variance])]))) :: (S1 ('MetaSel ('Just "bounds") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (RRBEnv ty)) :: (S1 ('MetaSel ('Just "defs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashMap LocSymbol Symbol)) :*: S1 ('MetaSel ('Just "axeqs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Equation]))))))))

data GhcSpecVars #

The collection of GHC Vars that a TargetSpec needs to verify (or skip).

Constructors

SpVar
Fields gsTgtVars :: ![Var] Top-level Binders To Verify (empty means ALL binders) gsIgnoreVars :: !(HashSet Var) Top-level Binders To NOT Verify (empty means ALL binders) gsLvars :: !(HashSet Var) Variables that should be checked "lazily" in the environment they are used gsCMethods :: ![Var] Refined Class methods

data GhcSpecSig #

Constructors

SpSig

Fields

gsTySigs :: ![(Var, LocSpecType)]
Asserted Reftypes
gsAsmSigs :: ![(Var, LocSpecType)]
Assumed Reftypes
gsRefSigs :: ![(Var, LocSpecType)]
Reflected Reftypes
gsInSigs :: ![(Var, LocSpecType)]
Auto generated Signatures
gsNewTypes :: ![(TyCon, LocSpecType)]
Mapping of 'newtype' type constructors with their refined types.
gsDicts :: !(DEnv Var LocSpecType)
Refined Classes from Instances
gsMethods :: ![(Var, MethodType LocSpecType)]
Refined Classes from Classes
gsTexprs :: ![(Var, LocSpecType, [Located Expr])]
Lexicographically ordered expressions for termination

data GhcSpecNames #

Constructors

SpNames

Fields

gsFreeSyms :: ![(Symbol, Var)]
List of Symbol free in spec and corresponding GHC var, eg. (Cons, Cons#7uz) from testsposex1.hs
gsDconsP :: ![Located DataCon]
Predicated Data-Constructors, e.g. see testsposMap.hs
gsTconsP :: ![TyConP]
Predicated Type-Constructors, e.g. see testsposMap.hs
gsTcEmbeds :: !(TCEmb TyCon)
Embedding GHC Tycons into fixpoint sorts e.g. "embed Set as Set_set" from includeDataSet.spec
gsADTs :: ![DataDecl]
ADTs extracted from Haskell 'data' definitions
gsTyconEnv :: !TyConMap

data GhcSpecTerm #

Constructors

SpTerm

Fields

gsStTerm :: !(HashSet Var)
Binders to CHECK by structural termination
gsAutosize :: !(HashSet TyCon)
Binders to IGNORE during termination checking
gsLazy :: !(HashSet Var)
Binders to IGNORE during termination checking
gsFail :: !(HashSet (Located Var))
Binders to fail type checking
gsDecr :: ![(Var, [Int])]
Lexicographic order of decreasing args (DEPRECATED)
gsNonStTerm :: !(HashSet Var)
Binders to CHECK using REFINEMENT-TYPES/termination metrics

data GhcSpecRefl #

Constructors

SpRefl

Fields

gsAutoInst :: !(HashMap Var (Maybe Int))
Binders to USE PLE
gsHAxioms :: ![(Var, LocSpecType, Equation)]
Lifted definitions
gsImpAxioms :: ![Equation]
Axioms from imported reflected functions
gsMyAxioms :: ![Equation]
Axioms from my reflected functions
gsReflects :: ![Var]
Binders for reflected functions
gsLogicMap :: !LogicMap
gsWiredReft :: ![Var]
gsRewrites :: HashSet (Located Var)
gsRewritesWith :: HashMap Var [Var]

data GhcSpecLaws #

Constructors

SpLaws
Fields gsLawDefs :: ![(Class, [(Var, LocSpecType)])] gsLawInst :: ![LawInstance]

data GhcSpecData #

Constructors

SpData

Fields

gsCtors :: ![(Var, LocSpecType)]
Data Constructor Measure Sigs
gsMeas :: ![(Symbol, LocSpecType)]
Measure Types eg. len :: [a] -> Int
gsInvariants :: ![(Maybe Var, LocSpecType)]
Data type invariants from measure definitions, e.g forall a. {v: [a] | len(v) >= 0}
gsIaliases :: ![(LocSpecType, LocSpecType)]
Data type invariant aliases
gsMeasures :: ![Measure SpecType DataCon]
Measure definitions
gsUnsorted :: ![UnSortedExpr]

data GhcSpecQual #

Constructors

SpQual
Fields gsQualifiers :: ![Qualifier] Qualifiers in SourceSpec files e.g testspos/qualTest.hs gsRTAliases :: ![Located SpecRTAlias] Refinement type aliases (only used for qualifiers)

type BareDef = Def LocBareType LocSymbol #

type BareMeasure = Measure LocBareType LocSymbol #

type SpecMeasure = Measure LocSpecType DataCon #

type VarOrLocSymbol = Either Var LocSymbol #

data LawInstance #

Constructors

LawInstance
Fields lilName :: Class liSupers :: [LocSpecType] lilTyArgs :: [LocSpecType] lilEqus :: [(VarOrLocSymbol, (VarOrLocSymbol, Maybe LocSpecType))] lilPos :: SrcSpan

Legacy data structures

data GhcSrc #

Constructors

Src

Fields

_giIncDir :: !FilePath
Path for LH include/prelude directory
_giTarget :: !FilePath
Source file for module
_giTargetMod :: !ModName
Name for module
_giCbs :: ![CoreBind]
Source Code
_gsTcs :: ![TyCon]
All used Type constructors
_gsCls :: !(Maybe [ClsInst])
Class instances?
_giDerVars :: !(HashSet Var)
Binders created by GHC eg dictionaries
_giImpVars :: ![Var]
Binders that are _read_ in module (but not defined?)
_giDefVars :: ![Var]
(Top-level) binders that are _defined_ in module
_giUseVars :: ![Var]
Binders that are _read_ in module
_gsExports :: !(HashSet StableName)
Names exported by the module being verified
_gsFiTcs :: ![TyCon]
Family instance TyCons
_gsFiDcs :: ![(Symbol, DataCon)]
Family instance DataCons
_gsPrimTcs :: ![TyCon]
Primitive GHC TyCons (from TysPrim.primTyCons)
_gsQualImps :: !QImports
Map of qualified imports
_gsAllImps :: !(HashSet Symbol)
Set of _all_ imported modules
_gsTyThings :: ![TyThing]
All the TyThings known to GHC

data GhcSpec #

Constructors

SP
Fields _gsSig :: !GhcSpecSig _gsQual :: !GhcSpecQual _gsData :: !GhcSpecData _gsName :: !GhcSpecNames _gsVars :: !GhcSpecVars _gsTerm :: !GhcSpecTerm _gsRefl :: !GhcSpecRefl _gsLaws :: !GhcSpecLaws _gsImps :: ![(Symbol, Sort)] Imported Environment _gsConfig :: !Config _gsLSpec :: !(Spec LocBareType LocSymbol) Lifted specification for the target module

Instances

Instances details

HasConfig GhcSpec #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods getConfig :: GhcSpec -> Config #

Provisional compatibility exports & optics

In order to smooth out the migration process to this API, here we provide some compat Iso and Prism to convert from/to the old data structures, so that migration can be done organically over time.

targetSrcIso :: Iso' GhcSrc TargetSrc #

targetSpecGetter :: Getter GhcSpec (TargetSpec, LiftedSpec) #

bareSpecIso :: Iso' (Spec LocBareType LocSymbol) BareSpec #

liftedSpecGetter :: Getter (Spec LocBareType LocSymbol) LiftedSpec #

unsafeFromLiftedSpec :: LiftedSpec -> Spec LocBareType LocSymbol #