| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Haskell.Liquid.Types.Specs
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 {}
- 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 {}
- toStableModule :: Module -> StableModule
- renderModule :: Module -> String
- newtype TargetDependencies = TargetDependencies {}
- dropDependency :: StableModule -> TargetDependencies -> TargetDependencies
- isPLEVar :: TargetSpec -> Var -> Bool
- isExportedVar :: TargetSrc -> Var -> Bool
- data QImports = QImports {}
- 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 {}
- 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" theBareSpec. Most importantly, aLiftedSpecgets serialised on disk and becomes a dependency for the verification of otherBareSpecs.
Lifting in this context consist of:
- Perform name-resolution (e.g. make all the relevant GHC's
Vars qualified, resolve GHC'sNames, etc); - Strip the final
LiftedSpecwith information which are relevant (read: local) to just the inputBareSpec. An example would be local signatures, used to annotate internal, auxiliary functions within aModule; - Strip termination checks, which are required (if specified) for a
BareSpecbut not for theLiftedSpec.
TargetSpec- is the specification we actually use for refinement, and is conceptually an "augmented"BareSpec. You can create aTargetSpecby callingmakeTargetSpec.
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 Source #
Constructors
| TargetInfo | |
Fields
| |
Instances
| Show TargetInfo Source # | |
Defined in Language.Haskell.Liquid.GHC.Interface Methods showsPrec :: Int -> TargetInfo -> ShowS # show :: TargetInfo -> String # showList :: [TargetInfo] -> ShowS # | |
| PPrint TargetInfo Source # | |
Defined in Language.Haskell.Liquid.GHC.Interface | |
| HasConfig TargetInfo Source # | |
Defined in Language.Haskell.Liquid.Types.Specs Methods getConfig :: TargetInfo -> Config Source # | |
Gathering information about a module
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
| |
TargetSpec
data TargetSpec Source #
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
| |
Instances
| PPrint TargetSpec Source # | Pretty Printing ----------------------------------------------------------- |
Defined in Language.Haskell.Liquid.GHC.Interface | |
| HasConfig TargetSpec Source # | |
Defined in Language.Haskell.Liquid.Types.Specs Methods getConfig :: TargetSpec -> Config Source # | |
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 | |
Instances
| Show BareSpec Source # | |
| Generic BareSpec Source # | |
| Semigroup BareSpec Source # | |
| Monoid BareSpec Source # | |
| Binary BareSpec Source # | |
| type Rep BareSpec Source # | |
Defined in Language.Haskell.Liquid.Types.Specs type Rep BareSpec = D1 ('MetaData "BareSpec" "Language.Haskell.Liquid.Types.Specs" "liquidhaskell-0.8.10.2-L92dB1QZcuO9sqg2FFZRKf" 'True) (C1 ('MetaCons "MkBareSpec" 'PrefixI 'True) (S1 ('MetaSel ('Just "getBareSpec") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Spec LocBareType LocSymbol)))) | |
LiftedSpec
data LiftedSpec Source #
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 ashmeas; - The
inlines, ditto ashmeas; - The
ignores, ditto ashmeas; - 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
| |
Instances
Tracking dependencies
newtype StableModule Source #
A newtype wrapper around a Module which:
Constructors
| StableModule | |
Fields | |
Instances
toStableModule :: Module -> StableModule Source #
Converts a Module into a StableModule.
renderModule :: Module -> String Source #
newtype TargetDependencies Source #
The target dependencies that concur to the creation of a TargetSpec and a LiftedSpec.
Constructors
| TargetDependencies | |
Fields | |
Instances
dropDependency :: StableModule -> TargetDependencies -> TargetDependencies Source #
Drop the given StableModule from the dependencies.
Predicates on spec types
Other types
A generic Spec type, polymorphic over the inner choice of type and binder.
Constructors
| Spec | |
Fields
| |
Instances
data GhcSpecVars Source #
The collection of GHC Vars that a TargetSpec needs to verify (or skip).
Constructors
| SpVar | |
Fields
| |
data GhcSpecSig Source #
Constructors
| SpSig | |
Fields
| |
data GhcSpecNames Source #
Constructors
| SpNames | |
Fields
| |
data GhcSpecTerm Source #
Constructors
| SpTerm | |
Fields
| |
data GhcSpecRefl Source #
Constructors
| SpRefl | |
Fields
| |
data GhcSpecLaws Source #
Constructors
| SpLaws | |
Fields
| |
data GhcSpecData Source #
Constructors
| SpData | |
Fields
| |
data GhcSpecQual Source #
Constructors
| SpQual | |
Fields
| |
type BareMeasure = Measure LocBareType LocSymbol Source #
type SpecMeasure = Measure LocSpecType DataCon Source #
data LawInstance Source #
Constructors
| LawInstance | |
Fields
| |
Legacy data structures
Constructors
| Src | |
Fields
| |
Constructors
| SP | |
Fields
| |