futhark-0.25.32: An optimising compiler for a functional, array-oriented language.

Safe Haskell | None
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 Shape 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 Source # show :: TypeError rep -> String Source # showList :: [TypeError rep] -> ShowS Source #

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 Shape 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 Source # show :: ErrorCase rep -> String Source # showList :: [ErrorCase rep] -> ShowS Source #

# 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 Source # (<*>) :: TypeM rep (a -> b) -> TypeM rep a -> TypeM rep b Source # liftA2 :: (a -> b -> c) -> TypeM rep a -> TypeM rep b -> TypeM rep c Source # (*>) :: TypeM rep a -> TypeM rep b -> TypeM rep b Source # (<*) :: TypeM rep a -> TypeM rep b -> TypeM rep a Source #
Functor (TypeM rep) Source # |
Instance details Defined in Futhark.IR.TypeCheck Methods fmap :: (a -> b) -> TypeM rep a -> TypeM rep b Source # (<$) :: a -> TypeM rep b -> TypeM rep a Source #
Monad (TypeM rep) Source # |
Instance details Defined in Futhark.IR.TypeCheck Methods (>>=) :: TypeM rep a -> (a -> TypeM rep b) -> TypeM rep b Source # (>>) :: TypeM rep a -> TypeM rep b -> TypeM rep b Source # return :: a -> TypeM rep a Source #
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.