Morphism.hs revision 650bafe7709533bc5f82bb9daf8fa06f431cd963
842ae4bd224140319ae7feec1872b93dfd491143fieldingModule : $Header$
842ae4bd224140319ae7feec1872b93dfd491143fieldingCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004
842ae4bd224140319ae7feec1872b93dfd491143fieldingLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
dc9d4f49d36e64c0157d930cb22ca82a6291c0cbdgaudetMaintainer : till@tzi.de
ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcndStability : provisional
dc9d4f49d36e64c0157d930cb22ca82a6291c0cbdgaudetPortability : non-portable (via Logic)
ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcndProvides data structures for institution morphisms.
ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcnd These are just collections of
ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcnd functions between (some of) the types of logics.
ab5581cc78e9d865b0a6ab1404c53347b3276968rbb{- References: see Logic.hs
024cd9589e52cf11ce765dfddb5b5f0c6e421a48gstein morphism modifications / representation maps
89211a3153be8b03353c3bfbca45fed67cb80f0bpquernaimport qualified Common.Lib.Set as Set
024cd9589e52cf11ce765dfddb5b5f0c6e421a48gsteinimport Common.AS_Annotation (Named, mapNamedM)
a742cbb3e85669473b3233f30e3978bb6a20083cylavicclass (Language cid,
a742cbb3e85669473b3233f30e3978bb6a20083cylavic Logic lid1 sublogics1
a742cbb3e85669473b3233f30e3978bb6a20083cylavic basic_spec1 sentence1 symb_items1 symb_map_items1
a742cbb3e85669473b3233f30e3978bb6a20083cylavic sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
9591ec71b8911ecefbf6571333ff78fcb6efffa5jorton Logic lid2 sublogics2
77e0c54d01cb01e700e939a78afa49a7aa1e2275pquerna basic_spec2 sentence2 symb_items2 symb_map_items2
77e0c54d01cb01e700e939a78afa49a7aa1e2275pquerna sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>
77e0c54d01cb01e700e939a78afa49a7aa1e2275pquerna Morphism cid
7184de27ec1d62a83c41cdeac0953ca9fd661e8csf lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
7184de27ec1d62a83c41cdeac0953ca9fd661e8csf sign1 morphism1 symbol1 raw_symbol1 proof_tree1
7184de27ec1d62a83c41cdeac0953ca9fd661e8csf lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
36ef8f77bffe75d1aa327882be1b5bdbe2ff567asf sign2 morphism2 symbol2 raw_symbol2 proof_tree2
e8fcc872d5caeea36adb6511f9d1ab6ce3fbb5c0jerenkrantz | cid -> lid1, cid -> lid2
a742cbb3e85669473b3233f30e3978bb6a20083cylavic -- source and target logic and sublogic
a742cbb3e85669473b3233f30e3978bb6a20083cylavic -- the source sublogic is the maximal one for which the comorphism works
a742cbb3e85669473b3233f30e3978bb6a20083cylavic -- the target sublogic is the resulting one
a742cbb3e85669473b3233f30e3978bb6a20083cylavic morSourceLogic :: cid -> lid1
a742cbb3e85669473b3233f30e3978bb6a20083cylavic morSourceSublogic :: cid -> sublogics1
a742cbb3e85669473b3233f30e3978bb6a20083cylavic morTargetLogic :: cid -> lid2
a742cbb3e85669473b3233f30e3978bb6a20083cylavic morTargetSublogic :: cid -> sublogics2
a742cbb3e85669473b3233f30e3978bb6a20083cylavic -- finer information of target sublogics corresponding to source sublogics
a742cbb3e85669473b3233f30e3978bb6a20083cylavic morMapSublogic :: cid -> sublogics1 -> sublogics2
a742cbb3e85669473b3233f30e3978bb6a20083cylavic -- default implementation
a742cbb3e85669473b3233f30e3978bb6a20083cylavic-- morMapSublogic cid _ = targetSublogic cid
a742cbb3e85669473b3233f30e3978bb6a20083cylavic -- the translation functions are partial
3c990331fc6702119e4f5b8ba9eae3021aea5265jim -- because the target may be a sublanguage
dc9d4f49d36e64c0157d930cb22ca82a6291c0cbdgaudet -- map_basic_spec :: cid -> basic_spec1 -> Maybe basic_spec2
dc9d4f49d36e64c0157d930cb22ca82a6291c0cbdgaudet -- we do not cover theoroidal morphisms,
a742cbb3e85669473b3233f30e3978bb6a20083cylavic -- since there are no relevant examples and they do not compose nicely
dc9d4f49d36e64c0157d930cb22ca82a6291c0cbdgaudet -- no mapping of theories, since signatrures and sentences are mapped
275419d6395e6f072962fb701b89accaff1f3690jerenkrantz -- contravariantly
9591ec71b8911ecefbf6571333ff78fcb6efffa5jorton morMap_sign :: cid -> sign1 -> Maybe sign2
de9479d1589cb756c9517611d8d193466536107bjkaluza morMap_morphism :: cid -> morphism1 -> Maybe morphism2
77e0c54d01cb01e700e939a78afa49a7aa1e2275pquerna morMap_sentence :: cid -> sign1 -> sentence2 -> Maybe sentence1
dc9d4f49d36e64c0157d930cb22ca82a6291c0cbdgaudet -- also covers semi-morphisms ??
dc9d4f49d36e64c0157d930cb22ca82a6291c0cbdgaudet -- with no sentence translation
77e0c54d01cb01e700e939a78afa49a7aa1e2275pquerna -- - but these are spans!
dc9d4f49d36e64c0157d930cb22ca82a6291c0cbdgaudet morMap_symbol :: cid -> symbol1 -> Set.Set symbol2
1ccd992d37d62c8cb2056126f2234f64ec189bfddougm -- morConstituents not needed, because composition only via lax triangles
95d00ea81131488769296fa5765ed745cbf45207trawick-- identity morphisms
95d00ea81131488769296fa5765ed745cbf45207trawickdata IdMorphism lid sublogics =
95d00ea81131488769296fa5765ed745cbf45207trawick IdMorphism lid sublogics deriving Show
95d00ea81131488769296fa5765ed745cbf45207trawickidMorphismTc :: TyCon
1ccd992d37d62c8cb2056126f2234f64ec189bfddougmidMorphismTc = mkTyCon "Logic.Morphism.IdMorphism"
85e4da1cf0dee899551b583b1f06314b2835100awroweinstance Typeable (IdMorphism lid sub) where
9179fa90e821c964d10f28b97fc6acee776af7cfwrowe typeOf _ = mkTyConApp idMorphismTc []
185aa71728867671e105178b4c66fbc22b65ae26sfinstance Logic lid sublogics
9179fa90e821c964d10f28b97fc6acee776af7cfwrowe basic_spec sentence symb_items symb_map_items
2261031aa94be82d7e6b1b8c367afc1b282317f5ianh sign morphism symbol raw_symbol proof_tree =>
ebf4099fd4921bbbcef21dc872b9cd4fc73e9f55trawick Language (IdMorphism lid sublogics) where
ebf4099fd4921bbbcef21dc872b9cd4fc73e9f55trawick language_name (IdMorphism lid sub) =
ebf4099fd4921bbbcef21dc872b9cd4fc73e9f55trawick case sublogic_names lid sub of
85e4da1cf0dee899551b583b1f06314b2835100awrowe [] -> error "language_name IdMorphism"
2261031aa94be82d7e6b1b8c367afc1b282317f5ianh h : _ -> "id_" ++ language_name lid ++ "." ++ h
ab5581cc78e9d865b0a6ab1404c53347b3276968rbbinstance Logic lid sublogics
185aa71728867671e105178b4c66fbc22b65ae26sf basic_spec sentence symb_items symb_map_items
9179fa90e821c964d10f28b97fc6acee776af7cfwrowe sign morphism symbol raw_symbol proof_tree =>
2261031aa94be82d7e6b1b8c367afc1b282317f5ianh Morphism (IdMorphism lid sublogics)
cf24c48249f38c34c04617f5b78b240f1cee380ajerenkrantz lid sublogics
cf24c48249f38c34c04617f5b78b240f1cee380ajerenkrantz basic_spec sentence symb_items symb_map_items
dc9d4f49d36e64c0157d930cb22ca82a6291c0cbdgaudet sign morphism symbol raw_symbol proof_tree
dc9d4f49d36e64c0157d930cb22ca82a6291c0cbdgaudet lid sublogics
dc9d4f49d36e64c0157d930cb22ca82a6291c0cbdgaudet basic_spec sentence symb_items symb_map_items
dc9d4f49d36e64c0157d930cb22ca82a6291c0cbdgaudet sign morphism symbol raw_symbol proof_tree
dc9d4f49d36e64c0157d930cb22ca82a6291c0cbdgaudet morSourceLogic (IdMorphism lid _sub) = lid
dc9d4f49d36e64c0157d930cb22ca82a6291c0cbdgaudet morTargetLogic (IdMorphism lid _sub) = lid
dc9d4f49d36e64c0157d930cb22ca82a6291c0cbdgaudet morSourceSublogic (IdMorphism _lid sub) = sub
dc9d4f49d36e64c0157d930cb22ca82a6291c0cbdgaudet morTargetSublogic (IdMorphism _lid sub) = sub
dc9d4f49d36e64c0157d930cb22ca82a6291c0cbdgaudet morMapSublogic _ _ =
dc9d4f49d36e64c0157d930cb22ca82a6291c0cbdgaudet morMap_sign _ = Just
dc9d4f49d36e64c0157d930cb22ca82a6291c0cbdgaudet morMap_morphism _ = Just
dc9d4f49d36e64c0157d930cb22ca82a6291c0cbdgaudet morMap_sentence _ = \_ -> Just
dc9d4f49d36e64c0157d930cb22ca82a6291c0cbdgaudet morMap_symbol _ = Set.singleton
dc9d4f49d36e64c0157d930cb22ca82a6291c0cbdgaudet-- composition not needed, use lax triangles instead
dc9d4f49d36e64c0157d930cb22ca82a6291c0cbdgaudet-- comorphisms inducing morphisms
dc9d4f49d36e64c0157d930cb22ca82a6291c0cbdgaudetclass Comorphism cid
dc9d4f49d36e64c0157d930cb22ca82a6291c0cbdgaudet lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
9179fa90e821c964d10f28b97fc6acee776af7cfwrowe sign1 morphism1 symbol1 raw_symbol1 proof_tree1
ab5581cc78e9d865b0a6ab1404c53347b3276968rbb lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
185aa71728867671e105178b4c66fbc22b65ae26sf sign2 morphism2 symbol2 raw_symbol2 proof_tree2 =>
2261031aa94be82d7e6b1b8c367afc1b282317f5ianh InducingComorphism cid
2261031aa94be82d7e6b1b8c367afc1b282317f5ianh lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
2261031aa94be82d7e6b1b8c367afc1b282317f5ianh sign1 morphism1 symbol1 raw_symbol1 proof_tree1
cf24c48249f38c34c04617f5b78b240f1cee380ajerenkrantz lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
cf24c48249f38c34c04617f5b78b240f1cee380ajerenkrantz sign2 morphism2 symbol2 raw_symbol2 proof_tree2
275419d6395e6f072962fb701b89accaff1f3690jerenkrantz indMorMap_sign :: cid -> sign2 -> Maybe sign1
275419d6395e6f072962fb701b89accaff1f3690jerenkrantz indMorMap_morphism :: cid -> morphism2 -> Maybe morphism1
275419d6395e6f072962fb701b89accaff1f3690jerenkrantz epsilon :: cid -> sign2 -> Maybe morphism2