Safe Haskell	Trustworthy
Language	Haskell2010

Futhark.TypeCheck

Contents

Interface
Extensionality
Checkers

Description

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

Synopsis

checkProg :: Checkable lore => Prog (Aliases lore) -> Either (TypeError lore) ()
data TypeError lore = Error [String] (ErrorCase lore)
data ErrorCase lore
- = 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)
data TypeM lore a
bad :: ErrorCase lore -> TypeM lore a
context :: String -> TypeM lore a -> TypeM lore a
message :: Pretty a => String -> a -> String
class (ASTLore lore, CanBeAliased (Op lore), CheckableOp lore) => Checkable lore where
- checkExpLore :: ExpDec lore -> TypeM lore ()
- checkBodyLore :: BodyDec lore -> TypeM lore ()
- checkFParamLore :: VName -> FParamInfo lore -> TypeM lore ()
- checkLParamLore :: VName -> LParamInfo lore -> TypeM lore ()
- checkLetBoundLore :: VName -> LetDec lore -> TypeM lore ()
- checkRetType :: [RetType lore] -> TypeM lore ()
- matchPattern :: Pattern (Aliases lore) -> Exp (Aliases lore) -> TypeM lore ()
- primFParam :: VName -> PrimType -> TypeM lore (FParam (Aliases lore))
- matchReturnType :: [RetType lore] -> Result -> TypeM lore ()
- matchBranchType :: [BranchType lore] -> Body (Aliases lore) -> TypeM lore ()
- matchLoopResult :: [FParam (Aliases lore)] -> [FParam (Aliases lore)] -> [SubExp] -> TypeM lore ()
class ASTLore lore => CheckableOp lore where
- checkOp :: OpWithAliases (Op lore) -> TypeM lore ()
lookupVar :: VName -> TypeM lore (NameInfo (Aliases lore))
lookupAliases :: Checkable lore => VName -> TypeM lore Names
checkOpWith :: (OpWithAliases (Op lore) -> TypeM lore ()) -> TypeM lore a -> TypeM lore a
require :: Checkable lore => [Type] -> SubExp -> TypeM lore ()
requireI :: Checkable lore => [Type] -> VName -> TypeM lore ()
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 ()
matchExtBranchType :: Checkable lore => [ExtType] -> Body (Aliases lore) -> TypeM lore ()
argType :: Arg -> Type
argAliases :: Arg -> Names
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 ()
consumeOnlyParams :: [(VName, Names)] -> TypeM lore a -> TypeM lore a
binding :: Checkable lore => Scope (Aliases lore) -> TypeM lore a -> TypeM lore a
alternative :: TypeM lore a -> TypeM lore b -> TypeM lore (a, b)

Interface

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

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

data TypeError lore Source #

A type error.

Constructors

Error [String] (ErrorCase lore)

Instances

Instances details

Checkable lore => Show (TypeError lore) Source #
Instance details Defined in Futhark.TypeCheck Methods showsPrec :: Int -> TypeError lore -> ShowS # show :: TypeError lore -> String # showList :: [TypeError lore] -> ShowS #

data ErrorCase lore Source #

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

Instances

Instances details

Checkable lore => Show (ErrorCase lore) Source #
Instance details Defined in Futhark.TypeCheck Methods showsPrec :: Int -> ErrorCase lore -> ShowS # show :: ErrorCase lore -> String # showList :: [ErrorCase lore] -> ShowS #

Extensionality

data TypeM lore a Source #

The type checker runs in this monad.

Instances

Instances details

MonadState Names (TypeM lore) Source #
Instance details Defined in Futhark.TypeCheck Methods get :: TypeM lore Names # put :: Names -> TypeM lore () # state :: (Names -> (a, Names)) -> TypeM lore a #
Monad (TypeM lore) Source #
Instance details 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) Source #
Instance details Defined in Futhark.TypeCheck Methods fmap :: (a -> b) -> TypeM lore a -> TypeM lore b # (<$) :: a -> TypeM lore b -> TypeM lore a #
Applicative (TypeM lore) Source #
Instance details 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) Source #
Instance details Defined in Futhark.TypeCheck Methods lookupType :: VName -> TypeM lore Type Source # lookupInfo :: VName -> TypeM lore (NameInfo (Aliases lore)) Source # askScope :: TypeM lore (Scope (Aliases lore)) Source # asksScope :: (Scope (Aliases lore) -> a) -> TypeM lore a Source #

