Morphism.hs revision 49744099bf207892e92973d47e43be679fe0f68d
5d801400993c9671010d244646936d8fd435638cChristian MaederModule : $Header$
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceMaintainer : hets@tzi.de
5d801400993c9671010d244646936d8fd435638cChristian MaederStability : provisional
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancePortability : non-portable (via Logic)
aa0ca44e856c87db27e61687cbb630f270976da1Felix Gabriel Mance Provides data structures for institution morphisms.
5d801400993c9671010d244646936d8fd435638cChristian Maeder These are just collections of
5d801400993c9671010d244646936d8fd435638cChristian Maeder functions between (some of) the types of logics.
097bc9f18b722812d480df0f5c634d09cbca8e21Felix Gabriel Mance{- References: see Logic.hs
f853560cb2b56c631af268adec9dd0c1f518ffd8Felix Gabriel Mance morphism modifications / representation maps
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport Common.AS_Annotation (Named, mapNamedM)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceclass (Language cid,
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Logic lid1 sublogics1
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance basic_spec1 sentence1 symb_items1 symb_map_items1
968930c7674ae3b63d308bf4fa651400aa263054Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Logic lid2 sublogics2
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance basic_spec2 sentence2 symb_items2 symb_map_items2
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance sign1 morphism1 symbol1 raw_symbol1 proof_tree1
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance sign2 morphism2 symbol2 raw_symbol2 proof_tree2
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance | cid -> lid1, cid -> lid2
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance -- source and target logic and sublogic
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance -- the source sublogic is the maximal one for which the comorphism works
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance -- the target sublogic is the resulting one
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance morSourceLogic :: cid -> lid1
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance morSourceSublogic :: cid -> sublogics1
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance morTargetLogic :: cid -> lid2
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance morTargetSublogic :: cid -> sublogics2
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance -- finer information of target sublogics corresponding to source sublogics
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance morMapSublogic :: cid -> sublogics1 -> sublogics2
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance -- default implementation
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance morMapSublogic cid _ = targetSublogic cid
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance -- the translation functions are partial
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance -- because the target may be a sublanguage
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance -- map_basic_spec :: cid -> basic_spec1 -> Maybe basic_spec2
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance -- we do not cover theoroidal morphisms,
1435782fda52a2898ea74e99088351d4f5b450dcChristian Maeder -- since there are no relevant examples and they do not compose nicely
1435782fda52a2898ea74e99088351d4f5b450dcChristian Maeder -- no mapping of theories, since signatrures and sentences are mapped
1435782fda52a2898ea74e99088351d4f5b450dcChristian Maeder -- contravariantly
1435782fda52a2898ea74e99088351d4f5b450dcChristian Maeder morMap_sign :: cid -> sign1 -> Maybe sign2
1435782fda52a2898ea74e99088351d4f5b450dcChristian Maeder morMap_morphism :: cid -> morphism1 -> Maybe morphism2
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance morMap_sentence :: cid -> sign1 -> sentence2 -> Maybe sentence1
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance -- also covers semi-morphisms ??
dd3c105fcc30b5d6b750d8fbe32250207b996109Felix Gabriel Mance -- with no sentence translation
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance -- - but these are spans!
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance morMap_symbol :: cid -> symbol1 -> Set symbol2
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance morConstituents :: cid -> [String]
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance -- default implementation
6a058c55573e9bbb71cee8a7361ef12bfaedd9efFelix Gabriel Mance morConstituents cid = [language_name cid]
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance-- identity morphisms
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mancedata IdMorphism lid sublogics =
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance IdMorphism lid sublogics deriving Show
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel ManceidMorphismTc :: TyCon
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel ManceidMorphismTc = mkTyCon "Logic.Morphism.IdMorphism"
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Manceinstance Typeable (IdMorphism lid sub) where
9cb6af1a7632f12b60f592ce5eb2ac51e6bd33bbFelix Gabriel Mance typeOf _ = mkTyConApp idMorphismTc []
1435782fda52a2898ea74e99088351d4f5b450dcChristian Maederinstance Logic lid sublogics
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance basic_spec sentence symb_items symb_map_items
097bc9f18b722812d480df0f5c634d09cbca8e21Felix Gabriel Mance sign morphism symbol raw_symbol proof_tree =>
968930c7674ae3b63d308bf4fa651400aa263054Christian Maeder Language (IdMorphism lid sublogics) where
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance language_name (IdMorphism lid sub) =
a921ae1da1302f673204e7b63cdce01439a9bd5eFelix Gabriel Mance case sublogic_names lid sub of
968930c7674ae3b63d308bf4fa651400aa263054Christian Maeder [] -> error "language_name IdMorphism"
a921ae1da1302f673204e7b63cdce01439a9bd5eFelix Gabriel Mance h : _ -> "id_" ++ language_name lid ++ "." ++ h
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceinstance Logic lid sublogics
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance basic_spec sentence symb_items symb_map_items
1435782fda52a2898ea74e99088351d4f5b450dcChristian Maeder sign morphism symbol raw_symbol proof_tree =>
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Morphism (IdMorphism lid sublogics)
097bc9f18b722812d480df0f5c634d09cbca8e21Felix Gabriel Mance basic_spec sentence symb_items symb_map_items
ba2c0d8be230f0b274cf3e0013e3844a80d9afd4Christian Maeder sign morphism symbol raw_symbol proof_tree
ba2c0d8be230f0b274cf3e0013e3844a80d9afd4Christian Maeder lid sublogics
5d801400993c9671010d244646936d8fd435638cChristian Maeder basic_spec sentence symb_items symb_map_items
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance sign morphism symbol raw_symbol proof_tree
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance sourceLogic (IdMorphism lid _sub) = lid
aa64389ee694577d9e665cf57331129000072a79Felix Gabriel Mance targetLogic (IdMorphism lid _sub) = lid
aa64389ee694577d9e665cf57331129000072a79Felix Gabriel Mance sourceSublogic (IdMorphism _lid sub) = sub
1435782fda52a2898ea74e99088351d4f5b450dcChristian Maeder targetSublogic (IdMorphism _lid sub) = sub
1435782fda52a2898ea74e99088351d4f5b450dcChristian Maeder map_sign _ = \sigma -> Just(sigma,[])
aa64389ee694577d9e665cf57331129000072a79Felix Gabriel Mance map_morphism _ = Just
aa64389ee694577d9e665cf57331129000072a79Felix Gabriel Mance map_sentence _ = \_ -> Just
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance map_symbol _ = single
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance constituents _ = []
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance-- composition not needed, use lax triangles instead
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance-- comorphisms inducing morphisms
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceclass Comorphism cid
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance sign1 morphism1 symbol1 raw_symbol1 proof_tree1
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance sign2 morphism2 symbol2 raw_symbol2 proof_tree2 =>
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance MorphismInducing cid
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance sign1 morphism1 symbol1 raw_symbol1 proof_tree1
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
1435782fda52a2898ea74e99088351d4f5b450dcChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance indMorMap_sign :: cid -> sign2 -> Maybe sign1
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance indMorMap_morphism :: cid -> morphism2 -> Maybe morphism1
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance epsilon :: cid -> sign2 -> Maybe morphism2