futhark-0.25.32: An optimising compiler for a functional, array-oriented language.

Safe Haskell | None
Language | GHC2021

Language.Futhark.TypeChecker.Terms.Monad

Contents

- Primitive checking
- Sizes
- Control flow
- Errors

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

- data TermTypeM a
- runTermTypeM :: (ExpBase (NoInfo :: Type -> Type) VName -> TermTypeM Exp) -> TermTypeM a -> TypeM a
- data ValBinding
  - = BoundV [TypeParam] StructType
  - | OverloadedF [PrimType] [Maybe PrimType] (Maybe PrimType)
  - | EqualityF
- data SizeSource = SourceSlice (Maybe Size) (Maybe (ExpBase (NoInfo :: Type -> Type) VName)) (Maybe (ExpBase (NoInfo :: Type -> Type) VName)) (Maybe (ExpBase (NoInfo :: Type -> Type) VName))
- data Inferred t
  - = NoneInferred
  - | Ascribed t
- data Checking
  - = CheckingApply (Maybe (QualName VName)) Exp StructType StructType
  - | CheckingReturn ResType StructType
  - | CheckingAscription StructType StructType
  - | CheckingLetGeneralise Name
  - | CheckingParams (Maybe Name)
  - | CheckingPat (PatBase (NoInfo :: Type -> Type) VName StructType) (Inferred StructType)
  - | CheckingLoopBody StructType StructType
  - | CheckingLoopInitial StructType StructType
  - | CheckingRecordUpdate [Name] StructType StructType
  - | CheckingRequired [StructType] StructType
  - | CheckingBranches StructType StructType
- withEnv :: TermEnv -> Env -> TermEnv
- localScope :: (TermScope -> TermScope) -> TermTypeM a -> TermTypeM a
- data TermEnv = TermEnv {
  - termScope :: TermScope
  - termChecking :: Maybe Checking
  - termLevel :: Level
  - termChecker :: ExpBase (NoInfo :: Type -> Type) VName -> TermTypeM Exp
  - termOuterEnv :: Env
  - termImportName :: ImportName
  }
- data TermScope = TermScope {
  - scopeVtable :: Map VName ValBinding
  - scopeTypeTable :: Map VName TypeBinding
  - scopeModTable :: Map VName Mod
  }
- data TermTypeState = TermTypeState {
  - stateConstraints :: Constraints
  - stateCounter :: !Int
  - stateWarnings :: Warnings
  - stateNameSource :: VNameSource
  }
- onFailure :: Checking -> TermTypeM a -> TermTypeM a
- extSize :: SrcLoc -> SizeSource -> TermTypeM (Size, Maybe VName)
- expType :: Exp -> TermTypeM StructType
- expTypeFully :: Exp -> TermTypeM StructType
- constrain :: VName -> Constraint -> TermTypeM ()
- newArrayType :: Usage -> Name -> Int -> TermTypeM (StructType, StructType)
- allDimsFreshInType :: Usage -> Rigidity -> Name -> TypeBase Size als -> TermTypeM (TypeBase Size als, Map VName Size)
- updateTypes :: ASTMappable e => e -> TermTypeM e
- type Names = Set VName
- unifies :: Text -> StructType -> Exp -> TermTypeM Exp
- require :: Text -> [PrimType] -> Exp -> TermTypeM Exp
- checkTypeExpNonrigid :: TypeExp (ExpBase (NoInfo :: Type -> Type) VName) VName -> TermTypeM (TypeExp Exp VName, ResType, [VName])
- lookupVar :: SrcLoc -> QualName VName -> TermTypeM StructType
- lookupMod :: QualName VName -> TermTypeM Mod
- isInt64 :: Exp -> Maybe Int64
- incLevel :: TermTypeM a -> TermTypeM a
- unusedSize :: MonadTypeChecker m => SizeBinder VName -> m a

# Documentation

data TermTypeM a Source #

#### Instances

Instances details

MonadTypeChecker TermTypeM Source # |

Instance details

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

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

warnings :: Warnings -> TermTypeM () Source #

newName :: VName -> TermTypeM VName Source #

newID :: Name -> TermTypeM VName Source #

newTypeName :: Name -> TermTypeM VName Source #

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

