LogicGraph.hs revision 0833beb79f31e71a77e39dabdf37b2e77b8525d7
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder{-# LANGUAGE CPP #-}
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederModule : $Header$
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederDescription : the logic graph
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiCopyright : (c) Till Mossakowski and Uni Bremen 2003
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederMaintainer : till@informatik.uni-bremen.de
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : unstable
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederPortability : non-portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederAssembles all the logics and comorphisms into a graph.
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski The modules for the Grothendieck logic are logic graph indepdenent,
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski and here is the logic graph that is used to instantiate these.
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Since the logic graph depends on a large number of modules for the
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder individual logics, this separation of concerns (and possibility for
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder separate compilation) is quite useful.
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder Comorphisms are either logic inclusions, or normal comorphisms.
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder The former are assembled in inclusionList, the latter in normalList.
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder An inclusion is an institution comorphism with the following properties:
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder * the signature translation is an embedding of categories
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder * the sentence translations are injective
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder * the model translations are isomorphisms
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder The FLIRTS home page: <http://www.informatik.uni-bremen.de/flirts>
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder T. Mossakowski:
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder Relating CASL with Other Specification Languages:
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder the Institution Level
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder Theoretical Computer Science 286, p. 367-475, 2002.
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , lookupComorphism_in_LG
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , comorphismList
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , inclusionList
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , lookupSquare_in_LG
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , lookupQTA_in_LG
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport qualified Data.Map as Map
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport Comorphisms.PCoClTyConsHOL2IsabelleHOL
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport Comorphisms.MonadicHasCASLTranslation
f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian Maederimport Comorphisms.PCoClTyConsHOL2PairsInIsaHOL
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder#ifdef CASLEXTENSIONS
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder#ifndef NOOWLLOGIC
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder#ifdef PROGRAMATICA
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- This needs to be seperated for utils/InlineAxioms/InlineAxioms.hs
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederaddComorphismName :: AnyComorphism -> (String, AnyComorphism)
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederaddComorphismName c@(Comorphism cid) = (language_name cid, c)
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederaddInclusionNames :: AnyComorphism -> ((String, String), AnyComorphism)
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederaddInclusionNames c@(Comorphism cid) =
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder ((language_name $ sourceLogic cid, language_name $ targetLogic cid), c)
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian MaederaddUnionNames :: (AnyComorphism, AnyComorphism)
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder -> ((String, String), (AnyComorphism, AnyComorphism))
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian MaederaddUnionNames (c1@(Comorphism cid1), c2@(Comorphism cid2)) =
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder ( (language_name $ sourceLogic cid1, language_name $ sourceLogic cid2)
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian MaederaddMorphismName :: AnyMorphism -> (String, AnyMorphism)
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian MaederaddMorphismName m@(Morphism cid) = (language_name cid, m)
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian MaederaddModificationName :: AnyModification -> (String, AnyModification)
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian MaederaddModificationName m@(Modification cid) = (language_name cid, m)
e6dccba746efe07338d3107fed512e713fd50b28Christian MaedercomorphismList :: [AnyComorphism]
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian MaedercomorphismList =
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder [ Comorphism CASL2HasCASL
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder , Comorphism CFOL2IsabelleHOL
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder , Comorphism Prop2CASL
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder , Comorphism CASL2Prop
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder , Comorphism DFOL2CASL
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder#ifdef CASLEXTENSIONS
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder , Comorphism CASL2Modal
9a6779c8495854bdf36e4a87f98f095e8d0a6e45Christian Maeder , Comorphism Modal2CASL
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder , Comorphism CASL2CoCASL
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder , Comorphism CASL2CspCASL
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder , Comorphism CspCASL2Modal
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maeder , Comorphism cspCASLTrace
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maeder , Comorphism cspCASLFailure
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder , Comorphism CASL_DL2CASL
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder , Comorphism CoCASL2CoPCFOL
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder , Comorphism CoCASL2CoSubCFOL
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder , Comorphism CoCFOL2IsabelleHOL
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder , Comorphism RelScheme2CASL
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder , Comorphism CASL2VSE
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder , Comorphism CASL2VSEImport
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder , Comorphism CASL2VSERefine
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder , Comorphism Maude2CASL
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder --, Comorphism CommonLogic2CASL
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder#ifndef NOOWLLOGIC
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder , Comorphism OWL2CASL
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder --, Comorphism OWL2CommonLogic
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder , Comorphism DMU2OWL
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder#ifdef PROGRAMATICA
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder , Comorphism HasCASL2Haskell
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder , Comorphism Haskell2IsabelleHOLCF
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder , Comorphism Haskell2IsabelleHOL
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder , Comorphism PCoClTyConsHOL2IsabelleHOL
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , Comorphism MonadicHasCASL2IsabelleHOL
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , Comorphism PCoClTyConsHOL2PairsInIsaHOL
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder , Comorphism HasCASL2IsabelleHOL
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder , Comorphism SuleCFOL2SoftFOLInduction
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , Comorphism HasCASL2PCoClTyConsHOL
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder , Comorphism HasCASL2HasCASL
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , Comorphism SuleCFOL2SoftFOL
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder , Comorphism CASL2PCFOL
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder , Comorphism $ CASL2SubCFOL True FormulaDependent -- unique bottoms
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder , Comorphism $ CASL2SubCFOL False SubsortBottoms -- keep free types
6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder , Comorphism $ CASL2SubCFOL False NoMembershipOrCast -- keep free types
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder , Comorphism CASL2TopSort ]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiinclusionList :: [AnyComorphism]
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederinclusionList =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski filter (\ (Comorphism cid) -> isInclusionComorphism cid) comorphismList
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiaddComps :: Map.Map (String, String) AnyComorphism
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder -> Map.Map (String, String) AnyComorphism
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder $ cm : map (\ ((l1, l2), c1) ->
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder Map.foldWithKey (\ (l3, l4) c2 m -> if l3 == l2 then
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder case compComorphism c1 c2 of
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder Just c3 -> Map.insert (l1, l4) c3 m
26d11a256b1433604a3dbc69913b520fff7586acChristian MaederaddCompsN :: Map.Map (String, String) AnyComorphism
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -> Map.Map (String, String) AnyComorphism
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederaddCompsN m = let n = addComps m in
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder if Map.keys m == Map.keys n then m else addCompsN n
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder{- | Unions of logics, represented as pairs of inclusions.
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Entries only necessary for non-trivial unions
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (a trivial union is a union of a sublogic with a superlogic).
b5056cf24da461ee868c4be7b803a76b677fa21dChristian MaederunionList :: [(AnyComorphism, AnyComorphism)]
b5056cf24da461ee868c4be7b803a76b677fa21dChristian MaederunionList = []
b5056cf24da461ee868c4be7b803a76b677fa21dChristian MaedermorphismList :: [AnyMorphism]
b5056cf24da461ee868c4be7b803a76b677fa21dChristian MaedermorphismList = [] -- for now
b5056cf24da461ee868c4be7b803a76b677fa21dChristian MaedermodificationList :: [AnyModification]
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedermodificationList = [Modification MODAL_EMBEDDING]
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedersquareMap :: Map.Map (AnyComorphism, AnyComorphism) [Square]
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedersquareMap = Map.empty --for now
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederlogicGraph :: LogicGraph
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederlogicGraph = emptyLogicGraph
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder { logics = Map.fromList $ map addLogicName $ logicList
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder ++ concatMap (\ (Comorphism cid) ->
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder [Logic $ sourceLogic cid, Logic $ targetLogic cid])
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski comorphismList
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder , comorphisms = Map.fromList $ map addComorphismName comorphismList
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder , inclusions = addCompsN $ Map.fromList
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder $ map addInclusionNames inclusionList
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder , unions = Map.fromList $ map addUnionNames unionList
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder , morphisms = Map.fromList $ map addMorphismName morphismList
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder , modifications = Map.fromList $ map addModificationName modificationList
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder , squares = squareMap
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder , qTATranslations =
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz Map.fromList $ map (\x@(Comorphism c)-> (show (sourceLogic c), x))
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst SchulzlookupSquare_in_LG :: AnyComorphism -> AnyComorphism -> Result [Square]
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian MaederlookupSquare_in_LG com1 com2 = lookupSquare com1 com2 logicGraph
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian MaederlookupComorphism_in_LG :: String -> Result AnyComorphism
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian MaederlookupComorphism_in_LG coname = lookupComorphism coname logicGraph
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder-- translations to logics with quotient term algebra implemented
4e3c46a1ca40d50a045342c5fab25b5db4fa9a87Christian MaederqtaList :: [AnyComorphism]
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder#ifdef CASLEXTENSIONS
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder Comorphism Maude2CASL
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst SchulzlookupQTA_in_LG :: String -> Result AnyComorphism
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst SchulzlookupQTA_in_LG coname =
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder qta = qTATranslations logicGraph
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder in if coname `elem` Map.keys qta then
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder return $ Map.findWithDefault (error "") coname qta
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder else fail "no translation found"