Comorphism.hs revision 44fb55f639914f4f531641f32dd4904f15c510a4
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederModule : $Header$
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004
ca010363454de207082dfaa4b753531ce2a34551Christian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
ca010363454de207082dfaa4b753531ce2a34551Christian MaederMaintainer : hets@tzi.de
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederStability : provisional
ca010363454de207082dfaa4b753531ce2a34551Christian MaederPortability : non-portable (via Logic)
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder Provides data structures for institution comorphisms.
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder These are just collections of
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder functions between (some of) the types of logics.
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder{- References: see Logic.hs
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder Weak amalgamability, also for comorphisms
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder comorphism modifications
23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maeder comorphisms out of sublogic relationships
fcb1d8a27670f3206bd4ca28d77d4172619db602Christian Maeder restrictions of comorphisms to sublogics
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder morphisms and other translations via spans
79d11c2e3ad242ebb241f5d4a5e98a674c0b986fChristian Maederimport Common.AS_Annotation (Named, mapNamedM)
53301de22afd7190981b363b57c48df86fcb50f7Christian Maederclass (Language cid,
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder Logic lid1 sublogics1
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder Logic lid2 sublogics2
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder Comorphism cid
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder | cid -> lid1, cid -> lid2
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder -- source and target logic and sublogic
d48085f765fca838c1d972d2123601997174583dChristian Maeder -- the source sublogic is the maximal one for which the comorphism works
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder -- the target sublogic is the resulting one
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder sourceLogic :: cid -> lid1
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder sourceSublogic :: cid -> sublogics1
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder targetLogic :: cid -> lid2
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder targetSublogic :: cid -> sublogics2
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder -- finer information of target sublogics corresponding to source sublogics
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder mapSublogic :: cid -> sublogics1 -> sublogics2
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder -- default implementation
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder mapSublogic cid _ = targetSublogic cid
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder -- the translation functions are partial
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder -- because the target may be a sublanguage
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder -- map_basic_spec :: cid -> basic_spec1 -> Maybe basic_spec2
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder -- cover theoroidal comorphisms as well
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder map_sign :: cid -> sign1 -> Maybe (sign2,[Named sentence2])
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder map_theory :: cid -> (sign1,[Named sentence1])
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder -> Maybe (sign2,[Named sentence2])
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder --default implementations
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder map_sign cid sign = map_theory cid (sign,[])
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder map_theory cid (sign,sens) = do
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder (sign',sens') <- map_sign cid sign
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder let sens'' = mapMaybe (mapNamedM (map_sentence cid sign)) sens
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder return (sign',sens'++sens'')
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder map_morphism :: cid -> morphism1 -> Maybe morphism2
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder map_sentence :: cid -> sign1 -> sentence1 -> Maybe sentence2
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder -- also covers semi-comorphisms
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder -- with no sentence translation
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder -- - but these are spans!
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder map_symbol :: cid -> symbol1 -> Set symbol2
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder constituents :: cid -> [String]
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder -- default implementation
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder constituents cid = [language_name cid]
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maederdata IdComorphism lid sublogics =
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder IdComorphism lid sublogics deriving Show
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian MaederidComorphismTc :: TyCon
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian MaederidComorphismTc = mkTyCon "Logic.Comorphism.IdComorphism"
975642b989852fc24119c59cf40bc1af653608ffChristian Maederinstance Typeable (IdComorphism lid sub) where
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder typeOf _ = mkTyConApp idComorphismTc []
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maederinstance Logic lid sublogics
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder basic_spec sentence symb_items symb_map_items
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder sign morphism symbol raw_symbol proof_tree =>
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder Language (IdComorphism lid sublogics) where
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder language_name (IdComorphism lid sub) =
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder case sublogic_names lid sub of
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder [] -> error "language_name IdComorphism"
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder h : _ -> "id_" ++ language_name lid ++ "." ++ h
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maederinstance Logic lid sublogics
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder basic_spec sentence symb_items symb_map_items
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder sign morphism symbol raw_symbol proof_tree =>
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder Comorphism (IdComorphism lid sublogics)
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder lid sublogics
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder basic_spec sentence symb_items symb_map_items
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder sign morphism symbol raw_symbol proof_tree
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder lid sublogics
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder basic_spec sentence symb_items symb_map_items
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder sign morphism symbol raw_symbol proof_tree
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder sourceLogic (IdComorphism lid _sub) = lid
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder targetLogic (IdComorphism lid _sub) = lid
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder sourceSublogic (IdComorphism _lid sub) = sub
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder targetSublogic (IdComorphism _lid sub) = sub
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder map_sign _ = \sigma -> Just(sigma,[])
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder map_morphism _ = Just
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder map_sentence _ = \_ -> Just
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder map_symbol _ = single
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder constituents _ = []
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maederdata CompComorphism cid1 cid2 = CompComorphism cid1 cid2 deriving Show
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian MaedertyconCompComorphism :: TyCon
53301de22afd7190981b363b57c48df86fcb50f7Christian MaedertyconCompComorphism = mkTyCon "Logic.Comorphism.CompComorphism"
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maederinstance Typeable (CompComorphism cid1 cid2) where
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder typeOf _ = mkTyConApp tyconCompComorphism []
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maederinstance (Comorphism cid1
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder Comorphism cid2
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder sign4 morphism4 symbol4 raw_symbol4 proof_tree4
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder sign3 morphism3 symbol3 raw_symbol3 proof_tree3)
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder => Language (CompComorphism cid1 cid2) where
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder language_name (CompComorphism cid1 cid2) =
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder language_name cid1++";"
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder ++language_name cid2
53301de22afd7190981b363b57c48df86fcb50f7Christian Maederinstance (Comorphism cid1
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maeder Comorphism cid2
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maeder lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maeder sign4 morphism4 symbol4 raw_symbol4 proof_tree4
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder sign3 morphism3 symbol3 raw_symbol3 proof_tree3)
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder => Comorphism (CompComorphism cid1 cid2)
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder sign3 morphism3 symbol3 raw_symbol3 proof_tree3 where
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder sourceLogic (CompComorphism cid1 _) =
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder sourceLogic cid1
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder targetLogic (CompComorphism _ cid2) =
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder targetLogic cid2
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder sourceSublogic (CompComorphism cid1 _) =
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder sourceSublogic cid1
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder targetSublogic (CompComorphism _ cid2) =
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder targetSublogic cid2
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maeder map_sentence (CompComorphism cid1 cid2) =
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder do (si2,_) <- map_sign cid1 si1
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder se2 <- map_sentence cid1 si1 se1
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder (si2', se2') <- mcoerce (targetLogic cid1) (sourceLogic cid2)
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder "Mapping sentence along comorphism" (si2, se2)
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder map_sentence cid2 si2' se2'
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder map_sign (CompComorphism cid1 cid2) =
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder do (si2, se2s) <- map_sign cid1 si1
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder (si2', se2s') <- mcoerce (targetLogic cid1) (sourceLogic cid2)
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder "Mapping signature along comorphism"(si2, se2s)
909ce57d58a9cec1d214f0ecbdb1dadddad2e6d9Christian Maeder (si3, se3s) <- map_sign cid2 si2'
f8a03685d9184046e88e1d76aabdab4f714db440Christian Maeder return (si3, se3s ++ catMaybes
909ce57d58a9cec1d214f0ecbdb1dadddad2e6d9Christian Maeder (map (mapNamedM (map_sentence cid2 si2')) se2s'))
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder map_theory (CompComorphism cid1 cid2) =
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder do ti2 <- map_theory cid1 ti1
46d766efdf8beaaadf3f34d99c305738064e9216Christian Maeder ti2' <- mcoerce (targetLogic cid1) (sourceLogic cid2)
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder "Mapping theory along comorphism" ti2
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder map_theory cid2 ti2'
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder map_morphism (CompComorphism cid1 cid2) = \ m1 ->
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder do m2 <- map_morphism cid1 m1
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder m3 <- mcoerce (targetLogic cid1) (sourceLogic cid2)
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder "Mapping signature morphism along comorphism"m2
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder map_morphism cid2 m3
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder map_symbol (CompComorphism cid1 cid2) = \ s1 ->
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder let mycast = fromJust . mcoerce (targetLogic cid1) (sourceLogic cid2)
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder "Mapping symbol along comorphism"
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder (map (map_symbol cid2 . mycast)
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder (toList (map_symbol cid1 s1)))
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder constituents (CompComorphism cid1 cid2) =
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder constituents cid1 ++ constituents cid2