Safe Haskell	None
Language	Haskell98

Language.Haskell.Liquid.Types.DataDecl

Contents

Parse-time entities describing refined data types
Orphan instances

Description

This module contains types to represent refined data types.

Synopsis

type DataDecl = DataDeclP Symbol BareType
type DataDeclLHName = DataDeclP LHName BareTypeLHName
type DataDeclParsed = DataDeclP LocSymbol BareTypeParsed
data DataDeclP v ty = DataDecl {
- tycName :: DataName
- tycTyVars :: [Symbol]
- tycPVars :: [PVarV v (BSortV v)]
- tycDCons :: Maybe [DataCtorP ty]
- tycSrcPos :: !SourcePos
- tycSFun :: Maybe (SizeFunV v)
- tycPropTy :: Maybe ty
- tycKind :: !DataDeclKind
}
data DataName
- = DnName !(Located LHName)
- | DnCon !(Located LHName)
dataNameSymbol :: DataName -> Located LHName
type DataCtor = DataCtorP BareType
type DataCtorParsed = DataCtorP BareTypeParsed
data DataCtorP ty = DataCtor {
- dcName :: Located LHName
- dcTyVars :: [Symbol]
- dcTheta :: [ty]
- dcFields :: [(LHName, ty)]
- dcResult :: Maybe ty
}
data DataConP = DataConP {
- dcpLoc :: !SourcePos
- dcpCon :: !DataCon
- dcpFreeTyVars :: ![RTyVar]
- dcpFreePred :: ![PVar RSort]
- dcpTyConstrs :: ![SpecType]
- dcpTyArgs :: ![(LHName, SpecType)]
- dcpTyRes :: !SpecType
- dcpIsGadt :: !Bool
- dcpModule :: !Symbol
- dcpLocE :: !SourcePos
}
data HasDataDecl
- = NoDecl (Maybe SizeFun)
- | HasDecl
hasDecl :: DataDecl -> HasDataDecl
data DataDeclKind
- = DataUser
- | DataReflected
data TyConP = TyConP {
- tcpLoc :: !SourcePos
- tcpCon :: !TyCon
- tcpFreeTyVarsTy :: ![RTyVar]
- tcpFreePredTy :: ![PVar RSort]
- tcpVarianceTs :: !VarianceInfo
- tcpVariancePs :: !VarianceInfo
- tcpSizeFun :: !(Maybe SizeFun)
}

Parse-time entities describing refined data types

type DataDecl = DataDeclP Symbol BareType Source #

Data type refinements

type DataDeclLHName = DataDeclP LHName BareTypeLHName Source #

type DataDeclParsed = DataDeclP LocSymbol BareTypeParsed Source #

data DataDeclP v ty Source #

Constructors

DataDecl

Fields

tycName :: DataName
Type Constructor Name
tycTyVars :: [Symbol]
Tyvar Parameters
tycPVars :: [PVarV v (BSortV v)]
PVar Parameters
tycDCons :: Maybe [DataCtorP ty]
Data Constructors (Nothing is reserved for non-GADT style empty data declarations)
tycSrcPos :: !SourcePos
Source Position
tycSFun :: Maybe (SizeFunV v)
Default termination measure
tycPropTy :: Maybe ty
Type of Ind-Prop
tycKind :: !DataDeclKind
User-defined or Auto-lifted

Instances

Instances details

Ord DataDecl Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

compare :: DataDecl -> DataDecl -> Ordering #

(<) :: DataDecl -> DataDecl -> Bool #

(<=) :: DataDecl -> DataDecl -> Bool #

(>) :: DataDecl -> DataDecl -> Bool #

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

max :: DataDecl -> DataDecl -> DataDecl #

min :: DataDecl -> DataDecl -> DataDecl #

Expand DataDecl Source #

Instance details

Defined in Language.Haskell.Liquid.Bare.Expand

Methods

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

Functor (DataDeclP v) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

fmap :: (a -> b) -> DataDeclP v a -> DataDeclP v b #

(<$) :: a -> DataDeclP v b -> DataDeclP v a #

Foldable (DataDeclP v) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

fold :: Monoid m => DataDeclP v m -> m #

foldMap :: Monoid m => (a -> m) -> DataDeclP v a -> m #

foldMap' :: Monoid m => (a -> m) -> DataDeclP v a -> m #

foldr :: (a -> b -> b) -> b -> DataDeclP v a -> b #

foldr' :: (a -> b -> b) -> b -> DataDeclP v a -> b #

