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
Orphan instances

Description

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

Synopsis

data TargetInfo = TargetInfo {
- giSrc :: !TargetSrc
- giSpec :: !TargetSpec
}
data TargetSrc = TargetSrc {
- 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]
}
data TargetSpec = TargetSpec {
- gsSig :: !GhcSpecSig
- gsQual :: !GhcSpecQual
- gsData :: !GhcSpecData
- gsName :: !GhcSpecNames
- gsVars :: !GhcSpecVars
- gsTerm :: !GhcSpecTerm
- gsRefl :: !GhcSpecRefl
- gsImps :: ![(Symbol, Sort)]
- gsConfig :: !Config
}
type BareSpec = Spec Symbol BareType
type BareSpecLHName = Spec LHName BareTypeLHName
type BareSpecParsed = Spec LocSymbol BareTypeParsed
data LiftedSpec = LiftedSpec {
- liftedMeasures :: HashMap Symbol (MeasureV LHName LocBareTypeLHName (Located LHName))
- liftedExpSigs :: HashSet (LHName, Sort)
- liftedPrivateReflects :: HashSet LocSymbol
- liftedAsmSigs :: HashSet (Located LHName, LocBareTypeLHName)
- liftedSigs :: HashSet (Located LHName, LocBareTypeLHName)
- liftedInvariants :: HashSet (Maybe LocSymbol, LocBareTypeLHName)
- liftedIaliases :: HashSet (LocBareTypeLHName, LocBareTypeLHName)
- liftedDataDecls :: HashSet DataDeclLHName
- liftedNewtyDecls :: HashSet DataDeclLHName
- liftedAliases :: HashSet (Located (RTAlias Symbol BareTypeLHName))
- liftedEaliases :: HashSet (Located (RTAlias Symbol (ExprV LHName)))
- liftedEmbeds :: TCEmb (Located LHName)
- liftedQualifiers :: HashSet (QualifierV LHName)
- liftedLvars :: HashSet (Located LHName)
- liftedAutois :: HashSet (Located LHName)
- liftedAutosize :: HashSet (Located LHName)
- liftedCmeasures :: HashMap Symbol (MeasureV LHName LocBareTypeLHName ())
- liftedImeasures :: HashSet (MeasureV LHName LocBareTypeLHName (Located LHName))
- liftedOmeasures :: HashSet (MeasureV LHName LocBareTypeLHName (Located LHName))
- liftedClasses :: HashSet (RClass LocBareTypeLHName)
- liftedRinstance :: HashSet (RInstance LocBareTypeLHName)
- liftedDsize :: [([LocBareTypeLHName], LHName)]
- liftedDvariance :: HashSet (Located LHName, [Variance])
- liftedBounds :: RRBEnvV LHName LocBareTypeLHName
- liftedAxeqs :: HashSet (EquationV LHName)
- liftedDefines :: HashMap Symbol (LMapV LHName)
- liftedUsedDataCons :: HashSet LHName
}
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 lname ty = Spec {
- measures :: ![MeasureV lname (Located ty) (Located LHName)]
- expSigs :: ![(lname, Sort)]
- asmSigs :: ![(Located LHName, Located ty)]
- asmReflectSigs :: ![(Located LHName, Located LHName)]
- sigs :: ![(Located LHName, Located (BareTypeV lname))]
- invariants :: ![(Maybe LocSymbol, Located ty)]
- ialiases :: ![(Located ty, Located ty)]
- dataDecls :: ![DataDeclP lname ty]
- newtyDecls :: ![DataDeclP lname ty]
- aliases :: ![Located (RTAlias Symbol (BareTypeV lname))]
- ealiases :: ![Located (RTAlias Symbol (ExprV lname))]
- embeds :: !(TCEmb (Located LHName))
- qualifiers :: ![QualifierV lname]
- lvars :: !(HashSet (Located LHName))
- lazy :: !(HashSet (Located LHName))
- rewrites :: !(HashSet (Located LHName))
- rewriteWith :: !(HashMap (Located LHName) [Located LHName])
- fails :: !(HashSet (Located LHName))
- reflects :: !(HashSet (Located LHName))
- privateReflects :: !(HashSet LocSymbol)
- opaqueReflects :: !(HashSet (Located LHName))
- autois :: !(HashSet (Located LHName))
- hmeas :: !(HashSet (Located LHName))
- inlines :: !(HashSet (Located LHName))
- ignores :: !(HashSet (Located LHName))
- autosize :: !(HashSet (Located LHName))
- pragmas :: ![Located String]
- cmeasures :: ![MeasureV lname (Located ty) ()]
- imeasures :: ![MeasureV lname (Located ty) (Located LHName)]
- omeasures :: ![MeasureV lname (Located ty) (Located LHName)]
- classes :: ![RClass (Located ty)]
- relational :: ![(Located LHName, Located LHName, Located (BareTypeV lname), Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
- asmRel :: ![(Located LHName, Located LHName, Located (BareTypeV lname), Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
- termexprs :: ![(Located LHName, [Located (ExprV lname)])]
- rinstance :: ![RInstance (Located ty)]
- dvariance :: ![(Located LHName, [Variance])]
- dsize :: ![([Located ty], lname)]
- bounds :: !(RRBEnvV lname (Located ty))
- axeqs :: ![EquationV lname]
- defines :: ![(Located LHName, LMapV lname)]
- usedDataCons :: HashSet LHName
}
data GhcSpecVars = SpVar {
- gsTgtVars :: ![Var]
- gsIgnoreVars :: !(HashSet Var)
- gsLvars :: !(HashSet Var)
- gsCMethods :: ![Var]
}
data GhcSpecSig = SpSig {
- gsTySigs :: ![(Var, LocSpecType)]
- gsAsmSigs :: ![(Var, LocSpecType)]
- gsAsmReflects :: ![(Var, Var)]
- gsRefSigs :: ![(Var, LocSpecType)]
- gsInSigs :: ![(Var, LocSpecType)]
- gsNewTypes :: ![(TyCon, LocSpecType)]
- gsDicts :: !(DEnv Var LocSpecType)
- gsMethods :: ![(Var, MethodType LocSpecType)]
- gsTexprs :: ![(Var, LocSpecType, [Located Expr])]
- gsRelation :: ![(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]
- gsAsmRel :: ![(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]
}
data GhcSpecNames = SpNames {
- gsDconsP :: ![Located DataCon]
- gsTconsP :: ![TyConP]
- gsTcEmbeds :: !(TCEmb TyCon)
- gsADTs :: ![DataDecl]
- gsTyconEnv :: !TyConMap
- gsDataConIds :: [Var]
}
data GhcSpecTerm = SpTerm {
- gsStTerm :: !(HashSet Var)
- gsAutosize :: !(HashSet TyCon)
- gsLazy :: !(HashSet Var)
- gsFail :: !(HashSet (Located Var))
- gsNonStTerm :: !(HashSet Var)
}
data GhcSpecRefl = SpRefl {
- gsAutoInst :: !(HashSet Var)
- gsHAxioms :: ![(Var, LocSpecType, Equation)]
- gsImpAxioms :: ![Equation]
- gsMyAxioms :: ![Equation]
- gsReflects :: ![Var]
- gsLogicMap :: !LogicMap
- gsRewrites :: HashSet (Located Var)
- gsRewritesWith :: HashMap Var [Var]
}
data GhcSpecData = SpData {
- gsCtors :: ![(Var, LocSpecType)]
- gsMeas :: ![(Symbol, LocSpecType)]
- gsInvariants :: ![(Maybe Var, LocSpecType)]
- gsIaliases :: ![(LocSpecType, LocSpecType)]
- gsMeasures :: ![Measure SpecType DataCon]
- gsOpaqueRefls :: ![Var]
- gsUnsorted :: ![UnSortedExpr]
}
data GhcSpecQual = SpQual {
- gsQualifiers :: ![Qualifier]
- gsRTAliases :: ![Located SpecRTAlias]
}
type BareDef = Def LocBareType (Located LHName)
type BareMeasure = Measure LocBareType (Located LHName)
type SpecMeasure = Measure LocSpecType DataCon
type VarOrLocSymbol = Either Var LocSymbol
emapSpecM :: Monad m => Bool -> (LHName -> [Symbol]) -> ([Symbol] -> lname0 -> m lname1) -> ([Symbol] -> ty0 -> m ty1) -> Spec lname0 ty0 -> m (Spec lname1 ty1)
fromBareSpecLHName :: BareSpecLHName -> BareSpec
fromBareSpecParsed :: BareSpecParsed -> BareSpec
mapSpecLName :: (lname0 -> lname1) -> Spec lname0 ty -> Spec lname1 ty
mapSpecTy :: (ty0 -> ty1) -> Spec lname ty0 -> Spec lname ty1
data GhcSrc = Src {
- _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]
}
data GhcSpec = SP {
- _gsSig :: !GhcSpecSig
- _gsQual :: !GhcSpecQual
- _gsData :: !GhcSpecData
- _gsName :: !GhcSpecNames
- _gsVars :: !GhcSpecVars
- _gsTerm :: !GhcSpecTerm
- _gsRefl :: !GhcSpecRefl
- _gsImps :: ![(Symbol, Sort)]
- _gsConfig :: !Config
- _gsLSpec :: !(Spec Symbol BareType)
}
toTargetSrc :: GhcSrc -> TargetSrc
fromTargetSrc :: TargetSrc -> GhcSrc
toTargetSpec :: GhcSpec -> TargetSpec
toLiftedSpec :: BareSpecLHName -> LiftedSpec
unsafeFromLiftedSpec :: LiftedSpec -> BareSpecLHName
emptyLiftedSpec :: LiftedSpec

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 Source #

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

Gathering information about a module

data TargetSrc Source #

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

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)

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 gsSig :: !GhcSpecSig gsQual :: !GhcSpecQual gsData :: !GhcSpecData gsName :: !GhcSpecNames gsVars :: !GhcSpecVars gsTerm :: !GhcSpecTerm gsRefl :: !GhcSpecRefl gsImps :: ![(Symbol, Sort)] Imported Environment gsConfig :: !Config

Instances

Instances details

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

BareSpec

type BareSpec = Spec Symbol BareType Source #

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.

type BareSpecLHName = Spec LHName BareTypeLHName Source #

type BareSpecParsed = Spec LocSymbol BareTypeParsed Source #

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 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 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 :: HashMap Symbol (MeasureV LHName LocBareTypeLHName (Located LHName))
Measures (a.k.a. user-defined properties for ADTs)
The key of the HashMap is the unqualified name of the measure. Constructing such a map discards preceding measures with the same name as later measures, which makes possible to predict which of a few conflicting measures will be exported.
Tested in MeasureOverlapC.hs
liftedExpSigs :: HashSet (LHName, Sort)
Exported logic symbols originated from reflecting functions
liftedPrivateReflects :: HashSet LocSymbol
Private functions that have been reflected
liftedAsmSigs :: HashSet (Located LHName, LocBareTypeLHName)
Assumed (unchecked) types; including reflected signatures
liftedSigs :: HashSet (Located LHName, LocBareTypeLHName)
Asserted spec signatures
liftedInvariants :: HashSet (Maybe LocSymbol, LocBareTypeLHName)
Data type invariants; the Maybe is the generating measure
liftedIaliases :: HashSet (LocBareTypeLHName, LocBareTypeLHName)
Data type invariants to be checked
liftedDataDecls :: HashSet DataDeclLHName
Predicated data definitions
liftedNewtyDecls :: HashSet DataDeclLHName
Predicated new type definitions
liftedAliases :: HashSet (Located (RTAlias Symbol BareTypeLHName))
RefType aliases
liftedEaliases :: HashSet (Located (RTAlias Symbol (ExprV LHName)))
Expression aliases
liftedEmbeds :: TCEmb (Located LHName)
GHC-Tycon-to-fixpoint Tycon map
liftedQualifiers :: HashSet (QualifierV LHName)
Qualifiers in source/spec files
liftedLvars :: HashSet (Located LHName)
Variables that should be checked in the environment they are used
liftedAutois :: HashSet (Located LHName)
Automatically instantiate axioms in these Functions
liftedAutosize :: HashSet (Located LHName)
Type Constructors that get automatically sizing info
liftedCmeasures :: HashMap Symbol (MeasureV LHName LocBareTypeLHName ())
Measures attached to a type-class
Imitates the arrangement for liftedMeasures
liftedImeasures :: HashSet (MeasureV LHName LocBareTypeLHName (Located LHName))
Mappings from (measure,type) -> measure
liftedOmeasures :: HashSet (MeasureV LHName LocBareTypeLHName (Located LHName))
Lifted opaque reflection measures
liftedClasses :: HashSet (RClass LocBareTypeLHName)
Refined Type-Classes
liftedRinstance :: HashSet (RInstance LocBareTypeLHName)
liftedDsize :: [([LocBareTypeLHName], LHName)]
liftedDvariance :: HashSet (Located LHName, [Variance])
? Where do these come from ?!
liftedBounds :: RRBEnvV LHName LocBareTypeLHName
liftedAxeqs :: HashSet (EquationV LHName)
Equalities used for Proof-By-Evaluation
liftedDefines :: HashMap Symbol (LMapV LHName)
Logic aliases
liftedUsedDataCons :: HashSet LHName
Data constructors used in specs

Instances

Instances details

Binary LiftedSpec Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Methods

put :: LiftedSpec -> Put #

get :: Get LiftedSpec #

putList :: [LiftedSpec] -> Put #

Data LiftedSpec Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LiftedSpec -> c LiftedSpec #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LiftedSpec #

toConstr :: LiftedSpec -> Constr #

dataTypeOf :: LiftedSpec -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LiftedSpec) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LiftedSpec) #

gmapT :: (forall b. Data b => b -> b) -> LiftedSpec -> LiftedSpec #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LiftedSpec -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LiftedSpec -> r #

gmapQ :: (forall d. Data d => d -> u) -> LiftedSpec -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> LiftedSpec -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LiftedSpec -> m LiftedSpec #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LiftedSpec -> m LiftedSpec #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LiftedSpec -> m LiftedSpec #

Generic LiftedSpec Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Associated Types

type Rep LiftedSpec

Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Methods

from :: LiftedSpec -> Rep LiftedSpec x #

to :: Rep LiftedSpec x -> LiftedSpec #

Show LiftedSpec Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Methods

showsPrec :: Int -> LiftedSpec -> ShowS #

show :: LiftedSpec -> String #

showList :: [LiftedSpec] -> ShowS #

Eq LiftedSpec Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Methods

(==) :: LiftedSpec -> LiftedSpec -> Bool #

(/=) :: LiftedSpec -> LiftedSpec -> Bool #

Hashable LiftedSpec Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Methods

hashWithSalt :: Int -> LiftedSpec -> Int #

hash :: LiftedSpec -> Int #

type Rep LiftedSpec Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Tracking dependencies

newtype TargetDependencies Source #

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

Constructors

TargetDependencies
Fields getDependencies :: HashMap StableModule LiftedSpec

Instances

Instances details

Binary TargetDependencies Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Methods

put :: TargetDependencies -> Put #

get :: Get TargetDependencies #

putList :: [TargetDependencies] -> Put #

Monoid TargetDependencies Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Methods

mempty :: TargetDependencies #

mappend :: TargetDependencies -> TargetDependencies -> TargetDependencies #

mconcat :: [TargetDependencies] -> TargetDependencies #

Semigroup TargetDependencies Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Methods

(<>) :: TargetDependencies -> TargetDependencies -> TargetDependencies #

sconcat :: NonEmpty TargetDependencies -> TargetDependencies #

stimes :: Integral b => b -> TargetDependencies -> TargetDependencies #

Data TargetDependencies Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TargetDependencies -> c TargetDependencies #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TargetDependencies #

toConstr :: TargetDependencies -> Constr #

dataTypeOf :: TargetDependencies -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TargetDependencies) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TargetDependencies) #

