Safe Haskell	None
Language	Haskell2010

Futhark.TypeCheck

Contents

Interface
Extensionality
Checkers

Description

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

Synopsis

checkProg :: Checkable lore => Prog 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 (Attributes lore, CanBeAliased (Op lore), CheckableOp lore) => Checkable lore where
- checkExpLore :: ExpAttr lore -> TypeM lore ()
- checkBodyLore :: BodyAttr lore -> TypeM lore ()
- checkFParamLore :: VName -> FParamAttr lore -> TypeM lore ()
- checkLParamLore :: VName -> LParamAttr lore -> TypeM lore ()
- checkLetBoundLore :: VName -> LetAttr 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 ()
class Attributes lore => CheckableOp lore where
- checkOp :: OpWithAliases (Op lore) -> TypeM lore ()
lookupVar :: VName -> TypeM lore (NameInfo (Aliases lore))
lookupAliases :: Checkable lore => VName -> TypeM lore Names
type Occurences = [Occurence]
type UsageMap = Map VName [Usage]
usageMap :: Occurences -> UsageMap
collectOccurences :: TypeM lore a -> TypeM lore (a, Occurences)
subCheck :: forall lore newlore a. (Checkable newlore, RetType lore ~ RetType newlore, LetAttr lore ~ LetAttr newlore, FParamAttr lore ~ FParamAttr newlore, LParamAttr lore ~ LParamAttr newlore) => TypeM newlore 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 ()
matchExtReturnType :: Checkable lore => [ExtType] -> Result -> 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 ()
checkFun' :: Checkable lore => (Name, [DeclExtType], [(VName, NameInfo (Aliases lore))], BodyT (Aliases lore)) -> [(VName, Names)] -> TypeM lore () -> TypeM lore ()
checkLambdaParams :: Checkable lore => [LParam lore] -> TypeM lore ()
checkBody :: Checkable lore => Body (Aliases lore) -> TypeM lore ()
checkLambdaBody :: Checkable lore => [Type] -> Body (Aliases lore) -> TypeM lore ()
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

Interface

checkProg :: Checkable lore => Prog 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

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

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

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 # fail :: String -> 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 (Attributes 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 :: ExpAttr lore -> TypeM lore () Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Instances