foldl :: (b -> a -> b) -> b -> DataDeclP v a -> b #

foldl' :: (b -> a -> b) -> b -> DataDeclP v a -> b #

foldr1 :: (a -> a -> a) -> DataDeclP v a -> a #

foldl1 :: (a -> a -> a) -> DataDeclP v a -> a #

toList :: DataDeclP v a -> [a] #

null :: DataDeclP v a -> Bool #

length :: DataDeclP v a -> Int #

elem :: Eq a => a -> DataDeclP v a -> Bool #

maximum :: Ord a => DataDeclP v a -> a #

minimum :: Ord a => DataDeclP v a -> a #

sum :: Num a => DataDeclP v a -> a #

product :: Num a => DataDeclP v a -> a #

Traversable (DataDeclP v) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

traverse :: Applicative f => (a -> f b) -> DataDeclP v a -> f (DataDeclP v b) #

sequenceA :: Applicative f => DataDeclP v (f a) -> f (DataDeclP v a) #

mapM :: Monad m => (a -> m b) -> DataDeclP v a -> m (DataDeclP v b) #

sequence :: Monad m => DataDeclP v (m a) -> m (DataDeclP v a) #

(Binary v, Binary ty) => Binary (DataDeclP v ty) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

put :: DataDeclP v ty -> Put #

get :: Get (DataDeclP v ty) #

putList :: [DataDeclP v ty] -> Put #

(Data v, Data ty) => Data (DataDeclP v ty) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

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

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

toConstr :: DataDeclP v ty -> Constr #

dataTypeOf :: DataDeclP v ty -> DataType #

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

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

gmapT :: (forall b. Data b => b -> b) -> DataDeclP v ty -> DataDeclP v ty #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DataDeclP v ty -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DataDeclP v ty -> r #

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

gmapQi :: Int -> (forall d. Data d => d -> u) -> DataDeclP v ty -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DataDeclP v ty -> m (DataDeclP v ty) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DataDeclP v ty -> m (DataDeclP v ty) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DataDeclP v ty -> m (DataDeclP v ty) #

Generic (DataDeclP v ty) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Associated Types

type Rep (DataDeclP v ty)

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

from :: DataDeclP v ty -> Rep (DataDeclP v ty) x #

to :: Rep (DataDeclP v ty) x -> DataDeclP v ty #

(Show v, Show ty) => Show (DataDeclP v ty) Source #

For debugging.

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

showsPrec :: Int -> DataDeclP v ty -> ShowS #

show :: DataDeclP v ty -> String #

showList :: [DataDeclP v ty] -> ShowS #

Eq (DataDeclP v ty) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

(==) :: DataDeclP v ty -> DataDeclP v ty -> Bool #

(/=) :: DataDeclP v ty -> DataDeclP v ty -> Bool #

(Hashable ty, Hashable v) => Hashable (DataDeclP v ty) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

hashWithSalt :: Int -> DataDeclP v ty -> Int #

hash :: DataDeclP v ty -> Int #

(PPrint lname, PPrint ty) => PPrint (DataDeclP lname ty) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

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

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

Loc (DataDeclP v ty) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

srcSpan :: DataDeclP v ty -> SrcSpan #

type Rep (DataDeclP v ty) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

data DataName Source #

The name of the TyCon corresponding to a DataDecl

Constructors

DnName !(Located LHName)	for `isVanillyAlgTyCon` we can directly use the `TyCon` name
DnCon !(Located LHName)	for `FamInst` TyCon we save some `DataCon` name

Instances

Instances details

Binary DataName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

put :: DataName -> Put #

get :: Get DataName #

putList :: [DataName] -> Put #

Data DataName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

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

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

toConstr :: DataName -> Constr #

dataTypeOf :: DataName -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic DataName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Associated Types

type Rep DataName

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

type Rep DataName = D1 ('MetaData "DataName" "Language.Haskell.Liquid.Types.DataDecl" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "DnName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Located LHName))) :+: C1 ('MetaCons "DnCon" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Located LHName))))

Methods

from :: DataName -> Rep DataName x #

to :: Rep DataName x -> DataName #

Show DataName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

showsPrec :: Int -> DataName -> ShowS #

show :: DataName -> String #

showList :: [DataName] -> ShowS #

Eq DataName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

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

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

Ord DataName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

compare :: DataName -> DataName -> Ordering #

(<) :: DataName -> DataName -> Bool #

(<=) :: DataName -> DataName -> Bool #

(>) :: DataName -> DataName -> Bool #

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

