futhark-0.25.15: An optimising compiler for a functional, array-oriented language.
Safe HaskellSafe-Inferred
LanguageGHC2021

Language.Futhark.TypeChecker.Types

Contents

Description

Type checker building blocks that do not involve unification.

Synopsis

Documentation

checkTypeExp :: (MonadTypeChecker m, Pretty df) => (df -> m Exp) -> TypeExp df VName -> m (TypeExp Exp VName, [VName], ResRetType, Liftedness) Source #

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 => ResRetType -> m ResRetType Source #

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

typeParamToArg :: TypeParam -> StructTypeArg Source #

Construct a type argument corresponding to a type parameter.

data Subst t Source #

A type substitution may be a substitution or a yet-unknown substitution (but which is certainly an overloaded primitive type!).

Constructors

Subst [TypeParam] t 
ExpSubst Exp 

Instances

Instances details
Functor Subst Source # 
Instance details

Defined in Language.Futhark.TypeChecker.Types

Methods

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

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

Show t => Show (Subst t) Source # 
Instance details

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) Source # 
Instance details

Defined in Language.Futhark.TypeChecker.Types

Methods

pretty :: Subst t -> Doc ann #

prettyList :: [Subst t] -> Doc ann #

substFromAbbr :: TypeBinding -> Subst StructRetType Source #

Create a type substitution corresponding to a type binding.

type TypeSubs = VName -> Maybe (Subst StructRetType) Source #

Substitutions to apply in a type.

class Substitutable a where Source #

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

Methods

applySubst :: TypeSubs -> a -> a Source #

Instances

Instances details
Substitutable Exp Source # 
Instance details

Defined in Language.Futhark.TypeChecker.Types

Methods

applySubst :: TypeSubs -> Exp -> Exp Source #

Substitutable ParamType Source # 
Instance details

Defined in Language.Futhark.TypeChecker.Types

Substitutable StructType Source # 
Instance details

Defined in Language.Futhark.TypeChecker.Types

Substitutable (Pat ParamType) Source # 
Instance details

Defined in Language.Futhark.TypeChecker.Types

Substitutable (Pat StructType) Source # 
Instance details

Defined in Language.Futhark.TypeChecker.Types

Substitutable d => Substitutable (Shape d) Source # 
Instance details

Defined in Language.Futhark.TypeChecker.Types

Methods

applySubst :: TypeSubs -> Shape d -> Shape d Source #

Substitutable (RetTypeBase Size NoUniqueness) Source # 
Instance details

Defined in Language.Futhark.TypeChecker.Types

Substitutable (RetTypeBase Size Uniqueness) Source # 
Instance details

Defined in Language.Futhark.TypeChecker.Types

Substitutable (TypeBase Size Uniqueness) Source # 
Instance details

Defined in Language.Futhark.TypeChecker.Types

substTypesAny :: Monoid u => (VName -> Maybe (Subst (RetTypeBase Size u))) -> TypeBase Size u -> TypeBase Size u Source #

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 Source #

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 Source #

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) Source #

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.