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
- = 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 # show :: Constraint -> String # showList :: [Constraint] -> ShowS #
Located Constraint Source #
Instance details Defined in Language.Futhark.TypeChecker.Unify Methods locOf :: Constraint -> Loc # locOfList :: [Constraint] -> Loc #

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

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 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 # show :: Rigidity -> String # showList :: [Rigidity] -> ShowS #
Eq Rigidity Source #
Instance details Defined in Language.Futhark.TypeChecker.Unify Methods (==) :: Rigidity -> Rigidity -> Bool # (/=) :: Rigidity -> Rigidity -> Bool #
Ord Rigidity Source #
Instance details 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 #

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 # show :: RigidSource -> String # showList :: [RigidSource] -> ShowS #
Eq RigidSource Source #
Instance details Defined in Language.Futhark.TypeChecker.Unify Methods (==) :: RigidSource -> RigidSource -> Bool # (/=) :: RigidSource -> RigidSource -> Bool #
Ord RigidSource Source #
Instance details 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

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.

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