max :: DataName -> DataName -> DataName #

min :: DataName -> DataName -> DataName #

Hashable DataName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

hashWithSalt :: Int -> DataName -> Int #

hash :: DataName -> Int #

PPrint DataName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

pprintTidy :: Tidy -> DataName -> Doc #

pprintPrec :: Int -> Tidy -> DataName -> Doc #

Loc DataName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

srcSpan :: DataName -> SrcSpan #

type Rep DataName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

type Rep DataName = D1 ('MetaData "DataName" "Language.Haskell.Liquid.Types.DataDecl" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "DnName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Located LHName))) :+: C1 ('MetaCons "DnCon" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Located LHName))))

dataNameSymbol :: DataName -> Located LHName Source #

type DataCtor = DataCtorP BareType Source #

Data Constructor

type DataCtorParsed = DataCtorP BareTypeParsed Source #

data DataCtorP ty Source #

Constructors

DataCtor
Fields dcName :: Located LHName DataCon name dcTyVars :: [Symbol] Type parameters dcTheta :: [ty] The GHC ThetaType corresponding to DataCon.dataConSig dcFields :: [(LHName, ty)] field-name and field-Type pairs dcResult :: Maybe ty Possible output (if in GADT form)

Instances

Instances details

Functor DataCtorP Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

fmap :: (a -> b) -> DataCtorP a -> DataCtorP b #

(<$) :: a -> DataCtorP b -> DataCtorP a #

Foldable DataCtorP Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

fold :: Monoid m => DataCtorP m -> m #

foldMap :: Monoid m => (a -> m) -> DataCtorP a -> m #

foldMap' :: Monoid m => (a -> m) -> DataCtorP a -> m #

foldr :: (a -> b -> b) -> b -> DataCtorP a -> b #

foldr' :: (a -> b -> b) -> b -> DataCtorP a -> b #

foldl :: (b -> a -> b) -> b -> DataCtorP a -> b #

foldl' :: (b -> a -> b) -> b -> DataCtorP a -> b #

foldr1 :: (a -> a -> a) -> DataCtorP a -> a #

foldl1 :: (a -> a -> a) -> DataCtorP a -> a #

toList :: DataCtorP a -> [a] #

null :: DataCtorP a -> Bool #

length :: DataCtorP a -> Int #

elem :: Eq a => a -> DataCtorP a -> Bool #

maximum :: Ord a => DataCtorP a -> a #

minimum :: Ord a => DataCtorP a -> a #

sum :: Num a => DataCtorP a -> a #

product :: Num a => DataCtorP a -> a #

Traversable DataCtorP Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

traverse :: Applicative f => (a -> f b) -> DataCtorP a -> f (DataCtorP b) #

sequenceA :: Applicative f => DataCtorP (f a) -> f (DataCtorP a) #

mapM :: Monad m => (a -> m b) -> DataCtorP a -> m (DataCtorP b) #

sequence :: Monad m => DataCtorP (m a) -> m (DataCtorP a) #

Expand DataCtor Source #

Instance details

Defined in Language.Haskell.Liquid.Bare.Expand

Methods

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

Binary ty => Binary (DataCtorP ty) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

put :: DataCtorP ty -> Put #

get :: Get (DataCtorP ty) #

putList :: [DataCtorP ty] -> Put #

Data ty => Data (DataCtorP ty) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

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

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

toConstr :: DataCtorP ty -> Constr #

dataTypeOf :: DataCtorP ty -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic (DataCtorP ty) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Associated Types

type Rep (DataCtorP ty)

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

