2665d7759e63acff0bcd4135678f2cc6f2041d46Christian Maeder{-# LANGUAGE CPP #-}
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaederDescription : the logic graph
aa4679922a8363b4e494079f53aaf4f64554aae0Christian MaederCopyright : (c) Till Mossakowski and Uni Bremen 2003
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
1d581e55c7ec020a445684310394c3a5fc056e96Christian MaederMaintainer : till@informatik.uni-bremen.de
aa4679922a8363b4e494079f53aaf4f64554aae0Christian MaederStability : unstable
aa4679922a8363b4e494079f53aaf4f64554aae0Christian MaederPortability : non-portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederAssembles all the logics and comorphisms into a graph.
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski The modules for the Grothendieck logic are logic graph indepdenent,
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski and here is the logic graph that is used to instantiate these.
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski Since the logic graph depends on a large number of modules for the
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski individual logics, this separation of concerns (and possibility for
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski separate compilation) is quite useful.
7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowski Comorphisms are either logic inclusions, or normal comorphisms.
7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowski The former are assembled in inclusionList, the latter in normalList.
7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowski An inclusion is an institution comorphism with the following properties:
7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowski * the signature translation is an embedding of categories
7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowski * the sentence translations are injective
7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowski * the model translations are isomorphisms
1d581e55c7ec020a445684310394c3a5fc056e96Christian Maeder The FLIRTS home page: <http://www.informatik.uni-bremen.de/flirts>
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski T. Mossakowski:
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski Relating CASL with Other Specification Languages:
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski the Institution Level
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski Theoretical Computer Science 286, p. 367-475, 2002.
aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder , lookupComorphism_in_LG
aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder , comorphismList
6a00a2b0961b1553d4f5106d655f6f90bb6c1777Christian Maeder , inclusionList
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu , lookupSquare_in_LG
342beb91d58bcf41178240c37d0f6c0c4f83c53eMihai Codescu , lookupQTA_in_LG
2add146602f6eb47058b67142bd91ae40a32fd66Christian Maederimport qualified Data.Map as Map
aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maederimport Comorphisms.PCoClTyConsHOL2IsabelleHOL
4278792968573e39da24e8eb73f931ba9c15cd50Christian Maederimport Comorphisms.MonadicHasCASLTranslation
e4257c7b13b1122a1e6ec9e43753f3e565b88449Christian Maederimport Comorphisms.PCoClTyConsHOL2PairsInIsaHOL
c64d33a7fbeae730cbe65193fe3cc24e7aa1ddd6Christian Maeder#ifdef CASLEXTENSIONS
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederimport Comorphisms.ExtModal2ExtModalNoSubsorts
c4451dc7da4a15726ba96179aecf046a5df5cae1Christian Maeder#ifndef NOOWLLOGIC
233c9bf946d6f3689b7901dfab3255300c873187Christian Maeder#ifdef CASLEXTENSIONS
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder#ifdef PROGRAMATICA
bf76f4fcf07abaebea587df8135de8356c26a363Till Mossakowski-- This needs to be seperated for utils/InlineAxioms/InlineAxioms.hs
aa4679922a8363b4e494079f53aaf4f64554aae0Christian MaederaddComorphismName :: AnyComorphism -> (String, AnyComorphism)
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till MossakowskiaddComorphismName c@(Comorphism cid) = (language_name cid, c)
aa4679922a8363b4e494079f53aaf4f64554aae0Christian MaederaddInclusionNames :: AnyComorphism -> ((String, String), AnyComorphism)
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till MossakowskiaddInclusionNames c@(Comorphism cid) =
aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder ((language_name $ sourceLogic cid, language_name $ targetLogic cid), c)
aa4679922a8363b4e494079f53aaf4f64554aae0Christian MaederaddUnionNames :: (AnyComorphism, AnyComorphism)
aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder -> ((String, String), (AnyComorphism, AnyComorphism))
aa4679922a8363b4e494079f53aaf4f64554aae0Christian MaederaddUnionNames (c1@(Comorphism cid1), c2@(Comorphism cid2)) =
aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder ( (language_name $ sourceLogic cid1, language_name $ sourceLogic cid2)
2b565fe5cfb9f99857fd25b52304758d8544e266Mihai CodescuaddMorphismName :: AnyMorphism -> (String, AnyMorphism)
2b565fe5cfb9f99857fd25b52304758d8544e266Mihai CodescuaddMorphismName m@(Morphism cid) = (language_name cid, m)
dd1a0e54a051de7a8a49e677f0d4082b640c75c7Christian MaederaddModificationName :: AnyModification -> (String, AnyModification)
2b565fe5cfb9f99857fd25b52304758d8544e266Mihai CodescuaddModificationName m@(Modification cid) = (language_name cid, m)
6a00a2b0961b1553d4f5106d655f6f90bb6c1777Christian MaedercomorphismList :: [AnyComorphism]
6a00a2b0961b1553d4f5106d655f6f90bb6c1777Christian MaedercomorphismList =
aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder [ Comorphism CASL2HasCASL
aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder , Comorphism CFOL2IsabelleHOL
e16215e4bbdbab16b50cd2e0e6fff19682baaa39Soeren D. Schulze , Comorphism CommonLogic2IsabelleHOL
6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu , Comorphism HolLight2Isabelle
aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder , Comorphism Prop2CASL
228f49c7667370745d5b07c12e49b06b55e2dab5Christian Maeder , Comorphism CASL2Prop
b0614ce452d26051ba4c94d3b41156fb3f4b100eKristina Sojakova , Comorphism DFOL2CASL
f9a337c44fbf30e9ea2058ccdb023cdb54bf92ffJonathan von Schroeder , Comorphism HasCASL2THFP_P
81e71677da25aee1caa7fef177c45ddd69bbf22eJonathan von Schroeder , Comorphism THFP2THF0
7cad2789c70e29f733effaed840d034e4a9e7aadJonathan von Schroeder , Comorphism THFP_P2HasCASL
bf453a6867cca0aa530bc8cac9eed9c3f70594b4Jonathan von Schroeder , Comorphism THFP_P2THFP
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder , Comorphism CASL2Hybrid
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder , Comorphism Hybrid2CASL
c64d33a7fbeae730cbe65193fe3cc24e7aa1ddd6Christian Maeder#ifdef CASLEXTENSIONS
aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder , Comorphism CASL2Modal
ce5fb67d0cc1313da4e63feeb6da2d318773f589Christian Maeder , Comorphism CASL2ExtModal
aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder , Comorphism Modal2CASL
91e9fabb7e21a8ca74be83cfbb06e79b99f4e42cChristian Maeder , Comorphism ExtModal2CASL
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder , Comorphism ExtModal2ExtModalNoSubsorts
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder , Comorphism ExtModal2ExtModalTotal
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder , Comorphism ExtModal2HasCASL
aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder , Comorphism CASL2CoCASL
aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder , Comorphism CASL2CspCASL
9533de2aedd63b932f9941016ad29654711c77c7Christian Maeder , Comorphism CspCASL2Modal
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder , Comorphism cspCASLTrace
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder , Comorphism cspCASLFailure
7fd4c34af8415eb699517b1b238a24c02a9a2e9bDominik Luecke , Comorphism CASL_DL2CASL
aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder , Comorphism CoCASL2CoPCFOL
aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder , Comorphism CoCASL2CoSubCFOL
7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowski , Comorphism CoCFOL2IsabelleHOL
a406e4512e77395a77726ad41e16108f571e3d92Mihai Codescu , Comorphism RelScheme2CASL
dd1a0e54a051de7a8a49e677f0d4082b640c75c7Christian Maeder , Comorphism CASL2VSE
0b06cf161496343f3320e45d228ad4bc2f1f2b0fMihai Codescu , Comorphism CASL2VSEImport
31d95eb87da83c0463988e5ca2a520a4b1af5e4fMihai Codescu , Comorphism CASL2VSERefine
a836ddc0778b3eb7636b831a3ca0afabab6c13c0mcodescu , Comorphism CASL2Skolem
a836ddc0778b3eb7636b831a3ca0afabab6c13c0mcodescu , Comorphism CASL2NNF
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu , Comorphism CASL2Prenex
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián Riesco , Comorphism Maude2CASL
1233e4dc235245cee0a6888f71cba0377934ae8fChristian Maeder , Comorphism (CL2CFOL folsl {compact = False})
1233e4dc235245cee0a6888f71cba0377934ae8fChristian Maeder , Comorphism (CL2CFOL fullclsl)
1233e4dc235245cee0a6888f71cba0377934ae8fChristian Maeder , Comorphism (CL2CFOL folsl)
1233e4dc235245cee0a6888f71cba0377934ae8fChristian Maeder , Comorphism (CL2CFOL fullclsl {compact = True})
91cba1f3e1492aaa327d5558583c684aaebc67deEugen Kuksa , Comorphism CommonLogicModuleElimination
e3ed0ae47dd551ddd9d74c33fff11b19a23a1d97Eugen Kuksa , Comorphism Prop2CommonLogic
0fefa32a0a32ce300e3a436457f19a04c1ca07f7Eugen Kuksa , Comorphism SoftFOL2CommonLogic
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian Maeder , Comorphism Adl2CASL
c4451dc7da4a15726ba96179aecf046a5df5cae1Christian Maeder#ifndef NOOWLLOGIC
f88469d6b07144237111e8148a7acf0652127066Christian Maeder , Comorphism OWL22CASL
a14f8718962397b20a50b662f2e5b3101991b195Francisc Nicolae Bungiu , Comorphism OWL22CommonLogic
6122c5e77abe39b3c296c2f273159178bd7a3e71Francisc Nicolae Bungiu , Comorphism DMU2OWL2
1ea4b86ab3f5a34824945e099176785070496d2dChristian Maeder , Comorphism CASL2OWL
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Mance , Comorphism Propositional2OWL2
233c9bf946d6f3689b7901dfab3255300c873187Christian Maeder#ifdef CASLEXTENSIONS
233c9bf946d6f3689b7901dfab3255300c873187Christian Maeder , Comorphism ExtModal2OWL
7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowski#ifdef PROGRAMATICA
ebe4d5a8e51f6009d6e7ca465f5963ce46a07fd2Christian Maeder , Comorphism HasCASL2Haskell
7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowski , Comorphism Haskell2IsabelleHOLCF
7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowski , Comorphism Haskell2IsabelleHOL
ebe4d5a8e51f6009d6e7ca465f5963ce46a07fd2Christian Maeder , Comorphism PCoClTyConsHOL2IsabelleHOL
4278792968573e39da24e8eb73f931ba9c15cd50Christian Maeder , Comorphism MonadicHasCASL2IsabelleHOL
e4257c7b13b1122a1e6ec9e43753f3e565b88449Christian Maeder , Comorphism PCoClTyConsHOL2PairsInIsaHOL
ebe4d5a8e51f6009d6e7ca465f5963ce46a07fd2Christian Maeder , Comorphism HasCASL2IsabelleHOL
e657b7607878955a69f627e959c7cf99133f7f76Christian Maeder , Comorphism suleCFOL2SoftFOLInduction
e657b7607878955a69f627e959c7cf99133f7f76Christian Maeder , Comorphism suleCFOL2SoftFOLInduction2
ebe4d5a8e51f6009d6e7ca465f5963ce46a07fd2Christian Maeder , Comorphism HasCASL2PCoClTyConsHOL
ebe4d5a8e51f6009d6e7ca465f5963ce46a07fd2Christian Maeder , Comorphism HasCASL2HasCASL
e657b7607878955a69f627e959c7cf99133f7f76Christian Maeder , Comorphism suleCFOL2SoftFOL
6b9d418b9d00bf4f5b37be276a48bed04965a0edEugen Kuksa , Comorphism suleCFOL2TPTP
aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder , Comorphism CASL2PCFOL
7c8e78fd66aca3d24b77a9f9635f201e2f576d27Christian Maeder , Comorphism $ CASL2SubCFOL True FormulaDependent -- unique bottoms
7c8e78fd66aca3d24b77a9f9635f201e2f576d27Christian Maeder , Comorphism $ CASL2SubCFOL False SubsortBottoms -- keep free types
7c8e78fd66aca3d24b77a9f9635f201e2f576d27Christian Maeder , Comorphism $ CASL2SubCFOL False NoMembershipOrCast -- keep free types
eb8bd58b5980a12a7f60ed40f9baf7263bc53946Jonathan von Schroeder , Comorphism CASL2TopSort
eb8bd58b5980a12a7f60ed40f9baf7263bc53946Jonathan von Schroeder , Comorphism QBF2Prop
f3a838d9e2932da421939f348a2c3d31ded88989Daniel Calegari , Comorphism Prop2QBF
9f226cec9f978edaba67aee4c4e04e3d3b994b87Daniel Calegari , Comorphism CSMOF2CASL
9f226cec9f978edaba67aee4c4e04e3d3b994b87Daniel Calegari , Comorphism QVTR2CASL ]
ebe4d5a8e51f6009d6e7ca465f5963ce46a07fd2Christian MaederinclusionList :: [AnyComorphism]
ebe4d5a8e51f6009d6e7ca465f5963ce46a07fd2Christian MaederinclusionList =
6a00a2b0961b1553d4f5106d655f6f90bb6c1777Christian Maeder filter (\ (Comorphism cid) -> isInclusionComorphism cid) comorphismList
a4a01ddab418043fd569676d24d5df7f23a84490Christian MaederaddComps :: Map.Map (String, String) AnyComorphism
a4a01ddab418043fd569676d24d5df7f23a84490Christian Maeder -> Map.Map (String, String) AnyComorphism
a4a01ddab418043fd569676d24d5df7f23a84490Christian Maeder $ cm : map (\ ((l1, l2), c1) ->
a74f814d3b445eadad6f68737a98a7a303698affChristian Maeder Map.foldWithKey (\ (l3, l4) c2 m -> if l3 == l2 then
a4a01ddab418043fd569676d24d5df7f23a84490Christian Maeder case compComorphism c1 c2 of
a4a01ddab418043fd569676d24d5df7f23a84490Christian Maeder Just c3 -> Map.insert (l1, l4) c3 m
a4a01ddab418043fd569676d24d5df7f23a84490Christian MaederaddCompsN :: Map.Map (String, String) AnyComorphism
a4a01ddab418043fd569676d24d5df7f23a84490Christian Maeder -> Map.Map (String, String) AnyComorphism
a4a01ddab418043fd569676d24d5df7f23a84490Christian MaederaddCompsN m = let n = addComps m in
a4a01ddab418043fd569676d24d5df7f23a84490Christian Maeder if Map.keys m == Map.keys n then m else addCompsN n
6e29f2565572024b963af2f6d486b567307dc770Till Mossakowski{- | Unions of logics, represented as pairs of inclusions.
934473566cf3a8e4044ed10e408b4c44079684b1Christian Maeder Entries only necessary for non-trivial unions
6e29f2565572024b963af2f6d486b567307dc770Till Mossakowski (a trivial union is a union of a sublogic with a superlogic).
aa4679922a8363b4e494079f53aaf4f64554aae0Christian MaederunionList :: [(AnyComorphism, AnyComorphism)]
9d34a8049237647d0188ee2ec88db2dc45f1f848Till MossakowskiunionList = []
2b565fe5cfb9f99857fd25b52304758d8544e266Mihai CodescumorphismList :: [AnyMorphism]
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaedermorphismList = [] -- for now
2b565fe5cfb9f99857fd25b52304758d8544e266Mihai CodescumodificationList :: [AnyModification]
2b565fe5cfb9f99857fd25b52304758d8544e266Mihai CodescumodificationList = [Modification MODAL_EMBEDDING]
c7e03d0708369f944b6f235057b39142a21599f2Mihai CodescusquareMap :: Map.Map (AnyComorphism, AnyComorphism) [Square]
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian MaedersquareMap = Map.empty -- for now
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till MossakowskilogicGraph :: LogicGraph
1cbee24256e1c03a06103283c9dd8dcd97a10f70Christian MaederlogicGraph = emptyLogicGraph
d0916b96ca9f90822c0bb6062b13d5de83bf410aSoeren D. Schulze { logics = Map.fromList $ map addLogicName (logicList
ebe4d5a8e51f6009d6e7ca465f5963ce46a07fd2Christian Maeder ++ concatMap (\ (Comorphism cid) ->
ebe4d5a8e51f6009d6e7ca465f5963ce46a07fd2Christian Maeder [Logic $ sourceLogic cid, Logic $ targetLogic cid])
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa comorphismList)
6a00a2b0961b1553d4f5106d655f6f90bb6c1777Christian Maeder , comorphisms = Map.fromList $ map addComorphismName comorphismList
a4a01ddab418043fd569676d24d5df7f23a84490Christian Maeder , inclusions = addCompsN $ Map.fromList
a4a01ddab418043fd569676d24d5df7f23a84490Christian Maeder $ map addInclusionNames inclusionList
aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder , unions = Map.fromList $ map addUnionNames unionList
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder , morphisms = Map.fromList $ map addMorphismName morphismList
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu , modifications = Map.fromList $ map addModificationName modificationList
342beb91d58bcf41178240c37d0f6c0c4f83c53eMihai Codescu , squares = squareMap
342beb91d58bcf41178240c37d0f6c0c4f83c53eMihai Codescu , qTATranslations =
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian Maeder Map.fromList $ map (\ x@(Comorphism c) -> (show (sourceLogic c), x))
c7e03d0708369f944b6f235057b39142a21599f2Mihai CodesculookupSquare_in_LG :: AnyComorphism -> AnyComorphism -> Result [Square]
c7e03d0708369f944b6f235057b39142a21599f2Mihai CodesculookupSquare_in_LG com1 com2 = lookupSquare com1 com2 logicGraph
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskilookupComorphism_in_LG :: String -> Result AnyComorphism
aa4679922a8363b4e494079f53aaf4f64554aae0Christian MaederlookupComorphism_in_LG coname = lookupComorphism coname logicGraph
342beb91d58bcf41178240c37d0f6c0c4f83c53eMihai Codescu-- translations to logics with quotient term algebra implemented
342beb91d58bcf41178240c37d0f6c0c4f83c53eMihai CodescuqtaList :: [AnyComorphism]
f66d509b0e67058c91f60a7c20d6e58b67ac7720Christian Maeder#ifdef CASLEXTENSIONS
f66d509b0e67058c91f60a7c20d6e58b67ac7720Christian Maeder Comorphism Maude2CASL
342beb91d58bcf41178240c37d0f6c0c4f83c53eMihai CodesculookupQTA_in_LG :: String -> Result AnyComorphism
342beb91d58bcf41178240c37d0f6c0c4f83c53eMihai CodesculookupQTA_in_LG coname =
342beb91d58bcf41178240c37d0f6c0c4f83c53eMihai Codescu qta = qTATranslations logicGraph
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian Maeder in if coname `elem` Map.keys qta then
342beb91d58bcf41178240c37d0f6c0c4f83c53eMihai Codescu return $ Map.findWithDefault (error "") coname qta
342beb91d58bcf41178240c37d0f6c0c4f83c53eMihai Codescu else fail "no translation found"