bad :: ErrorCase lore -> TypeM lore a Source #

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

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

class (ASTLore lore, CanBeAliased (Op lore), CheckableOp lore) => Checkable lore where Source #

The class of lores that can be type-checked.

Minimal complete definition

Nothing

Methods

checkExpLore :: ExpDec lore -> TypeM lore () Source #

default checkExpLore :: ExpDec lore ~ () => ExpDec lore -> TypeM lore () Source #

checkBodyLore :: BodyDec lore -> TypeM lore () Source #

default checkBodyLore :: BodyDec lore ~ () => BodyDec lore -> TypeM lore () Source #

checkFParamLore :: VName -> FParamInfo lore -> TypeM lore () Source #

default checkFParamLore :: FParamInfo lore ~ DeclType => VName -> FParamInfo lore -> TypeM lore () Source #

checkLParamLore :: VName -> LParamInfo lore -> TypeM lore () Source #

default checkLParamLore :: LParamInfo lore ~ Type => VName -> LParamInfo lore -> TypeM lore () Source #

checkLetBoundLore :: VName -> LetDec lore -> TypeM lore () Source #

default checkLetBoundLore :: LetDec lore ~ Type => VName -> LetDec lore -> TypeM lore () Source #

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

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

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

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

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

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

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

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

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

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

matchLoopResult :: [FParam (Aliases lore)] -> [FParam (Aliases lore)] -> [SubExp] -> TypeM lore () Source #

default matchLoopResult :: FParamInfo lore ~ DeclType => [FParam (Aliases lore)] -> [FParam (Aliases lore)] -> [SubExp] -> TypeM lore () Source #

Instances

Instances details

