Safe Haskell	None
Language	Haskell98

Language.Haskell.Liquid.Measure

Contents

Specifications
Type Aliases
Constructors

Synopsis

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 MSpec ty ctor = MSpec {
- ctorMap :: HashMap LHName [Def ty ctor]
- measMap :: HashMap (Located LHName) (Measure ty ctor)
- cmeasMap :: HashMap (Located LHName) (Measure ty ())
- imeas :: ![Measure ty ctor]
}
type BareSpec = Spec Symbol BareType
type BareMeasure = Measure LocBareType (Located LHName)
type SpecMeasure = Measure LocSpecType DataCon
mkM :: HasCallStack => Located LHName -> ty -> [DefV v ty bndr] -> MeasureKind -> UnSortedExprs -> MeasureV v ty bndr
mkMSpec :: [Measure t (Located LHName)] -> [Measure t ()] -> [Measure t (Located LHName)] -> [Measure t (Located LHName)] -> MSpec t (Located LHName)
mkMSpec' :: [Measure ty DataCon] -> MSpec ty DataCon
dataConTypes :: Bool -> MSpec (RRType Reft) DataCon -> ([(Var, RRType Reft)], [(Located LHName, RRType Reft)])
defRefType :: Bool -> Type -> Def (RRType Reft) DataCon -> RRType Reft
bodyPred :: Expr -> Body -> Expr

Specifications

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 MSpec ty ctor Source #

Constructors

MSpec
Fields ctorMap :: HashMap LHName [Def ty ctor] measMap :: HashMap (Located LHName) (Measure ty ctor) cmeasMap :: HashMap (Located LHName) (Measure ty ()) imeas :: ![Measure ty ctor]

Instances

Instances details

Bifunctor MSpec Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

bimap :: (a -> b) -> (c -> d) -> MSpec a c -> MSpec b d #

first :: (a -> b) -> MSpec a c -> MSpec b c #

second :: (b -> c) -> MSpec a b -> MSpec a c #

Functor (MSpec ty) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

fmap :: (a -> b) -> MSpec ty a -> MSpec ty b #

(<$) :: a -> MSpec ty b -> MSpec ty a #

Eq ctor => Monoid (MSpec ty ctor) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

mempty :: MSpec ty ctor #

mappend :: MSpec ty ctor -> MSpec ty ctor -> MSpec ty ctor #

mconcat :: [MSpec ty ctor] -> MSpec ty ctor #

Eq ctor => Semigroup (MSpec ty ctor) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(<>) :: MSpec ty ctor -> MSpec ty ctor -> MSpec ty ctor #

sconcat :: NonEmpty (MSpec ty ctor) -> MSpec ty ctor #

stimes :: Integral b => b -> MSpec ty ctor -> MSpec ty ctor #

(Data ty, Data ctor) => Data (MSpec ty ctor) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

toConstr :: MSpec ty ctor -> Constr #

dataTypeOf :: MSpec ty ctor -> DataType #

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

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

gmapT :: (forall b. Data b => b -> b) -> MSpec ty ctor -> MSpec ty ctor #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MSpec ty ctor -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MSpec ty ctor -> r #

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

gmapQi :: Int -> (forall d. Data d => d -> u) -> MSpec ty ctor -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> MSpec ty ctor -> m (MSpec ty ctor) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MSpec ty ctor -> m (MSpec ty ctor) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MSpec ty ctor -> m (MSpec ty ctor) #

Generic (MSpec ty ctor) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (MSpec ty ctor)

Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep (MSpec ty ctor) = D1 ('MetaData "MSpec" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "MSpec" 'PrefixI 'True) ((S1 ('MetaSel ('Just "ctorMap") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap LHName [Def ty ctor])) :*: S1 ('MetaSel ('Just "measMap") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap (Located LHName) (Measure ty ctor)))) :*: (S1 ('MetaSel ('Just "cmeasMap") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap (Located LHName) (Measure ty ()))) :*: S1 ('MetaSel ('Just "imeas") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Measure ty ctor]))))

Methods

from :: MSpec ty ctor -> Rep (MSpec ty ctor) x #

to :: Rep (MSpec ty ctor) x -> MSpec ty ctor #

(Show ty, Show ctor, PPrint ctor, PPrint ty) => Show (MSpec ty ctor) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> MSpec ty ctor -> ShowS #

show :: MSpec ty ctor -> String #

showList :: [MSpec ty ctor] -> ShowS #

(PPrint t, PPrint a) => PPrint (MSpec t a) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> MSpec t a -> Doc #

pprintPrec :: Int -> Tidy -> MSpec t a -> Doc #

type Rep (MSpec ty ctor) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep (MSpec ty ctor) = D1 ('MetaData "MSpec" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "MSpec" 'PrefixI 'True) ((S1 ('MetaSel ('Just "ctorMap") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap LHName [Def ty ctor])) :*: S1 ('MetaSel ('Just "measMap") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap (Located LHName) (Measure ty ctor)))) :*: (S1 ('MetaSel ('Just "cmeasMap") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap (Located LHName) (Measure ty ()))) :*: S1 ('MetaSel ('Just "imeas") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Measure ty ctor]))))

Type Aliases

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 BareMeasure = Measure LocBareType (Located LHName) Source #

type SpecMeasure = Measure LocSpecType DataCon Source #

Constructors

mkM :: HasCallStack => Located LHName -> ty -> [DefV v ty bndr] -> MeasureKind -> UnSortedExprs -> MeasureV v ty bndr Source #

mkMSpec :: [Measure t (Located LHName)] -> [Measure t ()] -> [Measure t (Located LHName)] -> [Measure t (Located LHName)] -> MSpec t (Located LHName) Source #

mkMSpec' :: [Measure ty DataCon] -> MSpec ty DataCon Source #

dataConTypes :: Bool -> MSpec (RRType Reft) DataCon -> ([(Var, RRType Reft)], [(Located LHName, RRType Reft)]) Source #

defRefType :: Bool -> Type -> Def (RRType Reft) DataCon -> RRType Reft Source #

bodyPred :: Expr -> Body -> Expr Source #