lookupType :: QualName VName -> TermTypeM ([TypeParam], StructRetType, Liftedness) Source #

typeError :: Located loc => loc -> Notes -> Doc () -> TermTypeM a Source #

MonadUnify TermTypeM Source # |

Instance details

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

getConstraints :: TermTypeM Constraints Source #

putConstraints :: Constraints -> TermTypeM () Source #

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

newTypeVar :: (Monoid als, Located a) => a -> Name -> TermTypeM (TypeBase dim als) Source #

newDimVar :: Usage -> Rigidity -> Name -> TermTypeM VName Source #

newRigidDim :: Located a => a -> RigidSource -> Name -> TermTypeM VName Source #

newFlexibleDim :: Usage -> Name -> TermTypeM VName Source #

curLevel :: TermTypeM Level Source #

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

unifyError :: Located loc => loc -> Notes -> BreadCrumbs -> Doc () -> TermTypeM a Source #

Applicative TermTypeM Source # |
Instance details Defined in Language.Futhark.TypeChecker.Terms.Monad Methods pure :: a -> TermTypeM a Source # (<*>) :: TermTypeM (a -> b) -> TermTypeM a -> TermTypeM b Source # liftA2 :: (a -> b -> c) -> TermTypeM a -> TermTypeM b -> TermTypeM c Source # (*>) :: TermTypeM a -> TermTypeM b -> TermTypeM b Source # (<*) :: TermTypeM a -> TermTypeM b -> TermTypeM a Source #
Functor TermTypeM Source # |
Instance details Defined in Language.Futhark.TypeChecker.Terms.Monad Methods fmap :: (a -> b) -> TermTypeM a -> TermTypeM b Source # (<$) :: a -> TermTypeM b -> TermTypeM a Source #
Monad TermTypeM Source # |
Instance details Defined in Language.Futhark.TypeChecker.Terms.Monad Methods (>>=) :: TermTypeM a -> (a -> TermTypeM b) -> TermTypeM b Source # (>>) :: TermTypeM a -> TermTypeM b -> TermTypeM b Source # return :: a -> TermTypeM a Source #
MonadError TypeError TermTypeM Source # |
Instance details Defined in Language.Futhark.TypeChecker.Terms.Monad Methods throwError :: TypeError -> TermTypeM a Source # catchError :: TermTypeM a -> (TypeError -> TermTypeM a) -> TermTypeM a Source #
MonadReader TermEnv TermTypeM Source # |
Instance details Defined in Language.Futhark.TypeChecker.Terms.Monad Methods ask :: TermTypeM TermEnv Source # local :: (TermEnv -> TermEnv) -> TermTypeM a -> TermTypeM a Source # reader :: (TermEnv -> a) -> TermTypeM a Source #
MonadState TermTypeState TermTypeM Source # |
Instance details Defined in Language.Futhark.TypeChecker.Terms.Monad Methods get :: TermTypeM TermTypeState Source # put :: TermTypeState -> TermTypeM () Source # state :: (TermTypeState -> (a, TermTypeState)) -> TermTypeM a Source #

runTermTypeM :: (ExpBase (NoInfo :: Type -> Type) VName -> TermTypeM Exp) -> TermTypeM a -> TypeM a Source #

data ValBinding Source #

Constructors

BoundV [TypeParam] StructType |
OverloadedF [PrimType] [Maybe PrimType] (Maybe PrimType) |
EqualityF |

#### Instances

Instances details

Show ValBinding Source # |
Instance details Defined in Language.Futhark.TypeChecker.Terms.Monad Methods showsPrec :: Int -> ValBinding -> ShowS Source # show :: ValBinding -> String Source # showList :: [ValBinding] -> ShowS Source #

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.

Constructors

SourceSlice (Maybe Size) (Maybe (ExpBase (NoInfo :: Type -> Type) VName)) (Maybe (ExpBase (NoInfo :: Type -> Type) VName)) (Maybe (ExpBase (NoInfo :: Type -> Type) VName)) |

#### Instances

Instances details

Show SizeSource Source # |
Instance details Defined in Language.Futhark.TypeChecker.Terms.Monad Methods showsPrec :: Int -> SizeSource -> ShowS Source # show :: SizeSource -> String Source # showList :: [SizeSource] -> ShowS Source #
Eq SizeSource Source # |
Instance details Defined in Language.Futhark.TypeChecker.Terms.Monad Methods (==) :: SizeSource -> SizeSource -> Bool Source # (/=) :: SizeSource -> SizeSource -> Bool Source #
Ord SizeSource Source # |

