Language.Haskell.Liquid.Types.Specs

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

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:

1. Perform name-resolution (e.g. make all the relevant GHC's Vars qualified, resolve GHC's Names, etc);
2. 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;
3. 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

Show TargetInfo

Defined in Language.Haskell.Liquid.GHC.Interface

Methods

showsPrec :: Int -> TargetInfo -> ShowS

show :: TargetInfo -> String

showList :: [TargetInfo] -> ShowS

PPrint TargetInfo

Defined in Language.Haskell.Liquid.GHC.Interface

Methods

pprintTidy :: Tidy -> TargetInfo -> Doc

pprintPrec :: Int -> Tidy -> TargetInfo -> Doc

HasConfig TargetInfo

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

• 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

PPrint TargetSpec

Pretty Printing -----------------------------------------------------------

Defined in Language.Haskell.Liquid.GHC.Interface

Methods

pprintTidy :: Tidy -> TargetSpec -> Doc

pprintPrec :: Int -> Tidy -> TargetSpec -> Doc

HasConfig TargetSpec

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

Monoid BareSpec

Defined in Language.Haskell.Liquid.Types.Specs

Methods

mempty :: BareSpec

mappend :: BareSpec -> BareSpec -> BareSpec

mconcat :: [BareSpec] -> BareSpec

Semigroup BareSpec

Defined in Language.Haskell.Liquid.Types.Specs

Methods

(<>) :: BareSpec -> BareSpec -> BareSpec

sconcat :: NonEmpty BareSpec -> BareSpec

stimes :: Integral b => b -> BareSpec -> BareSpec

Generic BareSpec

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

Show BareSpec

Defined in Language.Haskell.Liquid.Types.Specs

Methods

showsPrec :: Int -> BareSpec -> ShowS

show :: BareSpec -> String

showList :: [BareSpec] -> ShowS

Binary BareSpec

Defined in Language.Haskell.Liquid.Types.Specs

Methods

put :: BareSpec -> Put

get :: Get BareSpec

putList :: [BareSpec] -> Put

type Rep BareSpec

Defined in Language.Haskell.Liquid.Types.Specs

type Rep BareSpec = D1 ('MetaData "BareSpec" "Language.Haskell.Liquid.Types.Specs" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" '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

• 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)
• liftedDsize :: [([LocBareType], LocSymbol)]
• 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

Generic LiftedSpec

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

Show LiftedSpec

Defined in Language.Haskell.Liquid.Types.Specs

Methods

showsPrec :: Int -> LiftedSpec -> ShowS

show :: LiftedSpec -> String

showList :: [LiftedSpec] -> ShowS

Binary LiftedSpec

Defined in Language.Haskell.Liquid.Types.Specs

Methods

put :: LiftedSpec -> Put

get :: Get LiftedSpec

putList :: [LiftedSpec] -> Put

Eq LiftedSpec

Defined in Language.Haskell.Liquid.Types.Specs

Methods

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

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

Hashable LiftedSpec

Defined in Language.Haskell.Liquid.Types.Specs

Methods

hashWithSalt :: Int -> LiftedSpec -> Int

hash :: LiftedSpec -> Int

type Rep LiftedSpec

Defined in Language.Haskell.Liquid.Types.Specs

