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