LogicGraph.hs revision 308834907a120fd8771e18292ed2ca9cd767c12d
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder{-# LANGUAGE CPP #-}
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederModule : $Header$
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederDescription : the logic graph
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederCopyright : (c) Till Mossakowski and Uni Bremen 2003
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : till@informatik.uni-bremen.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : unstable
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederPortability : non-portable
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian MaederAssembles all the logics and comorphisms into a graph.
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder The modules for the Grothendieck logic are logic graph indepdenent,
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder and here is the logic graph that is used to instantiate these.
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Since the logic graph depends on a large number of modules for the
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder individual logics, this separation of concerns (and possibility for
68d10d143f29fcff3c637ba24f90e983995ceae6Christian Maeder separate compilation) is quite useful.
a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettich Comorphisms are either logic inclusions, or normal comorphisms.
a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettich The former are assembled in inclusionList, the latter in normalList.
a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettich An inclusion is an institution comorphism with the following properties:
68d10d143f29fcff3c637ba24f90e983995ceae6Christian Maeder * the signature translation is an embedding of categories
01e383014b555bbcf639c0ca60c5810b3eff83c0Christian Maeder * the sentence translations are injective
9dac90ec2be2a72e03893095461960d483fe2fc2Christian Maeder * the model translations are isomorphisms
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder The FLIRTS home page: <http://www.informatik.uni-bremen.de/flirts>
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder T. Mossakowski:
a1ed34933c266ce85066acb0d7b20c90cb8eb213Christian Maeder Relating CASL with Other Specification Languages:
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder the Institution Level
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder Theoretical Computer Science 286, p. 367-475, 2002.
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder , lookupComorphism_in_LG
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder , comorphismList
4d56f2fa72e4aec20eb827c11ed49c8cbb7014bdChristian Maeder , inclusionList
4cb215739e9ab13447fa21162482ebe485b47455Christian Maeder , lookupSquare_in_LG
8ef75f1cc0437656bf622cec5ac9e8ea221da8f2Christian Maeder , lookupQTA_in_LG
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maederimport qualified Data.Map as Map
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maederimport Comorphisms.PCoClTyConsHOL2IsabelleHOL
b886e9e5db2098d0112cc4f70aeba232962939ddChristian Maederimport Comorphisms.MonadicHasCASLTranslation
c2fcc35abb03cf0b4ca4b050efeb10827f38c322Christian Maederimport Comorphisms.PCoClTyConsHOL2PairsInIsaHOL
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maeder#ifdef CASLEXTENSIONS
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich#ifndef NOOWLLOGIC
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder#ifdef PROGRAMATICA
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder-- This needs to be seperated for utils/InlineAxioms/InlineAxioms.hs
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaederaddComorphismName :: AnyComorphism -> (String, AnyComorphism)
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaederaddComorphismName c@(Comorphism cid) = (language_name cid, c)
b886e9e5db2098d0112cc4f70aeba232962939ddChristian MaederaddInclusionNames :: AnyComorphism -> ((String, String), AnyComorphism)
15503d903d142d317200149b2d1d642053530365Christian MaederaddInclusionNames c@(Comorphism cid) =
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder ((language_name $ sourceLogic cid, language_name $ targetLogic cid), c)
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian MaederaddUnionNames :: (AnyComorphism, AnyComorphism)
4377600ef3dfb3962ec4c3de76e8486291b644eeChristian Maeder -> ((String, String), (AnyComorphism, AnyComorphism))
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian MaederaddUnionNames (c1@(Comorphism cid1), c2@(Comorphism cid2)) =
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder ( (language_name $ sourceLogic cid1, language_name $ sourceLogic cid2)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederaddMorphismName :: AnyMorphism -> (String, AnyMorphism)
61fa0ac06ede811c7aad54ec4c4202346727368eChristian MaederaddMorphismName m@(Morphism cid) = (language_name cid, m)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederaddModificationName :: AnyModification -> (String, AnyModification)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederaddModificationName m@(Modification cid) = (language_name cid, m)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedercomorphismList :: [AnyComorphism]
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedercomorphismList =
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder [ Comorphism CASL2HasCASL
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder , Comorphism CFOL2IsabelleHOL
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder , Comorphism HolLight2Isabelle
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder , Comorphism Prop2CASL
03a6d8f77f588dc5d3dd6653797fa2362efa1751Christian Maeder , Comorphism CASL2Prop
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , Comorphism DFOL2CASL
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , Comorphism HasCASL2THF0
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder#ifdef CASLEXTENSIONS
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder , Comorphism CASL2Modal
a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian Maeder , Comorphism CASL2ExtModal
bc8cbf12aa172bf5673b92a9e7a0151d4aa4c315Christian Maeder , Comorphism Modal2CASL
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder , Comorphism CASL2CoCASL
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder , Comorphism CASL2CspCASL
a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian Maeder , Comorphism CspCASL2Modal
a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian Maeder , Comorphism cspCASLTrace
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder , Comorphism cspCASLFailure
bc8cbf12aa172bf5673b92a9e7a0151d4aa4c315Christian Maeder , Comorphism CASL_DL2CASL
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder , Comorphism CoCASL2CoPCFOL
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder , Comorphism CoCASL2CoSubCFOL
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder , Comorphism CoCFOL2IsabelleHOL
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder , Comorphism RelScheme2CASL
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder , Comorphism CASL2VSE
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder , Comorphism CASL2VSEImport
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder , Comorphism CASL2VSERefine
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder , Comorphism Maude2CASL
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder , Comorphism CommonLogic2CASL
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder , Comorphism CommonLogic2CommonLogic
a9b59eb2ce961014974276cdae0e9df4419bd212Christian Maeder , Comorphism Adl2CASL
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder#ifndef NOOWLLOGIC
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder , Comorphism OWL22CASL
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder , Comorphism OWL22CommonLogic
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder , Comorphism DMU2OWL2
a3c6d8e0670bf2aa71bc8e2a3b1f45d56dd65e4cChristian Maeder#ifdef PROGRAMATICA
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , Comorphism HasCASL2Haskell
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , Comorphism Haskell2IsabelleHOLCF
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , Comorphism Haskell2IsabelleHOL
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder , Comorphism PCoClTyConsHOL2IsabelleHOL
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder , Comorphism MonadicHasCASL2IsabelleHOL
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , Comorphism PCoClTyConsHOL2PairsInIsaHOL
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , Comorphism HasCASL2IsabelleHOL
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , Comorphism suleCFOL2SoftFOLInduction
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , Comorphism suleCFOL2SoftFOLInduction2
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , Comorphism HasCASL2PCoClTyConsHOL
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder , Comorphism HasCASL2HasCASL
b568982efd0997d877286faa592d81b03c8c67b8Christian Maeder , Comorphism suleCFOL2SoftFOL
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , Comorphism CASL2PCFOL
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich , Comorphism $ CASL2SubCFOL True FormulaDependent -- unique bottoms
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , Comorphism $ CASL2SubCFOL False SubsortBottoms -- keep free types
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , Comorphism $ CASL2SubCFOL False NoMembershipOrCast -- keep free types
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , Comorphism CASL2TopSort
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , Comorphism QBF2Prop
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder , Comorphism Prop2QBF ]
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian MaederinclusionList :: [AnyComorphism]
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian MaederinclusionList =
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder filter (\ (Comorphism cid) -> isInclusionComorphism cid) comorphismList
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederaddComps :: Map.Map (String, String) AnyComorphism
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder -> Map.Map (String, String) AnyComorphism
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder $ cm : map (\ ((l1, l2), c1) ->
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder Map.foldWithKey (\ (l3, l4) c2 m -> if l3 == l2 then
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder case compComorphism c1 c2 of
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Just c3 -> Map.insert (l1, l4) c3 m
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaederaddCompsN :: Map.Map (String, String) AnyComorphism
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder -> Map.Map (String, String) AnyComorphism
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian MaederaddCompsN m = let n = addComps m in
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder if Map.keys m == Map.keys n then m else addCompsN n
e6d5dbbc3308f05197868806e0b860f4f53875f1Christian Maeder{- | Unions of logics, represented as pairs of inclusions.
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder Entries only necessary for non-trivial unions
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder (a trivial union is a union of a sublogic with a superlogic).
363939beade943a02b31004cea09dec34fa8a6d9Christian MaederunionList :: [(AnyComorphism, AnyComorphism)]
363939beade943a02b31004cea09dec34fa8a6d9Christian MaederunionList = []
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedermorphismList :: [AnyMorphism]
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedermorphismList = [] -- for now
e7757995211bd395dc79d26fe017d99375f7d2a6Christian MaedermodificationList :: [AnyModification]
4ed0007ac9caea5b468f202521352d153481423cChristian MaedermodificationList = [Modification MODAL_EMBEDDING]
2c619a4dfdc1df27573eba98e81ed1ace906941dChristian MaedersquareMap :: Map.Map (AnyComorphism, AnyComorphism) [Square]
b886e9e5db2098d0112cc4f70aeba232962939ddChristian MaedersquareMap = Map.empty -- for now
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederlogicGraph :: LogicGraph
e7757995211bd395dc79d26fe017d99375f7d2a6Christian MaederlogicGraph = emptyLogicGraph
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder { logics = Map.fromList $ map addLogicName $ logicList
42b12fba6830ada5057949f825fc27edf5574e5fChristian Maeder ++ concatMap (\ (Comorphism cid) ->
42b12fba6830ada5057949f825fc27edf5574e5fChristian Maeder [Logic $ sourceLogic cid, Logic $ targetLogic cid])
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder comorphismList
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder , comorphisms = Map.fromList $ map addComorphismName comorphismList
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , inclusions = addCompsN $ Map.fromList
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder $ map addInclusionNames inclusionList
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , unions = Map.fromList $ map addUnionNames unionList
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , morphisms = Map.fromList $ map addMorphismName morphismList
9df11f85fd7f8c4745d64464876e84ec4e263692Christian Maeder , modifications = Map.fromList $ map addModificationName modificationList
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers , squares = squareMap
fb328c4f646dd3dd78a9391c5cb58450a3dd0aa9Klaus Luettich , qTATranslations =
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski Map.fromList $ map (\ x@(Comorphism c) -> (show (sourceLogic c), x))
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix ReckerslookupSquare_in_LG :: AnyComorphism -> AnyComorphism -> Result [Square]
819e29dba060687cf391e444e0f6ff88c1908cc3Christian MaederlookupSquare_in_LG com1 com2 = lookupSquare com1 com2 logicGraph
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederlookupComorphism_in_LG :: String -> Result AnyComorphism
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian MaederlookupComorphism_in_LG coname = lookupComorphism coname logicGraph
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder-- translations to logics with quotient term algebra implemented
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederqtaList :: [AnyComorphism]
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder#ifdef CASLEXTENSIONS
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder Comorphism Maude2CASL
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian MaederlookupQTA_in_LG :: String -> Result AnyComorphism
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaederlookupQTA_in_LG coname =
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder qta = qTATranslations logicGraph
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder in if coname `elem` Map.keys qta then
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder return $ Map.findWithDefault (error "") coname qta
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder else fail "no translation found"