Language.Haskell.Liquid.Types.PredType

Documentation

type PrType = RRType Predicate

data TyConP

Constructors

TyConP

Fields

• tcpLoc :: !SourcePos
• tcpCon :: !TyCon
• tcpFreeTyVarsTy :: ![RTyVar]
• tcpFreePredTy :: ![PVar RSort]
• tcpVarianceTs :: !VarianceInfo
• tcpVariancePs :: !VarianceInfo
• tcpSizeFun :: !(Maybe SizeFun)

Instances

Data TyConP

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) -> TyConP -> c TyConP

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TyConP

toConstr :: TyConP -> Constr

dataTypeOf :: TyConP -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TyConP)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TyConP)

gmapT :: (forall b. Data b => b -> b) -> TyConP -> TyConP

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TyConP -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TyConP -> r

gmapQ :: (forall d. Data d => d -> u) -> TyConP -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> TyConP -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TyConP -> m TyConP

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TyConP -> m TyConP

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TyConP -> m TyConP

Show TyConP

Defined in Language.Haskell.Liquid.Types.PredType

Methods

showsPrec :: Int -> TyConP -> ShowS

show :: TyConP -> String

showList :: [TyConP] -> ShowS

Generic TyConP

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep TyConP :: Type -> Type

Methods

from :: TyConP -> Rep TyConP x

to :: Rep TyConP x -> TyConP

PPrint TyConP

Defined in Language.Haskell.Liquid.Types.PredType

Methods

pprintTidy :: Tidy -> TyConP -> Doc

pprintPrec :: Int -> Tidy -> TyConP -> Doc

Loc TyConP

Defined in Language.Haskell.Liquid.Types.Types

Methods

srcSpan :: TyConP -> SrcSpan

Qualify TyConP

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> TyConP -> TyConP

type Rep TyConP

Defined in Language.Haskell.Liquid.Types.Types

type Rep TyConP = D1 ('MetaData "TyConP" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-0.8.10.1-inplace" 'False) (C1 ('MetaCons "TyConP" 'PrefixI 'True) ((S1 ('MetaSel ('Just "tcpLoc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SourcePos) :*: (S1 ('MetaSel ('Just "tcpCon") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TyCon) :*: S1 ('MetaSel ('Just "tcpFreeTyVarsTy") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [RTyVar]))) :*: ((S1 ('MetaSel ('Just "tcpFreePredTy") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [PVar RSort]) :*: S1 ('MetaSel ('Just "tcpVarianceTs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 VarianceInfo)) :*: (S1 ('MetaSel ('Just "tcpVariancePs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 VarianceInfo) :*: S1 ('MetaSel ('Just "tcpSizeFun") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe SizeFun))))))

data DataConP

Constructors

DataConP

Fields

• dcpLoc :: !SourcePos
• dcpCon :: !DataCon

  Corresponding GHC DataCon

• dcpFreeTyVars :: ![RTyVar]

  Type parameters

• dcpFreePred :: ![PVar RSort]

  Abstract Refinement parameters

• dcpTyConstrs :: ![SpecType]

  ? Class constraints (via dataConStupidTheta)

• dcpTyArgs :: ![(Symbol, SpecType)]

  Value parameters

• dcpTyRes :: !SpecType

  Result type , tyData :: !SpecType -- ^ The generic ADT, see [NOTE:DataCon-Data]

• dcpIsGadt :: !Bool

  Was this specified in GADT style (if so, DONT use function names as fields)

• dcpModule :: !Symbol

  Which module was this defined in

• dcpLocE :: !SourcePos

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

Defined in Language.Haskell.Liquid.Types.PredType

Methods

showsPrec :: Int -> DataConP -> ShowS

show :: DataConP -> String

showList :: [DataConP] -> ShowS

Generic DataConP

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep DataConP :: Type -> Type

Methods

from :: DataConP -> Rep DataConP x

to :: Rep DataConP x -> DataConP

PPrint DataConP

Defined in Language.Haskell.Liquid.Types.PredType

Methods

pprintTidy :: Tidy -> DataConP -> Doc

pprintPrec :: Int -> Tidy -> DataConP -> Doc

Loc DataConP

NOTE:DataCon-Data

for each DataConP we also store the type of the constructed data. This is *the same as* tyRes for *vanilla* ADTs (e.g. List, Maybe etc.) but may differ for GADTs. For example,

data Thing a where X :: Thing Int Y :: Thing Bool

Here the DataConP associated with X (resp. Y) has tyRes corresponding to 'Thing Int' (resp. 'Thing Bool'), but in both cases, the tyData should be 'Thing a'.

Defined in Language.Haskell.Liquid.Types.Types

Methods

srcSpan :: DataConP -> SrcSpan

type Rep DataConP

Defined in Language.Haskell.Liquid.Types.Types

type Rep DataConP

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

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

makeTyConInfo :: TCEmb TyCon -> [TyCon] -> [TyConP] -> TyConMap

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

predType :: Type

Interface: Modified CoreSyn.exprType due to predApp -------------------

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]`

substParg :: Functor f => (Symbol, Expr) -> f Predicate -> f Predicate

pApp :: Symbol -> [Expr] -> Expr

pappSort :: Int -> Sort

pappArity :: Int

should be elsewhere

dataConWorkRep :: DataCon -> SpecRep

Orphan instances

Show DataConP

Methods

showsPrec :: Int -> DataConP -> ShowS

show :: DataConP -> String

showList :: [DataConP] -> ShowS

Show TyConP

Methods

showsPrec :: Int -> TyConP -> ShowS

show :: TyConP -> String

showList :: [TyConP] -> ShowS

PPrint DataConP

Methods

pprintTidy :: Tidy -> DataConP -> Doc

pprintPrec :: Int -> Tidy -> DataConP -> Doc

PPrint TyConP

Methods

pprintTidy :: Tidy -> TyConP -> Doc

pprintPrec :: Int -> Tidy -> TyConP -> Doc