Cross Reference: /hets/Comorphisms/LogicGraph.hs
LogicGraph.hs revision 0fefa32a0a32ce300e3a436457f19a04c1ca07f7
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
{-# LANGUAGE CPP #-}
{- |
Module : $Header$
Description : the logic graph
Copyright : (c) Till Mossakowski and Uni Bremen 2003
License : GPLv2 or higher, see LICENSE.txt
Maintainer : till@informatik.uni-bremen.de
Stability : unstable
Portability : non-portable
Assembles all the logics and comorphisms into a graph.
The modules for the Grothendieck logic are logic graph indepdenent,
and here is the logic graph that is used to instantiate these.
Since the logic graph depends on a large number of modules for the
individual logics, this separation of concerns (and possibility for
separate compilation) is quite useful.
Comorphisms are either logic inclusions, or normal comorphisms.
The former are assembled in inclusionList, the latter in normalList.
An inclusion is an institution comorphism with the following properties:
* the signature translation is an embedding of categories
* the sentence translations are injective
* the model translations are isomorphisms
References:
The FLIRTS home page: <http://www.informatik.uni-bremen.de/flirts>
T. Mossakowski:
Relating CASL with Other Specification Languages:
the Institution Level
Theoretical Computer Science 286, p. 367-475, 2002.
-}
module Comorphisms.LogicGraph
( logicGraph
, lookupComorphism_in_LG
, comorphismList
, inclusionList
, lookupSquare_in_LG
, lookupQTA_in_LG
) where
import qualified Data.Map as Map
import Common.Result
import Logic.Logic
import Logic.Grothendieck
import Logic.Comorphism
import Logic.Modification
import Logic.Morphism
import Modifications.ModalEmbedding
import Comorphisms.HasCASL2THF0
import Comorphisms.CASL2PCFOL
import Comorphisms.CASL2SubCFOL
import Comorphisms.CASL2HasCASL
import Comorphisms.HasCASL2HasCASL
import Comorphisms.CFOL2IsabelleHOL
import Comorphisms.HolLight2Isabelle
import Comorphisms.SuleCFOL2SoftFOL
import Comorphisms.Prop2CASL
import Comorphisms.CASL2Prop
import Comorphisms.HasCASL2IsabelleHOL
import Comorphisms.PCoClTyConsHOL2IsabelleHOL
import Comorphisms.MonadicHasCASLTranslation
import Comorphisms.PCoClTyConsHOL2PairsInIsaHOL
import Comorphisms.HasCASL2PCoClTyConsHOL
import Comorphisms.CASL2TopSort
import Comorphisms.DFOL2CASL
import Comorphisms.QBF2Prop
import Comorphisms.Prop2QBF
#ifdef CASLEXTENSIONS
import Comorphisms.CoCFOL2IsabelleHOL
import Comorphisms.CoCASL2CoPCFOL
import Comorphisms.CoCASL2CoSubCFOL
import Comorphisms.CASL2Modal
import Comorphisms.CASL2ExtModal
import Comorphisms.Modal2CASL
import Comorphisms.CASL2CoCASL
import Comorphisms.CASL2CspCASL
import Comorphisms.CspCASL2Modal
import CspCASL.Comorphisms
import Comorphisms.CASL_DL2CASL
import Comorphisms.RelScheme2CASL
import Comorphisms.CASL2VSE
import Comorphisms.CASL2VSERefine
import Comorphisms.CASL2VSEImport
import Comorphisms.Maude2CASL
import Comorphisms.CommonLogic2CASL
import Comorphisms.CommonLogic2CommonLogic
import Comorphisms.Prop2CommonLogic
import Comorphisms.SoftFOL2CommonLogic
import Comorphisms.Adl2CASL
#endif
#ifndef NOOWLLOGIC
import OWL2.DMU2OWL2
import OWL2.OWL22CASL
import OWL2.OWL22CommonLogic
#endif
#ifdef PROGRAMATICA
import Comorphisms.HasCASL2Haskell
import Comorphisms.Haskell2IsabelleHOLCF
#endif
-- This needs to be seperated for utils/InlineAxioms/InlineAxioms.hs
import Comorphisms.LogicList
addComorphismName :: AnyComorphism -> (String, AnyComorphism)
addComorphismName c@(Comorphism cid) = (language_name cid, c)
addInclusionNames :: AnyComorphism -> ((String, String), AnyComorphism)
addInclusionNames c@(Comorphism cid) =
((language_name $ sourceLogic cid, language_name $ targetLogic cid), c)
addUnionNames :: (AnyComorphism, AnyComorphism)
-> ((String, String), (AnyComorphism, AnyComorphism))
addUnionNames (c1@(Comorphism cid1), c2@(Comorphism cid2)) =
( (language_name $ sourceLogic cid1, language_name $ sourceLogic cid2)
, (c1, c2))
addMorphismName :: AnyMorphism -> (String, AnyMorphism)
addMorphismName m@(Morphism cid) = (language_name cid, m)
addModificationName :: AnyModification -> (String, AnyModification)
addModificationName m@(Modification cid) = (language_name cid, m)
comorphismList :: [AnyComorphism]
comorphismList =
[ Comorphism CASL2HasCASL
, Comorphism CFOL2IsabelleHOL
, Comorphism HolLight2Isabelle
, Comorphism Prop2CASL
, Comorphism CASL2Prop
, Comorphism DFOL2CASL
, Comorphism HasCASL2THF0
#ifdef CASLEXTENSIONS
, Comorphism CASL2Modal
, Comorphism CASL2ExtModal
, Comorphism Modal2CASL
, Comorphism CASL2CoCASL
, Comorphism CASL2CspCASL
, Comorphism CspCASL2Modal
, Comorphism cspCASLTrace
, Comorphism cspCASLFailure
, Comorphism CASL_DL2CASL
, Comorphism CoCASL2CoPCFOL
, Comorphism CoCASL2CoSubCFOL
, Comorphism CoCFOL2IsabelleHOL
, Comorphism RelScheme2CASL
, Comorphism CASL2VSE
, Comorphism CASL2VSEImport
, Comorphism CASL2VSERefine
, Comorphism Maude2CASL
, Comorphism CommonLogic2CASL
, Comorphism CommonLogic2CommonLogic
, Comorphism Prop2CommonLogic
, Comorphism SoftFOL2CommonLogic
, Comorphism Adl2CASL
#endif
#ifndef NOOWLLOGIC
, Comorphism OWL22CASL
, Comorphism OWL22CommonLogic
, Comorphism DMU2OWL2
#endif
#ifdef PROGRAMATICA
, Comorphism HasCASL2Haskell
, Comorphism Haskell2IsabelleHOLCF
, Comorphism Haskell2IsabelleHOL
#endif
, Comorphism PCoClTyConsHOL2IsabelleHOL
, Comorphism MonadicHasCASL2IsabelleHOL
, Comorphism PCoClTyConsHOL2PairsInIsaHOL
, Comorphism HasCASL2IsabelleHOL
, Comorphism suleCFOL2SoftFOLInduction
, Comorphism suleCFOL2SoftFOLInduction2
, Comorphism HasCASL2PCoClTyConsHOL
, Comorphism HasCASL2HasCASL
, Comorphism suleCFOL2SoftFOL
, Comorphism CASL2PCFOL
, Comorphism $ CASL2SubCFOL True FormulaDependent -- unique bottoms
, Comorphism $ CASL2SubCFOL False SubsortBottoms -- keep free types
, Comorphism $ CASL2SubCFOL False NoMembershipOrCast -- keep free types
, Comorphism CASL2TopSort
, Comorphism QBF2Prop
, Comorphism Prop2QBF ]
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_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 = [
#ifdef CASLEXTENSIONS
Comorphism Maude2CASL
#endif
]
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"