001 package escjava.vcGeneration.simplify;
002
003 import java.io.*;
004
005 import escjava.vcGeneration.*;
006
007 class TSimplifyVisitor extends TVisitor {
008
009 TSimplifyVisitor(Writer out) {
010 super(out);
011 }
012
013 /*
014 * General Function
015 * You give the operator at the first argument and then it outputs
016 * (op
017 * (son1 son2 ...)
018 * )
019 */
020
021 public void genericOp(/*@ non_null @*/String s, TFunction n) throws IOException {
022
023 lib.appendI(s);
024
025 int i = 0;
026 for (; i <= n.sons.size() - 1; i++)
027 n.getChildAt(i).accept(this);
028
029 /*
030 * Stick to the old representation :
031 * if last child was a variable don't go to next line
032 */
033 if ((n.getChildAt(--i)) instanceof TName)
034 lib.reduceIwNl();
035 else
036 lib.reduceI();
037 }
038
039
040 public void visitTName(/*@ non_null @*/TName n) throws IOException {
041 /*
042 * This call handles everything, ie if n is a variable or a type name
043 */
044 VariableInfo vi = TNode.getVariableInfo(n.name);
045 lib.appendN(" " + vi.getVariableInfo());
046 }
047
048 public void visitTRoot(/*@ non_null @*/TRoot n) throws IOException {
049 for (int i = 0; i <= n.sons.size() - 1; i++)
050 n.getChildAt(i).accept(this);
051 }
052
053 /*
054 * class created using the perl script
055 */
056 public void visitTBoolImplies(/*@ non_null @*/TBoolImplies n) throws IOException {
057 genericOp("IMPLIES", n);
058 }
059
060 // take care special behaviour here, fixme explains why
061 public void visitTBoolAnd(/*@ non_null @*/TBoolAnd n) throws IOException {
062
063 lib.appendI("AND");
064
065 int i = 0;
066 TNode m = null;
067 TNode o = null;
068
069 for (; i <= n.sons.size() - 2; i++) {
070 m = n.getChildAt(i);
071 o = n.getChildAt(i + 1);
072
073 if (o instanceof TBoolean) {
074 TBoolean p = (TBoolean) o;
075 if (p.value) // we have a true value just at the bottom
076 // of boolean and, it's means that the previous node
077 // need to be outputted as (EQ |@true|
078 // blabla)
079 {
080 lib.appendI("EQ");
081 lib.appendN(" |@true|");
082 m.accept(this);
083 i++;
084 }
085 } else {
086 m.accept(this);
087 o.accept(this);
088
089 /* not at the end */
090 if (i <= n.sons.size() - 3)
091 i++;
092 }
093 }
094
095 /*
096 * Stick to the old representation :
097 * if last child was a variable don't go to next line
098 */
099 if ((n.getChildAt(i)) instanceof TName)
100 lib.reduceIwNl();
101 else
102 lib.reduceI();
103
104 }
105
106 public void visitTBoolOr(/*@ non_null @*/TBoolOr n) throws IOException {
107 genericOp("OR", n);
108 }
109
110 public void visitTBoolNot(/*@ non_null @*/TBoolNot n) throws IOException {
111 genericOp("NOT", n);
112 }
113
114 public void visitTBoolEQ(/*@ non_null @*/TBoolEQ n) throws IOException {
115 genericOp("EQ", n);
116 }
117
118 public void visitTBoolNE(/*@ non_null @*/TBoolNE n) throws IOException {
119 genericOp("NEQ", n);
120 }
121
122 public void visitTAllocLT(/*@ non_null @*/TAllocLT n) throws IOException {
123 genericOp("<", n);
124 }
125
126 public void visitTAllocLE(/*@ non_null @*/TAllocLE n) throws IOException {
127 genericOp("<=", n);
128 }
129
130 public void visitTAnyEQ(/*@ non_null @*/TAnyEQ n) throws IOException {
131 genericOp("EQ", n);
132 }
133
134 public void visitTAnyNE(/*@ non_null @*/TAnyNE n) throws IOException {
135 genericOp("NEQ", n);
136 }
137
138 public void visitTIntegralEQ(/*@ non_null @*/TIntegralEQ n) throws IOException {
139 genericOp("EQ", n);
140 }
141
142 public void visitTIntegralGE(/*@ non_null @*/TIntegralGE n) throws IOException {
143 genericOp(">=", n);
144 }
145
146 public void visitTIntegralGT(/*@ non_null @*/TIntegralGT n) throws IOException {
147 genericOp(">", n);
148 }
149
150 public void visitTIntegralLE(/*@ non_null @*/TIntegralLE n) throws IOException {
151 genericOp("<=", n);
152 }
153
154 public void visitTIntegralLT(/*@ non_null @*/TIntegralLT n) throws IOException {
155 genericOp("<", n);
156 }
157
158 public void visitTIntegralNE(/*@ non_null @*/TIntegralNE n) throws IOException {
159 genericOp("NEQ", n);
160 }
161
162 public void visitTIntegralAdd(/*@ non_null @*/TIntegralAdd n) throws IOException {
163 genericOp("+", n);
164 }
165
166 public void visitTIntegralDiv(/*@ non_null @*/TIntegralDiv n) throws IOException {
167 genericOp("integralDiv", n);
168 }
169
170 public void visitTIntegralMod(/*@ non_null @*/TIntegralMod n) throws IOException {
171 genericOp("integralMod", n);
172 }
173
174 public void visitTIntegralMul(/*@ non_null @*/TIntegralMul n) throws IOException {
175 genericOp("*", n);
176 }
177
178 public void visitTFloatEQ(/*@ non_null @*/TFloatEQ n) throws IOException {
179 genericOp("floatingEQ", n);
180 }
181
182 public void visitTFloatGE(/*@ non_null @*/TFloatGE n) throws IOException {
183 genericOp("floatingGE", n);
184 }
185
186 public void visitTFloatGT(/*@ non_null @*/TFloatGT n) throws IOException {
187 genericOp("floatingGT", n);
188 }
189
190 public void visitTFloatLE(/*@ non_null @*/TFloatLE n) throws IOException {
191 genericOp("floatingLE", n);
192 }
193
194 public void visitTFloatLT(/*@ non_null @*/TFloatLT n) throws IOException {
195 genericOp("floatingGE", n);
196 }
197
198 public void visitTFloatNE(/*@ non_null @*/TFloatNE n) throws IOException {
199 genericOp("floatingNE", n);
200 }
201
202 public void visitTFloatAdd(/*@ non_null @*/TFloatAdd n) throws IOException {
203 genericOp("floatingAdd", n);
204 }
205
206 public void visitTFloatDiv(/*@ non_null @*/TFloatDiv n) throws IOException {
207 genericOp("floatingDiv", n);
208 }
209
210 public void visitTFloatMod(/*@ non_null @*/TFloatMod n) throws IOException {
211 genericOp("floatingMod", n);
212 }
213
214 public void visitTFloatMul(/*@ non_null @*/TFloatMul n) throws IOException {
215 genericOp("floatingMul", n);
216 }
217
218 public void visitTLockLE(/*@ non_null @*/TLockLE n) throws IOException {
219 genericOp("lockLE", n);
220 }
221
222 public void visitTLockLT(/*@ non_null @*/TLockLT n) throws IOException {
223 genericOp("lockLT", n);
224 }
225
226 public void visitTRefEQ(/*@ non_null @*/TRefEQ n) throws IOException {
227 genericOp("EQ", n);
228 }
229
230 public void visitTRefNE(/*@ non_null @*/TRefNE n) throws IOException {
231 genericOp("NEQ", n);
232 }
233
234 public void visitTTypeEQ(/*@ non_null @*/TTypeEQ n) throws IOException {
235 genericOp("EQ", n);
236 }
237
238 public void visitTTypeNE(/*@ non_null @*/TTypeNE n) throws IOException {
239 genericOp("NEQ", n);
240 }
241
242 public void visitTTypeLE(/*@ non_null @*/TTypeLE n) throws IOException {
243 genericOp("<:", n);
244 }
245
246 public void visitTCast(/*@ non_null @*/TCast n) throws IOException {
247 genericOp("cast", n);
248 }
249
250 public void visitTIs(/*@ non_null @*/TIs n) throws IOException {
251
252 //add (EQ |@true| blabla )
253 lib.appendI("EQ");
254 lib.appendN(" |@true|");
255
256 genericOp("is", n);
257
258 lib.reduceI();
259 }
260
261 public void visitTSelect(/*@ non_null @*/TSelect n) throws IOException {
262 genericOp("select", n);
263 }
264
265 public void visitTStore(/*@ non_null @*/TStore n) throws IOException {
266 genericOp("store", n);
267 }
268
269 public void visitTTypeOf(/*@ non_null @*/TTypeOf n) throws IOException {
270 genericOp("typeof", n);
271 }
272
273 public void visitTForAll(/*@ non_null @*/TForAll n) throws IOException {
274 }
275
276 public void visitTExist(/*@ non_null @*/TExist n) throws IOException {
277 }
278
279 public void visitTIsAllocated(/*@ non_null @*/TIsAllocated n) throws IOException {
280
281 //add (EQ |@true| blabla )
282 lib.appendI("EQ");
283 lib.appendN(" |@true|");
284
285 genericOp("isAllocated", n);
286
287 lib.reduceI();
288
289 }
290
291 public void visitTEClosedTime(/*@ non_null @*/TEClosedTime n) throws IOException {
292 genericOp("eClosedTime", n);
293 }
294
295 public void visitTFClosedTime(/*@ non_null @*/TFClosedTime n) throws IOException {
296 genericOp("fClosedTime", n);
297 }
298
299 public void visitTAsElems(/*@ non_null @*/TAsElems n) throws IOException {
300 genericOp("asElems", n);
301 }
302
303 public void visitTAsField(/*@ non_null @*/TAsField n) throws IOException {
304 genericOp("asField", n);
305 }
306
307 public void visitTAsLockSet(/*@ non_null @*/TAsLockSet n) throws IOException {
308 genericOp("asLockSet", n);
309 }
310
311 public void visitTArrayLength(/*@ non_null @*/TArrayLength n) throws IOException {
312 }
313
314 public void visitTArrayFresh(/*@ non_null @*/TArrayFresh n) throws IOException {
315 }
316
317 public void visitTArrayShapeOne(/*@ non_null @*/TArrayShapeOne n) throws IOException {
318 }
319
320 public void visitTArrayShapeMore(/*@ non_null @*/TArrayShapeMore n) throws IOException {
321 }
322
323 public void visitTIsNewArray(/*@ non_null @*/TIsNewArray n) throws IOException {
324 }
325
326 public void visitTString(/*@ non_null @*/TString n) throws IOException {
327 }
328
329 public void visitTBoolean(/*@ non_null @*/TBoolean n) throws IOException {
330 if (n.value)
331 lib.append(" |@true|");
332 else
333 lib.append(" |bool$false|");
334 }
335
336 public void visitTChar(/*@ non_null @*/TChar n) throws IOException {
337 lib.appendN(" |C_" + n.value + "|");
338 }
339
340 public void visitTInt(/*@ non_null @*/TInt n) throws IOException {
341 lib.appendN(" " + n.value); //fixme not sure
342 }
343
344 public void visitTFloat(/*@ non_null @*/TFloat n) throws IOException {
345 lib.appendN(" |F_" + n.value + "|");
346 }
347
348 public void visitTDouble(/*@ non_null @*/TDouble n) throws IOException {
349 lib.appendN(" |F_" + n.value + "|"); // fixme
350 }
351
352 public void visitTNull(/*@ non_null @*/TNull n) throws IOException {
353 lib.appendN(" null");
354 }
355
356
357 public void visitTUnset(/*@non_null*/TUnset n) throws IOException {
358 // TODO Auto-generated method stub
359
360 }
361
362
363 public void visitTMethodCall(/*@non_null*/TMethodCall call) throws IOException {
364 // TODO Auto-generated method stub
365
366 }
367
368
369 public void visitTIntegralSub(/*@non_null*/TIntegralSub sub) throws IOException {
370 // TODO Auto-generated method stub
371
372 }
373
374 public void visitTSum(TSum s) {
375 // TODO Auto-generated method stub
376
377 }
378
379 }