Language.Futhark.TypeChecker.Unify

Documentation

data Constraint

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

Defined in Language.Futhark.TypeChecker.Unify

Methods

showsPrec :: Int -> Constraint -> ShowS

show :: Constraint -> String

showList :: [Constraint] -> ShowS

Located Constraint

Defined in Language.Futhark.TypeChecker.Unify

Methods

locOf :: Constraint -> Loc

locOfList :: [Constraint] -> Loc

data Usage

A usage that caused a type constraint.

Instances

Show Usage

Defined in Language.Futhark.TypeChecker.Unify

Methods

showsPrec :: Int -> Usage -> ShowS

show :: Usage -> String

showList :: [Usage] -> ShowS

Pretty Usage

Defined in Language.Futhark.TypeChecker.Unify

Methods

ppr :: Usage -> Doc

pprPrec :: Int -> Usage -> Doc

pprList :: [Usage] -> Doc

Located Usage

Defined in Language.Futhark.TypeChecker.Unify

Methods

locOf :: Usage -> Loc

locOfList :: [Usage] -> Loc

mkUsage :: SrcLoc -> String -> Usage

mkUsage' :: SrcLoc -> Usage

type Level = Int

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)

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

Minimal complete definition

getConstraints, putConstraints, newTypeVar, newDimVar, curLevel, matchError, unifyError

Methods

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

The ridigity of a size variable. All rigid sizes are tagged with information about how they were generated.

Constructors

Rigid RigidSource

Nonrigid

Instances

Eq Rigidity

Defined in Language.Futhark.TypeChecker.Unify

Methods

(==) :: Rigidity -> Rigidity -> Bool

(/=) :: Rigidity -> Rigidity -> Bool

Ord Rigidity

Defined in Language.Futhark.TypeChecker.Unify

Methods

compare :: Rigidity -> Rigidity -> Ordering

(<) :: Rigidity -> Rigidity -> Bool

(<=) :: Rigidity -> Rigidity -> Bool

(>) :: Rigidity -> Rigidity -> Bool

(>=) :: Rigidity -> Rigidity -> Bool

max :: Rigidity -> Rigidity -> Rigidity

min :: Rigidity -> Rigidity -> Rigidity

Show Rigidity

Defined in Language.Futhark.TypeChecker.Unify

Methods

showsPrec :: Int -> Rigidity -> ShowS

show :: Rigidity -> String

showList :: [Rigidity] -> ShowS

data RigidSource

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

Defined in Language.Futhark.TypeChecker.Unify

Methods

(==) :: RigidSource -> RigidSource -> Bool

(/=) :: RigidSource -> RigidSource -> Bool

Ord RigidSource

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

Defined in Language.Futhark.TypeChecker.Unify

Methods

showsPrec :: Int -> RigidSource -> ShowS

show :: RigidSource -> String

showList :: [RigidSource] -> ShowS

data BreadCrumbs

Instances

Pretty BreadCrumbs

Defined in Language.Futhark.TypeChecker.Unify

Methods

ppr :: BreadCrumbs -> Doc

pprPrec :: Int -> BreadCrumbs -> Doc

pprList :: [BreadCrumbs] -> Doc

noBreadCrumbs :: BreadCrumbs

hasNoBreadCrumbs :: BreadCrumbs -> Bool

dimNotes :: (Located a, MonadUnify m) => a -> DimDecl VName -> m Notes

mkTypeVarName :: String -> Int -> Name

Construct a 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 ()

mustHaveConstr :: MonadUnify m => Usage -> Name -> StructType -> [StructType] -> m ()

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

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 ()

Unifies two types.

expect :: MonadUnify m => Usage -> StructType -> StructType -> m ()

expect super sub checks that sub is a subtype of super.

unifyMostCommon :: MonadUnify m => Usage -> PatternType -> PatternType -> m (PatternType, [VName])

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)])

Replace dimension mismatches with AnyDim.

doUnification :: SrcLoc -> [TypeParam] -> StructType -> StructType -> Either TypeError StructType

Perform a unification of two types outside a monadic context. The type parameters are allowed to be instantiated; all other types are considered rigid.