| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Haskell.Liquid.Types.PredType
Contents
- type PrType = RRType Predicate
- data TyConP = TyConP {
- ty_loc :: !SourcePos
- freeTyVarsTy :: ![RTyVar]
- freePredTy :: ![PVar RSort]
- freeLabelTy :: ![Symbol]
- varianceTs :: !VarianceInfo
- variancePs :: !VarianceInfo
- sizeFun :: !(Maybe SizeFun)
- data DataConP = DataConP {}
- dataConTy :: Monoid r => HashMap RTyVar (RType RTyCon RTyVar r) -> Type -> RType RTyCon RTyVar r
- dataConPSpecType :: DataCon -> DataConP -> SpecType
- makeTyConInfo :: [(TyCon, TyConP)] -> HashMap TyCon RTyCon
- 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
Documentation
Constructors
| TyConP | |
Fields
| |
Constructors
| DataConP | |
Fields
| |
dataConTy :: Monoid r => HashMap RTyVar (RType RTyCon RTyVar r) -> Type -> RType RTyCon RTyVar r 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
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]`