Hets - the Heterogeneous Tool Set

Copyright	(c) Christian Maeder and Uni Bremen 2003-2005
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	experimental
Portability	portable
Safe Haskell	None

HasCASL.TypeRel

Description

compute subtype dependencies

Synopsis

typeRel :: TypeMap -> Rel Id
getRawKind :: TypeMap -> Id -> RawKind
mkInjOrProjType :: Arrow -> TypeScheme
injType :: TypeScheme
projType :: TypeScheme
mkInjOrProj :: Arrow -> Set OpInfo
subtRelName :: Id
subtRelType :: TypeScheme
subtRel :: Set OpInfo
varRel :: Rel Id -> TypeMap -> Rel Id
subtAxioms :: TypeMap -> [Named Sentence]
nr :: Range
getKindAppl :: RawKind -> [Variance]
mkTypeArg :: Id -> Int -> TypeArg
subtAx :: TypeMap -> (Id, Id) -> Named Sentence
mkSubtTerm :: Type -> Type -> VarDecl -> VarDecl -> Term
subtReflex :: Named Sentence
xa :: VarDecl
yb :: VarDecl
zc :: VarDecl
xaToZc :: [GenVarDecl]
subtTrans :: Named Sentence
mkInjTerm :: Type -> Type -> Term -> Term
mkInjEq :: Type -> Type -> VarDecl -> VarDecl -> Term
subtInjProj :: Named Sentence
injTrans :: Named Sentence
idInj :: Named Sentence
monos :: Env -> [Named Sentence]
makeMonos :: Env -> (Id, Set OpInfo) -> [Named Sentence]
makeEquivMonos :: Env -> Id -> [TypeScheme] -> [Named Sentence]
mkTypedTerm :: Term -> Type -> Range -> Term
mkTypedEqTerm :: Id -> Type -> Range -> Term -> Term -> Term
makeEquivMono :: Env -> Id -> TypeScheme -> TypeScheme -> Maybe (Named Sentence)

Documentation

typeRel :: TypeMap -> Rel Id Source #

getRawKind :: TypeMap -> Id -> RawKind Source #

mkInjOrProjType :: Arrow -> TypeScheme Source #

make a polymorphic function from a to b

injType :: TypeScheme Source #

projType :: TypeScheme Source #

mkInjOrProj :: Arrow -> Set OpInfo Source #

subtRelName :: Id Source #

subtRelType :: TypeScheme Source #

subtRel :: Set OpInfo Source #

varRel :: Rel Id -> TypeMap -> Rel Id Source #

subtAxioms :: TypeMap -> [Named Sentence] Source #

nr :: Range Source #

getKindAppl :: RawKind -> [Variance] Source #

mkTypeArg :: Id -> Int -> TypeArg Source #

subtAx :: TypeMap -> (Id, Id) -> Named Sentence Source #

mkSubtTerm :: Type -> Type -> VarDecl -> VarDecl -> Term Source #

subtReflex :: Named Sentence Source #

xa :: VarDecl Source #

yb :: VarDecl Source #

zc :: VarDecl Source #

xaToZc :: [GenVarDecl] Source #

subtTrans :: Named Sentence Source #

mkInjTerm :: Type -> Type -> Term -> Term Source #

mkInjEq :: Type -> Type -> VarDecl -> VarDecl -> Term Source #

subtInjProj :: Named Sentence Source #

injTrans :: Named Sentence Source #

idInj :: Named Sentence Source #

monos :: Env -> [Named Sentence] Source #

makeMonos :: Env -> (Id, Set OpInfo) -> [Named Sentence] Source #

makeEquivMonos :: Env -> Id -> [TypeScheme] -> [Named Sentence] Source #

mkTypedTerm :: Term -> Type -> Range -> Term Source #

mkTypedEqTerm :: Id -> Type -> Range -> Term -> Term -> Term Source #

makeEquivMono :: Env -> Id -> TypeScheme -> TypeScheme -> Maybe (Named Sentence) Source #