LogicGraph.hs revision 2b565fe5cfb9f99857fd25b52304758d8544e266
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach{-# OPTIONS -cpp #-}
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettModule : $Header$
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyCopyright : (c) Till Mossakowski and Uni Bremen 2003
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachMaintainer : till@tzi.de
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettStability : unstable
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachPortability : non-portable
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachAssembles all the logics and comorphisms into a graph.
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett The modules for the Grothendieck logic are logic graph indepdenent,
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett and here is the logic graph that is used to instantiate these.
78718c37b1a50086a27e0f031db4cf82bea934aeChristian Maeder Since the logic graph depends on a large number of modules for the
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach individual logics, this separation of concerns (and possibility for
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach separate compilation) is quite useful.
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach Comorphisms are either logic inclusions, or normal comorphisms.
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach The former are assembled in inclusionList, the latter in normalList.
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett An inclusion is an institution comorphism with the following properties:
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett * the signature translation is an embedding of categories
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett * the sentence translations are injective
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett * the model translations are isomorphisms
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach The FLIRTS home page: <http://www.tzi.de/flirts>
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder T. Mossakowski:
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett Relating CASL with Other Specification Languages:
c60c643bbac58809100f35f187493b6f170314f0Liam O'Reilly the Institution Level
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach Theoretical Computer Science 286, p. 367-475, 2002.
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett ( defaultLogic
1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblett , lookupComorphism_in_LG
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder , comorphismList
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reillyimport Logic.Prover (prover_sublogic)
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly#ifdef CASLEXTENSIONS
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett#ifdef PROGRAMATICA
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblettimport qualified Data.Map as Map
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettimport qualified Data.Set as Set
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettimport Data.Maybe (fromJust)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett-- This needs to be seperated for utils/InlineAxioms/InlineAxioms.hs
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettaddComorphismName :: AnyComorphism -> (String, AnyComorphism)
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy GimblettaddComorphismName c@(Comorphism cid) = (language_name cid, c)
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy GimblettaddInclusionNames :: AnyComorphism -> ((String, String), AnyComorphism)
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettaddInclusionNames c@(Comorphism cid) =
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett ((language_name $ sourceLogic cid, language_name $ targetLogic cid), c)
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyaddUnionNames :: (AnyComorphism, AnyComorphism)
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett -> ((String, String), (AnyComorphism, AnyComorphism))
31f039ffdb33d78cb31d24b71d3155b11a323975Andy GimblettaddUnionNames (c1@(Comorphism cid1), c2@(Comorphism cid2)) =
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett ( (language_name $ sourceLogic cid1, language_name $ sourceLogic cid2)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettaddMorphismName :: AnyMorphism -> (String, AnyMorphism)
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian MaederaddMorphismName m@(Morphism cid) = (language_name cid, m)
90047eafd2de482c67bcd13103c6064e9b0cb254Andy GimblettaddModificationName :: AnyModification -> (String,AnyModification)
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettaddModificationName m@(Modification cid) = (language_name cid, m)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettinclusionList :: [AnyComorphism]
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettinclusionList =
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett [ Comorphism CASL2HasCASL
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett , Comorphism CFOL2IsabelleHOL
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett , Comorphism Prop2CASL
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett#ifdef CASLEXTENSIONS
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett , Comorphism CASL2Modal
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly , Comorphism Modal2CASL
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly , Comorphism CASL2CoCASL
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly , Comorphism CASL2CspCASL
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly , Comorphism PCoClTyConsHOL2IsabelleHOL
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly , Comorphism HasCASL2IsabelleHOL
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettnormalList :: [AnyComorphism]
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett [ Comorphism SuleCFOL2SoftFOLInduction
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett , Comorphism HasCASL2HasCASL
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett , Comorphism SuleCFOL2SoftFOL
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett#ifdef CASLEXTENSIONS
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett , Comorphism CoCASL2CoPCFOL
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett , Comorphism CoCASL2CoSubCFOL
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach , Comorphism CoCFOL2IsabelleHOL
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett , Comorphism CspCASL2Modal -- not stable yet
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett#ifdef PROGRAMATICA
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett , Comorphism HasCASL2Haskell
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett , Comorphism Haskell2IsabelleHOLCF
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett , Comorphism Haskell2IsabelleHOL
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett , Comorphism CASL2PCFOL
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett , Comorphism CASL2SubCFOL
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett , Comorphism CASL2TopSort
31f039ffdb33d78cb31d24b71d3155b11a323975Andy GimblettcomorphismList :: [AnyComorphism]
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettcomorphismList = inclusionList ++ normalList
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett{- | Unions of logics, represented as pairs of inclusions.
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett Entries only necessary for non-trivial unions
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett (a trivial union is a union of a sublogic with a superlogic).
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettunionList :: [(AnyComorphism, AnyComorphism)]
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettunionList = []
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettmorphismList :: [AnyMorphism]
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettmorphismList = [] --for now
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillymodificationList :: [AnyModification]
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillymodificationList = [Modification MODAL_EMBEDDING]
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillylogicGraph :: LogicGraph
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillylogicGraph = LogicGraph
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett { logics = Map.fromList $ map addLogicName logicList
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly , comorphisms = Map.fromList $ map addComorphismName comorphismList
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly , inclusions = Map.fromList $ map addInclusionNames inclusionList
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly , unions = Map.fromList $ map addUnionNames unionList
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly , morphisms = Map.fromList $ map addMorphismName morphismList
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett , modifications = Map.fromList $ map addModificationName modificationList
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian MaederlookupComorphism_in_LG :: String -> Result AnyComorphism
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettlookupComorphism_in_LG coname = lookupComorphism coname logicGraph