futhark-0.19.5: An optimising compiler for a functional, array-oriented language.
Safe HaskellTrustworthy
LanguageHaskell2010

Futhark.TypeCheck

Description

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

Synopsis

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.

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

Checkable SOACS Source # 
Instance details

Defined in Futhark.IR.SOACS

Checkable MCMem Source # 
Instance details

Defined in Futhark.IR.MCMem

Checkable MC Source # 
Instance details

Defined in Futhark.IR.MC

Checkable SeqMem Source # 
Instance details

Defined in Futhark.IR.SeqMem

Checkable Kernels Source # 
Instance details

Defined in Futhark.IR.Kernels

Checkable KernelsMem Source # 
Instance details

Defined in Futhark.IR.KernelsMem

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

CheckableOp SOACS Source # 
Instance details

Defined in Futhark.IR.SOACS

CheckableOp MCMem Source # 
Instance details

Defined in Futhark.IR.MCMem

CheckableOp MC Source # 
Instance details

Defined in Futhark.IR.MC

CheckableOp SeqMem Source # 
Instance details

Defined in Futhark.IR.SeqMem

CheckableOp Kernels Source # 
Instance details

Defined in Futhark.IR.Kernels

CheckableOp KernelsMem Source # 
Instance details

Defined in Futhark.IR.KernelsMem

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.

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 #

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 #