| Safe Haskell | Trustworthy |
|---|---|
| Language | Haskell2010 |
Language.Futhark.TypeChecker.Unify
Description
Implementation of unification and other core type system building blocks.
Synopsis
- data Constraint
- = NoConstraint Liftedness Usage
- | ParamType Liftedness SrcLoc
- | Constraint StructType Usage
- | Overloaded [PrimType] Usage
- | HasFields (Map Name StructType) Usage
- | Equality Usage
- | HasConstrs (Map Name [StructType]) Usage
- | ParamSize SrcLoc
- | Size (Maybe (DimDecl VName)) Usage
- | UnknowableSize SrcLoc RigidSource
- data Usage
- mkUsage :: SrcLoc -> String -> Usage
- mkUsage' :: SrcLoc -> 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 => SrcLoc -> String -> m (TypeBase dim als)
- newDimVar :: SrcLoc -> Rigidity -> String -> 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 -> DimDecl VName -> m Notes
- mkTypeVarName :: String -> Int -> Name
- zeroOrderType :: (MonadUnify m, Pretty (ShapeDecl dim), Monoid as) => Usage -> String -> TypeBase dim as -> m ()
- arrayElemType :: (MonadUnify m, Pretty (ShapeDecl dim), Monoid as) => Usage -> String -> TypeBase dim as -> m ()
- mustHaveConstr :: MonadUnify m => Usage -> Name -> StructType -> [StructType] -> m ()
- mustHaveField :: MonadUnify m => Usage -> Name -> PatternType -> m PatternType
- mustBeOneOf :: MonadUnify m => [PrimType] -> Usage -> StructType -> m ()
- equalityType :: (MonadUnify m, Pretty (ShapeDecl dim), Monoid as) => Usage -> TypeBase dim as -> m ()
- normPatternType :: MonadUnify m => PatternType -> m PatternType
- normTypeFully :: (Substitutable a, MonadUnify m) => a -> m a
- instantiateEmptyArrayDims :: MonadUnify m => SrcLoc -> String -> Rigidity -> TypeBase (DimDecl VName) als -> m (TypeBase (DimDecl VName) als, [VName])
- unify :: MonadUnify m => Usage -> StructType -> StructType -> m ()
- expect :: MonadUnify m => Usage -> StructType -> StructType -> m ()
- unifyMostCommon :: MonadUnify m => Usage -> PatternType -> PatternType -> m (PatternType, [VName])
- anyDimOnMismatch :: Monoid as => TypeBase (DimDecl VName) as -> TypeBase (DimDecl VName) as -> (TypeBase (DimDecl VName) as, [(DimDecl VName, DimDecl VName)])
- doUnification :: SrcLoc -> [TypeParam] -> StructType -> StructType -> Either TypeError StructType
Documentation
data Constraint Source #
A constraint on a yet-ambiguous type variable.
Constructors
| NoConstraint Liftedness Usage | |
| ParamType Liftedness SrcLoc | |
| Constraint StructType Usage | |
| Overloaded [PrimType] Usage | |
| HasFields (Map Name StructType) Usage | |
| Equality Usage | |
| HasConstrs (Map Name [StructType]) Usage | |
| ParamSize SrcLoc | |
| Size (Maybe (DimDecl VName)) Usage | Is not actually a type, but a term-level size, possibly already set to something specific. |
| UnknowableSize SrcLoc 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' :: SrcLoc -> 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 => SrcLoc -> String -> m (TypeBase dim als) Source #
newDimVar :: SrcLoc -> Rigidity -> String -> m VName Source #
matchError :: Located loc => loc -> Notes -> BreadCrumbs -> StructType -> StructType -> m a Source #
unifyError :: Located loc => loc -> Notes -> BreadCrumbs -> Doc -> m 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)) String | A function argument that is not a constant or variable name. |
| RigidRet (Maybe (QualName VName)) | An existential return size. |
| RigidLoop | |
| RigidSlice (Maybe (DimDecl VName)) String | Produced by a complicated slice expression. |
| RigidRange | Produced by a complicated range expression. |
| RigidBound String | Produced by a range expression with this bound. |
| RigidCond StructType StructType | Mismatch in branches. |
| RigidUnify | Invented during unification. |
| RigidOutOfScope SrcLoc VName |
Instances
| 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 # | |
| Show RigidSource Source # | |
Defined in Language.Futhark.TypeChecker.Unify Methods showsPrec :: Int -> RigidSource -> ShowS # show :: RigidSource -> String # showList :: [RigidSource] -> ShowS # | |
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 Methods ppr :: BreadCrumbs -> Doc # pprPrec :: Int -> BreadCrumbs -> Doc # pprList :: [BreadCrumbs] -> Doc # | |
noBreadCrumbs :: BreadCrumbs Source #
An empty path.
hasNoBreadCrumbs :: BreadCrumbs -> Bool Source #
Is the path empty?
dimNotes :: (Located a, MonadUnify m) => a -> DimDecl VName -> m Notes Source #
Retrieve notes describing the purpose or origin of the given
DimDecl. The location is used as the *current* location, for the
purpose of reporting relative locations.
mkTypeVarName :: String -> Int -> Name Source #
Construct the name of a new type variable given a base description and a tag number (note that this is distinct from actually constructing a VName; the tag here is intended for human consumption but the machine does not care).
zeroOrderType :: (MonadUnify m, Pretty (ShapeDecl dim), Monoid as) => Usage -> String -> TypeBase dim as -> m () Source #
Assert that this type must be zero-order.
arrayElemType :: (MonadUnify m, Pretty (ShapeDecl dim), Monoid as) => Usage -> String -> TypeBase dim as -> 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 -> PatternType -> m PatternType 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 (ShapeDecl dim), Monoid as) => Usage -> TypeBase dim as -> m () Source #
Assert that this type must support equality.
normPatternType :: MonadUnify m => PatternType -> m PatternType 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.
instantiateEmptyArrayDims :: MonadUnify m => SrcLoc -> String -> Rigidity -> TypeBase (DimDecl VName) als -> m (TypeBase (DimDecl VName) als, [VName]) Source #
Replace AnyDim dimensions that occur as PosImmediate or
PosParam with a fresh NamedDim.
unify :: MonadUnify m => Usage -> StructType -> StructType -> m () Source #
Unifies two types.
expect :: MonadUnify m => Usage -> StructType -> StructType -> m () Source #
expect super sub checks that sub is a subtype of super.
unifyMostCommon :: MonadUnify m => Usage -> PatternType -> PatternType -> m (PatternType, [VName]) Source #
Like unification, but creates new size variables where mismatches occur. Returns the new dimensions thus created.
anyDimOnMismatch :: Monoid as => TypeBase (DimDecl VName) as -> TypeBase (DimDecl VName) as -> (TypeBase (DimDecl VName) as, [(DimDecl VName, DimDecl VName)]) Source #
Replace dimension mismatches with AnyDim.
doUnification :: SrcLoc -> [TypeParam] -> StructType -> StructType -> Either TypeError StructType Source #
Perform a unification of two types outside a monadic context. The type parameters are allowed to be instantiated; all other types are considered rigid.