LogicGraph.hs revision 342beb91d58bcf41178240c37d0f6c0c4f83c53e
66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder{-# LANGUAGE CPP #-}
66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder{- |
66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederModule : $Header$
66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederDescription : the logic graph
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaederCopyright : (c) Till Mossakowski and Uni Bremen 2003
66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
ffd01020a4f35f434b912844ad6e0d6918fadffdChristian Maeder
66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederMaintainer : till@informatik.uni-bremen.de
66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederStability : unstable
fb69cd512eab767747f109e40322df7cae2f7bdfChristian MaederPortability : non-portable
fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder
fb69cd512eab767747f109e40322df7cae2f7bdfChristian MaederAssembles all the logics and comorphisms into a graph.
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder The modules for the Grothendieck logic are logic graph indepdenent,
fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder and here is the logic graph that is used to instantiate these.
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder Since the logic graph depends on a large number of modules for the
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder individual logics, this separation of concerns (and possibility for
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder separate compilation) is quite useful.
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder Comorphisms are either logic inclusions, or normal comorphisms.
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder The former are assembled in inclusionList, the latter in normalList.
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder An inclusion is an institution comorphism with the following properties:
08b724e8dcbba5820d80f0974b9a5385140815baChristian Maeder
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder * the signature translation is an embedding of categories
712f5e5ca1c3a5cfdd28518154ecf2dd0994cdb5Christian Maeder
da245da15da78363c896e44ea97a14ab1f83eb50Christian Maeder * the sentence translations are injective
f71a8dcf94fd9eb3c9800e16dcdc5e5ff74e5c22Christian Maeder
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder * the model translations are isomorphisms
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder References:
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder The FLIRTS home page: <http://www.informatik.uni-bremen.de/flirts>
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder T. Mossakowski:
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder Relating CASL with Other Specification Languages:
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder the Institution Level
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder Theoretical Computer Science 286, p. 367-475, 2002.
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder-}
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maedermodule Comorphisms.LogicGraph
cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maeder ( logicGraph
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , lookupComorphism_in_LG
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , comorphismList
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , inclusionList
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , lookupSquare_in_LG
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , lookupQTA_in_LG
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder ) where
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Data.Maybe
fb50920e621bfc152c19147cb52077ff06b3526bChristian Maederimport Data.List
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maederimport qualified Data.Map as Map
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederimport Common.Result
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederimport Logic.Logic
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederimport Logic.Grothendieck
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederimport Logic.Comorphism
fb50920e621bfc152c19147cb52077ff06b3526bChristian Maederimport Logic.Modification
fb50920e621bfc152c19147cb52077ff06b3526bChristian Maederimport Logic.Morphism
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederimport Modifications.ModalEmbedding
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederimport Comorphisms.CASL2PCFOL
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederimport Comorphisms.CASL2SubCFOL
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederimport Comorphisms.CASL2HasCASL
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederimport Comorphisms.HasCASL2HasCASL
fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maederimport Comorphisms.CFOL2IsabelleHOL
cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maederimport Comorphisms.SuleCFOL2SoftFOL
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maederimport Comorphisms.Prop2CASL
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederimport Comorphisms.CASL2Prop
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederimport Comorphisms.HasCASL2IsabelleHOL
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederimport Comorphisms.PCoClTyConsHOL2IsabelleHOL
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederimport Comorphisms.MonadicHasCASLTranslation
fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maederimport Comorphisms.PCoClTyConsHOL2PairsInIsaHOL
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Comorphisms.HasCASL2PCoClTyConsHOL
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Comorphisms.CASL2TopSort
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Comorphisms.DFOL2CASL
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder#ifdef CASLEXTENSIONS
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Comorphisms.CoCFOL2IsabelleHOL
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Comorphisms.CoCASL2CoPCFOL
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Comorphisms.CoCASL2CoSubCFOL
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Comorphisms.CASL2Modal
31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maederimport Comorphisms.Modal2CASL
31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maederimport Comorphisms.CASL2CoCASL
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederimport Comorphisms.CASL2CspCASL
31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maederimport Comorphisms.CspCASL2Modal
628310b42327ad76ce471caf0dde6563d6fa6307Christian Maederimport CspCASL.Comorphisms
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Comorphisms.CASL_DL2CASL
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Comorphisms.RelScheme2CASL
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Comorphisms.CASL2VSE
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Comorphisms.CASL2VSERefine
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Comorphisms.CASL2VSEImport
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Comorphisms.Maude2CASL
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder#endif
628310b42327ad76ce471caf0dde6563d6fa6307Christian Maeder#ifndef NOOWLLOGIC
628310b42327ad76ce471caf0dde6563d6fa6307Christian Maederimport Comorphisms.OWL2CASL
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder#endif
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder#ifdef PROGRAMATICA
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederimport Comorphisms.HasCASL2Haskell
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederimport Comorphisms.Haskell2IsabelleHOLCF
ffd01020a4f35f434b912844ad6e0d6918fadffdChristian Maeder#endif
ffd01020a4f35f434b912844ad6e0d6918fadffdChristian Maeder-- This needs to be seperated for utils/InlineAxioms/InlineAxioms.hs
ffd01020a4f35f434b912844ad6e0d6918fadffdChristian Maederimport Comorphisms.LogicList
f0742398d4587242b1a115de113cd17f63dcb6d0Christian Maeder
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian MaederaddComorphismName :: AnyComorphism -> (String, AnyComorphism)
715ffaf874309df081d1e1cd8e05073fc1227729Christian MaederaddComorphismName c@(Comorphism cid) = (language_name cid, c)
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder
05e2a3161e4589a717c6fe5c7306820273a473c5Christian MaederaddInclusionNames :: AnyComorphism -> ((String, String), AnyComorphism)
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaederaddInclusionNames c@(Comorphism cid) =
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder ((language_name $ sourceLogic cid, language_name $ targetLogic cid), c)
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder
05e2a3161e4589a717c6fe5c7306820273a473c5Christian MaederaddUnionNames :: (AnyComorphism, AnyComorphism)
c1031ac42b3f3d7d0fe7d9d6b54423a092d473a0Christian Maeder -> ((String, String), (AnyComorphism, AnyComorphism))
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaederaddUnionNames (c1@(Comorphism cid1), c2@(Comorphism cid2)) =
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder ( (language_name $ sourceLogic cid1, language_name $ sourceLogic cid2)
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder , (c1, c2))
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaederaddMorphismName :: AnyMorphism -> (String, AnyMorphism)
fb69cd512eab767747f109e40322df7cae2f7bdfChristian MaederaddMorphismName m@(Morphism cid) = (language_name cid, m)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederaddModificationName :: AnyModification -> (String, AnyModification)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederaddModificationName m@(Modification cid) = (language_name cid, m)
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder
05e2a3161e4589a717c6fe5c7306820273a473c5Christian MaedercomorphismList :: [AnyComorphism]
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian MaedercomorphismList =
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder [ Comorphism CASL2HasCASL
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , Comorphism CFOL2IsabelleHOL
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , Comorphism Prop2CASL
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , Comorphism CASL2Prop
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , Comorphism DFOL2CASL
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder#ifdef CASLEXTENSIONS
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , Comorphism CASL2Modal
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder , Comorphism Modal2CASL
772abb916b994ad9461ddb11c88829251c5ac87aChristian Maeder , Comorphism CASL2CoCASL
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder , Comorphism CASL2CspCASL
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder , Comorphism CspCASL2Modal
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder , Comorphism cspCASLTrace
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder , Comorphism cspCASLFailure
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder , Comorphism CASL_DL2CASL
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder , Comorphism CoCASL2CoPCFOL
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder , Comorphism CoCASL2CoSubCFOL
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder , Comorphism CoCFOL2IsabelleHOL
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder , Comorphism RelScheme2CASL
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder , Comorphism CASL2VSE
08b724e8dcbba5820d80f0974b9a5385140815baChristian Maeder , Comorphism CASL2VSEImport
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder , Comorphism CASL2VSERefine
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder , Comorphism Maude2CASL
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder#endif
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder#ifndef NOOWLLOGIC
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder , Comorphism OWL2CASL
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder#endif
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder#ifdef PROGRAMATICA
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder , Comorphism HasCASL2Haskell
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder , Comorphism Haskell2IsabelleHOLCF
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder , Comorphism Haskell2IsabelleHOL
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder#endif
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder , Comorphism PCoClTyConsHOL2IsabelleHOL
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder , Comorphism MonadicHasCASL2IsabelleHOL
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder , Comorphism PCoClTyConsHOL2PairsInIsaHOL
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder , Comorphism HasCASL2IsabelleHOL
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder , Comorphism SuleCFOL2SoftFOLInduction
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder , Comorphism HasCASL2PCoClTyConsHOL
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder , Comorphism HasCASL2HasCASL
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder , Comorphism SuleCFOL2SoftFOL
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder , Comorphism CASL2PCFOL
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder , Comorphism $ CASL2SubCFOL True FormulaDependent -- unique bottoms
, Comorphism $ CASL2SubCFOL False SubsortBottoms -- keep free types
, Comorphism $ CASL2SubCFOL False NoMembershipOrCast -- keep free types
, Comorphism CASL2TopSort ]
inclusionList :: [AnyComorphism]
inclusionList =
filter (\ (Comorphism cid) -> isInclusionComorphism cid) comorphismList
addComps :: Map.Map (String, String) AnyComorphism
-> Map.Map (String, String) AnyComorphism
addComps cm = Map.unions
$ cm : map (\ ((l1, l2), c1) ->
Map.foldWithKey (\ (l3, l4) c2 m -> if l3 == l2 then
case compComorphism c1 c2 of
Just c3 -> Map.insert (l1, l4) c3 m
_ -> m
else m) (Map.empty) cm) (Map.toList cm)
addCompsN :: Map.Map (String, String) AnyComorphism
-> Map.Map (String, String) AnyComorphism
addCompsN m = let n = addComps m in
if Map.keys m == Map.keys n then m else addCompsN n
{- | Unions of logics, represented as pairs of inclusions.
Entries only necessary for non-trivial unions
(a trivial union is a union of a sublogic with a superlogic).
-}
unionList :: [(AnyComorphism, AnyComorphism)]
unionList = []
morphismList :: [AnyMorphism]
morphismList = [] -- for now
modificationList :: [AnyModification]
modificationList = [Modification MODAL_EMBEDDING]
squareMap :: Map.Map (AnyComorphism, AnyComorphism) [Square]
squareMap = Map.empty --for now
logicGraph :: LogicGraph
logicGraph = emptyLogicGraph
{ logics = Map.fromList $ map addLogicName $ logicList
++ concatMap (\ (Comorphism cid) ->
[Logic $ sourceLogic cid, Logic $ targetLogic cid])
comorphismList
, comorphisms = Map.fromList $ map addComorphismName comorphismList
, inclusions = addCompsN $ Map.fromList
$ map addInclusionNames inclusionList
, unions = Map.fromList $ map addUnionNames unionList
, morphisms = Map.fromList $ map addMorphismName morphismList
, modifications = Map.fromList $ map addModificationName modificationList
, squares = squareMap
, qTATranslations =
Map.fromList $ map (\x@(Comorphism c)-> (show (sourceLogic c), x))
qtaList}
lookupSquare :: AnyComorphism -> AnyComorphism -> LogicGraph -> Result [Square]
lookupSquare com1 com2 lg = maybe (fail "lookupSquare") return $ do
sqL1 <- Map.lookup (com1, com2) $ squares lg
sqL2 <- Map.lookup (com2, com1) $ squares lg
return $ nub $ sqL1 ++ (map mirrorSquare sqL2)
-- Here have to update to nub $ .. ++ ..
-- after i write equality for AnyModifications (equality for Squares nyi)
lookupSquare_in_LG :: AnyComorphism -> AnyComorphism -> Result [Square]
lookupSquare_in_LG com1 com2 = lookupSquare com1 com2 logicGraph
lookupComorphism_in_LG :: String -> Result AnyComorphism
lookupComorphism_in_LG coname = lookupComorphism coname logicGraph
-- translations to logics with quotient term algebra implemented
qtaList :: [AnyComorphism]
qtaList = [Comorphism Maude2CASL]
lookupQTA_in_LG :: String -> Result AnyComorphism
lookupQTA_in_LG coname =
let
qta = qTATranslations logicGraph
in if coname `elem` Map.keys qta then
return $ Map.findWithDefault (error "") coname qta
else fail "no translation found"