Comorphism.hs revision 9e2e744c6b967c3f5f581acf01c13769b6769285
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederModule : $Header$
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederMaintainer : hets@tzi.de
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederStability : provisional
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederPortability : non-portable (via Logic)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Provides data structures logic (co)morphisms.
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Logic (co)morphisms are just collections of
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski functions between (some of) the types of logics.
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder{- 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
38f350357e92da312d2c344352180b3dc5c1fc8aTill Mossakowskiimport Common.AS_Annotation (Named, mapNamedM)
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
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
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- map_basic_spec :: cid -> basic_spec1 -> Maybe basic_spec2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- cover theoroidal comorphisms as well
38f350357e92da312d2c344352180b3dc5c1fc8aTill Mossakowski map_sign :: cid -> sign1 -> Maybe (sign2,[Named sentence2])
5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowski map_theory :: cid -> (sign1,[Named sentence1])
5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowski -> Maybe (sign2,[Named sentence2])
9a36df4f63e0214bc0b4aef9b388c8d4e48632bbTill Mossakowski --default implementations
9a36df4f63e0214bc0b4aef9b388c8d4e48632bbTill Mossakowski map_sign cid sign = map_theory cid (sign,[])
5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowski map_theory cid (sign,sens) = do
5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowski (sign',sens') <- map_sign cid sign
62867c8459918ce0a96960093eb43d758b97a603Till Mossakowski let sens'' = mapMaybe (mapNamedM (map_sentence cid sign)) sens
5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowski return (sign',sens'++sens'')
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_morphism :: cid -> morphism1 -> Maybe morphism2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_sentence :: cid -> sign1 -> sentence1 -> Maybe 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
586af0e9490a14dd3075095692b584c652584875Till Mossakowskidata IdComorphism lid sublogics =
586af0e9490a14dd3075095692b584c652584875Till Mossakowski IdComorphism lid sublogics deriving Show
8db2d2c5a8df6dd6d7302bc59577150b87237940Till MossakowskiidComorphismTc :: TyCon
8db2d2c5a8df6dd6d7302bc59577150b87237940Till MossakowskiidComorphismTc = mkTyCon "Logic.Comorphism.IdComorphism"
586af0e9490a14dd3075095692b584c652584875Till Mossakowskiinstance Typeable (IdComorphism lid sub) where
59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maeder typeOf _ = mkTyConApp idComorphismTc []
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) =
586af0e9490a14dd3075095692b584c652584875Till Mossakowski "id_"++language_name lid++"."++show sub
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
586af0e9490a14dd3075095692b584c652584875Till Mossakowski sourceLogic (IdComorphism lid sub) = lid
586af0e9490a14dd3075095692b584c652584875Till Mossakowski targetLogic (IdComorphism lid sub) = lid
586af0e9490a14dd3075095692b584c652584875Till Mossakowski sourceSublogic (IdComorphism lid sub) = sub
586af0e9490a14dd3075095692b584c652584875Till Mossakowski targetSublogic (IdComorphism lid sub) = sub
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_sign _ = \sigma -> Just(sigma,[])
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_morphism _ = Just
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_sentence _ = \_ -> Just
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_symbol _ = single
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maederdata CompComorphism cid1 cid2 = CompComorphism cid1 cid2 deriving Show
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskityconCompComorphism :: TyCon
8db2d2c5a8df6dd6d7302bc59577150b87237940Till MossakowskityconCompComorphism = mkTyCon "Logic.Comorphism.CompComorphism"
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maederinstance Typeable (CompComorphism cid1 cid2) where
59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maeder typeOf _ = mkTyConApp tyconCompComorphism []
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 => Language (CompComorphism cid1 cid2) where
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski language_name (CompComorphism cid1 cid2) =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski language_name cid1++";"
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ++language_name cid2
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
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski targetSublogic (CompComorphism _ cid2) =
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski targetSublogic cid2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_sentence (CompComorphism cid1 cid2) =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski do (si2,_) <- map_sign cid1 si1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski se2 <- map_sentence cid1 si1 se1
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder (si2', se2') <- coerce (targetLogic cid1) (sourceLogic cid2)
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder map_sentence cid2 si2' se2'
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_sign (CompComorphism cid1 cid2) =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski do (si2, se2s) <- map_sign cid1 si1
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder (si2', se2s') <- coerce (targetLogic cid1) (sourceLogic cid2)
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder (si3, se3s) <- map_sign cid2 si2'
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski return (si3, se3s ++ catMaybes
38f350357e92da312d2c344352180b3dc5c1fc8aTill Mossakowski (map (mapNamedM (map_sentence cid2 si2')) se2s'))
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder map_theory (CompComorphism cid1 cid2) =
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder do ti2 <- map_theory cid1 ti1
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder ti2' <- coerce (targetLogic cid1) (sourceLogic cid2) ti2
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder map_theory cid2 ti2'
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder map_morphism (CompComorphism cid1 cid2) = \ m1 ->
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder do m2 <- map_morphism cid1 m1
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder m3 <- coerce (targetLogic cid1) (sourceLogic cid2) m2
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder map_morphism cid2 m3
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder map_symbol (CompComorphism cid1 cid2) = \ s1 ->
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder let mycast = fromJust . coerce (targetLogic cid1) (sourceLogic cid2)
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder (map (map_symbol cid2 . mycast)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (toList (map_symbol cid1 s1)))