Safe Haskell	Safe-Inferred
Language	GHC2021

Futhark.IR.TypeCheck

Contents

Interface
Extensionality
Checkers

Description

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

Synopsis

checkProg :: Checkable rep => Prog (Aliases rep) -> Either (TypeError rep) ()
data TypeError rep = Error [Text] (ErrorCase rep)
data ErrorCase rep
- = 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)
data TypeM rep a
bad :: ErrorCase rep -> TypeM rep a
context :: Text -> TypeM rep a -> TypeM rep a
class (AliasableRep rep, TypedOp (OpC rep)) => Checkable rep where
- checkExpDec :: ExpDec rep -> TypeM rep ()
- checkBodyDec :: BodyDec rep -> TypeM rep ()
- checkFParamDec :: VName -> FParamInfo rep -> TypeM rep ()
- checkLParamDec :: VName -> LParamInfo rep -> TypeM rep ()
- checkLetBoundDec :: VName -> LetDec rep -> TypeM rep ()
- checkRetType :: [RetType rep] -> TypeM rep ()
- matchPat :: Pat (LetDec (Aliases rep)) -> Exp (Aliases rep) -> TypeM rep ()
- primFParam :: VName -> PrimType -> TypeM rep (FParam (Aliases rep))
- matchReturnType :: [RetType rep] -> Result -> TypeM rep ()
- matchBranchType :: [BranchType rep] -> Body (Aliases rep) -> TypeM rep ()
- matchLoopResult :: [FParam (Aliases rep)] -> Result -> TypeM rep ()
- checkOp :: Op (Aliases rep) -> TypeM rep ()
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
require :: Checkable rep => [Type] -> SubExp -> TypeM rep ()
requireI :: Checkable rep => [Type] -> VName -> TypeM rep ()
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 ()
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 ()
binding :: Checkable rep => Scope (Aliases rep) -> TypeM rep a -> TypeM rep a
alternative :: TypeM rep a -> TypeM rep b -> TypeM rep (a, b)

Interface

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

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

data TypeError rep Source #

A type error.

Constructors

Error [Text] (ErrorCase rep)

Instances

Instances details

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

data ErrorCase rep Source #

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

Instances details

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

Extensionality

data TypeM rep a Source #

The type checker runs in this monad.

Instances

Instances details

Applicative (TypeM rep) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details Defined in Futhark.IR.TypeCheck Methods lookupType :: VName -> TypeM rep Type Source # lookupInfo :: VName -> TypeM rep (NameInfo (Aliases rep)) Source # askScope :: TypeM rep (Scope (Aliases rep)) Source # asksScope :: (Scope (Aliases rep) -> a) -> TypeM rep a Source #

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

Signal a type error.

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

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

The class of representations that can be type-checked.

Minimal complete definition

checkOp

Methods

checkExpDec :: ExpDec rep -> TypeM rep () Source #

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

checkBodyDec :: BodyDec rep -> TypeM rep () Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Instances

Instances details

