Morphism.hs revision 797595aad6dfd626bc1c9df52616f1ac4235c669
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina Sojakova{-|
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina Sojakova
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina SojakovaModule : $Header$
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina SojakovaCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina Sojakova
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina SojakovaMaintainer : hets@tzi.de
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina SojakovaStability : provisional
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina SojakovaPortability : non-portable (via Logic)
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina Sojakova
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina Sojakova Provides data structures for institution morphisms.
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina Sojakova These are just collections of
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina Sojakova functions between (some of) the types of logics.
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina Sojakova
ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa-}
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina Sojakova
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina Sojakova{- References: see Logic.hs
f20841e0b3d9311fd39f2615e43538214f720dd5Kristina Sojakova
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina Sojakova Todo:
ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa morphism modifications / representation maps
ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa-}
ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina Sojakovamodule Logic.Morphism where
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina Sojakova
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina Sojakovaimport Logic.Logic
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina Sojakovaimport Logic.Comorphism
f20841e0b3d9311fd39f2615e43538214f720dd5Kristina Sojakovaimport Common.Lib.Set
f20841e0b3d9311fd39f2615e43538214f720dd5Kristina Sojakovaimport Data.Maybe
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Data.Dynamic
f20841e0b3d9311fd39f2615e43538214f720dd5Kristina Sojakovaimport Common.DynamicUtils
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Common.AS_Annotation (Named, mapNamedM)
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina Sojakova
109f89c82ec8769e9ec81bc967987b5deecdfd25Kristina Sojakovaclass (Language cid,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Logic lid1 sublogics1
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder basic_spec1 sentence1 symb_items1 symb_map_items1
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
109f89c82ec8769e9ec81bc967987b5deecdfd25Kristina Sojakova Logic lid2 sublogics2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder basic_spec2 sentence2 symb_items2 symb_map_items2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Morphism cid
3df50f2bdc19d6aa0d3ee0ecac5ad7ad785ddb45Kristina Sojakova lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina Sojakova lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina Sojakova sign2 morphism2 symbol2 raw_symbol2 proof_tree2
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov | cid -> lid1, cid -> lid2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov where
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov -- source and target logic and sublogic
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -- the source sublogic is the maximal one for which the comorphism works
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov -- the target sublogic is the resulting one
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder morSourceLogic :: cid -> lid1
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov morSourceSublogic :: cid -> sublogics1
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder morTargetLogic :: cid -> lid2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder morTargetSublogic :: cid -> sublogics2
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov -- finer information of target sublogics corresponding to source sublogics
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder morMapSublogic :: cid -> sublogics1 -> sublogics2
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov -- default implementation
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov morMapSublogic cid _ = targetSublogic cid
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -- the translation functions are partial
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -- because the target may be a sublanguage
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov -- map_basic_spec :: cid -> basic_spec1 -> Maybe basic_spec2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -- we do not cover theoroidal morphisms,
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov -- since there are no relevant examples and they do not compose nicely
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov -- no mapping of theories, since signatrures and sentences are mapped
f20841e0b3d9311fd39f2615e43538214f720dd5Kristina Sojakova -- contravariantly
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov morMap_sign :: cid -> sign1 -> Maybe sign2
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina Sojakova morMap_morphism :: cid -> morphism1 -> Maybe morphism2
f20841e0b3d9311fd39f2615e43538214f720dd5Kristina Sojakova morMap_sentence :: cid -> sign1 -> sentence2 -> Maybe sentence1
f20841e0b3d9311fd39f2615e43538214f720dd5Kristina Sojakova -- also covers semi-morphisms ??
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov -- with no sentence translation
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov -- - but these are spans!
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina Sojakova morMap_symbol :: cid -> symbol1 -> Set symbol2
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina Sojakova -- morConstituents not needed, because composition only via lax triangles
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina Sojakova
f20841e0b3d9311fd39f2615e43538214f720dd5Kristina Sojakova
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- identity morphisms
f20841e0b3d9311fd39f2615e43538214f720dd5Kristina Sojakova
109f89c82ec8769e9ec81bc967987b5deecdfd25Kristina Sojakovadata IdMorphism lid sublogics =
3df50f2bdc19d6aa0d3ee0ecac5ad7ad785ddb45Kristina Sojakova IdMorphism lid sublogics deriving Show
f20841e0b3d9311fd39f2615e43538214f720dd5Kristina Sojakova
109f89c82ec8769e9ec81bc967987b5deecdfd25Kristina SojakovaidMorphismTc :: TyCon
f20841e0b3d9311fd39f2615e43538214f720dd5Kristina SojakovaidMorphismTc = mkTyCon "Logic.Morphism.IdMorphism"
3df50f2bdc19d6aa0d3ee0ecac5ad7ad785ddb45Kristina Sojakova
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederinstance Typeable (IdMorphism lid sub) where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder typeOf _ = mkTyConApp idMorphismTc []
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatovinstance Logic lid sublogics
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov basic_spec sentence symb_items symb_map_items
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov sign morphism symbol raw_symbol proof_tree =>
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov Language (IdMorphism lid sublogics) where
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov language_name (IdMorphism lid sub) =
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov case sublogic_names lid sub of
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov [] -> error "language_name IdMorphism"
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov h : _ -> "id_" ++ language_name lid ++ "." ++ h
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina Sojakovainstance Logic lid sublogics
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina Sojakova basic_spec sentence symb_items symb_map_items
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina Sojakova sign morphism symbol raw_symbol proof_tree =>
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina Sojakova Morphism (IdMorphism lid sublogics)
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina Sojakova lid sublogics
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree
lid sublogics
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree
where
sourceLogic (IdMorphism lid _sub) = lid
targetLogic (IdMorphism lid _sub) = lid
sourceSublogic (IdMorphism _lid sub) = sub
targetSublogic (IdMorphism _lid sub) = sub
map_sign _ = \sigma -> Just(sigma,[])
map_morphism _ = Just
map_sentence _ = \_ -> Just
map_symbol _ = single
constituents _ = []
-- composition not needed, use lax triangles instead
-- comorphisms inducing morphisms
class Comorphism cid
lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 symbol1 raw_symbol1 proof_tree1
lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
sign2 morphism2 symbol2 raw_symbol2 proof_tree2 =>
InducingComorphism cid
lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 symbol1 raw_symbol1 proof_tree1
lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
sign2 morphism2 symbol2 raw_symbol2 proof_tree2
where
indMorMap_sign :: cid -> sign2 -> Maybe sign1
indMorMap_morphism :: cid -> morphism2 -> Maybe morphism1
epsilon :: cid -> sign2 -> Maybe morphism2
instance InducingComorphism cid
lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 symbol1 raw_symbol1 proof_tree1
lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
sign2 morphism2 symbol2 raw_symbol2 proof_tree2 =>
Morphism cid
lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 symbol1 raw_symbol1 proof_tree1
lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
sign2 morphism2 symbol2 raw_symbol2 proof_tree2 =>
where
morSourceLogic cid = targetLogic cid
morSourceSublogic cid = targetSublogic cid
morTargetLogic cid = sourceSublogic cid
morTargetSublogic cid = sourceSublogic cid
morMapSublogic :: cid -> sublogics1 -> sublogics2
-- the translation functions are partial
-- because the target may be a sublanguage
-- map_basic_spec :: cid -> basic_spec1 -> Maybe basic_spec2
-- we do not cover theoroidal morphisms,
-- since there are no relevant examples and they do not compose nicely
-- no mapping of theories, since signatrures and sentences are mapped
-- contravariantly
morMap_sign :: cid -> sign1 -> Maybe sign2
morMap_morphism :: cid -> morphism1 -> Maybe morphism2
morMap_sentence :: cid -> sign1 -> sentence2 -> Maybe sentence1
-- also covers semi-morphisms ??
-- with no sentence translation
-- - but these are spans!
morMap_symbol :: cid -> symbol1 -> Set symbol2