futhark-0.25.32: An optimising compiler for a functional, array-oriented language.

Safe Haskell | None
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 :: Type -> Type) 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
  - = Rigid RigidSource
  - | Nonrigid
- 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
- sizeFree :: MonadUnify m => SrcLoc -> (Exp -> Maybe VName) -> TypeBase Size u -> m (TypeBase Size u, [VName])
- 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

Instances details

Show Constraint Source # |
Instance details Defined in Language.Futhark.TypeChecker.Unify Methods showsPrec :: Int -> Constraint -> ShowS Source # show :: Constraint -> String Source # showList :: [Constraint] -> ShowS Source #
Located Constraint Source # |
Instance details Defined in Language.Futhark.TypeChecker.Unify Methods locOf :: Constraint -> Loc Source # locOfList :: [Constraint] -> Loc Source #

data Usage Source #

A usage that caused a type constraint.

Constructors

Usage (Maybe Text) Loc |

#### Instances

Instances details

Show Usage Source # |
Instance details Defined in Language.Futhark.TypeChecker.Unify Methods showsPrec :: Int -> Usage -> ShowS Source # show :: Usage -> String Source # showList :: [Usage] -> ShowS Source #
Pretty Usage Source # |
Instance details Defined in Language.Futhark.TypeChecker.Unify Methods pretty :: Usage -> Doc ann Source # prettyList :: [Usage] -> Doc ann Source #
Located Usage Source # |
Instance details Defined in Language.Futhark.TypeChecker.Unify Methods locOf :: Usage -> Loc Source # locOfList :: [Usage] -> Loc Source #

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.

type Level = Int Source #

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, 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 #

curLevel :: m Level Source #

matchError :: Located loc => loc -> Notes -> BreadCrumbs -> StructType -> StructType -> m a Source #

unifyError :: Located loc => loc -> Notes -> BreadCrumbs -> Doc () -> m a Source #

#### Instances

Instances details

MonadUnify TermTypeM Source # |

Instance details

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 #

data Rigidity Source #

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

Constructors

Rigid RigidSource |
Nonrigid |

#### Instances

Instances details

Show Rigidity Source # |
Instance details Defined in Language.Futhark.TypeChecker.Unify Methods showsPrec :: Int -> Rigidity -> ShowS Source # show :: Rigidity -> String Source # showList :: [Rigidity] -> ShowS Source #
Eq Rigidity Source # |
Instance details Defined in Language.Futhark.TypeChecker.Unify Methods (==) :: Rigidity -> Rigidity -> Bool Source # (/=) :: Rigidity -> Rigidity -> Bool Source #
Ord Rigidity Source # |

Instance details

Defined in Language.Futhark.TypeChecker.Unify

Methods

compare :: Rigidity -> Rigidity -> Ordering Source #

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

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

(>) :: Rigidity -> Rigidity -> Bool Source #

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

max :: Rigidity -> Rigidity -> Rigidity Source #

min :: Rigidity -> Rigidity -> Rigidity Source #

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 `RigidRet`, but produce by a loop.
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

Instances details

Show RigidSource Source # |
Instance details Defined in Language.Futhark.TypeChecker.Unify Methods showsPrec :: Int -> RigidSource -> ShowS Source # show :: RigidSource -> String Source # showList :: [RigidSource] -> ShowS Source #
Eq RigidSource Source # |
Instance details Defined in Language.Futhark.TypeChecker.Unify Methods (==) :: RigidSource -> RigidSource -> Bool Source # (/=) :: RigidSource -> RigidSource -> Bool Source #
Ord RigidSource Source # |

Instance details

Defined in Language.Futhark.TypeChecker.Unify

Methods

compare :: RigidSource -> RigidSource -> Ordering Source #

(<) :: RigidSource -> RigidSource -> Bool Source #

(<=) :: RigidSource -> RigidSource -> Bool Source #

(>) :: RigidSource -> RigidSource -> Bool Source #

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

max :: RigidSource -> RigidSource -> RigidSource Source #

min :: RigidSource -> RigidSource -> RigidSource Source #

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

Instances details

Pretty BreadCrumbs Source # |
Instance details Defined in Language.Futhark.TypeChecker.Unify Methods pretty :: BreadCrumbs -> Doc ann Source # prettyList :: [BreadCrumbs] -> Doc ann Source #

sizeFree :: MonadUnify m => SrcLoc -> (Exp -> Maybe VName) -> TypeBase Size u -> m (TypeBase Size u, [VName]) Source #

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.