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

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
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 #

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 #

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 #

MonadTypeChecker TermTypeM Source # 
Instance details

Defined in Language.Futhark.TypeChecker.Terms.Monad

MonadUnify TermTypeM Source # 
Instance details

Defined in Language.Futhark.TypeChecker.Terms.Monad

MonadState TermTypeState 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 #

MonadError TypeError TermTypeM Source # 
Instance details

Defined in Language.Futhark.TypeChecker.Terms.Monad

data ValBinding Source #

Constructors

BoundV Locality [TypeParam] PatType

Aliases in parameters indicate the lexical closure.

OverloadedF [PrimType] [Maybe PrimType] (Maybe PrimType) 
EqualityF 
WasConsumed SrcLoc 

Instances

Instances details
Show ValBinding Source # 
Instance details

Defined in Language.Futhark.TypeChecker.Terms.Monad

data Locality Source #

Whether something is a global or a local variable.

Constructors

Local 
Global 

Instances

Instances details
Show Locality 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 NameReason Source #

A description of where an artificial compiler-generated intermediate name came from.

Constructors

NameAppRes (Maybe (QualName VName)) SrcLoc

Name is the result of a function application.

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.

Constructors

TermTypeState 

Fields

expType :: Exp -> TermTypeM PatType 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 PatType 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 :: SrcLoc -> Rigidity -> Name -> TypeBase (DimDecl VName) als -> TermTypeM (TypeBase (DimDecl VName) als, Map VName (DimDecl VName)) 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 :: String -> [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

noSizeEscape :: TermTypeM a -> TermTypeM a Source #

Any argument sizes created with extSize inside the given action will be removed once the action finishes. This is to ensure that just because e.g. n+1 appears as a size in one branch of a conditional, that doesn't mean it's also available in the other branch.

Control flow

Consumption and uniqueness

data Occurrence Source #

The consumption set is a Maybe so we can distinguish whether a consumption took place, but the variable went out of scope since, or no consumption at all took place.

Constructors

Occurrence 

noUnique :: TermTypeM a -> TermTypeM a Source #

Enter a context where nothing outside can be consumed (i.e. the body of a function definition).

observe :: Ident -> TermTypeM () Source #

Proclaim that we have made read-only use of the given variable.

consume :: SrcLoc -> Aliasing -> TermTypeM () Source #

Proclaim that we have written to the given variable.

consuming :: Ident -> TermTypeM a -> TermTypeM a Source #

Proclaim that we have written to the given variable, and mark accesses to it and all of its aliases as invalid inside the given computation.

Errors

badLetWithValue :: (Pretty arr, Pretty src) => arr -> src -> SrcLoc -> TermTypeM a Source #