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.TypeAna

Contents

Description

analyse types

Synopsis

infer kind

getIdKind :: Env -> Id -> Result ((Variance, RawKind, Set Kind), Type)

extract kinds of type identifier

getCoVarKind :: Maybe Bool -> Env -> Id -> Result ((RawKind, Set Kind), Type)

extract kinds of co- or invariant type identifiers

subKinds :: DiagKind -> ClassMap -> Type -> Set Kind -> Set Kind -> Set Kind -> Result (Set Kind)

check if there is at least one solution

addTypeVarDecl :: Bool -> TypeArg -> State Env ()

add an analysed type argument (warn on redeclared types)

inferKinds :: Maybe Bool -> Type -> Env -> Result ((RawKind, Set Kind), Type)

infer all minimal kinds

rawKindOfType :: Type -> RawKind

extract the raw kind from a type term

lesserType :: Env -> Type -> Type -> Bool

subtyping relation

getMinAssumps :: Env -> Id -> [OpInfo]

get operations by name removing super profiles

idsOf :: (Int -> Bool) -> Type -> Set Id

type identifiers of a type

super type ids

superIds :: TypeMap -> Id -> Set Id

compute super type ids of one type id

supIds :: TypeMap -> Set Id -> Set Id -> Set Id

compute all super type ids for several type ids given as second argument

expand alias types

expand :: TypeMap -> TypeScheme -> TypeScheme

expand aliases in a type scheme

expandAlias :: TypeMap -> Type -> Type

expand aliases in a type and reduce type map first

expandAliases :: TypeMap -> Type -> Type

expand aliases in a type if type map non-null

expandAux :: TypeMap -> Type -> Type

expand aliases in a type

hasAlias :: TypeMap -> Type -> [Diagnosis]

find unexpanded alias identifier

resolve and analyse types

anaTypeM :: (Maybe Kind, Type) -> Env -> Result ((RawKind, Set Kind), Type)

resolve type and infer minimal kinds

anaStarTypeM :: Type -> Env -> Result ((RawKind, Set Kind), Type)

resolve the type and check if it is of the universe class

misc functions on types

cyclicType :: Id -> Type -> Bool

check if an id occurs in a type

unboundTypevars :: Bool -> [TypeArg] -> Type -> [Diagnosis]

check for unbound (or if False for too many) type variables

generalizable :: Bool -> TypeScheme -> [Diagnosis]

check for proper generalizability (False: warn also for unused types)

checkUniqueTypevars :: [TypeArg] -> [Diagnosis]

check uniqueness of type variables