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.

Synopsis

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

data CASL2HasCASL Source #

The identity of the comorphism

Constructors

CASL2HasCASL

Instances

Instances details

Show CASL2HasCASL Source #
Instance details Defined in Comorphisms.CASL2HasCASL Methods showsPrec :: Int -> CASL2HasCASL -> ShowS show :: CASL2HasCASL -> String showList :: [CASL2HasCASL] -> ShowS
Language CASL2HasCASL Source #
Instance details Defined in Comorphisms.CASL2HasCASL Methods language_name :: CASL2HasCASL -> String Source # description :: CASL2HasCASL -> String Source #
Comorphism CASL2HasCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2HasCASL Methods sourceLogic :: CASL2HasCASL -> CASL Source # sourceSublogic :: CASL2HasCASL -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2HasCASL -> CASL_Sublogics Source # minSourceTheory :: CASL2HasCASL -> Maybe (LibName, String) Source # targetLogic :: CASL2HasCASL -> HasCASL Source # mapSublogic :: CASL2HasCASL -> CASL_Sublogics -> Maybe Sublogic Source # map_theory :: CASL2HasCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: CASL2HasCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (Env, [Named Sentence]) Source # map_morphism :: CASL2HasCASL -> CASLMor -> Result Morphism Source # map_sentence :: CASL2HasCASL -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2HasCASL -> CASLSign -> Symbol0 -> Set Symbol Source # extractModel :: CASL2HasCASL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2HasCASL -> Bool Source # has_model_expansion :: CASL2HasCASL -> Bool Source # is_weakly_amalgamable :: CASL2HasCASL -> Bool Source # constituents :: CASL2HasCASL -> [String] Source # isInclusionComorphism :: CASL2HasCASL -> Bool Source # rps :: CASL2HasCASL -> Bool Source # eps :: CASL2HasCASL -> Bool Source # isGTC :: CASL2HasCASL -> Bool Source #