LogicGraph.hs revision ebe4d5a8e51f6009d6e7ca465f5963ce46a07fd2
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder{-# OPTIONS -cpp #-}
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederModule : $Header$
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederDescription : the logic graph
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Till Mossakowski and Uni Bremen 2003
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederMaintainer : till@informatik.uni-bremen.de
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederStability : unstable
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederPortability : non-portable
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederAssembles all the logics and comorphisms into a graph.
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder The modules for the Grothendieck logic are logic graph indepdenent,
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder and here is the logic graph that is used to instantiate these.
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder Since the logic graph depends on a large number of modules for the
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder individual logics, this separation of concerns (and possibility for
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder separate compilation) is quite useful.
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder Comorphisms are either logic inclusions, or normal comorphisms.
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder The former are assembled in inclusionList, the latter in normalList.
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder An inclusion is an institution comorphism with the following properties:
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder * the signature translation is an embedding of categories
4cb77926a2d85ce3bb32ac0938f0100c8c528dc2Till Mossakowski * the sentence translations are injective
4cb77926a2d85ce3bb32ac0938f0100c8c528dc2Till Mossakowski * the model translations are isomorphisms
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder The FLIRTS home page: <http://www.informatik.uni-bremen.de/flirts>
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder T. Mossakowski:
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder Relating CASL with Other Specification Languages:
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder the Institution Level
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder Theoretical Computer Science 286, p. 367-475, 2002.
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder , lookupComorphism_in_LG
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder , comorphismList
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder , lookupSquare_in_LG
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maederimport Comorphisms.PCoClTyConsHOL2IsabelleHOL
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder#ifdef CASLEXTENSIONS
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder#ifdef PROGRAMATICA
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maederimport qualified Data.Map as Map
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder-- This needs to be seperated for utils/InlineAxioms/InlineAxioms.hs
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederaddComorphismName :: AnyComorphism -> (String, AnyComorphism)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederaddComorphismName c@(Comorphism cid) = (language_name cid, c)
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian MaederaddInclusionNames :: AnyComorphism -> ((String, String), AnyComorphism)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederaddInclusionNames c@(Comorphism cid) =
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder ((language_name $ sourceLogic cid, language_name $ targetLogic cid), c)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederaddUnionNames :: (AnyComorphism, AnyComorphism)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder -> ((String, String), (AnyComorphism, AnyComorphism))
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederaddUnionNames (c1@(Comorphism cid1), c2@(Comorphism cid2)) =
e220b2051a2342a9291721e6c7f408860bed01b7Jorina Freya Gerken ( (language_name $ sourceLogic cid1, language_name $ sourceLogic cid2)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederaddMorphismName :: AnyMorphism -> (String, AnyMorphism)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederaddMorphismName m@(Morphism cid) = (language_name cid, m)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederaddModificationName :: AnyModification -> (String,AnyModification)
e220b2051a2342a9291721e6c7f408860bed01b7Jorina Freya GerkenaddModificationName m@(Modification cid) = (language_name cid, m)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaedernormalList :: [AnyComorphism]
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder [ Comorphism CASL2HasCASL
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder , Comorphism CFOL2IsabelleHOL
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder , Comorphism Prop2CASL
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder#ifdef CASLEXTENSIONS
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder , Comorphism CASL2Modal
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder , Comorphism Modal2CASL
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder , Comorphism CASL2CoCASL
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder , Comorphism CASL2CspCASL
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder , Comorphism CspCASL2Modal
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder , Comorphism CASL_DL2CASL
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder , Comorphism CoCASL2CoPCFOL
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder , Comorphism CoCASL2CoSubCFOL
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder , Comorphism CoCFOL2IsabelleHOL
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder , Comorphism OWL2CASL_DL
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder , Comorphism DL2CASL_DL
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder#ifdef PROGRAMATICA
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder , Comorphism HasCASL2Haskell
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder , Comorphism Haskell2IsabelleHOLCF
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder , Comorphism Haskell2IsabelleHOL
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder , Comorphism PCoClTyConsHOL2IsabelleHOL
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder , Comorphism HasCASL2IsabelleHOL
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder , Comorphism SuleCFOL2SoftFOLInduction
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder , Comorphism HasCASL2PCoClTyConsHOL
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder , Comorphism HasCASL2HasCASL
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder , Comorphism SuleCFOL2SoftFOL
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder , Comorphism CASL2PCFOL
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder , Comorphism $ CASL2SubCFOL True FormulaDependent -- unique bottoms
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder , Comorphism $ CASL2SubCFOL False SubsortBottoms -- keep free types
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder , Comorphism $ CASL2SubCFOL False NoMembershipOrCast -- keep free types
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder , Comorphism CASL2TopSort ]
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaedercomorphismList :: [AnyComorphism]
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaedercomorphismList = Map.elems $ comorphisms logicGraph
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederinclusionList :: [AnyComorphism]
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederinclusionList =
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder filter (\ (Comorphism cid) -> isInclusionComorphism cid) normalList
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder{- | Unions of logics, represented as pairs of inclusions.
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder Entries only necessary for non-trivial unions
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder (a trivial union is a union of a sublogic with a superlogic).
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederunionList :: [(AnyComorphism, AnyComorphism)]
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederunionList = []
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaedermorphismList :: [AnyMorphism]
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaedermorphismList = [] -- for now
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaedermodificationList :: [AnyModification]
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaedermodificationList = [Modification MODAL_EMBEDDING]
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaedersquareMap :: Map.Map (AnyComorphism, AnyComorphism) [Square]
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaedersquareMap = Map.empty --for now
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian MaederlogicGraph :: LogicGraph
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian MaederlogicGraph = emptyLogicGraph
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder { logics = Map.fromList $ map addLogicName $ logicList
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder ++ concatMap (\ (Comorphism cid) ->
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder [Logic $ sourceLogic cid, Logic $ targetLogic cid])
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder , comorphisms = Map.fromList $ map addComorphismName normalList
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder , inclusions = Map.fromList $ map addInclusionNames inclusionList
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder , unions = Map.fromList $ map addUnionNames unionList
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder , morphisms = Map.fromList $ map addMorphismName morphismList
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder , modifications = Map.fromList $ map addModificationName modificationList
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder , squares = squareMap }
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian MaederlookupSquare :: AnyComorphism -> AnyComorphism -> LogicGraph -> Result [Square]
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian MaederlookupSquare com1 com2 lg = do
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder sqL1 <- Map.lookup (com1, com2) $ squares lg
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder sqL2 <- Map.lookup (com2, com1) $ squares lg
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder return $ sqL1 ++ (map mirrorSquare sqL2)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder -- Here have to update to nub $ .. ++ ..
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder -- after i write equality for AnyModifications (equality for Squares nyi)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederlookupSquare_in_LG :: AnyComorphism -> AnyComorphism -> Result [Square]
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederlookupSquare_in_LG com1 com2 = lookupSquare com1 com2 logicGraph
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederlookupComorphism_in_LG :: String -> Result AnyComorphism
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederlookupComorphism_in_LG coname = lookupComorphism coname logicGraph