Hets - the Heterogeneous Tool Set

Copyright(c) Till Mossakowski Uni Bremen 2002-2006
LicenseGPLv2 or higher, see LICENSE.txt
Maintainertill@informatik.uni-bremen.de
Stabilityprovisional
Portabilitynon-portable (via Logic)
Safe HaskellNone

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

Documentation

data CompComorphism cid1 cid2 Source #

Constructors

CompComorphism cid1 cid2 

Instances

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 # 
(Data cid2, Data cid1) => Data (CompComorphism cid1 cid2) Source # 

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 :: (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 cid2, Show cid1) => Show (CompComorphism cid1 cid2) Source # 

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 # 

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 # 

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 #

(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 # 

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

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 # 
(Data sublogics, Data lid) => Data (InclComorphism lid sublogics) Source # 

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 :: (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 sublogics, Show lid) => Show (InclComorphism lid sublogics) Source # 

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 # 

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 # 

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 #

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, Monad 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 #

Instances

Comorphism HasCASL2HasCASL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism HasCASL2PCoClTyConsHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () 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 # 
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 # 
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 # 
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 # 
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 # 
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 # 
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 # 
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 # 
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 # 
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 # 
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 # 
Comorphism CFOL2IsabelleHOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism CoCFOL2IsabelleHOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism CSMOF2CASL CSMOF () Metamodel Sen () () Sign Morphism () () () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism QVTR2CASL QVTR () Transformation Sen () () Sign Morphism () () () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree 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 # 
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 # 
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 # 
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 # 
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 # 

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 #

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 # 
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 # 
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 # 
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 # 
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 # 
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 # 
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 # 
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 # 
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 # 
Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source # 
Comorphism THFP2THF0 THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source # 
Comorphism THFP_P2HasCASL THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism THFP_P2THFP THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree 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 # 
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 # 
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 # 
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 # 
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 # 
Comorphism CommonLogic2IsabelleHOL CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () 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 # 

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 #

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 # 
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 # 
Comorphism HolLight2Isabelle HolLight HolLightSL () Sentence () () Sign HolLightMorphism () () () Isabelle () () Sentence () () Sign IsabelleMorphism () () () 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 # 
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 # 
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 # 
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 # 
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 # 
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 # 
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 # 
Comorphism DMU2OWL2 DMU () Text () () () Text (DefaultMorphism Text) () () () OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree 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 # 
(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 # 

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 #

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 # 

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 #

(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 # 

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

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 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

isWeaklyAmalgamable :: AnyComorphism -> Bool Source #

Test whether a comorphism is weakly amalgamable

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

Compose comorphisms