Futhark.IR.TypeCheck

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

Interface

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

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

data TypeError rep

A type error.

Constructors

Error [Text] (ErrorCase rep)

Instances

Checkable rep => Show (TypeError rep)

Defined in Futhark.IR.TypeCheck

Methods

showsPrec :: Int -> TypeError rep -> ShowS

show :: TypeError rep -> String

showList :: [TypeError rep] -> ShowS

data ErrorCase rep

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

Constructors

TypeError Text

UnexpectedType (Exp rep) Type [Type]

ReturnTypeError Name [ExtType] [ExtType]

DupDefinitionError Name

DupParamError Name VName

DupPatError VName

InvalidPatError (Pat (LetDec (Aliases rep))) [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 rep => Show (ErrorCase rep)

Defined in Futhark.IR.TypeCheck

Methods

showsPrec :: Int -> ErrorCase rep -> ShowS

show :: ErrorCase rep -> String

showList :: [ErrorCase rep] -> ShowS

Extensionality

data TypeM rep a

The type checker runs in this monad.

Instances

Applicative (TypeM rep)

Defined in Futhark.IR.TypeCheck

Methods

pure :: a -> TypeM rep a

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

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

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

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

Functor (TypeM rep)

Defined in Futhark.IR.TypeCheck

Methods

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

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

Monad (TypeM rep)

Defined in Futhark.IR.TypeCheck

Methods

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

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

return :: a -> TypeM rep a

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

Defined in Futhark.IR.TypeCheck

Methods

lookupType :: VName -> TypeM rep Type

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

askScope :: TypeM rep (Scope (Aliases rep))

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

bad :: ErrorCase rep -> TypeM rep a

Signal a type error.

context :: Text -> TypeM rep a -> TypeM rep 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.

class (AliasableRep rep, TypedOp (OpC rep (Aliases rep))) => Checkable rep where

The class of representations that can be type-checked.

Minimal complete definition

checkOp

Methods

checkExpDec :: ExpDec rep -> TypeM rep ()

default checkExpDec :: ExpDec rep ~ () => ExpDec rep -> TypeM rep ()

checkBodyDec :: BodyDec rep -> TypeM rep ()

default checkBodyDec :: BodyDec rep ~ () => BodyDec rep -> TypeM rep ()

checkFParamDec :: VName -> FParamInfo rep -> TypeM rep ()

default checkFParamDec :: FParamInfo rep ~ DeclType => VName -> FParamInfo rep -> TypeM rep ()

checkLParamDec :: VName -> LParamInfo rep -> TypeM rep ()

default checkLParamDec :: LParamInfo rep ~ Type => VName -> LParamInfo rep -> TypeM rep ()

checkLetBoundDec :: VName -> LetDec rep -> TypeM rep ()

default checkLetBoundDec :: LetDec rep ~ Type => VName -> LetDec rep -> TypeM rep ()

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

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

matchPat :: Pat (LetDec (Aliases rep)) -> Exp (Aliases rep) -> TypeM rep ()

default matchPat :: Pat (LetDec (Aliases rep)) -> Exp (Aliases rep) -> TypeM rep ()

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

default primFParam :: FParamInfo rep ~ DeclType => VName -> PrimType -> TypeM rep (FParam (Aliases rep))

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

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

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

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

matchLoopResult :: [FParam (Aliases rep)] -> Result -> TypeM rep ()

default matchLoopResult :: FParamInfo rep ~ DeclType => [FParam (Aliases rep)] -> Result -> TypeM rep ()

checkOp :: Op (Aliases rep) -> TypeM rep ()

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

Instances

Checkable GPU

Defined in Futhark.IR.GPU

Methods

checkExpDec :: ExpDec GPU -> TypeM GPU ()

checkBodyDec :: BodyDec GPU -> TypeM GPU ()

checkFParamDec :: VName -> FParamInfo GPU -> TypeM GPU ()

checkLParamDec :: VName -> LParamInfo GPU -> TypeM GPU ()

checkLetBoundDec :: VName -> LetDec GPU -> TypeM GPU ()

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

matchPat :: Pat (LetDec (Aliases GPU)) -> Exp (Aliases GPU) -> TypeM GPU ()

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

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

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

matchLoopResult :: [FParam (Aliases GPU)] -> Result -> TypeM GPU ()

checkOp :: Op (Aliases GPU) -> TypeM GPU ()

Checkable GPUMem

Defined in Futhark.IR.GPUMem

Methods

checkExpDec :: ExpDec GPUMem -> TypeM GPUMem ()

checkBodyDec :: BodyDec GPUMem -> TypeM GPUMem ()

checkFParamDec :: VName -> FParamInfo GPUMem -> TypeM GPUMem ()

checkLParamDec :: VName -> LParamInfo GPUMem -> TypeM GPUMem ()

checkLetBoundDec :: VName -> LetDec GPUMem -> TypeM GPUMem ()

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

matchPat :: Pat (LetDec (Aliases GPUMem)) -> Exp (Aliases GPUMem) -> TypeM GPUMem ()

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

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

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

matchLoopResult :: [FParam (Aliases GPUMem)] -> Result -> TypeM GPUMem ()

checkOp :: Op (Aliases GPUMem) -> TypeM GPUMem ()

Checkable MC

Defined in Futhark.IR.MC

Methods

checkExpDec :: ExpDec MC -> TypeM MC ()

checkBodyDec :: BodyDec MC -> TypeM MC ()

checkFParamDec :: VName -> FParamInfo MC -> TypeM MC ()

checkLParamDec :: VName -> LParamInfo MC -> TypeM MC ()

checkLetBoundDec :: VName -> LetDec MC -> TypeM MC ()

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

matchPat :: Pat (LetDec (Aliases MC)) -> Exp (Aliases MC) -> TypeM MC ()

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

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

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

matchLoopResult :: [FParam (Aliases MC)] -> Result -> TypeM MC ()

checkOp :: Op (Aliases MC) -> TypeM MC ()

Checkable MCMem

Defined in Futhark.IR.MCMem

Methods

checkExpDec :: ExpDec MCMem -> TypeM MCMem ()

checkBodyDec :: BodyDec MCMem -> TypeM MCMem ()

checkFParamDec :: VName -> FParamInfo MCMem -> TypeM MCMem ()

checkLParamDec :: VName -> LParamInfo MCMem -> TypeM MCMem ()

checkLetBoundDec :: VName -> LetDec MCMem -> TypeM MCMem ()

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

matchPat :: Pat (LetDec (Aliases MCMem)) -> Exp (Aliases MCMem) -> TypeM MCMem ()

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

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

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

matchLoopResult :: [FParam (Aliases MCMem)] -> Result -> TypeM MCMem ()

checkOp :: Op (Aliases MCMem) -> TypeM MCMem ()

Checkable SOACS

Defined in Futhark.IR.SOACS

Methods

checkExpDec :: ExpDec SOACS -> TypeM SOACS ()

checkBodyDec :: BodyDec SOACS -> TypeM SOACS ()

checkFParamDec :: VName -> FParamInfo SOACS -> TypeM SOACS ()

checkLParamDec :: VName -> LParamInfo SOACS -> TypeM SOACS ()

checkLetBoundDec :: VName -> LetDec SOACS -> TypeM SOACS ()

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

matchPat :: Pat (LetDec (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 ()

matchLoopResult :: [FParam (Aliases SOACS)] -> Result -> TypeM SOACS ()

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

Checkable Seq

Defined in Futhark.IR.Seq

Methods

checkExpDec :: ExpDec Seq -> TypeM Seq ()

checkBodyDec :: BodyDec Seq -> TypeM Seq ()

checkFParamDec :: VName -> FParamInfo Seq -> TypeM Seq ()

checkLParamDec :: VName -> LParamInfo Seq -> TypeM Seq ()

checkLetBoundDec :: VName -> LetDec Seq -> TypeM Seq ()

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

matchPat :: Pat (LetDec (Aliases Seq)) -> Exp (Aliases Seq) -> TypeM Seq ()

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

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

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

matchLoopResult :: [FParam (Aliases Seq)] -> Result -> TypeM Seq ()

checkOp :: Op (Aliases Seq) -> TypeM Seq ()

Checkable SeqMem

Defined in Futhark.IR.SeqMem

Methods

checkExpDec :: ExpDec SeqMem -> TypeM SeqMem ()

checkBodyDec :: BodyDec SeqMem -> TypeM SeqMem ()

checkFParamDec :: VName -> FParamInfo SeqMem -> TypeM SeqMem ()

checkLParamDec :: VName -> LParamInfo SeqMem -> TypeM SeqMem ()

checkLetBoundDec :: VName -> LetDec SeqMem -> TypeM SeqMem ()

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

matchPat :: Pat (LetDec (Aliases SeqMem)) -> Exp (Aliases SeqMem) -> TypeM SeqMem ()

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

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

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

matchLoopResult :: [FParam (Aliases SeqMem)] -> Result -> TypeM SeqMem ()

checkOp :: Op (Aliases SeqMem) -> TypeM SeqMem ()

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

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

checkOpWith :: (Op (Aliases rep) -> TypeM rep ()) -> TypeM rep a -> TypeM rep a

Checkers

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

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 rep => [Type] -> VName -> TypeM rep ()

Variant of require working on variable names.

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

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

checkCerts :: Checkable rep => Certs -> TypeM rep ()

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

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

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

checkSlice :: Checkable rep => Type -> Slice SubExp -> TypeM rep ()

Check a slicing operation of an array of the provided type.

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

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

matchExtPat :: Checkable rep => Pat (LetDec (Aliases rep)) -> [ExtType] -> TypeM rep ()

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

argType :: Arg -> Type

noArgAliases :: Arg -> Arg

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

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

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

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

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

Proclaim that we have written to the given variables.

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

alternative :: TypeM rep a -> TypeM rep b -> TypeM rep (a, b)

Type check two mutually exclusive control flow branches. Think if. This interacts with consumption checking, as it is OK for an array to be consumed in both branches.