Checkable Seq Source #
Instance details Defined in Futhark.IR.Seq Methods checkExpLore :: ExpDec Seq -> TypeM Seq () Source # checkBodyLore :: BodyDec Seq -> TypeM Seq () Source # checkFParamLore :: VName -> FParamInfo Seq -> TypeM Seq () Source # checkLParamLore :: VName -> LParamInfo Seq -> TypeM Seq () Source # checkLetBoundLore :: VName -> LetDec Seq -> TypeM Seq () Source # checkRetType :: [RetType Seq] -> TypeM Seq () Source # matchPattern :: Pattern (Aliases Seq) -> Exp (Aliases Seq) -> TypeM Seq () Source # primFParam :: VName -> PrimType -> TypeM Seq (FParam (Aliases Seq)) Source # matchReturnType :: [RetType Seq] -> Result -> TypeM Seq () Source # matchBranchType :: [BranchType Seq] -> Body (Aliases Seq) -> TypeM Seq () Source # matchLoopResult :: [FParam (Aliases Seq)] -> [FParam (Aliases Seq)] -> [SubExp] -> TypeM Seq () Source #
Checkable SOACS Source #
Instance details Defined in Futhark.IR.SOACS Methods checkExpLore :: ExpDec SOACS -> TypeM SOACS () Source # checkBodyLore :: BodyDec SOACS -> TypeM SOACS () Source # checkFParamLore :: VName -> FParamInfo SOACS -> TypeM SOACS () Source # checkLParamLore :: VName -> LParamInfo SOACS -> TypeM SOACS () Source # checkLetBoundLore :: VName -> LetDec SOACS -> TypeM SOACS () Source # checkRetType :: [RetType SOACS] -> TypeM SOACS () Source # matchPattern :: Pattern (Aliases SOACS) -> Exp (Aliases SOACS) -> TypeM SOACS () Source # primFParam :: VName -> PrimType -> TypeM SOACS (FParam (Aliases SOACS)) Source # matchReturnType :: [RetType SOACS] -> Result -> TypeM SOACS () Source # matchBranchType :: [BranchType SOACS] -> Body (Aliases SOACS) -> TypeM SOACS () Source # matchLoopResult :: [FParam (Aliases SOACS)] -> [FParam (Aliases SOACS)] -> [SubExp] -> TypeM SOACS () Source #
Checkable MCMem Source #
Instance details Defined in Futhark.IR.MCMem Methods checkExpLore :: ExpDec MCMem -> TypeM MCMem () Source # checkBodyLore :: BodyDec MCMem -> TypeM MCMem () Source # checkFParamLore :: VName -> FParamInfo MCMem -> TypeM MCMem () Source # checkLParamLore :: VName -> LParamInfo MCMem -> TypeM MCMem () Source # checkLetBoundLore :: VName -> LetDec MCMem -> TypeM MCMem () Source # checkRetType :: [RetType MCMem] -> TypeM MCMem () Source # matchPattern :: Pattern (Aliases MCMem) -> Exp (Aliases MCMem) -> TypeM MCMem () Source # primFParam :: VName -> PrimType -> TypeM MCMem (FParam (Aliases MCMem)) Source # matchReturnType :: [RetType MCMem] -> Result -> TypeM MCMem () Source # matchBranchType :: [BranchType MCMem] -> Body (Aliases MCMem) -> TypeM MCMem () Source # matchLoopResult :: [FParam (Aliases MCMem)] -> [FParam (Aliases MCMem)] -> [SubExp] -> TypeM MCMem () Source #
Checkable MC Source #
Instance details Defined in Futhark.IR.MC Methods checkExpLore :: ExpDec MC -> TypeM MC () Source # checkBodyLore :: BodyDec MC -> TypeM MC () Source # checkFParamLore :: VName -> FParamInfo MC -> TypeM MC () Source # checkLParamLore :: VName -> LParamInfo MC -> TypeM MC () Source # checkLetBoundLore :: VName -> LetDec MC -> TypeM MC () Source # checkRetType :: [RetType MC] -> TypeM MC () Source # matchPattern :: Pattern (Aliases MC) -> Exp (Aliases MC) -> TypeM MC () Source # primFParam :: VName -> PrimType -> TypeM MC (FParam (Aliases MC)) Source # matchReturnType :: [RetType MC] -> Result -> TypeM MC () Source # matchBranchType :: [BranchType MC] -> Body (Aliases MC) -> TypeM MC () Source # matchLoopResult :: [FParam (Aliases MC)] -> [FParam (Aliases MC)] -> [SubExp] -> TypeM MC () Source #
Checkable SeqMem Source #
Instance details Defined in Futhark.IR.SeqMem Methods checkExpLore :: ExpDec SeqMem -> TypeM SeqMem () Source # checkBodyLore :: BodyDec SeqMem -> TypeM SeqMem () Source # checkFParamLore :: VName -> FParamInfo SeqMem -> TypeM SeqMem () Source # checkLParamLore :: VName -> LParamInfo SeqMem -> TypeM SeqMem () Source # checkLetBoundLore :: VName -> LetDec SeqMem -> TypeM SeqMem () Source # checkRetType :: [RetType SeqMem] -> TypeM SeqMem () Source # matchPattern :: Pattern (Aliases SeqMem) -> Exp (Aliases SeqMem) -> TypeM SeqMem () Source # primFParam :: VName -> PrimType -> TypeM SeqMem (FParam (Aliases SeqMem)) Source # matchReturnType :: [RetType SeqMem] -> Result -> TypeM SeqMem () Source # matchBranchType :: [BranchType SeqMem] -> Body (Aliases SeqMem) -> TypeM SeqMem () Source # matchLoopResult :: [FParam (Aliases SeqMem)] -> [FParam (Aliases SeqMem)] -> [SubExp] -> TypeM SeqMem () Source #
Checkable Kernels Source #
Instance details Defined in Futhark.IR.Kernels Methods checkExpLore :: ExpDec Kernels -> TypeM Kernels () Source # checkBodyLore :: BodyDec Kernels -> TypeM Kernels () Source # checkFParamLore :: VName -> FParamInfo Kernels -> TypeM Kernels () Source # checkLParamLore :: VName -> LParamInfo Kernels -> TypeM Kernels () Source # checkLetBoundLore :: VName -> LetDec Kernels -> TypeM Kernels () Source # checkRetType :: [RetType Kernels] -> TypeM Kernels () Source # matchPattern :: Pattern (Aliases Kernels) -> Exp (Aliases Kernels) -> TypeM Kernels () Source # primFParam :: VName -> PrimType -> TypeM Kernels (FParam (Aliases Kernels)) Source # matchReturnType :: [RetType Kernels] -> Result -> TypeM Kernels () Source # matchBranchType :: [BranchType Kernels] -> Body (Aliases Kernels) -> TypeM Kernels () Source # matchLoopResult :: [FParam (Aliases Kernels)] -> [FParam (Aliases Kernels)] -> [SubExp] -> TypeM Kernels () Source #
Checkable KernelsMem Source #
Instance details Defined in Futhark.IR.KernelsMem Methods checkExpLore :: ExpDec KernelsMem -> TypeM KernelsMem () Source # checkBodyLore :: BodyDec KernelsMem -> TypeM KernelsMem () Source # checkFParamLore :: VName -> FParamInfo KernelsMem -> TypeM KernelsMem () Source # checkLParamLore :: VName -> LParamInfo KernelsMem -> TypeM KernelsMem () Source # checkLetBoundLore :: VName -> LetDec KernelsMem -> TypeM KernelsMem () Source # checkRetType :: [RetType KernelsMem] -> TypeM KernelsMem () Source # matchPattern :: Pattern (Aliases KernelsMem) -> Exp (Aliases KernelsMem) -> TypeM KernelsMem () Source # primFParam :: VName -> PrimType -> TypeM KernelsMem (FParam (Aliases KernelsMem)) Source # matchReturnType :: [RetType KernelsMem] -> Result -> TypeM KernelsMem () Source # matchBranchType :: [BranchType KernelsMem] -> Body (Aliases KernelsMem) -> TypeM KernelsMem () Source # matchLoopResult :: [FParam (Aliases KernelsMem)] -> [FParam (Aliases KernelsMem)] -> [SubExp] -> TypeM KernelsMem () Source #

