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