Futhark.TypeCheck

The type checker checks whether the program is type-consistent.

Interface

checkProg :: Checkable lore => Prog (Aliases lore) -> Either (TypeError lore) ()

Type check a program containing arbitrary type information, yielding either a type error or a program with complete type information.

data TypeError lore

A type error.

Constructors

Error [String] (ErrorCase lore)

Instances

Checkable lore => Show (TypeError lore)

Defined in Futhark.TypeCheck

Methods

showsPrec :: Int -> TypeError lore -> ShowS

show :: TypeError lore -> String

showList :: [TypeError lore] -> ShowS

data ErrorCase lore

Information about an error during type checking. The Show instance for this type produces a human-readable description.

Constructors

TypeError String

UnexpectedType (Exp lore) Type [Type]

ReturnTypeError Name [ExtType] [ExtType]

DupDefinitionError Name

DupParamError Name VName

DupPatternError VName

InvalidPatternError (Pattern (Aliases lore)) [ExtType] (Maybe String)

UnknownVariableError VName

UnknownFunctionError Name

ParameterMismatch (Maybe Name) [Type] [Type]

SlicingError Int Int

BadAnnotation String Type Type

ReturnAliased Name VName

UniqueReturnAliased Name

NotAnArray VName Type

PermutationError [Int] Int (Maybe VName)

Instances

Checkable lore => Show (ErrorCase lore)

Defined in Futhark.TypeCheck

Methods

showsPrec :: Int -> ErrorCase lore -> ShowS

show :: ErrorCase lore -> String

showList :: [ErrorCase lore] -> ShowS

Extensionality

data TypeM lore a

The type checker runs in this monad.

Instances

MonadState Names (TypeM lore)

Defined in Futhark.TypeCheck

Methods

get :: TypeM lore Names

put :: Names -> TypeM lore ()

state :: (Names -> (a, Names)) -> TypeM lore a

Monad (TypeM lore)

Defined in Futhark.TypeCheck

Methods

(>>=) :: TypeM lore a -> (a -> TypeM lore b) -> TypeM lore b

(>>) :: TypeM lore a -> TypeM lore b -> TypeM lore b

return :: a -> TypeM lore a

Functor (TypeM lore)

Defined in Futhark.TypeCheck

Methods

fmap :: (a -> b) -> TypeM lore a -> TypeM lore b

(<$) :: a -> TypeM lore b -> TypeM lore a

Applicative (TypeM lore)

Defined in Futhark.TypeCheck

Methods

pure :: a -> TypeM lore a

(<*>) :: TypeM lore (a -> b) -> TypeM lore a -> TypeM lore b

liftA2 :: (a -> b -> c) -> TypeM lore a -> TypeM lore b -> TypeM lore c

(*>) :: TypeM lore a -> TypeM lore b -> TypeM lore b

(<*) :: TypeM lore a -> TypeM lore b -> TypeM lore a

Checkable lore => HasScope (Aliases lore) (TypeM lore)

Defined in Futhark.TypeCheck

Methods

lookupType :: VName -> TypeM lore Type

lookupInfo :: VName -> TypeM lore (NameInfo (Aliases lore))

askScope :: TypeM lore (Scope (Aliases lore))

asksScope :: (Scope (Aliases lore) -> a) -> TypeM lore a

bad :: ErrorCase lore -> TypeM lore a

context :: String -> TypeM lore a -> TypeM lore a

Add information about what is being type-checked to the current context. Liberal use of this combinator makes it easier to track type errors, as the strings are added to type errors signalled via bad.

message :: Pretty a => String -> a -> String

class (Attributes lore, CanBeAliased (Op lore), CheckableOp lore) => Checkable lore where

The class of lores that can be type-checked.

Minimal complete definition

Nothing

Methods

checkExpLore :: ExpAttr lore -> TypeM lore ()

default checkExpLore :: ExpAttr lore ~ () => ExpAttr lore -> TypeM lore ()

checkBodyLore :: BodyAttr lore -> TypeM lore ()

default checkBodyLore :: BodyAttr lore ~ () => BodyAttr lore -> TypeM lore ()

