Copyright	(c) Till Mossakowski Uni Bremen 2002-2006
License	GPLv2 or higher, see LICENSE.txt
Maintainer	till@informatik.uni-bremen.de
Stability	provisional
Portability	non-portable (via Logic)
Safe Haskell	None

Logic.Comorphism

Description

Central interface (type class) for logic translations (comorphisms) in Hets These are just collections of functions between (some of) the types of logics.

References: see Logic.hs

Synopsis

data CompComorphism cid1 cid2 = CompComorphism cid1 cid2
data InclComorphism lid sublogics
inclusion_logic :: InclComorphism lid sublogics -> lid
inclusion_source_sublogic :: InclComorphism lid sublogics -> sublogics
inclusion_target_sublogic :: InclComorphism lid sublogics -> sublogics
mkInclComorphism :: (Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree, MonadFail m) => lid -> sublogics -> sublogics -> m (InclComorphism lid sublogics)
mkIdComorphism :: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> sublogics -> InclComorphism lid sublogics
class (Language cid, Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1, Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2) => Comorphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 | cid -> lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 where
- sourceLogic :: cid -> lid1
- sourceSublogic :: cid -> sublogics1
- sourceSublogicLossy :: cid -> sublogics1
- minSourceTheory :: cid -> Maybe (LibName, String)
- targetLogic :: cid -> lid2
- mapSublogic :: cid -> sublogics1 -> Maybe sublogics2
- map_theory :: cid -> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
- mapMarkedTheory :: cid -> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
- map_morphism :: cid -> morphism1 -> Result morphism2
- map_sentence :: cid -> sign1 -> sentence1 -> Result sentence2
- map_symbol :: cid -> sign1 -> symbol1 -> Set symbol2
- extractModel :: cid -> sign1 -> proof_tree2 -> Result (sign1, [Named sentence1])
- is_model_transportable :: cid -> Bool
- has_model_expansion :: cid -> Bool
- is_weakly_amalgamable :: cid -> Bool
- constituents :: cid -> [String]
- isInclusionComorphism :: cid -> Bool
- rps :: cid -> Bool
- eps :: cid -> Bool
- isGTC :: cid -> Bool
targetSublogic :: Comorphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 => cid -> sublogics2
map_sign :: Comorphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 => cid -> sign1 -> Result (sign2, [Named sentence2])
wrapMapTheory :: Comorphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 => cid -> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
wrapMapTheoryPossiblyLossy :: Comorphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 => Bool -> cid -> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
mkTheoryMapping :: Monad m => (sign1 -> m (sign2, [Named sentence2])) -> (sign1 -> sentence1 -> m sentence2) -> (sign1, [Named sentence1]) -> m (sign2, [Named sentence2])
data AnyComorphism = forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2.Comorphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 => Comorphism cid
idComorphism :: AnyLogic -> AnyComorphism
isIdComorphism :: AnyComorphism -> Bool
isModelTransportable :: AnyComorphism -> Bool
hasModelExpansion :: AnyComorphism -> Bool
isEps :: AnyComorphism -> Bool
isRps :: AnyComorphism -> Bool
isWeaklyAmalgamable :: AnyComorphism -> Bool
compComorphism :: MonadFail m => AnyComorphism -> AnyComorphism -> m AnyComorphism

Documentation

data CompComorphism cid1 cid2 Source #

Constructors

CompComorphism cid1 cid2

Instances

Instances details

Modification MODAL_EMBEDDING (InclComorphism CASL CASL_Sublogics) (CompComorphism CASL2Modal Modal2CASL) CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Modifications.ModalEmbedding Methods tauSigma :: MODAL_EMBEDDING -> CASLSign -> Result CASLMor Source # sourceComorphism :: MODAL_EMBEDDING -> InclComorphism CASL CASL_Sublogics Source # targetComorphism :: MODAL_EMBEDDING -> CompComorphism CASL2Modal Modal2CASL Source #
(Data cid1, Data cid2) => Data (CompComorphism cid1 cid2) Source #
Instance details Defined in Logic.Comorphism Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CompComorphism cid1 cid2 -> c (CompComorphism cid1 cid2) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (CompComorphism cid1 cid2) toConstr :: CompComorphism cid1 cid2 -> Constr dataTypeOf :: CompComorphism cid1 cid2 -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (CompComorphism cid1 cid2)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (CompComorphism cid1 cid2)) gmapT :: (forall b. Data b => b -> b) -> CompComorphism cid1 cid2 -> CompComorphism cid1 cid2 gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CompComorphism cid1 cid2 -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CompComorphism cid1 cid2 -> r gmapQ :: (forall d. Data d => d -> u) -> CompComorphism cid1 cid2 -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> CompComorphism cid1 cid2 -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> CompComorphism cid1 cid2 -> m (CompComorphism cid1 cid2) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CompComorphism cid1 cid2 -> m (CompComorphism cid1 cid2) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CompComorphism cid1 cid2 -> m (CompComorphism cid1 cid2)
(Show cid1, Show cid2) => Show (CompComorphism cid1 cid2) Source #
Instance details Defined in Logic.Comorphism Methods showsPrec :: Int -> CompComorphism cid1 cid2 -> ShowS show :: CompComorphism cid1 cid2 -> String showList :: [CompComorphism cid1 cid2] -> ShowS
(Language cid1, Language cid2) => Language (CompComorphism cid1 cid2) Source #
Instance details Defined in Logic.Comorphism Methods language_name :: CompComorphism cid1 cid2 -> String Source # description :: CompComorphism cid1 cid2 -> String Source #
(Comorphism cid1 lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2, Comorphism cid2 lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4 sign4 morphism4 symbol4 raw_symbol4 proof_tree4 lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3 sign3 morphism3 symbol3 raw_symbol3 proof_tree3) => Comorphism (CompComorphism cid1 cid2) lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3 sign3 morphism3 symbol3 raw_symbol3 proof_tree3 Source #
Instance details Defined in Logic.Comorphism Methods sourceLogic :: CompComorphism cid1 cid2 -> lid1 Source # sourceSublogic :: CompComorphism cid1 cid2 -> sublogics1 Source # sourceSublogicLossy :: CompComorphism cid1 cid2 -> sublogics1 Source # minSourceTheory :: CompComorphism cid1 cid2 -> Maybe (LibName, String) Source # targetLogic :: CompComorphism cid1 cid2 -> lid3 Source # mapSublogic :: CompComorphism cid1 cid2 -> sublogics1 -> Maybe sublogics3 Source # map_theory :: CompComorphism cid1 cid2 -> (sign1, [Named sentence1]) -> Result (sign3, [Named sentence3]) Source # mapMarkedTheory :: CompComorphism cid1 cid2 -> (sign1, [Named sentence1]) -> Result (sign3, [Named sentence3]) Source # map_morphism :: CompComorphism cid1 cid2 -> morphism1 -> Result morphism3 Source # map_sentence :: CompComorphism cid1 cid2 -> sign1 -> sentence1 -> Result sentence3 Source # map_symbol :: CompComorphism cid1 cid2 -> sign1 -> symbol1 -> Set symbol3 Source # extractModel :: CompComorphism cid1 cid2 -> sign1 -> proof_tree3 -> Result (sign1, [Named sentence1]) Source # is_model_transportable :: CompComorphism cid1 cid2 -> Bool Source # has_model_expansion :: CompComorphism cid1 cid2 -> Bool Source # is_weakly_amalgamable :: CompComorphism cid1 cid2 -> Bool Source # constituents :: CompComorphism cid1 cid2 -> [String] Source # isInclusionComorphism :: CompComorphism cid1 cid2 -> Bool Source # rps :: CompComorphism cid1 cid2 -> Bool Source # eps :: CompComorphism cid1 cid2 -> Bool Source # isGTC :: CompComorphism cid1 cid2 -> Bool Source #
(Modification lid1 cid1 cid2 log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3 sign3 morphism3 symbol3 raw_symbol3 proof_tree3 log4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4 sign4 morphism4 symbol4 raw_symbol4 proof_tree4, Modification lid2 cid3 cid4 log5 sublogics5 basic_spec5 sentence5 symb_items5 symb_map_items5 sign5 morphism5 symbol5 raw_symbol5 proof_tree5 log6 sublogics6 basic_spec6 sentence6 symb_items6 symb_map_items6 sign6 morphism6 symbol6 raw_symbol6 proof_tree6 log7 sublogics7 basic_spec7 sentence7 symb_items7 symb_map_items7 sign7 morphism7 symbol7 raw_symbol7 proof_tree7 log8 sublogics8 basic_spec8 sentence8 symb_items8 symb_map_items8 sign8 morphism8 symbol8 raw_symbol8 proof_tree8, Comorphism (CompComorphism cid1 cid3) log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 log6 sublogics6 basic_spec6 sentence6 symb_items6 symb_map_items6 sign6 morphism6 symbol6 raw_symbol6 proof_tree6, Comorphism (CompComorphism cid2 cid4) log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3 sign3 morphism3 symbol3 raw_symbol3 proof_tree3 log8 sublogics8 basic_spec8 sentence8 symb_items8 symb_map_items8 sign8 morphism8 symbol8 raw_symbol8 proof_tree8) => Modification (HorCompModif lid1 lid2) (CompComorphism cid1 cid3) (CompComorphism cid2 cid4) log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 log6 sublogics6 basic_spec6 sentence6 symb_items6 symb_map_items6 sign6 morphism6 symbol6 raw_symbol6 proof_tree6 log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3 sign3 morphism3 symbol3 raw_symbol3 proof_tree3 log8 sublogics8 basic_spec8 sentence8 symb_items8 symb_map_items8 sign8 morphism8 symbol8 raw_symbol8 proof_tree8 Source #
Instance details Defined in Logic.Modification Methods tauSigma :: HorCompModif lid1 lid2 -> sign1 -> Result morphism6 Source # sourceComorphism :: HorCompModif lid1 lid2 -> CompComorphism cid1 cid3 Source # targetComorphism :: HorCompModif lid1 lid2 -> CompComorphism cid2 cid4 Source #

data InclComorphism lid sublogics Source #

Instances

Instances details

Modification MODAL_EMBEDDING (InclComorphism CASL CASL_Sublogics) (CompComorphism CASL2Modal Modal2CASL) CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Modifications.ModalEmbedding Methods tauSigma :: MODAL_EMBEDDING -> CASLSign -> Result CASLMor Source # sourceComorphism :: MODAL_EMBEDDING -> InclComorphism CASL CASL_Sublogics Source # targetComorphism :: MODAL_EMBEDDING -> CompComorphism CASL2Modal Modal2CASL Source #
(Data lid, Data sublogics) => Data (InclComorphism lid sublogics) Source #
Instance details Defined in Logic.Comorphism Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> InclComorphism lid sublogics -> c (InclComorphism lid sublogics) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (InclComorphism lid sublogics) toConstr :: InclComorphism lid sublogics -> Constr dataTypeOf :: InclComorphism lid sublogics -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (InclComorphism lid sublogics)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (InclComorphism lid sublogics)) gmapT :: (forall b. Data b => b -> b) -> InclComorphism lid sublogics -> InclComorphism lid sublogics gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> InclComorphism lid sublogics -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> InclComorphism lid sublogics -> r gmapQ :: (forall d. Data d => d -> u) -> InclComorphism lid sublogics -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> InclComorphism lid sublogics -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> InclComorphism lid sublogics -> m (InclComorphism lid sublogics) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> InclComorphism lid sublogics -> m (InclComorphism lid sublogics) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> InclComorphism lid sublogics -> m (InclComorphism lid sublogics)
(Show lid, Show sublogics) => Show (InclComorphism lid sublogics) Source #
Instance details Defined in Logic.Comorphism Methods showsPrec :: Int -> InclComorphism lid sublogics -> ShowS show :: InclComorphism lid sublogics -> String showList :: [InclComorphism lid sublogics] -> ShowS
(Language lid, Eq sublogics, Show sublogics, SublogicName sublogics) => Language (InclComorphism lid sublogics) Source #
Instance details Defined in Logic.Comorphism Methods language_name :: InclComorphism lid sublogics -> String Source # description :: InclComorphism lid sublogics -> String Source #
Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => Comorphism (InclComorphism lid sublogics) lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree Source #
Instance details Defined in Logic.Comorphism Methods sourceLogic :: InclComorphism lid sublogics -> lid Source # sourceSublogic :: InclComorphism lid sublogics -> sublogics Source # sourceSublogicLossy :: InclComorphism lid sublogics -> sublogics Source # minSourceTheory :: InclComorphism lid sublogics -> Maybe (LibName, String) Source # targetLogic :: InclComorphism lid sublogics -> lid Source # mapSublogic :: InclComorphism lid sublogics -> sublogics -> Maybe sublogics Source # map_theory :: InclComorphism lid sublogics -> (sign, [Named sentence]) -> Result (sign, [Named sentence]) Source # mapMarkedTheory :: InclComorphism lid sublogics -> (sign, [Named sentence]) -> Result (sign, [Named sentence]) Source # map_morphism :: InclComorphism lid sublogics -> morphism -> Result morphism Source # map_sentence :: InclComorphism lid sublogics -> sign -> sentence -> Result sentence Source # map_symbol :: InclComorphism lid sublogics -> sign -> symbol -> Set symbol Source # extractModel :: InclComorphism lid sublogics -> sign -> proof_tree -> Result (sign, [Named sentence]) Source # is_model_transportable :: InclComorphism lid sublogics -> Bool Source # has_model_expansion :: InclComorphism lid sublogics -> Bool Source # is_weakly_amalgamable :: InclComorphism lid sublogics -> Bool Source # constituents :: InclComorphism lid sublogics -> [String] Source # isInclusionComorphism :: InclComorphism lid sublogics -> Bool Source # rps :: InclComorphism lid sublogics -> Bool Source # eps :: InclComorphism lid sublogics -> Bool Source # isGTC :: InclComorphism lid sublogics -> Bool Source #

