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 (<>) :: 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
MonadError TypeError TermTypeM Source #
Instance details Defined in Language.Futhark.TypeChecker.Terms.Monad Methods throwError :: TypeError -> TermTypeM a # catchError :: TermTypeM a -> (TypeError -> TermTypeM a) -> TermTypeM a
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 Methods get :: TermTypeM TermTypeState put :: TermTypeState -> TermTypeM () state :: (TermTypeState -> (a, TermTypeState)) -> TermTypeM a

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 show :: ValBinding -> String showList :: [ValBinding] -> ShowS

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 show :: SizeSource -> String showList :: [SizeSource] -> ShowS
Eq SizeSource Source #
Instance details Defined in Language.Futhark.TypeChecker.Terms.Monad Methods (==) :: SizeSource -> SizeSource -> Bool (/=) :: SizeSource -> SizeSource -> Bool
Ord SizeSource Source #
Instance details 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

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

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 # local :: (TermEnv -> TermEnv) -> TermTypeM a -> TermTypeM a # reader :: (TermEnv -> a) -> TermTypeM a #

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

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

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 #

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