hets/Logic/Comorphism.hs

	Comorphism.hs revision ca8550c6d47234042130bdc10a152806ecbc9832
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder{-|
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederModule      :  $Header$
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederCopyright   :  (c) Till Mossakowski, Uni Bremen 2002-2004
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederLicence     :  similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederMaintainer  :  hets@tzi.de
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederStability   :  provisional
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederPortability :  non-portable (via Logic)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
44fb55f639914f4f531641f32dd4904f15c510a4Till Mossakowski   Provides data structures for institution comorphisms.
44fb55f639914f4f531641f32dd4904f15c510a4Till Mossakowski   These are just collections of
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski   functions between (some of) the types of logics.
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder-}
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder{-   References: see Logic.hs
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski   Todo:
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski   Weak amalgamability, also for comorphisms
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski   comorphism modifications
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski   comorphisms out of sublogic relationships
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski   restrictions of comorphisms to sublogics
ae7058143db9e9993b5eff70bd6b7aede7cec658Till Mossakowski   morphisms and other translations via spans
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-}
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskimodule Logic.Comorphism where
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport Logic.Logic
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport Common.Lib.Set
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maederimport Common.Result
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maederimport Data.Maybe
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport Data.Dynamic
9e2e744c6b967c3f5f581acf01c13769b6769285Till Mossakowskiimport Common.DynamicUtils
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maederimport Common.AS_Annotation
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maederclass (Language cid,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski       Logic lid1 sublogics1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski        basic_spec1 sentence1 symb_items1 symb_map_items1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski        sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski       Logic lid2 sublogics2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski        basic_spec2 sentence2 symb_items2 symb_map_items2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski        sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski  Comorphism cid
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski            lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski                sign1 morphism1 symbol1 raw_symbol1 proof_tree1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski            lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski                sign2 morphism2 symbol2 raw_symbol2 proof_tree2
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder             | cid -> lid1, cid -> lid2
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski  where
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski    -- source and target logic and sublogic
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski    -- the source sublogic is the maximal one for which the comorphism works
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski    -- the target sublogic is the resulting one
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski    sourceLogic :: cid -> lid1
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski    sourceSublogic :: cid -> sublogics1
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski    targetLogic :: cid -> lid2
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski    targetSublogic :: cid -> sublogics2
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski    -- finer information of target sublogics corresponding to source sublogics
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski    mapSublogic :: cid -> sublogics1 -> sublogics2
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski    -- default implementation
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski    mapSublogic cid _ = targetSublogic cid
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski    -- the translation functions are partial
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski    -- because the target may be a sublanguage
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder    -- map_basic_spec :: cid -> basic_spec1 -> Result basic_spec2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski    -- cover theoroidal comorphisms as well
5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowski    map_theory :: cid -> (sign1,[Named sentence1])
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder                      -> Result (sign2,[Named sentence2])
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder    map_morphism :: cid -> morphism1 -> Result morphism2
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder    map_sentence :: cid -> sign1 -> sentence1 -> Result sentence2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski          -- also covers semi-comorphisms
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski          -- with no sentence translation
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski          -- - but these are spans!
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski    map_symbol :: cid -> symbol1 -> Set symbol2
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski    constituents :: cid -> [String]
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski    -- default implementation
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski    constituents cid = [language_name cid]
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maedermap_sign :: Comorphism cid
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder            lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder                sign1 morphism1 symbol1 raw_symbol1 proof_tree1
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder            lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder                sign2 morphism2 symbol2 raw_symbol2 proof_tree2
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder         => cid -> sign1 -> Result (sign2,[Named sentence2])
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maedermap_sign cid sign = map_theory cid (sign,[])
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder
19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaedersimpleTheoryMapping :: (sign1 -> sign2) -> (sentence1 -> sentence2)
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder                    -> (sign1, [Named sentence1])
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder                    -> (sign2, [Named sentence2])
19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaedersimpleTheoryMapping mapSig mapSen (sign,sens) =
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder    (mapSig sign, map (mapNamed mapSen) sens)
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder
19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaedermkTheoryMapping :: (Monad m) => (sign1 -> m (sign2, [Named sentence2]))
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder           -> (sign1 -> sentence1 -> m sentence2)
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder                   -> (sign1, [Named sentence1])
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder                   -> m (sign2, [Named sentence2])
19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaedermkTheoryMapping mapSig mapSen (sign,sens) = do
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder       (sign',sens') <- mapSig sign
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder       sens'' <- mapM (mapNamedM $ mapSen sign) sens
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder       return (sign',sens'++sens'')
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder
586af0e9490a14dd3075095692b584c652584875Till Mossakowskidata IdComorphism lid sublogics =
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski     IdComorphism lid sublogics
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowskiinstance Logic lid sublogics
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski        basic_spec sentence symb_items symb_map_items
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski        sign morphism symbol raw_symbol proof_tree =>
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski   Show (IdComorphism lid sublogics)
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski   where
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski   show = language_name
933baca0720dae81434de384b32a93b47e754d09Christian Maeder
8db2d2c5a8df6dd6d7302bc59577150b87237940Till MossakowskiidComorphismTc :: TyCon
8db2d2c5a8df6dd6d7302bc59577150b87237940Till MossakowskiidComorphismTc = mkTyCon "Logic.Comorphism.IdComorphism"
933baca0720dae81434de384b32a93b47e754d09Christian Maeder
586af0e9490a14dd3075095692b584c652584875Till Mossakowskiinstance Typeable (IdComorphism lid sub) where
59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maeder  typeOf _ = mkTyConApp idComorphismTc []
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance Logic lid sublogics
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski        basic_spec sentence symb_items symb_map_items
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski        sign morphism symbol raw_symbol proof_tree =>
586af0e9490a14dd3075095692b584c652584875Till Mossakowski         Language (IdComorphism lid sublogics) where
586af0e9490a14dd3075095692b584c652584875Till Mossakowski           language_name (IdComorphism lid sub) =
933baca0720dae81434de384b32a93b47e754d09Christian Maeder               case sublogic_names lid sub of
933baca0720dae81434de384b32a93b47e754d09Christian Maeder               [] -> error "language_name IdComorphism"
933baca0720dae81434de384b32a93b47e754d09Christian Maeder               h : _ -> "id_" ++ language_name lid ++ "." ++ h
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance Logic lid sublogics
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski        basic_spec sentence symb_items symb_map_items
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski        sign morphism symbol raw_symbol proof_tree =>
586af0e9490a14dd3075095692b584c652584875Till Mossakowski         Comorphism (IdComorphism lid sublogics)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski          lid sublogics
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski          basic_spec sentence symb_items symb_map_items
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski          sign morphism symbol raw_symbol proof_tree
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski          lid sublogics
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski          basic_spec sentence symb_items symb_map_items
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski          sign morphism symbol raw_symbol proof_tree
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski         where
933baca0720dae81434de384b32a93b47e754d09Christian Maeder           sourceLogic (IdComorphism lid _sub) = lid
933baca0720dae81434de384b32a93b47e754d09Christian Maeder           targetLogic (IdComorphism lid _sub) = lid
933baca0720dae81434de384b32a93b47e754d09Christian Maeder           sourceSublogic (IdComorphism _lid sub) = sub
933baca0720dae81434de384b32a93b47e754d09Christian Maeder           targetSublogic (IdComorphism _lid sub) = sub
f2a87c712ea3cd13f86a95cae738f861f6c4a908Till Mossakowski           mapSublogic _ = id
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder           map_theory _ = return
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder           map_morphism _ = return
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder           map_sentence _ = \_ -> return
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski           map_symbol _ = single
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski           constituents _ = []
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maederdata CompComorphism cid1 cid2 = CompComorphism cid1 cid2 deriving Show
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskityconCompComorphism :: TyCon
8db2d2c5a8df6dd6d7302bc59577150b87237940Till MossakowskityconCompComorphism = mkTyCon "Logic.Comorphism.CompComorphism"
933baca0720dae81434de384b32a93b47e754d09Christian Maeder
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maederinstance Typeable (CompComorphism cid1 cid2) where
59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maeder  typeOf _ = mkTyConApp tyconCompComorphism []
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
ca8550c6d47234042130bdc10a152806ecbc9832Christian Maederinstance (Language cid1, Language cid2)
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder          => Language (CompComorphism cid1 cid2) where
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski   language_name (CompComorphism cid1 cid2) =
ca8550c6d47234042130bdc10a152806ecbc9832Christian Maeder     language_name cid1++ ";" ++language_name cid2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance (Comorphism cid1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski            lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski                sign1 morphism1 symbol1 raw_symbol1 proof_tree1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski            lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski                sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski          Comorphism cid2
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder            lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder                sign4 morphism4 symbol4 raw_symbol4 proof_tree4
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski            lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski                sign3 morphism3 symbol3 raw_symbol3 proof_tree3)
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder          => Comorphism (CompComorphism cid1 cid2)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski              lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski              sign1 morphism1 symbol1 raw_symbol1 proof_tree1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski              lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder              sign3 morphism3 symbol3 raw_symbol3 proof_tree3 where
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski   sourceLogic (CompComorphism cid1 _) =
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski     sourceLogic cid1
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski   targetLogic (CompComorphism _ cid2) =
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski     targetLogic cid2
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski   sourceSublogic (CompComorphism cid1 _) =
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski     sourceSublogic cid1
f2a87c712ea3cd13f86a95cae738f861f6c4a908Till Mossakowski   targetSublogic (CompComorphism cid1 cid2) =
f2a87c712ea3cd13f86a95cae738f861f6c4a908Till Mossakowski     mapSublogic cid2
f2a87c712ea3cd13f86a95cae738f861f6c4a908Till Mossakowski      (idcoerce (targetLogic cid1) (sourceLogic cid2)
f2a87c712ea3cd13f86a95cae738f861f6c4a908Till Mossakowski        (targetSublogic cid1))
f2a87c712ea3cd13f86a95cae738f861f6c4a908Till Mossakowski   mapSublogic (CompComorphism cid1 cid2) =
f2a87c712ea3cd13f86a95cae738f861f6c4a908Till Mossakowski     mapSublogic cid2
f2a87c712ea3cd13f86a95cae738f861f6c4a908Till Mossakowski     . idcoerce (targetLogic cid1) (sourceLogic cid2)
f2a87c712ea3cd13f86a95cae738f861f6c4a908Till Mossakowski     . mapSublogic cid1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski   map_sentence (CompComorphism cid1 cid2) =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski       \si1 se1 ->
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski         do (si2,_) <- map_sign cid1 si1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski            se2 <- map_sentence cid1 si1 se1
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder            (si2', se2') <- mcoerce (targetLogic cid1) (sourceLogic cid2)
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder                            "Mapping sentence along comorphism" (si2, se2)
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder            map_sentence cid2 si2' se2'
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder   map_theory (CompComorphism cid1 cid2) =
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder       \ti1 ->
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder         do ti2 <- map_theory cid1 ti1
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski            ti2' <- mcoerce (targetLogic cid1) (sourceLogic cid2)
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski                        "Mapping theory along comorphism" ti2
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder            map_theory cid2 ti2'
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder   map_morphism (CompComorphism cid1 cid2) = \ m1 ->
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder       do m2 <- map_morphism cid1 m1
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder          m3 <- mcoerce (targetLogic cid1) (sourceLogic cid2)
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski                  "Mapping signature morphism along comorphism"m2
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder          map_morphism cid2 m3
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder   map_symbol (CompComorphism cid1 cid2) = \ s1 ->
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski         let mycast = fromJust . mcoerce (targetLogic cid1) (sourceLogic cid2)
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski                                  "Mapping symbol along comorphism"
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder         in unions
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder                (map (map_symbol cid2 . mycast)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski                 (toList (map_symbol cid1 s1)))
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski   constituents (CompComorphism cid1 cid2) =
933baca0720dae81434de384b32a93b47e754d09Christian Maeder      constituents cid1 ++ constituents cid2