Safe Haskell | Trustworthy |
---|---|
Language | Haskell2010 |
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 ()
- normType :: MonadUnify m => StructType -> m StructType
- 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.
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 showsPrec :: Int -> Constraint -> ShowS # show :: Constraint -> String # showList :: [Constraint] -> ShowS # | |
Located Constraint Source # | |
Defined in Language.Futhark.TypeChecker.Unify locOf :: Constraint -> Loc # locOfList :: [Constraint] -> Loc # |
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.
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.
data RigidSource Source #
The source of a rigid size.
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 (==) :: RigidSource -> RigidSource -> Bool # (/=) :: RigidSource -> RigidSource -> Bool # | |
Ord RigidSource Source # | |
Defined in Language.Futhark.TypeChecker.Unify 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 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 |
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.
normType :: MonadUnify m => StructType -> m StructType Source #
Replace any top-level type variable with its substitution.
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.