Safe Haskell | Trustworthy |
---|---|
Language | Haskell2010 |
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 :: TermTypeM a -> TypeM (a, Occurrences)
- liftTypeM :: TypeM a -> TermTypeM a
- data ValBinding
- data Locality
- data SizeSource
- data NameReason = NameAppRes (Maybe (QualName VName)) SrcLoc
- data InferredType
- data Checking
- = CheckingApply (Maybe (QualName VName)) Exp StructType StructType
- | CheckingReturn StructType StructType
- | CheckingAscription StructType StructType
- | CheckingLetGeneralise Name
- | CheckingParams (Maybe Name)
- | CheckingPat UncheckedPat InferredType
- | 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 PatType
- expTypeFully :: Exp -> TermTypeM PatType
- constrain :: VName -> Constraint -> TermTypeM ()
- newArrayType :: SrcLoc -> Name -> Int -> TermTypeM (StructType, StructType)
- allDimsFreshInType :: SrcLoc -> Rigidity -> Name -> TypeBase Size als -> TermTypeM (TypeBase Size als, Map VName Size)
- updateTypes :: ASTMappable e => e -> TermTypeM e
- unifies :: String -> StructType -> Exp -> TermTypeM Exp
- require :: String -> [PrimType] -> Exp -> TermTypeM Exp
- checkTypeExpNonrigid :: TypeExp Name -> TermTypeM (TypeExp VName, StructType, [VName])
- checkTypeExpRigid :: TypeExp Name -> RigidSource -> TermTypeM (TypeExp VName, StructType, [VName])
- isInt64 :: Exp -> Maybe Int64
- maybeDimFromExp :: Exp -> Maybe Size
- dimFromExp :: (Exp -> SizeSource) -> Exp -> TermTypeM (Size, Maybe VName)
- sizeFromArg :: Maybe (QualName VName) -> Exp -> TermTypeM (Size, Maybe VName)
- noSizeEscape :: TermTypeM a -> TermTypeM a
- collectOccurrences :: TermTypeM a -> TermTypeM (a, Occurrences)
- tapOccurrences :: TermTypeM a -> TermTypeM (a, Occurrences)
- alternative :: TermTypeM a -> TermTypeM b -> TermTypeM (a, b)
- sequentially :: TermTypeM a -> (a -> Occurrences -> TermTypeM b) -> TermTypeM b
- incLevel :: TermTypeM a -> TermTypeM a
- type Names = Set VName
- data Occurrence = Occurrence {}
- type Occurrences = [Occurrence]
- onlySelfAliasing :: TermTypeM a -> TermTypeM a
- noUnique :: TermTypeM a -> TermTypeM a
- removeSeminullOccurrences :: TermTypeM a -> TermTypeM a
- occur :: Occurrences -> TermTypeM ()
- observe :: Ident -> TermTypeM ()
- consume :: SrcLoc -> Aliasing -> TermTypeM ()
- consuming :: Ident -> TermTypeM a -> TermTypeM a
- observation :: Aliasing -> SrcLoc -> Occurrence
- consumption :: Aliasing -> SrcLoc -> Occurrence
- checkIfConsumable :: SrcLoc -> Aliasing -> TermTypeM ()
- seqOccurrences :: Occurrences -> Occurrences -> Occurrences
- checkOccurrences :: Occurrences -> TermTypeM ()
- allConsumed :: Occurrences -> Names
- useAfterConsume :: VName -> SrcLoc -> SrcLoc -> TermTypeM a
- unusedSize :: MonadTypeChecker m => SizeBinder VName -> m a
- notConsumable :: MonadTypeChecker m => SrcLoc -> Doc -> m b
- uniqueReturnAliased :: SrcLoc -> TermTypeM a
- returnAliased :: Name -> SrcLoc -> TermTypeM ()
- badLetWithValue :: (Pretty arr, Pretty src) => arr -> src -> SrcLoc -> TermTypeM a
- anyConsumption :: Occurrences -> Maybe Occurrence
- allOccurring :: Occurrences -> Names
Documentation
Instances
runTermTypeM :: TermTypeM a -> TypeM (a, Occurrences) Source #
data ValBinding Source #
Constructors
BoundV Locality [TypeParam] PatType | Aliases in parameters indicate the lexical closure. |
OverloadedF [PrimType] [Maybe PrimType] (Maybe PrimType) | |
EqualityF | |
WasConsumed SrcLoc |
Instances
Show ValBinding Source # | |
Defined in Language.Futhark.TypeChecker.Terms.Monad Methods showsPrec :: Int -> ValBinding -> ShowS # show :: ValBinding -> String # showList :: [ValBinding] -> ShowS # |
How something was bound.
Constructors
Local | In the current function |
Nonlocal | In an enclosing function, but not the current one. |
Global | At global scope. |
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
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 # | |
Show SizeSource Source # | |
Defined in Language.Futhark.TypeChecker.Terms.Monad Methods showsPrec :: Int -> SizeSource -> ShowS # show :: SizeSource -> String # showList :: [SizeSource] -> ShowS # |
data NameReason Source #
A description of where an artificial compiler-generated intermediate name came from.
Constructors
NameAppRes (Maybe (QualName VName)) SrcLoc | Name is the result of a function application. |
data InferredType Source #
Constructors
NoneInferred | |
Ascribed PatType |
Constructors
Type checking happens with access to this environment. The
TermScope
will be extended during type-checking as bindings come into
scope.
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 PatType Source #
Get the type of an expression, with top level type variables
substituted. Never call typeOf
directly (except in a few
carefully inspected locations)!
newArrayType :: SrcLoc -> Name -> Int -> TermTypeM (StructType, StructType) Source #
allDimsFreshInType :: SrcLoc -> 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 :: String -> [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 Name -> TermTypeM (TypeExp VName, StructType, [VName]) Source #
checkTypeExpRigid :: TypeExp Name -> RigidSource -> TermTypeM (TypeExp VName, StructType, [VName]) Source #
Sizes
dimFromExp :: (Exp -> SizeSource) -> Exp -> TermTypeM (Size, Maybe VName) Source #
noSizeEscape :: TermTypeM a -> TermTypeM a Source #
Any argument sizes created with extSize
inside the given action
will be removed once the action finishes. This is to ensure that
just because e.g. n+1
appears as a size in one branch of a
conditional, that doesn't mean it's also available in the other
branch.
Control flow
collectOccurrences :: TermTypeM a -> TermTypeM (a, Occurrences) Source #
tapOccurrences :: TermTypeM a -> TermTypeM (a, Occurrences) Source #
sequentially :: TermTypeM a -> (a -> Occurrences -> TermTypeM b) -> TermTypeM b Source #
Consumption and uniqueness
data Occurrence Source #
The consumption set is a Maybe so we can distinguish whether a consumption took place, but the variable went out of scope since, or no consumption at all took place.
Instances
Eq Occurrence Source # | |
Defined in Language.Futhark.TypeChecker.Terms.Monad | |
Show Occurrence Source # | |
Defined in Language.Futhark.TypeChecker.Terms.Monad Methods showsPrec :: Int -> Occurrence -> ShowS # show :: Occurrence -> String # showList :: [Occurrence] -> ShowS # | |
Located Occurrence Source # | |
Defined in Language.Futhark.TypeChecker.Terms.Monad |
type Occurrences = [Occurrence] Source #
onlySelfAliasing :: TermTypeM a -> TermTypeM a Source #
noUnique :: TermTypeM a -> TermTypeM a Source #
Enter a context where nothing outside can be consumed (i.e. the body of a function definition).
removeSeminullOccurrences :: TermTypeM a -> TermTypeM a Source #
occur :: Occurrences -> TermTypeM () Source #
observe :: Ident -> TermTypeM () Source #
Proclaim that we have made read-only use of the given variable.
consume :: SrcLoc -> Aliasing -> TermTypeM () Source #
Proclaim that we have written to the given variable.
consuming :: Ident -> TermTypeM a -> TermTypeM a Source #
Proclaim that we have written to the given variable, and mark accesses to it and all of its aliases as invalid inside the given computation.
observation :: Aliasing -> SrcLoc -> Occurrence Source #
consumption :: Aliasing -> SrcLoc -> Occurrence Source #
seqOccurrences :: Occurrences -> Occurrences -> Occurrences Source #
checkOccurrences :: Occurrences -> TermTypeM () Source #
allConsumed :: Occurrences -> Names Source #
Errors
unusedSize :: MonadTypeChecker m => SizeBinder VName -> m a Source #
notConsumable :: MonadTypeChecker m => SrcLoc -> Doc -> m b Source #
uniqueReturnAliased :: SrcLoc -> TermTypeM a Source #
allOccurring :: Occurrences -> Names Source #