liquidhaskell-0.8.0.2: Liquid Types for Haskell

Safe HaskellNone
LanguageHaskell98

Language.Haskell.Liquid.Types.PredType

Contents

Synopsis

Documentation

data TyConP Source #

Instances

Data TyConP Source # 

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 :: (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 # 

Associated Types

type Rep TyConP :: * -> * #

Methods

from :: TyConP -> Rep TyConP x #

to :: Rep TyConP x -> TyConP #

type Rep TyConP Source # 
type Rep TyConP

data DataConP Source #

Constructors

DataConP 

Fields

Instances

Data DataConP Source # 

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 :: (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 # 

Associated Types

type Rep DataConP :: * -> * #

Methods

from :: DataConP -> Rep DataConP x #

to :: Rep DataConP x -> DataConP #

Loc DataConP Source # 

Methods

srcSpan :: DataConP -> SrcSpan

ExpandAliases DataConP Source # 
type Rep DataConP 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 #

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 #

Orphan instances