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