Language.Futhark.TypeChecker.Terms.Monad

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.

Documentation

data TermTypeM a

Instances

Monad TermTypeM

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

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

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

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

Applicative TermTypeM

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

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

warn :: Located loc => loc -> Doc -> TermTypeM ()

newName :: VName -> TermTypeM VName

newID :: Name -> TermTypeM VName

newTypeName :: Name -> TermTypeM VName

bindNameMap :: NameMap -> TermTypeM a -> TermTypeM a

bindVal :: VName -> BoundV -> TermTypeM a -> TermTypeM a

checkQualName :: Namespace -> QualName Name -> SrcLoc -> TermTypeM (QualName VName)

lookupType :: SrcLoc -> QualName Name -> TermTypeM (QualName VName, [TypeParam], StructRetType, Liftedness)

lookupMod :: SrcLoc -> QualName Name -> TermTypeM (QualName VName, Mod)

lookupVar :: SrcLoc -> QualName Name -> TermTypeM (QualName VName, PatType)

checkNamedSize :: SrcLoc -> QualName Name -> TermTypeM (QualName VName)

typeError :: Located loc => loc -> Notes -> Doc -> TermTypeM a

MonadUnify TermTypeM

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

getConstraints :: TermTypeM Constraints

putConstraints :: Constraints -> TermTypeM ()

modifyConstraints :: (Constraints -> Constraints) -> TermTypeM ()

newTypeVar :: Monoid als => SrcLoc -> Name -> TermTypeM (TypeBase dim als)

newDimVar :: SrcLoc -> Rigidity -> Name -> TermTypeM VName

curLevel :: TermTypeM Level

matchError :: Located loc => loc -> Notes -> BreadCrumbs -> StructType -> StructType -> TermTypeM a

unifyError :: Located loc => loc -> Notes -> BreadCrumbs -> Doc -> TermTypeM a

MonadReader TermEnv TermTypeM

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

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

get :: TermTypeM TermTypeState

put :: TermTypeState -> TermTypeM ()

state :: (TermTypeState -> (a, TermTypeState)) -> TermTypeM a

MonadError TypeError TermTypeM

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

throwError :: TypeError -> TermTypeM a

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

runTermTypeM :: TermTypeM a -> TypeM (a, Occurrences)

liftTypeM :: TypeM a -> TermTypeM a

data ValBinding

Constructors

BoundV Locality [TypeParam] PatType

Aliases in parameters indicate the lexical closure.

OverloadedF [PrimType] [Maybe PrimType] (Maybe PrimType)

EqualityF

WasConsumed SrcLoc

Instances

Show ValBinding

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

showsPrec :: Int -> ValBinding -> ShowS

show :: ValBinding -> String

showList :: [ValBinding] -> ShowS

data Locality

How something was bound.

Constructors

Local

In the current function

Nonlocal

In an enclosing function, but not the current one.

Global

At global scope.

Instances

Eq Locality

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

(==) :: Locality -> Locality -> Bool

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

Ord Locality

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

compare :: Locality -> Locality -> Ordering

(<) :: Locality -> Locality -> Bool

(<=) :: Locality -> Locality -> Bool

(>) :: Locality -> Locality -> Bool

(>=) :: Locality -> Locality -> Bool

max :: Locality -> Locality -> Locality

min :: Locality -> Locality -> Locality

Show Locality

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

showsPrec :: Int -> Locality -> ShowS

show :: Locality -> String

showList :: [Locality] -> ShowS

data SizeSource

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.

Constructors

SourceBound (ExpBase NoInfo VName)

SourceSlice (Maybe Size) (Maybe (ExpBase NoInfo VName)) (Maybe (ExpBase NoInfo VName)) (Maybe (ExpBase NoInfo VName))

Instances

Eq SizeSource

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

(==) :: SizeSource -> SizeSource -> Bool

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

Ord SizeSource

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

compare :: SizeSource -> SizeSource -> Ordering

(<) :: SizeSource -> SizeSource -> Bool

(<=) :: SizeSource -> SizeSource -> Bool

(>) :: SizeSource -> SizeSource -> Bool

(>=) :: SizeSource -> SizeSource -> Bool

max :: SizeSource -> SizeSource -> SizeSource

min :: SizeSource -> SizeSource -> SizeSource

Show SizeSource

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

showsPrec :: Int -> SizeSource -> ShowS

show :: SizeSource -> String

showList :: [SizeSource] -> ShowS

data NameReason

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 InferredType

Constructors

NoneInferred

Ascribed PatType

data Checking

Constructors

CheckingApply (Maybe (QualName VName)) Exp StructType StructType

CheckingReturn StructType StructType

CheckingAscription StructType StructType

CheckingLetGeneralise Name

CheckingParams (Maybe Name)

CheckingPat UncheckedPat InferredType

CheckingLoopBody StructType StructType

CheckingLoopInitial StructType StructType

CheckingRecordUpdate [Name] StructType StructType

CheckingRequired [StructType] StructType

CheckingBranches StructType StructType

Instances

Pretty Checking

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

ppr :: Checking -> Doc

pprPrec :: Int -> Checking -> Doc

pprList :: [Checking] -> Doc

withEnv :: TermEnv -> Env -> TermEnv

localScope :: (TermScope -> TermScope) -> TermTypeM a -> TermTypeM a

