Cross Reference: /hets/Comorphisms/LogicList.hs
LogicList.hs revision 36b9e4cf34070e81d93765f129044abc5dbcf678
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
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder{-# LANGUAGE CPP #-}
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder{- |
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederModule : $Header$
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederDescription : Assembles all the logics into a list, as a prerequisite
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder for the logic graph
ca010363454de207082dfaa4b753531ce2a34551Christian MaederCopyright : (c) Till Mossakowski and Uni Bremen 2003
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederMaintainer : till@informatik.uni-bremen.de
ca010363454de207082dfaa4b753531ce2a34551Christian MaederStability : provisional
79d11c2e3ad242ebb241f5d4a5e98a674c0b986fChristian MaederPortability : non-portable (existential types)
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder
ca010363454de207082dfaa4b753531ce2a34551Christian MaederAssembles all the logics into a list, as a prerequisite for the logic graph.
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder The modules for the Grothendieck logic are logic graph indepdenent,
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder and here is the logic graph that is used to instantiate these.
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder Since the logic graph depends on a large number of modules for the
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder individual logics, this separation of concerns (and possibility for
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder separate compilation) is quite useful.
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder References:
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder J. A. Goguen, R. M. Burstall: Institutions:
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder Abstract Model Theory for Specification and Programming,
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder Journal of the Association for Computing Machinery 39, p. 95-146.
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder J. Meseguer: General logics. Logic Colloquium 87, p. 275-329, North Holland.
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder Todo:
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder Add many many logics.
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder-}
23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maeder
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maedermodule Comorphisms.LogicList
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder ( logicList
e68f45f355ed9d4026ee9baff5aa75aa7c911cc2Christian Maeder , addLogicName
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder , defaultLogic
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder , preLogicGraph
83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maeder ) where
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder
028f19cdb09d52bb2fd207399b6fa874540d1670Christian Maederimport qualified Data.Map as Map
975642b989852fc24119c59cf40bc1af653608ffChristian Maederimport Logic.Logic
53301de22afd7190981b363b57c48df86fcb50f7Christian Maederimport Logic.Grothendieck
83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maederimport CASL.Logic_CASL -- also serves as default logic
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport HasCASL.Logic_HasCASL
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport Propositional.Logic_Propositional
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport QBF.Logic_QBF
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder#ifdef PROGRAMATICA
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maederimport Haskell.Logic_Haskell
83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maeder#endif
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport Isabelle.Logic_Isabelle
53301de22afd7190981b363b57c48df86fcb50f7Christian Maederimport SoftFOL.Logic_SoftFOL
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder#ifdef CASLEXTENSIONS
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maederimport Modal.Logic_Modal
53301de22afd7190981b363b57c48df86fcb50f7Christian Maederimport ExtModal.Logic_ExtModal
53301de22afd7190981b363b57c48df86fcb50f7Christian Maederimport CoCASL.Logic_CoCASL
0a39036fa485579a7b7c81cdd44a412392571927Christian Maederimport CspCASL.Logic_CspCASL
da2b959c50c95309d8eb8b24174249c2847e74b5Christian Maederimport COL.Logic_COL ()
0a39036fa485579a7b7c81cdd44a412392571927Christian Maederimport CASL_DL.Logic_CASL_DL
0a39036fa485579a7b7c81cdd44a412392571927Christian Maederimport ConstraintCASL.Logic_ConstraintCASL
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport VSE.Logic_VSE
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder-- no CASL extension, but omit them as non-essential
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maederimport RelationalScheme.Logic_Rel
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maederimport Temporal.Logic_Temporal
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maederimport DFOL.Logic_DFOL
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maederimport LF.Logic_LF
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maederimport Framework.Logic_Framework
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder--import OMDoc.Logic_OMDoc ()
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport Maude.Logic_Maude
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maederimport Reduce.Logic_Reduce
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maederimport CommonLogic.Logic_CommonLogic
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder#endif
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder#ifndef NOOWLLOGIC
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maederimport DMU.Logic_DMU
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maederimport OWL.Logic_OWL
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder#endif
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian MaederlogicList :: [AnyLogic]
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian MaederlogicList =
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder [ Logic CASL
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder , Logic HasCASL
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder , Logic Isabelle
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder , Logic SoftFOL
c2c1ca07d7f3c2228b66599a7fb37b90fe6fb3bcChristian Maeder , Logic Propositional
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder , Logic QBF
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder#ifdef PROGRAMATICA
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder , Logic Haskell
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder#endif
c2c1ca07d7f3c2228b66599a7fb37b90fe6fb3bcChristian Maeder#ifdef CASLEXTENSIONS
c2c1ca07d7f3c2228b66599a7fb37b90fe6fb3bcChristian Maeder , Logic CoCASL
c2c1ca07d7f3c2228b66599a7fb37b90fe6fb3bcChristian Maeder , Logic ExtModal
c2c1ca07d7f3c2228b66599a7fb37b90fe6fb3bcChristian Maeder , Logic Modal
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder , Logic cspCASL
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder , Logic traceCspCASL
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder , Logic failureCspCASL
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder , Logic CASL_DL
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder , Logic ConstraintCASL
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder , Logic VSE
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder , Logic RelScheme
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder , Logic Temporal
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder , Logic DFOL
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder , Logic LF
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder , Logic Framework
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder , Logic Maude
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder , Logic Reduce
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder , Logic CommonLogic
da2b959c50c95309d8eb8b24174249c2847e74b5Christian Maeder#endif
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder#ifndef NOOWLLOGIC
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder , Logic DMU
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder , Logic OWL
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder#endif
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder ]
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederaddLogicName :: AnyLogic -> (String,AnyLogic)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederaddLogicName l@(Logic lid) = (language_name lid, l)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederdefaultLogic :: AnyLogic
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederdefaultLogic = Logic CASL
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederpreLogicGraph :: LogicGraph
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederpreLogicGraph =
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder emptyLogicGraph { logics = Map.fromList $ map addLogicName logicList }
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder