LogicGraph.hs revision 0fefa32a0a32ce300e3a436457f19a04c1ca07f7
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder{-# LANGUAGE CPP #-}
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyModule : $Header$
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyDescription : the logic graph
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyCopyright : (c) Till Mossakowski and Uni Bremen 2003
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyMaintainer : till@informatik.uni-bremen.de
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyStability : unstable
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyPortability : non-portable
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyAssembles all the logics and comorphisms into a graph.
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly The modules for the Grothendieck logic are logic graph indepdenent,
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly and here is the logic graph that is used to instantiate these.
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Since the logic graph depends on a large number of modules for the
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly individual logics, this separation of concerns (and possibility for
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder separate compilation) is quite useful.
66bc8d6e69cde43f1ccbeb76104cf7b8038acd6cChristian Maeder Comorphisms are either logic inclusions, or normal comorphisms.
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder The former are assembled in inclusionList, the latter in normalList.
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder An inclusion is an institution comorphism with the following properties:
56899f6457976a2ee20f6a23f088cb5655b15715Liam O'Reilly * the signature translation is an embedding of categories
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian Maeder * the sentence translations are injective
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly * the model translations are isomorphisms
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder The FLIRTS home page: <http://www.informatik.uni-bremen.de/flirts>
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder T. Mossakowski:
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Relating CASL with Other Specification Languages:
c0833539c8cf577dd3f2497792fbdd818442744cChristian Maeder the Institution Level
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Theoretical Computer Science 286, p. 367-475, 2002.
036ecbd8f721096321f47cf6a354a9d1bf3d032fChristian Maeder , lookupComorphism_in_LG
fa373bc327620e08861294716b4454be8d25669fChristian Maeder , comorphismList
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , inclusionList
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly , lookupSquare_in_LG
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly , lookupQTA_in_LG
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyimport qualified Data.Map as Map
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederimport Comorphisms.PCoClTyConsHOL2IsabelleHOL
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederimport Comorphisms.MonadicHasCASLTranslation
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederimport Comorphisms.PCoClTyConsHOL2PairsInIsaHOL
fa373bc327620e08861294716b4454be8d25669fChristian Maeder#ifdef CASLEXTENSIONS
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder#ifndef NOOWLLOGIC
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder#ifdef PROGRAMATICA
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder-- This needs to be seperated for utils/InlineAxioms/InlineAxioms.hs
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian MaederaddComorphismName :: AnyComorphism -> (String, AnyComorphism)
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian MaederaddComorphismName c@(Comorphism cid) = (language_name cid, c)
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian MaederaddInclusionNames :: AnyComorphism -> ((String, String), AnyComorphism)
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian MaederaddInclusionNames c@(Comorphism cid) =
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder ((language_name $ sourceLogic cid, language_name $ targetLogic cid), c)
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederaddUnionNames :: (AnyComorphism, AnyComorphism)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder -> ((String, String), (AnyComorphism, AnyComorphism))
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian MaederaddUnionNames (c1@(Comorphism cid1), c2@(Comorphism cid2)) =
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder ( (language_name $ sourceLogic cid1, language_name $ sourceLogic cid2)
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederaddMorphismName :: AnyMorphism -> (String, AnyMorphism)
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederaddMorphismName m@(Morphism cid) = (language_name cid, m)
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederaddModificationName :: AnyModification -> (String, AnyModification)
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederaddModificationName m@(Modification cid) = (language_name cid, m)
648fe1220044aac847acbdfbc4155af5556063ebChristian MaedercomorphismList :: [AnyComorphism]
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian MaedercomorphismList =
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder [ Comorphism CASL2HasCASL
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , Comorphism CFOL2IsabelleHOL
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , Comorphism HolLight2Isabelle
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly , Comorphism Prop2CASL
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder , Comorphism CASL2Prop
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder , Comorphism DFOL2CASL
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , Comorphism HasCASL2THF0
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder#ifdef CASLEXTENSIONS
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , Comorphism CASL2Modal
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , Comorphism CASL2ExtModal
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , Comorphism Modal2CASL
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , Comorphism CASL2CoCASL
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , Comorphism CASL2CspCASL
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , Comorphism CspCASL2Modal
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder , Comorphism cspCASLTrace
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder , Comorphism cspCASLFailure
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder , Comorphism CASL_DL2CASL
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , Comorphism CoCASL2CoPCFOL
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , Comorphism CoCASL2CoSubCFOL
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder , Comorphism CoCFOL2IsabelleHOL
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder , Comorphism RelScheme2CASL
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder , Comorphism CASL2VSE
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder , Comorphism CASL2VSEImport
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder , Comorphism CASL2VSERefine
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , Comorphism Maude2CASL
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder , Comorphism CommonLogic2CASL
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , Comorphism CommonLogic2CommonLogic
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , Comorphism Prop2CommonLogic
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , Comorphism SoftFOL2CommonLogic
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , Comorphism Adl2CASL
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder#ifndef NOOWLLOGIC
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , Comorphism OWL22CASL
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly , Comorphism OWL22CommonLogic
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly , Comorphism DMU2OWL2
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder#ifdef PROGRAMATICA
fa373bc327620e08861294716b4454be8d25669fChristian Maeder , Comorphism HasCASL2Haskell
fa373bc327620e08861294716b4454be8d25669fChristian Maeder , Comorphism Haskell2IsabelleHOLCF
fa373bc327620e08861294716b4454be8d25669fChristian Maeder , Comorphism Haskell2IsabelleHOL
fa373bc327620e08861294716b4454be8d25669fChristian Maeder , Comorphism PCoClTyConsHOL2IsabelleHOL
fa373bc327620e08861294716b4454be8d25669fChristian Maeder , Comorphism MonadicHasCASL2IsabelleHOL
fa373bc327620e08861294716b4454be8d25669fChristian Maeder , Comorphism PCoClTyConsHOL2PairsInIsaHOL
fa373bc327620e08861294716b4454be8d25669fChristian Maeder , Comorphism HasCASL2IsabelleHOL
fa373bc327620e08861294716b4454be8d25669fChristian Maeder , Comorphism suleCFOL2SoftFOLInduction
fa373bc327620e08861294716b4454be8d25669fChristian Maeder , Comorphism suleCFOL2SoftFOLInduction2
fa373bc327620e08861294716b4454be8d25669fChristian Maeder , Comorphism HasCASL2PCoClTyConsHOL
fa373bc327620e08861294716b4454be8d25669fChristian Maeder , Comorphism HasCASL2HasCASL
fa373bc327620e08861294716b4454be8d25669fChristian Maeder , Comorphism suleCFOL2SoftFOL
fa373bc327620e08861294716b4454be8d25669fChristian Maeder , Comorphism CASL2PCFOL
fa373bc327620e08861294716b4454be8d25669fChristian Maeder , Comorphism $ CASL2SubCFOL True FormulaDependent -- unique bottoms
fa373bc327620e08861294716b4454be8d25669fChristian Maeder , Comorphism $ CASL2SubCFOL False SubsortBottoms -- keep free types
fa373bc327620e08861294716b4454be8d25669fChristian Maeder , Comorphism $ CASL2SubCFOL False NoMembershipOrCast -- keep free types
fa373bc327620e08861294716b4454be8d25669fChristian Maeder , Comorphism CASL2TopSort
fa373bc327620e08861294716b4454be8d25669fChristian Maeder , Comorphism QBF2Prop
fa373bc327620e08861294716b4454be8d25669fChristian Maeder , Comorphism Prop2QBF ]
fa373bc327620e08861294716b4454be8d25669fChristian MaederinclusionList :: [AnyComorphism]
fa373bc327620e08861294716b4454be8d25669fChristian MaederinclusionList =
fa373bc327620e08861294716b4454be8d25669fChristian Maeder filter (\ (Comorphism cid) -> isInclusionComorphism cid) comorphismList
fa373bc327620e08861294716b4454be8d25669fChristian MaederaddComps :: Map.Map (String, String) AnyComorphism
fa373bc327620e08861294716b4454be8d25669fChristian Maeder -> Map.Map (String, String) AnyComorphism
fa373bc327620e08861294716b4454be8d25669fChristian Maeder $ cm : map (\ ((l1, l2), c1) ->
fa373bc327620e08861294716b4454be8d25669fChristian Maeder Map.foldWithKey (\ (l3, l4) c2 m -> if l3 == l2 then
fa373bc327620e08861294716b4454be8d25669fChristian Maeder case compComorphism c1 c2 of
fa373bc327620e08861294716b4454be8d25669fChristian Maeder Just c3 -> Map.insert (l1, l4) c3 m
fa373bc327620e08861294716b4454be8d25669fChristian MaederaddCompsN :: Map.Map (String, String) AnyComorphism
fa373bc327620e08861294716b4454be8d25669fChristian Maeder -> Map.Map (String, String) AnyComorphism
fa373bc327620e08861294716b4454be8d25669fChristian MaederaddCompsN m = let n = addComps m in
fa373bc327620e08861294716b4454be8d25669fChristian Maeder if Map.keys m == Map.keys n then m else addCompsN n
fa373bc327620e08861294716b4454be8d25669fChristian Maeder{- | Unions of logics, represented as pairs of inclusions.
fa373bc327620e08861294716b4454be8d25669fChristian Maeder Entries only necessary for non-trivial unions
fa373bc327620e08861294716b4454be8d25669fChristian Maeder (a trivial union is a union of a sublogic with a superlogic).
fa373bc327620e08861294716b4454be8d25669fChristian MaederunionList :: [(AnyComorphism, AnyComorphism)]
fa373bc327620e08861294716b4454be8d25669fChristian MaederunionList = []
56899f6457976a2ee20f6a23f088cb5655b15715Liam O'ReillymorphismList :: [AnyMorphism]
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian MaedermorphismList = [] -- for now
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian MaedermodificationList :: [AnyModification]
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian MaedermodificationList = [Modification MODAL_EMBEDDING]
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian MaedersquareMap :: Map.Map (AnyComorphism, AnyComorphism) [Square]
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian MaedersquareMap = Map.empty -- for now
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian MaederlogicGraph :: LogicGraph
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian MaederlogicGraph = emptyLogicGraph
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder { logics = Map.fromList $ map addLogicName $ logicList
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder ++ concatMap (\ (Comorphism cid) ->
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder [Logic $ sourceLogic cid, Logic $ targetLogic cid])
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder comorphismList
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder , comorphisms = Map.fromList $ map addComorphismName comorphismList
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder , inclusions = addCompsN $ Map.fromList
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder $ map addInclusionNames inclusionList
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder , unions = Map.fromList $ map addUnionNames unionList
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder , morphisms = Map.fromList $ map addMorphismName morphismList
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder , modifications = Map.fromList $ map addModificationName modificationList
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder , squares = squareMap
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder , qTATranslations =
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Map.fromList $ map (\ x@(Comorphism c) -> (show (sourceLogic c), x))
66bc8d6e69cde43f1ccbeb76104cf7b8038acd6cChristian MaederlookupSquare_in_LG :: AnyComorphism -> AnyComorphism -> Result [Square]
66bc8d6e69cde43f1ccbeb76104cf7b8038acd6cChristian MaederlookupSquare_in_LG com1 com2 = lookupSquare com1 com2 logicGraph
66bc8d6e69cde43f1ccbeb76104cf7b8038acd6cChristian MaederlookupComorphism_in_LG :: String -> Result AnyComorphism
66bc8d6e69cde43f1ccbeb76104cf7b8038acd6cChristian MaederlookupComorphism_in_LG coname = lookupComorphism coname logicGraph
ace03c3051e5c5144e43ae78cae73f6a29dde6d5Christian Maeder-- translations to logics with quotient term algebra implemented
ace03c3051e5c5144e43ae78cae73f6a29dde6d5Christian MaederqtaList :: [AnyComorphism]
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder#ifdef CASLEXTENSIONS
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder Comorphism Maude2CASL
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillylookupQTA_in_LG :: String -> Result AnyComorphism
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillylookupQTA_in_LG coname =
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly qta = qTATranslations logicGraph
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly in if coname `elem` Map.keys qta then
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder return $ Map.findWithDefault (error "") coname qta
8e9c3881fb6e710b1e08bf5ac8ff9d393df2e74eChristian Maeder else fail "no translation found"