ddc-core-0.4.3.1: Disciplined Disciple Compiler core language and type checker.

Safe HaskellSafe
LanguageHaskell98

DDC.Type.Exp.Simple.Predicates

Contents

Description

Predicates on type expressions.

Synopsis

Binders

Atoms

isTVar :: Type n -> Bool Source #

Check whether a type is a TVar

isBot :: Type n -> Bool Source #

Test if some type is an empty TSum

isAtomT :: Type n -> Bool Source #

Check whether a type is a TVar, TCon or is Bottom.

isTExists :: Type n -> Bool Source #

Check whether this type is an existential variable.

Kinds

isDataKind :: Kind n -> Bool Source #

Check if some kind is the data kind.

isRegionKind :: Region n -> Bool Source #

Check if some kind is the region kind.

isEffectKind :: Kind n -> Bool Source #

Check if some kind is the effect kind.

isClosureKind :: Kind n -> Bool Source #

Check if some kind is the closure kind.

isWitnessKind :: Kind n -> Bool Source #

Check if some kind is the witness kind.

Data Types

isAlgDataType :: Eq n => Type n -> Bool Source #

Check whether this type is that of algebraic data.

It needs to have an explicit data constructor out the front, and not a type variable. The constructor must not be the function constructor, and must return a value of kind *.

isWitnessType :: Eq n => Type n -> Bool Source #

Check whether type is a witness constructor

isConstWitType :: Eq n => Type n -> Bool Source #

Check whether this is the type of a Const witness.

isMutableWitType :: Eq n => Type n -> Bool Source #

Check whether this is the type of a Mutable witness.

isDistinctWitType :: Eq n => Type n -> Bool Source #

Check whether this is the type of a Distinct witness.

isFunishTCon :: Type n -> Bool Source #

Check if this is the TyFun or KiFun constructor.

Effect Types

isReadEffect :: Effect n -> Bool Source #

Check whether this is an atomic read effect.

isWriteEffect :: Effect n -> Bool Source #

Check whether this is an atomic write effect.

isAllocEffect :: Effect n -> Bool Source #

Check whether this is an atomic alloc effect.

isSomeReadEffect :: Effect n -> Bool Source #

Check whether an effect is some sort of read effect. Matches Read HeadRead and DeepRead.

isSomeWriteEffect :: Effect n -> Bool Source #

Check whether an effect is some sort of allocation effect. Matches Alloc and DeepAlloc

isSomeAllocEffect :: Effect n -> Bool Source #

Check whether an effect is some sort of allocation effect. Matches Alloc and DeepAlloc