checkFParamLore :: VName -> FParamAttr lore -> TypeM lore ()

default checkFParamLore :: FParamAttr lore ~ DeclType => VName -> FParamAttr lore -> TypeM lore ()

checkLParamLore :: VName -> LParamAttr lore -> TypeM lore ()

default checkLParamLore :: LParamAttr lore ~ Type => VName -> LParamAttr lore -> TypeM lore ()

checkLetBoundLore :: VName -> LetAttr lore -> TypeM lore ()

default checkLetBoundLore :: LetAttr lore ~ Type => VName -> LetAttr lore -> TypeM lore ()

checkRetType :: [RetType lore] -> TypeM lore ()

default checkRetType :: RetType lore ~ DeclExtType => [RetType lore] -> TypeM lore ()

matchPattern :: Pattern (Aliases lore) -> Exp (Aliases lore) -> TypeM lore ()

default matchPattern :: Pattern (Aliases lore) -> Exp (Aliases lore) -> TypeM lore ()

primFParam :: VName -> PrimType -> TypeM lore (FParam (Aliases lore))

default primFParam :: FParamAttr lore ~ DeclType => VName -> PrimType -> TypeM lore (FParam (Aliases lore))

matchReturnType :: [RetType lore] -> Result -> TypeM lore ()

default matchReturnType :: RetType lore ~ DeclExtType => [RetType lore] -> Result -> TypeM lore ()

matchBranchType :: [BranchType lore] -> Body (Aliases lore) -> TypeM lore ()

default matchBranchType :: BranchType lore ~ ExtType => [BranchType lore] -> Body (Aliases lore) -> TypeM lore ()

Instances

Checkable SOACS

Defined in Futhark.Representation.SOACS

Methods

checkExpLore :: ExpAttr SOACS -> TypeM SOACS ()

checkBodyLore :: BodyAttr SOACS -> TypeM SOACS ()

checkFParamLore :: VName -> FParamAttr SOACS -> TypeM SOACS ()

checkLParamLore :: VName -> LParamAttr SOACS -> TypeM SOACS ()

checkLetBoundLore :: VName -> LetAttr SOACS -> TypeM SOACS ()

checkRetType :: [RetType SOACS] -> TypeM SOACS ()

matchPattern :: Pattern (Aliases SOACS) -> Exp (Aliases SOACS) -> TypeM SOACS ()

primFParam :: VName -> PrimType -> TypeM SOACS (FParam (Aliases SOACS))

matchReturnType :: [RetType SOACS] -> Result -> TypeM SOACS ()

matchBranchType :: [BranchType SOACS] -> Body (Aliases SOACS) -> TypeM SOACS ()

Checkable Kernels

Defined in Futhark.Representation.Kernels

Methods

checkExpLore :: ExpAttr Kernels -> TypeM Kernels ()

checkBodyLore :: BodyAttr Kernels -> TypeM Kernels ()

checkFParamLore :: VName -> FParamAttr Kernels -> TypeM Kernels ()

checkLParamLore :: VName -> LParamAttr Kernels -> TypeM Kernels ()

checkLetBoundLore :: VName -> LetAttr Kernels -> TypeM Kernels ()

checkRetType :: [RetType Kernels] -> TypeM Kernels ()

matchPattern :: Pattern (Aliases Kernels) -> Exp (Aliases Kernels) -> TypeM Kernels ()

primFParam :: VName -> PrimType -> TypeM Kernels (FParam (Aliases Kernels))

matchReturnType :: [RetType Kernels] -> Result -> TypeM Kernels ()

matchBranchType :: [BranchType Kernels] -> Body (Aliases Kernels) -> TypeM Kernels ()

Checkable ExplicitMemory

Defined in Futhark.Representation.ExplicitMemory

Methods

checkExpLore :: ExpAttr ExplicitMemory -> TypeM ExplicitMemory ()

checkBodyLore :: BodyAttr ExplicitMemory -> TypeM ExplicitMemory ()

checkFParamLore :: VName -> FParamAttr ExplicitMemory -> TypeM ExplicitMemory ()

checkLParamLore :: VName -> LParamAttr ExplicitMemory -> TypeM ExplicitMemory ()

