Cross Reference: /hets/CspCASL/Logic_CspCASL.hs
Logic_CspCASL.hs revision f08f7774e4c47012f3c349205310750198cdc434
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
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder{- |
ca010363454de207082dfaa4b753531ce2a34551Christian MaederModule : $Id$
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederDescription : CspCASL instance of type class logic
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederCopyright : (c) Markus Roggenbach, Till Mossakowski and Uni Bremen 2003
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : M.Roggenbach@swansea.ac.uk
ca010363454de207082dfaa4b753531ce2a34551Christian MaederStability : experimental
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederPortability : non-portable(import Logic.Logic)
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder
79d11c2e3ad242ebb241f5d4a5e98a674c0b986fChristian MaederHere is the place where the class Logic is instantiated for CspCASL.
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder Also the instances for Syntax an Category.
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder-}
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder{-
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder todo:
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder - writing real functions
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder - Modul Sign.hs mit CSP-CASL-Signaturen und Morphismen, basiernd
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder auf CASL.Sign
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder CSP-CASL-Signatur = (CASL-Sig,Menge von Kanalnamen)
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder CSP-CASL-Morphismus = (CASL-Morphismus, Kanalnamenabbildung)
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder oder nur CASL-Morphismus
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder SYMB_ITEMS SYMB_MAP_ITEMS: erstmal von CASL (d.h. nur CASL-Morphismus)
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder - instance Sentences
23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maeder S�tze = entweder CASL-S�tze oder CSP-CASL-S�tze
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder Rest soweit wie m�glich von CASL �bernehmen
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder - statische Analyse (gem�� Typ in Logic.Logic) schreiben
e68f45f355ed9d4026ee9baff5aa75aa7c911cc2Christian Maeder und unten f�r basic_analysis einh�ngen
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder K�r:
83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maeder - Teillogiken (instance SemiLatticeWithTop ...)
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder
028f19cdb09d52bb2fd207399b6fa874540d1670Christian Maeder-}
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder
53301de22afd7190981b363b57c48df86fcb50f7Christian Maedermodule CspCASL.Logic_CspCASL(CspCASL(CspCASL)) where
83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maeder
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport Logic.Logic
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport CASL.AS_Basic_CASL
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport CASL.Logic_CASL
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport CASL.Morphism
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maederimport CASL.Sign
83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maederimport CASL.SymbolParser
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport CASL.SymbolMapAnalysis
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder
53301de22afd7190981b363b57c48df86fcb50f7Christian Maederimport qualified Data.Set as Set
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder--import CspCASL.AS_CspCASL
53301de22afd7190981b363b57c48df86fcb50f7Christian Maederimport qualified CspCASL.AS_CspCASL as AS_CspCASL
53301de22afd7190981b363b57c48df86fcb50f7Christian Maederimport qualified CspCASL.ATC_CspCASL()
da2b959c50c95309d8eb8b24174249c2847e74b5Christian Maederimport qualified CspCASL.CspCASL_Keywords as CspCASL_Keywords
da2b959c50c95309d8eb8b24174249c2847e74b5Christian Maederimport qualified CspCASL.Morphism as CspCASL_Morphism
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maederimport qualified CspCASL.Parse_CspCASL as Parse_CspCASL
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport qualified CspCASL.Print_CspCASL ()
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport qualified CspCASL.SignCSP as SignCSP
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maederimport qualified CspCASL.StatAnaCSP as StatAnaCSP
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder-- | Lid for CspCASL
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederdata CspCASL = CspCASL deriving (Show)
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederinstance Language CspCASL
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder where
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder description _ =
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder "CspCASL - see\n\n"++
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder "http://www.cs.swan.ac.uk/~csmarkus/ProcessesAndData/"
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maederinstance SignExtension SignCSP.CspSign where
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder isSubSignExtension = SignCSP.isInclusion
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder-- | Instance for CspCASL morphism extension (used for Category)
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederinstance MorphismExtension SignCSP.CspSign SignCSP.CspAddMorphism where
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder ideMorphismExtension _ = SignCSP.emptyCspAddMorphism
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder composeMorphismExtension = SignCSP.composeCspAddMorphism
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder inverseMorphismExtension = SignCSP.inverseCspAddMorphism
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder isInclusionMorphismExtension _ = True -- missing!
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder
da2b959c50c95309d8eb8b24174249c2847e74b5Christian Maeder-- | Instance of Sentences for CspCASL (missing)
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maederinstance Sentences CspCASL
da2b959c50c95309d8eb8b24174249c2847e74b5Christian Maeder SignCSP.CspCASLSen -- sentence (missing)
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder SignCSP.CspCASLSign -- signature
da2b959c50c95309d8eb8b24174249c2847e74b5Christian Maeder SignCSP.CspMorphism -- morphism
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder Symbol -- symbol
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder where
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder parse_sentence CspCASL = Nothing
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder map_sen CspCASL mor sen =
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder if isInclusionMorphism isInclusionMorphismExtension mor
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder then return sen
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder else fail "renaming in map_sen CspCASL not implemented"
d48085f765fca838c1d972d2123601997174583dChristian Maeder sym_of CspCASL = CspCASL_Morphism.symOf
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder symmap_of CspCASL = morphismToSymbMap
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder-- | Syntax of CspCASL
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maederinstance Syntax CspCASL
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder AS_CspCASL.CspBasicSpec -- basic_spec
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder SYMB_ITEMS -- symb_items
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder SYMB_MAP_ITEMS -- symb_map_items
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder where
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder parse_basic_spec CspCASL =
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder Just Parse_CspCASL.cspBasicSpec
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder parse_symb_items CspCASL =
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder Just $ symbItems CspCASL_Keywords.csp_casl_keywords
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder parse_symb_map_items CspCASL =
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder Just $ symbMapItems CspCASL_Keywords.csp_casl_keywords
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder-- lattices (for sublogics) missing
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder-- | Instance of Logic for CspCASL
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maederinstance Logic CspCASL
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder () -- Sublogics (missing)
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder AS_CspCASL.CspBasicSpec -- basic_spec
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder SignCSP.CspCASLSen -- sentence (missing)
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder SYMB_ITEMS -- symb_items
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder SYMB_MAP_ITEMS -- symb_map_items
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder SignCSP.CspCASLSign -- signature
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder SignCSP.CspMorphism -- morphism
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder Symbol
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder RawSymbol
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder () -- proof_tree (missing)
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder where
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder stability CspCASL = Experimental
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder data_logic CspCASL = Just (Logic CASL)
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder empty_proof_tree _ = ()
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder-- | Static Analysis for CspCASL
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maederinstance StaticAnalysis CspCASL
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder AS_CspCASL.CspBasicSpec -- basic_spec
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder SignCSP.CspCASLSen -- sentence (missing)
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder SYMB_ITEMS -- symb_items
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder SYMB_MAP_ITEMS -- symb_map_items
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder SignCSP.CspCASLSign -- signature
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder SignCSP.CspMorphism -- morphism
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder Symbol
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder RawSymbol
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder where
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder basic_analysis CspCASL =
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder Just StatAnaCSP.basicAnalysisCspCASL
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder stat_symb_map_items CspCASL = error "Logic_CspCASL.hs"
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder stat_symb_items CspCASL = error "Logic_CspCASL.hs"
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder empty_signature CspCASL = SignCSP.emptyCspCASLSign
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder inclusion CspCASL =
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder sigInclusion SignCSP.emptyCspAddMorphism
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder SignCSP.isInclusion const -- this is still wrong
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder signature_union CspCASL s =
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder return . addSig SignCSP.addCspProcSig s
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder induced_from_morphism CspCASL = inducedFromMorphism
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder SignCSP.emptyCspAddMorphism
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder SignCSP.isInclusion
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder induced_from_to_morphism CspCASL = inducedFromToMorphism
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder SignCSP.emptyCspAddMorphism
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder SignCSP.isInclusion
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder SignCSP.diffCspProcSig
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder