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
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
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : M.Roggenbach@swansea.ac.uk
ca010363454de207082dfaa4b753531ce2a34551Christian MaederStability : experimental
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederPortability : non-portable(import Logic.Logic)
79d11c2e3ad242ebb241f5d4a5e98a674c0b986fChristian MaederHere is the place where the class Logic is instantiated for CspCASL.
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder Also the instances for Syntax an Category.
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder - writing real functions
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder - Modul Sign.hs mit CSP-CASL-Signaturen und Morphismen, basiernd
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
83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maeder - Teillogiken (instance SemiLatticeWithTop ...)
53301de22afd7190981b363b57c48df86fcb50f7Christian Maedermodule CspCASL.Logic_CspCASL(CspCASL(CspCASL)) where
53301de22afd7190981b363b57c48df86fcb50f7Christian Maederimport qualified Data.Set as Set
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-- | Lid for CspCASL
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederdata CspCASL = CspCASL deriving (Show)
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederinstance Language CspCASL
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder description _ =
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder "CspCASL - see\n\n"++
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder "http://www.cs.swan.ac.uk/~csmarkus/ProcessesAndData/"
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maederinstance SignExtension SignCSP.CspSign where
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder isSubSignExtension = SignCSP.isInclusion
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!
da2b959c50c95309d8eb8b24174249c2847e74b5Christian Maeder-- | Instance of Sentences for CspCASL (missing)
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maederinstance Sentences CspCASL
da2b959c50c95309d8eb8b24174249c2847e74b5Christian Maeder SignCSP.CspCASLSen -- sentence (missing)
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder Symbol -- symbol
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"
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder symmap_of CspCASL = morphismToSymbMap
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder-- | Syntax of CspCASL
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maederinstance Syntax CspCASL
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder SYMB_ITEMS -- symb_items
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder SYMB_MAP_ITEMS -- symb_map_items
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder parse_basic_spec CspCASL =
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-- lattices (for sublogics) missing
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder-- | Instance of Logic for CspCASL
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maederinstance Logic CspCASL
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder () -- Sublogics (missing)
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder SignCSP.CspCASLSen -- sentence (missing)
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder SYMB_ITEMS -- symb_items
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder SYMB_MAP_ITEMS -- symb_map_items
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder () -- proof_tree (missing)
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder stability CspCASL = Experimental
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder data_logic CspCASL = Just (Logic CASL)
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder empty_proof_tree _ = ()
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder-- | Static Analysis for CspCASL
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maederinstance StaticAnalysis CspCASL
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder SignCSP.CspCASLSen -- sentence (missing)
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder SYMB_ITEMS -- symb_items
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder SYMB_MAP_ITEMS -- symb_map_items
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder basic_analysis CspCASL =
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 =
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder SignCSP.isInclusion const -- this is still wrong
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder signature_union CspCASL s =
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder induced_from_morphism CspCASL = inducedFromMorphism
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder induced_from_to_morphism CspCASL = inducedFromToMorphism