| Safe Haskell | Safe-Inferred |
|---|---|
| Language | GHC2021 |
Language.Futhark.TypeChecker.Terms.Monad
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 VName -> 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 (PatBase NoInfo 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 {}
- 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 (ExpBase NoInfo 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
Instances
data ValBinding Source #
Constructors
| BoundV [TypeParam] StructType | |
| OverloadedF [PrimType] [Maybe PrimType] (Maybe PrimType) | |
| EqualityF |
Instances
| Show ValBinding Source # | |
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
| 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 Methods showsPrec :: Int -> SizeSource -> ShowS # show :: SizeSource -> String # showList :: [SizeSource] -> ShowS # | |
| Eq SizeSource Source # | |
Defined in Language.Futhark.TypeChecker.Terms.Monad | |
| Ord SizeSource Source # | |
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 # | |
Constructors
| NoneInferred | |
| Ascribed t |
Constructors
Type checking happens with access to this environment. The
TermScope will be extended during type-checking as bindings come into
scope.
Constructors
| TermEnv | |
Fields
| |
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 | |
Instances
| MonadState TermTypeState TermTypeM Source # | |
Defined in Language.Futhark.TypeChecker.Terms.Monad Methods 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 (ExpBase NoInfo VName) VName -> TermTypeM (TypeExp Exp VName, ResType, [VName]) Source #
Sizes
Control flow
Errors
unusedSize :: MonadTypeChecker m => SizeBinder VName -> m a Source #