| Safe Haskell | None |
|---|---|
| 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 Info VName -> TermTypeM Exp) -> Map TyVar (TypeBase () NoMode) -> TermTypeM a -> TypeM a
- data ValBinding dim
- 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 Info VName StructType) (Inferred StructType)
- | CheckingLoopBody StructType StructType
- | CheckingLoopInitial StructType StructType
- | CheckingRecordUpdate [Name] StructType StructType
- | CheckingBranches StructType StructType
- withEnv :: TermEnv -> Env -> TermEnv
- localScope :: (TermScope Size -> TermScope Size) -> TermTypeM a -> TermTypeM a
- data TermEnv = TermEnv {
- termScope :: TermScope Size
- termChecking :: Maybe Checking
- termLevel :: Level
- termCheckExp :: ExpBase Info VName -> TermTypeM Exp
- termOuterEnv :: Env
- termTySet :: TySet
- termTyVars :: Map TyVar (TypeBase () NoMode)
- termImportName :: ImportName
- data TermScope dim = TermScope {
- scopeVtable :: Map VName (ValBinding dim)
- scopeTypeTable :: Map VName TypeBinding
- scopeModTable :: Map VName Mod
- 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 ()
- instTyVars :: Substitutable (TypeBase Size o) => SrcLoc -> Map VName Liftedness -> TypeBase () o -> TypeBase Size o -> TermTypeM (TypeBase Size o)
- replaceTyVars :: SrcLoc -> TypeBase Size o -> TermTypeM (TypeBase Size o)
- replaceTyVarsAbsorbable :: SrcLoc -> TypeBase Size o -> TermTypeM (TypeBase Size o)
- updateTypes :: ASTMappable e => e -> TermTypeM e
- type Names = Set VName
- unifies :: Text -> StructType -> Exp -> TermTypeM Exp
- checkTypeExpNonrigid :: TypeExp Exp VName -> TermTypeM (TypeExp Exp VName, ResType, [VName])
- lookupVar :: SrcLoc -> QualName VName -> StructType -> TermTypeM StructType
- lookupMod :: QualName VName -> TermTypeM Mod
- typeSchemes :: TermTypeM (QualName VName -> Maybe BoundV)
- lookupAbsTy :: QualName VName -> TermTypeM Liftedness
- isInt64 :: Exp -> Maybe Int64
- incLevel :: TermTypeM a -> TermTypeM a
- unusedSize :: MonadTypeChecker m => SizeBinder VName -> m a
Documentation
Instances
runTermTypeM :: (ExpBase Info VName -> TermTypeM Exp) -> Map TyVar (TypeBase () NoMode) -> TermTypeM a -> TypeM a Source #
data ValBinding dim Source #
What a bound value stands for. Note that although modules are in the same name space, they are not value bindings.
Constructors
| BoundV [TypeParam] (TypeBase dim NoMode) | |
| OverloadedF [PrimType] [Maybe PrimType] (Maybe PrimType) | |
| EqualityF | |
| RecursiveV | A recursive function with no declared return type, currently being checked and in scope of its own body. Each occurrence adopts the type recorded for it by the unsized type checker, with fresh (unrelated) sizes. See Note [Checking recursive functions] in Language.Futhark.TypeChecker.Terms. |
Instances
| Show dim => Show (ValBinding dim) Source # | |
Defined in Language.Futhark.TypeChecker.Terms.Scope Methods showsPrec :: Int -> ValBinding dim -> ShowS # show :: ValBinding dim -> String # showList :: [ValBinding dim] -> 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
| 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 # | |
During type checking a pattern, we might find an explicit ascription. These contain complete type information (although they must of course still be checked against what remains of the pattern).
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
| |
The lexical scope information.
Constructors
| TermScope | |
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. Currently no different from
typeOf, but kept as the counterpart of expTypeFully.
expTypeFully :: Exp -> TermTypeM StructType Source #
Arguments
| :: Substitutable (TypeBase Size o) | |
| => SrcLoc | |
| -> Map VName Liftedness | The type parameters being instantiated, along with their liftedness. |
| -> TypeBase () o | |
| -> TypeBase Size o | |
| -> TermTypeM (TypeBase Size o) |
Instantiate the type parameters of a type scheme with the types inferred by the unsized type checker, creating fresh variables for their sizes. See Note [Size Inference] in Language.Futhark.TypeChecker.Terms.
replaceTyVars :: SrcLoc -> TypeBase Size o -> TermTypeM (TypeBase Size o) Source #
Replace type variables inferred by the unsized type checker with their solutions, instantiating their sizes with fresh (non-absorbable) size variables. See Note [Size Inference] in Language.Futhark.TypeChecker.Terms.
replaceTyVarsAbsorbable :: SrcLoc -> TypeBase Size o -> TermTypeM (TypeBase Size o) Source #
Like replaceTyVars, but the fresh sizes may be determined to
be existential by unification, like instantiated sizes. This is
used for holes, which adopt whatever type the context provides.
See Note [Size Inference] in Language.Futhark.TypeChecker.Terms.
updateTypes :: ASTMappable e => e -> TermTypeM e Source #
Replace all type variables with their concrete types.
Primitive checking
checkTypeExpNonrigid :: TypeExp Exp VName -> TermTypeM (TypeExp Exp VName, ResType, [VName]) Source #
lookupVar :: SrcLoc -> QualName VName -> StructType -> TermTypeM StructType Source #
typeSchemes :: TermTypeM (QualName VName -> Maybe BoundV) Source #
A pure function for looking up the type scheme of a global name. Used by consumption checking to exploit parametricity; see Note [Parametric results] in Language.Futhark.TypeChecker.Consumption.
lookupAbsTy :: QualName VName -> TermTypeM Liftedness Source #
Look up the liftedness of an abstract type.
Sizes
Control flow
Errors
unusedSize :: MonadTypeChecker m => SizeBinder VName -> m a Source #