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 -> (Warnings, Either TypeError (FileModule, 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 checked results. The ImportName is used to resolve relative imports.

checkExp :: Imports -> VNameSource -> Env -> UncheckedExp -> (Warnings, 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 -> (Warnings, 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 -> (Warnings, 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 Notes

A collection of extra information regarding a type error.

Instances

Monoid Notes

Defined in Language.Futhark.TypeChecker.Monad

Methods

mempty :: Notes

mappend :: Notes -> Notes -> Notes

mconcat :: [Notes] -> Notes

Semigroup Notes

Defined in Language.Futhark.TypeChecker.Monad

Methods

(<>) :: Notes -> Notes -> Notes

sconcat :: NonEmpty Notes -> Notes

stimes :: Integral b => b -> Notes -> Notes

Pretty Notes

Defined in Language.Futhark.TypeChecker.Monad

Methods

pretty :: Notes -> Doc ann

prettyList :: [Notes] -> Doc ann

data TypeError

Information about an error during type checking.

Constructors

TypeError Loc Notes (Doc ())

Instances

MonadError TypeError TypeM

Defined in Language.Futhark.TypeChecker.Monad

Methods

throwError :: TypeError -> TypeM a

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

MonadError TypeError TermTypeM

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

throwError :: TypeError -> TermTypeM a

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

prettyTypeError :: TypeError -> Doc AnsiStyle

Prettyprint type error.

prettyTypeErrorNoLoc :: TypeError -> Doc AnsiStyle

Prettyprint type error, without location information. This can be used for cases where the location is printed in some other way.

data Warnings

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

Instances

Monoid Warnings

Defined in Language.Futhark.Warnings

Methods

mempty :: Warnings

mappend :: Warnings -> Warnings -> Warnings

mconcat :: [Warnings] -> Warnings

Semigroup Warnings

Defined in Language.Futhark.Warnings

Methods

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

sconcat :: NonEmpty Warnings -> Warnings

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

initialEnv :: Env

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

envWithImports :: Imports -> Env -> Env

Produce an environment, based on the one passed in, where all of the provided imports have been openened in order. This could in principle also be done with checkDec, but this is more precise.