| Copyright | (c) Till Mossakowski, Christian Maeder and Uni Bremen 2003-2005 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | Christian.Maeder@dfki.de |
| Stability | provisional |
| Portability | non-portable (imports Logic.Logic) |
| Safe Haskell | None |
Comorphisms.CASL2HasCASL
Description
The embedding comorphism from CASL to HasCASL.
- data CASL2HasCASL = CASL2HasCASL
- fromOPTYPE :: OP_TYPE -> Type
- fromOpType :: OpType -> Type
- fromPREDTYPE :: PRED_TYPE -> Type
- fromPredType :: PredType -> Type
- mapTheory :: (TermExtension f, FormExtension f) => (Sign f e, [Named (FORMULA f)]) -> (Env, [Named Sentence])
- mapSig :: Set (Id, OpType) -> Sign f e -> Env
- mapSigAux :: (Id -> Id) -> (OpType -> Type) -> (PredType -> Type) -> Set (Id, OpType) -> Sign f e -> Env
- mapMor :: Morphism f e m -> Morphism
- mapSym :: Symbol -> Symbol
- mapSymAux :: (Id -> Id) -> (OpType -> Type) -> (PredType -> Type) -> Symbol -> Symbol
- toQuant :: QUANTIFIER -> Quantifier
- toVarDecl :: VAR_DECL -> [GenVarDecl]
- toSentence :: (TermExtension f, FormExtension f) => FORMULA f -> Sentence
- toTerm :: (TermExtension f, FormExtension f) => FORMULA f -> Term
- transRecord :: TermExtension f => String -> Record f Term Term
- typeOfTerm :: TermExtension f => TERM f -> Type
- qualName2var :: Id -> Term -> Term
- trId :: Id -> Id
Documentation
fromOPTYPE :: OP_TYPE -> Type
fromOpType :: OpType -> Type
fromPREDTYPE :: PRED_TYPE -> Type
fromPredType :: PredType -> Type
mapTheory :: (TermExtension f, FormExtension f) => (Sign f e, [Named (FORMULA f)]) -> (Env, [Named Sentence])
mapSigAux :: (Id -> Id) -> (OpType -> Type) -> (PredType -> Type) -> Set (Id, OpType) -> Sign f e -> Env
sort names or not translated
toQuant :: QUANTIFIER -> Quantifier
toVarDecl :: VAR_DECL -> [GenVarDecl]
toSentence :: (TermExtension f, FormExtension f) => FORMULA f -> Sentence
toTerm :: (TermExtension f, FormExtension f) => FORMULA f -> Term
transRecord :: TermExtension f => String -> Record f Term Term
typeOfTerm :: TermExtension f => TERM f -> Type
qualName2var :: Id -> Term -> Term
replace qualified names by variables in second order formulas