Safe Haskell	None
Language	Haskell2010

HOL.TypeSubst

Description

Synopsis

data TypeSubst = TypeSubst (Map TypeVar Type) (Map Type (Maybe Type))
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
- 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
compose :: TypeSubst -> TypeSubst -> TypeSubst

Documentation

data TypeSubst Source #

Constructors

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

Instances

Instances details

Eq TypeSubst Source #
Instance details Defined in HOL.TypeSubst Methods (==) :: TypeSubst -> TypeSubst -> Bool # (/=) :: TypeSubst -> TypeSubst -> Bool #
Printable TypeSubst Source #
Instance details Defined in HOL.Print Methods toDoc :: TypeSubst -> Doc Source # toStringWith :: Style -> TypeSubst -> String Source # toString :: TypeSubst -> String Source #

mk :: Map TypeVar Type -> TypeSubst Source #

dest :: TypeSubst -> Map TypeVar Type Source #

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

empty :: TypeSubst Source #

singleton :: TypeVar -> Type -> TypeSubst Source #

null :: TypeSubst -> Bool Source #

varSubst :: TypeVar -> TypeSubst -> Maybe Type Source #

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

class CanSubst a where Source #

Minimal complete definition

basicSubst

Methods

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

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

subst :: TypeSubst -> a -> Maybe a Source #

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

trySubst :: TypeSubst -> a -> a Source #

Instances

Instances details

CanSubst Var Source #
Instance details Defined in HOL.TypeSubst Methods basicSubst :: Var -> TypeSubst -> (Maybe Var, TypeSubst) Source # sharingSubst :: Var -> TypeSubst -> (Maybe Var, TypeSubst) Source # subst :: TypeSubst -> Var -> Maybe Var Source # trySharingSubst :: Var -> TypeSubst -> (Var, TypeSubst) Source # trySubst :: TypeSubst -> Var -> Var Source #
CanSubst Type Source #
Instance details Defined in HOL.TypeSubst Methods basicSubst :: Type -> TypeSubst -> (Maybe Type, TypeSubst) Source # sharingSubst :: Type -> TypeSubst -> (Maybe Type, TypeSubst) Source # subst :: TypeSubst -> Type -> Maybe Type Source # trySharingSubst :: Type -> TypeSubst -> (Type, TypeSubst) Source # trySubst :: TypeSubst -> Type -> Type Source #
CanSubst a => CanSubst [a] Source #
Instance details Defined in HOL.TypeSubst Methods basicSubst :: [a] -> TypeSubst -> (Maybe [a], TypeSubst) Source # sharingSubst :: [a] -> TypeSubst -> (Maybe [a], TypeSubst) Source # subst :: TypeSubst -> [a] -> Maybe [a] Source # trySharingSubst :: [a] -> TypeSubst -> ([a], TypeSubst) Source # trySubst :: TypeSubst -> [a] -> [a] Source #
(Ord a, CanSubst a) => CanSubst (Set a) Source #
Instance details Defined in HOL.TypeSubst Methods basicSubst :: Set a -> TypeSubst -> (Maybe (Set a), TypeSubst) Source # sharingSubst :: Set a -> TypeSubst -> (Maybe (Set a), TypeSubst) Source # subst :: TypeSubst -> Set a -> Maybe (Set a) Source # trySharingSubst :: Set a -> TypeSubst -> (Set a, TypeSubst) Source # trySubst :: TypeSubst -> Set a -> Set a Source #

compose :: TypeSubst -> TypeSubst -> TypeSubst Source #

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