Language.Futhark.TypeChecker

The type checker checks whether the program is type-consistent and adds type annotations and various other elaborations. The program does not need to have any particular properties for the type checker to function; in particular it does not need unique names.

Documentation

checkProg :: Imports -> VNameSource -> ImportName -> UncheckedProg -> Either TypeError (FileModule, Warnings, VNameSource)

Type check a program containing no type information, yielding either a type error or a program with complete type information. Accepts a mapping from file names (excluding extension) to previously type checker results. The FilePath is used to resolve relative imports.

checkExp :: Imports -> VNameSource -> Env -> UncheckedExp -> Either TypeError ([TypeParam], Exp)

Type check a single expression containing no type information, yielding either a type error or the same expression annotated with type information. Also returns a list of type parameters, which will be nonempty if the expression is polymorphic. See also checkProg.

checkDec :: Imports -> VNameSource -> Env -> ImportName -> UncheckedDec -> Either TypeError (Env, Dec, VNameSource)

Type check a single declaration containing no type information, yielding either a type error or the same declaration annotated with type information along the Env produced by that declaration. See also checkProg.

checkModExp :: Imports -> VNameSource -> Env -> ModExpBase NoInfo Name -> Either TypeError (MTy, ModExpBase Info VName)

Type check a single module expression containing no type information, yielding either a type error or the same expression annotated with type information along the Env produced by that declaration. See also checkProg.

data TypeError

Information about an error during type checking.

Instances

Pretty TypeError

Defined in Language.Futhark.TypeChecker.Monad

Methods

ppr :: TypeError -> Doc

pprPrec :: Int -> TypeError -> Doc

pprList :: [TypeError] -> Doc

MonadError TypeError TypeM

Defined in Language.Futhark.TypeChecker.Monad

Methods

throwError :: TypeError -> TypeM a

catchError :: TypeM a -> (TypeError -> TypeM a) -> TypeM a

data Warnings

The warnings produced by the compiler. The Show instance produces a human-readable description.

Instances

Eq Warnings

Defined in Language.Futhark.Warnings

Methods

(==) :: Warnings -> Warnings -> Bool

(/=) :: Warnings -> Warnings -> Bool

Show Warnings

Defined in Language.Futhark.Warnings

Methods

showsPrec :: Int -> Warnings -> ShowS

show :: Warnings -> String

showList :: [Warnings] -> ShowS

Semigroup Warnings

Defined in Language.Futhark.Warnings

Methods

(<>) :: Warnings -> Warnings -> Warnings

sconcat :: NonEmpty Warnings -> Warnings

stimes :: Integral b => b -> Warnings -> Warnings

Monoid Warnings

Defined in Language.Futhark.Warnings

Methods

mempty :: Warnings

mappend :: Warnings -> Warnings -> Warnings

mconcat :: [Warnings] -> Warnings

MonadWriter Warnings TypeM

Defined in Language.Futhark.TypeChecker.Monad

Methods

writer :: (a, Warnings) -> TypeM a

tell :: Warnings -> TypeM ()

listen :: TypeM a -> TypeM (a, Warnings)

pass :: TypeM (a, Warnings -> Warnings) -> TypeM a

initialEnv :: Env

An initial environment for the type checker, containing intrinsics and such.