inclusion_logic :: InclComorphism lid sublogics -> lid Source #

inclusion_source_sublogic :: InclComorphism lid sublogics -> sublogics Source #

inclusion_target_sublogic :: InclComorphism lid sublogics -> sublogics Source #

mkInclComorphism :: (Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree, MonadFail m) => lid -> sublogics -> sublogics -> m (InclComorphism lid sublogics) Source #

construction of an inclusion comorphism

mkIdComorphism :: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> sublogics -> InclComorphism lid sublogics Source #

construction of an identity comorphism

class (Language cid, Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1, Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2) => Comorphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 | cid -> lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 where Source #

Minimal complete definition

sourceLogic, targetLogic, map_theory

Methods

sourceLogic :: cid -> lid1 Source #

sourceSublogic :: cid -> sublogics1 Source #

sourceSublogicLossy :: cid -> sublogics1 Source #

minSourceTheory :: cid -> Maybe (LibName, String) Source #

targetLogic :: cid -> lid2 Source #

mapSublogic :: cid -> sublogics1 -> Maybe sublogics2 Source #

map_theory :: cid -> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2]) Source #

mapMarkedTheory :: cid -> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2]) Source #

map_morphism :: cid -> morphism1 -> Result morphism2 Source #

map_sentence :: cid -> sign1 -> sentence1 -> Result sentence2 Source #

map_symbol :: cid -> sign1 -> symbol1 -> Set symbol2 Source #

extractModel :: cid -> sign1 -> proof_tree2 -> Result (sign1, [Named sentence1]) Source #

is_model_transportable :: cid -> Bool Source #

has_model_expansion :: cid -> Bool Source #

is_weakly_amalgamable :: cid -> Bool Source #

constituents :: cid -> [String] Source #

isInclusionComorphism :: cid -> Bool Source #

rps :: cid -> Bool Source #

eps :: cid -> Bool Source #

isGTC :: cid -> Bool Source #

Instances

Instances details