data TermEnv

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

Constructors

TermEnv

Fields

• termScope :: TermScope
• termChecking :: Maybe Checking
• termLevel :: Level

Instances

MonadReader TermEnv TermTypeM

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

ask :: TermTypeM TermEnv

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

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

data TermScope

Constructors

TermScope

Fields

• scopeVtable :: Map VName ValBinding
• scopeTypeTable :: Map VName TypeBinding
• scopeModTable :: Map VName Mod
• scopeNameMap :: NameMap

Instances

Show TermScope

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

showsPrec :: Int -> TermScope -> ShowS

show :: TermScope -> String

showList :: [TermScope] -> ShowS

Semigroup TermScope

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

(<>) :: TermScope -> TermScope -> TermScope

sconcat :: NonEmpty TermScope -> TermScope

stimes :: Integral b => b -> TermScope -> TermScope

data TermTypeState

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

• stateConstraints :: Constraints
• stateCounter :: !Int
• stateDimTable :: Map SizeSource VName

  Mapping function arguments encountered to the sizes they ended up generating (when they could not be substituted directly). This happens for function arguments that are not constants or names.

• stateNames :: Map VName NameReason
• stateOccs :: Occurrences

Instances

MonadState TermTypeState TermTypeM

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

get :: TermTypeM TermTypeState

put :: TermTypeState -> TermTypeM ()

state :: (TermTypeState -> (a, TermTypeState)) -> TermTypeM a

onFailure :: Checking -> TermTypeM a -> TermTypeM a

extSize :: SrcLoc -> SizeSource -> TermTypeM (Size, Maybe VName)

expType :: Exp -> TermTypeM PatType

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

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)!

constrain :: VName -> Constraint -> TermTypeM ()

newArrayType :: SrcLoc -> Name -> Int -> TermTypeM (StructType, StructType)

allDimsFreshInType :: SrcLoc -> Rigidity -> Name -> TypeBase Size als -> TermTypeM (TypeBase Size als, Map VName Size)

Replace *all* dimensions with distinct fresh size variables.

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

Replace all type variables with their concrete types.

Primitive checking

unifies :: String -> StructType -> Exp -> TermTypeM Exp

require :: String -> [PrimType] -> Exp -> TermTypeM Exp

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

checkTypeExpNonrigid :: TypeExp Name -> TermTypeM (TypeExp VName, StructType, [VName])

checkTypeExpRigid :: TypeExp Name -> RigidSource -> TermTypeM (TypeExp VName, StructType, [VName])

Sizes

isInt64 :: Exp -> Maybe Int64

maybeDimFromExp :: Exp -> Maybe Size

dimFromExp :: (Exp -> SizeSource) -> Exp -> TermTypeM (Size, Maybe VName)

sizeFromArg :: Maybe (QualName VName) -> Exp -> TermTypeM (Size, Maybe VName)

noSizeEscape :: TermTypeM a -> TermTypeM a

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

collectOccurrences :: TermTypeM a -> TermTypeM (a, Occurrences)

tapOccurrences :: TermTypeM a -> TermTypeM (a, Occurrences)

alternative :: TermTypeM a -> TermTypeM b -> TermTypeM (a, b)

sequentially :: TermTypeM a -> (a -> Occurrences -> TermTypeM b) -> TermTypeM b

incLevel :: TermTypeM a -> TermTypeM a

Consumption and uniqueness

type Names = Set VName

data Occurrence

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

Fields

• observed :: Names
• consumed :: Maybe Names
• location :: SrcLoc

Instances

Eq Occurrence

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

(==) :: Occurrence -> Occurrence -> Bool

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

Show Occurrence

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

showsPrec :: Int -> Occurrence -> ShowS

show :: Occurrence -> String

showList :: [Occurrence] -> ShowS

Located Occurrence

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

locOf :: Occurrence -> Loc

locOfList :: [Occurrence] -> Loc

type Occurrences = [Occurrence]

onlySelfAliasing :: TermTypeM a -> TermTypeM a

noUnique :: TermTypeM a -> TermTypeM a

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

removeSeminullOccurrences :: TermTypeM a -> TermTypeM a

occur :: Occurrences -> TermTypeM ()

observe :: Ident -> TermTypeM ()

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

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

Proclaim that we have written to the given variable.

consuming :: Ident -> TermTypeM a -> TermTypeM a

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.

observation :: Aliasing -> SrcLoc -> Occurrence

consumption :: Aliasing -> SrcLoc -> Occurrence

checkIfConsumable :: SrcLoc -> Aliasing -> TermTypeM ()

seqOccurrences :: Occurrences -> Occurrences -> Occurrences

checkOccurrences :: Occurrences -> TermTypeM ()

allConsumed :: Occurrences -> Names

Errors

useAfterConsume :: VName -> SrcLoc -> SrcLoc -> TermTypeM a

unusedSize :: MonadTypeChecker m => SizeBinder VName -> m a

notConsumable :: MonadTypeChecker m => SrcLoc -> Doc -> m b

uniqueReturnAliased :: SrcLoc -> TermTypeM a

returnAliased :: Name -> SrcLoc -> TermTypeM ()

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

anyConsumption :: Occurrences -> Maybe Occurrence

allOccurring :: Occurrences -> Names