Morphism.hs revision cf31aaf25d0fe96b0578755e7ee18b732e337343
c1d71ac637c449feb0a25369f029397e6a1f241cChristian Maeder{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiModule : $Header$
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDescription : interface (type class) for logic projections (morphisms) in Hets
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)
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiInterface (type class) for logic projections (morphisms) in Hets
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian 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
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Set as Set
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
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder 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
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder -- 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
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder -- 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
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder-- identity morphisms
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maederdata IdMorphism lid sublogics =
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski IdMorphism lid sublogics deriving Show
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiidMorphismTc :: TyCon
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiidMorphismTc = mkTyCon "Logic.Morphism.IdMorphism"
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maederinstance 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
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder language_name (IdMorphism lid sub) =
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder case sublogic_names 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
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder 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
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian 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