type Rep (DataCtorP ty) = D1 ('MetaData "DataCtorP" "Language.Haskell.Liquid.Types.DataDecl" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "DataCtor" 'PrefixI 'True) ((S1 ('MetaSel ('Just "dcName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located LHName)) :*: S1 ('MetaSel ('Just "dcTyVars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Symbol])) :*: (S1 ('MetaSel ('Just "dcTheta") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ty]) :*: (S1 ('MetaSel ('Just "dcFields") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(LHName, ty)]) :*: S1 ('MetaSel ('Just "dcResult") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ty))))))

Methods

from :: DataCtorP ty -> Rep (DataCtorP ty) x #

to :: Rep (DataCtorP ty) x -> DataCtorP ty #

Eq ty => Eq (DataCtorP ty) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

(==) :: DataCtorP ty -> DataCtorP ty -> Bool #

(/=) :: DataCtorP ty -> DataCtorP ty -> Bool #

Hashable ty => Hashable (DataCtorP ty) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

hashWithSalt :: Int -> DataCtorP ty -> Int #

hash :: DataCtorP ty -> Int #

PPrint ty => PPrint (DataCtorP ty) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

pprintTidy :: Tidy -> DataCtorP ty -> Doc #

pprintPrec :: Int -> Tidy -> DataCtorP ty -> Doc #

Loc (DataCtorP ty) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

srcSpan :: DataCtorP ty -> SrcSpan #

type Rep (DataCtorP ty) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

type Rep (DataCtorP ty) = D1 ('MetaData "DataCtorP" "Language.Haskell.Liquid.Types.DataDecl" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "DataCtor" 'PrefixI 'True) ((S1 ('MetaSel ('Just "dcName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located LHName)) :*: S1 ('MetaSel ('Just "dcTyVars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Symbol])) :*: (S1 ('MetaSel ('Just "dcTheta") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ty]) :*: (S1 ('MetaSel ('Just "dcFields") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(LHName, ty)]) :*: S1 ('MetaSel ('Just "dcResult") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ty))))))

data DataConP Source #

Constructors

DataConP

Fields

dcpLoc :: !SourcePos
dcpCon :: !DataCon
Corresponding GHC DataCon
dcpFreeTyVars :: ![RTyVar]
Type parameters
dcpFreePred :: ![PVar RSort]
Abstract Refinement parameters
dcpTyConstrs :: ![SpecType]
? Class constraints (via dataConStupidTheta)
dcpTyArgs :: ![(LHName, SpecType)]
Value parameters
dcpTyRes :: !SpecType
Result type
dcpIsGadt :: !Bool
Was this specified in GADT style (if so, DONT use function names as fields)
dcpModule :: !Symbol
Which module was this defined in
dcpLocE :: !SourcePos

Instances

Instances details

Data DataConP Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

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

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

toConstr :: DataConP -> Constr #

dataTypeOf :: DataConP -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic DataConP Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Associated Types

type Rep DataConP

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

from :: DataConP -> Rep DataConP x #

to :: Rep DataConP x -> DataConP #

PPrint SpecType => Show DataConP Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

showsPrec :: Int -> DataConP -> ShowS #

show :: DataConP -> String #

showList :: [DataConP] -> ShowS #

PPrint SpecType => PPrint DataConP Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

pprintTidy :: Tidy -> DataConP -> Doc #

pprintPrec :: Int -> Tidy -> DataConP -> Doc #

Loc DataConP Source #

NOTE:DataCon-Data: for each DataConP we also store the type of the constructed data. This is *the same as* tyRes for *vanilla* ADTs (e.g. List, Maybe etc.) but may differ for GADTs. For example,
data Thing a where X :: Thing Int Y :: Thing Bool

Here the DataConP associated with X (resp. Y) has tyRes corresponding to 'Thing Int' (resp. 'Thing Bool'), but in both cases, the tyData should be 'Thing a'.

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

srcSpan :: DataConP -> SrcSpan #

type Rep DataConP Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

data HasDataDecl Source #

Constructors

NoDecl (Maybe SizeFun)
HasDecl

Instances

Instances details

Show HasDataDecl Source #
Instance details Defined in Language.Haskell.Liquid.Types.DataDecl Methods showsPrec :: Int -> HasDataDecl -> ShowS # show :: HasDataDecl -> String # showList :: [HasDataDecl] -> ShowS #
PPrint HasDataDecl Source #
Instance details Defined in Language.Haskell.Liquid.Types.DataDecl Methods pprintTidy :: Tidy -> HasDataDecl -> Doc # pprintPrec :: Int -> Tidy -> HasDataDecl -> Doc #

hasDecl :: DataDecl -> HasDataDecl Source #

data DataDeclKind Source #

What kind of DataDecl is it?

Constructors

DataUser	User defined data-definitions (should have refined fields)
DataReflected	Automatically lifted data-definitions (do not have refined fields)

Instances

Instances details

Binary DataDeclKind Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

put :: DataDeclKind -> Put #

get :: Get DataDeclKind #

putList :: [DataDeclKind] -> Put #

NFData DataDeclKind Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

rnf :: DataDeclKind -> () #

Data DataDeclKind Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

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

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

toConstr :: DataDeclKind -> Constr #

dataTypeOf :: DataDeclKind -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic DataDeclKind Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Associated Types

type Rep DataDeclKind
Instance details Defined in Language.Haskell.Liquid.Types.DataDecl type Rep DataDeclKind = D1 ('MetaData "DataDeclKind" "Language.Haskell.Liquid.Types.DataDecl" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "DataUser" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DataReflected" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: DataDeclKind -> Rep DataDeclKind x #

to :: Rep DataDeclKind x -> DataDeclKind #

Show DataDeclKind Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

showsPrec :: Int -> DataDeclKind -> ShowS #

show :: DataDeclKind -> String #

showList :: [DataDeclKind] -> ShowS #

Eq DataDeclKind Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

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

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

Hashable DataDeclKind Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

hashWithSalt :: Int -> DataDeclKind -> Int #

hash :: DataDeclKind -> Int #

type Rep DataDeclKind Source #

Instance details

Defined in Language.Haskell.Liquid.Types.DataDecl

type Rep DataDeclKind = D1 ('MetaData "DataDeclKind" "Language.Haskell.Liquid.Types.DataDecl" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "DataUser" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DataReflected" 'PrefixI 'False) (U1 :: Type -> Type))

data TyConP Source #

Constructors

TyConP
Fields tcpLoc :: !SourcePos tcpCon :: !TyCon tcpFreeTyVarsTy :: ![RTyVar] tcpFreePredTy :: ![PVar RSort] tcpVarianceTs :: !VarianceInfo tcpVariancePs :: !VarianceInfo tcpSizeFun :: !(Maybe SizeFun)

Instances

Instances details

Data TyConP Source #

Instance details

Defined in Language.Haskell.Liquid.Types.RType

Methods

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

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

toConstr :: TyConP -> Constr #

dataTypeOf :: TyConP -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic TyConP Source #

Instance details

Defined in Language.Haskell.Liquid.Types.RType

Associated Types

type Rep TyConP

Instance details

Defined in Language.Haskell.Liquid.Types.RType

type Rep TyConP = D1 ('MetaData "TyConP" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "TyConP" 'PrefixI 'True) ((S1 ('MetaSel ('Just "tcpLoc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SourcePos) :*: (S1 ('MetaSel ('Just "tcpCon") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TyCon) :*: S1 ('MetaSel ('Just "tcpFreeTyVarsTy") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [RTyVar]))) :*: ((S1 ('MetaSel ('Just "tcpFreePredTy") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [PVar RSort]) :*: S1 ('MetaSel ('Just "tcpVarianceTs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 VarianceInfo)) :*: (S1 ('MetaSel ('Just "tcpVariancePs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 VarianceInfo) :*: S1 ('MetaSel ('Just "tcpSizeFun") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe SizeFun))))))

Methods

from :: TyConP -> Rep TyConP x #

to :: Rep TyConP x -> TyConP #

Show TyConP Source #

Instance details

Defined in Language.Haskell.Liquid.Types.RType

Methods

showsPrec :: Int -> TyConP -> ShowS #

show :: TyConP -> String #

showList :: [TyConP] -> ShowS #

PPrint TyConP Source #

Instance details

Defined in Language.Haskell.Liquid.Types.RType

Methods

pprintTidy :: Tidy -> TyConP -> Doc #

pprintPrec :: Int -> Tidy -> TyConP -> Doc #

Loc TyConP Source #

Instance details

Defined in Language.Haskell.Liquid.Types.RType

Methods

srcSpan :: TyConP -> SrcSpan #

type Rep TyConP Source #

Instance details

Defined in Language.Haskell.Liquid.Types.RType

type Rep TyConP = D1 ('MetaData "TyConP" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "TyConP" 'PrefixI 'True) ((S1 ('MetaSel ('Just "tcpLoc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SourcePos) :*: (S1 ('MetaSel ('Just "tcpCon") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TyCon) :*: S1 ('MetaSel ('Just "tcpFreeTyVarsTy") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [RTyVar]))) :*: ((S1 ('MetaSel ('Just "tcpFreePredTy") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [PVar RSort]) :*: S1 ('MetaSel ('Just "tcpVarianceTs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 VarianceInfo)) :*: (S1 ('MetaSel ('Just "tcpVariancePs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 VarianceInfo) :*: S1 ('MetaSel ('Just "tcpSizeFun") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe SizeFun))))))

Orphan instances

Show DataCon Source #
Instance details Methods showsPrec :: Int -> DataCon -> ShowS # show :: DataCon -> String # showList :: [DataCon] -> ShowS #
PPrint DataCon Source #
Instance details Methods pprintTidy :: Tidy -> DataCon -> Doc # pprintPrec :: Int -> Tidy -> DataCon -> Doc #