gmapT :: (forall b. Data b => b -> b) -> TargetDependencies -> TargetDependencies #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TargetDependencies -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TargetDependencies -> r #

gmapQ :: (forall d. Data d => d -> u) -> TargetDependencies -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> TargetDependencies -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TargetDependencies -> m TargetDependencies #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TargetDependencies -> m TargetDependencies #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TargetDependencies -> m TargetDependencies #

Generic TargetDependencies Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Associated Types

type Rep TargetDependencies

Instance details

Defined in Language.Haskell.Liquid.Types.Specs

type Rep TargetDependencies = D1 ('MetaData "TargetDependencies" "Language.Haskell.Liquid.Types.Specs" "liquidhaskell-boot-0.9.10.1.2-inplace" 'True) (C1 ('MetaCons "TargetDependencies" 'PrefixI 'True) (S1 ('MetaSel ('Just "getDependencies") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap StableModule LiftedSpec))))

Methods

from :: TargetDependencies -> Rep TargetDependencies x #

to :: Rep TargetDependencies x -> TargetDependencies #

Show TargetDependencies Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Methods

showsPrec :: Int -> TargetDependencies -> ShowS #

show :: TargetDependencies -> String #

showList :: [TargetDependencies] -> ShowS #

Eq TargetDependencies Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Methods

(==) :: TargetDependencies -> TargetDependencies -> Bool #

(/=) :: TargetDependencies -> TargetDependencies -> Bool #

type Rep TargetDependencies Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Specs

type Rep TargetDependencies = D1 ('MetaData "TargetDependencies" "Language.Haskell.Liquid.Types.Specs" "liquidhaskell-boot-0.9.10.1.2-inplace" 'True) (C1 ('MetaCons "TargetDependencies" 'PrefixI 'True) (S1 ('MetaSel ('Just "getDependencies") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap StableModule LiftedSpec))))

dropDependency :: StableModule -> TargetDependencies -> TargetDependencies Source #

Drop the given StableModule from the dependencies.

Predicates on spec types

isPLEVar :: TargetSpec -> Var -> Bool Source #

Returns True if the input Var is a PLE one.

isExportedVar :: TargetSrc -> Var -> Bool Source #

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

Other types

data QImports Source #

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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods showsPrec :: Int -> QImports -> ShowS # show :: QImports -> String # showList :: [QImports] -> ShowS #

data Spec lname ty Source #

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

lname corresponds to the names used for entities only known to LH like non-interpreted functions and type aliases.

Constructors

Spec

Fields

measures :: ![MeasureV lname (Located ty) (Located LHName)]
User-defined properties for ADTs
expSigs :: ![(lname, Sort)]
Exported logic symbols originated by reflecting functions
asmSigs :: ![(Located LHName, Located ty)]
Assumed (unchecked) types; including reflected signatures
asmReflectSigs :: ![(Located LHName, Located LHName)]
Assume reflects : left is the actual function and right the pretended one
sigs :: ![(Located LHName, Located (BareTypeV lname))]
Asserted spec signatures
invariants :: ![(Maybe LocSymbol, Located ty)]
Data type invariants; the Maybe is the generating measure
ialiases :: ![(Located ty, Located ty)]
Data type invariants to be checked
dataDecls :: ![DataDeclP lname ty]
Predicated data definitions
newtyDecls :: ![DataDeclP lname ty]
Predicated new type definitions
aliases :: ![Located (RTAlias Symbol (BareTypeV lname))]
RefType aliases
ealiases :: ![Located (RTAlias Symbol (ExprV lname))]
Expression aliases
embeds :: !(TCEmb (Located LHName))
GHC-Tycon-to-fixpoint Tycon map
qualifiers :: ![QualifierV lname]
Qualifiers in source files
lvars :: !(HashSet (Located LHName))
Variables that should be checked in the environment they are used
lazy :: !(HashSet (Located LHName))
Ignore Termination Check in these Functions
rewrites :: !(HashSet (Located LHName))
Theorems turned into rewrite rules
rewriteWith :: !(HashMap (Located LHName) [Located LHName])
Definitions using rewrite rules
fails :: !(HashSet (Located LHName))
These Functions should be unsafe
reflects :: !(HashSet (Located LHName))
Binders to reflect
privateReflects :: !(HashSet LocSymbol)
Private binders to reflect
opaqueReflects :: !(HashSet (Located LHName))
Binders to opaque-reflect
autois :: !(HashSet (Located LHName))
Automatically instantiate axioms in these Functions
hmeas :: !(HashSet (Located LHName))
Binders to turn into measures using haskell definitions
inlines :: !(HashSet (Located LHName))
Binders to turn into logic inline using haskell definitions
ignores :: !(HashSet (Located LHName))
Binders to ignore during checking; that is DON't check the corebind.
autosize :: !(HashSet (Located LHName))
Type Constructors that get automatically sizing info
pragmas :: ![Located String]
Command-line configurations passed in through source
cmeasures :: ![MeasureV lname (Located ty) ()]
Measures attached to a type-class
imeasures :: ![MeasureV lname (Located ty) (Located LHName)]
Mappings from (measure,type) -> measure
omeasures :: ![MeasureV lname (Located ty) (Located LHName)]
Opaque reflection measures. Separate field bc measures are checked for duplicates, and we want to allow for opaque-reflected measures to be duplicated. See Note [Duplicate measures and opaque reflection] in Language.Haskell.Liquid.Measure.
classes :: ![RClass (Located ty)]
Refined Type-Classes
relational :: ![(Located LHName, Located LHName, Located (BareTypeV lname), Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
Relational types
asmRel :: ![(Located LHName, Located LHName, Located (BareTypeV lname), Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
Assumed relational types
termexprs :: ![(Located LHName, [Located (ExprV lname)])]
Terminating Conditions for functions
rinstance :: ![RInstance (Located ty)]
dvariance :: ![(Located LHName, [Variance])]
TODO ? Where do these come from ?!
dsize :: ![([Located ty], lname)]
Size measure to enforce fancy termination
bounds :: !(RRBEnvV lname (Located ty))
axeqs :: ![EquationV lname]
Equalities used for Proof-By-Evaluation
defines :: ![(Located LHName, LMapV lname)]
Logic aliases
usedDataCons :: HashSet LHName
Data constructors used in specs

Instances

Instances details

Show BareSpec Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Methods

showsPrec :: Int -> BareSpec -> ShowS #

show :: BareSpec -> String #

showList :: [BareSpec] -> ShowS #

Expand BareSpec Source #

Instance details

Defined in Language.Haskell.Liquid.Bare.Expand

Methods

expand :: BareRTEnv -> SourcePos -> BareSpec -> BareSpec Source #

Monoid (Spec lname ty) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Methods

mempty :: Spec lname ty #

mappend :: Spec lname ty -> Spec lname ty -> Spec lname ty #

mconcat :: [Spec lname ty] -> Spec lname ty #

Semigroup (Spec lname ty) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Methods

(<>) :: Spec lname ty -> Spec lname ty -> Spec lname ty #

sconcat :: NonEmpty (Spec lname ty) -> Spec lname ty #

stimes :: Integral b => b -> Spec lname ty -> Spec lname ty #

(Data lname, Data ty) => Data (Spec lname ty) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Spec lname ty -> c (Spec lname ty) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Spec lname ty) #

toConstr :: Spec lname ty -> Constr #

dataTypeOf :: Spec lname ty -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Spec lname ty)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Spec lname ty)) #

gmapT :: (forall b. Data b => b -> b) -> Spec lname ty -> Spec lname ty #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Spec lname ty -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Spec lname ty -> r #

gmapQ :: (forall d. Data d => d -> u) -> Spec lname ty -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Spec lname ty -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Spec lname ty -> m (Spec lname ty) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Spec lname ty -> m (Spec lname ty) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Spec lname ty -> m (Spec lname ty) #

Generic (Spec lname ty) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Associated Types

type Rep (Spec lname ty)

Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Methods

from :: Spec lname ty -> Rep (Spec lname ty) x #

to :: Rep (Spec lname ty) x -> Spec lname ty #

(Show lname, PPrint lname, Show ty, PPrint ty, PPrint (RTypeV lname BTyCon BTyVar (RReftV lname))) => PPrint (Spec lname ty) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Methods

pprintTidy :: Tidy -> Spec lname ty -> Doc #

pprintPrec :: Int -> Tidy -> Spec lname ty -> Doc #

type Rep (Spec lname ty) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Specs

data GhcSpecVars Source #

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

Instances

Instances details

Monoid GhcSpecVars Source #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods mempty :: GhcSpecVars # mappend :: GhcSpecVars -> GhcSpecVars -> GhcSpecVars # mconcat :: [GhcSpecVars] -> GhcSpecVars #
Semigroup GhcSpecVars Source #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods (<>) :: GhcSpecVars -> GhcSpecVars -> GhcSpecVars # sconcat :: NonEmpty GhcSpecVars -> GhcSpecVars # stimes :: Integral b => b -> GhcSpecVars -> GhcSpecVars #
Show GhcSpecVars Source #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods showsPrec :: Int -> GhcSpecVars -> ShowS # show :: GhcSpecVars -> String # showList :: [GhcSpecVars] -> ShowS #

data GhcSpecSig Source #

Constructors

SpSig

Fields

gsTySigs :: ![(Var, LocSpecType)]
Asserted Reftypes
gsAsmSigs :: ![(Var, LocSpecType)]
Assumed Reftypes
gsAsmReflects :: ![(Var, Var)]
Assumed Reftypes (left is the actual function name and right the pretended one)
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
gsRelation :: ![(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]
gsAsmRel :: ![(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]

Instances

Instances details

Monoid GhcSpecSig Source #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods mempty :: GhcSpecSig # mappend :: GhcSpecSig -> GhcSpecSig -> GhcSpecSig # mconcat :: [GhcSpecSig] -> GhcSpecSig #
Semigroup GhcSpecSig Source #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods (<>) :: GhcSpecSig -> GhcSpecSig -> GhcSpecSig # sconcat :: NonEmpty GhcSpecSig -> GhcSpecSig # stimes :: Integral b => b -> GhcSpecSig -> GhcSpecSig #
Show GhcSpecSig Source #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods showsPrec :: Int -> GhcSpecSig -> ShowS # show :: GhcSpecSig -> String # showList :: [GhcSpecSig] -> ShowS #

data GhcSpecNames Source #

Constructors

SpNames
Fields 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" gsADTs :: ![DataDecl] ADTs extracted from Haskell 'data' definitions gsTyconEnv :: !TyConMap gsDataConIds :: [Var]

Instances

Instances details

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

data GhcSpecTerm Source #

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 gsNonStTerm :: !(HashSet Var) Binders to CHECK using REFINEMENT-TYPES/termination metrics

Instances

Instances details

Monoid GhcSpecTerm Source #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods mempty :: GhcSpecTerm # mappend :: GhcSpecTerm -> GhcSpecTerm -> GhcSpecTerm # mconcat :: [GhcSpecTerm] -> GhcSpecTerm #
Semigroup GhcSpecTerm Source #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods (<>) :: GhcSpecTerm -> GhcSpecTerm -> GhcSpecTerm # sconcat :: NonEmpty GhcSpecTerm -> GhcSpecTerm # stimes :: Integral b => b -> GhcSpecTerm -> GhcSpecTerm #
Show GhcSpecTerm Source #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods showsPrec :: Int -> GhcSpecTerm -> ShowS # show :: GhcSpecTerm -> String # showList :: [GhcSpecTerm] -> ShowS #

data GhcSpecRefl Source #

Constructors

SpRefl
Fields gsAutoInst :: !(HashSet Var) 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 gsRewrites :: HashSet (Located Var) gsRewritesWith :: HashMap Var [Var]

Instances

Instances details

Monoid GhcSpecRefl Source #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods mempty :: GhcSpecRefl # mappend :: GhcSpecRefl -> GhcSpecRefl -> GhcSpecRefl # mconcat :: [GhcSpecRefl] -> GhcSpecRefl #
Semigroup GhcSpecRefl Source #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods (<>) :: GhcSpecRefl -> GhcSpecRefl -> GhcSpecRefl # sconcat :: NonEmpty GhcSpecRefl -> GhcSpecRefl # stimes :: Integral b => b -> GhcSpecRefl -> GhcSpecRefl #
Show GhcSpecRefl Source #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods showsPrec :: Int -> GhcSpecRefl -> ShowS # show :: GhcSpecRefl -> String # showList :: [GhcSpecRefl] -> ShowS #

data GhcSpecData Source #

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
gsOpaqueRefls :: ![Var]
List of opaque reflected measures
gsUnsorted :: ![UnSortedExpr]

Instances

Instances details

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

data GhcSpecQual Source #

Constructors

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

Instances

Instances details

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

type BareDef = Def LocBareType (Located LHName) Source #

type BareMeasure = Measure LocBareType (Located LHName) Source #

type SpecMeasure = Measure LocSpecType DataCon Source #

type VarOrLocSymbol = Either Var LocSymbol Source #

emapSpecM Source #

Arguments

:: Monad m
=> Bool	The bscope setting, which affects which names are considered to be in scope in refinment types.
-> (LHName -> [Symbol])	For names that have a local environment return the names in scope.
-> ([Symbol] -> lname0 -> m lname1)	The first parameter of the function argument are the variables in scope.
-> ([Symbol] -> ty0 -> m ty1)
-> Spec lname0 ty0
-> m (Spec lname1 ty1)

A function to resolve names in the ty parameter of Spec

fromBareSpecLHName :: BareSpecLHName -> BareSpec Source #

fromBareSpecParsed :: BareSpecParsed -> BareSpec Source #

mapSpecLName :: (lname0 -> lname1) -> Spec lname0 ty -> Spec lname1 ty Source #

mapSpecTy :: (ty0 -> ty1) -> Spec lname ty0 -> Spec lname ty1 Source #

Legacy data structures

data GhcSrc Source #

Constructors

Src

Fields

_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)

data GhcSpec Source #

Constructors

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

Instances

Instances details

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

Provisional compatibility exports & optics

toTargetSrc :: GhcSrc -> TargetSrc Source #

fromTargetSrc :: TargetSrc -> GhcSrc Source #

toTargetSpec :: GhcSpec -> TargetSpec Source #

toLiftedSpec :: BareSpecLHName -> LiftedSpec Source #

unsafeFromLiftedSpec :: LiftedSpec -> BareSpecLHName Source #

emptyLiftedSpec :: LiftedSpec Source #

Orphan instances

Show TyConMap Source #
Instance details Methods showsPrec :: Int -> TyConMap -> ShowS # show :: TyConMap -> String # showList :: [TyConMap] -> ShowS #