class ASTLore lore => CheckableOp lore where Source #

Methods

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

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

Instances

Instances details

CheckableOp Seq Source #
Instance details Defined in Futhark.IR.Seq Methods checkOp :: OpWithAliases (Op Seq) -> TypeM Seq () Source #
CheckableOp SOACS Source #
Instance details Defined in Futhark.IR.SOACS Methods checkOp :: OpWithAliases (Op SOACS) -> TypeM SOACS () Source #
CheckableOp MCMem Source #
Instance details Defined in Futhark.IR.MCMem Methods checkOp :: OpWithAliases (Op MCMem) -> TypeM MCMem () Source #
CheckableOp MC Source #
Instance details Defined in Futhark.IR.MC Methods checkOp :: OpWithAliases (Op MC) -> TypeM MC () Source #
CheckableOp SeqMem Source #
Instance details Defined in Futhark.IR.SeqMem Methods checkOp :: OpWithAliases (Op SeqMem) -> TypeM SeqMem () Source #
CheckableOp Kernels Source #
Instance details Defined in Futhark.IR.Kernels Methods checkOp :: OpWithAliases (Op Kernels) -> TypeM Kernels () Source #
CheckableOp KernelsMem Source #
Instance details Defined in Futhark.IR.KernelsMem Methods checkOp :: OpWithAliases (Op KernelsMem) -> TypeM KernelsMem () Source #

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

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

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

Checkers

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

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

Variant of require working on variable names.

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

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

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

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

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

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

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

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

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

argType :: Arg -> Type Source #

argAliases :: Arg -> Names Source #

Remove all aliases from the Arg.

noArgAliases :: Arg -> Arg Source #

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

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

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

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

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

Proclaim that we have written to the given variables.

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

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

alternative :: TypeM lore a -> TypeM lore b -> TypeM lore (a, b) Source #

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)