Comorphism.hs revision bba825b39570777866d560bfde3807731131097e
c1d71ac637c449feb0a25369f029397e6a1f241cChristian Maeder{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederModule : $Header$
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian MaederDescription : central interface (type class) for logic translations (comorphisms) in Hets
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaederCopyright : (c) Till Mossakowski, Uni Bremen 2002-2006
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : till@tzi.de
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederStability : provisional
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederPortability : non-portable (via Logic)
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian MaederCentral interface (type class) for logic translations (comorphisms) in Hets
44fb55f639914f4f531641f32dd4904f15c510a4Till Mossakowski These are just collections of
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski functions between (some of) the types of logics.
af0cbe339851fc558d2b18cde3666981325e667cTill Mossakowski References: see Logic.hs
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport qualified Data.Set as Set
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederclass (Language cid,
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Logic lid1 sublogics1
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Logic lid2 sublogics2
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Comorphism cid
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder | cid -> lid1, cid -> lid2
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder -- source and target logic and sublogic
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder -- the source sublogic is the maximal one for which the comorphism works
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder sourceLogic :: cid -> lid1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sourceSublogic :: cid -> sublogics1
59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maeder targetLogic :: cid -> lid2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- finer information of target sublogics corresponding to source sublogics
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- this function must be partial because mapTheory is partial
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski mapSublogic :: cid -> sublogics1 -> Maybe sublogics2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- the translation functions are partial
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder -- because the target may be a sublanguage
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- map_basic_spec :: cid -> basic_spec1 -> Result basic_spec2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- cover theoroidal comorphisms as well
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_theory :: cid -> (sign1,[Named sentence1])
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -> Result (sign2,[Named sentence2])
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_morphism :: cid -> morphism1 -> Result morphism2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_sentence :: cid -> sign1 -> sentence1 -> Result sentence2
2b565fe5cfb9f99857fd25b52304758d8544e266Mihai Codescu -- also covers semi-comorphisms
2b565fe5cfb9f99857fd25b52304758d8544e266Mihai Codescu -- with no sentence translation
2b565fe5cfb9f99857fd25b52304758d8544e266Mihai Codescu -- - but these are spans!
2b565fe5cfb9f99857fd25b52304758d8544e266Mihai Codescu map_symbol :: cid -> symbol1 -> Set.Set symbol2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski --properties of comorphisms
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski is_model_transportable :: cid -> Bool
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski -- a comorphism (\phi, \alpha, \beta) is model-transportable
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski -- if for any signature \Sigma, any \Sigma-model M and any \phi(\Sigma)-model N
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski -- for any isomorphism h : \beta_\Sigma(N) -> M
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski -- there exists an isomorphism h': N -> M' such that \beta_\Sigma(h') = h
bba825b39570777866d560bfde3807731131097eKlaus Luettich has_model_expansion :: cid -> Bool
bba825b39570777866d560bfde3807731131097eKlaus Luettich is_weakly_amalgamable :: cid -> Bool
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder --default implementation for properties
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski is_model_transportable _ = False
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder has_model_expansion _ = False
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski is_weakly_amalgamable _ = False
5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowski constituents :: cid -> [String]
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder -- default implementation
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder constituents cid = [language_name cid]
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskitargetSublogic :: Comorphism cid
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1
0647a6c86b231e391826c7715338ba29cb4934c0Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu sign2 morphism2 symbol2 raw_symbol2 proof_tree2
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu => cid -> sublogics2
a98fd29a06e80e447af26d898044c23497adbc73Mihai CodescutargetSublogic cid = maybe (error ("Logic.Comorphism: " ++
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu language_name cid ++
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu " does not provide a mapping for it's " ++
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu "source sublogic"))
da955132262baab309a50fdffe228c9efe68251dCui Jian id $ mapSublogic cid $ sourceSublogic cid
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu-- | this function is base on 'map_theory' using no sentences as input
f2c050360525df494e6115073b0edc4c443a847cMihai Codescumap_sign :: Comorphism cid
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu sign1 morphism1 symbol1 raw_symbol1 proof_tree1
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski => cid -> sign1 -> Result (sign2,[Named sentence2])
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowskimap_sign cid sign = wrapMapTheory cid (sign,[])
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus LuettichmapDefaultMorphism :: Comorphism cid
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder => cid -> morphism1 -> Result morphism2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedermapDefaultMorphism cid mor = do
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder let src = sourceLogic cid
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder (sig1, _) <- map_sign cid $ dom src mor
da955132262baab309a50fdffe228c9efe68251dCui Jian (sig2, _) <- map_sign cid $ cod src mor
da955132262baab309a50fdffe228c9efe68251dCui Jian inclusion (targetLogic cid) sig1 sig2
da955132262baab309a50fdffe228c9efe68251dCui JianfailMapSentence :: Comorphism cid
bba825b39570777866d560bfde3807731131097eKlaus Luettich lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder => cid -> sign1 -> sentence1 -> Result sentence2
19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaederfailMapSentence cid _ _ =
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder fail $ "Unsupported sentence translation " ++ show cid
19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaedererrMapSymbol :: Comorphism cid
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder => cid -> symbol1 -> Set.Set symbol2
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedererrMapSymbol cid _ = error $ "no symbol mapping for " ++ show cid
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder-- | use this function instead of 'map_theory'
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederwrapMapTheory :: Comorphism cid
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder => cid -> (sign1, [Named sentence1])
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder -> Result (sign2, [Named sentence2])
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaederwrapMapTheory cid (sign, sens) =
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder case sourceSublogic cid of
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder sub -> case minSublogic sign of
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder sigLog -> case foldl join sigLog
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder $ map (minSublogic . sentence) sens of
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder if isSubElem senLog sub
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder then map_theory cid (sign, sens)
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder else fail $ "for '" ++ language_name cid ++
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder "' expected sublogic '" ++
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder concat (sublogic_names sub) ++
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder "'\n but found sublogic '" ++
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder concat (sublogic_names senLog) ++
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder "' with signature sublogic '" ++
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder concat (sublogic_names sigLog) ++ "'\n" ++
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder show (vcat $ pretty sign : map
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder (print_named $ sourceLogic cid) sens)
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedersimpleTheoryMapping :: (sign1 -> sign2) -> (sentence1 -> sentence2)
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder -> (sign1, [Named sentence1])
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder -> (sign2, [Named sentence2])
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedersimpleTheoryMapping mapSig mapSen (sign,sens) =
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder (mapSig sign, map (mapNamed mapSen) sens)
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedermkTheoryMapping :: (Monad m) => (sign1 -> m (sign2, [Named sentence2]))
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder -> (sign1 -> sentence1 -> m sentence2)
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder -> (sign1, [Named sentence1])
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder -> m (sign2, [Named sentence2])
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian MaedermkTheoryMapping mapSig mapSen (sign,sens) = do
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder (sign',sens') <- mapSig sign
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder sens'' <- mapM (mapNamedM $ mapSen sign) sens
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder return (sign', disambiguateSens Set.empty . nameSens $ sens' ++ sens'')
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maederdata IdComorphism lid sublogics =
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder IdComorphism lid sublogics
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maederinstance Logic lid sublogics
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder basic_spec sentence symb_items symb_map_items
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder sign morphism symbol raw_symbol proof_tree =>
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder Show (IdComorphism lid sublogics)
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder show = language_name
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maederinstance Logic lid sublogics
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder basic_spec sentence symb_items symb_map_items
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder sign morphism symbol raw_symbol proof_tree =>
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder Language (IdComorphism lid sublogics) where
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder language_name (IdComorphism lid sub) =
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder case sublogic_names sub of
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder [] -> error "language_name IdComorphism"
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder h : _ -> "id_" ++ language_name lid ++ "." ++ h
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maederinstance Logic lid sublogics
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder basic_spec sentence symb_items symb_map_items
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder sign morphism symbol raw_symbol proof_tree =>
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder Comorphism (IdComorphism lid sublogics)
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder lid sublogics
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder basic_spec sentence symb_items symb_map_items
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder sign morphism symbol raw_symbol proof_tree
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder lid sublogics
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder basic_spec sentence symb_items symb_map_items
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder sign morphism symbol raw_symbol proof_tree
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder sourceLogic (IdComorphism lid _sub) = lid
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder targetLogic (IdComorphism lid _sub) = lid
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder sourceSublogic (IdComorphism _lid sub) = sub
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder mapSublogic _ = Just . id
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder map_theory _ = return
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich map_morphism _ = return
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich map_sentence _ = \_ -> return
da955132262baab309a50fdffe228c9efe68251dCui Jian map_symbol _ = Set.singleton
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich constituents _ = []
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich is_model_transportable _ = True
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich has_model_expansion _ = True
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich is_weakly_amalgamable _ = True
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettichdata CompComorphism cid1 cid2 = CompComorphism cid1 cid2 deriving Show
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettichinstance (Language cid1, Language cid2)
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich => Language (CompComorphism cid1 cid2) where
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich language_name (CompComorphism cid1 cid2) =
da955132262baab309a50fdffe228c9efe68251dCui Jian language_name cid1++ ";" ++language_name cid2
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettichinstance (Comorphism cid1
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich sign1 morphism1 symbol1 raw_symbol1 proof_tree1
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich Comorphism cid2
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich sign4 morphism4 symbol4 raw_symbol4 proof_tree4
da955132262baab309a50fdffe228c9efe68251dCui Jian lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich sign3 morphism3 symbol3 raw_symbol3 proof_tree3)
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich => Comorphism (CompComorphism cid1 cid2)
da955132262baab309a50fdffe228c9efe68251dCui Jian lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich sign1 morphism1 symbol1 raw_symbol1 proof_tree1
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich sign3 morphism3 symbol3 raw_symbol3 proof_tree3 where
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich sourceLogic (CompComorphism cid1 _) =
da955132262baab309a50fdffe228c9efe68251dCui Jian sourceLogic cid1
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich targetLogic (CompComorphism _ cid2) =
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich targetLogic cid2
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich sourceSublogic (CompComorphism cid1 _) =
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski sourceSublogic cid1
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski mapSublogic (CompComorphism cid1 cid2) sl =
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski mapSublogic cid1 sl >>=
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski (\ y -> mapSublogic cid2 $
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich forceCoerceSublogic (targetLogic cid1) (sourceLogic cid2) y)
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder map_sentence (CompComorphism cid1 cid2) =
933baca0720dae81434de384b32a93b47e754d09Christian Maeder do (si2,_) <- map_sign cid1 si1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski se2 <- map_sentence cid1 si1 se1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (si2', se2') <- coerceBasicTheory
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (targetLogic cid1) (sourceLogic cid2)
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich "Mapping sentence along comorphism" (si2, [makeNamed "" se2])
da955132262baab309a50fdffe228c9efe68251dCui Jian [x] -> map_sentence cid2 si2' $ sentence x
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich map_theory (CompComorphism cid1 cid2) =
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich do ti2 <- map_theory cid1 ti1
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich ti2' <- coerceBasicTheory (targetLogic cid1) (sourceLogic cid2)
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich "Mapping theory along comorphism" ti2
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich wrapMapTheory cid2 ti2'
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_morphism (CompComorphism cid1 cid2) = \ m1 ->
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski do m2 <- map_morphism cid1 m1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski m3 <- coerceMorphism (targetLogic cid1) (sourceLogic cid2)
586af0e9490a14dd3075095692b584c652584875Till Mossakowski "Mapping signature morphism along comorphism"m2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_morphism cid2 m3
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_symbol (CompComorphism cid1 cid2) = \ s1 ->
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski let mycast = coerceSymbol (targetLogic cid1) (sourceLogic cid2)
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder (map (map_symbol cid2 . mycast)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (Set.toList (map_symbol cid1 s1)))
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich constituents (CompComorphism cid1 cid2) =
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich constituents cid1 ++ constituents cid2
da955132262baab309a50fdffe228c9efe68251dCui Jian is_model_transportable (CompComorphism cid1 cid2) =
da955132262baab309a50fdffe228c9efe68251dCui Jian is_model_transportable cid1 && is_model_transportable cid2
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich has_model_expansion (CompComorphism cid1 cid2) =
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder has_model_expansion cid1 && has_model_expansion cid2
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder is_weakly_amalgamable (CompComorphism cid1 cid2) =
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder is_weakly_amalgamable cid1 && is_weakly_amalgamable cid2