001    /* $Id: StandardPrettyPrint.java,v 1.14 2006/08/05 16:58:04 chalin Exp $
002     * Copyright 2000, 2001, Compaq Computer Corporation .
003     * Copyright 2006, DSRG, Concordia University and others.
004     */
005    
006    package javafe.ast;
007    
008    import java.io.OutputStream;
009    import java.io.ByteArrayOutputStream;
010    import java.io.IOException;
011    import javafe.util.Assert;
012    import javafe.util.Location;
013    
014    public class StandardPrettyPrint extends PrettyPrint {
015    
016        //@ ensures this.self == this;
017        public StandardPrettyPrint() { }
018    
019      //@ ensures this.self == self;
020        public StandardPrettyPrint(/*@ non_null */ PrettyPrint self) { super(self); }
021    
022        public void print(/*@non_null*/OutputStream o, /*@ nullable */ CompilationUnit cu) {
023            if (cu == null) {
024                writeln(o, "<null CompilationUnit>");
025                return;
026            }
027            if (cu.lexicalPragmas != null) {
028                for (int i = 0; i < cu.lexicalPragmas.size(); i++)
029                    self.print(o, cu.lexicalPragmas.elementAt(i));
030                writeln(o);
031            }
032            if (cu.pkgName != null) {
033                write(o, "package "); self.print(o, cu.pkgName); writeln(o, ";");
034                writeln(o);
035            }
036            if (cu.imports.size() > 0) {
037                for(int j=0; j<cu.imports.size(); j++) {
038                    ImportDecl i = cu.imports.elementAt(j);
039                    write(o, "import ");
040                    if (i instanceof SingleTypeImportDecl)
041                        self.print(o, ((SingleTypeImportDecl)i).typeName);
042                    else {
043                        self.print(o, ((OnDemandImportDecl)i).pkgName);     //@ nowarn Cast;
044                        write(o, ".*");
045                    }
046                    writeln(o, ";");
047                }
048                writeln(o);
049            }
050            for(int j=0; j<cu.elems.size(); j++) {
051                self.print(o, 0, cu.elems.elementAt(j));
052                writeln(o);
053            }
054            for (int j=0; j<cu.otherPragmas.size(); ++j) {
055                TypeDeclElemPragma tde = (TypeDeclElemPragma)cu.otherPragmas.elementAt(j);
056                self.print(o, 0, tde);
057            }
058        }
059    
060        public void printnoln(/*@non_null*/OutputStream o, int ind, TypeDecl d) {
061            if (d == null) {
062                write(o, "<null TypeDecl>");
063                return;
064            }
065    
066            if (d.specOnly) {
067                writeln(o);
068                spaces(o, ind);
069                writeln(o, "/* Only specification information is available for "
070                        + "this type */");
071                writeln(o);
072                spaces(o, ind);
073            }
074            
075            if (d.pmodifiers != null)
076                for (int i = 0; i < d.pmodifiers.size(); i++) {
077                    self.print(o, ind, d.pmodifiers.elementAt(i));
078                    writeln(o);
079                    spaces(o, ind);
080                }
081            String mod = Modifiers.toString(d.modifiers);
082            if (!mod.equals("")) {
083                writeln(o, mod);
084                spaces(o, ind);
085            }
086    
087            Identifier id;
088    
089            switch (d.getTag()) {
090          
091                case TagConstants.CLASSDECL:
092                    {
093                        ClassDecl cd = (ClassDecl)d;
094                        writeln(o, "class "+(id=cd.id));
095                        if (cd.superClass != null) {
096                            if (!toString(cd.superClass).equals("java.lang.Object")
097                                || PrettyPrint.displayInferred) {
098                                spaces(o, ind);
099                                write(o, "extends ");
100                                self.print(o, cd.superClass);
101                                writeln(o);
102                            }
103                        }
104                        if (cd.superInterfaces.size() != 0) {
105                            spaces(o, ind);
106                            write(o, "implements ");
107                            self.print(o, cd.superInterfaces);
108                            writeln(o);
109                        }
110                        break;
111                    }
112          
113                case TagConstants.INTERFACEDECL:
114                    {
115                        InterfaceDecl cd = (InterfaceDecl)d;
116                        writeln(o, "interface "+(id=cd.id));
117                        if (cd.superInterfaces.size() != 0) {
118                            spaces(o, ind);
119                            write(o, "extends ");
120                            self.print(o, cd.superInterfaces);
121                            writeln(o,"");
122                        }
123                        break;
124                    }
125    
126                default:
127                    spaces(o, ind);
128                    writeln(o, unknownTag(d));
129                    id = Identifier.intern("?");
130            }
131    
132            spaces(o, ind);
133            writeln(o, "{");
134            for (int i = 0; i < d.elems.size(); i++) {
135                TypeDeclElem elem = d.elems.elementAt(i);
136                //@ assume elem.hasParent ;  // "invariant"
137                spaces(o, ind+INDENT);
138                self.print(o, ind+INDENT, elem, id, true);
139                if (i != d.elems.size()-1) writeln(o);
140            }
141            spaces(o, ind);
142            write(o, "}");
143        }
144    
145        public void print(/*@non_null*/OutputStream o, int ind, Stmt s) {
146            if (s == null) {
147                writeln(o, "<null Stmt>");
148                return;
149            }
150    
151            switch (s.getTag()) {
152          
153                case TagConstants.RETURNSTMT: 
154                    {
155                        ReturnStmt r = (ReturnStmt)s;
156                        if (r.expr == null)
157                            write(o, "return;");
158                        else {
159                            write(o, "return ");
160                            self.print(o, ind, r.expr);
161                            write(o, ';');
162                        }
163                        return;
164                    }
165          
166                case TagConstants.THROWSTMT: 
167                    {
168                        ThrowStmt t = (ThrowStmt)s;
169                        write(o, "throw "); self.print(o, ind, t.expr); write(o, ';');
170                        return;
171                    }
172          
173                case TagConstants.ASSERTSTMT: {
174                    AssertStmt a = (AssertStmt)s;
175                    write(o, "assert "); self.print(o, ind, a.pred); //write(o, ")");
176                    if (a.label != null) {
177                        write(o, " : ");
178                        self.print(o, ind, a.label);
179                    }
180                    write(o, ";");
181                    return;
182                }
183          
184                case TagConstants.SWITCHSTMT: 
185                    {
186                        SwitchStmt c = (SwitchStmt)s;
187                        write(o, "switch ("); self.print(o, ind, c.expr); write(o, ") ");
188                        // Fall through
189                    }
190    
191                case TagConstants.BLOCKSTMT: 
192                    {
193                        GenericBlockStmt b = (GenericBlockStmt)s;
194                        int nextInd = ind + INDENT;
195                        writeln(o, "{");
196                        boolean lastWasLabel = false;
197                        for(int i = 0; i < b.stmts.size(); i++) {
198                            Stmt sub = b.stmts.elementAt(i);
199                            if (sub.getTag() == TagConstants.SWITCHLABEL) {
200                                SwitchLabel x = (SwitchLabel)sub;
201                                if (x.expr == null && sub.getStartLoc() == b.locCloseBrace) {
202                                    // this is an implicit "default: break;" statement
203                                    Assert.notFalse(i == b.stmts.size() - 2); //@ nowarn Pre;
204                                    // don't print this statement or the next, which should be
205                                    // a "break"
206                                    Assert.notFalse(b.stmts.elementAt(i+1).getTag() //@ nowarn Pre;
207                                                    == TagConstants.BREAKSTMT);
208                                    if (!PrettyPrint.displayInferred)
209                                        break;
210                                }
211                                if (i != 0 && ! lastWasLabel) writeln(o);
212                                if (x.expr == null) { spaces(o, ind); writeln(o, "default:"); }
213                                else {
214                                    spaces(o, ind);
215                                    write(o, "case ");
216                                    self.print(o, ind, x.expr);
217                                    writeln(o, ":");
218                                }
219                                lastWasLabel = true;
220                            } else {
221                                spaces(o, nextInd);
222                                self.print(o, nextInd, sub);
223                                writeln(o);
224                                lastWasLabel = false;
225                            }
226                        }
227                        spaces(o, ind);
228                        write(o, '}');
229                        return;
230                    }
231          
232                case TagConstants.WHILESTMT: 
233                    {
234                        WhileStmt w = (WhileStmt)s;
235                        write(o, "while ("); self.print(o, ind, w.expr); write(o, ") ");
236                        self.print(o, ind, w.stmt);
237                        return;
238                    }
239          
240                case TagConstants.DOSTMT: 
241                    {
242                        DoStmt d = (DoStmt)s;
243                        write(o, "do ");
244                        self.print(o, ind, d.stmt);
245                        write(o, " while ("); self.print(o, ind, d.expr); write(o, ");");
246                        return;
247                    }
248          
249                case TagConstants.IFSTMT: 
250                    {
251                        IfStmt i = (IfStmt)s;
252                        write(o, "if ("); self.print(o, ind, i.expr); write(o, ") ");
253                        self.print(o, ind, i.thn);
254                        if (! (i.els.getTag() == TagConstants.SKIPSTMT)) {
255                            write(o, '\n');
256                            spaces(o, ind); write(o, "else "); self.print(o, ind, i.els);
257                        }
258                        return;
259                    }
260          
261                case TagConstants.BREAKSTMT: 
262                    {
263                        BreakStmt b = (BreakStmt)s;
264                        if (b.label == null) write(o, "break;");
265                        else {
266                            write(o, "break ");
267                            write(o, b.label.toString());
268                            write(o, ';');
269                        }
270                        return;
271                    }
272          
273                case TagConstants.CONTINUESTMT: 
274                    {
275                        ContinueStmt c = (ContinueStmt)s;
276                        if (c.label == null) write(o, "continue;");
277                        else {
278                            write(o, "continue ");
279                            write(o, c.label.toString());
280                            write(o, ';');
281                        }
282                        return;
283                    }
284          
285                case TagConstants.SYNCHRONIZESTMT: 
286                    {
287                        SynchronizeStmt x = (SynchronizeStmt)s;
288                        if (x.stmt.getTag() == TagConstants.BLOCKSTMT) {
289                            write(o, "synchronized (");
290                            self.print(o, ind, x.expr);
291                            write(o, ") ");
292                            self.print(o, ind, x.stmt);
293                        } else {
294                            write(o, "synchronized (");
295                            self.print(o, ind, x.expr);
296                            write(o, ") {\n");
297                            spaces(o, ind+INDENT);
298                            self.print(o, ind+INDENT, x.stmt);
299                            spaces(o, ind);
300                            write(o, '}');
301                        }
302                        return;
303                    }
304          
305                case TagConstants.EVALSTMT: 
306                    {
307                        EvalStmt x = (EvalStmt)s;
308                        self.print(o, ind, x.expr); write(o, ';');
309                        return;
310                    }
311          
312                case TagConstants.LABELSTMT: 
313                    {
314                        LabelStmt x = (LabelStmt)s;
315                        write(o, x.label.toString());
316                        write(o, ": ");
317                        self.print(o, ind, x.stmt);
318                        return;
319                    }
320          
321                case TagConstants.SKIPSTMT: 
322                    write(o, ';');
323                    return;
324          
325                case TagConstants.TRYFINALLYSTMT: 
326                    {
327                        TryFinallyStmt x = (TryFinallyStmt)s;
328                        if (x.tryClause.getTag() == TagConstants.TRYCATCHSTMT)
329                            self.print(o, ind, x.tryClause);
330                        else if (x.tryClause instanceof BlockStmt) {
331                            write(o, "try ");
332                            self.print(o, ind, x.tryClause);
333                        } else {
334                            write(o, "try {\b");
335                            spaces(o, ind);
336                            self.print(o, ind+INDENT, x.tryClause);
337                            spaces(o, ind);
338                            write(o, '}');
339                        }
340            
341                        if (x.finallyClause.getTag() == TagConstants.BLOCKSTMT) {
342                            write(o, " finally ");
343                            self.print(o, ind, x.finallyClause);
344                        } else {
345                            write(o, " finally {\n");
346                            spaces(o, ind);
347                            self.print(o, ind+INDENT, x.finallyClause);
348                            spaces(o, ind);
349                            write(o, '}');
350                        }
351                        return;
352                    }
353          
354                case TagConstants.TRYCATCHSTMT: 
355                    {
356                        TryCatchStmt x = (TryCatchStmt)s;
357                        if (x.tryClause.getTag() == TagConstants.BLOCKSTMT) {
358                            write(o, "try ");
359                            self.print(o, ind, x.tryClause);
360                        } else {
361                            write(o, "try {\n");
362                            spaces(o, ind+INDENT);
363                            self.print(o, ind+INDENT, x.tryClause);
364                            spaces(o, ind);
365                            write(o, '}');
366                        }
367            
368                        for(int i = 0; i < x.catchClauses.size(); i++) {
369                            CatchClause c = x.catchClauses.elementAt(i);
370                            write(o, " catch ("); self.print(o, c.arg); write(o, ") ");
371                            self.print(o, ind, c.body);
372                        }
373                        return;
374                    }
375          
376                case TagConstants.CLASSDECLSTMT: 
377                    {
378                        ClassDecl x = ((ClassDeclStmt)s).decl;
379                        self.printnoln(o, ind, x);
380                        return;
381                    }
382          
383                case TagConstants.VARDECLSTMT: 
384                    {
385                        LocalVarDecl x = ((VarDeclStmt)s).decl;
386                        self.print(o, ind, x, true);
387                        return;
388                    }
389          
390                case TagConstants.FORSTMT: 
391                    {
392                        ForStmt x = (ForStmt)s;
393                        write(o, "for (");
394            
395                        if (x.forInit.size() > 0)
396                            if (x.forInit.elementAt(0).getTag() == TagConstants.VARDECLSTMT) {
397                                self.print(o, ((VarDeclStmt)x.forInit.elementAt(0))//@nowarn Cast;
398                                           .decl.type);
399                                write(o, ' ');
400                                for(int i = 0; i < x.forInit.size(); i++) {
401                                    VarDeclStmt d = (VarDeclStmt)x.forInit.elementAt(i); //@nowarn Cast;
402                                    write(o, d.decl.id.toString());
403                                    if (d.decl.init != null) {
404                                        write(o, '=');
405                                        self.print(o, ind, d.decl.init);
406                                    }
407                                    if (i+1 < x.forInit.size()) write(o, ", ");
408                                }
409                            } else
410                                for(int i = 0; i < x.forInit.size(); i++) {
411                                    EvalStmt e = (EvalStmt) x.forInit.elementAt(i); //@nowarn Cast;
412                                    self.print(o, ind, e.expr);
413                                    if (i+1 < x.forInit.size()) write(o, ", ");
414                                }
415                        write(o, "; ");
416                        self.print(o, ind, x.test);
417                        write(o, "; ");
418                        for(int i = 0; i < x.forUpdate.size(); i++) {
419                            self.print(o, ind, x.forUpdate.elementAt(i));
420                            if (i+1 < x.forUpdate.size()) write(o, ", ");
421                        }
422                        write(o, ") ");
423                        self.print(o, ind, x.body);
424                        return;
425                    }
426          
427                case TagConstants.CONSTRUCTORINVOCATION: {
428                    ConstructorInvocation x = (ConstructorInvocation)s;
429                    if (x.enclosingInstance != null) {
430                        if (!(x.enclosingInstance instanceof ThisExpr) ||
431                            !(((ThisExpr)x.enclosingInstance).inferred) ||
432                            PrettyPrint.displayInferred) {
433                            self.print(o, ind, x.enclosingInstance);
434                            write(o, ".");
435                        }
436                    }
437                    write(o, (x.superCall ? "super" : "this"));
438                    self.print(o, ind, x.args);
439                    write(o, ';');
440                    return;
441                }
442    
443                case TagConstants.SWITCHLABEL: {
444                    /*
445                     * This case never happens unless a client directly calls us on
446                     * a SwitchLabel; normally block and switch statements handle
447                     * switch labels directly for better formating (multiple
448                     * cases/line).
449                     */
450                    SwitchLabel x = (SwitchLabel)s;
451    
452                    if (x.expr == null)
453                        writeln(o, "default:");
454                    else {
455                        write(o, "case ");
456                        self.print(o, ind, x.expr);
457                        writeln(o, ":");
458                    }
459                    return;
460                }
461    
462                default:
463                    if (s instanceof StmtPragma)
464                        self.print(o, ind, (StmtPragma)s);
465                    else write(o, unknownTag(s));
466                    return;
467            }
468        }
469    
470        public void print(/*@non_null*/OutputStream o, 
471                          int ind, 
472                          /*@ nullable */ TypeDeclElem d, 
473                          /*@ non_null */ Identifier classId, 
474                          boolean showBody) 
475        {
476            if (d == null) {
477                writeln(o, "<null TypeDeclElem>");
478                return;
479            }
480            switch( d.getTag() ) {
481          
482                case TagConstants.FIELDDECL:
483                    self.print(o, ind, (FieldDecl)d, showBody); writeln(o);
484                    break;
485    
486                case TagConstants.INITBLOCK:
487                    {
488                        if (showBody) {
489                            InitBlock si = (InitBlock)d;
490                            write(o, Modifiers.toString(si.modifiers));
491                            if (si.pmodifiers != null)
492                                for (int i = 0; i < si.pmodifiers.size(); i++) {
493                                    write(o, ' ');
494                                    self.print(o, ind, si.pmodifiers.elementAt(i));
495                                }
496                            self.print(o, ind, si.block);
497                            writeln(o);
498                        }
499                        break;
500                    }
501    
502                case TagConstants.METHODDECL:
503                    {
504                        MethodDecl md = (MethodDecl)d;
505            
506                        if (md.id.toString().equals("<clinit>")) {
507                            break;
508                        }
509            
510                        write(o, Modifiers.toString(md.modifiers));
511                        self.print(o, md.returnType);
512                        write(o, ' ');
513                        write(o, md.id.toString());
514                        self.print(o, ind, md.args);
515                        if (md.raises.size() != 0)
516                        { write(o, " throws "); self.print(o, md.raises); }
517                        if (md.pmodifiers != null) {
518                            for (int i = 0; i < md.pmodifiers.size(); i++) {
519                                writeln(o);
520                                spaces(o, ind+1);
521                                self.print(o, ind, md.pmodifiers.elementAt(i));
522                            }
523                            write(o, ' ');
524                        }
525                        displayBody(o,ind, md.body, showBody,
526                                    d.getParent().specOnly,
527                                    "method");
528                        break;
529                    }
530            
531                case TagConstants.CONSTRUCTORDECL:
532                    {
533                        ConstructorDecl md = (ConstructorDecl)d;
534    
535                        // Don't print default constructors:
536                        if (md.implicit && !PrettyPrint.displayInferred) {
537                            // need to at least do a <newline> here!
538                            writeln(o, "// <default constructor>");
539                            break;
540                        }
541    
542                        write(o, Modifiers.toString(md.modifiers));
543                        write(o, classId.toString());
544                        self.print(o, ind, md.args);
545                        if (md.raises.size() != 0)
546                        { write(o, " throws "); self.print(o, md.raises); }
547                        if (md.pmodifiers != null) {
548                            for (int i = 0; i < md.pmodifiers.size(); i++) {
549                                writeln(o);
550                                spaces(o, ind+1);
551                                self.print(o, ind, md.pmodifiers.elementAt(i));
552                            }
553                            write(o, ' ');
554                        }
555    
556                        displayBody(o, ind, md.body, showBody,
557                                    d.getParent().specOnly,
558                                    "constructor");
559                        break;
560                    }
561    
562                case TagConstants.CLASSDECL:
563                case TagConstants.INTERFACEDECL:
564                    {
565                        self.print(o, ind, (TypeDecl)d);
566                        break;
567                    }
568    
569                default:
570                    if (d instanceof TypeDeclElemPragma)
571                        self.print(o, ind, (TypeDeclElemPragma)d);
572                    else writeln(o, unknownTagMsg(d.getTag()));
573                    break;
574            }
575        }
576    
577    
578        //@ requires o != null;
579        void displayBody(/*@non_null*/OutputStream o, int ind, BlockStmt body,
580                         boolean showBody, boolean specOnly, String kind) {
581            if (!showBody || body==null) {
582                writeln(o, ";");
583                return;
584            }
585    
586            writeln(o);
587            spaces(o, ind);
588    
589            if (specOnly) {
590                writeln(o,"{");
591                spaces(o, ind);
592                writeln(o, "  /* " + kind + " body unavailable */");
593                spaces(o, ind);
594                writeln(o,"}");
595            } else {
596                self.print(o, ind, body);
597                writeln(o);
598            }
599        }
600    
601         
602        public void print(/*@non_null*/OutputStream o, TypeNameVec tns) {
603            if (tns == null) write(o, "<null TypeNameVec>");
604            else
605                for( int i=0; i<tns.size(); i++ ) {
606                    if (i != 0) write(o, ", ");
607                    self.print(o, tns.elementAt(i));
608                }
609        }
610    
611        public void print(/*@non_null*/OutputStream o, int ind, FormalParaDeclVec fps) {
612            if (fps == null) write(o, "<null FormalParaDeclVec>");
613            else {
614                write(o, '(');
615                for (int i=0; i<fps.size(); i++) {
616                    if (i != 0) write(o, ", ");
617    
618                    FormalParaDecl d = fps.elementAt(i);
619                    write(o, Modifiers.toString(d.modifiers));
620                    self.print(o, d);
621                    if (d.pmodifiers != null)
622                        for (int j = 0; j < d.pmodifiers.size(); j++) {
623                            write(o, ' ');
624                            self.print(o, ind, d.pmodifiers.elementAt(j));
625                        }
626                }
627                write(o, ')');
628            }
629        }
630    
631        public void print(/*@non_null*/OutputStream o, int ind, ExprVec es) {
632            if (es == null) write(o, "<null ExprVec>");
633            else {
634                write(o, '(');
635                for (int i = 0; i < es.size(); i++) {
636                    if (i != 0) write(o, ", ");
637                    self.print(o, ind, es.elementAt(i));
638                }
639                write(o, ')');
640            }
641        }
642    
643        public void print(/*@non_null*/OutputStream o, GenericVarDecl d) {
644            if (d == null) write(o, "<null GenericVarDecl>");
645            else {
646                self.print(o, d.type);
647                write(o, ' ');
648                write(o, d.id.toString());
649            }
650        }
651      
652        public void print(/*@non_null*/OutputStream o, int ind, LocalVarDecl d,
653                          boolean showBody) {
654            if (d == null) write(o, "<null VarDecl>");
655            else {
656                write(o, Modifiers.toString(d.modifiers));
657                self.print(o, d.type);
658                write(o, ' ');
659                write(o, d.id.toString());
660                if (showBody && d.init != null)
661                { write(o, " = "); self.print(o, ind, d.init); }
662                if (d.pmodifiers != null)
663                    for (int i = 0; i < d.pmodifiers.size(); i++) {
664                        write(o, ' ');
665                        self.print(o, ind, d.pmodifiers.elementAt(i));
666                    }
667                write(o, ';');
668            }
669        }
670      
671        public void print(/*@non_null*/OutputStream o, int ind, FieldDecl d, boolean showBody) {
672            if (d == null) write(o, "<null VarDecl>");
673            else {
674                boolean specOnly = d.getParent().specOnly;
675    
676                write(o, Modifiers.toString(d.modifiers));
677                self.print(o, d.type);
678                write(o, ' ');
679                write(o, d.id.toString());
680                if (showBody && d.init != null && !specOnly)
681                { write(o, " = "); self.print(o, ind, d.init); }
682                if (d.pmodifiers != null)
683                    for (int i = 0; i < d.pmodifiers.size(); i++) {
684                        write(o, ' ');
685                        self.print(o, ind, d.pmodifiers.elementAt(i));
686                    }
687                write(o, ';');
688            }
689        }
690      
691        public void print(/*@non_null*/OutputStream o, /*@ non_null */ Type t) {
692            if (t == null) { write(o, "<null Type>"); return; }
693            switch (t.getTag()) {
694                case TagConstants.BOOLEANTYPE: write(o, "boolean"); break;
695                case TagConstants.BYTETYPE: write(o, "byte"); break;
696                case TagConstants.ERRORTYPE: write(o, "error"); break;
697                case TagConstants.SHORTTYPE: write(o, "short"); break;
698                case TagConstants.INTTYPE: write(o, "int"); break;
699                case TagConstants.LONGTYPE: write(o, "long"); break;
700                case TagConstants.CHARTYPE: write(o, "char"); break;
701                case TagConstants.FLOATTYPE: write(o, "float"); break;
702                case TagConstants.DOUBLETYPE: write(o, "double"); break;
703                case TagConstants.VOIDTYPE: write(o, "void"); break;
704                case TagConstants.NULLTYPE: write(o, "null"); break;
705                case TagConstants.TYPENAME:
706                    self.print(o, ((TypeName)t).name); break;
707                case TagConstants.ARRAYTYPE:
708                    self.print(o, ((ArrayType)t).elemType); write(o, "[");
709                    write(o,"]");
710                    break;
711                default:
712                    write(o, t.toString() );
713                    break;
714            }
715            print(o, 2, t.tmodifiers);
716        }
717      
718        public void print(/*@non_null*/OutputStream o, Name n) {
719            if (n == null) write(o, "<null Name>");
720            else write(o, n.printName());
721        }
722      
723        static public void println(VarInit e) {
724            inst.print(System.out,0,e);
725            System.out.println("");
726        }
727    
728        public void print(/*@non_null*/OutputStream o, int ind, VarInit e) {
729            if (e == null) {
730                write(o, "<null expression>");
731                return;
732            }
733    
734            int eTag = e.getTag();
735            switch (eTag) {
736          
737                case TagConstants.ARRAYINIT: 
738                    {
739                        VarInitVec v = ((ArrayInit)e).elems;
740                        write(o, "{ ");
741                        for(int i = 0; i < v.size(); i++) {
742                            if (i != 0 ) write(o, ", ");
743                            self.print(o, ind, v.elementAt(i));
744                        }
745                        write(o, " }");
746                        return;
747                    }
748                        
749                case TagConstants.THISEXPR: {
750                    ThisExpr t = (ThisExpr)e;
751                    if (t.classPrefix != null) {
752                        self.print(o, t.classPrefix);
753                        write(o, ".");
754                    }
755                    write(o, "this");
756                    return;
757                }
758    
759                    // Literals
760                case TagConstants.BOOLEANLIT: 
761                case TagConstants.STRINGLIT:
762                case TagConstants.CHARLIT:
763                case TagConstants.DOUBLELIT: 
764                case TagConstants.FLOATLIT:
765                case TagConstants.INTLIT:
766                case TagConstants.LONGLIT:
767                    write(o, toCanonicalString(eTag, ((LiteralExpr)e).value));
768                    return;
769    
770                case TagConstants.NULLLIT:
771                    write(o, "null");
772                    return;
773    
774                case TagConstants.ARRAYREFEXPR:
775                    {
776                        ArrayRefExpr r = (ArrayRefExpr)e;
777                        self.print(o, ind, r.array);
778                        write(o, '['); self.print(o, ind, r.index); write(o, ']');
779                        return;
780                    }
781    
782                case TagConstants.NEWINSTANCEEXPR:
783                    { 
784                        NewInstanceExpr ne = (NewInstanceExpr)e;
785                        if (ne.enclosingInstance != null) {
786                            if (!(ne.enclosingInstance instanceof ThisExpr) ||
787                                !(((ThisExpr)ne.enclosingInstance).inferred) ||
788                                PrettyPrint.displayInferred) {
789                                self.print(o, ind, ne.enclosingInstance);
790                                write(o, ".");
791                            }
792                        }
793                        write(o, "new "); self.print(o, ne.type); self.print(o, ind, ne.args);
794                        if (ne.anonDecl != null) {
795                            writeln(o, " {");
796                            for (int i = 0; i < ne.anonDecl.elems.size(); i++) {
797                                TypeDeclElem elem = ne.anonDecl.elems.elementAt(i);
798                                //@ assume elem.hasParent;   // "invariant"
799                                spaces(o, ind+INDENT);
800                                self.print(o, ind+INDENT, elem, ne.anonDecl.id, true);
801                                if (i != ne.anonDecl.elems.size()-1) writeln(o);
802                            }
803                            spaces(o, ind);
804                            write(o, "}");
805                        }
806                        return;
807                    }
808    
809                case TagConstants.NEWARRAYEXPR:
810                    {
811                        NewArrayExpr na = (NewArrayExpr)e;
812                        Type basetype = na.type;
813                        int cnt;
814    
815                        for (cnt = 0; basetype.getTag() == TagConstants.ARRAYTYPE; cnt++) {
816                            basetype = ((ArrayType)basetype).elemType;
817                        }
818                        write(o, "new "); self.print(o, basetype);
819                        for(int i=0; i<na.dims.size(); i++) {
820                            write(o, '[');
821                            if (na.init == null) {
822                                self.print(o, ind, na.dims.elementAt(i));
823                            }
824                            write(o, ']');
825                        }
826                        for ( ; 0 < cnt; cnt--) write(o, "[]");
827                        if (na.init != null) self.print(o, ind, na.init);
828                        return;
829                    }
830    
831                case TagConstants.CONDEXPR:
832                    {
833                        CondExpr ce = (CondExpr)e;
834                        self.print(o, ind, ce.test); write(o, " ? ");
835                        self.print(o, ind, ce.thn); write(o, " : ");
836                        self.print(o, ind, ce.els);
837                        return;
838                    }
839    
840                case TagConstants.INSTANCEOFEXPR:
841                    {
842                        InstanceOfExpr ie = (InstanceOfExpr)e;
843                        self.print(o, ind, ie.expr);
844                        write(o, " instanceof ");
845                        self.print(o, ie.type);
846                        return;
847                    }
848    
849                case TagConstants.CASTEXPR:
850                    {
851                        CastExpr ce = (CastExpr)e;
852                        write(o, '('); self.print(o, ce.type); write(o, ')');
853                        self.print(o, ind, ce.expr);
854                        return;
855                    }
856    
857                case TagConstants.CLASSLITERAL:
858                    {
859                        ClassLiteral cl = (ClassLiteral)e;
860                        self.print(o, cl.type); write(o, ".class");
861                        return;
862                    }
863    
864                    // Binary expressions
865                case TagConstants.OR: case TagConstants.AND:
866                case TagConstants.BITOR: case TagConstants.BITXOR:
867                case TagConstants.BITAND: case TagConstants.NE:
868                case TagConstants.EQ: case TagConstants.GE:
869                case TagConstants.GT: case TagConstants.LE:
870                case TagConstants.LT: case TagConstants.LSHIFT:
871                case TagConstants.RSHIFT: case TagConstants.URSHIFT:
872                case TagConstants.ADD: case TagConstants.SUB:
873                case TagConstants.DIV: case TagConstants.MOD:
874                case TagConstants.STAR:
875                case TagConstants.ASSIGN: case TagConstants.ASGMUL:
876                case TagConstants.ASGDIV: case TagConstants.ASGREM:
877                case TagConstants.ASGADD: case TagConstants.ASGSUB:
878                case TagConstants.ASGLSHIFT: case TagConstants.ASGRSHIFT:
879                case TagConstants.ASGURSHIFT: case TagConstants.ASGBITAND:
880                case TagConstants.ASGBITOR: case TagConstants.ASGBITXOR:
881                    {
882                        BinaryExpr be = (BinaryExpr)e;
883                        self.print(o, ind, be.left); write(o, ' ');
884                        write(o, OperatorTags.toString(be.op)); write(o, ' ');
885                        self.print(o, ind, be.right);
886                        return;
887                    }
888    
889                    // Unary expressions
890                case TagConstants.UNARYSUB: case TagConstants.UNARYADD:
891                case TagConstants.NOT: case TagConstants.BITNOT:
892                case TagConstants.INC: case TagConstants.DEC:
893                case TagConstants.POSTFIXINC: case TagConstants.POSTFIXDEC:
894                    {
895                        UnaryExpr ue = (UnaryExpr)e;
896                        if (ue.op == TagConstants.POSTFIXINC)
897                        { self.print(o, ind, ue.expr); write(o, "++"); }
898                        else if (ue.op == TagConstants.POSTFIXDEC)
899                        { self.print(o, ind, ue.expr); write(o, "--"); }
900                        else {
901                            write(o, OperatorTags.toString(ue.op));
902                            write(o, " "); self.print(o, ind, ue.expr);
903                        }
904                        return;
905                    }
906    
907                case TagConstants.PARENEXPR:
908                    {
909                        ParenExpr pe = (ParenExpr)e;
910                        write(o, '('); self.print(o, ind, pe.expr); write(o, ')');
911                        return;
912                    }
913    
914                case TagConstants.AMBIGUOUSVARIABLEACCESS:
915                    self.print(o, ((AmbiguousVariableAccess)e).name);
916                    return;
917    
918                case TagConstants.VARIABLEACCESS:
919                    {
920                        VariableAccess lva = (VariableAccess)e;
921                        write(o, lva.decl.id.toString());
922                        return;
923                    }
924          
925                case TagConstants.FIELDACCESS:
926                    {
927                        FieldAccess a = (FieldAccess)e;
928                        self.print(o, ind, a.od); write(o, a.id.toString());
929                        return;
930                    }
931          
932                case TagConstants.AMBIGUOUSMETHODINVOCATION:
933                    {
934                        AmbiguousMethodInvocation ie = (AmbiguousMethodInvocation)e;
935                        self.print(o, ie.name); self.print(o, ind, ie.args);
936                        return;
937                    }
938    
939                case TagConstants.METHODINVOCATION:
940                    {
941                        MethodInvocation ie = (MethodInvocation)e;
942                        self.print(o, ind, ie.od);
943                        write(o, ie.id.toString());
944                        self.print(o, ind, ie.args);
945                        return;
946                    }
947    
948                default:
949                    write(o, unknownTag(e));
950                    return;
951            }
952        }
953    
954        public void print(/*@non_null*/OutputStream o, int ind, ObjectDesignator od) {
955            if (od == null) { write(o, "<null object designator>"); return; }
956            switch (od.getTag()) {
957                case TagConstants.EXPROBJECTDESIGNATOR:
958                    {
959                        ExprObjectDesignator a = (ExprObjectDesignator)od;
960                        if (a.expr.getTag() != TagConstants.THISEXPR
961                            || !((ThisExpr)a.expr).inferred
962                            || PrettyPrint.displayInferred)
963                        { self.print(o, ind, a.expr); write(o, '.'); }
964                        return;
965                    }
966          
967                case TagConstants.TYPEOBJECTDESIGNATOR:
968                    {
969                        TypeObjectDesignator a = (TypeObjectDesignator)od;
970                        if (a.type.getTag() == TagConstants.TYPENAME
971                            || PrettyPrint.displayInferred)
972                        { self.print(o, a.type); write(o, '.'); }
973                        return;
974                    }
975          
976                case TagConstants.SUPEROBJECTDESIGNATOR:
977                    write(o, "super.");
978                    return;
979          
980                default:
981                    write(o, unknownTag(od));
982                    break;
983            }
984        }
985    
986        //// toString methods
987    
988        /**
989         * Requires that <code>tag</code> is one of constants on the left of this
990         * table:
991         * <center><code><table>
992         * <tr> <td> TagConstants.BOOLEANLIT </td> <td> Boolean </td> </tr>
993         * <tr> <td> TagConstants.CHARLIT </td>   <td> Integer </td> </tr>
994         * <tr> <td> TagConstants.DOUBLELIT </td> <td> Double </td> </tr>
995         * <tr> <td> TagConstants.FLOATLIT </td>  <td> Float </td> </tr>
996         * <tr> <td> TagConstants.INTLIT </td>    <td> Integer </td> </tr>
997         * <tr> <td> TagConstants.LONGLIT </td>   <td> Long </td> </tr>
998         * <tr> <td> TagConstants.STRINGLIT </td> <td> String </td> </tr>
999         * </center></code></table>
1000         * 
1001         * and that <code>val</code> is an instance of the corresponding type
1002         * on the right.
1003         * @return a canonical text representation for literal values.
1004         */
1005    
1006        /*@ requires ((tag==TagConstants.BOOLEANLIT) ||
1007          @           (tag==TagConstants.INTLIT) ||
1008          @           (tag==TagConstants.LONGLIT) ||
1009          @           (tag==TagConstants.FLOATLIT) ||
1010          @           (tag==TagConstants.DOUBLELIT) ||
1011          @           (tag==TagConstants.STRINGLIT) ||
1012          @           (tag==TagConstants.CHARLIT));
1013          @*/
1014        /*@ requires (((tag==TagConstants.BOOLEANLIT) ==> (val instanceof Boolean)) &&
1015          @           ((tag==TagConstants.INTLIT) ==> (val instanceof Integer)) &&
1016          @           ((tag==TagConstants.LONGLIT) ==> (val instanceof Long)) &&
1017          @           ((tag==TagConstants.FLOATLIT) ==> (val instanceof Float)) &&
1018          @           ((tag==TagConstants.DOUBLELIT) ==> (val instanceof Double)) &&
1019          @           ((tag==TagConstants.STRINGLIT) ==> (val instanceof String)) &&
1020          @           ((tag==TagConstants.CHARLIT) ==> (val instanceof Integer)));
1021          @*/
1022        //@ ensures \result != null;
1023        public static String toCanonicalString(int tag, Object val) {
1024            if (tag == TagConstants.BOOLEANLIT) return val.toString();
1025    
1026            if (tag == TagConstants.DOUBLELIT) {
1027                String s = val.toString();
1028                if (s.equals("Infinity")) return "1.0 / 0.0";
1029                if (s.equals("-Infinity")) return "-1.0 / 0.0";
1030                if (s.equals("NaN")) return "0.0d / 0.0";
1031                return val.toString() + "D";
1032            }
1033    
1034            if (tag == TagConstants.FLOATLIT) {
1035                String s = val.toString();
1036                if (s.equals("Infinity")) return "1.0f / 0.0f";
1037                if (s.equals("-Infinity")) return "-1.0f / 0.0f";
1038                if (s.equals("NaN")) return "0.0f / 0.0f";
1039                return val.toString() + "F";
1040            }
1041    
1042            if (tag == TagConstants.INTLIT) {
1043                int v = ((Integer) val).intValue();
1044                if (v == Integer.MIN_VALUE) return "0x80000000";
1045                else if (v < 0) return "0x" + Integer.toHexString(v);
1046                else return Integer.toString(v);
1047            }
1048    
1049            if (tag == TagConstants.LONGLIT) {
1050                long v = ((Long) val).longValue();
1051                if (v == Long.MIN_VALUE) return "0x8000000000000000L";
1052                else if (v < 0) return "0x" + Long.toHexString(v) + "L";
1053                else return Long.toString(v) + "L";
1054            }
1055    
1056            if (tag == TagConstants.CHARLIT || tag == TagConstants.STRINGLIT) {
1057                char quote;
1058                if (tag == TagConstants.CHARLIT) {
1059                    quote = '\'';
1060                    val = new Character((char)((Integer)val).intValue());
1061                } else quote = '\"';
1062                String s = val.toString();
1063                StringBuffer result = new StringBuffer(s.length()+2);
1064                result.append(quote);
1065                for(int i = 0, len = s.length(); i < len; i++) {
1066                    char c = s.charAt(i);
1067                    switch (c) {
1068                        case '\b': result.append("\\b"); break;
1069                        case '\t': result.append("\\t"); break;
1070                        case '\n': result.append("\\n"); break;
1071                        case '\f': result.append("\\f"); break;
1072                        case '\r': result.append("\\r"); break;
1073                        case '\"': result.append("\\\""); break;
1074                        case '\'': result.append("\\'"); break;
1075                        case '\\': result.append("\\\\"); break;
1076                        default:
1077                            if (32 <= c && c < 128) result.append(c);
1078                            else {
1079                                result.append("\\u");
1080                                for(int j=12; j>=0; j-=4)
1081                                    result.append(Character.forDigit((c>>j)&0xf, 16));
1082                            }
1083                    }
1084                }
1085                result.append(quote);
1086                return result.toString();
1087            }    
1088    
1089            Assert.precondition(false);
1090            return null; // Dummy
1091        }
1092    
1093        public void print(/*@non_null*/OutputStream o, /*@ non_null */ LexicalPragma lp) {
1094            write(o, "// Lexical pragma at " + lp.getStartLoc() + " ");
1095            writeln(o, lp.toString());
1096        }
1097    
1098        public void print(/*@non_null*/OutputStream o, int ind, /*@ non_null */ TypeDeclElemPragma tp) {
1099            spaces(o, ind);
1100            write(o, "// TypeDeclElemPragma pragma at " + tp.getStartLoc() + " ");
1101            write(o, tp.toString());
1102        }
1103    
1104        public void print(/*@non_null*/OutputStream o, int ind, /*@ non_null */ ModifierPragma mp) {
1105            write(o, "// ModifierPragma pragma at " + mp.getStartLoc() + " ");
1106            write(o, mp.toString());
1107        }
1108    
1109        public void print(/*@non_null*/OutputStream o, int ind, /*@ non_null */ StmtPragma sp) {
1110            spaces(o, ind);
1111            write(o, "// StmtPragma pragma at " + sp.getStartLoc() + " ");
1112            write(o, sp.toString());
1113        }
1114    
1115    
1116        public void print(/*@non_null*/OutputStream o, int ind, /*@ non_null */ TypeModifierPragma tp) {
1117            spaces(o, ind);
1118            write(o, "// TypeModifierPragma pragma at " + tp.getStartLoc() + " ");
1119            write(o, tp.toString());
1120        }
1121      
1122        public void print(/*@non_null*/OutputStream o, int ind, /*@ nullable */ TypeModifierPragmaVec t) {
1123            if (t != null) {
1124                for (int i = 0; i < t.size(); i++) {
1125                    write(o, ' ');
1126                    self.print(o, ind, t.elementAt(i));
1127                }
1128            }
1129        }
1130      
1131        /**
1132         * Generate text to describe a ASTNote with an unknown tag
1133         */
1134        public /*@ non_null */ String unknownTag(/*@ non_null */ ASTNode n) {
1135            return unknownTagMsg(n.getTag());
1136        }
1137      
1138        /**
1139         * Generate text to describe a given unknown tag
1140         */
1141        public /*@ non_null */ String unknownTagMsg(int tag) {
1142            return "UnknownTag<" + tag + ":"
1143                + PrettyPrint.inst.toString(tag) + ">";
1144        }
1145    }