checkLetBoundLore :: VName -> LetAttr ExplicitMemory -> TypeM ExplicitMemory ()

checkRetType :: [RetType ExplicitMemory] -> TypeM ExplicitMemory ()

matchPattern :: Pattern (Aliases ExplicitMemory) -> Exp (Aliases ExplicitMemory) -> TypeM ExplicitMemory ()

primFParam :: VName -> PrimType -> TypeM ExplicitMemory (FParam (Aliases ExplicitMemory))

matchReturnType :: [RetType ExplicitMemory] -> Result -> TypeM ExplicitMemory ()

matchBranchType :: [BranchType ExplicitMemory] -> Body (Aliases ExplicitMemory) -> TypeM ExplicitMemory ()

class Attributes lore => CheckableOp lore where

Methods

checkOp :: OpWithAliases (Op lore) -> TypeM lore ()

Used at top level; can be locally changed with checkOpWith.

Instances

CheckableOp SOACS

Defined in Futhark.Representation.SOACS

Methods

checkOp :: OpWithAliases (Op SOACS) -> TypeM SOACS ()

CheckableOp Kernels

Defined in Futhark.Representation.Kernels

Methods

checkOp :: OpWithAliases (Op Kernels) -> TypeM Kernels ()

CheckableOp ExplicitMemory

Defined in Futhark.Representation.ExplicitMemory

Methods

checkOp :: OpWithAliases (Op ExplicitMemory) -> TypeM ExplicitMemory ()

lookupVar :: VName -> TypeM lore (NameInfo (Aliases lore))

lookupAliases :: Checkable lore => VName -> TypeM lore Names

type Occurences = [Occurence]

collectOccurences :: TypeM lore a -> TypeM lore (a, Occurences)

checkOpWith :: (OpWithAliases (Op lore) -> TypeM lore ()) -> TypeM lore a -> TypeM lore a

Checkers

require :: Checkable lore => [Type] -> SubExp -> TypeM lore ()

require ts se causes a '(TypeError vn)' if the type of se is not a subtype of one of the types in ts.

requireI :: Checkable lore => [Type] -> VName -> TypeM lore ()

Variant of require working on variable names.

requirePrimExp :: Checkable lore => PrimType -> PrimExp VName -> TypeM lore ()

checkSubExp :: Checkable lore => SubExp -> TypeM lore Type

checkExp :: Checkable lore => Exp (Aliases lore) -> TypeM lore ()

checkStms :: Checkable lore => Stms (Aliases lore) -> TypeM lore a -> TypeM lore a

checkStm :: Checkable lore => Stm (Aliases lore) -> TypeM lore a -> TypeM lore a

checkType :: Checkable lore => TypeBase Shape u -> TypeM lore ()

checkExtType :: Checkable lore => TypeBase ExtShape u -> TypeM lore ()

matchExtPattern :: Checkable lore => Pattern (Aliases lore) -> [ExtType] -> TypeM lore ()

matchExtReturnType :: Checkable lore => [ExtType] -> Result -> TypeM lore ()

matchExtBranchType :: Checkable lore => [ExtType] -> Body (Aliases lore) -> TypeM lore ()

argType :: Arg -> Type

argAliases :: Arg -> Names

Remove all aliases from the Arg.

noArgAliases :: Arg -> Arg

checkArg :: Checkable lore => SubExp -> TypeM lore Arg

checkSOACArrayArgs :: Checkable lore => SubExp -> [VName] -> TypeM lore [Arg]

checkLambda :: Checkable lore => Lambda (Aliases lore) -> [Arg] -> TypeM lore ()

checkBody :: Checkable lore => Body (Aliases lore) -> TypeM lore [Names]

consume :: Checkable lore => Names -> TypeM lore ()

Proclaim that we have written to the given variables.

consumeOnlyParams :: [(VName, Names)] -> TypeM lore a -> TypeM lore a

Permit consumption of only the specified names. If one of these names is consumed, the consumption will be rewritten to be a consumption of the corresponding alias set. Consumption of anything else will result in a type error.

binding :: Checkable lore => Scope (Aliases lore) -> TypeM lore a -> TypeM lore a