| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell98 |
Language.Haskell.Liquid.Types.PredType
Synopsis
- type PrType = RRType Predicate
- data TyConP = TyConP {
- tcpLoc :: !SourcePos
- tcpCon :: !TyCon
- tcpFreeTyVarsTy :: ![RTyVar]
- tcpFreePredTy :: ![PVar RSort]
- tcpVarianceTs :: !VarianceInfo
- tcpVariancePs :: !VarianceInfo
- tcpSizeFun :: !(Maybe SizeFun)
- data DataConP = DataConP {}
- 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 :: PVar BSort -> PVar BSort -> BareType -> BareType
Documentation
Constructors
| TyConP | |
Fields
| |
Instances
Constructors
| DataConP | |
Fields
| |
Instances
| Data DataConP Source # | |
Defined in Language.Haskell.Liquid.Types.Types 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 # | |
| Show DataConP Source # | |
| PPrint DataConP Source # | |
Defined in Language.Haskell.Liquid.Types.PredType | |
| Loc DataConP Source # |
Here the |
Defined in Language.Haskell.Liquid.Types.Types | |
| type Rep DataConP Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
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
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 -------
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]`
should be elsewhere
dataConWorkRep :: DataCon -> SpecRep Source #