| Safe Haskell | None |
|---|---|
| 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 :: 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
Documentation
Constructors
| TyConP | |
Fields
| |
Instances
Constructors
| DataConP | |
Fields
| |
Instances
| Data DataConP # | |
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 # | |
| Show DataConP # | |
| Generic DataConP # | |
| PPrint DataConP # | |
Defined in Language.Haskell.Liquid.Types.PredType | |
| Loc DataConP # |
Here the |
Defined in Language.Haskell.Liquid.Types.Types | |
| type Rep DataConP # | |
Defined in Language.Haskell.Liquid.Types.Types | |
dataConPSpecType :: DataConP -> [(Var, SpecType)] #
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 #
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 #
Interface: Replace Predicate With Uninterpreted Function Symbol -------
pVartoRConc :: PVar t -> (Symbol, [(a, b, Expr)]) -> Expr #
Dummy Type that represents _all_ abstract-predicates
Compute RType of a given PVar
pvarRType :: (PPrint r, Reftable r) => PVar RSort -> RRType r #
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 #