LogicGraph.hs revision 342beb91d58bcf41178240c37d0f6c0c4f83c53e
66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder{-# LANGUAGE CPP #-}
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
66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederMaintainer : till@informatik.uni-bremen.de
66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederStability : unstable
fb69cd512eab767747f109e40322df7cae2f7bdfChristian MaederPortability : non-portable
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 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:
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder * the signature translation is an embedding of categories
da245da15da78363c896e44ea97a14ab1f83eb50Christian Maeder * the sentence translations are injective
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder * the model translations are isomorphisms
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder The FLIRTS home page: <http://www.informatik.uni-bremen.de/flirts>
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.
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , lookupComorphism_in_LG
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , comorphismList
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , inclusionList
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , lookupSquare_in_LG
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , lookupQTA_in_LG
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maederimport qualified Data.Map as Map
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederimport Comorphisms.PCoClTyConsHOL2IsabelleHOL
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederimport Comorphisms.MonadicHasCASLTranslation
fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maederimport Comorphisms.PCoClTyConsHOL2PairsInIsaHOL
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder#ifdef CASLEXTENSIONS
628310b42327ad76ce471caf0dde6563d6fa6307Christian Maeder#ifndef NOOWLLOGIC
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder#ifdef PROGRAMATICA
ffd01020a4f35f434b912844ad6e0d6918fadffdChristian Maeder-- This needs to be seperated for utils/InlineAxioms/InlineAxioms.hs
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian MaederaddComorphismName :: AnyComorphism -> (String, AnyComorphism)
715ffaf874309df081d1e1cd8e05073fc1227729Christian MaederaddComorphismName c@(Comorphism cid) = (language_name cid, c)
05e2a3161e4589a717c6fe5c7306820273a473c5Christian MaederaddInclusionNames :: AnyComorphism -> ((String, String), AnyComorphism)
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaederaddInclusionNames c@(Comorphism cid) =
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder ((language_name $ sourceLogic cid, language_name $ targetLogic cid), c)
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)
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaederaddMorphismName :: AnyMorphism -> (String, AnyMorphism)
fb69cd512eab767747f109e40322df7cae2f7bdfChristian MaederaddMorphismName m@(Morphism cid) = (language_name cid, m)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederaddModificationName :: AnyModification -> (String, AnyModification)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederaddModificationName m@(Modification cid) = (language_name cid, m)
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#ifndef NOOWLLOGIC
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder , Comorphism OWL2CASL
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder#ifdef PROGRAMATICA
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder , Comorphism HasCASL2Haskell
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder , Comorphism Haskell2IsabelleHOLCF
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder , Comorphism Haskell2IsabelleHOL
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
addComps :: Map.Map (String, String) AnyComorphism
-> Map.Map (String, String) AnyComorphism
addComps cm = Map.unions
Map.foldWithKey (\ (l3, l4) c2 m -> if l3 == l2 then
Just c3 -> Map.insert (l1, l4) c3 m
addCompsN :: Map.Map (String, String) AnyComorphism
-> Map.Map (String, String) AnyComorphism
squareMap :: Map.Map (AnyComorphism, AnyComorphism) [Square]
squareMap = Map.empty --for now
{ logics = Map.fromList $ map addLogicName $ logicList
, comorphisms = Map.fromList $ map addComorphismName comorphismList
, inclusions = addCompsN $ Map.fromList
, unions = Map.fromList $ map addUnionNames unionList
, morphisms = Map.fromList $ map addMorphismName morphismList
, modifications = Map.fromList $ map addModificationName modificationList
Map.fromList $ map (\x@(Comorphism c)-> (show (sourceLogic c), x))
sqL1 <- Map.lookup (com1, com2) $ squares lg
sqL2 <- Map.lookup (com2, com1) $ squares lg
in if coname `elem` Map.keys qta then
return $ Map.findWithDefault (error "") coname qta