Safe Haskell	None
Language	Haskell98

Language.Haskell.Liquid.Types.PredType

Contents

Dummy Type that represents _all_ abstract-predicates
Compute RType of a given PVar
should be elsewhere

Synopsis

data TyConP = TyConP {
- tcpLoc :: !SourcePos
- tcpCon :: !TyCon
- tcpFreeTyVarsTy :: ![RTyVar]
- tcpFreePredTy :: ![PVar RSort]
- tcpVarianceTs :: !VarianceInfo
- tcpVariancePs :: !VarianceInfo
- tcpSizeFun :: !(Maybe SizeFun)
}
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
}
dataConTy :: Monoid r => HashMap RTyVar (RType RTyCon RTyVar r) -> Type -> RType RTyCon RTyVar r
dataConPSpecType :: Bool -> DataConP -> [(Var, SpecType)]
makeTyConInfo :: TCEmb TyCon -> [TyCon] -> [TyConP] -> TyConMap
replacePreds :: String -> SpecType -> [(RPVar, SpecProp)] -> SpecType
replacePredsWithRefs :: (UsedPVar, (Symbol, [((), Symbol, Expr)]) -> Expr) -> UReft Reft -> UReft Reft
pVartoRConc :: PVar t -> (Symbol, [(a, b, Expr)]) -> Expr
predType :: Type
pvarRType :: (PPrint r, Reftable r) => PVar RSort -> RRType r
substParg :: Functor f => (Symbol, Expr) -> f Predicate -> f Predicate
pApp :: Symbol -> [Expr] -> Expr
pappSort :: Int -> Sort
pappArity :: Int
dataConWorkRep :: DataCon -> SpecRep
substPVar :: PVarV v (BSortV v) -> PVarV v (BSortV v) -> BareTypeParsed -> BareTypeParsed

Documentation

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

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

dataConTy :: Monoid r => HashMap RTyVar (RType RTyCon RTyVar r) -> Type -> RType RTyCon RTyVar r Source #

dataConPSpecType :: Bool -> DataConP -> [(Var, SpecType)] Source #

dataConPSpecType converts a DataConP, LH's internal representation for a (refined) data constructor into a SpecType for that constructor. TODO: duplicated with Liquid.Measure.makeDataConType

makeTyConInfo :: TCEmb TyCon -> [TyCon] -> [TyConP] -> TyConMap Source #

replacePreds :: String -> SpecType -> [(RPVar, SpecProp)] -> SpecType Source #

Instantiate PVar with RTProp -----------------------------------------------

replacePreds is the main function used to substitute an (abstract) predicate with a concrete Ref, that is either an RProp or RHProp type. The substitution is invoked to obtain the SpecType resulting at predicate application sites in Constraint. The range of the PVar substitutions are fresh or true RefType. That is, there are no further _quantified_ PVar in the target.

replacePredsWithRefs :: (UsedPVar, (Symbol, [((), Symbol, Expr)]) -> Expr) -> UReft Reft -> UReft Reft Source #

Interface: Replace Predicate With Uninterpreted Function Symbol -------

pVartoRConc :: PVar t -> (Symbol, [(a, b, Expr)]) -> Expr Source #

Dummy `Type` that represents _all_ abstract-predicates

predType :: Type Source #

Interface: Modified CoreSyn.exprType due to predApp -------------------

Compute `RType` of a given `PVar`

pvarRType :: (PPrint r, Reftable r) => PVar RSort -> RRType r Source #

pvarRType π returns a trivial RType corresponding to the function signature for a PVar π. For example, if π :: T1 -> T2 -> T3 -> Prop then pvarRType π returns an RType with an RTycon called predRTyCon `RApp predRTyCon [T1, T2, T3]`

substParg :: Functor f => (Symbol, Expr) -> f Predicate -> f Predicate Source #

pApp :: Symbol -> [Expr] -> Expr Source #

pappSort :: Int -> Sort Source #

pappArity :: Int Source #

should be elsewhere

dataConWorkRep :: DataCon -> SpecRep Source #

substPVar :: PVarV v (BSortV v) -> PVarV v (BSortV v) -> BareTypeParsed -> BareTypeParsed Source #

Documentation

Instances

Instances

Dummy Type that represents _all_ abstract-predicates

Compute RType of a given PVar

should be elsewhere

Dummy `Type` that represents _all_ abstract-predicates

Compute `RType` of a given `PVar`