Comorphism.hs revision 9a36df4f63e0214bc0b4aef9b388c8d4e48632bb
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
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski comorphism maps
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski comorphisms out of sublogic relationships
38f350357e92da312d2c344352180b3dc5c1fc8aTill Mossakowskiimport Common.AS_Annotation (Named, mapNamedM)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- Logic comorphisms (possibly also morphisms via adjointness)
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
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski sourceLogic :: cid -> lid1
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski sourceSublogic :: cid -> sublogics1
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski targetLogic :: cid -> lid2
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski targetSublogic :: cid -> sublogics2
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
5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowski sens'' <- mapM (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
425b287f28abf82702d46c176a38b668fb017ce4Felix Reckers fromShATerm_sign1 :: (ATermConvertible sign) => cid -> ATermTable -> sign
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder fromShATerm_sign1 _ att = fromShATerm att
425b287f28abf82702d46c176a38b668fb017ce4Felix Reckers fromShATerm_morphism2 :: (ATermConvertible morphism) => cid -> ATermTable -> morphism
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder fromShATerm_morphism2 _ att = fromShATerm att
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidata IdComorphism lid =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski IdComorphism lid deriving Show
8db2d2c5a8df6dd6d7302bc59577150b87237940Till MossakowskiidComorphismTc :: TyCon
8db2d2c5a8df6dd6d7302bc59577150b87237940Till MossakowskiidComorphismTc = mkTyCon "Logic.Comorphism.IdComorphism"
8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowskiinstance Typeable (IdComorphism lid) 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 =>
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Language (IdComorphism lid) where
230a51f3c282a3222d1cf40c2040fee19259964eTill Mossakowski language_name (IdComorphism lid) =
230a51f3c282a3222d1cf40c2040fee19259964eTill Mossakowski "id_"++language_name lid
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance Logic lid sublogics
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec sentence symb_items symb_map_items
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign morphism symbol raw_symbol proof_tree =>
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Comorphism (IdComorphism 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 lid sublogics
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec sentence symb_items symb_map_items
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign morphism symbol raw_symbol proof_tree
5e21bb46b24f477dafad6fdeff51aed7aaad0a47Till Mossakowski sourceLogic (IdComorphism lid) = lid
5e21bb46b24f477dafad6fdeff51aed7aaad0a47Till Mossakowski targetLogic (IdComorphism lid) = lid
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski sourceSublogic _ = top
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski targetSublogic _ = top
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'))
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)))