Morphism.hs revision ad270004874ce1d0697fb30d7309f180553bb315
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederModule : $Header$
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederDescription : interface (type class) for logic projections (morphisms) in Hets
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : till@tzi.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederPortability : non-portable (via Logic)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederInterface (type class) for logic projections (morphisms) in Hets
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian MaederProvides data structures for institution morphisms.
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder These are just collections of
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder functions between (some of) the types of logics.
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder{- References: see Logic.hs
a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettich morphism modifications / representation maps
9dac90ec2be2a72e03893095461960d483fe2fc2Christian Maederimport qualified Data.Set as Set
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maederclass (Language cid,
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder Logic lid1 sublogics1
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
a1ed34933c266ce85066acb0d7b20c90cb8eb213Christian Maeder Logic lid2 sublogics2
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder | cid -> lid1, cid -> lid2
8ef75f1cc0437656bf622cec5ac9e8ea221da8f2Christian Maeder -- source and target logic and sublogic
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich -- the source sublogic is the maximal one for which the comorphism works
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -- the target sublogic is the resulting one
74eed04be26f549d2f7ca35c370e1c03879b28b1Christian Maeder morSourceLogic :: cid -> lid1
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder morSourceSublogic :: cid -> sublogics1
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder morTargetLogic :: cid -> lid2
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder morTargetSublogic :: cid -> sublogics2
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -- finer information of target sublogics corresponding to source sublogics
e593b89bfd4952698dc37feced21cefe869d87a2Christian Maeder morMapSublogic :: cid -> sublogics1 -> sublogics2
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -- default implementation
f38b3687c5558128515e34fb85d8b466d22dc300Christian Maeder-- morMapSublogic cid _ = targetSublogic cid
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder -- the translation functions are partial
7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maeder -- because the target may be a sublanguage
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder -- map_basic_spec :: cid -> basic_spec1 -> Maybe basic_spec2
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder -- we do not cover theoroidal morphisms,
51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maeder -- since there are no relevant examples and they do not compose nicely
f041c9a6bda23de33a38490e35b831ae18d96b45Christian Maeder -- no mapping of theories, since signatrures and sentences are mapped
7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maeder -- contravariantly
51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maeder morMap_sign :: cid -> sign1 -> Maybe sign2
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder morMap_morphism :: cid -> morphism1 -> Maybe morphism2
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder morMap_sentence :: cid -> sign1 -> sentence2 -> Maybe sentence1
c3053d57f642ca507cdf79512e604437c4546cb9Christian Maeder -- also covers semi-morphisms ??
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder -- with no sentence translation
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder -- - but these are spans!
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder morMap_symbol :: cid -> symbol1 -> Set.Set symbol2
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder -- morConstituents not needed, because composition only via lax triangles
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder-- identity morphisms
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maederdata IdMorphism lid sublogics =
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder IdMorphism lid sublogics deriving Show
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian MaederidMorphismTc :: TyCon
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian MaederidMorphismTc = mkTyCon "Logic.Morphism.IdMorphism"
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian Maederinstance Typeable (IdMorphism lid sub) where
8cacad2a09782249243b80985f28e9387019fe40Christian Maeder typeOf _ = mkTyConApp idMorphismTc []
a7c27282e71cf4505026645f96d4f5cb8a284e32Christian Maederinstance Logic lid sublogics
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder basic_spec sentence symb_items symb_map_items
8a28707e9155465c6f2236a06eac6580a65c7025Christian Maeder sign morphism symbol raw_symbol proof_tree =>
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich Language (IdMorphism lid sublogics) where
797ccd67cb8ae127be097cd43448801b673e3b69Christian Maeder language_name (IdMorphism lid sub) =
797ccd67cb8ae127be097cd43448801b673e3b69Christian Maeder case sublogic_names sub of
431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maeder [] -> error "language_name IdMorphism"
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder h : _ -> "id_" ++ language_name lid ++ "." ++ h
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maederinstance Logic lid sublogics
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder basic_spec sentence symb_items symb_map_items
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder sign morphism symbol raw_symbol proof_tree =>
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder Morphism (IdMorphism lid sublogics)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder lid sublogics
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder basic_spec sentence symb_items symb_map_items
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder sign morphism symbol raw_symbol proof_tree
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder lid sublogics
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder basic_spec sentence symb_items symb_map_items
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder sign morphism symbol raw_symbol proof_tree
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder morSourceLogic (IdMorphism lid _sub) = lid
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder morTargetLogic (IdMorphism lid _sub) = lid
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder morSourceSublogic (IdMorphism _lid sub) = sub
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder morTargetSublogic (IdMorphism _lid sub) = sub
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder morMapSublogic _ _ =
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder error "Logic.Morphism.IdMorphism.morMapSublogic"
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder morMap_sign _ = Just
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder morMap_morphism _ = Just
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder morMap_sentence _ = \_ -> Just
a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian Maeder morMap_symbol _ = Set.singleton
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder-- composition not needed, use lax triangles instead
51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maeder-- comorphisms inducing morphisms
2d130d212db7208777ca896a7ecad619a8944971Christian Maederclass Comorphism cid
bc8cbf12aa172bf5673b92a9e7a0151d4aa4c315Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2 =>
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder InducingComorphism cid
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder indMorMap_sign :: cid -> sign2 -> Maybe sign1
a9b59eb2ce961014974276cdae0e9df4419bd212Christian Maeder indMorMap_morphism :: cid -> morphism2 -> Maybe morphism1
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder epsilon :: cid -> sign2 -> Maybe morphism2