Comorphism.hs revision a89e661aad28f1b39f4fc9f9f9a4d46074234123
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederModule : $Header$
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian MaederCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiMaintainer : hets@tzi.de
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederStability : provisional
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederPortability : non-portable (via Logic)
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder 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{- References: see Logic.hs
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
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maederimport Common.AS_Annotation (Named, mapNamedM)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiclass (Language cid,
59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maeder 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
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder 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
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski | cid -> lid1, cid -> lid2
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski -- source and target logic and sublogic
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski -- the source sublogic is the maximal one for which the comorphism works
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski -- the target sublogic is the resulting one
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski sourceLogic :: cid -> lid1
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski sourceSublogic :: cid -> sublogics1
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski targetLogic :: cid -> lid2
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski targetSublogic :: cid -> sublogics2
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder -- finer information of target sublogics corresponding to source sublogics
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski mapSublogic :: cid -> sublogics1 -> sublogics2
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder -- default implementation
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski mapSublogic cid _ = targetSublogic cid
5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowski -- the translation functions are partial
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder -- because the target may be a sublanguage
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder -- map_basic_spec :: cid -> basic_spec1 -> Result basic_spec2
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder -- cover theoroidal comorphisms as well
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_sign :: cid -> sign1 -> Result (sign2,[Named sentence2])
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_theory :: cid -> (sign1,[Named sentence1])
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -> Result (sign2,[Named sentence2])
0647a6c86b231e391826c7715338ba29cb4934c0Christian Maeder --default implementations
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski map_sign cid sign = map_theory cid (sign,[])
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski map_theory cid (sign,sens) = do
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski (sign',sens') <- map_sign cid sign
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sens'' <- mapM (mapNamedM $ map_sentence cid sign) sens
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder return (sign',sens'++sens'')
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder map_morphism :: cid -> morphism1 -> Result morphism2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder map_sentence :: cid -> sign1 -> sentence1 -> Result sentence2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder -- also covers semi-comorphisms
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder -- with no sentence translation
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder -- - but these are spans!
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder map_symbol :: cid -> symbol1 -> Set symbol2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder constituents :: cid -> [String]
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder -- default implementation
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder constituents cid = [language_name cid]
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maederdata IdComorphism lid sublogics =
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder IdComorphism lid sublogics deriving Show
19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaederidComorphismTc :: TyCon
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian MaederidComorphismTc = mkTyCon "Logic.Comorphism.IdComorphism"
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederinstance Typeable (IdComorphism lid sub) where
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder typeOf _ = mkTyConApp idComorphismTc []
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederinstance Logic lid sublogics
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder basic_spec sentence symb_items symb_map_items
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder sign morphism symbol raw_symbol proof_tree =>
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder Language (IdComorphism lid sublogics) where
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder language_name (IdComorphism lid sub) =
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder case sublogic_names lid sub of
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder [] -> error "language_name IdComorphism"
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder h : _ -> "id_" ++ language_name lid ++ "." ++ h
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederinstance Logic lid sublogics
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder basic_spec sentence symb_items symb_map_items
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder sign morphism symbol raw_symbol proof_tree =>
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder Comorphism (IdComorphism lid sublogics)
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder lid sublogics
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder basic_spec sentence symb_items symb_map_items
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder sign morphism symbol raw_symbol proof_tree
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder lid sublogics
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder basic_spec sentence symb_items symb_map_items
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder sign morphism symbol raw_symbol proof_tree
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder sourceLogic (IdComorphism lid _sub) = lid
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder targetLogic (IdComorphism lid _sub) = lid
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder sourceSublogic (IdComorphism _lid sub) = sub
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder targetSublogic (IdComorphism _lid sub) = sub
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder map_sign _ = \sigma -> return (sigma,[])
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder map_morphism _ = return
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder map_sentence _ = \_ -> return
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder map_symbol _ = single
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder constituents _ = []
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maederdata CompComorphism cid1 cid2 = CompComorphism cid1 cid2 deriving Show
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaedertyconCompComorphism :: TyCon
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaedertyconCompComorphism = mkTyCon "Logic.Comorphism.CompComorphism"
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maederinstance Typeable (CompComorphism cid1 cid2) where
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder typeOf _ = mkTyConApp tyconCompComorphism []
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maederinstance (Comorphism cid1
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder Comorphism cid2
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder sign4 morphism4 symbol4 raw_symbol4 proof_tree4
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder sign3 morphism3 symbol3 raw_symbol3 proof_tree3)
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder => Language (CompComorphism cid1 cid2) where
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder language_name (CompComorphism cid1 cid2) =
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder language_name cid1++";"
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder ++language_name cid2
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maederinstance (Comorphism cid1
53310804002cd9e3c9c5844db3b984abcf001788Christian 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,
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder Comorphism cid2
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder sign4 morphism4 symbol4 raw_symbol4 proof_tree4
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder sign3 morphism3 symbol3 raw_symbol3 proof_tree3)
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder => Comorphism (CompComorphism cid1 cid2)
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder sign3 morphism3 symbol3 raw_symbol3 proof_tree3 where
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski sourceLogic (CompComorphism cid1 _) =
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski sourceLogic cid1
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski targetLogic (CompComorphism _ cid2) =
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski targetLogic cid2
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski sourceSublogic (CompComorphism cid1 _) =
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder sourceSublogic cid1
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski targetSublogic (CompComorphism _ cid2) =
933baca0720dae81434de384b32a93b47e754d09Christian Maeder targetSublogic cid2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_sentence (CompComorphism cid1 cid2) =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski do (si2,_) <- map_sign cid1 si1
586af0e9490a14dd3075095692b584c652584875Till Mossakowski se2 <- map_sentence cid1 si1 se1
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder (si2', se2') <- mcoerce (targetLogic cid1) (sourceLogic cid2)
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder "Mapping sentence along comorphism" (si2, se2)
933baca0720dae81434de384b32a93b47e754d09Christian Maeder map_sentence cid2 si2' se2'
933baca0720dae81434de384b32a93b47e754d09Christian Maeder map_sign (CompComorphism cid1 cid2) =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski do (si2, se2s) <- map_sign cid1 si1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (si2', se2s') <- mcoerce (targetLogic cid1) (sourceLogic cid2)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski "Mapping signature along comorphism"(si2, se2s)
586af0e9490a14dd3075095692b584c652584875Till Mossakowski (si3, se3s) <- map_sign cid2 si2'
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski se3s' <- mapM (mapNamedM $ map_sentence cid2 si2') se2s'
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski return (si3, se3s ++ se3s')
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_theory (CompComorphism cid1 cid2) =
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder do ti2 <- map_theory cid1 ti1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ti2' <- mcoerce (targetLogic cid1) (sourceLogic cid2)
933baca0720dae81434de384b32a93b47e754d09Christian Maeder "Mapping theory along comorphism" ti2
933baca0720dae81434de384b32a93b47e754d09Christian Maeder map_theory cid2 ti2'
f2a87c712ea3cd13f86a95cae738f861f6c4a908Till Mossakowski map_morphism (CompComorphism cid1 cid2) = \ m1 ->
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder do m2 <- map_morphism cid1 m1
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder m3 <- mcoerce (targetLogic cid1) (sourceLogic cid2)
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder "Mapping signature morphism along comorphism"m2
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder map_morphism cid2 m3
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_symbol (CompComorphism cid1 cid2) = \ s1 ->
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder let mycast = fromJust . mcoerce (targetLogic cid1) (sourceLogic cid2)
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder "Mapping symbol along comorphism"
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder (map (map_symbol cid2 . mycast)
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder (toList (map_symbol cid1 s1)))
ca8550c6d47234042130bdc10a152806ecbc9832Christian Maeder constituents (CompComorphism cid1 cid2) =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski constituents cid1 ++ constituents cid2