Newer
Older
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
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
/*** generated by caesar.adt 5.2 with options -cc "" ***/
#define CAESAR_ADT 5.2
#include <stdio.h>
#include <signal.h>
#include <string.h>
#include <stdlib.h>
#ifndef CAESAR_ADT_ALLOC
#ifndef CAESAR_ADT_GARBAGE_COLLECTION
#define GC_malloc(CAESAR_ADT_0) malloc(CAESAR_ADT_0)
#else
extern char *GC_malloc ();
#endif
#define CAESAR_ADT_ALLOC(CAESAR_ADT_0,CAESAR_ADT_BODY,CAESAR_ADT_TYPE,CAESAR_ADT_LOTOS_OPERATION,CAESAR_ADT_C_FUNCTION) if (((CAESAR_ADT_0) = (CAESAR_ADT_TYPE) GC_malloc (sizeof (CAESAR_ADT_BODY))) == NULL) {printf ("#249 erreur dans le fichier ``.h'' :\n penurie de memoire pour les types abstraits\n dans l'operation %s\n implementee par la fonction %s [%s:%d]\n", CAESAR_ADT_LOTOS_OPERATION, CAESAR_ADT_C_FUNCTION, __FILE__, __LINE__); raise (15); }
#endif
#ifndef CAESAR_ADT_ERROR
#define CAESAR_ADT_ERROR(CAESAR_ADT_LOTOS_OPERATION,CAESAR_ADT_C_FUNCTION) if (1) {printf ("#250 erreur dans le fichier ``.h'' :\n cas imprevu (non defini par les equations)\n dans l'operation %s\n implementee par la fonction %s [%s:%d]\n", CAESAR_ADT_LOTOS_OPERATION, CAESAR_ADT_C_FUNCTION, __FILE__, __LINE__); raise (15); } else
#endif
/* LINTLIBRARY */
/* ========================================================================= */
#define CAESAR_ADT_UNCANONICAL_CAESAR_ADT_TYPE_QUEUE_NAT
#define CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT(CAESAR_ADT_0) (*(CAESAR_ADT_0))
#define CAESAR_ADT_SCALAR_CAESAR_ADT_TYPE_QUEUE_NAT
/* forward */ typedef struct CAESAR_ADT_STRUCT_CAESAR_ADT_TYPE_QUEUE_NAT CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_TYPE_QUEUE_NAT);
/* forward */ int CAESAR_ADT_CMP_QUEUE_NAT ();
/* forward */ void CAESAR_ADT_PRT_QUEUE_NAT ();
/* ========================================================================= */
typedef unsigned char ADT_BOOL;
#define CAESAR_ADT_SCALAR_ADT_BOOL
#define CAESAR_ADT_BITS_ADT_BOOL : 1
/* ------------------------------------------------------------------------- */
#define ADT_FALSE() ((ADT_BOOL) 0)
#define ADT_TRUE() ((ADT_BOOL) 1)
/* ------------------------------------------------------------------------- */
#define ADT_CMP_BOOL(CAESAR_ADT_1,CAESAR_ADT_2) ((CAESAR_ADT_1) == (CAESAR_ADT_2))
/* ------------------------------------------------------------------------- */
#ifdef CAESAR_ADT_INTERFACE
extern char *CAESAR_ADT_ASCII_ADT_BOOL[];
#else
char *CAESAR_ADT_ASCII_ADT_BOOL[] = {
"FALSE",
"TRUE"
};
#endif /* CAESAR_ADT_INTERFACE */
#define ADT_PRINT_BOOL(CAESAR_ADT_FILE,CAESAR_ADT_0) fprintf (CAESAR_ADT_FILE, CAESAR_ADT_ASCII_ADT_BOOL [CAESAR_ADT_0])
/* ------------------------------------------------------------------------- */
#define CAESAR_ADT_is_ADT_FALSE(CAESAR_ADT_0) ((CAESAR_ADT_0) == ADT_FALSE())
#define CAESAR_ADT_is_ADT_TRUE(CAESAR_ADT_0) ((CAESAR_ADT_0) == ADT_TRUE())
/* ========================================================================= */
#include "spec_1.t"
#define CAESAR_ADT_INCLUDE_T
/* CAUTION: there exists C types, comparison functions, enumeration functions and printing macros that can not be generated automatically by CAESAR.ADT, since the corresponding LOTOS sorts have no constructors. These C objects will be considered as extern and it is assumed that their definition is contained in file "spec_1.t" provided by the user. The list of these objects is given below: */
/* (1) the type ADT_NAT implementing sort NAT */
/* (2) the comparison function ADT_CMP_NAT for sort NAT */
/* (3) the enumeration macro ADT_ENUM_FIRST_NAT for sort NAT */
/* (4) the enumeration macro ADT_ENUM_NEXT_NAT for sort NAT */
/* (5) the printing function ADT_PRINT_NAT for sort NAT */
/* (6) the function ADT_N0 implementing constructor 0 */
/* (7) the testor function CAESAR_ADT_is_ADT_N0 for constructor 0 */
/* (8) the function ADT_SUCC implementing constructor SUCC */
/* (9) the testor function CAESAR_ADT_is_ADT_SUCC for constructor SUCC */
/* (10) the selector #1 function CAESAR_ADT_Get_1_ADT_SUCC for constructor SUCC */
/* ========================================================================= */
#ifndef ADT_ENUM_FIRST_BOOL
#define ADT_ENUM_FIRST_BOOL() (ADT_FALSE())
#endif
#ifndef ADT_ENUM_NEXT_BOOL
#define ADT_ENUM_NEXT_BOOL(CAESAR_ADT_0) ((CAESAR_ADT_0)++ < ADT_TRUE())
#endif
/* ========================================================================= */
#define CAESAR_ADT_CASE_NIL ((unsigned char) 0)
#define CAESAR_ADT_CASE_ENQUEUE ((unsigned char) 1)
typedef struct CAESAR_ADT_STRUCT_CAESAR_ADT_TYPE_QUEUE_NAT {
unsigned char CAESAR_ADT_ENUM_CAESAR_ADT_TYPE_QUEUE_NAT:1;
union {
struct {
ADT_NAT CAESAR_ADT_1_ENQUEUE
#ifdef CAESAR_ADT_BITS_ADT_NAT
CAESAR_ADT_BITS_ADT_NAT
#endif
;
CAESAR_ADT_TYPE_QUEUE_NAT CAESAR_ADT_2_ENQUEUE
#ifdef CAESAR_ADT_BITS_CAESAR_ADT_TYPE_QUEUE_NAT
CAESAR_ADT_BITS_CAESAR_ADT_TYPE_QUEUE_NAT
#endif
;
} CAESAR_ADT_FIELD_ENQUEUE;
} CAESAR_ADT_UNION_CAESAR_ADT_TYPE_QUEUE_NAT;
} CAESAR_ADT_BODY_CAESAR_ADT_TYPE_QUEUE_NAT;
/* ========================================================================= */
#ifndef CAESAR_ADT_INTERFACE
int CAESAR_ADT_CMP_QUEUE_NAT (CAESAR_ADT_1, CAESAR_ADT_2)
CAESAR_ADT_TYPE_QUEUE_NAT CAESAR_ADT_1;
CAESAR_ADT_TYPE_QUEUE_NAT CAESAR_ADT_2;
{
if ((CAESAR_ADT_1 == NULL) || (CAESAR_ADT_2 == NULL))
return (CAESAR_ADT_1 == CAESAR_ADT_2);
if (CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_1).CAESAR_ADT_ENUM_CAESAR_ADT_TYPE_QUEUE_NAT != CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_2).CAESAR_ADT_ENUM_CAESAR_ADT_TYPE_QUEUE_NAT)
return 0;
switch (CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_1).CAESAR_ADT_ENUM_CAESAR_ADT_TYPE_QUEUE_NAT) {
case CAESAR_ADT_CASE_NIL:
return 1;
case CAESAR_ADT_CASE_ENQUEUE:
return ADT_CMP_NAT (CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_1).CAESAR_ADT_UNION_CAESAR_ADT_TYPE_QUEUE_NAT.CAESAR_ADT_FIELD_ENQUEUE.CAESAR_ADT_1_ENQUEUE, CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_2).CAESAR_ADT_UNION_CAESAR_ADT_TYPE_QUEUE_NAT.CAESAR_ADT_FIELD_ENQUEUE.CAESAR_ADT_1_ENQUEUE) && CAESAR_ADT_CMP_QUEUE_NAT (CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_1).CAESAR_ADT_UNION_CAESAR_ADT_TYPE_QUEUE_NAT.CAESAR_ADT_FIELD_ENQUEUE.CAESAR_ADT_2_ENQUEUE, CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_2).CAESAR_ADT_UNION_CAESAR_ADT_TYPE_QUEUE_NAT.CAESAR_ADT_FIELD_ENQUEUE.CAESAR_ADT_2_ENQUEUE);
}
/* NOTREACHED */
}
#endif /* CAESAR_ADT_INTERFACE */
/* ------------------------------------------------------------------------- */
#ifndef CAESAR_ADT_INTERFACE
void CAESAR_ADT_PRT_QUEUE_NAT (CAESAR_ADT_FILE, CAESAR_ADT_0)
FILE *CAESAR_ADT_FILE;
CAESAR_ADT_TYPE_QUEUE_NAT CAESAR_ADT_0;
{
if (CAESAR_ADT_0 == NULL)
fprintf (CAESAR_ADT_FILE, "?");
else {
switch (CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_0).CAESAR_ADT_ENUM_CAESAR_ADT_TYPE_QUEUE_NAT) {
case CAESAR_ADT_CASE_NIL:
fprintf (CAESAR_ADT_FILE, "NIL");
break;
case CAESAR_ADT_CASE_ENQUEUE:
fprintf (CAESAR_ADT_FILE, "ENQUEUE (");
ADT_PRINT_NAT (CAESAR_ADT_FILE, CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_0).CAESAR_ADT_UNION_CAESAR_ADT_TYPE_QUEUE_NAT.CAESAR_ADT_FIELD_ENQUEUE.CAESAR_ADT_1_ENQUEUE);
fprintf (CAESAR_ADT_FILE, ", ");
CAESAR_ADT_PRT_QUEUE_NAT (CAESAR_ADT_FILE, CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_0).CAESAR_ADT_UNION_CAESAR_ADT_TYPE_QUEUE_NAT.CAESAR_ADT_FIELD_ENQUEUE.CAESAR_ADT_2_ENQUEUE);
fprintf (CAESAR_ADT_FILE, ")");
break;
}
}
}
#endif /* CAESAR_ADT_INTERFACE */
/* ========================================================================= */
#ifdef CAESAR_ADT_INTERFACE
extern CAESAR_ADT_TYPE_QUEUE_NAT NIL ();
#else
CAESAR_ADT_TYPE_QUEUE_NAT NIL ()
{
static CAESAR_ADT_TYPE_QUEUE_NAT CAESAR_ADT_0 = NULL;
if (CAESAR_ADT_0 == NULL) {
CAESAR_ADT_ALLOC (CAESAR_ADT_0, CAESAR_ADT_BODY_CAESAR_ADT_TYPE_QUEUE_NAT, CAESAR_ADT_TYPE_QUEUE_NAT, "NIL [8]", "NIL");
CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_0).CAESAR_ADT_ENUM_CAESAR_ADT_TYPE_QUEUE_NAT = CAESAR_ADT_CASE_NIL;
}
return CAESAR_ADT_0;
}
#endif /* CAESAR_ADT_INTERFACE */
/* ------------------------------------------------------------------------- */
#ifdef CAESAR_ADT_INTERFACE
extern CAESAR_ADT_TYPE_QUEUE_NAT ENQUEUE ();
#else
CAESAR_ADT_TYPE_QUEUE_NAT ENQUEUE (CAESAR_ADT_1, CAESAR_ADT_2)
ADT_NAT CAESAR_ADT_1;
CAESAR_ADT_TYPE_QUEUE_NAT CAESAR_ADT_2;
{
CAESAR_ADT_TYPE_QUEUE_NAT CAESAR_ADT_0;
CAESAR_ADT_ALLOC (CAESAR_ADT_0, CAESAR_ADT_BODY_CAESAR_ADT_TYPE_QUEUE_NAT, CAESAR_ADT_TYPE_QUEUE_NAT, "ENQUEUE [9]", "ENQUEUE");
CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_0).CAESAR_ADT_ENUM_CAESAR_ADT_TYPE_QUEUE_NAT = CAESAR_ADT_CASE_ENQUEUE;
CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_0).CAESAR_ADT_UNION_CAESAR_ADT_TYPE_QUEUE_NAT.CAESAR_ADT_FIELD_ENQUEUE.CAESAR_ADT_1_ENQUEUE = CAESAR_ADT_1;
CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_0).CAESAR_ADT_UNION_CAESAR_ADT_TYPE_QUEUE_NAT.CAESAR_ADT_FIELD_ENQUEUE.CAESAR_ADT_2_ENQUEUE = CAESAR_ADT_2;
return CAESAR_ADT_0;
}
#endif /* CAESAR_ADT_INTERFACE */
/* ------------------------------------------------------------------------- */
#define CAESAR_ADT_is_NIL(CAESAR_ADT_0) (CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_0).CAESAR_ADT_ENUM_CAESAR_ADT_TYPE_QUEUE_NAT == CAESAR_ADT_CASE_NIL)
#define CAESAR_ADT_is_ENQUEUE(CAESAR_ADT_0) (CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_0).CAESAR_ADT_ENUM_CAESAR_ADT_TYPE_QUEUE_NAT == CAESAR_ADT_CASE_ENQUEUE)
#define CAESAR_ADT_Get_1_ENQUEUE(CAESAR_ADT_0) (CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_0).CAESAR_ADT_UNION_CAESAR_ADT_TYPE_QUEUE_NAT.CAESAR_ADT_FIELD_ENQUEUE.CAESAR_ADT_1_ENQUEUE)
#define CAESAR_ADT_Get_2_ENQUEUE(CAESAR_ADT_0) (CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_0).CAESAR_ADT_UNION_CAESAR_ADT_TYPE_QUEUE_NAT.CAESAR_ADT_FIELD_ENQUEUE.CAESAR_ADT_2_ENQUEUE)
/* ------------------------------------------------------------------------- */
/* sort QUEUE_NAT is infinite: no iterator can be generated automatically for this sort; however, it is possible to specify manually an iterator for a finite subset of QUEUE_NAT by defining two macros CAESAR_ADT_ITR_FIRST_QUEUE_NAT() and CAESAR_ADT_ITR_NEXT_QUEUE_NAT() in file "spec_1.t" */
/* ========================================================================= */
/* forward */ ADT_BOOL ADT_AND ();
/* forward */ ADT_BOOL ADT_OR ();
/* forward */ ADT_BOOL ADT_XOR ();
/* forward */ ADT_BOOL ADT_IFF ();
/* ------------------------------------------------------------------------- */
/* forward */ CAESAR_ADT_TYPE_QUEUE_NAT DEQUEUE ();
/* forward */ ADT_NAT FIRST ();
/* forward */ ADT_NAT LAST ();
/* forward */ CAESAR_ADT_TYPE_QUEUE_NAT DESTROY ();
/* ========================================================================= */
#define ADT_NOT(CAESAR_ADT_1) (CAESAR_ADT_is_ADT_TRUE (CAESAR_ADT_1) ? ADT_FALSE () : ADT_TRUE ())
/* ------------------------------------------------------------------------- */
#define ADT_IMPLIES(CAESAR_ADT_1, CAESAR_ADT_2) ADT_OR (CAESAR_ADT_2, ADT_NOT (CAESAR_ADT_1))
/* ------------------------------------------------------------------------- */
#define ADT_EQ_BOOL(CAESAR_ADT_1, CAESAR_ADT_2) ADT_IFF (CAESAR_ADT_1, CAESAR_ADT_2)
/* ------------------------------------------------------------------------- */
#define ADT_NE_BOOL(CAESAR_ADT_1, CAESAR_ADT_2) ADT_XOR (CAESAR_ADT_1, CAESAR_ADT_2)
/* ========================================================================= */
#define EMPTY(CAESAR_ADT_1) (CAESAR_ADT_is_NIL (CAESAR_ADT_1) ? ADT_TRUE () : ADT_FALSE ())
/* ========================================================================= */
#ifndef CAESAR_ADT_INTERFACE
#include "spec_1.f"
#define CAESAR_ADT_INCLUDE_F
#endif /* CAESAR_ADT_INTERFACE */
/* CAUTION: there exists C functions that can not be generated automatically by CAESAR.ADT, since the corresponding LOTOS (non-constructor) operations are not defined by equations. These C functions will be considered as extern and it is assumed that their definition is contained in file "spec_1.f" provided by the user. The list of these functions is given below: */
/* (1) the function ADT_PLUS implementing operation + */
/* (2) the function ADT_MULT implementing operation * */
/* (3) the function ADT_POWER implementing operation ** */
/* (4) the function ADT_EQ_NAT implementing operation EQ */
/* (5) the function ADT_NE_NAT implementing operation NE */
/* (6) the function ADT_LT_NAT implementing operation LT */
/* (7) the function ADT_LE_NAT implementing operation LE */
/* (8) the function ADT_GT_NAT implementing operation GT */
/* (9) the function ADT_GE_NAT implementing operation GE */
/* (10) the function ADT_N1 implementing operation 1 */
/* (11) the function ADT_N2 implementing operation 2 */
/* (12) the function ADT_N3 implementing operation 3 */
/* (13) the function ADT_N4 implementing operation 4 */
/* (14) the function ADT_N5 implementing operation 5 */
/* (15) the function ADT_N6 implementing operation 6 */
/* (16) the function ADT_N7 implementing operation 7 */
/* (17) the function ADT_N8 implementing operation 8 */
/* (18) the function ADT_N9 implementing operation 9 */
/* (19) the function ADT_MINUS implementing operation - */
/* (20) the function ADT_DIV implementing operation DIV */
/* (21) the function ADT_MOD implementing operation MOD */
/* (22) the function ADT_EQ_BIS_NAT implementing operation == */
/* (23) the function ADT_NE_BIS_NAT implementing operation <> */
/* (24) the function ADT_LT_BIS_NAT implementing operation < */
/* (25) the function ADT_LE_BIS_NAT implementing operation <= */
/* (26) the function ADT_GT_BIS_NAT implementing operation > */
/* (27) the function ADT_GE_BIS_NAT implementing operation >= */
/* (28) the function ADT_MIN implementing operation MIN */
/* (29) the function ADT_MAX implementing operation MAX */
/* (30) the function ADT_GCD implementing operation GCD */
/* (31) the function ADT_SCM implementing operation SCM */
/* ========================================================================= */
#ifndef CAESAR_ADT_INTERFACE
ADT_BOOL ADT_AND (CAESAR_ADT_1, CAESAR_ADT_2)
ADT_BOOL CAESAR_ADT_1;
ADT_BOOL CAESAR_ADT_2;
{
if (CAESAR_ADT_is_ADT_TRUE (CAESAR_ADT_2))
return CAESAR_ADT_1;
else
return CAESAR_ADT_2;
}
#endif /* CAESAR_ADT_INTERFACE */
/* ------------------------------------------------------------------------- */
#ifndef CAESAR_ADT_INTERFACE
ADT_BOOL ADT_OR (CAESAR_ADT_1, CAESAR_ADT_2)
ADT_BOOL CAESAR_ADT_1;
ADT_BOOL CAESAR_ADT_2;
{
if (CAESAR_ADT_is_ADT_TRUE (CAESAR_ADT_2))
return CAESAR_ADT_2;
else
return CAESAR_ADT_1;
}
#endif /* CAESAR_ADT_INTERFACE */
/* ------------------------------------------------------------------------- */
#ifndef CAESAR_ADT_INTERFACE
ADT_BOOL ADT_XOR (CAESAR_ADT_1, CAESAR_ADT_2)
ADT_BOOL CAESAR_ADT_1;
ADT_BOOL CAESAR_ADT_2;
{
return ADT_OR (ADT_AND (CAESAR_ADT_1, ADT_NOT (CAESAR_ADT_2)), ADT_AND (CAESAR_ADT_2, ADT_NOT (CAESAR_ADT_1)));
}
#endif /* CAESAR_ADT_INTERFACE */
/* ------------------------------------------------------------------------- */
#ifndef CAESAR_ADT_INTERFACE
ADT_BOOL ADT_IFF (CAESAR_ADT_1, CAESAR_ADT_2)
ADT_BOOL CAESAR_ADT_1;
ADT_BOOL CAESAR_ADT_2;
{
return ADT_AND (ADT_IMPLIES (CAESAR_ADT_1, CAESAR_ADT_2), ADT_IMPLIES (CAESAR_ADT_2, CAESAR_ADT_1));
}
#endif /* CAESAR_ADT_INTERFACE */
/* ========================================================================= */
#ifndef CAESAR_ADT_INTERFACE
CAESAR_ADT_TYPE_QUEUE_NAT DEQUEUE (CAESAR_ADT_1)
CAESAR_ADT_TYPE_QUEUE_NAT CAESAR_ADT_1;
{
if (CAESAR_ADT_is_ENQUEUE (CAESAR_ADT_1))
if (CAESAR_ADT_is_NIL (CAESAR_ADT_Get_2_ENQUEUE (CAESAR_ADT_1)))
return NIL ();
else if (ADT_NOT (EMPTY (CAESAR_ADT_Get_2_ENQUEUE (CAESAR_ADT_1))))
return ENQUEUE (CAESAR_ADT_Get_1_ENQUEUE (CAESAR_ADT_1), DEQUEUE (CAESAR_ADT_Get_2_ENQUEUE (CAESAR_ADT_1)));
else
CAESAR_ADT_ERROR ("DEQUEUE [10]", "DEQUEUE");
else
CAESAR_ADT_ERROR ("DEQUEUE [10]", "DEQUEUE");
/* NOTREACHED */
}
#endif /* CAESAR_ADT_INTERFACE */
/* ------------------------------------------------------------------------- */
#ifndef CAESAR_ADT_INTERFACE
ADT_NAT FIRST (CAESAR_ADT_1)
CAESAR_ADT_TYPE_QUEUE_NAT CAESAR_ADT_1;
{
if (CAESAR_ADT_is_ENQUEUE (CAESAR_ADT_1))
if (CAESAR_ADT_is_NIL (CAESAR_ADT_Get_2_ENQUEUE (CAESAR_ADT_1)))
return CAESAR_ADT_Get_1_ENQUEUE (CAESAR_ADT_1);
else if (ADT_NOT (EMPTY (CAESAR_ADT_Get_2_ENQUEUE (CAESAR_ADT_1))))
return FIRST (CAESAR_ADT_Get_2_ENQUEUE (CAESAR_ADT_1));
else
CAESAR_ADT_ERROR ("FIRST [12]", "FIRST");
else
CAESAR_ADT_ERROR ("FIRST [12]", "FIRST");
/* NOTREACHED */
}
#endif /* CAESAR_ADT_INTERFACE */
/* ------------------------------------------------------------------------- */
#ifndef CAESAR_ADT_INTERFACE
ADT_NAT LAST (CAESAR_ADT_1)
CAESAR_ADT_TYPE_QUEUE_NAT CAESAR_ADT_1;
{
if (CAESAR_ADT_is_ENQUEUE (CAESAR_ADT_1))
return CAESAR_ADT_Get_1_ENQUEUE (CAESAR_ADT_1);
else
CAESAR_ADT_ERROR ("LAST [13]", "LAST");
/* NOTREACHED */
}
#endif /* CAESAR_ADT_INTERFACE */
/* ------------------------------------------------------------------------- */
#ifndef CAESAR_ADT_INTERFACE
CAESAR_ADT_TYPE_QUEUE_NAT DESTROY (CAESAR_ADT_1, CAESAR_ADT_2)
ADT_NAT CAESAR_ADT_1;
CAESAR_ADT_TYPE_QUEUE_NAT CAESAR_ADT_2;
{
if (CAESAR_ADT_is_NIL (CAESAR_ADT_2))
return CAESAR_ADT_2;
else if (ADT_EQ_NAT (CAESAR_ADT_1, CAESAR_ADT_Get_1_ENQUEUE (CAESAR_ADT_2)))
return DESTROY (CAESAR_ADT_1, CAESAR_ADT_Get_2_ENQUEUE (CAESAR_ADT_2));
else if (ADT_NE_NAT (CAESAR_ADT_1, CAESAR_ADT_Get_1_ENQUEUE (CAESAR_ADT_2)))
return ENQUEUE (CAESAR_ADT_Get_1_ENQUEUE (CAESAR_ADT_2), DESTROY (CAESAR_ADT_1, CAESAR_ADT_Get_2_ENQUEUE (CAESAR_ADT_2)));
else
CAESAR_ADT_ERROR ("DESTROY [14]", "DESTROY");
/* NOTREACHED */
}
#endif /* CAESAR_ADT_INTERFACE */
/* ========================================================================= */
#ifndef CAESAR_ADT_INTERFACE
void CAESAR_ADT_INIT ()
{
}
#endif /* CAESAR_ADT_INTERFACE */
/* ========================================================================= */