HOL.TypeSubst

Documentation

data TypeSubst

Constructors

TypeSubst (Map TypeVar Type) (Map Type (Maybe Type))

Instances

Eq TypeSubst

Methods

(==) :: TypeSubst -> TypeSubst -> Bool

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

Printable TypeSubst

Methods

toDoc :: TypeSubst -> Doc

toStringWith :: Style -> TypeSubst -> String

toString :: TypeSubst -> String

mk :: Map TypeVar Type -> TypeSubst

dest :: TypeSubst -> Map TypeVar Type

fromList :: [(TypeVar, Type)] -> TypeSubst

empty :: TypeSubst

singleton :: TypeVar -> Type -> TypeSubst

null :: TypeSubst -> Bool

varSubst :: TypeVar -> TypeSubst -> Maybe Type

dataSubst :: TypeData -> TypeSubst -> (Maybe Type, TypeSubst)

class CanSubst a where

Minimal complete definition

basicSubst

Methods

basicSubst :: a -> TypeSubst -> (Maybe a, TypeSubst)

sharingSubst :: a -> TypeSubst -> (Maybe a, TypeSubst)

subst :: TypeSubst -> a -> Maybe a

trySharingSubst :: a -> TypeSubst -> (a, TypeSubst)

trySubst :: TypeSubst -> a -> a

Instances

CanSubst Var

Methods

basicSubst :: Var -> TypeSubst -> (Maybe Var, TypeSubst)

sharingSubst :: Var -> TypeSubst -> (Maybe Var, TypeSubst)

subst :: TypeSubst -> Var -> Maybe Var

trySharingSubst :: Var -> TypeSubst -> (Var, TypeSubst)

trySubst :: TypeSubst -> Var -> Var

CanSubst Type

Methods

basicSubst :: Type -> TypeSubst -> (Maybe Type, TypeSubst)

sharingSubst :: Type -> TypeSubst -> (Maybe Type, TypeSubst)

subst :: TypeSubst -> Type -> Maybe Type

trySharingSubst :: Type -> TypeSubst -> (Type, TypeSubst)

trySubst :: TypeSubst -> Type -> Type

CanSubst a => CanSubst [a]

Methods

basicSubst :: [a] -> TypeSubst -> (Maybe [a], TypeSubst)

sharingSubst :: [a] -> TypeSubst -> (Maybe [a], TypeSubst)

subst :: TypeSubst -> [a] -> Maybe [a]

trySharingSubst :: [a] -> TypeSubst -> ([a], TypeSubst)

trySubst :: TypeSubst -> [a] -> [a]

(Ord a, CanSubst a) => CanSubst (Set a)

Methods

basicSubst :: Set a -> TypeSubst -> (Maybe (Set a), TypeSubst)

sharingSubst :: Set a -> TypeSubst -> (Maybe (Set a), TypeSubst)

subst :: TypeSubst -> Set a -> Maybe (Set a)

trySharingSubst :: Set a -> TypeSubst -> (Set a, TypeSubst)

trySubst :: TypeSubst -> Set a -> Set a

compose :: TypeSubst -> TypeSubst -> TypeSubst

• subst (compose s1 s2) t == subst s2 (subst s1 t)