| 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
- 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
getRawKind :: TypeMap -> Id -> RawKind
mkInjOrProjType :: Arrow -> TypeScheme
make a polymorphic function from a to b
mkInjOrProj :: Arrow -> Set OpInfo
subtRelName :: Id
subtAxioms :: TypeMap -> [Named Sentence]
getKindAppl :: RawKind -> [Variance]
xaToZc :: [GenVarDecl]
makeEquivMonos :: Env -> Id -> [TypeScheme] -> [Named Sentence]
mkTypedTerm :: Term -> Type -> Range -> Term
makeEquivMono :: Env -> Id -> TypeScheme -> TypeScheme -> Maybe (Named Sentence)