futhark-0.25.19: An optimising compiler for a functional, array-oriented language.
Safe HaskellSafe-Inferred
LanguageGHC2021

Language.Futhark.TypeChecker.Terms.Monad

Description

Facilities for type-checking terms. Factored out of Language.Futhark.TypeChecker.Terms to prevent the module from being gigantic.

Incidentally also a nice place to put Haddock comments to make the internal API of the type checker easier to browse.

Synopsis

Documentation

data TermTypeM a Source #

Instances

Instances details
Applicative TermTypeM Source # 
Instance details

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

pure :: a -> TermTypeM a #

(<*>) :: TermTypeM (a -> b) -> TermTypeM a -> TermTypeM b #

liftA2 :: (a -> b -> c) -> TermTypeM a -> TermTypeM b -> TermTypeM c #

(*>) :: TermTypeM a -> TermTypeM b -> TermTypeM b #

(<*) :: TermTypeM a -> TermTypeM b -> TermTypeM a #

Functor TermTypeM Source # 
Instance details

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

fmap :: (a -> b) -> TermTypeM a -> TermTypeM b #

(<$) :: a -> TermTypeM b -> TermTypeM a #

Monad TermTypeM Source # 
Instance details

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

(>>=) :: TermTypeM a -> (a -> TermTypeM b) -> TermTypeM b #

(>>) :: TermTypeM a -> TermTypeM b -> TermTypeM b #

return :: a -> TermTypeM a #

MonadTypeChecker TermTypeM Source # 
Instance details

Defined in Language.Futhark.TypeChecker.Terms.Monad

MonadUnify TermTypeM Source # 
Instance details

Defined in Language.Futhark.TypeChecker.Terms.Monad

MonadError TypeError TermTypeM Source # 
Instance details

Defined in Language.Futhark.TypeChecker.Terms.Monad

MonadReader TermEnv TermTypeM Source # 
Instance details

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

ask :: TermTypeM TermEnv #

local :: (TermEnv -> TermEnv) -> TermTypeM a -> TermTypeM a #

reader :: (TermEnv -> a) -> TermTypeM a #

MonadState TermTypeState TermTypeM Source # 
Instance details

Defined in Language.Futhark.TypeChecker.Terms.Monad

data SizeSource Source #

What was the source of some existential size? This is used for using the same existential variable if the same source is encountered in multiple locations.

data Inferred t Source #

Constructors

NoneInferred 
Ascribed t 

Instances

Instances details
Functor Inferred Source # 
Instance details

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

fmap :: (a -> b) -> Inferred a -> Inferred b #

(<$) :: a -> Inferred b -> Inferred a #

data TermEnv Source #

Type checking happens with access to this environment. The TermScope will be extended during type-checking as bindings come into scope.

Instances

Instances details
MonadReader TermEnv TermTypeM Source # 
Instance details

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

ask :: TermTypeM TermEnv #

local :: (TermEnv -> TermEnv) -> TermTypeM a -> TermTypeM a #

reader :: (TermEnv -> a) -> TermTypeM a #

data TermTypeState Source #

The state is a set of constraints and a counter for generating type names. This is distinct from the usual counter we use for generating unique names, as these will be user-visible.

expType :: Exp -> TermTypeM StructType Source #

Get the type of an expression, with top level type variables substituted. Never call typeOf directly (except in a few carefully inspected locations)!

expTypeFully :: Exp -> TermTypeM StructType Source #

Get the type of an expression, with all type variables substituted. Slower than expType, but sometimes necessary. Never call typeOf directly (except in a few carefully inspected locations)!

allDimsFreshInType :: Usage -> Rigidity -> Name -> TypeBase Size als -> TermTypeM (TypeBase Size als, Map VName Size) Source #

Replace *all* dimensions with distinct fresh size variables.

updateTypes :: ASTMappable e => e -> TermTypeM e Source #

Replace all type variables with their concrete types.

Primitive checking

require :: Text -> [PrimType] -> Exp -> TermTypeM Exp Source #

require ts e causes a TypeError if expType e is not one of the types in ts. Otherwise, simply returns e.

Sizes

Control flow

Errors