Safe Haskell | None |
---|---|
Language | Haskell98 |
- type PrType = RRType Predicate
- data TyConP = TyConP {
- freeTyVarsTy :: ![RTyVar]
- freePredTy :: ![PVar RSort]
- freeLabelTy :: ![Symbol]
- varianceTs :: !VarianceInfo
- variancePs :: !VarianceInfo
- sizeFun :: !(Maybe (Symbol -> Expr))
- 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
TyConP | |
|
dataConTy :: Monoid r => HashMap RTyVar (RType RTyCon RTyVar r) -> Type -> RType RTyCon RTyVar r Source
dataConPSpecType :: DataCon -> DataConP -> SpecType 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