Safe Haskell	None
Language	Haskell98

Language.Haskell.Liquid.PredType

Contents

Dummy Type that represents _all_ abstract-predicates
Compute RType of a given PVar

Synopsis

Documentation

type PrType = RRType Predicate Source

data TyConP Source

Constructors

TyConP
Fields freeTyVarsTy :: ![RTyVar] freePredTy :: ![PVar RSort] freeLabelTy :: ![Symbol] varianceTs :: !VarianceInfo variancePs :: !VarianceInfo sizeFun :: !(Maybe (Symbol -> Expr))

Instances

Data TyConP
Show TyConP
PPrint TyConP
Typeable * TyConP

data DataConP Source

Constructors

DataConP
Fields dc_loc :: !SourcePos freeTyVars :: ![RTyVar] freePred :: ![PVar RSort] freeLabels :: ![Symbol] tyConsts :: ![SpecType] FIXME: WHAT IS THIS?? tyArgs :: ![(Symbol, SpecType)] These are backwards, why?? tyRes :: !SpecType

Instances

Data DataConP
Show DataConP
PPrint DataConP
Transformable DataConP
Typeable * DataConP

dataConTy :: Monoid r => HashMap RTyVar (RType RTyCon RTyVar r) -> Type -> RType RTyCon RTyVar r Source

dataConPSpecType :: DataCon -> DataConP -> SpecType Source

makeTyConInfo :: [(TyCon, TyConP)] -> HashMap TyCon RTyCon 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)]) -> Refa) -> UReft Reft -> UReft Reft Source

pVartoRConc :: PVar t -> (Symbol, [(a, b, Expr)]) -> Refa 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] -> Pred Source

wiredSortedSyms :: [(Symbol, Sort)] Source

Documentation

Dummy Type that represents _all_ abstract-predicates

Compute RType of a given PVar

Dummy `Type` that represents _all_ abstract-predicates

Compute `RType` of a given `PVar`