Comorphism.hs revision ca8550c6d47234042130bdc10a152806ecbc9832
e071fb22ea9923a2a4ff41184d80ca46b55ee932Till MossakowskiModule : $Header$
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiMaintainer : hets@tzi.de
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachStability : provisional
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachPortability : non-portable (via Logic)
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder Provides data structures for institution comorphisms.
8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy Gimblett These are just collections of
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach functions between (some of) the types of logics.
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach{- References: see Logic.hs
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly Weak amalgamability, also for comorphisms
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach comorphism modifications
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly comorphisms out of sublogic relationships
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly restrictions of comorphisms to sublogics
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly morphisms and other translations via spans
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettclass (Language cid,
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder Logic lid1 sublogics1
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett Logic lid2 sublogics2
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett basic_spec2 sentence2 symb_items2 symb_map_items2
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett Comorphism cid
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett sign2 morphism2 symbol2 raw_symbol2 proof_tree2
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett | cid -> lid1, cid -> lid2
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett -- source and target logic and sublogic
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett -- the source sublogic is the maximal one for which the comorphism works
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder -- the target sublogic is the resulting one
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett sourceLogic :: cid -> lid1
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett sourceSublogic :: cid -> sublogics1
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett targetLogic :: cid -> lid2
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder targetSublogic :: cid -> sublogics2
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder -- finer information of target sublogics corresponding to source sublogics
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder mapSublogic :: cid -> sublogics1 -> sublogics2
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder -- default implementation
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder mapSublogic cid _ = targetSublogic cid
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder -- the translation functions are partial
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder -- because the target may be a sublanguage
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett -- map_basic_spec :: cid -> basic_spec1 -> Result basic_spec2
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett -- cover theoroidal comorphisms as well
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett map_theory :: cid -> (sign1,[Named sentence1])
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett -> Result (sign2,[Named sentence2])
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder map_morphism :: cid -> morphism1 -> Result morphism2
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder map_sentence :: cid -> sign1 -> sentence1 -> Result sentence2
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett -- also covers semi-comorphisms
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett -- with no sentence translation
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett -- - but these are spans!
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett map_symbol :: cid -> symbol1 -> Set symbol2
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder constituents :: cid -> [String]
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder -- default implementation
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett constituents cid = [language_name cid]
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblettmap_sign :: Comorphism cid
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett sign2 morphism2 symbol2 raw_symbol2 proof_tree2
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett => cid -> sign1 -> Result (sign2,[Named sentence2])
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maedermap_sign cid sign = map_theory cid (sign,[])
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian MaedersimpleTheoryMapping :: (sign1 -> sign2) -> (sentence1 -> sentence2)
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder -> (sign1, [Named sentence1])
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett -> (sign2, [Named sentence2])
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettsimpleTheoryMapping mapSig mapSen (sign,sens) =
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett (mapSig sign, map (mapNamed mapSen) sens)
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettmkTheoryMapping :: (Monad m) => (sign1 -> m (sign2, [Named sentence2]))
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett -> (sign1 -> sentence1 -> m sentence2)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett -> (sign1, [Named sentence1])
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -> m (sign2, [Named sentence2])
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillymkTheoryMapping mapSig mapSen (sign,sens) = do
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly (sign',sens') <- mapSig sign
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett sens'' <- mapM (mapNamedM $ mapSen sign) sens
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach return (sign',sens'++sens'')
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettdata IdComorphism lid sublogics =
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett IdComorphism lid sublogics
cdf1545bdcd39a9d53c00761ffa42e7b1174b91eLiam O'Reillyinstance Logic lid sublogics
cdf1545bdcd39a9d53c00761ffa42e7b1174b91eLiam O'Reilly basic_spec sentence symb_items symb_map_items
cdf1545bdcd39a9d53c00761ffa42e7b1174b91eLiam O'Reilly sign morphism symbol raw_symbol proof_tree =>
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly Show (IdComorphism lid sublogics)
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly show = language_name
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettidComorphismTc :: TyCon
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettidComorphismTc = mkTyCon "Logic.Comorphism.IdComorphism"
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettinstance Typeable (IdComorphism lid sub) where
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett typeOf _ = mkTyConApp idComorphismTc []
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettinstance Logic lid sublogics
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett basic_spec sentence symb_items symb_map_items
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly sign morphism symbol raw_symbol proof_tree =>
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett Language (IdComorphism lid sublogics) where
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett language_name (IdComorphism lid sub) =
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett case sublogic_names lid sub of
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett [] -> error "language_name IdComorphism"
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett h : _ -> "id_" ++ language_name lid ++ "." ++ h
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettinstance Logic lid sublogics
eca4db63ed0bdbd93b62678feea6e3eb80aa47bbChristian Maeder basic_spec sentence symb_items symb_map_items
1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski sign morphism symbol raw_symbol proof_tree =>
f08f7774e4c47012f3c349205310750198cdc434Liam O'Reilly Comorphism (IdComorphism lid sublogics)
f08f7774e4c47012f3c349205310750198cdc434Liam O'Reilly lid sublogics
f08f7774e4c47012f3c349205310750198cdc434Liam O'Reilly basic_spec sentence symb_items symb_map_items
f08f7774e4c47012f3c349205310750198cdc434Liam O'Reilly sign morphism symbol raw_symbol proof_tree
f08f7774e4c47012f3c349205310750198cdc434Liam O'Reilly lid sublogics
f08f7774e4c47012f3c349205310750198cdc434Liam O'Reilly basic_spec sentence symb_items symb_map_items
f08f7774e4c47012f3c349205310750198cdc434Liam O'Reilly sign morphism symbol raw_symbol proof_tree
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett sourceLogic (IdComorphism lid _sub) = lid
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett targetLogic (IdComorphism lid _sub) = lid
1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski sourceSublogic (IdComorphism _lid sub) = sub
1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski targetSublogic (IdComorphism _lid sub) = sub
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett mapSublogic _ = id
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett map_theory _ = return
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett map_morphism _ = return
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimblett map_sentence _ = \_ -> return
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett map_symbol _ = single
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett constituents _ = []
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowskidata CompComorphism cid1 cid2 = CompComorphism cid1 cid2 deriving Show
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian MaedertyconCompComorphism :: TyCon
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian MaedertyconCompComorphism = mkTyCon "Logic.Comorphism.CompComorphism"
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maederinstance Typeable (CompComorphism cid1 cid2) where
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder typeOf _ = mkTyConApp tyconCompComorphism []
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maederinstance (Language cid1, Language cid2)
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder => Language (CompComorphism cid1 cid2) where
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder language_name (CompComorphism cid1 cid2) =
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder language_name cid1++ ";" ++language_name cid2
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maederinstance (Comorphism cid1
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder Comorphism cid2
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder sign4 morphism4 symbol4 raw_symbol4 proof_tree4
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder sign3 morphism3 symbol3 raw_symbol3 proof_tree3)
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett => Comorphism (CompComorphism cid1 cid2)
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimblett lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder sign3 morphism3 symbol3 raw_symbol3 proof_tree3 where
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett sourceLogic (CompComorphism cid1 _) =
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett sourceLogic cid1
1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski targetLogic (CompComorphism _ cid2) =
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski targetLogic cid2
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly sourceSublogic (CompComorphism cid1 _) =
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly sourceSublogic cid1
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly targetSublogic (CompComorphism cid1 cid2) =
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly mapSublogic cid2
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly (idcoerce (targetLogic cid1) (sourceLogic cid2)
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly (targetSublogic cid1))
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly mapSublogic (CompComorphism cid1 cid2) =
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly mapSublogic cid2
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly . idcoerce (targetLogic cid1) (sourceLogic cid2)
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly . mapSublogic cid1
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly map_sentence (CompComorphism cid1 cid2) =
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly do (si2,_) <- map_sign cid1 si1
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly se2 <- map_sentence cid1 si1 se1
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly (si2', se2') <- mcoerce (targetLogic cid1) (sourceLogic cid2)
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly "Mapping sentence along comorphism" (si2, se2)
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly map_sentence cid2 si2' se2'
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly map_theory (CompComorphism cid1 cid2) =
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly do ti2 <- map_theory cid1 ti1
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly ti2' <- mcoerce (targetLogic cid1) (sourceLogic cid2)
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly "Mapping theory along comorphism" ti2
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly map_theory cid2 ti2'
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly map_morphism (CompComorphism cid1 cid2) = \ m1 ->
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly do m2 <- map_morphism cid1 m1
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly m3 <- mcoerce (targetLogic cid1) (sourceLogic cid2)
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly "Mapping signature morphism along comorphism"m2
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly map_morphism cid2 m3
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly map_symbol (CompComorphism cid1 cid2) = \ s1 ->
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly let mycast = fromJust . mcoerce (targetLogic cid1) (sourceLogic cid2)
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly "Mapping symbol along comorphism"
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly (map (map_symbol cid2 . mycast)
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly (toList (map_symbol cid1 s1)))
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly constituents (CompComorphism cid1 cid2) =
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly constituents cid1 ++ constituents cid2