Hets - the Heterogeneous Tool Set
Copyright(c) Christian Maeder and Uni Bremen 2003-2005
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityexperimental
Portabilityportable
Safe HaskellNone

HasCASL.Unify

Description

substitution and unification of types

Synopsis

Documentation

compSubst :: Subst -> Subst -> Subst Source #

composition (reversed: first substitution first!)

instScheme :: TypeMap -> Int -> TypeScheme -> TypeScheme -> Bool Source #

test if second scheme is a substitution instance

toEnvState :: State Int a -> State Env a Source #

lift State Int to State Env

toSchemes :: (Type -> Type -> a) -> TypeScheme -> TypeScheme -> State Int a Source #

asSchemes :: Int -> (Type -> Type -> a) -> TypeScheme -> TypeScheme -> a Source #

mapArgs :: Subst -> [(Id, Type)] -> [TypeArg] -> [(Type, VarKind)] Source #

inc :: State Int Int Source #

freshVar :: Id -> State Int (Id, Int) Source #

mkSubst :: [(Id, RawKind)] -> State Int [Type] Source #

type Subst = Map Int Type Source #

noAbs :: Type -> Bool Source #

match :: TypeMap -> (Id -> Id -> Bool) -> (Bool, Type) -> (Bool, Type) -> Result Subst Source #

subsume :: TypeMap -> Type -> Type -> Bool Source #

substGen :: Subst -> Type -> Type Source #

substitute generic variables with negative index

getTypeOf :: MonadFail m => Term -> m Type Source #

subst :: Subst -> Type -> Type Source #

substitute variables with positive index

uniResult :: String -> Type -> String -> Type -> Result Subst Source #

generalize :: [TypeArg] -> Type -> Type Source #

make representation of bound variables unique