type Rep LiftedSpec = D1 ('MetaData "LiftedSpec" "Language.Haskell.Liquid.Types.Specs" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" '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 "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 "liftedDsize") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [([LocBareType], LocSymbol)]))) :*: ((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 TargetDependencies

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

Constructors

TargetDependencies

Fields

• getDependencies :: HashMap StableModule LiftedSpec

Instances

Monoid TargetDependencies

Defined in Language.Haskell.Liquid.Types.Specs

Methods

mempty :: TargetDependencies

mappend :: TargetDependencies -> TargetDependencies -> TargetDependencies

mconcat :: [TargetDependencies] -> TargetDependencies

Semigroup TargetDependencies

Defined in Language.Haskell.Liquid.Types.Specs

Methods

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

sconcat :: NonEmpty TargetDependencies -> TargetDependencies

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

Generic TargetDependencies

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

Show TargetDependencies

Defined in Language.Haskell.Liquid.Types.Specs

Methods

showsPrec :: Int -> TargetDependencies -> ShowS

show :: TargetDependencies -> String

showList :: [TargetDependencies] -> ShowS

Binary TargetDependencies

Defined in Language.Haskell.Liquid.Types.Specs

Methods

put :: TargetDependencies -> Put

get :: Get TargetDependencies

putList :: [TargetDependencies] -> Put

Eq TargetDependencies

Defined in Language.Haskell.Liquid.Types.Specs

Methods

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

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

type Rep TargetDependencies

Defined in Language.Haskell.Liquid.Types.Specs

type Rep TargetDependencies = D1 ('MetaData "TargetDependencies" "Language.Haskell.Liquid.Types.Specs" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" '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

Show QImports

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

• 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

• relational :: ![(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]

  Relational types

• asmRel :: ![(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]

  Assumed relational types

• termexprs :: ![(LocSymbol, [Located Expr])]

  Terminating Conditions for functions

• rinstance :: ![RInstance ty]
• ilaws :: ![RILaws ty]
• dvariance :: ![(LocSymbol, [Variance])]

  TODO ? Where do these come from ?!

• dsize :: ![([ty], LocSymbol)]

  Size measure to enforce fancy termination

• 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

Qualify ModSpecs

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> ModSpecs -> ModSpecs

Qualify BareSpec

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareSpec -> BareSpec

Monoid (Spec ty bndr)

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

Semigroup (Spec ty bndr)

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

Generic (Spec ty bndr)

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

(PPrint ty, PPrint bndr, Show ty) => Show (Spec ty bndr)

Defined in Language.Haskell.Liquid.Types.Specs

Methods

showsPrec :: Int -> Spec ty bndr -> ShowS

show :: Spec ty bndr -> String

showList :: [Spec ty bndr] -> ShowS

Binary (Spec LocBareType LocSymbol)

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)

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)

Defined in Language.Haskell.Liquid.Types.Specs

type Rep (Spec ty bndr) = D1 ('MetaData "Spec" "Language.Haskell.Liquid.Types.Specs" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" '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 "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 "relational") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)])) :*: (S1 ('MetaSel ('Just "asmRel") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]) :*: (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 "dsize") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [([ty], LocSymbol)]))) :*: (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

Instances

Monoid GhcSpecVars

Defined in Language.Haskell.Liquid.Types.Specs

Methods

mempty :: GhcSpecVars

mappend :: GhcSpecVars -> GhcSpecVars -> GhcSpecVars

mconcat :: [GhcSpecVars] -> GhcSpecVars

Semigroup GhcSpecVars

Defined in Language.Haskell.Liquid.Types.Specs

Methods

(<>) :: GhcSpecVars -> GhcSpecVars -> GhcSpecVars

sconcat :: NonEmpty GhcSpecVars -> GhcSpecVars

stimes :: Integral b => b -> GhcSpecVars -> GhcSpecVars

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

• gsRelation :: ![(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]
• gsAsmRel :: ![(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]

Instances

Monoid GhcSpecSig

Defined in Language.Haskell.Liquid.Types.Specs

Methods

mempty :: GhcSpecSig

mappend :: GhcSpecSig -> GhcSpecSig -> GhcSpecSig

mconcat :: [GhcSpecSig] -> GhcSpecSig

Semigroup GhcSpecSig

Defined in Language.Haskell.Liquid.Types.Specs

Methods

(<>) :: GhcSpecSig -> GhcSpecSig -> GhcSpecSig

sconcat :: NonEmpty GhcSpecSig -> GhcSpecSig

stimes :: Integral b => b -> GhcSpecSig -> GhcSpecSig

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

• gsNonStTerm :: !(HashSet Var)

  Binders to CHECK using REFINEMENT-TYPES/termination metrics

Instances

Monoid GhcSpecTerm

Defined in Language.Haskell.Liquid.Types.Specs

Methods

mempty :: GhcSpecTerm

mappend :: GhcSpecTerm -> GhcSpecTerm -> GhcSpecTerm

mconcat :: [GhcSpecTerm] -> GhcSpecTerm

Semigroup GhcSpecTerm

Defined in Language.Haskell.Liquid.Types.Specs

Methods

(<>) :: GhcSpecTerm -> GhcSpecTerm -> GhcSpecTerm

sconcat :: NonEmpty GhcSpecTerm -> GhcSpecTerm

stimes :: Integral b => b -> GhcSpecTerm -> GhcSpecTerm

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]

Instances

Monoid GhcSpecRefl

Defined in Language.Haskell.Liquid.Types.Specs

Methods

mempty :: GhcSpecRefl

mappend :: GhcSpecRefl -> GhcSpecRefl -> GhcSpecRefl

mconcat :: [GhcSpecRefl] -> GhcSpecRefl

Semigroup GhcSpecRefl

Defined in Language.Haskell.Liquid.Types.Specs

Methods

(<>) :: GhcSpecRefl -> GhcSpecRefl -> GhcSpecRefl

sconcat :: NonEmpty GhcSpecRefl -> GhcSpecRefl

stimes :: Integral b => b -> GhcSpecRefl -> GhcSpecRefl

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

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

HasConfig GhcSpec

Defined in Language.Haskell.Liquid.Types.Specs

Methods

getConfig :: GhcSpec -> Config

Provisional compatibility exports & optics

toTargetSrc :: GhcSrc -> TargetSrc

fromTargetSrc :: TargetSrc -> GhcSrc

toTargetSpec :: GhcSpec -> (TargetSpec, LiftedSpec)

toBareSpec :: Spec LocBareType LocSymbol -> BareSpec

fromBareSpec :: BareSpec -> Spec LocBareType LocSymbol

toLiftedSpec :: Spec LocBareType LocSymbol -> LiftedSpec

unsafeFromLiftedSpec :: LiftedSpec -> Spec LocBareType LocSymbol

emptyLiftedSpec :: LiftedSpec

Orphan instances

Binary Equation

Methods

put :: Equation -> Put

get :: Get Equation

putList :: [Equation] -> Put