Morphism.hs revision 717686b54b9650402e2ebfbaadf433eab8ba5171
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiModule : $Header$
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiMaintainer : till@tzi.de
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiStability : provisional
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiPortability : non-portable (via Logic)
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederProvides data structures for institution morphisms.
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski These are just collections of
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski functions between (some of) the types of logics.
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski{- References: see Logic.hs
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morphism modifications / representation maps
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maederimport qualified Common.Lib.Set as Set
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport Common.AS_Annotation (Named, mapNamedM)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiclass (Language cid,
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Logic lid1 sublogics1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski basic_spec1 sentence1 symb_items1 symb_map_items1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Logic lid2 sublogics2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski basic_spec2 sentence2 symb_items2 symb_map_items2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski | cid -> lid1, cid -> lid2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- source and target logic and sublogic
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- the source sublogic is the maximal one for which the comorphism works
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- the target sublogic is the resulting one
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morSourceLogic :: cid -> lid1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morSourceSublogic :: cid -> sublogics1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morTargetLogic :: cid -> lid2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morTargetSublogic :: cid -> sublogics2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- finer information of target sublogics corresponding to source sublogics
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morMapSublogic :: cid -> sublogics1 -> sublogics2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- default implementation
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- morMapSublogic cid _ = targetSublogic cid
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- the translation functions are partial
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- because the target may be a sublanguage
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- map_basic_spec :: cid -> basic_spec1 -> Maybe basic_spec2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- we do not cover theoroidal morphisms,
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- since there are no relevant examples and they do not compose nicely
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- no mapping of theories, since signatrures and sentences are mapped
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- contravariantly
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morMap_sign :: cid -> sign1 -> Maybe sign2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morMap_morphism :: cid -> morphism1 -> Maybe morphism2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morMap_sentence :: cid -> sign1 -> sentence2 -> Maybe sentence1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- also covers semi-morphisms ??
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- with no sentence translation
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- - but these are spans!
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder morMap_symbol :: cid -> symbol1 -> Set.Set symbol2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- morConstituents not needed, because composition only via lax triangles
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- identity morphisms
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskidata IdMorphism lid sublogics =
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski IdMorphism lid sublogics deriving Show
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiidMorphismTc :: TyCon
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiidMorphismTc = mkTyCon "Logic.Morphism.IdMorphism"
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiinstance Typeable (IdMorphism lid sub) where
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski typeOf _ = mkTyConApp idMorphismTc []
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiinstance Logic lid sublogics
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski basic_spec sentence symb_items symb_map_items
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski sign morphism symbol raw_symbol proof_tree =>
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Language (IdMorphism lid sublogics) where
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski language_name (IdMorphism lid sub) =
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski case sublogic_names lid sub of
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski [] -> error "language_name IdMorphism"
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski h : _ -> "id_" ++ language_name lid ++ "." ++ h
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiinstance Logic lid sublogics
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski basic_spec sentence symb_items symb_map_items
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski sign morphism symbol raw_symbol proof_tree =>
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Morphism (IdMorphism lid sublogics)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski lid sublogics
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski basic_spec sentence symb_items symb_map_items
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski sign morphism symbol raw_symbol proof_tree
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski lid sublogics
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski basic_spec sentence symb_items symb_map_items
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski sign morphism symbol raw_symbol proof_tree
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morSourceLogic (IdMorphism lid _sub) = lid
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morTargetLogic (IdMorphism lid _sub) = lid
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morSourceSublogic (IdMorphism _lid sub) = sub
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morTargetSublogic (IdMorphism _lid sub) = sub
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder morMapSublogic _ _ =
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder error "Logic.Morphism.IdMorphism.morMapSublogic"
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morMap_sign _ = Just
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morMap_morphism _ = Just
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morMap_sentence _ = \_ -> Just
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder morMap_symbol _ = Set.singleton
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- composition not needed, use lax triangles instead
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- comorphisms inducing morphisms
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiclass Comorphism cid
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2 =>
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski InducingComorphism cid
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski indMorMap_sign :: cid -> sign2 -> Maybe sign1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski indMorMap_morphism :: cid -> morphism2 -> Maybe morphism1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski epsilon :: cid -> sign2 -> Maybe morphism2