001 package escjava.vcGeneration.coq;
002
003 import java.lang.StringBuffer;
004 import java.io.*;
005
006 import escjava.vcGeneration.TAllocLE;
007 import escjava.vcGeneration.TAllocLT;
008 import escjava.vcGeneration.TAnyEQ;
009 import escjava.vcGeneration.TAnyNE;
010 import escjava.vcGeneration.TArrayFresh;
011 import escjava.vcGeneration.TArrayLength;
012 import escjava.vcGeneration.TArrayShapeMore;
013 import escjava.vcGeneration.TArrayShapeOne;
014 import escjava.vcGeneration.TAsElems;
015 import escjava.vcGeneration.TAsField;
016 import escjava.vcGeneration.TAsLockSet;
017 import escjava.vcGeneration.TBoolAnd;
018 import escjava.vcGeneration.TBoolEQ;
019 import escjava.vcGeneration.TBoolImplies;
020 import escjava.vcGeneration.TBoolNE;
021 import escjava.vcGeneration.TBoolNot;
022 import escjava.vcGeneration.TBoolOr;
023 import escjava.vcGeneration.TBoolRes;
024 import escjava.vcGeneration.TBoolean;
025 import escjava.vcGeneration.TCast;
026 import escjava.vcGeneration.TChar;
027 import escjava.vcGeneration.TDisplay;
028 import escjava.vcGeneration.TDouble;
029 import escjava.vcGeneration.TEClosedTime;
030 import escjava.vcGeneration.TExist;
031 import escjava.vcGeneration.TFClosedTime;
032 import escjava.vcGeneration.TFloat;
033 import escjava.vcGeneration.TFloatAdd;
034 import escjava.vcGeneration.TFloatDiv;
035 import escjava.vcGeneration.TFloatEQ;
036 import escjava.vcGeneration.TFloatGE;
037 import escjava.vcGeneration.TFloatGT;
038 import escjava.vcGeneration.TFloatLE;
039 import escjava.vcGeneration.TFloatLT;
040 import escjava.vcGeneration.TFloatMod;
041 import escjava.vcGeneration.TFloatMul;
042 import escjava.vcGeneration.TFloatNE;
043 import escjava.vcGeneration.TForAll;
044 import escjava.vcGeneration.TFunction;
045 import escjava.vcGeneration.TInt;
046 import escjava.vcGeneration.TIntegralAdd;
047 import escjava.vcGeneration.TIntegralDiv;
048 import escjava.vcGeneration.TIntegralEQ;
049 import escjava.vcGeneration.TIntegralGE;
050 import escjava.vcGeneration.TIntegralGT;
051 import escjava.vcGeneration.TIntegralLE;
052 import escjava.vcGeneration.TIntegralLT;
053 import escjava.vcGeneration.TIntegralMod;
054 import escjava.vcGeneration.TIntegralMul;
055 import escjava.vcGeneration.TIntegralNE;
056 import escjava.vcGeneration.TIntegralSub;
057 import escjava.vcGeneration.TIs;
058 import escjava.vcGeneration.TIsAllocated;
059 import escjava.vcGeneration.TIsNewArray;
060 import escjava.vcGeneration.TLockLE;
061 import escjava.vcGeneration.TLockLT;
062 import escjava.vcGeneration.TMethodCall;
063 import escjava.vcGeneration.TName;
064 import escjava.vcGeneration.TNode;
065 import escjava.vcGeneration.TNull;
066 import escjava.vcGeneration.TRefEQ;
067 import escjava.vcGeneration.TRefNE;
068 import escjava.vcGeneration.TRoot;
069 import escjava.vcGeneration.TSelect;
070 import escjava.vcGeneration.TStore;
071 import escjava.vcGeneration.TString;
072 import escjava.vcGeneration.TSum;
073 import escjava.vcGeneration.TTypeEQ;
074 import escjava.vcGeneration.TTypeLE;
075 import escjava.vcGeneration.TTypeNE;
076 import escjava.vcGeneration.TTypeOf;
077 import escjava.vcGeneration.TUnset;
078 import escjava.vcGeneration.TVisitor;
079
080 /**
081 * Stolen from the PVS extension.
082 * FIXME: it should be adapted to Coq specific environment.
083 * FIXME: it deletes too much nodes!!!
084 * @author C. Hurlin
085 * @version 14/11/2005
086 */
087 public class TProofSimplifier extends TVisitor {
088
089 TProofSimplifier(Writer out){
090 super(out);
091 }
092
093 /*
094 * Generic functions used by different visit* functions
095 */
096 public void visitTFunction(/*@ non_null @*/ TFunction n) throws IOException {
097
098 int i = 0;
099 int sizeTemp = n.sons.size();
100
101 /* recursive call on the sons */
102 for(; i <= n.sons.size() - 1; ) {
103
104 sizeTemp = n.sons.size();
105 n.getChildAt(i).accept(this);
106
107 /*
108 * If a son have been deleted, do not increase index
109 */
110 if(!(sizeTemp > n.sons.size()))
111 ++i;
112
113 }
114
115 }
116
117 /*
118 * Methods used to simplify the proof
119 */
120 // @ requires indexOfSons >= 0 & indexOfSons <= n.sons.size() - 1;
121 /*@
122 @ requires n.sons.contains(m);
123 @*/
124 public void simplify(/*@ non_null @*/ TBoolRes n, TNode m){
125
126 int i = 0;
127
128 //++
129 if( (i = n.sons.indexOf(m)) == -1)
130 TDisplay.err(this, "simplify(TBoolAnd n, TNode m)","!n.sons.contains(m)");
131 //++
132 else
133 n.sons.remove(i);
134
135 /*
136 * Behavior of simplification process done here.
137 */
138 i = n.sons.size();
139
140 if(i >=2)
141 ; // this node still makes sense, do nothing
142 else {
143
144 if(i == 1) {
145 // check that the remaining node returns a boolean
146
147 //++
148 if(! (n.getChildAt(0) instanceof TBoolRes))
149 TDisplay.err(this, "simplify(TBoolRes n, TNode m)", "Remaining child does not return a boolean, continuing anyway...");
150 //++
151
152 /*
153 this piece of code delete the BoolAnd node and add the sons
154 to its parent.
155 ie changing x -> n -> m to x -> m
156 */
157 simplify(n.parent, n, m);
158 }
159
160 }
161
162 }
163
164 /*
165 * Node m is replaced by o in the list of sons of n.
166 * Note that after the operation, \old(n.indexOf(m)) == n.indexOf(o);
167 */
168 // @ requires m.sons.contains(o);
169 // @ ensures \old(n.indexOf(m)) == n.indexOf(o);
170 /*@
171 @ requires n.sons.contains(m);
172 @ ensures n.sons.contains(o);
173 @ ensures !n.sons.contains(m);
174 @*/
175 public void simplify(TFunction n, TNode m, TNode o){
176
177 int i = n.sons.indexOf(m);
178
179 //++
180 if(i == -1)
181 TDisplay.err(this, "simplify(TFunction n, TNode m, TNode o)", "!n.contiains(m)");
182 //++
183
184 n.sons.setElementAt(o, i);
185 }
186
187 /*
188 * non automatic generated class
189 */
190 public void visitTName(/*@ non_null @*/ TName n) throws IOException{
191 }
192
193 public void visitTRoot(/*@ non_null @*/ TRoot n) throws IOException{
194 /* add all the sons */
195 for(int i = 0; i <= n.sons.size() - 1; i++){
196
197 /* recursive call on the sons */
198 n.getChildAt(i).accept(this);
199 }
200 }
201
202 /*
203 * class created using the perl script
204 */
205 public void visitTBoolImplies(/*@ non_null @*/ TBoolImplies n) throws IOException{
206 visitTFunction(n);
207 }
208
209 public void visitTBoolAnd(/*@ non_null @*/ TBoolAnd n) throws IOException{
210 visitTFunction(n);
211 }
212
213 public void visitTBoolOr(/*@ non_null @*/ TBoolOr n) throws IOException{
214 visitTFunction(n);
215 }
216
217 public void visitTBoolNot(/*@ non_null @*/ TBoolNot n) throws IOException{
218 visitTFunction(n);
219 }
220
221 public void visitTBoolEQ(/*@ non_null @*/ TBoolEQ n) throws IOException{
222 visitTFunction(n);
223 }
224
225 public void visitTBoolNE(/*@ non_null @*/ TBoolNE n) throws IOException{
226 visitTFunction(n);
227 }
228
229 public void visitTAllocLT(/*@ non_null @*/ TAllocLT n) throws IOException{
230 visitTFunction(n);
231 }
232
233 public void visitTAllocLE(/*@ non_null @*/ TAllocLE n) throws IOException{
234 visitTFunction(n);
235 }
236
237 public void visitTAnyEQ(/*@ non_null @*/ TAnyEQ n) throws IOException{
238 visitTFunction(n);
239 }
240
241 public void visitTAnyNE(/*@ non_null @*/ TAnyNE n) throws IOException{
242 visitTFunction(n);
243 }
244
245 public void visitTIntegralEQ(/*@ non_null @*/ TIntegralEQ n) throws IOException{
246 visitTFunction(n);
247 }
248
249 public void visitTIntegralGE(/*@ non_null @*/ TIntegralGE n) throws IOException{
250 visitTFunction(n);
251 }
252
253 public void visitTIntegralGT(/*@ non_null @*/ TIntegralGT n) throws IOException{
254 visitTFunction(n);
255 }
256
257 public void visitTIntegralLE(/*@ non_null @*/ TIntegralLE n) throws IOException{
258 visitTFunction(n);
259 }
260
261 public void visitTIntegralLT(/*@ non_null @*/ TIntegralLT n) throws IOException{
262 visitTFunction(n);
263 }
264
265 public void visitTIntegralNE(/*@ non_null @*/ TIntegralNE n) throws IOException{
266 visitTFunction(n);
267 }
268
269 public void visitTIntegralAdd(/*@ non_null @*/ TIntegralAdd n) throws IOException{
270 visitTFunction(n);
271 }
272
273 public void visitTIntegralDiv(/*@ non_null @*/ TIntegralDiv n) throws IOException{
274 visitTFunction(n);
275 }
276
277 public void visitTIntegralMod(/*@ non_null @*/ TIntegralMod n) throws IOException{
278 visitTFunction(n);
279 }
280
281 public void visitTIntegralMul(/*@ non_null @*/ TIntegralMul n) throws IOException{
282 visitTFunction(n);
283 }
284
285 public void visitTFloatEQ(/*@ non_null @*/ TFloatEQ n) throws IOException{
286 visitTFunction(n);
287 }
288
289 public void visitTFloatGE(/*@ non_null @*/ TFloatGE n) throws IOException{
290 visitTFunction(n);
291 }
292
293 public void visitTFloatGT(/*@ non_null @*/ TFloatGT n) throws IOException{
294 visitTFunction(n);
295 }
296
297 public void visitTFloatLE(/*@ non_null @*/ TFloatLE n) throws IOException{
298 visitTFunction(n);
299 }
300
301 public void visitTFloatLT(/*@ non_null @*/ TFloatLT n) throws IOException{
302 visitTFunction(n);
303 }
304
305 public void visitTFloatNE(/*@ non_null @*/ TFloatNE n) throws IOException{
306 visitTFunction(n);
307 }
308
309 public void visitTFloatAdd(/*@ non_null @*/ TFloatAdd n) throws IOException{
310 visitTFunction(n);
311 }
312
313 public void visitTFloatDiv(/*@ non_null @*/ TFloatDiv n) throws IOException{
314 visitTFunction(n);
315 }
316
317 public void visitTFloatMod(/*@ non_null @*/ TFloatMod n) throws IOException{
318 visitTFunction(n);
319 }
320
321 public void visitTFloatMul(/*@ non_null @*/ TFloatMul n) throws IOException{
322 visitTFunction(n);
323 }
324
325 public void visitTLockLE(/*@ non_null @*/ TLockLE n) throws IOException{
326 visitTFunction(n);
327 }
328
329 public void visitTLockLT(/*@ non_null @*/ TLockLT n) throws IOException{
330 visitTFunction(n);
331 }
332
333 public void visitTRefEQ(/*@ non_null @*/ TRefEQ n) throws IOException{
334 visitTFunction(n);
335 }
336
337 public void visitTRefNE(/*@ non_null @*/ TRefNE n) throws IOException{
338 visitTFunction(n);
339 }
340
341 public void visitTTypeEQ(/*@ non_null @*/ TTypeEQ n) throws IOException{
342 visitTFunction(n);
343 }
344
345 public void visitTTypeNE(/*@ non_null @*/ TTypeNE n) throws IOException{
346 visitTFunction(n);
347 }
348
349 public void visitTTypeLE(/*@ non_null @*/ TTypeLE n) throws IOException{
350 visitTFunction(n);
351 }
352
353 public void visitTCast(/*@ non_null @*/ TCast n) throws IOException{
354 visitTFunction(n);
355 }
356
357 public void visitTIs(/*@ non_null @*/ TIs n) throws IOException{
358
359 if(n.parent instanceof TBoolRes) {
360 TBoolRes nTemp = (TBoolRes) n.parent;
361 simplify(nTemp, n);
362 }
363 else
364 TDisplay.err(this, "visitTIs", "TIs node has a parent which type is != from TBoolRes");
365
366 }
367
368 public void visitTSelect(/*@ non_null @*/ TSelect n) throws IOException{
369 visitTFunction(n);
370 }
371
372 public void visitTStore(/*@ non_null @*/ TStore n) throws IOException{
373 visitTFunction(n);
374 }
375
376 public void visitTTypeOf(/*@ non_null @*/ TTypeOf n) throws IOException{
377 visitTFunction(n);
378 }
379
380 public void visitTForAll(/*@ non_null @*/ TForAll n) throws IOException{
381
382 // if(n.parent instanceof TBoolRes) {
383 // TBoolRes nTemp = (TBoolRes) n.parent;
384 // simplify(nTemp, n);
385 // }
386 // else
387 // TDisplay.err(this, "visitTForAll", "TIs node has a parent which type is != from TBoolRes");
388
389 }
390
391 public void visitTExist(/*@ non_null @*/ TExist n) throws IOException{
392
393 // if(n.parent instanceof TBoolRes) {
394 // TBoolRes nTemp = (TBoolRes) n.parent;
395 // simplify(nTemp, n);
396 // }
397 // else
398 // TDisplay.err(this, "visitTExist", "TIs node has a parent which type is != from TBoolRes");
399
400 }
401
402 public void visitTIsAllocated(/*@ non_null @*/ TIsAllocated n) throws IOException{
403 visitTFunction(n);
404 }
405
406 public void visitTEClosedTime(/*@ non_null @*/ TEClosedTime n) throws IOException{
407 visitTFunction(n);
408 }
409
410 public void visitTFClosedTime(/*@ non_null @*/ TFClosedTime n) throws IOException{
411 visitTFunction(n);
412 }
413
414 public void visitTAsElems(/*@ non_null @*/ TAsElems n) throws IOException{
415 visitTFunction(n);
416 }
417
418 public void visitTAsField(/*@ non_null @*/ TAsField n) throws IOException{
419 visitTFunction(n);
420 }
421
422 public void visitTAsLockSet(/*@ non_null @*/ TAsLockSet n) throws IOException{
423 visitTFunction(n);
424 }
425
426 public void visitTArrayLength(/*@ non_null @*/ TArrayLength n) throws IOException{
427 visitTFunction(n);
428 }
429
430 public void visitTArrayFresh(/*@ non_null @*/ TArrayFresh n) throws IOException{
431 visitTFunction(n);
432 }
433
434 public void visitTArrayShapeOne(/*@ non_null @*/ TArrayShapeOne n) throws IOException{
435 visitTFunction(n);
436 }
437
438 public void visitTArrayShapeMore(/*@ non_null @*/ TArrayShapeMore n) throws IOException{
439 visitTFunction(n);
440 }
441
442 public void visitTIsNewArray(/*@ non_null @*/ TIsNewArray n) throws IOException{
443 visitTFunction(n);
444 }
445
446 public void visitTString(/*@ non_null @*/ TString n) throws IOException{}
447
448 public void visitTBoolean(/*@ non_null @*/ TBoolean n) throws IOException{
449
450 if(n.parent instanceof TBoolRes) {
451 TBoolRes nTemp = (TBoolRes) n.parent;
452 simplify(nTemp, n);
453 }
454 else
455 TDisplay.err(this, "visitTBoolean", "TIs node has a parent which type is != from TBoolRes");
456
457 }
458
459 public void visitTChar(/*@ non_null @*/ TChar n) throws IOException{}
460 public void visitTInt(/*@ non_null @*/ TInt n) throws IOException{}
461 public void visitTFloat(/*@ non_null @*/ TFloat n) throws IOException{}
462 public void visitTDouble(/*@ non_null @*/ TDouble n) throws IOException{}
463 public void visitTNull(/*@ non_null @*/ TNull n) throws IOException{}
464
465 public void visitTMethodCall(/*@non_null*/TMethodCall call) throws IOException {}
466
467 public void visitTUnset(/*@non_null*/TUnset n) throws IOException {
468 // TODO Auto-generated method stub
469
470 }
471
472 public void visitTIntegralSub(/*@non_null*/TIntegralSub sub) throws IOException {
473 // TODO Auto-generated method stub
474
475 }
476
477 public void visitTSum(TSum s) {
478 // TODO Auto-generated method stub
479
480 }
481
482 }