| Safe Haskell | Safe-Inferred |
|---|---|
| Language | GHC2021 |
Language.Futhark.TypeChecker.Unify
Description
Implementation of unification and other core type system building blocks.
Synopsis
- data Constraint
- = NoConstraint Liftedness Usage
- | ParamType Liftedness Loc
- | Constraint StructRetType Usage
- | Overloaded [PrimType] Usage
- | HasFields Liftedness (Map Name StructType) Usage
- | Equality Usage
- | HasConstrs Liftedness (Map Name [StructType]) Usage
- | ParamSize Loc
- | Size (Maybe Exp) Usage
- | UnknownSize Loc RigidSource
- 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 where
- getConstraints :: m Constraints
- putConstraints :: Constraints -> m ()
- modifyConstraints :: (Constraints -> Constraints) -> m ()
- newTypeVar :: (Monoid als, Located a) => a -> Name -> m (TypeBase dim als)
- 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
- data BreadCrumbs
- noBreadCrumbs :: BreadCrumbs
- hasNoBreadCrumbs :: BreadCrumbs -> Bool
- dimNotes :: (Located a, MonadUnify m) => a -> Exp -> m Notes
- zeroOrderType :: MonadUnify m => Usage -> Text -> StructType -> m ()
- arrayElemType :: (MonadUnify m, Pretty (Shape dim), Pretty u) => Usage -> Text -> TypeBase dim u -> m ()
- mustHaveConstr :: MonadUnify m => Usage -> Name -> StructType -> [StructType] -> m ()
- mustHaveField :: MonadUnify m => Usage -> Name -> StructType -> m StructType
- mustBeOneOf :: MonadUnify m => [PrimType] -> Usage -> StructType -> m ()
- equalityType :: (MonadUnify m, Pretty (Shape dim), Pretty u) => Usage -> TypeBase dim u -> m ()
- normType :: MonadUnify m => StructType -> m StructType
- 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 StructType
Documentation
data Constraint Source #
A constraint on a yet-ambiguous type variable.
Constructors
| NoConstraint Liftedness Usage | |
| ParamType Liftedness Loc | |
| Constraint StructRetType Usage | |
| Overloaded [PrimType] Usage | |
| HasFields Liftedness (Map Name StructType) Usage | |
| Equality Usage | |
| HasConstrs Liftedness (Map Name [StructType]) Usage | |
| 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. |
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 where Source #
Monads that which to perform unification must implement this type class.
Minimal complete definition
getConstraints, putConstraints, newTypeVar, newDimVar, curLevel, matchError, unifyError
Methods
getConstraints :: m Constraints Source #
putConstraints :: Constraints -> m () Source #
modifyConstraints :: (Constraints -> Constraints) -> m () Source #
newTypeVar :: (Monoid als, Located a) => a -> Name -> m (TypeBase dim als) 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 # newTypeVar :: (Monoid als, Located a) => a -> Name -> TermTypeM (TypeBase dim als) 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 | |
| RigidSlice (Maybe Size) Text | Produced by a complicated slice expression. |
| RigidRange | Produced by a complicated range expression. |
| RigidBound Text | Produced by a range expression with this bound. |
| RigidCond StructType StructType | Mismatch in branches. |
| RigidUnify | Invented during unification. |
| RigidOutOfScope Loc VName | |
| RigidCoerce | Blank dimension in coercion. |
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.
Instances
| Pretty BreadCrumbs Source # | |
Defined in Language.Futhark.TypeChecker.Unify | |
noBreadCrumbs :: BreadCrumbs Source #
An empty path.
hasNoBreadCrumbs :: BreadCrumbs -> Bool Source #
Is the path empty?
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.
zeroOrderType :: MonadUnify m => Usage -> Text -> StructType -> m () Source #
Assert that this type must be zero-order.
arrayElemType :: (MonadUnify m, Pretty (Shape dim), Pretty u) => Usage -> Text -> TypeBase dim u -> m () Source #
Assert that this type must be valid as an array element.
mustHaveConstr :: MonadUnify m => Usage -> Name -> StructType -> [StructType] -> m () Source #
In mustHaveConstr usage c t fs, the type t must have a
constructor named c that takes arguments of types ts.
mustHaveField :: MonadUnify m => Usage -> Name -> StructType -> m StructType Source #
Assert that some type must have a field with this name and type.
mustBeOneOf :: MonadUnify m => [PrimType] -> Usage -> StructType -> m () Source #
Assert that this type must be one of the given primitive types.
equalityType :: (MonadUnify m, Pretty (Shape dim), Pretty u) => Usage -> TypeBase dim u -> m () Source #
Assert that this type must support equality.
normType :: MonadUnify m => StructType -> m StructType Source #
Replace any top-level type variable with its substitution.
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 StructType Source #
Perform a unification of two types outside a monadic context. The first list of type parameters are rigid but may have liftedness constraints; the second list of type parameters are allowed to be instantiated. All other types are considered rigid with no constraints.