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

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

(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

(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

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

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

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

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

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

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

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

Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Instance details

Defined in Comorphisms.MonadicHasCASLTranslation

Comorphism HolLight2Isabelle HolLight HolLightSL () Sentence () () Sign HolLightMorphism () () () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Instance details

Defined in Comorphisms.HolLight2Isabelle

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

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

Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Instance details

Defined in Comorphisms.HasCASL2IsabelleHOL

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(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

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

Ord AnyComorphism Source # 
Instance details

Defined in Logic.Comorphism

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

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

isWeaklyAmalgamable :: AnyComorphism -> Bool Source #

Test whether a comorphism is weakly amalgamable

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

Compose comorphisms