Checkable SOACS Source #
Instance details Defined in Futhark.Representation.SOACS Methods checkExpLore :: ExpAttr SOACS -> TypeM SOACS () Source # checkBodyLore :: BodyAttr SOACS -> TypeM SOACS () Source # checkFParamLore :: VName -> FParamAttr SOACS -> TypeM SOACS () Source # checkLParamLore :: VName -> LParamAttr SOACS -> TypeM SOACS () Source # checkLetBoundLore :: VName -> LetAttr 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 #
Checkable InKernel Source #
Instance details Defined in Futhark.Representation.Kernels Methods checkExpLore :: ExpAttr InKernel -> TypeM InKernel () Source # checkBodyLore :: BodyAttr InKernel -> TypeM InKernel () Source # checkFParamLore :: VName -> FParamAttr InKernel -> TypeM InKernel () Source # checkLParamLore :: VName -> LParamAttr InKernel -> TypeM InKernel () Source # checkLetBoundLore :: VName -> LetAttr InKernel -> TypeM InKernel () Source # checkRetType :: [RetType InKernel] -> TypeM InKernel () Source # matchPattern :: Pattern (Aliases InKernel) -> Exp (Aliases InKernel) -> TypeM InKernel () Source # primFParam :: VName -> PrimType -> TypeM InKernel (FParam (Aliases InKernel)) Source # matchReturnType :: [RetType InKernel] -> Result -> TypeM InKernel () Source # matchBranchType :: [BranchType InKernel] -> Body (Aliases InKernel) -> TypeM InKernel () Source #
Checkable Kernels Source #
Instance details Defined in Futhark.Representation.Kernels Methods checkExpLore :: ExpAttr Kernels -> TypeM Kernels () Source # checkBodyLore :: BodyAttr Kernels -> TypeM Kernels () Source # checkFParamLore :: VName -> FParamAttr Kernels -> TypeM Kernels () Source # checkLParamLore :: VName -> LParamAttr Kernels -> TypeM Kernels () Source # checkLetBoundLore :: VName -> LetAttr 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 #
Checkable InKernel Source #
Instance details Defined in Futhark.Representation.ExplicitMemory Methods checkExpLore :: ExpAttr InKernel -> TypeM InKernel () Source # checkBodyLore :: BodyAttr InKernel -> TypeM InKernel () Source # checkFParamLore :: VName -> FParamAttr InKernel -> TypeM InKernel () Source # checkLParamLore :: VName -> LParamAttr InKernel -> TypeM InKernel () Source # checkLetBoundLore :: VName -> LetAttr InKernel -> TypeM InKernel () Source # checkRetType :: [RetType InKernel] -> TypeM InKernel () Source # matchPattern :: Pattern (Aliases InKernel) -> Exp (Aliases InKernel) -> TypeM InKernel () Source # primFParam :: VName -> PrimType -> TypeM InKernel (FParam (Aliases InKernel)) Source # matchReturnType :: [RetType InKernel] -> Result -> TypeM InKernel () Source # matchBranchType :: [BranchType InKernel] -> Body (Aliases InKernel) -> TypeM InKernel () Source #
Checkable ExplicitMemory Source #
Instance details Defined in Futhark.Representation.ExplicitMemory Methods checkExpLore :: ExpAttr ExplicitMemory -> TypeM ExplicitMemory () Source # checkBodyLore :: BodyAttr ExplicitMemory -> TypeM ExplicitMemory () Source # checkFParamLore :: VName -> FParamAttr ExplicitMemory -> TypeM ExplicitMemory () Source # checkLParamLore :: VName -> LParamAttr ExplicitMemory -> TypeM ExplicitMemory () Source # checkLetBoundLore :: VName -> LetAttr ExplicitMemory -> TypeM ExplicitMemory () Source # checkRetType :: [RetType ExplicitMemory] -> TypeM ExplicitMemory () Source # matchPattern :: Pattern (Aliases ExplicitMemory) -> Exp (Aliases ExplicitMemory) -> TypeM ExplicitMemory () Source # primFParam :: VName -> PrimType -> TypeM ExplicitMemory (FParam (Aliases ExplicitMemory)) Source # matchReturnType :: [RetType ExplicitMemory] -> Result -> TypeM ExplicitMemory () Source # matchBranchType :: [BranchType ExplicitMemory] -> Body (Aliases ExplicitMemory) -> TypeM ExplicitMemory () Source #

class Attributes lore => CheckableOp lore where Source #

Methods

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

Instances

CheckableOp SOACS Source #
Instance details Defined in Futhark.Representation.SOACS Methods checkOp :: OpWithAliases (Op SOACS) -> TypeM SOACS () Source #
CheckableOp InKernel Source #
Instance details Defined in Futhark.Representation.Kernels Methods checkOp :: OpWithAliases (Op InKernel) -> TypeM InKernel () Source #
CheckableOp Kernels Source #
Instance details Defined in Futhark.Representation.Kernels Methods checkOp :: OpWithAliases (Op Kernels) -> TypeM Kernels () Source #
CheckableOp InKernel Source #
Instance details Defined in Futhark.Representation.ExplicitMemory Methods checkOp :: OpWithAliases (Op InKernel) -> TypeM InKernel () Source #
CheckableOp ExplicitMemory Source #
Instance details Defined in Futhark.Representation.ExplicitMemory Methods checkOp :: OpWithAliases (Op ExplicitMemory) -> TypeM ExplicitMemory () Source #

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

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

type Occurences = [Occurence] Source #

type UsageMap = Map VName [Usage] Source #

usageMap :: Occurences -> UsageMap Source #

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

subCheck :: forall lore newlore a. (Checkable newlore, RetType lore ~ RetType newlore, LetAttr lore ~ LetAttr newlore, FParamAttr lore ~ FParamAttr newlore, LParamAttr lore ~ LParamAttr newlore) => TypeM newlore 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 #

matchExtReturnType :: Checkable lore => [ExtType] -> Result -> 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 #

checkFun' :: Checkable lore => (Name, [DeclExtType], [(VName, NameInfo (Aliases lore))], BodyT (Aliases lore)) -> [(VName, Names)] -> TypeM lore () -> TypeM lore () Source #

checkLambdaParams :: Checkable lore => [LParam lore] -> TypeM lore () Source #

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

checkLambdaBody :: Checkable lore => [Type] -> Body (Aliases lore) -> TypeM lore () 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 #

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)