| Safe Haskell | None |
|---|---|
| Language | GHC2021 |
Language.Futhark.TypeChecker.Unify
Description
Implementation of unification and other core type system building blocks.
Synopsis
- data Constraint
- data Usage = Usage (Maybe Text) Loc
- mkUsage :: Located a => a -> Text -> Usage
- mkUsage' :: Located a => a -> Usage
- type Level = Int
- type Constraints = Map VName (Level, Constraint)
- class Monad m => MonadUnify (m :: Type -> Type) where
- getConstraints :: m Constraints
- putConstraints :: Constraints -> m ()
- modifyConstraints :: (Constraints -> Constraints) -> m ()
- newDimVar :: Usage -> Rigidity -> Name -> m VName
- newRigidDim :: Located a => a -> RigidSource -> Name -> m VName
- newFlexibleDim :: Usage -> Name -> m VName
- curLevel :: m Level
- matchError :: Located loc => loc -> Notes -> BreadCrumbs -> StructType -> StructType -> m a
- unifyError :: Located loc => loc -> Notes -> BreadCrumbs -> Doc () -> m a
- data Rigidity
- data RigidSource
- = RigidArg (Maybe (QualName VName)) Text
- | RigidRet (Maybe (QualName VName))
- | RigidLoop
- | RigidSlice (Maybe Size) Text
- | RigidRange
- | RigidCond StructType StructType
- | RigidUnify
- | RigidOutOfScope Loc VName
- data BreadCrumbs
- allDimsFreshInType :: MonadUnify m => Usage -> Rigidity -> Name -> TypeBase d o -> m (TypeBase Size o, Map VName d)
- dimNotes :: (Located a, MonadUnify m) => a -> Exp -> m Notes
- normTypeFully :: (Substitutable a, MonadUnify m) => a -> m a
- unify :: MonadUnify m => Usage -> StructType -> StructType -> m ()
- unifyMostCommon :: MonadUnify m => Usage -> StructType -> StructType -> m (StructType, [VName])
- doUnification :: Loc -> [TypeParam] -> [TypeParam] -> StructType -> StructType -> Either TypeError ()
Documentation
data Constraint Source #
A constraint on a yet-ambiguous size variable, or information about a rigid type parameter or size.
Constructors
| ParamSize Loc | |
| Size (Maybe Exp) Usage | Is not actually a type, but a term-level size, possibly already set to something specific. |
| UnknownSize Loc RigidSource | A size that does not unify with anything - created from the result of applying a function whose return size is existential, or otherwise hiding a size. |
| InstSize Liftedness Usage | A size arising from instantiating a type parameter (of the
given liftedness) with a type whose sizes are not yet known.
In contrast to an ordinary |
| CopySize VName Int Usage | Another occurrence of the instantiated size denoted by the
given canonical size variable (an |
| ExistentialSize (Maybe VName) (Maybe Loc) Usage | An instantiated size that unification has determined to
correspond to an existential size, possibly with the variable
it was unified with (used to identify existentials with the
same origin). Each variable constrained by this (or a
|
Instances
| Show Constraint Source # | |
Defined in Language.Futhark.TypeChecker.Unify Methods showsPrec :: Int -> Constraint -> ShowS # show :: Constraint -> String # showList :: [Constraint] -> ShowS # | |
| Located Constraint Source # | |
Defined in Language.Futhark.TypeChecker.Unify | |
A usage that caused a type constraint.
mkUsage :: Located a => a -> Text -> Usage Source #
Construct a Usage from a location and a description.
mkUsage' :: Located a => a -> Usage Source #
Construct a Usage that has just a location, but no particular
description.
The level at which a type variable is bound. Higher means
deeper. We can only unify a type variable at level i with a type
t if all type names that occur in t are at most at level i.
type Constraints = Map VName (Level, Constraint) Source #
Mapping from fresh type variables, instantiated from the type schemes of polymorphic functions, to (possibly) specific types as determined on application and the location of that application, or a partial constraint on their type.
class Monad m => MonadUnify (m :: Type -> Type) where Source #
Monads that which to perform unification must implement this type class.
Minimal complete definition
getConstraints, putConstraints, newDimVar, curLevel, matchError, unifyError
Methods
getConstraints :: m Constraints Source #
putConstraints :: Constraints -> m () Source #
modifyConstraints :: (Constraints -> Constraints) -> m () Source #
newDimVar :: Usage -> Rigidity -> Name -> m VName Source #
newRigidDim :: Located a => a -> RigidSource -> Name -> m VName Source #
newFlexibleDim :: Usage -> Name -> m VName Source #
matchError :: Located loc => loc -> Notes -> BreadCrumbs -> StructType -> StructType -> m a Source #
unifyError :: Located loc => loc -> Notes -> BreadCrumbs -> Doc () -> m a Source #
Instances
| MonadUnify TermTypeM Source # | |
Defined in Language.Futhark.TypeChecker.Terms.Monad Methods getConstraints :: TermTypeM Constraints Source # putConstraints :: Constraints -> TermTypeM () Source # modifyConstraints :: (Constraints -> Constraints) -> TermTypeM () 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 # | |
The ridigity of a size variable. All rigid sizes are tagged with information about how they were generated.
Constructors
| Rigid RigidSource | |
| Nonrigid |
data RigidSource Source #
The source of a rigid size.
Constructors
| RigidArg (Maybe (QualName VName)) Text | A function argument that is not a constant or variable name. |
| RigidRet (Maybe (QualName VName)) | An existential return size. |
| RigidLoop | Similarly to |
| RigidSlice (Maybe Size) Text | Produced by a complicated slice expression. |
| RigidRange | Produced by a complicated range expression. |
| RigidCond StructType StructType | Mismatch in branches. |
| RigidUnify | Invented during unification. |
| RigidOutOfScope Loc VName | A name used in a size went out of scope. |
Instances
| Show RigidSource Source # | |
Defined in Language.Futhark.TypeChecker.Unify Methods showsPrec :: Int -> RigidSource -> ShowS # show :: RigidSource -> String # showList :: [RigidSource] -> ShowS # | |
| Eq RigidSource Source # | |
Defined in Language.Futhark.TypeChecker.Unify | |
| Ord RigidSource Source # | |
Defined in Language.Futhark.TypeChecker.Unify Methods compare :: RigidSource -> RigidSource -> Ordering # (<) :: RigidSource -> RigidSource -> Bool # (<=) :: RigidSource -> RigidSource -> Bool # (>) :: RigidSource -> RigidSource -> Bool # (>=) :: RigidSource -> RigidSource -> Bool # max :: RigidSource -> RigidSource -> RigidSource # min :: RigidSource -> RigidSource -> RigidSource # | |
data BreadCrumbs Source #
Unification failures can occur deep down inside complicated types
(consider nested records). We leave breadcrumbs behind us so we can
report the path we took to find the mismatch. When combining
breadcrumbs with the Semigroup instance, put the innermost
breadcrumbs to the left.
Instances
| Monoid BreadCrumbs Source # | |
Defined in Language.Futhark.TypeChecker.Error Methods mempty :: BreadCrumbs # mappend :: BreadCrumbs -> BreadCrumbs -> BreadCrumbs # mconcat :: [BreadCrumbs] -> BreadCrumbs # | |
| Semigroup BreadCrumbs Source # | |
Defined in Language.Futhark.TypeChecker.Error Methods (<>) :: BreadCrumbs -> BreadCrumbs -> BreadCrumbs # sconcat :: NonEmpty BreadCrumbs -> BreadCrumbs # stimes :: Integral b => b -> BreadCrumbs -> BreadCrumbs # | |
| Pretty BreadCrumbs Source # | |
Defined in Language.Futhark.TypeChecker.Error | |
allDimsFreshInType :: MonadUnify m => Usage -> Rigidity -> Name -> TypeBase d o -> m (TypeBase Size o, Map VName d) Source #
Replace *all* dimensions with distinct fresh size variables.
dimNotes :: (Located a, MonadUnify m) => a -> Exp -> m Notes Source #
Retrieve notes describing the purpose or origin of the given
Size. The location is used as the *current* location, for the
purpose of reporting relative locations.
normTypeFully :: (Substitutable a, MonadUnify m) => a -> m a Source #
Replace all type variables with their substitution.
unify :: MonadUnify m => Usage -> StructType -> StructType -> m () Source #
Unifies two types.
unifyMostCommon :: MonadUnify m => Usage -> StructType -> StructType -> m (StructType, [VName]) Source #
Like unification, but creates new size variables where mismatches occur. Returns the new dimensions thus created.
doUnification :: Loc -> [TypeParam] -> [TypeParam] -> StructType -> StructType -> Either TypeError () Source #
Check that two types match, instantiating the nonrigid type parameters of the second type as necessary. This is used when matching a value or type in a module against a specification.
This works in two phases. First the types are checked while disregarding sizes entirely, using the same constraint solver as the unsized type checker. This also determines the instantiation of the nonrigid type parameters, up to sizes. Then the instantiations, given fresh size variables, are substituted into the second type, and the sizes are checked with ordinary (size-only) unification.