Checkable GPU Source #
Instance details Defined in Futhark.IR.GPU Methods checkExpDec :: ExpDec GPU -> TypeM GPU () Source # checkBodyDec :: BodyDec GPU -> TypeM GPU () Source # checkFParamDec :: VName -> FParamInfo GPU -> TypeM GPU () Source # checkLParamDec :: VName -> LParamInfo GPU -> TypeM GPU () Source # checkLetBoundDec :: VName -> LetDec GPU -> TypeM GPU () Source # checkRetType :: [RetType GPU] -> TypeM GPU () Source # matchPat :: Pat (LetDec (Aliases GPU)) -> Exp (Aliases GPU) -> TypeM GPU () Source # primFParam :: VName -> PrimType -> TypeM GPU (FParam (Aliases GPU)) Source # matchReturnType :: [RetType GPU] -> Result -> TypeM GPU () Source # matchBranchType :: [BranchType GPU] -> Body (Aliases GPU) -> TypeM GPU () Source # matchLoopResult :: [FParam (Aliases GPU)] -> Result -> TypeM GPU () Source # checkOp :: Op (Aliases GPU) -> TypeM GPU () Source #
Checkable GPUMem Source #
Instance details Defined in Futhark.IR.GPUMem Methods checkExpDec :: ExpDec GPUMem -> TypeM GPUMem () Source # checkBodyDec :: BodyDec GPUMem -> TypeM GPUMem () Source # checkFParamDec :: VName -> FParamInfo GPUMem -> TypeM GPUMem () Source # checkLParamDec :: VName -> LParamInfo GPUMem -> TypeM GPUMem () Source # checkLetBoundDec :: VName -> LetDec GPUMem -> TypeM GPUMem () Source # checkRetType :: [RetType GPUMem] -> TypeM GPUMem () Source # matchPat :: Pat (LetDec (Aliases GPUMem)) -> Exp (Aliases GPUMem) -> TypeM GPUMem () Source # primFParam :: VName -> PrimType -> TypeM GPUMem (FParam (Aliases GPUMem)) Source # matchReturnType :: [RetType GPUMem] -> Result -> TypeM GPUMem () Source # matchBranchType :: [BranchType GPUMem] -> Body (Aliases GPUMem) -> TypeM GPUMem () Source # matchLoopResult :: [FParam (Aliases GPUMem)] -> Result -> TypeM GPUMem () Source # checkOp :: Op (Aliases GPUMem) -> TypeM GPUMem () Source #
Checkable MC Source #
Instance details Defined in Futhark.IR.MC Methods checkExpDec :: ExpDec MC -> TypeM MC () Source # checkBodyDec :: BodyDec MC -> TypeM MC () Source # checkFParamDec :: VName -> FParamInfo MC -> TypeM MC () Source # checkLParamDec :: VName -> LParamInfo MC -> TypeM MC () Source # checkLetBoundDec :: VName -> LetDec MC -> TypeM MC () Source # checkRetType :: [RetType MC] -> TypeM MC () Source # matchPat :: Pat (LetDec (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)] -> Result -> TypeM MC () Source # checkOp :: Op (Aliases MC) -> TypeM MC () Source #
Checkable MCMem Source #
Instance details Defined in Futhark.IR.MCMem Methods checkExpDec :: ExpDec MCMem -> TypeM MCMem () Source # checkBodyDec :: BodyDec MCMem -> TypeM MCMem () Source # checkFParamDec :: VName -> FParamInfo MCMem -> TypeM MCMem () Source # checkLParamDec :: VName -> LParamInfo MCMem -> TypeM MCMem () Source # checkLetBoundDec :: VName -> LetDec MCMem -> TypeM MCMem () Source # checkRetType :: [RetType MCMem] -> TypeM MCMem () Source # matchPat :: Pat (LetDec (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)] -> Result -> TypeM MCMem () Source # checkOp :: Op (Aliases MCMem) -> TypeM MCMem () Source #
Checkable SOACS Source #
Instance details Defined in Futhark.IR.SOACS Methods checkExpDec :: ExpDec SOACS -> TypeM SOACS () Source # checkBodyDec :: BodyDec SOACS -> TypeM SOACS () Source # checkFParamDec :: VName -> FParamInfo SOACS -> TypeM SOACS () Source # checkLParamDec :: VName -> LParamInfo SOACS -> TypeM SOACS () Source # checkLetBoundDec :: VName -> LetDec SOACS -> TypeM SOACS () Source # checkRetType :: [RetType SOACS] -> TypeM SOACS () Source # matchPat :: Pat (LetDec (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)] -> Result -> TypeM SOACS () Source # checkOp :: Op (Aliases SOACS) -> TypeM SOACS () Source #
Checkable Seq Source #
Instance details Defined in Futhark.IR.Seq Methods checkExpDec :: ExpDec Seq -> TypeM Seq () Source # checkBodyDec :: BodyDec Seq -> TypeM Seq () Source # checkFParamDec :: VName -> FParamInfo Seq -> TypeM Seq () Source # checkLParamDec :: VName -> LParamInfo Seq -> TypeM Seq () Source # checkLetBoundDec :: VName -> LetDec Seq -> TypeM Seq () Source # checkRetType :: [RetType Seq] -> TypeM Seq () Source # matchPat :: Pat (LetDec (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)] -> Result -> TypeM Seq () Source # checkOp :: Op (Aliases Seq) -> TypeM Seq () Source #
Checkable SeqMem Source #
Instance details Defined in Futhark.IR.SeqMem Methods checkExpDec :: ExpDec SeqMem -> TypeM SeqMem () Source # checkBodyDec :: BodyDec SeqMem -> TypeM SeqMem () Source # checkFParamDec :: VName -> FParamInfo SeqMem -> TypeM SeqMem () Source # checkLParamDec :: VName -> LParamInfo SeqMem -> TypeM SeqMem () Source # checkLetBoundDec :: VName -> LetDec SeqMem -> TypeM SeqMem () Source # checkRetType :: [RetType SeqMem] -> TypeM SeqMem () Source # matchPat :: Pat (LetDec (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)] -> Result -> TypeM SeqMem () Source # checkOp :: Op (Aliases SeqMem) -> TypeM SeqMem () Source #

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

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

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

Checkers

require :: Checkable rep => [Type] -> SubExp -> TypeM rep () 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 rep => [Type] -> VName -> TypeM rep () Source #

Variant of require working on variable names.

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

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

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

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

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

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

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

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

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

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

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

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

argType :: Arg -> Type Source #

noArgAliases :: Arg -> Arg Source #

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

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

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

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

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

Proclaim that we have written to the given variables.

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

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

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.