Comorphism Propositional2OWL2 Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree Source #
Instance details Defined in OWL2.Propositional2OWL2 Methods sourceLogic :: Propositional2OWL2 -> Propositional Source # sourceSublogic :: Propositional2OWL2 -> PropSL Source # sourceSublogicLossy :: Propositional2OWL2 -> PropSL Source # minSourceTheory :: Propositional2OWL2 -> Maybe (LibName, String) Source # targetLogic :: Propositional2OWL2 -> OWL2 Source # mapSublogic :: Propositional2OWL2 -> PropSL -> Maybe ProfSub Source # map_theory :: Propositional2OWL2 -> (Sign, [Named FORMULA]) -> Result (Sign0, [Named Axiom]) Source # mapMarkedTheory :: Propositional2OWL2 -> (Sign, [Named FORMULA]) -> Result (Sign0, [Named Axiom]) Source # map_morphism :: Propositional2OWL2 -> Morphism -> Result OWLMorphism Source # map_sentence :: Propositional2OWL2 -> Sign -> FORMULA -> Result Axiom Source # map_symbol :: Propositional2OWL2 -> Sign -> Symbol -> Set Entity Source # extractModel :: Propositional2OWL2 -> Sign -> ProofTree -> Result (Sign, [Named FORMULA]) Source # is_model_transportable :: Propositional2OWL2 -> Bool Source # has_model_expansion :: Propositional2OWL2 -> Bool Source # is_weakly_amalgamable :: Propositional2OWL2 -> Bool Source # constituents :: Propositional2OWL2 -> [String] Source # isInclusionComorphism :: Propositional2OWL2 -> Bool Source # rps :: Propositional2OWL2 -> Bool Source # eps :: Propositional2OWL2 -> Bool Source # isGTC :: Propositional2OWL2 -> Bool Source #
Comorphism OWL22NeSyPatterns OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree NeSyPatterns () BASIC_SPEC () SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source #
Instance details Defined in OWL2.OWL22NeSyPatterns Methods sourceLogic :: OWL22NeSyPatterns -> OWL2 Source # sourceSublogic :: OWL22NeSyPatterns -> ProfSub Source # sourceSublogicLossy :: OWL22NeSyPatterns -> ProfSub Source # minSourceTheory :: OWL22NeSyPatterns -> Maybe (LibName, String) Source # targetLogic :: OWL22NeSyPatterns -> NeSyPatterns Source # mapSublogic :: OWL22NeSyPatterns -> ProfSub -> Maybe () Source # map_theory :: OWL22NeSyPatterns -> (Sign0, [Named Axiom]) -> Result (Sign, [Named ()]) Source # mapMarkedTheory :: OWL22NeSyPatterns -> (Sign0, [Named Axiom]) -> Result (Sign, [Named ()]) Source # map_morphism :: OWL22NeSyPatterns -> OWLMorphism -> Result Morphism Source # map_sentence :: OWL22NeSyPatterns -> Sign0 -> Axiom -> Result () Source # map_symbol :: OWL22NeSyPatterns -> Sign0 -> Entity -> Set Symbol Source # extractModel :: OWL22NeSyPatterns -> Sign0 -> ProofTree -> Result (Sign0, [Named Axiom]) Source # is_model_transportable :: OWL22NeSyPatterns -> Bool Source # has_model_expansion :: OWL22NeSyPatterns -> Bool Source # is_weakly_amalgamable :: OWL22NeSyPatterns -> Bool Source # constituents :: OWL22NeSyPatterns -> [String] Source # isInclusionComorphism :: OWL22NeSyPatterns -> Bool Source # rps :: OWL22NeSyPatterns -> Bool Source # eps :: OWL22NeSyPatterns -> Bool Source # isGTC :: OWL22NeSyPatterns -> Bool Source #
Comorphism THFP_P2THFP THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source #
Instance details Defined in Comorphisms.THFP_P2THFP Methods sourceLogic :: THFP_P2THFP -> THF Source # sourceSublogic :: THFP_P2THFP -> THFSl Source # sourceSublogicLossy :: THFP_P2THFP -> THFSl Source # minSourceTheory :: THFP_P2THFP -> Maybe (LibName, String) Source # targetLogic :: THFP_P2THFP -> THF Source # mapSublogic :: THFP_P2THFP -> THFSl -> Maybe THFSl Source # map_theory :: THFP_P2THFP -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source # mapMarkedTheory :: THFP_P2THFP -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source # map_morphism :: THFP_P2THFP -> MorphismTHF -> Result MorphismTHF Source # map_sentence :: THFP_P2THFP -> SignTHF -> THFFormula -> Result THFFormula Source # map_symbol :: THFP_P2THFP -> SignTHF -> SymbolTHF -> Set SymbolTHF Source # extractModel :: THFP_P2THFP -> SignTHF -> ProofTree -> Result (SignTHF, [Named THFFormula]) Source # is_model_transportable :: THFP_P2THFP -> Bool Source # has_model_expansion :: THFP_P2THFP -> Bool Source # is_weakly_amalgamable :: THFP_P2THFP -> Bool Source # constituents :: THFP_P2THFP -> [String] Source # isInclusionComorphism :: THFP_P2THFP -> Bool Source # rps :: THFP_P2THFP -> Bool Source # eps :: THFP_P2THFP -> Bool Source # isGTC :: THFP_P2THFP -> Bool Source #
Comorphism THFP_P2HasCASL THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.THFP_P2HasCASL Methods sourceLogic :: THFP_P2HasCASL -> THF Source # sourceSublogic :: THFP_P2HasCASL -> THFSl Source # sourceSublogicLossy :: THFP_P2HasCASL -> THFSl Source # minSourceTheory :: THFP_P2HasCASL -> Maybe (LibName, String) Source # targetLogic :: THFP_P2HasCASL -> HasCASL Source # mapSublogic :: THFP_P2HasCASL -> THFSl -> Maybe Sublogic Source # map_theory :: THFP_P2HasCASL -> (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: THFP_P2HasCASL -> (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence]) Source # map_morphism :: THFP_P2HasCASL -> MorphismTHF -> Result Morphism Source # map_sentence :: THFP_P2HasCASL -> SignTHF -> THFFormula -> Result Sentence Source # map_symbol :: THFP_P2HasCASL -> SignTHF -> SymbolTHF -> Set Symbol Source # extractModel :: THFP_P2HasCASL -> SignTHF -> () -> Result (SignTHF, [Named THFFormula]) Source # is_model_transportable :: THFP_P2HasCASL -> Bool Source # has_model_expansion :: THFP_P2HasCASL -> Bool Source # is_weakly_amalgamable :: THFP_P2HasCASL -> Bool Source # constituents :: THFP_P2HasCASL -> [String] Source # isInclusionComorphism :: THFP_P2HasCASL -> Bool Source # rps :: THFP_P2HasCASL -> Bool Source # eps :: THFP_P2HasCASL -> Bool Source # isGTC :: THFP_P2HasCASL -> Bool Source #
Comorphism THFP2THF0 THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source #
Instance details Defined in Comorphisms.THFP2THF0 Methods sourceLogic :: THFP2THF0 -> THF Source # sourceSublogic :: THFP2THF0 -> THFSl Source # sourceSublogicLossy :: THFP2THF0 -> THFSl Source # minSourceTheory :: THFP2THF0 -> Maybe (LibName, String) Source # targetLogic :: THFP2THF0 -> THF Source # mapSublogic :: THFP2THF0 -> THFSl -> Maybe THFSl Source # map_theory :: THFP2THF0 -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source # mapMarkedTheory :: THFP2THF0 -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source # map_morphism :: THFP2THF0 -> MorphismTHF -> Result MorphismTHF Source # map_sentence :: THFP2THF0 -> SignTHF -> THFFormula -> Result THFFormula Source # map_symbol :: THFP2THF0 -> SignTHF -> SymbolTHF -> Set SymbolTHF Source # extractModel :: THFP2THF0 -> SignTHF -> ProofTree -> Result (SignTHF, [Named THFFormula]) Source # is_model_transportable :: THFP2THF0 -> Bool Source # has_model_expansion :: THFP2THF0 -> Bool Source # is_weakly_amalgamable :: THFP2THF0 -> Bool Source # constituents :: THFP2THF0 -> [String] Source # isInclusionComorphism :: THFP2THF0 -> Bool Source # rps :: THFP2THF0 -> Bool Source # eps :: THFP2THF0 -> Bool Source # isGTC :: THFP2THF0 -> Bool Source #
Comorphism QBF2Prop QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source #
Instance details Defined in Comorphisms.QBF2Prop Methods sourceLogic :: QBF2Prop -> QBF Source # sourceSublogic :: QBF2Prop -> QBFSL Source # sourceSublogicLossy :: QBF2Prop -> QBFSL Source # minSourceTheory :: QBF2Prop -> Maybe (LibName, String) Source # targetLogic :: QBF2Prop -> Propositional Source # mapSublogic :: QBF2Prop -> QBFSL -> Maybe PropSL Source # map_theory :: QBF2Prop -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA0]) Source # mapMarkedTheory :: QBF2Prop -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA0]) Source # map_morphism :: QBF2Prop -> Morphism -> Result Morphism0 Source # map_sentence :: QBF2Prop -> Sign -> FORMULA -> Result FORMULA0 Source # map_symbol :: QBF2Prop -> Sign -> Symbol -> Set Symbol0 Source # extractModel :: QBF2Prop -> Sign -> ProofTree -> Result (Sign, [Named FORMULA]) Source # is_model_transportable :: QBF2Prop -> Bool Source # has_model_expansion :: QBF2Prop -> Bool Source # is_weakly_amalgamable :: QBF2Prop -> Bool Source # constituents :: QBF2Prop -> [String] Source # isInclusionComorphism :: QBF2Prop -> Bool Source # rps :: QBF2Prop -> Bool Source # eps :: QBF2Prop -> Bool Source # isGTC :: QBF2Prop -> Bool Source #
Comorphism Prop2QBF Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree Source #
Instance details Defined in Comorphisms.Prop2QBF Methods sourceLogic :: Prop2QBF -> Propositional Source # sourceSublogic :: Prop2QBF -> PropSL Source # sourceSublogicLossy :: Prop2QBF -> PropSL Source # minSourceTheory :: Prop2QBF -> Maybe (LibName, String) Source # targetLogic :: Prop2QBF -> QBF Source # mapSublogic :: Prop2QBF -> PropSL -> Maybe QBFSL Source # map_theory :: Prop2QBF -> (Sign, [Named FORMULA0]) -> Result (Sign, [Named FORMULA]) Source # mapMarkedTheory :: Prop2QBF -> (Sign, [Named FORMULA0]) -> Result (Sign, [Named FORMULA]) Source # map_morphism :: Prop2QBF -> Morphism0 -> Result Morphism Source # map_sentence :: Prop2QBF -> Sign -> FORMULA0 -> Result FORMULA Source # map_symbol :: Prop2QBF -> Sign -> Symbol0 -> Set Symbol Source # extractModel :: Prop2QBF -> Sign -> ProofTree -> Result (Sign, [Named FORMULA0]) Source # is_model_transportable :: Prop2QBF -> Bool Source # has_model_expansion :: Prop2QBF -> Bool Source # is_weakly_amalgamable :: Prop2QBF -> Bool Source # constituents :: Prop2QBF -> [String] Source # isInclusionComorphism :: Prop2QBF -> Bool Source # rps :: Prop2QBF -> Bool Source # eps :: Prop2QBF -> Bool Source # isGTC :: Prop2QBF -> Bool Source #
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.PCoClTyConsHOL2PairsInIsaHOL Methods sourceLogic :: PCoClTyConsHOL2PairsInIsaHOL -> HasCASL Source # sourceSublogic :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic Source # sourceSublogicLossy :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic Source # minSourceTheory :: PCoClTyConsHOL2PairsInIsaHOL -> Maybe (LibName, String) Source # targetLogic :: PCoClTyConsHOL2PairsInIsaHOL -> Isabelle Source # mapSublogic :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic -> Maybe () Source # map_theory :: PCoClTyConsHOL2PairsInIsaHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: PCoClTyConsHOL2PairsInIsaHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: PCoClTyConsHOL2PairsInIsaHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Symbol -> Set () Source # extractModel :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # has_model_expansion :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # is_weakly_amalgamable :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # constituents :: PCoClTyConsHOL2PairsInIsaHOL -> [String] Source # isInclusionComorphism :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # rps :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # eps :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # isGTC :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source #
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.PCoClTyConsHOL2IsabelleHOL Methods sourceLogic :: PCoClTyConsHOL2IsabelleHOL -> HasCASL Source # sourceSublogic :: PCoClTyConsHOL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: PCoClTyConsHOL2IsabelleHOL -> Sublogic Source # minSourceTheory :: PCoClTyConsHOL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: PCoClTyConsHOL2IsabelleHOL -> Isabelle Source # mapSublogic :: PCoClTyConsHOL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: PCoClTyConsHOL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: PCoClTyConsHOL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: PCoClTyConsHOL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: PCoClTyConsHOL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: PCoClTyConsHOL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: PCoClTyConsHOL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # has_model_expansion :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # constituents :: PCoClTyConsHOL2IsabelleHOL -> [String] Source # isInclusionComorphism :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # rps :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # eps :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # isGTC :: PCoClTyConsHOL2IsabelleHOL -> Bool Source #
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.MonadicHasCASLTranslation Methods sourceLogic :: MonadicHasCASL2IsabelleHOL -> HasCASL Source # sourceSublogic :: MonadicHasCASL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: MonadicHasCASL2IsabelleHOL -> Sublogic Source # minSourceTheory :: MonadicHasCASL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: MonadicHasCASL2IsabelleHOL -> Isabelle Source # mapSublogic :: MonadicHasCASL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: MonadicHasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: MonadicHasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: MonadicHasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: MonadicHasCASL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: MonadicHasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: MonadicHasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: MonadicHasCASL2IsabelleHOL -> Bool Source # has_model_expansion :: MonadicHasCASL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: MonadicHasCASL2IsabelleHOL -> Bool Source # constituents :: MonadicHasCASL2IsabelleHOL -> [String] Source # isInclusionComorphism :: MonadicHasCASL2IsabelleHOL -> Bool Source # rps :: MonadicHasCASL2IsabelleHOL -> Bool Source # eps :: MonadicHasCASL2IsabelleHOL -> Bool Source # isGTC :: MonadicHasCASL2IsabelleHOL -> Bool Source #
Comorphism HolLight2Isabelle HolLight HolLightSL () Sentence () () Sign HolLightMorphism () () () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.HolLight2Isabelle Methods sourceLogic :: HolLight2Isabelle -> HolLight Source # sourceSublogic :: HolLight2Isabelle -> HolLightSL Source # sourceSublogicLossy :: HolLight2Isabelle -> HolLightSL Source # minSourceTheory :: HolLight2Isabelle -> Maybe (LibName, String) Source # targetLogic :: HolLight2Isabelle -> Isabelle Source # mapSublogic :: HolLight2Isabelle -> HolLightSL -> Maybe () Source # map_theory :: HolLight2Isabelle -> (Sign0, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: HolLight2Isabelle -> (Sign0, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: HolLight2Isabelle -> HolLightMorphism -> Result IsabelleMorphism Source # map_sentence :: HolLight2Isabelle -> Sign0 -> Sentence0 -> Result Sentence Source # map_symbol :: HolLight2Isabelle -> Sign0 -> () -> Set () Source # extractModel :: HolLight2Isabelle -> Sign0 -> () -> Result (Sign0, [Named Sentence0]) Source # is_model_transportable :: HolLight2Isabelle -> Bool Source # has_model_expansion :: HolLight2Isabelle -> Bool Source # is_weakly_amalgamable :: HolLight2Isabelle -> Bool Source # constituents :: HolLight2Isabelle -> [String] Source # isInclusionComorphism :: HolLight2Isabelle -> Bool Source # rps :: HolLight2Isabelle -> Bool Source # eps :: HolLight2Isabelle -> Bool Source # isGTC :: HolLight2Isabelle -> Bool Source #
Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source #
Instance details Defined in Comorphisms.HasCASL2THFP_P Methods sourceLogic :: HasCASL2THFP_P -> HasCASL Source # sourceSublogic :: HasCASL2THFP_P -> Sublogic Source # sourceSublogicLossy :: HasCASL2THFP_P -> Sublogic Source # minSourceTheory :: HasCASL2THFP_P -> Maybe (LibName, String) Source # targetLogic :: HasCASL2THFP_P -> THF Source # mapSublogic :: HasCASL2THFP_P -> Sublogic -> Maybe THFSl Source # map_theory :: HasCASL2THFP_P -> (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula]) Source # mapMarkedTheory :: HasCASL2THFP_P -> (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula]) Source # map_morphism :: HasCASL2THFP_P -> Morphism -> Result MorphismTHF Source # map_sentence :: HasCASL2THFP_P -> Env -> Sentence -> Result THFFormula Source # map_symbol :: HasCASL2THFP_P -> Env -> Symbol -> Set SymbolTHF Source # extractModel :: HasCASL2THFP_P -> Env -> ProofTree -> Result (Env, [Named Sentence]) Source # is_model_transportable :: HasCASL2THFP_P -> Bool Source # has_model_expansion :: HasCASL2THFP_P -> Bool Source # is_weakly_amalgamable :: HasCASL2THFP_P -> Bool Source # constituents :: HasCASL2THFP_P -> [String] Source # isInclusionComorphism :: HasCASL2THFP_P -> Bool Source # rps :: HasCASL2THFP_P -> Bool Source # eps :: HasCASL2THFP_P -> Bool Source # isGTC :: HasCASL2THFP_P -> Bool Source #
Comorphism HasCASL2PCoClTyConsHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.HasCASL2PCoClTyConsHOL Methods sourceLogic :: HasCASL2PCoClTyConsHOL -> HasCASL Source # sourceSublogic :: HasCASL2PCoClTyConsHOL -> Sublogic Source # sourceSublogicLossy :: HasCASL2PCoClTyConsHOL -> Sublogic Source # minSourceTheory :: HasCASL2PCoClTyConsHOL -> Maybe (LibName, String) Source # targetLogic :: HasCASL2PCoClTyConsHOL -> HasCASL Source # mapSublogic :: HasCASL2PCoClTyConsHOL -> Sublogic -> Maybe Sublogic Source # map_theory :: HasCASL2PCoClTyConsHOL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2PCoClTyConsHOL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # map_morphism :: HasCASL2PCoClTyConsHOL -> Morphism -> Result Morphism Source # map_sentence :: HasCASL2PCoClTyConsHOL -> Env -> Sentence -> Result Sentence Source # map_symbol :: HasCASL2PCoClTyConsHOL -> Env -> Symbol -> Set Symbol Source # extractModel :: HasCASL2PCoClTyConsHOL -> Env -> () -> Result (Env, [Named Sentence]) Source # is_model_transportable :: HasCASL2PCoClTyConsHOL -> Bool Source # has_model_expansion :: HasCASL2PCoClTyConsHOL -> Bool Source # is_weakly_amalgamable :: HasCASL2PCoClTyConsHOL -> Bool Source # constituents :: HasCASL2PCoClTyConsHOL -> [String] Source # isInclusionComorphism :: HasCASL2PCoClTyConsHOL -> Bool Source # rps :: HasCASL2PCoClTyConsHOL -> Bool Source # eps :: HasCASL2PCoClTyConsHOL -> Bool Source # isGTC :: HasCASL2PCoClTyConsHOL -> Bool Source #
Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.HasCASL2IsabelleHOL Methods sourceLogic :: HasCASL2IsabelleHOL -> HasCASL Source # sourceSublogic :: HasCASL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: HasCASL2IsabelleHOL -> Sublogic Source # minSourceTheory :: HasCASL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: HasCASL2IsabelleHOL -> Isabelle Source # mapSublogic :: HasCASL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: HasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: HasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: HasCASL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: HasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: HasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: HasCASL2IsabelleHOL -> Bool Source # has_model_expansion :: HasCASL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: HasCASL2IsabelleHOL -> Bool Source # constituents :: HasCASL2IsabelleHOL -> [String] Source # isInclusionComorphism :: HasCASL2IsabelleHOL -> Bool Source # rps :: HasCASL2IsabelleHOL -> Bool Source # eps :: HasCASL2IsabelleHOL -> Bool Source # isGTC :: HasCASL2IsabelleHOL -> Bool Source #
Comorphism HasCASL2HasCASL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.HasCASL2HasCASL Methods sourceLogic :: HasCASL2HasCASL -> HasCASL Source # sourceSublogic :: HasCASL2HasCASL -> Sublogic Source # sourceSublogicLossy :: HasCASL2HasCASL -> Sublogic Source # minSourceTheory :: HasCASL2HasCASL -> Maybe (LibName, String) Source # targetLogic :: HasCASL2HasCASL -> HasCASL Source # mapSublogic :: HasCASL2HasCASL -> Sublogic -> Maybe Sublogic Source # map_theory :: HasCASL2HasCASL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2HasCASL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # map_morphism :: HasCASL2HasCASL -> Morphism -> Result Morphism Source # map_sentence :: HasCASL2HasCASL -> Env -> Sentence -> Result Sentence Source # map_symbol :: HasCASL2HasCASL -> Env -> Symbol -> Set Symbol Source # extractModel :: HasCASL2HasCASL -> Env -> () -> Result (Env, [Named Sentence]) Source # is_model_transportable :: HasCASL2HasCASL -> Bool Source # has_model_expansion :: HasCASL2HasCASL -> Bool Source # is_weakly_amalgamable :: HasCASL2HasCASL -> Bool Source # constituents :: HasCASL2HasCASL -> [String] Source # isInclusionComorphism :: HasCASL2HasCASL -> Bool Source # rps :: HasCASL2HasCASL -> Bool Source # eps :: HasCASL2HasCASL -> Bool Source # isGTC :: HasCASL2HasCASL -> Bool Source #
Comorphism OWL22CommonLogic OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source #
Instance details Defined in OWL2.OWL22CommonLogic Methods sourceLogic :: OWL22CommonLogic -> OWL2 Source # sourceSublogic :: OWL22CommonLogic -> ProfSub Source # sourceSublogicLossy :: OWL22CommonLogic -> ProfSub Source # minSourceTheory :: OWL22CommonLogic -> Maybe (LibName, String) Source # targetLogic :: OWL22CommonLogic -> CommonLogic Source # mapSublogic :: OWL22CommonLogic -> ProfSub -> Maybe CommonLogicSL Source # map_theory :: OWL22CommonLogic -> (Sign, [Named Axiom]) -> Result (Sign0, [Named TEXT_META]) Source # mapMarkedTheory :: OWL22CommonLogic -> (Sign, [Named Axiom]) -> Result (Sign0, [Named TEXT_META]) Source # map_morphism :: OWL22CommonLogic -> OWLMorphism -> Result Morphism Source # map_sentence :: OWL22CommonLogic -> Sign -> Axiom -> Result TEXT_META Source # map_symbol :: OWL22CommonLogic -> Sign -> Entity -> Set Symbol Source # extractModel :: OWL22CommonLogic -> Sign -> ProofTree -> Result (Sign, [Named Axiom]) Source # is_model_transportable :: OWL22CommonLogic -> Bool Source # has_model_expansion :: OWL22CommonLogic -> Bool Source # is_weakly_amalgamable :: OWL22CommonLogic -> Bool Source # constituents :: OWL22CommonLogic -> [String] Source # isInclusionComorphism :: OWL22CommonLogic -> Bool Source # rps :: OWL22CommonLogic -> Bool Source # eps :: OWL22CommonLogic -> Bool Source # isGTC :: OWL22CommonLogic -> Bool Source #
Comorphism Prop2CommonLogic Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source #
Instance details Defined in Comorphisms.Prop2CommonLogic Methods sourceLogic :: Prop2CommonLogic -> Propositional Source # sourceSublogic :: Prop2CommonLogic -> PropSL Source # sourceSublogicLossy :: Prop2CommonLogic -> PropSL Source # minSourceTheory :: Prop2CommonLogic -> Maybe (LibName, String) Source # targetLogic :: Prop2CommonLogic -> CommonLogic Source # mapSublogic :: Prop2CommonLogic -> PropSL -> Maybe CommonLogicSL Source # map_theory :: Prop2CommonLogic -> (Sign, [Named FORMULA]) -> Result (Sign0, [Named TEXT_META]) Source # mapMarkedTheory :: Prop2CommonLogic -> (Sign, [Named FORMULA]) -> Result (Sign0, [Named TEXT_META]) Source # map_morphism :: Prop2CommonLogic -> Morphism -> Result Morphism0 Source # map_sentence :: Prop2CommonLogic -> Sign -> FORMULA -> Result TEXT_META Source # map_symbol :: Prop2CommonLogic -> Sign -> Symbol -> Set Symbol0 Source # extractModel :: Prop2CommonLogic -> Sign -> ProofTree -> Result (Sign, [Named FORMULA]) Source # is_model_transportable :: Prop2CommonLogic -> Bool Source # has_model_expansion :: Prop2CommonLogic -> Bool Source # is_weakly_amalgamable :: Prop2CommonLogic -> Bool Source # constituents :: Prop2CommonLogic -> [String] Source # isInclusionComorphism :: Prop2CommonLogic -> Bool Source # rps :: Prop2CommonLogic -> Bool Source # eps :: Prop2CommonLogic -> Bool Source # isGTC :: Prop2CommonLogic -> Bool Source #
Comorphism CommonLogicModuleElimination CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source #
Instance details Defined in Comorphisms.CommonLogicModuleElimination Methods sourceLogic :: CommonLogicModuleElimination -> CommonLogic Source # sourceSublogic :: CommonLogicModuleElimination -> CommonLogicSL Source # sourceSublogicLossy :: CommonLogicModuleElimination -> CommonLogicSL Source # minSourceTheory :: CommonLogicModuleElimination -> Maybe (LibName, String) Source # targetLogic :: CommonLogicModuleElimination -> CommonLogic Source # mapSublogic :: CommonLogicModuleElimination -> CommonLogicSL -> Maybe CommonLogicSL Source # map_theory :: CommonLogicModuleElimination -> (Sign, [Named TEXT_META]) -> Result (Sign, [Named TEXT_META]) Source # mapMarkedTheory :: CommonLogicModuleElimination -> (Sign, [Named TEXT_META]) -> Result (Sign, [Named TEXT_META]) Source # map_morphism :: CommonLogicModuleElimination -> Morphism -> Result Morphism Source # map_sentence :: CommonLogicModuleElimination -> Sign -> TEXT_META -> Result TEXT_META Source # map_symbol :: CommonLogicModuleElimination -> Sign -> Symbol -> Set Symbol Source # extractModel :: CommonLogicModuleElimination -> Sign -> ProofTree -> Result (Sign, [Named TEXT_META]) Source # is_model_transportable :: CommonLogicModuleElimination -> Bool Source # has_model_expansion :: CommonLogicModuleElimination -> Bool Source # is_weakly_amalgamable :: CommonLogicModuleElimination -> Bool Source # constituents :: CommonLogicModuleElimination -> [String] Source # isInclusionComorphism :: CommonLogicModuleElimination -> Bool Source # rps :: CommonLogicModuleElimination -> Bool Source # eps :: CommonLogicModuleElimination -> Bool Source # isGTC :: CommonLogicModuleElimination -> Bool Source #
Comorphism CommonLogic2IsabelleHOL CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.CommonLogic2IsabelleHOL Methods sourceLogic :: CommonLogic2IsabelleHOL -> CommonLogic Source # sourceSublogic :: CommonLogic2IsabelleHOL -> CommonLogicSL Source # sourceSublogicLossy :: CommonLogic2IsabelleHOL -> CommonLogicSL Source # minSourceTheory :: CommonLogic2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: CommonLogic2IsabelleHOL -> Isabelle Source # mapSublogic :: CommonLogic2IsabelleHOL -> CommonLogicSL -> Maybe () Source # map_theory :: CommonLogic2IsabelleHOL -> (Sign0, [Named TEXT_META]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: CommonLogic2IsabelleHOL -> (Sign0, [Named TEXT_META]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: CommonLogic2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: CommonLogic2IsabelleHOL -> Sign0 -> TEXT_META -> Result Sentence Source # map_symbol :: CommonLogic2IsabelleHOL -> Sign0 -> Symbol -> Set () Source # extractModel :: CommonLogic2IsabelleHOL -> Sign0 -> () -> Result (Sign0, [Named TEXT_META]) Source # is_model_transportable :: CommonLogic2IsabelleHOL -> Bool Source # has_model_expansion :: CommonLogic2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: CommonLogic2IsabelleHOL -> Bool Source # constituents :: CommonLogic2IsabelleHOL -> [String] Source # isInclusionComorphism :: CommonLogic2IsabelleHOL -> Bool Source # rps :: CommonLogic2IsabelleHOL -> Bool Source # eps :: CommonLogic2IsabelleHOL -> Bool Source # isGTC :: CommonLogic2IsabelleHOL -> Bool Source #
Comorphism OWL22CASL OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in OWL2.OWL22CASL Methods sourceLogic :: OWL22CASL -> OWL2 Source # sourceSublogic :: OWL22CASL -> ProfSub Source # sourceSublogicLossy :: OWL22CASL -> ProfSub Source # minSourceTheory :: OWL22CASL -> Maybe (LibName, String) Source # targetLogic :: OWL22CASL -> CASL Source # mapSublogic :: OWL22CASL -> ProfSub -> Maybe CASL_Sublogics Source # map_theory :: OWL22CASL -> (Sign, [Named Axiom]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: OWL22CASL -> (Sign, [Named Axiom]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: OWL22CASL -> OWLMorphism -> Result CASLMor Source # map_sentence :: OWL22CASL -> Sign -> Axiom -> Result CASLFORMULA Source # map_symbol :: OWL22CASL -> Sign -> Entity -> Set Symbol Source # extractModel :: OWL22CASL -> Sign -> ProofTree -> Result (Sign, [Named Axiom]) Source # is_model_transportable :: OWL22CASL -> Bool Source # has_model_expansion :: OWL22CASL -> Bool Source # is_weakly_amalgamable :: OWL22CASL -> Bool Source # constituents :: OWL22CASL -> [String] Source # isInclusionComorphism :: OWL22CASL -> Bool Source # rps :: OWL22CASL -> Bool Source # eps :: OWL22CASL -> Bool Source # isGTC :: OWL22CASL -> Bool Source #
Comorphism CASL2OWL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree Source #
Instance details Defined in OWL2.CASL2OWL Methods sourceLogic :: CASL2OWL -> CASL Source # sourceSublogic :: CASL2OWL -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2OWL -> CASL_Sublogics Source # minSourceTheory :: CASL2OWL -> Maybe (LibName, String) Source # targetLogic :: CASL2OWL -> OWL2 Source # mapSublogic :: CASL2OWL -> CASL_Sublogics -> Maybe ProfSub Source # map_theory :: CASL2OWL -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named Axiom]) Source # mapMarkedTheory :: CASL2OWL -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named Axiom]) Source # map_morphism :: CASL2OWL -> CASLMor -> Result OWLMorphism Source # map_sentence :: CASL2OWL -> CASLSign -> CASLFORMULA -> Result Axiom Source # map_symbol :: CASL2OWL -> CASLSign -> Symbol -> Set Entity Source # extractModel :: CASL2OWL -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2OWL -> Bool Source # has_model_expansion :: CASL2OWL -> Bool Source # is_weakly_amalgamable :: CASL2OWL -> Bool Source # constituents :: CASL2OWL -> [String] Source # isInclusionComorphism :: CASL2OWL -> Bool Source # rps :: CASL2OWL -> Bool Source # eps :: CASL2OWL -> Bool Source # isGTC :: CASL2OWL -> Bool Source #
Comorphism ExtModal2OWL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree Source #
Instance details Defined in Comorphisms.ExtModal2OWL Methods sourceLogic :: ExtModal2OWL -> ExtModal Source # sourceSublogic :: ExtModal2OWL -> ExtModalSL Source # sourceSublogicLossy :: ExtModal2OWL -> ExtModalSL Source # minSourceTheory :: ExtModal2OWL -> Maybe (LibName, String) Source # targetLogic :: ExtModal2OWL -> OWL2 Source # mapSublogic :: ExtModal2OWL -> ExtModalSL -> Maybe ProfSub Source # map_theory :: ExtModal2OWL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Sign, [Named Axiom]) Source # mapMarkedTheory :: ExtModal2OWL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Sign, [Named Axiom]) Source # map_morphism :: ExtModal2OWL -> ExtModalMorph -> Result OWLMorphism Source # map_sentence :: ExtModal2OWL -> ExtModalSign -> ExtModalFORMULA -> Result Axiom Source # map_symbol :: ExtModal2OWL -> ExtModalSign -> Symbol -> Set Entity Source # extractModel :: ExtModal2OWL -> ExtModalSign -> ProofTree -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # is_model_transportable :: ExtModal2OWL -> Bool Source # has_model_expansion :: ExtModal2OWL -> Bool Source # is_weakly_amalgamable :: ExtModal2OWL -> Bool Source # constituents :: ExtModal2OWL -> [String] Source # isInclusionComorphism :: ExtModal2OWL -> Bool Source # rps :: ExtModal2OWL -> Bool Source # eps :: ExtModal2OWL -> Bool Source # isGTC :: ExtModal2OWL -> Bool Source #
Comorphism RelScheme2CASL RelScheme () RSScheme Sentence () () Sign RSMorphism RSSymbol RSRawSymbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.RelScheme2CASL Methods sourceLogic :: RelScheme2CASL -> RelScheme Source # sourceSublogic :: RelScheme2CASL -> () Source # sourceSublogicLossy :: RelScheme2CASL -> () Source # minSourceTheory :: RelScheme2CASL -> Maybe (LibName, String) Source # targetLogic :: RelScheme2CASL -> CASL Source # mapSublogic :: RelScheme2CASL -> () -> Maybe CASL_Sublogics Source # map_theory :: RelScheme2CASL -> (Sign, [Named Sentence]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: RelScheme2CASL -> (Sign, [Named Sentence]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: RelScheme2CASL -> RSMorphism -> Result CASLMor Source # map_sentence :: RelScheme2CASL -> Sign -> Sentence -> Result CASLFORMULA Source # map_symbol :: RelScheme2CASL -> Sign -> RSSymbol -> Set Symbol Source # extractModel :: RelScheme2CASL -> Sign -> ProofTree -> Result (Sign, [Named Sentence]) Source # is_model_transportable :: RelScheme2CASL -> Bool Source # has_model_expansion :: RelScheme2CASL -> Bool Source # is_weakly_amalgamable :: RelScheme2CASL -> Bool Source # constituents :: RelScheme2CASL -> [String] Source # isInclusionComorphism :: RelScheme2CASL -> Bool Source # rps :: RelScheme2CASL -> Bool Source # eps :: RelScheme2CASL -> Bool Source # isGTC :: RelScheme2CASL -> Bool Source #
Comorphism Prop2CASL Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.Prop2CASL Methods sourceLogic :: Prop2CASL -> Propositional Source # sourceSublogic :: Prop2CASL -> PropSL Source # sourceSublogicLossy :: Prop2CASL -> PropSL Source # minSourceTheory :: Prop2CASL -> Maybe (LibName, String) Source # targetLogic :: Prop2CASL -> CASL Source # mapSublogic :: Prop2CASL -> PropSL -> Maybe CASL_Sublogics Source # map_theory :: Prop2CASL -> (Sign, [Named FORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: Prop2CASL -> (Sign, [Named FORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: Prop2CASL -> Morphism -> Result CASLMor Source # map_sentence :: Prop2CASL -> Sign -> FORMULA -> Result CASLFORMULA Source # map_symbol :: Prop2CASL -> Sign -> Symbol -> Set Symbol0 Source # extractModel :: Prop2CASL -> Sign -> ProofTree -> Result (Sign, [Named FORMULA]) Source # is_model_transportable :: Prop2CASL -> Bool Source # has_model_expansion :: Prop2CASL -> Bool Source # is_weakly_amalgamable :: Prop2CASL -> Bool Source # constituents :: Prop2CASL -> [String] Source # isInclusionComorphism :: Prop2CASL -> Bool Source # rps :: Prop2CASL -> Bool Source # eps :: Prop2CASL -> Bool Source # isGTC :: Prop2CASL -> Bool Source #
Comorphism Modal2CASL Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.Modal2CASL Methods sourceLogic :: Modal2CASL -> Modal Source # sourceSublogic :: Modal2CASL -> () Source # sourceSublogicLossy :: Modal2CASL -> () Source # minSourceTheory :: Modal2CASL -> Maybe (LibName, String) Source # targetLogic :: Modal2CASL -> CASL Source # mapSublogic :: Modal2CASL -> () -> Maybe CASL_Sublogics Source # map_theory :: Modal2CASL -> (MSign, [Named ModalFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: Modal2CASL -> (MSign, [Named ModalFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: Modal2CASL -> ModalMor -> Result CASLMor Source # map_sentence :: Modal2CASL -> MSign -> ModalFORMULA -> Result CASLFORMULA Source # map_symbol :: Modal2CASL -> MSign -> Symbol -> Set Symbol Source # extractModel :: Modal2CASL -> MSign -> ProofTree -> Result (MSign, [Named ModalFORMULA]) Source # is_model_transportable :: Modal2CASL -> Bool Source # has_model_expansion :: Modal2CASL -> Bool Source # is_weakly_amalgamable :: Modal2CASL -> Bool Source # constituents :: Modal2CASL -> [String] Source # isInclusionComorphism :: Modal2CASL -> Bool Source # rps :: Modal2CASL -> Bool Source # eps :: Modal2CASL -> Bool Source # isGTC :: Modal2CASL -> Bool Source #
Comorphism Maude2CASL Maude () MaudeText Sentence () () Sign Morphism Symbol Symbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.Maude2CASL Methods sourceLogic :: Maude2CASL -> Maude Source # sourceSublogic :: Maude2CASL -> () Source # sourceSublogicLossy :: Maude2CASL -> () Source # minSourceTheory :: Maude2CASL -> Maybe (LibName, String) Source # targetLogic :: Maude2CASL -> CASL Source # mapSublogic :: Maude2CASL -> () -> Maybe CASL_Sublogics Source # map_theory :: Maude2CASL -> (Sign, [Named Sentence]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: Maude2CASL -> (Sign, [Named Sentence]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: Maude2CASL -> Morphism -> Result CASLMor Source # map_sentence :: Maude2CASL -> Sign -> Sentence -> Result CASLFORMULA Source # map_symbol :: Maude2CASL -> Sign -> Symbol -> Set Symbol0 Source # extractModel :: Maude2CASL -> Sign -> ProofTree -> Result (Sign, [Named Sentence]) Source # is_model_transportable :: Maude2CASL -> Bool Source # has_model_expansion :: Maude2CASL -> Bool Source # is_weakly_amalgamable :: Maude2CASL -> Bool Source # constituents :: Maude2CASL -> [String] Source # isInclusionComorphism :: Maude2CASL -> Bool Source # rps :: Maude2CASL -> Bool Source # eps :: Maude2CASL -> Bool Source # isGTC :: Maude2CASL -> Bool Source #
Comorphism ExtModal2CASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.ExtModal2CASL Methods sourceLogic :: ExtModal2CASL -> ExtModal Source # sourceSublogic :: ExtModal2CASL -> ExtModalSL Source # sourceSublogicLossy :: ExtModal2CASL -> ExtModalSL Source # minSourceTheory :: ExtModal2CASL -> Maybe (LibName, String) Source # targetLogic :: ExtModal2CASL -> CASL Source # mapSublogic :: ExtModal2CASL -> ExtModalSL -> Maybe CASL_Sublogics Source # map_theory :: ExtModal2CASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: ExtModal2CASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: ExtModal2CASL -> ExtModalMorph -> Result CASLMor Source # map_sentence :: ExtModal2CASL -> ExtModalSign -> ExtModalFORMULA -> Result CASLFORMULA Source # map_symbol :: ExtModal2CASL -> ExtModalSign -> Symbol -> Set Symbol Source # extractModel :: ExtModal2CASL -> ExtModalSign -> ProofTree -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # is_model_transportable :: ExtModal2CASL -> Bool Source # has_model_expansion :: ExtModal2CASL -> Bool Source # is_weakly_amalgamable :: ExtModal2CASL -> Bool Source # constituents :: ExtModal2CASL -> [String] Source # isInclusionComorphism :: ExtModal2CASL -> Bool Source # rps :: ExtModal2CASL -> Bool Source # eps :: ExtModal2CASL -> Bool Source # isGTC :: ExtModal2CASL -> Bool Source #
Comorphism DFOL2CASL DFOL () BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.DFOL2CASL Methods sourceLogic :: DFOL2CASL -> DFOL Source # sourceSublogic :: DFOL2CASL -> () Source # sourceSublogicLossy :: DFOL2CASL -> () Source # minSourceTheory :: DFOL2CASL -> Maybe (LibName, String) Source # targetLogic :: DFOL2CASL -> CASL Source # mapSublogic :: DFOL2CASL -> () -> Maybe CASL_Sublogics Source # map_theory :: DFOL2CASL -> (Sign, [Named FORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: DFOL2CASL -> (Sign, [Named FORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: DFOL2CASL -> Morphism -> Result CASLMor Source # map_sentence :: DFOL2CASL -> Sign -> FORMULA -> Result CASLFORMULA Source # map_symbol :: DFOL2CASL -> Sign -> Symbol -> Set Symbol0 Source # extractModel :: DFOL2CASL -> Sign -> ProofTree -> Result (Sign, [Named FORMULA]) Source # is_model_transportable :: DFOL2CASL -> Bool Source # has_model_expansion :: DFOL2CASL -> Bool Source # is_weakly_amalgamable :: DFOL2CASL -> Bool Source # constituents :: DFOL2CASL -> [String] Source # isInclusionComorphism :: DFOL2CASL -> Bool Source # rps :: DFOL2CASL -> Bool Source # eps :: DFOL2CASL -> Bool Source # isGTC :: DFOL2CASL -> Bool Source #
Comorphism CL2CFOL CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.CommonLogic2CASL Methods sourceLogic :: CL2CFOL -> CommonLogic Source # sourceSublogic :: CL2CFOL -> CommonLogicSL Source # sourceSublogicLossy :: CL2CFOL -> CommonLogicSL Source # minSourceTheory :: CL2CFOL -> Maybe (LibName, String) Source # targetLogic :: CL2CFOL -> CASL Source # mapSublogic :: CL2CFOL -> CommonLogicSL -> Maybe CASL_Sublogics Source # map_theory :: CL2CFOL -> (Sign, [Named TEXT_META]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: CL2CFOL -> (Sign, [Named TEXT_META]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: CL2CFOL -> Morphism -> Result CASLMor Source # map_sentence :: CL2CFOL -> Sign -> TEXT_META -> Result CASLFORMULA Source # map_symbol :: CL2CFOL -> Sign -> Symbol -> Set Symbol0 Source # extractModel :: CL2CFOL -> Sign -> ProofTree -> Result (Sign, [Named TEXT_META]) Source # is_model_transportable :: CL2CFOL -> Bool Source # has_model_expansion :: CL2CFOL -> Bool Source # is_weakly_amalgamable :: CL2CFOL -> Bool Source # constituents :: CL2CFOL -> [String] Source # isInclusionComorphism :: CL2CFOL -> Bool Source # rps :: CL2CFOL -> Bool Source # eps :: CL2CFOL -> Bool Source # isGTC :: CL2CFOL -> Bool Source #
Comorphism CSMOF2CASL CSMOF () Metamodel Sen () () Sign Morphism () () () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.CSMOF2CASL Methods sourceLogic :: CSMOF2CASL -> CSMOF Source # sourceSublogic :: CSMOF2CASL -> () Source # sourceSublogicLossy :: CSMOF2CASL -> () Source # minSourceTheory :: CSMOF2CASL -> Maybe (LibName, String) Source # targetLogic :: CSMOF2CASL -> CASL Source # mapSublogic :: CSMOF2CASL -> () -> Maybe CASL_Sublogics Source # map_theory :: CSMOF2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: CSMOF2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: CSMOF2CASL -> Morphism -> Result CASLMor Source # map_sentence :: CSMOF2CASL -> Sign -> Sen -> Result CASLFORMULA Source # map_symbol :: CSMOF2CASL -> Sign -> () -> Set Symbol Source # extractModel :: CSMOF2CASL -> Sign -> ProofTree -> Result (Sign, [Named Sen]) Source # is_model_transportable :: CSMOF2CASL -> Bool Source # has_model_expansion :: CSMOF2CASL -> Bool Source # is_weakly_amalgamable :: CSMOF2CASL -> Bool Source # constituents :: CSMOF2CASL -> [String] Source # isInclusionComorphism :: CSMOF2CASL -> Bool Source # rps :: CSMOF2CASL -> Bool Source # eps :: CSMOF2CASL -> Bool Source # isGTC :: CSMOF2CASL -> Bool Source #
Comorphism QVTR2CASL QVTR () Transformation Sen () () Sign Morphism () () () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.QVTR2CASL Methods sourceLogic :: QVTR2CASL -> QVTR Source # sourceSublogic :: QVTR2CASL -> () Source # sourceSublogicLossy :: QVTR2CASL -> () Source # minSourceTheory :: QVTR2CASL -> Maybe (LibName, String) Source # targetLogic :: QVTR2CASL -> CASL Source # mapSublogic :: QVTR2CASL -> () -> Maybe CASL_Sublogics Source # map_theory :: QVTR2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: QVTR2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: QVTR2CASL -> Morphism -> Result CASLMor Source # map_sentence :: QVTR2CASL -> Sign -> Sen -> Result CASLFORMULA Source # map_symbol :: QVTR2CASL -> Sign -> () -> Set Symbol Source # extractModel :: QVTR2CASL -> Sign -> ProofTree -> Result (Sign, [Named Sen]) Source # is_model_transportable :: QVTR2CASL -> Bool Source # has_model_expansion :: QVTR2CASL -> Bool Source # is_weakly_amalgamable :: QVTR2CASL -> Bool Source # constituents :: QVTR2CASL -> [String] Source # isInclusionComorphism :: QVTR2CASL -> Bool Source # rps :: QVTR2CASL -> Bool Source # eps :: QVTR2CASL -> Bool Source # isGTC :: QVTR2CASL -> Bool Source #
Comorphism CFOL2IsabelleHOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.CFOL2IsabelleHOL Methods sourceLogic :: CFOL2IsabelleHOL -> CASL Source # sourceSublogic :: CFOL2IsabelleHOL -> CASL_Sublogics Source # sourceSublogicLossy :: CFOL2IsabelleHOL -> CASL_Sublogics Source # minSourceTheory :: CFOL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: CFOL2IsabelleHOL -> Isabelle Source # mapSublogic :: CFOL2IsabelleHOL -> CASL_Sublogics -> Maybe () Source # map_theory :: CFOL2IsabelleHOL -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: CFOL2IsabelleHOL -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: CFOL2IsabelleHOL -> CASLMor -> Result IsabelleMorphism Source # map_sentence :: CFOL2IsabelleHOL -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CFOL2IsabelleHOL -> CASLSign -> Symbol -> Set () Source # extractModel :: CFOL2IsabelleHOL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CFOL2IsabelleHOL -> Bool Source # has_model_expansion :: CFOL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: CFOL2IsabelleHOL -> Bool Source # constituents :: CFOL2IsabelleHOL -> [String] Source # isInclusionComorphism :: CFOL2IsabelleHOL -> Bool Source # rps :: CFOL2IsabelleHOL -> Bool Source # eps :: CFOL2IsabelleHOL -> Bool Source # isGTC :: CFOL2IsabelleHOL -> Bool Source #
Comorphism CASL2TopSort CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.CASL2TopSort Methods sourceLogic :: CASL2TopSort -> CASL Source # sourceSublogic :: CASL2TopSort -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2TopSort -> CASL_Sublogics Source # minSourceTheory :: CASL2TopSort -> Maybe (LibName, String) Source # targetLogic :: CASL2TopSort -> CASL Source # mapSublogic :: CASL2TopSort -> CASL_Sublogics -> Maybe CASL_Sublogics Source # map_theory :: CASL2TopSort -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: CASL2TopSort -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: CASL2TopSort -> CASLMor -> Result CASLMor Source # map_sentence :: CASL2TopSort -> CASLSign -> CASLFORMULA -> Result CASLFORMULA Source # map_symbol :: CASL2TopSort -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2TopSort -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2TopSort -> Bool Source # has_model_expansion :: CASL2TopSort -> Bool Source # is_weakly_amalgamable :: CASL2TopSort -> Bool Source # constituents :: CASL2TopSort -> [String] Source # isInclusionComorphism :: CASL2TopSort -> Bool Source # rps :: CASL2TopSort -> Bool Source # eps :: CASL2TopSort -> Bool Source # isGTC :: CASL2TopSort -> Bool Source #
Comorphism CASL2SubCFOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.CASL2SubCFOL Methods sourceLogic :: CASL2SubCFOL -> CASL Source # sourceSublogic :: CASL2SubCFOL -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2SubCFOL -> CASL_Sublogics Source # minSourceTheory :: CASL2SubCFOL -> Maybe (LibName, String) Source # targetLogic :: CASL2SubCFOL -> CASL Source # mapSublogic :: CASL2SubCFOL -> CASL_Sublogics -> Maybe CASL_Sublogics Source # map_theory :: CASL2SubCFOL -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: CASL2SubCFOL -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: CASL2SubCFOL -> CASLMor -> Result CASLMor Source # map_sentence :: CASL2SubCFOL -> CASLSign -> CASLFORMULA -> Result CASLFORMULA Source # map_symbol :: CASL2SubCFOL -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2SubCFOL -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2SubCFOL -> Bool Source # has_model_expansion :: CASL2SubCFOL -> Bool Source # is_weakly_amalgamable :: CASL2SubCFOL -> Bool Source # constituents :: CASL2SubCFOL -> [String] Source # isInclusionComorphism :: CASL2SubCFOL -> Bool Source # rps :: CASL2SubCFOL -> Bool Source # eps :: CASL2SubCFOL -> Bool Source # isGTC :: CASL2SubCFOL -> Bool Source #
Comorphism ExtModal2ExtModalTotal ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.ExtModal2ExtModalTotal Methods sourceLogic :: ExtModal2ExtModalTotal -> ExtModal Source # sourceSublogic :: ExtModal2ExtModalTotal -> ExtModalSL Source # sourceSublogicLossy :: ExtModal2ExtModalTotal -> ExtModalSL Source # minSourceTheory :: ExtModal2ExtModalTotal -> Maybe (LibName, String) Source # targetLogic :: ExtModal2ExtModalTotal -> ExtModal Source # mapSublogic :: ExtModal2ExtModalTotal -> ExtModalSL -> Maybe ExtModalSL Source # map_theory :: ExtModal2ExtModalTotal -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # mapMarkedTheory :: ExtModal2ExtModalTotal -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # map_morphism :: ExtModal2ExtModalTotal -> ExtModalMorph -> Result ExtModalMorph Source # map_sentence :: ExtModal2ExtModalTotal -> ExtModalSign -> ExtModalFORMULA -> Result ExtModalFORMULA Source # map_symbol :: ExtModal2ExtModalTotal -> ExtModalSign -> Symbol -> Set Symbol Source # extractModel :: ExtModal2ExtModalTotal -> ExtModalSign -> () -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # is_model_transportable :: ExtModal2ExtModalTotal -> Bool Source # has_model_expansion :: ExtModal2ExtModalTotal -> Bool Source # is_weakly_amalgamable :: ExtModal2ExtModalTotal -> Bool Source # constituents :: ExtModal2ExtModalTotal -> [String] Source # isInclusionComorphism :: ExtModal2ExtModalTotal -> Bool Source # rps :: ExtModal2ExtModalTotal -> Bool Source # eps :: ExtModal2ExtModalTotal -> Bool Source # isGTC :: ExtModal2ExtModalTotal -> Bool Source #
Comorphism CASL2Skolem CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.CASL2Skolem Methods sourceLogic :: CASL2Skolem -> CASL Source # sourceSublogic :: CASL2Skolem -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2Skolem -> CASL_Sublogics Source # minSourceTheory :: CASL2Skolem -> Maybe (LibName, String) Source # targetLogic :: CASL2Skolem -> CASL Source # mapSublogic :: CASL2Skolem -> CASL_Sublogics -> Maybe CASL_Sublogics Source # map_theory :: CASL2Skolem -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: CASL2Skolem -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: CASL2Skolem -> CASLMor -> Result CASLMor Source # map_sentence :: CASL2Skolem -> CASLSign -> CASLFORMULA -> Result CASLFORMULA Source # map_symbol :: CASL2Skolem -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2Skolem -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2Skolem -> Bool Source # has_model_expansion :: CASL2Skolem -> Bool Source # is_weakly_amalgamable :: CASL2Skolem -> Bool Source # constituents :: CASL2Skolem -> [String] Source # isInclusionComorphism :: CASL2Skolem -> Bool Source # rps :: CASL2Skolem -> Bool Source # eps :: CASL2Skolem -> Bool Source # isGTC :: CASL2Skolem -> Bool Source #
Comorphism CASL2Prop CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source #
Instance details Defined in Comorphisms.CASL2Prop Methods sourceLogic :: CASL2Prop -> CASL Source # sourceSublogic :: CASL2Prop -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2Prop -> CASL_Sublogics Source # minSourceTheory :: CASL2Prop -> Maybe (LibName, String) Source # targetLogic :: CASL2Prop -> Propositional Source # mapSublogic :: CASL2Prop -> CASL_Sublogics -> Maybe PropSL Source # map_theory :: CASL2Prop -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named FORMULA]) Source # mapMarkedTheory :: CASL2Prop -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named FORMULA]) Source # map_morphism :: CASL2Prop -> CASLMor -> Result Morphism Source # map_sentence :: CASL2Prop -> CASLSign -> CASLFORMULA -> Result FORMULA Source # map_symbol :: CASL2Prop -> CASLSign -> Symbol0 -> Set Symbol Source # extractModel :: CASL2Prop -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2Prop -> Bool Source # has_model_expansion :: CASL2Prop -> Bool Source # is_weakly_amalgamable :: CASL2Prop -> Bool Source # constituents :: CASL2Prop -> [String] Source # isInclusionComorphism :: CASL2Prop -> Bool Source # rps :: CASL2Prop -> Bool Source # eps :: CASL2Prop -> Bool Source # isGTC :: CASL2Prop -> Bool Source #
Comorphism CASL2Prenex CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.CASL2Prenex Methods sourceLogic :: CASL2Prenex -> CASL Source # sourceSublogic :: CASL2Prenex -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2Prenex -> CASL_Sublogics Source # minSourceTheory :: CASL2Prenex -> Maybe (LibName, String) Source # targetLogic :: CASL2Prenex -> CASL Source # mapSublogic :: CASL2Prenex -> CASL_Sublogics -> Maybe CASL_Sublogics Source # map_theory :: CASL2Prenex -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: CASL2Prenex -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: CASL2Prenex -> CASLMor -> Result CASLMor Source # map_sentence :: CASL2Prenex -> CASLSign -> CASLFORMULA -> Result CASLFORMULA Source # map_symbol :: CASL2Prenex -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2Prenex -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2Prenex -> Bool Source # has_model_expansion :: CASL2Prenex -> Bool Source # is_weakly_amalgamable :: CASL2Prenex -> Bool Source # constituents :: CASL2Prenex -> [String] Source # isInclusionComorphism :: CASL2Prenex -> Bool Source # rps :: CASL2Prenex -> Bool Source # eps :: CASL2Prenex -> Bool Source # isGTC :: CASL2Prenex -> Bool Source #
Comorphism CASL2PCFOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.CASL2PCFOL Methods sourceLogic :: CASL2PCFOL -> CASL Source # sourceSublogic :: CASL2PCFOL -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2PCFOL -> CASL_Sublogics Source # minSourceTheory :: CASL2PCFOL -> Maybe (LibName, String) Source # targetLogic :: CASL2PCFOL -> CASL Source # mapSublogic :: CASL2PCFOL -> CASL_Sublogics -> Maybe CASL_Sublogics Source # map_theory :: CASL2PCFOL -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: CASL2PCFOL -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: CASL2PCFOL -> CASLMor -> Result CASLMor Source # map_sentence :: CASL2PCFOL -> CASLSign -> CASLFORMULA -> Result CASLFORMULA Source # map_symbol :: CASL2PCFOL -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2PCFOL -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2PCFOL -> Bool Source # has_model_expansion :: CASL2PCFOL -> Bool Source # is_weakly_amalgamable :: CASL2PCFOL -> Bool Source # constituents :: CASL2PCFOL -> [String] Source # isInclusionComorphism :: CASL2PCFOL -> Bool Source # rps :: CASL2PCFOL -> Bool Source # eps :: CASL2PCFOL -> Bool Source # isGTC :: CASL2PCFOL -> Bool Source #
Comorphism CspCASL2Modal CspCASL () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CspCASL2Modal Methods sourceLogic :: CspCASL2Modal -> CspCASL Source # sourceSublogic :: CspCASL2Modal -> () Source # sourceSublogicLossy :: CspCASL2Modal -> () Source # minSourceTheory :: CspCASL2Modal -> Maybe (LibName, String) Source # targetLogic :: CspCASL2Modal -> Modal Source # mapSublogic :: CspCASL2Modal -> () -> Maybe () Source # map_theory :: CspCASL2Modal -> (CspCASLSign, [Named CspCASLSen]) -> Result (MSign, [Named ModalFORMULA]) Source # mapMarkedTheory :: CspCASL2Modal -> (CspCASLSign, [Named CspCASLSen]) -> Result (MSign, [Named ModalFORMULA]) Source # map_morphism :: CspCASL2Modal -> CspCASLMorphism -> Result ModalMor Source # map_sentence :: CspCASL2Modal -> CspCASLSign -> CspCASLSen -> Result ModalFORMULA Source # map_symbol :: CspCASL2Modal -> CspCASLSign -> CspSymbol -> Set Symbol Source # extractModel :: CspCASL2Modal -> CspCASLSign -> () -> Result (CspCASLSign, [Named CspCASLSen]) Source # is_model_transportable :: CspCASL2Modal -> Bool Source # has_model_expansion :: CspCASL2Modal -> Bool Source # is_weakly_amalgamable :: CspCASL2Modal -> Bool Source # constituents :: CspCASL2Modal -> [String] Source # isInclusionComorphism :: CspCASL2Modal -> Bool Source # rps :: CspCASL2Modal -> Bool Source # eps :: CspCASL2Modal -> Bool Source # isGTC :: CspCASL2Modal -> Bool Source #
Comorphism ExtModal2ExtModalNoSubsorts ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.ExtModal2ExtModalNoSubsorts Methods sourceLogic :: ExtModal2ExtModalNoSubsorts -> ExtModal Source # sourceSublogic :: ExtModal2ExtModalNoSubsorts -> ExtModalSL Source # sourceSublogicLossy :: ExtModal2ExtModalNoSubsorts -> ExtModalSL Source # minSourceTheory :: ExtModal2ExtModalNoSubsorts -> Maybe (LibName, String) Source # targetLogic :: ExtModal2ExtModalNoSubsorts -> ExtModal Source # mapSublogic :: ExtModal2ExtModalNoSubsorts -> ExtModalSL -> Maybe ExtModalSL Source # map_theory :: ExtModal2ExtModalNoSubsorts -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # mapMarkedTheory :: ExtModal2ExtModalNoSubsorts -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # map_morphism :: ExtModal2ExtModalNoSubsorts -> ExtModalMorph -> Result ExtModalMorph Source # map_sentence :: ExtModal2ExtModalNoSubsorts -> ExtModalSign -> ExtModalFORMULA -> Result ExtModalFORMULA Source # map_symbol :: ExtModal2ExtModalNoSubsorts -> ExtModalSign -> Symbol -> Set Symbol Source # extractModel :: ExtModal2ExtModalNoSubsorts -> ExtModalSign -> () -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # is_model_transportable :: ExtModal2ExtModalNoSubsorts -> Bool Source # has_model_expansion :: ExtModal2ExtModalNoSubsorts -> Bool Source # is_weakly_amalgamable :: ExtModal2ExtModalNoSubsorts -> Bool Source # constituents :: ExtModal2ExtModalNoSubsorts -> [String] Source # isInclusionComorphism :: ExtModal2ExtModalNoSubsorts -> Bool Source # rps :: ExtModal2ExtModalNoSubsorts -> Bool Source # eps :: ExtModal2ExtModalNoSubsorts -> Bool Source # isGTC :: ExtModal2ExtModalNoSubsorts -> Bool Source #
Comorphism CASL2NNF CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.CASL2NNF Methods sourceLogic :: CASL2NNF -> CASL Source # sourceSublogic :: CASL2NNF -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2NNF -> CASL_Sublogics Source # minSourceTheory :: CASL2NNF -> Maybe (LibName, String) Source # targetLogic :: CASL2NNF -> CASL Source # mapSublogic :: CASL2NNF -> CASL_Sublogics -> Maybe CASL_Sublogics Source # map_theory :: CASL2NNF -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: CASL2NNF -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: CASL2NNF -> CASLMor -> Result CASLMor Source # map_sentence :: CASL2NNF -> CASLSign -> CASLFORMULA -> Result CASLFORMULA Source # map_symbol :: CASL2NNF -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2NNF -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2NNF -> Bool Source # has_model_expansion :: CASL2NNF -> Bool Source # is_weakly_amalgamable :: CASL2NNF -> Bool Source # constituents :: CASL2NNF -> [String] Source # isInclusionComorphism :: CASL2NNF -> Bool Source # rps :: CASL2NNF -> Bool Source # eps :: CASL2NNF -> Bool Source # isGTC :: CASL2NNF -> Bool Source #
Comorphism CASL2Modal CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2Modal Methods sourceLogic :: CASL2Modal -> CASL Source # sourceSublogic :: CASL2Modal -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2Modal -> CASL_Sublogics Source # minSourceTheory :: CASL2Modal -> Maybe (LibName, String) Source # targetLogic :: CASL2Modal -> Modal Source # mapSublogic :: CASL2Modal -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2Modal -> (CASLSign, [Named CASLFORMULA]) -> Result (MSign, [Named ModalFORMULA]) Source # mapMarkedTheory :: CASL2Modal -> (CASLSign, [Named CASLFORMULA]) -> Result (MSign, [Named ModalFORMULA]) Source # map_morphism :: CASL2Modal -> CASLMor -> Result ModalMor Source # map_sentence :: CASL2Modal -> CASLSign -> CASLFORMULA -> Result ModalFORMULA Source # map_symbol :: CASL2Modal -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2Modal -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2Modal -> Bool Source # has_model_expansion :: CASL2Modal -> Bool Source # is_weakly_amalgamable :: CASL2Modal -> Bool Source # constituents :: CASL2Modal -> [String] Source # isInclusionComorphism :: CASL2Modal -> Bool Source # rps :: CASL2Modal -> Bool Source # eps :: CASL2Modal -> Bool Source # isGTC :: CASL2Modal -> Bool Source #
Comorphism CASL2Hybrid CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Hybrid () H_BASIC_SPEC HybridFORMULA SYMB_ITEMS SYMB_MAP_ITEMS HSign HybridMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2Hybrid Methods sourceLogic :: CASL2Hybrid -> CASL Source # sourceSublogic :: CASL2Hybrid -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2Hybrid -> CASL_Sublogics Source # minSourceTheory :: CASL2Hybrid -> Maybe (LibName, String) Source # targetLogic :: CASL2Hybrid -> Hybrid Source # mapSublogic :: CASL2Hybrid -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2Hybrid -> (CASLSign, [Named CASLFORMULA]) -> Result (HSign, [Named HybridFORMULA]) Source # mapMarkedTheory :: CASL2Hybrid -> (CASLSign, [Named CASLFORMULA]) -> Result (HSign, [Named HybridFORMULA]) Source # map_morphism :: CASL2Hybrid -> CASLMor -> Result HybridMor Source # map_sentence :: CASL2Hybrid -> CASLSign -> CASLFORMULA -> Result HybridFORMULA Source # map_symbol :: CASL2Hybrid -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2Hybrid -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2Hybrid -> Bool Source # has_model_expansion :: CASL2Hybrid -> Bool Source # is_weakly_amalgamable :: CASL2Hybrid -> Bool Source # constituents :: CASL2Hybrid -> [String] Source # isInclusionComorphism :: CASL2Hybrid -> Bool Source # rps :: CASL2Hybrid -> Bool Source # eps :: CASL2Hybrid -> Bool Source # isGTC :: CASL2Hybrid -> Bool 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 #
Comorphism ExtModal2HasCASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.ExtModal2HasCASL Methods sourceLogic :: ExtModal2HasCASL -> ExtModal Source # sourceSublogic :: ExtModal2HasCASL -> ExtModalSL Source # sourceSublogicLossy :: ExtModal2HasCASL -> ExtModalSL Source # minSourceTheory :: ExtModal2HasCASL -> Maybe (LibName, String) Source # targetLogic :: ExtModal2HasCASL -> HasCASL Source # mapSublogic :: ExtModal2HasCASL -> ExtModalSL -> Maybe Sublogic Source # map_theory :: ExtModal2HasCASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: ExtModal2HasCASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Env, [Named Sentence]) Source # map_morphism :: ExtModal2HasCASL -> ExtModalMorph -> Result Morphism Source # map_sentence :: ExtModal2HasCASL -> ExtModalSign -> ExtModalFORMULA -> Result Sentence Source # map_symbol :: ExtModal2HasCASL -> ExtModalSign -> Symbol0 -> Set Symbol Source # extractModel :: ExtModal2HasCASL -> ExtModalSign -> () -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # is_model_transportable :: ExtModal2HasCASL -> Bool Source # has_model_expansion :: ExtModal2HasCASL -> Bool Source # is_weakly_amalgamable :: ExtModal2HasCASL -> Bool Source # constituents :: ExtModal2HasCASL -> [String] Source # isInclusionComorphism :: ExtModal2HasCASL -> Bool Source # rps :: ExtModal2HasCASL -> Bool Source # eps :: ExtModal2HasCASL -> Bool Source # isGTC :: ExtModal2HasCASL -> Bool Source #
Comorphism CASL2ExtModal CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2ExtModal Methods sourceLogic :: CASL2ExtModal -> CASL Source # sourceSublogic :: CASL2ExtModal -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2ExtModal -> CASL_Sublogics Source # minSourceTheory :: CASL2ExtModal -> Maybe (LibName, String) Source # targetLogic :: CASL2ExtModal -> ExtModal Source # mapSublogic :: CASL2ExtModal -> CASL_Sublogics -> Maybe ExtModalSL Source # map_theory :: CASL2ExtModal -> (CASLSign, [Named CASLFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # mapMarkedTheory :: CASL2ExtModal -> (CASLSign, [Named CASLFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # map_morphism :: CASL2ExtModal -> CASLMor -> Result ExtModalMorph Source # map_sentence :: CASL2ExtModal -> CASLSign -> CASLFORMULA -> Result ExtModalFORMULA Source # map_symbol :: CASL2ExtModal -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2ExtModal -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2ExtModal -> Bool Source # has_model_expansion :: CASL2ExtModal -> Bool Source # is_weakly_amalgamable :: CASL2ExtModal -> Bool Source # constituents :: CASL2ExtModal -> [String] Source # isInclusionComorphism :: CASL2ExtModal -> Bool Source # rps :: CASL2ExtModal -> Bool Source # eps :: CASL2ExtModal -> Bool Source # isGTC :: CASL2ExtModal -> Bool Source #
Comorphism CASL2CspCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CspCASL () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () Source #
Instance details Defined in Comorphisms.CASL2CspCASL Methods sourceLogic :: CASL2CspCASL -> CASL Source # sourceSublogic :: CASL2CspCASL -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2CspCASL -> CASL_Sublogics Source # minSourceTheory :: CASL2CspCASL -> Maybe (LibName, String) Source # targetLogic :: CASL2CspCASL -> CspCASL Source # mapSublogic :: CASL2CspCASL -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2CspCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (CspCASLSign, [Named CspCASLSen]) Source # mapMarkedTheory :: CASL2CspCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (CspCASLSign, [Named CspCASLSen]) Source # map_morphism :: CASL2CspCASL -> CASLMor -> Result CspCASLMorphism Source # map_sentence :: CASL2CspCASL -> CASLSign -> CASLFORMULA -> Result CspCASLSen Source # map_symbol :: CASL2CspCASL -> CASLSign -> Symbol -> Set CspSymbol Source # extractModel :: CASL2CspCASL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2CspCASL -> Bool Source # has_model_expansion :: CASL2CspCASL -> Bool Source # is_weakly_amalgamable :: CASL2CspCASL -> Bool Source # constituents :: CASL2CspCASL -> [String] Source # isInclusionComorphism :: CASL2CspCASL -> Bool Source # rps :: CASL2CspCASL -> Bool Source # eps :: CASL2CspCASL -> Bool Source # isGTC :: CASL2CspCASL -> Bool Source #
Comorphism Adl2CASL Adl () Context Sen () () Sign Morphism Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.Adl2CASL Methods sourceLogic :: Adl2CASL -> Adl Source # sourceSublogic :: Adl2CASL -> () Source # sourceSublogicLossy :: Adl2CASL -> () Source # minSourceTheory :: Adl2CASL -> Maybe (LibName, String) Source # targetLogic :: Adl2CASL -> CASL Source # mapSublogic :: Adl2CASL -> () -> Maybe CASL_Sublogics Source # map_theory :: Adl2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: Adl2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: Adl2CASL -> Morphism -> Result CASLMor Source # map_sentence :: Adl2CASL -> Sign -> Sen -> Result CASLFORMULA Source # map_symbol :: Adl2CASL -> Sign -> Symbol -> Set Symbol0 Source # extractModel :: Adl2CASL -> Sign -> ProofTree -> Result (Sign, [Named Sen]) Source # is_model_transportable :: Adl2CASL -> Bool Source # has_model_expansion :: Adl2CASL -> Bool Source # is_weakly_amalgamable :: Adl2CASL -> Bool Source # constituents :: Adl2CASL -> [String] Source # isInclusionComorphism :: Adl2CASL -> Bool Source # rps :: Adl2CASL -> Bool Source # eps :: Adl2CASL -> Bool Source # isGTC :: Adl2CASL -> Bool Source #
Comorphism CoCFOL2IsabelleHOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.CoCFOL2IsabelleHOL Methods sourceLogic :: CoCFOL2IsabelleHOL -> CoCASL Source # sourceSublogic :: CoCFOL2IsabelleHOL -> CoCASL_Sublogics Source # sourceSublogicLossy :: CoCFOL2IsabelleHOL -> CoCASL_Sublogics Source # minSourceTheory :: CoCFOL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: CoCFOL2IsabelleHOL -> Isabelle Source # mapSublogic :: CoCFOL2IsabelleHOL -> CoCASL_Sublogics -> Maybe () Source # map_theory :: CoCFOL2IsabelleHOL -> (CSign, [Named CoCASLFORMULA]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: CoCFOL2IsabelleHOL -> (CSign, [Named CoCASLFORMULA]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: CoCFOL2IsabelleHOL -> CoCASLMor -> Result IsabelleMorphism Source # map_sentence :: CoCFOL2IsabelleHOL -> CSign -> CoCASLFORMULA -> Result Sentence Source # map_symbol :: CoCFOL2IsabelleHOL -> CSign -> Symbol -> Set () Source # extractModel :: CoCFOL2IsabelleHOL -> CSign -> () -> Result (CSign, [Named CoCASLFORMULA]) Source # is_model_transportable :: CoCFOL2IsabelleHOL -> Bool Source # has_model_expansion :: CoCFOL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: CoCFOL2IsabelleHOL -> Bool Source # constituents :: CoCFOL2IsabelleHOL -> [String] Source # isInclusionComorphism :: CoCFOL2IsabelleHOL -> Bool Source # rps :: CoCFOL2IsabelleHOL -> Bool Source # eps :: CoCFOL2IsabelleHOL -> Bool Source # isGTC :: CoCFOL2IsabelleHOL -> Bool Source #
Comorphism CoCASL2CoSubCFOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CoCASL2CoSubCFOL Methods sourceLogic :: CoCASL2CoSubCFOL -> CoCASL Source # sourceSublogic :: CoCASL2CoSubCFOL -> CoCASL_Sublogics Source # sourceSublogicLossy :: CoCASL2CoSubCFOL -> CoCASL_Sublogics Source # minSourceTheory :: CoCASL2CoSubCFOL -> Maybe (LibName, String) Source # targetLogic :: CoCASL2CoSubCFOL -> CoCASL Source # mapSublogic :: CoCASL2CoSubCFOL -> CoCASL_Sublogics -> Maybe CoCASL_Sublogics Source # map_theory :: CoCASL2CoSubCFOL -> (CSign, [Named CoCASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # mapMarkedTheory :: CoCASL2CoSubCFOL -> (CSign, [Named CoCASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # map_morphism :: CoCASL2CoSubCFOL -> CoCASLMor -> Result CoCASLMor Source # map_sentence :: CoCASL2CoSubCFOL -> CSign -> CoCASLFORMULA -> Result CoCASLFORMULA Source # map_symbol :: CoCASL2CoSubCFOL -> CSign -> Symbol -> Set Symbol Source # extractModel :: CoCASL2CoSubCFOL -> CSign -> () -> Result (CSign, [Named CoCASLFORMULA]) Source # is_model_transportable :: CoCASL2CoSubCFOL -> Bool Source # has_model_expansion :: CoCASL2CoSubCFOL -> Bool Source # is_weakly_amalgamable :: CoCASL2CoSubCFOL -> Bool Source # constituents :: CoCASL2CoSubCFOL -> [String] Source # isInclusionComorphism :: CoCASL2CoSubCFOL -> Bool Source # rps :: CoCASL2CoSubCFOL -> Bool Source # eps :: CoCASL2CoSubCFOL -> Bool Source # isGTC :: CoCASL2CoSubCFOL -> Bool Source #
Comorphism CoCASL2CoPCFOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CoCASL2CoPCFOL Methods sourceLogic :: CoCASL2CoPCFOL -> CoCASL Source # sourceSublogic :: CoCASL2CoPCFOL -> CoCASL_Sublogics Source # sourceSublogicLossy :: CoCASL2CoPCFOL -> CoCASL_Sublogics Source # minSourceTheory :: CoCASL2CoPCFOL -> Maybe (LibName, String) Source # targetLogic :: CoCASL2CoPCFOL -> CoCASL Source # mapSublogic :: CoCASL2CoPCFOL -> CoCASL_Sublogics -> Maybe CoCASL_Sublogics Source # map_theory :: CoCASL2CoPCFOL -> (CSign, [Named CoCASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # mapMarkedTheory :: CoCASL2CoPCFOL -> (CSign, [Named CoCASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # map_morphism :: CoCASL2CoPCFOL -> CoCASLMor -> Result CoCASLMor Source # map_sentence :: CoCASL2CoPCFOL -> CSign -> CoCASLFORMULA -> Result CoCASLFORMULA Source # map_symbol :: CoCASL2CoPCFOL -> CSign -> Symbol -> Set Symbol Source # extractModel :: CoCASL2CoPCFOL -> CSign -> () -> Result (CSign, [Named CoCASLFORMULA]) Source # is_model_transportable :: CoCASL2CoPCFOL -> Bool Source # has_model_expansion :: CoCASL2CoPCFOL -> Bool Source # is_weakly_amalgamable :: CoCASL2CoPCFOL -> Bool Source # constituents :: CoCASL2CoPCFOL -> [String] Source # isInclusionComorphism :: CoCASL2CoPCFOL -> Bool Source # rps :: CoCASL2CoPCFOL -> Bool Source # eps :: CoCASL2CoPCFOL -> Bool Source # isGTC :: CoCASL2CoPCFOL -> Bool Source #
Comorphism CASL2CoCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2CoCASL Methods sourceLogic :: CASL2CoCASL -> CASL Source # sourceSublogic :: CASL2CoCASL -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2CoCASL -> CASL_Sublogics Source # minSourceTheory :: CASL2CoCASL -> Maybe (LibName, String) Source # targetLogic :: CASL2CoCASL -> CoCASL Source # mapSublogic :: CASL2CoCASL -> CASL_Sublogics -> Maybe CoCASL_Sublogics Source # map_theory :: CASL2CoCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # mapMarkedTheory :: CASL2CoCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # map_morphism :: CASL2CoCASL -> CASLMor -> Result CoCASLMor Source # map_sentence :: CASL2CoCASL -> CASLSign -> CASLFORMULA -> Result CoCASLFORMULA Source # map_symbol :: CASL2CoCASL -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2CoCASL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2CoCASL -> Bool Source # has_model_expansion :: CASL2CoCASL -> Bool Source # is_weakly_amalgamable :: CASL2CoCASL -> Bool Source # constituents :: CASL2CoCASL -> [String] Source # isInclusionComorphism :: CASL2CoCASL -> Bool Source # rps :: CASL2CoCASL -> Bool Source # eps :: CASL2CoCASL -> Bool Source # isGTC :: CASL2CoCASL -> Bool Source #
Comorphism CASL_DL2CASL CASL_DL CASL_DL_SL DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS DLSign DLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.CASL_DL2CASL Methods sourceLogic :: CASL_DL2CASL -> CASL_DL Source # sourceSublogic :: CASL_DL2CASL -> CASL_DL_SL Source # sourceSublogicLossy :: CASL_DL2CASL -> CASL_DL_SL Source # minSourceTheory :: CASL_DL2CASL -> Maybe (LibName, String) Source # targetLogic :: CASL_DL2CASL -> CASL Source # mapSublogic :: CASL_DL2CASL -> CASL_DL_SL -> Maybe CASL_Sublogics Source # map_theory :: CASL_DL2CASL -> (DLSign, [Named DLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: CASL_DL2CASL -> (DLSign, [Named DLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: CASL_DL2CASL -> DLMor -> Result CASLMor Source # map_sentence :: CASL_DL2CASL -> DLSign -> DLFORMULA -> Result CASLFORMULA Source # map_symbol :: CASL_DL2CASL -> DLSign -> Symbol -> Set Symbol Source # extractModel :: CASL_DL2CASL -> DLSign -> ProofTree -> Result (DLSign, [Named DLFORMULA]) Source # is_model_transportable :: CASL_DL2CASL -> Bool Source # has_model_expansion :: CASL_DL2CASL -> Bool Source # is_weakly_amalgamable :: CASL_DL2CASL -> Bool Source # constituents :: CASL_DL2CASL -> [String] Source # isInclusionComorphism :: CASL_DL2CASL -> Bool Source # rps :: CASL_DL2CASL -> Bool Source # eps :: CASL_DL2CASL -> Bool Source # isGTC :: CASL_DL2CASL -> Bool Source #
Comorphism CASL2VSERefine CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2VSERefine Methods sourceLogic :: CASL2VSERefine -> CASL Source # sourceSublogic :: CASL2VSERefine -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSERefine -> CASL_Sublogics Source # minSourceTheory :: CASL2VSERefine -> Maybe (LibName, String) Source # targetLogic :: CASL2VSERefine -> VSE Source # mapSublogic :: CASL2VSERefine -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSERefine -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSERefine -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSERefine -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSERefine -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSERefine -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSERefine -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSERefine -> Bool Source # has_model_expansion :: CASL2VSERefine -> Bool Source # is_weakly_amalgamable :: CASL2VSERefine -> Bool Source # constituents :: CASL2VSERefine -> [String] Source # isInclusionComorphism :: CASL2VSERefine -> Bool Source # rps :: CASL2VSERefine -> Bool Source # eps :: CASL2VSERefine -> Bool Source # isGTC :: CASL2VSERefine -> Bool Source #
Comorphism CASL2VSEImport CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2VSEImport Methods sourceLogic :: CASL2VSEImport -> CASL Source # sourceSublogic :: CASL2VSEImport -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSEImport -> CASL_Sublogics Source # minSourceTheory :: CASL2VSEImport -> Maybe (LibName, String) Source # targetLogic :: CASL2VSEImport -> VSE Source # mapSublogic :: CASL2VSEImport -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSEImport -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSEImport -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSEImport -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSEImport -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSEImport -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSEImport -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSEImport -> Bool Source # has_model_expansion :: CASL2VSEImport -> Bool Source # is_weakly_amalgamable :: CASL2VSEImport -> Bool Source # constituents :: CASL2VSEImport -> [String] Source # isInclusionComorphism :: CASL2VSEImport -> Bool Source # rps :: CASL2VSEImport -> Bool Source # eps :: CASL2VSEImport -> Bool Source # isGTC :: CASL2VSEImport -> Bool Source #
Comorphism CASL2VSE CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2VSE Methods sourceLogic :: CASL2VSE -> CASL Source # sourceSublogic :: CASL2VSE -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSE -> CASL_Sublogics Source # minSourceTheory :: CASL2VSE -> Maybe (LibName, String) Source # targetLogic :: CASL2VSE -> VSE Source # mapSublogic :: CASL2VSE -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSE -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSE -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSE -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSE -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSE -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSE -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSE -> Bool Source # has_model_expansion :: CASL2VSE -> Bool Source # is_weakly_amalgamable :: CASL2VSE -> Bool Source # constituents :: CASL2VSE -> [String] Source # isInclusionComorphism :: CASL2VSE -> Bool Source # rps :: CASL2VSE -> Bool Source # eps :: CASL2VSE -> Bool Source # isGTC :: CASL2VSE -> Bool Source #
Comorphism DMU2OWL2 DMU () Text () () () Text (DefaultMorphism Text) () () () OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree Source #
Instance details Defined in OWL2.DMU2OWL2 Methods sourceLogic :: DMU2OWL2 -> DMU Source # sourceSublogic :: DMU2OWL2 -> () Source # sourceSublogicLossy :: DMU2OWL2 -> () Source # minSourceTheory :: DMU2OWL2 -> Maybe (LibName, String) Source # targetLogic :: DMU2OWL2 -> OWL2 Source # mapSublogic :: DMU2OWL2 -> () -> Maybe ProfSub Source # map_theory :: DMU2OWL2 -> (Text, [Named ()]) -> Result (Sign, [Named Axiom]) Source # mapMarkedTheory :: DMU2OWL2 -> (Text, [Named ()]) -> Result (Sign, [Named Axiom]) Source # map_morphism :: DMU2OWL2 -> DefaultMorphism Text -> Result OWLMorphism Source # map_sentence :: DMU2OWL2 -> Text -> () -> Result Axiom Source # map_symbol :: DMU2OWL2 -> Text -> () -> Set Entity Source # extractModel :: DMU2OWL2 -> Text -> ProofTree -> Result (Text, [Named ()]) Source # is_model_transportable :: DMU2OWL2 -> Bool Source # has_model_expansion :: DMU2OWL2 -> Bool Source # is_weakly_amalgamable :: DMU2OWL2 -> Bool Source # constituents :: DMU2OWL2 -> [String] Source # isInclusionComorphism :: DMU2OWL2 -> Bool Source # rps :: DMU2OWL2 -> Bool Source # eps :: DMU2OWL2 -> Bool Source # isGTC :: DMU2OWL2 -> Bool Source #
Comorphism SoftFOL2CommonLogic SoftFOL () [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () ProofTree CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source #
Instance details Defined in Comorphisms.SoftFOL2CommonLogic Methods sourceLogic :: SoftFOL2CommonLogic -> SoftFOL Source # sourceSublogic :: SoftFOL2CommonLogic -> () Source # sourceSublogicLossy :: SoftFOL2CommonLogic -> () Source # minSourceTheory :: SoftFOL2CommonLogic -> Maybe (LibName, String) Source # targetLogic :: SoftFOL2CommonLogic -> CommonLogic Source # mapSublogic :: SoftFOL2CommonLogic -> () -> Maybe CommonLogicSL Source # map_theory :: SoftFOL2CommonLogic -> (Sign, [Named Sentence]) -> Result (Sign0, [Named TEXT_META]) Source # mapMarkedTheory :: SoftFOL2CommonLogic -> (Sign, [Named Sentence]) -> Result (Sign0, [Named TEXT_META]) Source # map_morphism :: SoftFOL2CommonLogic -> SoftFOLMorphism -> Result Morphism Source # map_sentence :: SoftFOL2CommonLogic -> Sign -> Sentence -> Result TEXT_META Source # map_symbol :: SoftFOL2CommonLogic -> Sign -> SFSymbol -> Set Symbol Source # extractModel :: SoftFOL2CommonLogic -> Sign -> ProofTree -> Result (Sign, [Named Sentence]) Source # is_model_transportable :: SoftFOL2CommonLogic -> Bool Source # has_model_expansion :: SoftFOL2CommonLogic -> Bool Source # is_weakly_amalgamable :: SoftFOL2CommonLogic -> Bool Source # constituents :: SoftFOL2CommonLogic -> [String] Source # isInclusionComorphism :: SoftFOL2CommonLogic -> Bool Source # rps :: SoftFOL2CommonLogic -> Bool Source # eps :: SoftFOL2CommonLogic -> Bool Source # isGTC :: SoftFOL2CommonLogic -> Bool Source #
(Comorphism cid1 lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2, Comorphism cid2 lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4 sign4 morphism4 symbol4 raw_symbol4 proof_tree4 lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3 sign3 morphism3 symbol3 raw_symbol3 proof_tree3) => Comorphism (CompComorphism cid1 cid2) lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3 sign3 morphism3 symbol3 raw_symbol3 proof_tree3 Source #
Instance details Defined in Logic.Comorphism Methods sourceLogic :: CompComorphism cid1 cid2 -> lid1 Source # sourceSublogic :: CompComorphism cid1 cid2 -> sublogics1 Source # sourceSublogicLossy :: CompComorphism cid1 cid2 -> sublogics1 Source # minSourceTheory :: CompComorphism cid1 cid2 -> Maybe (LibName, String) Source # targetLogic :: CompComorphism cid1 cid2 -> lid3 Source # mapSublogic :: CompComorphism cid1 cid2 -> sublogics1 -> Maybe sublogics3 Source # map_theory :: CompComorphism cid1 cid2 -> (sign1, [Named sentence1]) -> Result (sign3, [Named sentence3]) Source # mapMarkedTheory :: CompComorphism cid1 cid2 -> (sign1, [Named sentence1]) -> Result (sign3, [Named sentence3]) Source # map_morphism :: CompComorphism cid1 cid2 -> morphism1 -> Result morphism3 Source # map_sentence :: CompComorphism cid1 cid2 -> sign1 -> sentence1 -> Result sentence3 Source # map_symbol :: CompComorphism cid1 cid2 -> sign1 -> symbol1 -> Set symbol3 Source # extractModel :: CompComorphism cid1 cid2 -> sign1 -> proof_tree3 -> Result (sign1, [Named sentence1]) Source # is_model_transportable :: CompComorphism cid1 cid2 -> Bool Source # has_model_expansion :: CompComorphism cid1 cid2 -> Bool Source # is_weakly_amalgamable :: CompComorphism cid1 cid2 -> Bool Source # constituents :: CompComorphism cid1 cid2 -> [String] Source # isInclusionComorphism :: CompComorphism cid1 cid2 -> Bool Source # rps :: CompComorphism cid1 cid2 -> Bool Source # eps :: CompComorphism cid1 cid2 -> Bool Source # isGTC :: CompComorphism cid1 cid2 -> Bool Source #
Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => Comorphism (InclComorphism lid sublogics) lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree Source #
Instance details Defined in Logic.Comorphism Methods sourceLogic :: InclComorphism lid sublogics -> lid Source # sourceSublogic :: InclComorphism lid sublogics -> sublogics Source # sourceSublogicLossy :: InclComorphism lid sublogics -> sublogics Source # minSourceTheory :: InclComorphism lid sublogics -> Maybe (LibName, String) Source # targetLogic :: InclComorphism lid sublogics -> lid Source # mapSublogic :: InclComorphism lid sublogics -> sublogics -> Maybe sublogics Source # map_theory :: InclComorphism lid sublogics -> (sign, [Named sentence]) -> Result (sign, [Named sentence]) Source # mapMarkedTheory :: InclComorphism lid sublogics -> (sign, [Named sentence]) -> Result (sign, [Named sentence]) Source # map_morphism :: InclComorphism lid sublogics -> morphism -> Result morphism Source # map_sentence :: InclComorphism lid sublogics -> sign -> sentence -> Result sentence Source # map_symbol :: InclComorphism lid sublogics -> sign -> symbol -> Set symbol Source # extractModel :: InclComorphism lid sublogics -> sign -> proof_tree -> Result (sign, [Named sentence]) Source # is_model_transportable :: InclComorphism lid sublogics -> Bool Source # has_model_expansion :: InclComorphism lid sublogics -> Bool Source # is_weakly_amalgamable :: InclComorphism lid sublogics -> Bool Source # constituents :: InclComorphism lid sublogics -> [String] Source # isInclusionComorphism :: InclComorphism lid sublogics -> Bool Source # rps :: InclComorphism lid sublogics -> Bool Source # eps :: InclComorphism lid sublogics -> Bool Source # isGTC :: InclComorphism lid sublogics -> Bool Source #
(CspCASLSemantics a, CspCASLSemantics b) => Comorphism (CspCASL2CspCASL a b) (GenCspCASL a) () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () (GenCspCASL b) () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () Source #
Instance details Defined in CspCASL.Comorphisms Methods sourceLogic :: CspCASL2CspCASL a b -> GenCspCASL a Source # sourceSublogic :: CspCASL2CspCASL a b -> () Source # sourceSublogicLossy :: CspCASL2CspCASL a b -> () Source # minSourceTheory :: CspCASL2CspCASL a b -> Maybe (LibName, String) Source # targetLogic :: CspCASL2CspCASL a b -> GenCspCASL b Source # mapSublogic :: CspCASL2CspCASL a b -> () -> Maybe () Source # map_theory :: CspCASL2CspCASL a b -> (CspCASLSign, [Named CspCASLSen]) -> Result (CspCASLSign, [Named CspCASLSen]) Source # mapMarkedTheory :: CspCASL2CspCASL a b -> (CspCASLSign, [Named CspCASLSen]) -> Result (CspCASLSign, [Named CspCASLSen]) Source # map_morphism :: CspCASL2CspCASL a b -> CspCASLMorphism -> Result CspCASLMorphism Source # map_sentence :: CspCASL2CspCASL a b -> CspCASLSign -> CspCASLSen -> Result CspCASLSen Source # map_symbol :: CspCASL2CspCASL a b -> CspCASLSign -> CspSymbol -> Set CspSymbol Source # extractModel :: CspCASL2CspCASL a b -> CspCASLSign -> () -> Result (CspCASLSign, [Named CspCASLSen]) Source # is_model_transportable :: CspCASL2CspCASL a b -> Bool Source # has_model_expansion :: CspCASL2CspCASL a b -> Bool Source # is_weakly_amalgamable :: CspCASL2CspCASL a b -> Bool Source # constituents :: CspCASL2CspCASL a b -> [String] Source # isInclusionComorphism :: CspCASL2CspCASL a b -> Bool Source # rps :: CspCASL2CspCASL a b -> Bool Source # eps :: CspCASL2CspCASL a b -> Bool Source # isGTC :: CspCASL2CspCASL a b -> Bool Source #

targetSublogic :: Comorphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 => cid -> sublogics2 Source #

map_sign :: Comorphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 => cid -> sign1 -> Result (sign2, [Named sentence2]) Source #

this function is based on map_theory using no sentences as input

wrapMapTheory :: Comorphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 => cid -> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2]) Source #

