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)

checkNamedDim :: 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

MonadState TermTypeState TermTypeM

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

get :: TermTypeM TermTypeState

put :: TermTypeState -> TermTypeM ()

state :: (TermTypeState -> (a, TermTypeState)) -> 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

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

Whether something is a global or a local variable.

Constructors

Local

Global

Instances

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

SourceArg FName (ExpBase NoInfo VName)

SourceBound (ExpBase NoInfo VName)

SourceSlice (Maybe (DimDecl VName)) (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 (DimDecl VName, 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 (DimDecl VName) als -> TermTypeM (TypeBase (DimDecl VName) als, Map VName (DimDecl VName))

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 (DimDecl VName)

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

dimFromArg :: Maybe (QualName VName) -> Exp -> TermTypeM (DimDecl VName, 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

unexpectedType :: MonadTypeChecker m => SrcLoc -> StructType -> [StructType] -> m a

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