Morphism.hs revision 797595aad6dfd626bc1c9df52616f1ac4235c669
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 SojakovaMaintainer : hets@tzi.de
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina SojakovaStability : provisional
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina SojakovaPortability : non-portable (via Logic)
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{- References: see Logic.hs
ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa morphism modifications / representation maps
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Common.AS_Annotation (Named, mapNamedM)
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) =>
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
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
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- identity morphisms
109f89c82ec8769e9ec81bc967987b5deecdfd25Kristina Sojakovadata IdMorphism lid sublogics =
3df50f2bdc19d6aa0d3ee0ecac5ad7ad785ddb45Kristina Sojakova IdMorphism lid sublogics deriving Show
109f89c82ec8769e9ec81bc967987b5deecdfd25Kristina SojakovaidMorphismTc :: TyCon
f20841e0b3d9311fd39f2615e43538214f720dd5Kristina SojakovaidMorphismTc = mkTyCon "Logic.Morphism.IdMorphism"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederinstance Typeable (IdMorphism lid sub) where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder typeOf _ = mkTyConApp idMorphismTc []
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
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)