Instance details

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

compare :: SizeSource -> SizeSource -> Ordering Source #

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

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

(>) :: SizeSource -> SizeSource -> Bool Source #

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

max :: SizeSource -> SizeSource -> SizeSource Source #

min :: SizeSource -> SizeSource -> SizeSource Source #

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 Source # (<$) :: a -> Inferred b -> Inferred a Source #

data Checking Source #

Constructors

CheckingApply (Maybe (QualName VName)) Exp StructType StructType |
CheckingReturn ResType StructType |
CheckingAscription StructType StructType |
CheckingLetGeneralise Name |
CheckingParams (Maybe Name) |
CheckingPat (PatBase (NoInfo :: Type -> Type) VName StructType) (Inferred StructType) |
CheckingLoopBody StructType StructType |
CheckingLoopInitial StructType StructType |
CheckingRecordUpdate [Name] StructType StructType |
CheckingRequired [StructType] StructType |
CheckingBranches StructType StructType |

#### Instances

Instances details

Pretty Checking Source # |
Instance details Defined in Language.Futhark.TypeChecker.Terms.Monad Methods pretty :: Checking -> Doc ann Source # prettyList :: [Checking] -> Doc ann Source #

withEnv :: TermEnv -> Env -> TermEnv Source #

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

data TermEnv Source #

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
- termChecker :: ExpBase (NoInfo :: Type -> Type) VName -> TermTypeM Exp
- termOuterEnv :: Env
- termImportName :: ImportName

#### Instances

Instances details

MonadReader TermEnv TermTypeM Source # |
Instance details Defined in Language.Futhark.TypeChecker.Terms.Monad Methods ask :: TermTypeM TermEnv Source # local :: (TermEnv -> TermEnv) -> TermTypeM a -> TermTypeM a Source # reader :: (TermEnv -> a) -> TermTypeM a Source #

data TermScope Source #

Constructors

TermScope |

Fields

- scopeVtable :: Map VName ValBinding
- scopeTypeTable :: Map VName TypeBinding
- scopeModTable :: Map VName Mod

#### Instances

Instances details

Semigroup TermScope Source # |
Instance details Defined in Language.Futhark.TypeChecker.Terms.Monad Methods (<>) :: TermScope -> TermScope -> TermScope Source # sconcat :: NonEmpty TermScope -> TermScope Source # stimes :: Integral b => b -> TermScope -> TermScope Source #
Show TermScope Source # |
Instance details Defined in Language.Futhark.TypeChecker.Terms.Monad Methods showsPrec :: Int -> TermScope -> ShowS Source # show :: TermScope -> String Source # showList :: [TermScope] -> ShowS Source #

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

- stateConstraints :: Constraints
- stateCounter :: !Int
- stateWarnings :: Warnings
- stateNameSource :: VNameSource

#### Instances

Instances details

MonadState TermTypeState TermTypeM Source # |
Instance details Defined in Language.Futhark.TypeChecker.Terms.Monad Methods get :: TermTypeM TermTypeState Source # put :: TermTypeState -> TermTypeM () Source # state :: (TermTypeState -> (a, TermTypeState)) -> TermTypeM a Source #

onFailure :: Checking -> TermTypeM a -> TermTypeM a Source #

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

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

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

newArrayType :: Usage -> Name -> Int -> TermTypeM (StructType, StructType) Source #

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.

type Names = Set VName Source #

# Primitive checking

unifies :: Text -> StructType -> Exp -> TermTypeM Exp Source #

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`.

checkTypeExpNonrigid :: TypeExp (ExpBase (NoInfo :: Type -> Type) VName) VName -> TermTypeM (TypeExp Exp VName, ResType, [VName]) Source #

lookupVar :: SrcLoc -> QualName VName -> TermTypeM StructType Source #

lookupMod :: QualName VName -> TermTypeM Mod Source #

# Sizes

isInt64 :: Exp -> Maybe Int64 Source #

# Control flow

incLevel :: TermTypeM a -> TermTypeM a Source #

# Errors

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