Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
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 :: (UncheckedExp -> TermTypeM Exp) -> TermTypeM a -> TypeM a
- data ValBinding
- = BoundV [TypeParam] StructType
- | OverloadedF [PrimType] [Maybe PrimType] (Maybe PrimType)
- | EqualityF
- data SizeSource
- 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 (UncheckedPat 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 {}
- data TermScope = TermScope {}
- data TermTypeState = TermTypeState {}
- 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 NoInfo Name -> TermTypeM (TypeExp Info VName, ResType, [VName])
- isInt64 :: Exp -> Maybe Int64
- incLevel :: TermTypeM a -> TermTypeM a
- unusedSize :: MonadTypeChecker m => SizeBinder VName -> m a
Documentation
Instances
runTermTypeM :: (UncheckedExp -> TermTypeM Exp) -> TermTypeM a -> TypeM a Source #
data ValBinding Source #
Instances
Show ValBinding Source # | |
Defined in Language.Futhark.TypeChecker.Terms.Monad 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.
SourceBound (ExpBase NoInfo VName) | |
SourceSlice (Maybe Size) (Maybe (ExpBase NoInfo VName)) (Maybe (ExpBase NoInfo VName)) (Maybe (ExpBase NoInfo VName)) |
Instances
Show SizeSource Source # | |
Defined in Language.Futhark.TypeChecker.Terms.Monad showsPrec :: Int -> SizeSource -> ShowS # show :: SizeSource -> String # showList :: [SizeSource] -> ShowS # | |
Eq SizeSource Source # | |
Defined in Language.Futhark.TypeChecker.Terms.Monad (==) :: SizeSource -> SizeSource -> Bool # (/=) :: SizeSource -> SizeSource -> Bool # | |
Ord SizeSource Source # | |
Defined in Language.Futhark.TypeChecker.Terms.Monad compare :: SizeSource -> SizeSource -> Ordering # (<) :: SizeSource -> SizeSource -> Bool # (<=) :: SizeSource -> SizeSource -> Bool # (>) :: SizeSource -> SizeSource -> Bool # (>=) :: SizeSource -> SizeSource -> Bool # max :: SizeSource -> SizeSource -> SizeSource # min :: SizeSource -> SizeSource -> SizeSource # |
Type checking happens with access to this environment. The
TermScope
will be extended during type-checking as bindings come into
scope.
TermEnv | |
|
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.
Instances
MonadState TermTypeState TermTypeM Source # | |
Defined in Language.Futhark.TypeChecker.Terms.Monad get :: TermTypeM TermTypeState # put :: TermTypeState -> TermTypeM () # state :: (TermTypeState -> (a, TermTypeState)) -> TermTypeM a # |
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 #
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.
Primitive checking
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 NoInfo Name -> TermTypeM (TypeExp Info VName, ResType, [VName]) Source #
Sizes
Control flow
Errors
unusedSize :: MonadTypeChecker m => SizeBinder VName -> m a Source #