Language.Futhark.TypeChecker.Types

Type checker building blocks that do not involve unification.

Documentation

checkTypeExp :: MonadTypeChecker m => TypeExp Name -> m (TypeExp VName, [VName], StructRetType, Liftedness)

Check a type expression, producing:

• The checked expression.
• Size variables for any anonymous sizes in the expression.
• The elaborated type.
• The liftedness of the type.

renameRetType :: MonadTypeChecker m => StructRetType -> m StructRetType

Ensure that the dimensions of the RetType are unique by generating new names for them. This is to avoid name capture.

subtypeOf :: TypeBase () () -> TypeBase () () -> Bool

x `subtypeOf` y is true if x is a subtype of y (or equal to y), meaning x is valid whenever y is. Ignores sizes. Mostly used for checking uniqueness.

subuniqueOf :: Uniqueness -> Uniqueness -> Bool

x subuniqueOf y is true if x is not less unique than y.

addAliasesFromType :: StructType -> PatType -> PatType

The two types are assumed to be structurally equal, but not necessarily regarding sizes. Adds aliases from the latter to the former.

checkForDuplicateNames :: MonadTypeChecker m => [UncheckedTypeParam] -> [UncheckedPat] -> m ()

Check for duplication of names inside a binding group.

checkTypeParams :: MonadTypeChecker m => [TypeParamBase Name] -> ([TypeParamBase VName] -> m a) -> m a

checkTypeParams ps m checks the type parameters ps, then invokes the continuation m with the checked parameters, while extending the monadic name map with ps.

typeParamToArg :: TypeParam -> StructTypeArg

Construct a type argument corresponding to a type parameter.

data Subst t

A type substitution may be a substitution or a yet-unknown substitution (but which is certainly an overloaded primitive type!). The latter is used to remove aliases from types that are yet-unknown but that we know cannot carry aliases (see issue #682).

Constructors

Subst [TypeParam] t

PrimSubst

SizeSubst Size

Instances

Functor Subst

Defined in Language.Futhark.TypeChecker.Types

Methods

fmap :: (a -> b) -> Subst a -> Subst b

(<$) :: a -> Subst b -> Subst a

Show t => Show (Subst t)

Defined in Language.Futhark.TypeChecker.Types

Methods

showsPrec :: Int -> Subst t -> ShowS

show :: Subst t -> String

showList :: [Subst t] -> ShowS

Pretty t => Pretty (Subst t)

Defined in Language.Futhark.TypeChecker.Types

Methods

ppr :: Subst t -> Doc

pprPrec :: Int -> Subst t -> Doc

pprList :: [Subst t] -> Doc

substFromAbbr :: TypeBinding -> Subst StructRetType

Create a type substitution corresponding to a type binding.

type TypeSubs = VName -> Maybe (Subst StructRetType)

Substitutions to apply in a type.

class Substitutable a where

Class of types which allow for substitution of types with no annotations for type variable names.

Methods

applySubst :: TypeSubs -> a -> a

Instances

Substitutable Pat

Defined in Language.Futhark.TypeChecker.Types

Methods

applySubst :: TypeSubs -> Pat -> Pat

Substitutable Size

Defined in Language.Futhark.TypeChecker.Types

Methods

applySubst :: TypeSubs -> Size -> Size

Substitutable d => Substitutable (Shape d)

Defined in Language.Futhark.TypeChecker.Types

Methods

applySubst :: TypeSubs -> Shape d -> Shape d

Substitutable (RetTypeBase Size Aliasing)

Defined in Language.Futhark.TypeChecker.Types

Methods

applySubst :: TypeSubs -> RetTypeBase Size Aliasing -> RetTypeBase Size Aliasing

Substitutable (RetTypeBase Size ())

Defined in Language.Futhark.TypeChecker.Types

Methods

applySubst :: TypeSubs -> RetTypeBase Size () -> RetTypeBase Size ()

Substitutable (TypeBase Size Aliasing)

Defined in Language.Futhark.TypeChecker.Types

Methods

applySubst :: TypeSubs -> TypeBase Size Aliasing -> TypeBase Size Aliasing

Substitutable (TypeBase Size ())

Defined in Language.Futhark.TypeChecker.Types

Methods

applySubst :: TypeSubs -> TypeBase Size () -> TypeBase Size ()

substTypesAny :: Monoid as => (VName -> Maybe (Subst (RetTypeBase Size as))) -> TypeBase Size as -> TypeBase Size as

Perform substitutions, from type names to types, on a type. Works regardless of what shape and uniqueness information is attached to the type.

Witnesses

mustBeExplicitInType :: StructType -> Set VName

Figure out which of the sizes in a parameter type must be passed explicitly, because their first use is as something else than just an array dimension.

mustBeExplicitInBinding :: StructType -> Set VName

Figure out which of the sizes in a binding type must be passed explicitly, because their first use is as something else than just an array dimension.

determineSizeWitnesses :: StructType -> (Set VName, Set VName)

Determine which of the sizes in a type are used as sizes outside of functions in the type, and which are not. The former are said to be "witnessed" by this type, while the latter are not. In practice, the latter means that the actual sizes must come from somewhere else.