wrapMapTheoryPossiblyLossy :: Comorphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 => Bool -> cid -> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2]) Source #

use this function instead of mapMarkedTheory

mkTheoryMapping :: Monad m => (sign1 -> m (sign2, [Named sentence2])) -> (sign1 -> sentence1 -> m sentence2) -> (sign1, [Named sentence1]) -> m (sign2, [Named sentence2]) Source #

data AnyComorphism Source #

Existential type for comorphisms

Constructors

forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2.Comorphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 => Comorphism cid

Instances

Instances details

Eq AnyComorphism Source #
Instance details Defined in Logic.Comorphism Methods (==) :: AnyComorphism -> AnyComorphism -> Bool (/=) :: AnyComorphism -> AnyComorphism -> Bool
Ord AnyComorphism Source #
Instance details Defined in Logic.Comorphism Methods compare :: AnyComorphism -> AnyComorphism -> Ordering (<) :: AnyComorphism -> AnyComorphism -> Bool (<=) :: AnyComorphism -> AnyComorphism -> Bool (>) :: AnyComorphism -> AnyComorphism -> Bool (>=) :: AnyComorphism -> AnyComorphism -> Bool max :: AnyComorphism -> AnyComorphism -> AnyComorphism min :: AnyComorphism -> AnyComorphism -> AnyComorphism
Show AnyComorphism Source #
Instance details Defined in Logic.Comorphism Methods showsPrec :: Int -> AnyComorphism -> ShowS show :: AnyComorphism -> String showList :: [AnyComorphism] -> ShowS
Pretty AnyComorphism Source #
Instance details Defined in Logic.Comorphism Methods pretty :: AnyComorphism -> Doc Source # pretties :: [AnyComorphism] -> Doc Source #
ShATermLG AnyComorphism Source #
Instance details Defined in ATC.Grothendieck Methods toShATermLG :: ATermTable -> AnyComorphism -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, AnyComorphism) Source #

idComorphism :: AnyLogic -> AnyComorphism Source #

compute the identity comorphism for a logic

isIdComorphism :: AnyComorphism -> Bool Source #

Test whether a comporphism is the identity

isModelTransportable :: AnyComorphism -> Bool Source #

Test whether a comorphism is model-transportable

hasModelExpansion :: AnyComorphism -> Bool Source #

Test whether a comorphism has model expansion

isEps :: AnyComorphism -> Bool Source #

Tests whether a comorphism is rps or eps

isRps :: AnyComorphism -> Bool Source #

isWeaklyAmalgamable :: AnyComorphism -> Bool Source #

Test whether a comorphism is weakly amalgamable

compComorphism :: MonadFail m => AnyComorphism -> AnyComorphism -> m AnyComorphism Source #

Compose comorphisms