liquidhaskell-0.2.1.0: Liquid Types for Haskell

Safe HaskellNone
LanguageHaskell98

Language.Haskell.Liquid.PredType

Contents

Synopsis

Documentation

type PrType = RRType Predicate Source

data TyConP Source

Constructors

TyConP 

Fields

freeTyVarsTy :: ![RTyVar]
 
freePredTy :: ![PVar RSort]
 
freeLabelTy :: ![Symbol]
 
covPs :: ![Int]

indexes of covariant predicate arguments

contravPs :: ![Int]

indexes of contravariant predicate arguments

sizeFun :: !(Maybe (Symbol -> Expr))
 

Instances

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

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

dataConPSpecType :: DataCon -> DataConP -> SpecType Source

makeTyConInfo :: [(TyCon, TyConP)] -> HashMap TyCon RTyCon Source

unify :: Maybe PrType -> SpecType -> SpecType Source

Unify PrType with SpecType -------------------------------------------

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

Compute Type of GHC CoreExpr

exprType :: CoreExpr -> Type 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