CspProver_Consts.hs revision 3d3889e0cefcdce9b3f43c53aaa201943ac2e895
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
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillyDescription : Isabelle Abstract syntax constants for CSP-Prover operations
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillyCopyright : (c) Andy Gimblett, Liam O'Reilly and Markus Roggenbach,
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly Swansea University 2008
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillyMaintainer : csliam@swansea.ac.uk
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillyStability : provisional
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillyPortability : portable
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillyIsabelle Abstract syntax constants for CSP-Prover operations.
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly cspProver_skipOp,
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly cspProver_stopOp,
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly cspProver_divOp,
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly cspProver_runOp,
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly cspProver_chaosOp,
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly cspProver_action_prefixOp,
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly cspProver_external_prefix_choiceOp,
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly cspProver_internal_prefix_choiceOp,
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly cspProver_sequenceOp,
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly cspProver_external_choiceOp,
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly cspProver_internal_choiceOp,
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly cspProver_interleavingOp,
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly cspProver_synchronousOp,
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly cspProver_general_parallelOp,
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly cspProver_alphabetised_parallelOp,
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly cspProver_hidingOp,
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly cspProver_renamingOp,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder cspProver_conditionalOp,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder cspProver_chan_nondeterministic_sendOp
059e541d741fa3faa3a2e4cf81fc7627a87ce3b7Liam O'Reillyimport Isabelle.IsaSign as IsaSign
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reillyimport Isabelle.IsaConsts (binVNameAppl, con, termAppl)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- Symbols for CspProver
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederThese symbols and priorities have come from the CSP-Prover source code -}
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- SKIP primitive process symbol
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_skipS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_skipS = "SKIP"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- STOP primitive process symbol
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_stopS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_stopS = "STOP"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- DIV primitive process symbol
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_divS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_divS = "DIV"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- RUN primitive process symbol
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_runS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_runS = "??? RUN ??? - NOT YET DONE"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- CHAOS primitive process symbol
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_chaosS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_chaosS = "??? CHAOS ??? - NOT YET DONE"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- Action prefix operator symbols
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_action_prefixS :: String
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillycspProver_action_prefixS = "Act_prefix"
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_action_prefixAltS :: String
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_action_prefixAltS = "(_ -> _)"
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_action_prefixAltArgPrios :: [Int]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspProver_action_prefixAltArgPrios = [150, 80]
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_action_prefixAltOpPrio :: Int
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_action_prefixAltOpPrio = 80
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- External prefix choice operator symbols
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_external_prefix_choiceS :: String
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillycspProver_external_prefix_choiceS = "Ext_pre_choice"
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_external_prefix_choiceAltS :: String
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_external_prefix_choiceAltS = "(? _:_ -> _)"
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_external_prefix_choiceAltArgPrios :: [Int]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspProver_external_prefix_choiceAltArgPrios = [900, 900, 80]
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_external_prefix_choiceAltOpPrio :: Int
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_external_prefix_choiceAltOpPrio = 80
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- Internal prefix choice operator symbols
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_internal_prefix_choiceS :: String
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillycspProver_internal_prefix_choiceS = "Int_pre_choice"
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_internal_prefix_choiceAltS :: String
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_internal_prefix_choiceAltS = "(! _:_ -> _)"
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_internal_prefix_choiceAltArgPrios :: [Int]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspProver_internal_prefix_choiceAltArgPrios = [900, 900, 80]
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_internal_prefix_choiceAltOpPrio :: Int
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_internal_prefix_choiceAltOpPrio = 80
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- Sequence combinator operator symbols
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_sequenceS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_sequenceS = "Seq_compo"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_sequenceAltS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_sequenceAltS = "(_ ;; _)"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_sequenceAltArgPrios :: [Int]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspProver_sequenceAltArgPrios = [79, 78]
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_sequenceAltOpPrio :: Int
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_sequenceAltOpPrio = 78
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- External choice operator symbols
059e541d741fa3faa3a2e4cf81fc7627a87ce3b7Liam O'ReillycspProver_external_choiceS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_external_choiceS = "Ext_choice"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_external_choiceAltS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_external_choiceAltS = "( _ [+] _)"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_external_choiceAltArgPrios :: [Int]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspProver_external_choiceAltArgPrios = [72, 73]
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_external_choiceAltOpPrio :: Int
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_external_choiceAltOpPrio = 72
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- Internal choice operator symbols
059e541d741fa3faa3a2e4cf81fc7627a87ce3b7Liam O'ReillycspProver_internal_choiceS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_internal_choiceS = "Int_choice"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_internal_choiceAltS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_internal_choiceAltS = "(_ |~| _)"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_internal_choiceAltArgPrios :: [Int]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspProver_internal_choiceAltArgPrios = [64, 65]
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_internal_choiceAltOpPrio :: Int
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_internal_choiceAltOpPrio = 64
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- Interleaving parallel operator symbols
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_interleavingS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_interleavingS = "Interleave"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_interleavingAltS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_interleavingAltS = "(_ ||| _)"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_interleavingAltArgPrios :: [Int]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspProver_interleavingAltArgPrios = [76, 77]
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_interleavingAltOpPrio :: Int
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_interleavingAltOpPrio = 76
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- Synchronous parallel operator symbols
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_synchronousS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_synchronousS = "Synchro"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_synchronousAltS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_synchronousAltS = "(_ || _)"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_synchronousAltArgPrios :: [Int]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspProver_synchronousAltArgPrios = [76, 77]
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_synchronousAltOpPrio :: Int
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_synchronousAltOpPrio = 76
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- Generalised parallel operator symbols
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_general_parallelS :: String
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspProver_general_parallelS = "Parallel"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_general_parallelAltS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_general_parallelAltS = "(_ |[_]| _)"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_general_parallelAltArgPrios :: [Int]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspProver_general_parallelAltArgPrios = [76, 0, 77]
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_general_parallelAltOpPrio :: Int
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_general_parallelAltOpPrio = 76
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- Alphabetised parallel operator symbols
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_alphabetised_parallelS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_alphabetised_parallelS = "Alpha_parallel"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_alphabetised_parallelAltS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_alphabetised_parallelAltS = "(_ |[_,_]| _)"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_alphabetised_parallelAltArgPrios :: [Int]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspProver_alphabetised_parallelAltArgPrios = [76, 0, 0, 77]
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_alphabetised_parallelAltOpPrio :: Int
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_alphabetised_parallelAltOpPrio = 76
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- Hiding operator symbols
059e541d741fa3faa3a2e4cf81fc7627a87ce3b7Liam O'ReillycspProver_hidingS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_hidingS = "Hiding"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_hidingAltS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_hidingAltS = "(_ -- _)"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_hidingAltArgPrios :: [Int]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspProver_hidingAltArgPrios = [84, 85]
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_hidingAltOpPrio :: Int
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_hidingAltOpPrio = 85
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- Renaming operator symbols
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_renamingS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_renamingS = "Renaming"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_renamingAltS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_renamingAltS = "(_ [[_]])"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_renamingAltArgPrios :: [Int]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspProver_renamingAltArgPrios = [84, 0]
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_renamingAltOpPrio :: Int
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_renamingAltOpPrio = 84
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- Conditional operator symbols
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_conditionalS :: String
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'ReillycspProver_conditionalS = "IF"
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_conditionalAltS :: String
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'ReillycspProver_conditionalAltS = "(IF _ THEN _ ELSE _)"
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_conditionalAltArgPrios :: [Int]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspProver_conditionalAltArgPrios = [900, 88, 88]
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_conditionalAltArgOpPrio :: Int
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_conditionalAltArgOpPrio = 88
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- Channel Non-deterministic send operator symbols
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederOnly works if pretty printed using the alternative syntax -}
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillycspProver_chan_nondeterministic_sendS :: String
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillycspProver_chan_nondeterministic_sendS = "Nondet_send_prefix"
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillycspProver_chan_nondeterministic_sendAltS :: String
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillycspProver_chan_nondeterministic_sendAltS = "(_ !? _:_ -> _)"
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillycspProver_chan_nondeterministic_sendAltArgPrios :: [Int]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspProver_chan_nondeterministic_sendAltArgPrios = [900, 900, 1000, 80]
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillycspProver_chan_nondeterministic_sendAltArgOpPrio :: Int
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillycspProver_chan_nondeterministic_sendAltArgOpPrio = 80
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- Isabelle Terms representing the operations for CspProver
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | SKIP primitive process operator
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_skipOp :: Term
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_skipOp = makeCspProverOpNoAlt cspProver_skipS
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | STOP primitive process operator
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_stopOp :: Term
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_stopOp = makeCspProverOpNoAlt cspProver_stopS
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | DIV primitive process operator
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_divOp :: Term
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_divOp = makeCspProverOpNoAlt cspProver_divS
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | RUN primitive process operator
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_runOp :: Term
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_runOp = makeCspProverOpNoAlt cspProver_runS
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | CHAOS primitive process operator
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_chaosOp :: Term
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_chaosOp = makeCspProverOpNoAlt cspProver_chaosS
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | Action prefix operator
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_action_prefixOp :: Term -> Term -> Term
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_action_prefixOp =
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly makeBinCspProverOp cspProver_action_prefixS
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly cspProver_action_prefixAltS
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly cspProver_action_prefixAltArgPrios
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly cspProver_action_prefixAltOpPrio
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | External prefix choice operator
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_external_prefix_choiceOp :: Term -> Term -> Term -> Term
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_external_prefix_choiceOp =
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly makeTriCspProverOp cspProver_external_prefix_choiceS
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly cspProver_external_prefix_choiceAltS
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly cspProver_external_prefix_choiceAltArgPrios
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly cspProver_external_prefix_choiceAltOpPrio
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | Internal prefix choice operator
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_internal_prefix_choiceOp :: Term -> Term -> Term -> Term
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_internal_prefix_choiceOp =
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly makeTriCspProverOp cspProver_internal_prefix_choiceS
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly cspProver_internal_prefix_choiceAltS
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly cspProver_internal_prefix_choiceAltArgPrios
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly cspProver_internal_prefix_choiceAltOpPrio
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | Sequence combinator operator
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillycspProver_sequenceOp :: Term -> Term -> Term
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_sequenceOp =
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly makeBinCspProverOp cspProver_sequenceS
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_sequenceAltS
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_sequenceAltArgPrios
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_sequenceAltOpPrio
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | External choice operator
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillycspProver_external_choiceOp :: Term -> Term -> Term
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_external_choiceOp =
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly makeBinCspProverOp cspProver_external_choiceS
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_external_choiceAltS
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_external_choiceAltArgPrios
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_external_choiceAltOpPrio
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | Internal choice operator
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillycspProver_internal_choiceOp :: Term -> Term -> Term
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_internal_choiceOp =
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly makeBinCspProverOp cspProver_internal_choiceS
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_internal_choiceAltS
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_internal_choiceAltArgPrios
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_internal_choiceAltOpPrio
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | Interleaving parallel operator
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillycspProver_interleavingOp :: Term -> Term -> Term
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_interleavingOp =
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly makeBinCspProverOp cspProver_interleavingS
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_interleavingAltS
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_interleavingAltArgPrios
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_interleavingAltOpPrio
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | Synchronous parallel operator
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillycspProver_synchronousOp :: Term -> Term -> Term
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_synchronousOp =
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly makeBinCspProverOp cspProver_synchronousS
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_synchronousAltS
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_synchronousAltArgPrios
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_synchronousAltOpPrio
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | Generalised parallel operator
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillycspProver_general_parallelOp :: Term -> Term -> Term -> Term
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_general_parallelOp =
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly makeTriCspProverOp cspProver_general_parallelS
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_general_parallelAltS
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_general_parallelAltArgPrios
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_general_parallelAltOpPrio
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | Alphabetised parallel operator symbols
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillycspProver_alphabetised_parallelOp :: Term -> Term -> Term -> Term -> Term
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_alphabetised_parallelOp =
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly makeQuadCspProverOp cspProver_alphabetised_parallelS
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly cspProver_alphabetised_parallelAltS
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly cspProver_alphabetised_parallelAltArgPrios
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly cspProver_alphabetised_parallelAltOpPrio
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | Hiding operator
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillycspProver_hidingOp :: Term -> Term -> Term
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_hidingOp =
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly makeBinCspProverOp cspProver_hidingS
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_hidingAltS
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_hidingAltArgPrios
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_hidingAltOpPrio
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | Renaming operator
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillycspProver_renamingOp :: Term -> Term -> Term
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_renamingOp =
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly makeBinCspProverOp cspProver_renamingS
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_renamingAltS
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_renamingAltArgPrios
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_renamingAltOpPrio
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | Conditional operator
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_conditionalOp :: Term -> Term -> Term -> Term
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspProver_conditionalOp =
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly makeTriCspProverOp cspProver_conditionalS
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly cspProver_conditionalAltS
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly cspProver_conditionalAltArgPrios
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly cspProver_conditionalAltArgOpPrio
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- | Conditional operator
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillycspProver_chan_nondeterministic_sendOp :: Term -> Term -> Term -> Term
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspProver_chan_nondeterministic_sendOp =
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly makeQuadCspProverOp cspProver_chan_nondeterministic_sendS
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly cspProver_chan_nondeterministic_sendAltS
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly cspProver_chan_nondeterministic_sendAltArgPrios
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly cspProver_chan_nondeterministic_sendAltArgOpPrio
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- Create an Isabelle Term representing a (Unary) CspProver operator
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederwith no alternative syntax -}
902bfaac7e88afebb6684fe1f2414ae2efbc7edfChristian MaedermakeCspProverOpNoAlt :: String -> Term
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillymakeCspProverOpNoAlt opName =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder con $ VName opName Nothing
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- Create an Isabelle Term representing a CspProver operator with
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederalternative syntax -}
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillymakeBinCspProverOp :: String -> String -> [Int] -> Int -> Term -> Term -> Term
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillymakeBinCspProverOp opName altSyntax altArgPrios altOpPrio t1 t2 =
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly let vname = VName opName $ Just $ AltSyntax altSyntax altArgPrios altOpPrio
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly in binVNameAppl vname t1 t2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- Create an Isabelle Term representing a CspProver operator (with 3
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederparameters) with alternative syntax -}
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillymakeTriCspProverOp :: String -> String -> [Int] -> Int -> Term -> Term ->
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillymakeTriCspProverOp opName altSyntax altArgPrios altOpPrio t1 t2 t3 =
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly let vname = VName opName $ Just $ AltSyntax altSyntax altArgPrios altOpPrio
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly in termAppl (binVNameAppl vname t1 t2) t3
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- Create an Isabelle Term representing a CspProver operator (with 4
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederparameters) with alternative syntax -}
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillymakeQuadCspProverOp :: String -> String -> [Int] -> Int -> Term -> Term ->
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly Term -> Term -> Term
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillymakeQuadCspProverOp opName altSyntax altArgPrios altOpPrio t1 t2 t3 t4 =
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly let vname = VName opName $ Just $ AltSyntax altSyntax altArgPrios altOpPrio
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly in termAppl (termAppl (binVNameAppl vname t1 t2) t3) t4