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
|
/*
* Copyright (C) 2000, Imperial College
*
* This file is part of the Imperial College Exact Real Arithmetic Library.
* See the copyright notice included in the distribution for conditions
* of use.
*/
#include <stdio.h>
#include "real.h"
#include "real-impl.h"
/*
* This file contains support for realIf (aka alternation).
*/
#include <stdarg.h>
Real
realIf(int numGE, ...)
{
va_list ap;
Alt *alt;
GuardedExpr *geList;
void force_To_Alt_From_The_Abyss();
int i;
bool isSigned = FALSE;
if ((alt = (Alt *) malloc(sizeof(Alt))) == NULL)
Error(FATAL, E_INT, "realIf", "malloc failed (Alt)");
#ifdef DAVINCI
newNodeId(alt);
#else
#ifdef TRACE
newNodeId(alt);
#endif
#endif
va_start(ap, numGE);
if ((geList = (GuardedExpr *) malloc(sizeof(GuardedExpr) * numGE)) == NULL)
Error(FATAL, E_INT, "realIf", "malloc failed (GE)");
alt->tag.type = ALT;
alt->tag.dumped = FALSE;
alt->GE = geList;
alt->numGE = numGE;
alt->nextGE = 0;
alt->force = force_To_Alt_From_The_Abyss;
alt->redirect = NULL;
#ifdef DAVINCI
beginGraphUpdate();
newNode(alt, ALT);
endGraphUpdate();
#endif
/*
* Now we consume the arguments. Each is a guard/value pair.
*/
for (i = 0; i < numGE; i++) {
geList[i].guard = va_arg(ap, Bool);
geList[i].x = va_arg(ap, Real);
isSigned = isSigned || geList[i].x->gen.tag.isSigned;
#ifdef DAVINCI
beginGraphUpdate();
newEdgeToChildN(alt, geList[i].guard, i);
newEdgeToChildN(alt, geList[i].x, i);
endGraphUpdate();
#endif
}
va_end(ap);
alt->tag.isSigned = isSigned;
return (Real) alt;
}
void
force_To_Alt_From_The_Abyss()
{
Error(FATAL, E_INT, "force_To_Alt_From_The_Abyss",
"trying to force a conditional");
}
/*
* This force method is used to force (evaluate) an alt. To accommodate
* the case where the alt itself evaluates to an alt, the force methods are
* applied recursively and the alt chain reduced. Thus, once the force is
* complete, the alt on the stack has a value alt->redirect which is a real
* and which is not itself an alt. If we were writing a recursive function,
* rather than using an explicit stack, the following three functions
* including the reduction would be coded as a single function as follows:
*
* force_Alt(Alt *alt)
* {
* if (alt->redirect == NULL)
* force_Alt_Eval(alt); evaluate the single alt and set alt->redirect
* if (alt->redirect->gen.tag.type == ALT) {
* force_Alt(alt->redirect); make the recusive call and do the reduction
* alt->redirect = alt->redirect->alt.redirect;
* }
* }
*/
void
force_To_Alt_Entry()
{
Alt *alt;
void force_To_Alt_Cont();
void force_Alt_Eval();
Bool guard;
alt = (Alt *) POP;
PUSH_2(force_To_Alt_Cont, alt);
/*
* If alt->redirect is not valid (equals NULL) then the value of
* the conditional has not been determined so we need to force it.
* This means forcing the first guard.
*/
if (alt->redirect == NULL) {
PUSH_2(force_Alt_Eval, alt);
guard = alt->GE[alt->nextGE].guard;
PUSH_2(guard->gen.force, guard);
}
}
void
force_To_Alt_Cont()
{
Alt *alt;
void force_To_Alt_Reduce();
alt = (Alt *) POP;
/*
* So we have evaluated the alternation and alt->redirect is the real
* associated with the guard that evaluated to true. However, that
* real may itself be an alt. If so, then we arrange to evaluate the
* second alt and also to reduce the chain.
*/
if (alt->redirect->gen.tag.type == ALT) {
PUSH_2(force_To_Alt_Reduce, alt);
PUSH_2(force_To_Alt_Entry, alt->redirect);
}
}
/*
* The following is used only when the alt evaluates to a real which is
* itself an alt. This function performs the reduction.
*/
void
force_To_Alt_Reduce()
{
Alt *alt;
alt = (Alt *) POP;
#ifdef DAVINCI
beginGraphUpdate();
deleteOnlyEdge(alt, alt->redirect);
newEdgeToOnlyChild(alt, alt->redirect->alt.redirect);
endGraphUpdate();
#endif
alt->redirect = alt->redirect->alt.redirect;
if (alt->redirect->gen.tag.type == ALT)
Error(FATAL, E_INT, "force_To_Alt_Cont_Cont",
"alt chain not fully reduced");
}
/*
* Our objective here is to evaluate a single conditional. This means
* forcing each guard in turn and checking to see if it becomes true.
* This force function is only activated by force_To_Alt_Entry and by itself.
* When activated, we know that we have forced one of the guards so
* we start by checking the value of the guard.
*/
void
force_Alt_Eval()
{
Alt *alt;
Bool guard;
int advanceToNextGE(Alt *alt);
alt = (Alt *) POP;
guard = alt->GE[alt->nextGE].guard;
switch (guard->gen.tag.value) {
/*
* If the current guard is true, then record the value of the guard
* in the Alt structure. Thereafter we will used the stored value. At this
* point it might be wise to make all the pointers in the guard/value
* pairs to NULL so that the garbage collector can have them.
*/
case LAZY_TRUE :
alt->redirect = alt->GE[alt->nextGE].x;
#ifdef DAVINCI
deleteEdgeToChildN(alt, alt->GE[alt->nextGE].guard, alt->nextGE);
deleteEdgeToChildN(alt, alt->GE[alt->nextGE].x, alt->nextGE);
drawEqEdge(alt, alt->GE[alt->nextGE].x);
alt->GE[alt->nextGE].guard = NULL;
alt->GE[alt->nextGE].x = NULL;
while (advanceToNextGE(alt)) {
deleteEdgeToChildN(alt, alt->GE[alt->nextGE].guard, alt->nextGE);
deleteEdgeToChildN(alt, alt->GE[alt->nextGE].x, alt->nextGE);
alt->GE[alt->nextGE].guard = NULL;
alt->GE[alt->nextGE].x = NULL;
}
#endif
break;
/*
* If the current guard evaluates to false, then we want to eliminate the
* the guard (and value) from future consideration. So we set the fields
* to NULL and advance to the next pair and force the guard.
*/
case LAZY_FALSE :
#ifdef DAVINCI
beginGraphUpdate();
deleteEdgeToChildN(alt, alt->GE[alt->nextGE].guard, alt->nextGE);
deleteEdgeToChildN(alt, alt->GE[alt->nextGE].x, alt->nextGE);
endGraphUpdate();
#endif
alt->GE[alt->nextGE].guard = NULL;
alt->GE[alt->nextGE].x = NULL;
if (!advanceToNextGE(alt))
Error(FATAL, E_INT, "force_Alt_Eval", "no guards left");
PUSH_2(force_Alt_Eval, alt);
PUSH_2(alt->GE[alt->nextGE].guard->gen.force,
alt->GE[alt->nextGE].guard);
break;
/*
* Finally, if the guard is still unknown, we simply advance to the
* next pair and force the guard.
*/
case LAZY_UNKNOWN :
if (!advanceToNextGE(alt))
Error(FATAL, E_INT, "force_Alt_Eval", "no guards left");
PUSH_2(force_Alt_Eval, alt);
PUSH_2(alt->GE[alt->nextGE].guard->gen.force,
alt->GE[alt->nextGE].guard);
break;
default :
Error(FATAL, E_INT, "force_Alt_Eval",
"invalid boolean value encountered");
break;
}
}
/*
* This local function scans through the list of guarded expressions looking
* for the index of the next valid pair following the given index. Pairs in
* which the guard has been evaluated to false have been set to NULL.
* So we are looking for the first non-NULL pair. It may be the same
* index we are given though to be honest, if we are down to one GE pair
* without a true guard, then there is a pretty good chance the programmer
* has chosen guards which don't overlap.
* This returns 0 (false) if no pair is found.
*/
int
advanceToNextGE(Alt *alt)
{
int i;
for (i = (alt->nextGE + 1) % alt->numGE;
i != alt->nextGE; i = (i + 1) % alt->numGE) {
if (alt->GE[i].guard != NULL) {
alt->nextGE = i;
return 1;
}
}
if (alt->GE[i].guard != NULL) {
alt->nextGE = i;
return 1;
}
return 0;
}
|
