001    /* Copyright 2000, 2001, Compaq Computer Corporation */
002    
003    package escjava.ast;
004    
005    import java.io.OutputStream;
006    import java.util.Enumeration;
007    import javafe.ast.*;
008    import javafe.util.Assert;
009    import escjava.parser.EscPragmaParser;
010    import escjava.ast.TagConstants;
011    import escjava.ParsedRoutineSpecs;
012    
013    public class EscPrettyPrint extends DelegatingPrettyPrint
014    {
015      public EscPrettyPrint() { }
016      
017      //@ requires self != null;
018      //@ requires del != null;
019      public EscPrettyPrint(PrettyPrint self, PrettyPrint del) {
020        super(self, del);
021      }
022      
023      //@ also
024      //@ requires o != null;
025      //@ requires lp != null;
026      public void print(OutputStream o, LexicalPragma lp) {
027        if (lp.getTag() == TagConstants.NOWARNPRAGMA) {
028          write(o, "//@ ");
029          write(o, TagConstants.toString(TagConstants.NOWARN));
030          NowarnPragma nwp = (NowarnPragma)lp;
031          for (int i = 0; i < nwp.checks.size(); i++) {
032            if (i == 0) write(o, ' ');
033            else write(o, ", ");
034            write(o, nwp.checks.elementAt(i).toString());
035          }
036          write(o, "\n");
037        } else writeln(o, "// Unknown LexicalPragma (tag = " + lp.getTag() + 
038                       " " + TagConstants.toString(lp.getTag()) + ')');
039      }
040      
041      //@ requires o != null; // note that d can be null
042      public void exsuresPrintDecl(OutputStream o, GenericVarDecl d) {
043        if (d == null)
044          write(o, "<null GenericVarDecl>");
045        else {
046          self.print(o, d.type);
047          if (!(d.id.equals(TagConstants.ExsuresIdnName))) {
048            write (o, ' ');
049            write(o, d.id.toString());
050          }
051        }
052      }
053      
054      //@ also
055      //@ requires o != null;
056      //@ requires tp != null;
057      public void print(OutputStream o, int ind, TypeDeclElemPragma tp) {
058        int tag = tp.getTag();
059        int otag = tag; if (tp.isRedundant()) otag = TagConstants.makeRedundant(tag);
060        switch (tag) {
061        case TagConstants.AXIOM:
062        case TagConstants.INVARIANT:
063        case TagConstants.REPRESENTS:
064        case TagConstants.CONSTRAINT: {
065          Expr e = tag == TagConstants.REPRESENTS ?
066            ((NamedExprDeclPragma)tp).expr :
067            ((ExprDeclPragma)tp).expr;
068          write(o, "/*@ "); 
069          write(o, TagConstants.toString(otag));
070          write(o, ' ');
071          self.print(o, ind, e);
072          write(o, "; */");
073          break;
074        }
075          
076        case TagConstants.MODELTYPEPRAGMA: {
077          ModelTypePragma mtp = (ModelTypePragma)tp;
078          write(o, "/*@ model ");
079          self.print(o, ind, mtp.decl);
080          write(o, "@*/");
081            
082          break;
083        }
084          
085        case TagConstants.MODELDECLPRAGMA: {
086          FieldDecl d = ((ModelDeclPragma)tp).decl;
087          /*
088           * Below is a "//@" to prevent illegal nested /* ...  comments
089           * that otherwise might result from any attached modifier pragmas.
090           *
091           * We rely on the fact that no ESC modifier can generate newlines
092           * when pretty printed.  !!!!
093           */
094          write(o, "//@ model ");
095          self.print(o, ind, d, true); 
096          // write(o, "  */\n");
097          write(o, "\n");
098          break;
099        }
100          
101        case TagConstants.GHOSTDECLPRAGMA: {
102          FieldDecl d = ((GhostDeclPragma)tp).decl;
103          /*
104           * Below is a "//@" to prevent illegal nested /* ...  comments
105           * that otherwise might result from any attached modifier pragmas.
106           *
107           * We rely on the fact that no ESC modifier can generate newlines
108           * when pretty printed.  !!!!
109           */
110          write(o, "//@ ghost ");
111          self.print(o, ind, d, true); 
112          // write(o, "  */\n");
113          write(o, "\n");
114          break;
115        }
116        case TagConstants.STILLDEFERREDDECLPRAGMA: {
117          Identifier v = ((StillDeferredDeclPragma)tp).var;
118          write(o, "/*@ ");
119          write(o, TagConstants.toString(TagConstants.STILL_DEFERRED));
120          write(o, " "); 
121          write(o,v.toString()); 
122          write(o, "; */");
123          break;
124        }
125        default:
126          write(o, "/* Unknown TypeDeclElemPragma (tag = " + TagConstants.toString(tag) + ") */");
127          break;
128        }
129      }
130      
131      //@ requires o != null;
132      //@ requires v != null;
133      public void print(OutputStream o, int ind, ModifierPragmaVec v) {
134        int n = v.size();
135        for (int i=0; i<n; ++i) {
136          print(o,ind,v.elementAt(i));
137        }
138      }
139      
140      //@ also
141      //@ requires o != null;
142      //@ requires mp != null;
143      public void print(OutputStream o, int ind, ModifierPragma mp) {
144        int tag = mp.getTag();
145        switch (tag) {
146        case TagConstants.ALSO:
147          write(o, "/*@ "); 
148          write(o, TagConstants.toString(mp.originalTag())); 
149          write(o, " */");
150          break;
151          
152        case TagConstants.OPENPRAGMA:
153          writeln(o, "{|");
154          ++ind;
155          break;
156          
157        case TagConstants.CLOSEPRAGMA:
158          --ind;
159          writeln(o, "|}");
160          break;
161          
162        case TagConstants.MODEL_PROGRAM:
163          write(o, "/*@ "); 
164          write(o, TagConstants.toString(tag)); 
165          write(o, "{...} */"); // FIXME - do all of model program
166          break;
167          
168        case TagConstants.ALSO_REFINE:
169        case TagConstants.CODE_BIGINT_MATH:
170        case TagConstants.CODE_CONTRACT:
171        case TagConstants.CODE_JAVA_MATH:
172        case TagConstants.CODE_SAFE_MATH:
173        case TagConstants.END:
174        case TagConstants.EXAMPLE:
175        case TagConstants.EXCEPTIONAL_EXAMPLE:
176        case TagConstants.FOR_EXAMPLE:
177        case TagConstants.HELPER:
178        case TagConstants.IMMUTABLE:
179        case TagConstants.IMPLIES_THAT:
180        case TagConstants.INSTANCE:
181        case TagConstants.MAY_BE_NULL: // Chalin-Kiniry experiements
182        case TagConstants.MONITORED:
183        case TagConstants.NON_NULL:
184        case TagConstants.NON_NULL_REF_BY_DEFAULT: // Chalin-Kiniry experiements
185        case TagConstants.NORMAL_EXAMPLE:
186        case TagConstants.NULL_REF_BY_DEFAULT: // Chalin-Kiniry experiements
187        case TagConstants.OBS_PURE: // Chalin-Kiniry experiements
188        case TagConstants.PEER: // Universe type annotation
189        case TagConstants.PURE:
190        case TagConstants.READONLY: // Universe type annotation
191        case TagConstants.REP: // Universe type annotation
192        case TagConstants.SPEC_BIGINT_MATH:
193        case TagConstants.SPEC_JAVA_MATH:
194        case TagConstants.SPEC_PROTECTED: // SC HPT AAST 3
195        case TagConstants.SPEC_PUBLIC:
196        case TagConstants.SPEC_SAFE_MATH:
197        case TagConstants.UNINITIALIZED:
198        case TagConstants.WRITABLE_DEFERRED:
199          write(o, "/*@ "); 
200          write(o, TagConstants.toString(tag)); 
201          write(o, " */");
202          break;
203          
204        case TagConstants.GHOST:
205        case TagConstants.MODEL:
206          break;
207          
208        case TagConstants.NO_WACK_FORALL:
209        case TagConstants.OLD:
210          write(o, "/*@ "); 
211          write(o, TagConstants.toString(tag)); 
212          write(o, " */");
213          LocalVarDecl d = ((VarDeclModifierPragma)mp).decl;
214          self.print(o, ind, d, true); 
215          write(o, "; */");
216          break;
217          
218        case TagConstants.ALSO_ENSURES:
219        case TagConstants.ALSO_REQUIRES:
220        case TagConstants.ENSURES:
221        case TagConstants.DIVERGES:
222        case TagConstants.POSTCONDITION:
223        case TagConstants.PRECONDITION:
224        case TagConstants.WHEN:
225        case TagConstants.MONITORED_BY: // from EscPragmaParser.continuePragma(Token)
226        case TagConstants.READABLE_IF:
227        case TagConstants.REQUIRES:
228        case TagConstants.WRITABLE_IF: {
229          write(o, "/*@ ");
230          if (mp.isRedundant())
231            write(o, TagConstants.toString(TagConstants.makeRedundant(tag)));
232          else
233            write(o, TagConstants.toString(tag)); 
234          write(o, ' ');
235          if (!(mp instanceof ExprModifierPragma)) System.out.print("{{{{ " + mp + "}}}}");
236          Expr e = ((ExprModifierPragma)mp).expr;
237          self.print(o, ind, e); 
238          write(o, "; */");
239          break;
240        }
241          
242          // All redundant tokens should not exist in the AST
243          // anymore; they are represented with redundant fields in
244          // the AST nodes.
245        case TagConstants.ASSERT_REDUNDANTLY:
246        case TagConstants.ASSIGNABLE_REDUNDANTLY:
247        case TagConstants.ASSUME_REDUNDANTLY:
248        case TagConstants.CONSTRAINT_REDUNDANTLY:
249        case TagConstants.DECREASES_REDUNDANTLY:
250        case TagConstants.DECREASING_REDUNDANTLY:
251        case TagConstants.DIVERGES_REDUNDANTLY:
252        case TagConstants.DURATION_REDUNDANTLY:
253        case TagConstants.ENSURES_REDUNDANTLY:
254        case TagConstants.EXSURES_REDUNDANTLY:
255        case TagConstants.HENCE_BY_REDUNDANTLY: 
256        case TagConstants.INVARIANT_REDUNDANTLY: 
257        case TagConstants.LOOP_INVARIANT_REDUNDANTLY: 
258        case TagConstants.MAINTAINING_REDUNDANTLY:
259        case TagConstants.MEASURED_BY_REDUNDANTLY:
260        case TagConstants.MODIFIABLE_REDUNDANTLY:
261        case TagConstants.MODIFIES_REDUNDANTLY:
262        case TagConstants.POSTCONDITION_REDUNDANTLY:
263        case TagConstants.PRECONDITION_REDUNDANTLY:
264        case TagConstants.REPRESENTS_REDUNDANTLY:
265        case TagConstants.REQUIRES_REDUNDANTLY:
266        case TagConstants.SIGNALS_REDUNDANTLY:
267        case TagConstants.WHEN_REDUNDANTLY:
268        case TagConstants.WORKING_SPACE_REDUNDANTLY:
269          Assert.fail("Redundant keywords should not be in AST!: "
270                      + TagConstants.toString(tag));
271          break;
272          
273        case TagConstants.MODIFIESGROUPPRAGMA: {
274          ModifiesGroupPragma mm = (ModifiesGroupPragma)mp;
275          write(o, "/*@ modifies ");
276          if (mm.precondition != null) {
277            self.print(o,ind,mm.precondition);
278            write(o, " ==> (");
279          }
280          for (int i=0; i<mm.items.size(); ++i) {
281            if (i != 0) write(o, ", ");
282            CondExprModifierPragma ce = mm.items.elementAt(i);
283            self.print(o, ind, ce.expr); 
284            if (ce.cond != null) {
285              write(o, " if ");
286              self.print(o, ind, ce.cond); 
287            }
288          }
289          if (mm.precondition != null) write(o, ")");
290            
291          write(o, "; @*/");
292          break;
293        }
294          
295        case TagConstants.DURATION:
296        case TagConstants.WORKING_SPACE:
297        case TagConstants.ALSO_MODIFIES:
298        case TagConstants.ASSIGNABLE:
299        case TagConstants.MEASURED_BY:
300        case TagConstants.MODIFIABLE:
301        case TagConstants.MODIFIES: {
302          Expr e = ((CondExprModifierPragma)mp).expr;
303          Expr p = ((CondExprModifierPragma)mp).cond;
304          write(o, "/*@ "); 
305          if (mp.isRedundant())
306            write(o, TagConstants.toString(TagConstants.makeRedundant(tag))); 
307          else
308            write(o, TagConstants.toString(tag)); 
309          write(o, ' ');
310          self.print(o, ind, e); 
311          if (p != null) {
312            write(o, " if ");
313            self.print(o, ind, p); 
314          }
315          write(o, "; */");
316          break;
317        }
318          
319        case TagConstants.ALSO_EXSURES: 
320        case TagConstants.EXSURES:
321        case TagConstants.SIGNALS: {
322          VarExprModifierPragma vemp = (VarExprModifierPragma)mp;
323          write(o, "/*@ "); 
324          write(o, TagConstants.toString(mp.originalTag()));
325          write(o, " ("); 
326          //self.print(o, vemp.arg);
327          exsuresPrintDecl(o, vemp.arg); 
328          write(o, ") ");
329          self.print(o, ind, vemp.expr); 
330          write(o, "; */");
331          break;
332        }
333          
334        case TagConstants.BEHAVIOR:
335        case TagConstants.EXCEPTIONAL_BEHAVIOR:
336        case TagConstants.NORMAL_BEHAVIOR:
337          write(o, "/*@ "); 
338          write(o, TagConstants.toString(tag));
339          write(o, " */");
340          break;
341          
342        case TagConstants.PARSEDSPECS: {
343          ParsedRoutineSpecs s = ((ParsedSpecs)mp).specs;
344          writeln(o,"/*@");
345          if (s.initialAlso != null) self.print(o,ind,s.initialAlso);
346          java.util.Iterator i = s.specs.iterator();
347          int k = 0;
348          while (i.hasNext()) {
349            Object oo = i.next();
350            if (oo == mp || oo == s) break;
351            print(o,ind,(ModifierPragmaVec)oo);
352          }
353          if (s.impliesThat.size() > 0) writeln(o, "implies_that");
354          i = s.impliesThat.iterator();
355          while (i.hasNext()) {
356            print(o,ind,(ModifierPragmaVec)i.next());
357          }
358          if (s.examples.size() > 0) writeln(o, "for_example");
359          i = s.examples.iterator();
360          while (i.hasNext()) {
361            print(o,ind,(ModifierPragmaVec)i.next());
362          }
363          for (int j=0; j<s.modifiers.size(); ++j) {
364            //print(o,ind,s.modifiers.elementAt(j));
365          }
366          writeln(o,"@*/");
367          break;
368        }
369          
370        default:
371          write(o, "/* Unknown ModifierPragma (tag = " + TagConstants.toString(tag) + ") */");
372          break;
373        }
374      }
375      
376      //@ also
377      //@ requires o != null;
378      //@ requires sp != null;
379      public void print(OutputStream o, int ind, StmtPragma sp) {
380        int tag = sp.getTag();
381        int otag = sp.originalTag();
382        switch (tag) {
383        case TagConstants.UNREACHABLE:
384          write(o, "/*@ "); 
385          write(o, TagConstants.toString(otag)); 
386          write(o, " */");
387          break;
388          
389        case TagConstants.ASSERT: {
390          Expr e = ((ExprStmtPragma)sp).expr;
391          Expr l = ((ExprStmtPragma)sp).label;
392          write(o, "/*@ "); 
393          write(o, TagConstants.toString(otag)); 
394          write(o, " ");
395          self.print(o, ind, e);
396          if (l != null) {
397            write(o, " : ");
398            self.print(o, ind, l);
399          }
400          write(o, "; */");
401          break;
402        }
403          
404        case TagConstants.HENCE_BY:
405        case TagConstants.ASSUME:
406        case TagConstants.DECREASES:
407        case TagConstants.DECREASING:
408        case TagConstants.MAINTAINING:
409        case TagConstants.LOOP_INVARIANT:
410        case TagConstants.LOOP_PREDICATE: {
411          Expr e = ((ExprStmtPragma)sp).expr;
412          write(o, "/*@ "); 
413          write(o, TagConstants.toString(otag)); 
414          write(o, ' ');
415          self.print(o, ind, e); 
416          write(o, "; */");
417          break;
418        }
419          
420        case TagConstants.SETSTMTPRAGMA: {
421          SetStmtPragma s = (SetStmtPragma)sp;
422          write(o, "/*@ ");
423          write(o, TagConstants.toString(TagConstants.SET));
424          write(o, " ");
425          self.print(o, ind, s.target);
426          write(o, " = ");
427          self.print(o, ind, s.value);
428          write(o, "; */");
429          break;
430        }
431          
432        default:
433          write(o, "/* Unknown StmtPragma (tag = " + TagConstants.toString(otag) + ") */");
434          break;
435        }
436      }
437    
438      // g can be null
439      public static void print(GuardedCmd g) {
440        ((EscPrettyPrint)inst).print(System.out,0,g);
441      }
442      
443      /** Print a guarded command.  Assumes that <code>g</code> should be
444          printed starting at the current position of <code>o</code>.  It
445          does <em>not</em> print a new-line at the end of the statement.
446          However, if the statement needs to span multiple lines (for
447          example, because it has embedded statements), then these lines are
448          indented by <code>ind</code> spaces. */
449      
450      //@ requires o != null; 
451      // g can be null
452      public void print(OutputStream o, int ind, GuardedCmd g) {
453        if (g == null) {
454          writeln(o, "<null Stmt>");
455          return;
456        }
457        
458        int tag = g.getTag();
459        switch (tag) {
460        case TagConstants.SKIPCMD:
461          write(o, "SKIP");
462          return;
463          
464        case TagConstants.RAISECMD:
465          write(o, "RAISE");
466          return;
467          
468        case TagConstants.ASSERTCMD:
469          write(o, "ASSERT ");
470          print(o, ind, ((ExprCmd)g).pred);
471          return;
472          
473        case TagConstants.ASSUMECMD:
474          write(o, "ASSUME ");
475          print(o, ind, ((ExprCmd)g).pred);
476          return;
477          
478        case TagConstants.GETSCMD: {
479          GetsCmd gc = (GetsCmd)g;
480          if (escjava.Main.options().nvu)
481            write(o, gc.v.decl.id.toString());
482          else
483            write(o, escjava.translate.UniqName.variable(gc.v.decl));
484          write(o, " = ");
485          if (gc.rhs != null) print(o, ind, gc.rhs);
486          return;
487        }
488          
489        case TagConstants.SUBGETSCMD: {
490          SubGetsCmd sgc = (SubGetsCmd)g;
491          if (escjava.Main.options().nvu)
492            write(o, sgc.v.decl.id.toString());
493          else
494            write(o, escjava.translate.UniqName.variable(sgc.v.decl));
495          write(o, "[");
496          print(o, ind, sgc.index);
497          write(o, "] = ");
498          if (sgc.rhs != null) print(o, ind, sgc.rhs);
499          return;
500        }
501          
502        case TagConstants.SUBSUBGETSCMD: {
503          SubSubGetsCmd ssgc = (SubSubGetsCmd)g;
504          if (escjava.Main.options().nvu)
505            write(o, ssgc.v.decl.id.toString());
506          else
507            write(o, escjava.translate.UniqName.variable(ssgc.v.decl));
508          write(o, "[");
509          print(o, ind, ssgc.index1);
510          write(o, "][");
511          print(o, ind, ssgc.index2);
512          write(o, "] = ");
513          if (ssgc.rhs != null) print(o, ind, ssgc.rhs);
514          return;
515        }
516          
517        case TagConstants.RESTOREFROMCMD: {
518          RestoreFromCmd gc = (RestoreFromCmd)g;
519          write(o, "RESTORE ");
520          if (escjava.Main.options().nvu)
521            write(o, gc.v.decl.id.toString());
522          else
523            write(o, escjava.translate.UniqName.variable(gc.v.decl));
524          write(o, " FROM ");
525          print(o, ind, gc.rhs);
526          return;
527        }
528          
529        case TagConstants.VARINCMD: {
530          VarInCmd vc = (VarInCmd)g;
531          write(o, "VAR");
532          printVarVec(o, vc.v);
533          writeln(o, " IN");
534          spaces(o, ind+INDENT);
535          print(o, ind+INDENT, vc.g);
536          writeln(o);
537          spaces(o, ind);
538          write(o, "END");
539          return;
540        }
541          
542        case TagConstants.DYNINSTCMD: {
543          DynInstCmd dc = (DynInstCmd)g;
544          writeln(o, "DynamicInstanceCmd \"" + dc.s + "\" IN");
545          spaces(o, ind+INDENT);
546          print(o, ind+INDENT, dc.g);
547          writeln(o);
548          spaces(o, ind);
549          write(o, "END");
550          return;
551        }
552          
553        case TagConstants.SEQCMD: {
554          SeqCmd sc = (SeqCmd)g;
555          int len = sc.cmds.size();
556          if (len == 0) write(o, "SKIP");
557          else if (len == 1) print(o, ind, sc.cmds.elementAt(0));
558          else {
559            for (int i = 0; i < len; i++) {
560              if (i != 0) {
561                writeln(o, ";");
562                spaces(o, ind);
563              }
564              print(o, ind, sc.cmds.elementAt(i));
565            }
566          }
567          return;
568        }
569          
570        case TagConstants.CALL: {
571          Call call = (Call)g;
572          if (call.inlined) {
573            write(o, "INLINED ");
574          }
575          write(o, "CALL "+ call.spec.dmd.getId());
576          print(o, ind, call.args );
577          if (escjava.Main.options().showCallDetails) {
578            writeln(o, " {");
579            spaces(o, ind+INDENT);
580            printSpec(o, ind+INDENT, call.spec );
581            writeln(o);
582            spaces(o, ind);
583            writeln(o, "DESUGARED:");
584            spaces(o, ind+INDENT);
585            print(o, ind+INDENT, call.desugared);
586            writeln(o);
587            spaces(o, ind);
588            write(o, "}");
589          }
590          return;
591        }
592          
593        case TagConstants.TRYCMD: {
594          CmdCmdCmd tc = (CmdCmdCmd)g;
595          write(o, "{");
596          spaces(o, INDENT-1 );
597          print(o, ind+INDENT, tc.g1);
598            
599          writeln(o);
600          spaces(o, ind);
601          write(o, "!");
602          spaces(o, INDENT-1 );
603          print(o, ind+INDENT, tc.g2);
604          writeln(o);
605            
606          spaces(o, ind);
607          write(o, "}");
608          return;
609        }
610          
611        case TagConstants.LOOPCMD: {
612          LoopCmd lp = (LoopCmd)g;
613          writeln(o, "LOOP");
614          printCondVec(o, ind+INDENT, lp.invariants,
615                       TagConstants.toString(TagConstants.LOOP_INVARIANT));
616          printDecrInfoVec(o, ind+INDENT, lp.decreases,
617                           TagConstants.toString(TagConstants.DECREASES));
618            
619          int nextInd = ind+INDENT;
620          if (lp.tempVars.size() != 0) {
621            spaces(o, nextInd);
622            write(o, "VAR");
623            printVarVec(o, lp.tempVars);
624            writeln(o, " IN");
625            nextInd += INDENT;
626          }
627            
628          spaces(o, nextInd);
629          print(o, nextInd, lp.guard);
630          // let a double-semicolon denote the break between the "guard" and "body"
631          writeln(o, ";;");
632          spaces(o, nextInd);
633          print(o, nextInd, lp.body);
634          writeln(o);
635            
636          if (lp.tempVars.size() != 0) {
637            spaces(o, ind+INDENT);
638            writeln(o, "END");
639          }
640            
641          if (escjava.Main.options().showLoopDetails) {
642            spaces(o, ind);
643            writeln(o, "PREDICATES:");
644            for (int i = 0; i < lp.predicates.size(); i++) {
645              spaces(o, ind+INDENT);
646              print(o, ind+INDENT, lp.predicates.elementAt(i));
647              writeln(o);
648            }
649              
650            /*
651              spaces(o, ind);
652              writeln(o, "INVARIANTS:");
653              for (int i = 1; i < lp.invariants.size(); i++) {
654              spaces(o, ind+INDENT);
655              print(o, ind+INDENT, lp.invariants.elementAt(i).pred);
656              writeln(o);
657              }
658            */
659              
660            spaces(o, ind);
661            writeln(o, "DESUGARED:");
662            spaces(o, ind+INDENT);
663            print(o, ind+INDENT, lp.desugared);
664            writeln(o);
665          }
666            
667          spaces(o, ind);
668          write(o, "END");
669          return;
670        }
671          
672        case TagConstants.CHOOSECMD: {
673          CmdCmdCmd cc = (CmdCmdCmd)g;
674          write(o, "{");
675          spaces(o, INDENT-1 );
676          print(o, ind+INDENT, cc.g1);
677            
678          writeln(o);
679          spaces(o, ind);
680          writeln(o, "[]");
681            
682          spaces(o, ind+INDENT);
683          print(o, ind+INDENT, cc.g2);
684          writeln(o);
685            
686          spaces(o, ind);
687          write(o, "}");
688          return;
689        }
690          
691        default:
692          write(o, "UnknownTag<" + tag + ":");
693          write(o, TagConstants.toString(tag) + ">");
694          return;
695        }
696      }
697      
698      //@ requires o != null;
699      //@ requires vars != null;
700      private void printVarVec(OutputStream o, GenericVarDeclVec vars) {
701        for (int i = 0; i < vars.size(); i++) {
702          GenericVarDecl vd = vars.elementAt(i);
703          write(o, ' ');
704          if (false) {
705            // Someday we may have special variables for map types
706            write(o, "Map[");
707            // write(o, ((FieldDecl)vd).parent.id.toString());
708            write(o, " -> ");
709            print(o, vd.type);
710            write(o, "]");
711          } else print(o, vd.type);
712          write(o, ' ');
713          if (escjava.Main.options().nvu)
714            write(o, vd.id.toString());
715          else
716            write(o, escjava.translate.UniqName.variable(vd));
717          if (i != vars.size()-1) {
718            write(o, ';');
719          }
720        }
721      }
722      
723      //@ requires o != null;
724      //@ requires spec != null;
725      public void printSpec(OutputStream o, int ind, Spec spec) {
726        write(o, "SPEC ");
727        
728        ModifierPragmaVec local = spec.dmd.original.pmodifiers;
729        ModifierPragmaVec combined = ModifierPragmaVec.make();
730        
731        for (int i=0; i<spec.dmd.requires.size(); i++)
732          combined.addElement(spec.dmd.requires.elementAt(i));
733        for (int i=0; i<spec.dmd.modifies.size(); i++)
734          combined.addElement(spec.dmd.modifies.elementAt(i));
735        for (int i=0; i<spec.dmd.ensures.size(); i++)
736          combined.addElement(spec.dmd.ensures.elementAt(i));
737        for (int i=0; i<spec.dmd.exsures.size(); i++)
738          combined.addElement(spec.dmd.exsures.elementAt(i));
739        
740        spec.dmd.original.pmodifiers = combined;
741        print(o, ind+INDENT, spec.dmd.original,
742              spec.dmd.getContainingClass().id,
743              false);
744        spec.dmd.original.pmodifiers = local;
745        
746        
747        spaces(o, ind);
748        write(o, "targets ");
749        print(o, ind, spec.targets);
750        writeln(o, ";");
751        
752        spaces(o, ind);
753        write(o, "prevarmap { ");
754        boolean first=true;
755        for(Enumeration e = spec.preVarMap.keys(); e.hasMoreElements(); )
756          {
757            if( !first )
758              write(o, ", ");
759            else
760              first = false;
761          
762            GenericVarDecl vd = (GenericVarDecl)e.nextElement();
763            VariableAccess va = (VariableAccess)spec.preVarMap.get(vd);
764            print( o, vd );
765            write(o, "->" );
766            print( o, ind, va );
767          }
768        writeln(o, " };");
769        
770        printCondVec(o, ind, spec.pre, "pre");
771        printCondVec(o, ind, spec.post, "post");
772        return;
773      }
774      
775      //@ requires o != null;
776      //@ requires cv != null;
777      //@ requires name != null;
778      public void printCondVec(OutputStream o, int ind, ConditionVec cv,
779                               String name) {
780        for(int i=0; i<cv.size(); i++)
781          {
782            spaces(o, ind);
783            write(o, name+" ");
784            printCond(o, ind, cv.elementAt(i));
785            writeln(o, ";");
786          }
787      }
788      
789      //@ requires o != null;
790      //@ requires div != null;
791      //@ requires name != null;
792      public void printDecrInfoVec(OutputStream o, int ind,
793                                   DecreasesInfoVec div, String name) {
794        for (int i = 0; i < div.size(); i++) {
795          spaces(o, ind);
796          write(o, name+" ");
797          print(o, ind, div.elementAt(i).f);
798          writeln(o, ";");
799        }
800      }
801      
802      //@ requires o != null;
803      //@ requires cond != null;
804      public void printCond(OutputStream o, int ind, Condition cond) {
805        write(o, TagConstants.toString(cond.label)+": ");
806        print(o, ind, cond.pred );
807      }
808      
809      //@ also
810      //@ requires o != null;
811      //@ requires e != null;
812      public void print(OutputStream o, int ind, VarInit e) {
813        int tag = e.getTag();
814        switch (tag) {
815          
816        case TagConstants.VARIABLEACCESS: {
817          VariableAccess lva = (VariableAccess)e;
818          if (escjava.Main.options().nvu)
819            write(o, lva.decl.id.toString());
820          else
821            write(o, escjava.translate.UniqName.variable(lva.decl));
822          break;
823        }
824          
825        case TagConstants.IMPLIES:
826        case TagConstants.EXPLIES:
827        case TagConstants.IFF:
828        case TagConstants.NIFF:
829        case TagConstants.SUBTYPE: {
830          BinaryExpr be = (BinaryExpr)e;
831          self.print(o, ind, be.left);
832          write(o, ' '); write(o, TagConstants.toString(be.op)); write(o, ' ');
833          self.print(o, ind, be.right);
834          break;
835        }
836          
837        case TagConstants.SYMBOLLIT:
838          write(o, (String) (((LiteralExpr)e).value));
839          break;
840          
841        case TagConstants.LABELEXPR: {
842          LabelExpr le = (LabelExpr)e;
843          write(o, "(");
844          write(o, (le.positive ? TagConstants.toString(TagConstants.LBLPOS) :
845                    TagConstants.toString(TagConstants.LBLNEG)));
846          write(o, " ");
847          write(o, le.label.toString());
848          write(o, ' ');
849          self.print(o, ind, le.expr);
850          write(o, ")");
851          break;
852        }
853          
854        case TagConstants.LOCKSETEXPR:
855          write(o, TagConstants.toString(TagConstants.LS));
856          break;
857          
858        case TagConstants.ELEMSNONNULL:
859        case TagConstants.ELEMTYPE:
860        case TagConstants.FRESH:
861        case TagConstants.MAX:
862        case TagConstants.NOWARN_OP:
863        case TagConstants.PRE:
864        case TagConstants.SPACE:
865        case TagConstants.TYPEOF:
866        case TagConstants.WACK_BIGINT_MATH: 
867        case TagConstants.WACK_DURATION:
868        case TagConstants.WACK_JAVA_MATH:
869        case TagConstants.WACK_NOWARN:
870        case TagConstants.WACK_SAFE_MATH:
871        case TagConstants.WACK_WORKING_SPACE:
872        case TagConstants.WARN:
873        case TagConstants.WARN_OP: {
874          write(o, TagConstants.toString(tag));
875          self.print(o, ind, ((NaryExpr)e).exprs);
876          break;
877        }
878          
879        case TagConstants.NOT_MODIFIED: 
880          write(o, TagConstants.toString(tag));
881          write(o, '(');
882          self.print(o, ind, ((NotModifiedExpr)e).expr);
883          write(o, ')');
884          break;
885          
886        case TagConstants.DTTFSA: {
887          ExprVec es = ((NaryExpr)e).exprs;
888          write(o, TagConstants.toString(tag));
889          write(o, '(');
890          self.print(o, ((TypeExpr)es.elementAt(0)).type);
891          for (int i = 1; i < es.size(); i++) {
892            write(o, ", ");
893            self.print(o, ind, es.elementAt(i));
894          }
895          write(o, ')');
896          break;
897        }
898          
899        case TagConstants.NUM_OF:{
900          NumericalQuantifiedExpr qe = (NumericalQuantifiedExpr)e;
901          write(o, "(");
902          write(o, TagConstants.toString(tag));
903          write(o, " ");
904          String prefix = "";
905          for( int i=0; i<qe.vars.size(); i++) {
906            GenericVarDecl decl = qe.vars.elementAt(i);
907            write(o, prefix );
908            if (i == 0) self.print(o, decl.type);
909            write(o, ' ');
910            if (escjava.Main.options().nvu)
911              write(o, decl.id.toString());
912            else
913              write(o, escjava.translate.UniqName.variable(decl));
914            prefix = ", ";
915          }
916          write(o, "; ");
917          self.print(o, ind, qe.expr);
918          write(o, ')');
919          break;
920        }
921          
922        case TagConstants.SUM:
923        case TagConstants.PRODUCT:
924        case TagConstants.MIN:
925        case TagConstants.MAXQUANT:{
926          GeneralizedQuantifiedExpr qe = (GeneralizedQuantifiedExpr)e;
927          write(o, "(");
928          write(o, TagConstants.toString(tag));
929          write(o, " ");
930          String prefix = "";
931          for( int i=0; i<qe.vars.size(); i++) {
932            GenericVarDecl decl = qe.vars.elementAt(i);
933            write(o, prefix );
934            if (i == 0) self.print(o, decl.type);
935            write(o, ' ');
936            if (escjava.Main.options().nvu)
937              write(o, decl.id.toString());
938            else
939              write(o, escjava.translate.UniqName.variable(decl));
940            prefix = ", ";
941          }
942          write(o, "; ");
943          self.print(o, ind, qe.expr);
944          write(o, "; ");
945          self.print(o, ind, qe.rangeExpr);
946          write(o, ')');
947          break;
948        }
949        case TagConstants.FORALL:
950        case TagConstants.EXISTS: {
951          QuantifiedExpr qe = (QuantifiedExpr)e;
952          write(o, "(");
953          write(o, TagConstants.toString(tag));
954          write(o, " ");
955          String prefix = "";
956          for( int i=0; i<qe.vars.size(); i++) {
957            GenericVarDecl decl = qe.vars.elementAt(i);
958            write(o, prefix );
959            if (i == 0) self.print(o, decl.type);
960            write(o, ' ');
961            if (escjava.Main.options().nvu)
962              write(o, decl.id.toString());
963            else
964              write(o, escjava.translate.UniqName.variable(decl));
965            prefix = ", ";
966          }
967          write(o, "; ");
968          self.print(o, ind, qe.expr);
969          write(o, ')');
970          break;
971        }
972          
973        case TagConstants.RESEXPR:
974          write(o, TagConstants.toString(TagConstants.RES));
975          break;
976          
977        case TagConstants.BOOLEANLIT: {
978          String comment = (String)EscPragmaParser.informalPredicateDecoration.get(e);
979          if (comment != null) {
980            LiteralExpr le = (LiteralExpr)e;
981            Boolean b = (Boolean)le.value;
982            Assert.notFalse(b.booleanValue() == true);
983              
984            write(o, "(*");
985            write(o, comment);
986            write(o, "*)");
987          } else {
988            super.print(o, ind, e);
989          }
990          break;
991        }
992          
993        case TagConstants.SUBSTEXPR: {
994          SubstExpr subst = (SubstExpr)e;
995          write(o, "[subst ");
996          self.print(o, ind, subst.val);
997          write(o, " for ");
998          if (escjava.Main.options().nvu)
999            write(o, subst.var.id.toString());
1000          else
1001            write(o, escjava.translate.UniqName.variable(subst.var));
1002          write(o, " in ");
1003          self.print(o, ind, subst.target);
1004          write(o, "]");
1005          break;
1006        }
1007          
1008        case TagConstants.TYPEEXPR:
1009          write(o, TagConstants.toString(TagConstants.TYPE));
1010          write(o, "(");
1011          self.print(o, ((TypeExpr)e).type);
1012          write(o, ")");
1013          break;
1014          
1015        case TagConstants.ARRAYRANGEREFEXPR: {
1016          ArrayRangeRefExpr we = (ArrayRangeRefExpr)e;
1017          print( o, ind, we.array );
1018          write(o, "[");
1019          if (we.lowIndex == null && we.highIndex == null) {
1020            write(o, "*");
1021          } else {
1022            print(o, ind, we.lowIndex);
1023            write(o,"..");
1024            print(o, ind, we.highIndex);
1025          }
1026          write(o, "]");
1027          break;
1028        }
1029          
1030        case TagConstants.WILDREFEXPR: {
1031          WildRefExpr we = (WildRefExpr)e;
1032          print( o, ind, we.od );
1033          // The ObjectDesignator prints the '.'
1034          write(o, "*");
1035          break;
1036        }
1037          
1038        case TagConstants.GUARDEXPR: {
1039          GuardExpr ge = (GuardExpr)e;
1040          write ( o, "(GUARD ");
1041          write ( o, escjava.translate.UniqName.locToSuffix(ge.locPragmaDecl) + " ");
1042          print( o, ind, ge.expr );
1043          write(o, ")");
1044          break;
1045        }
1046          
1047        case TagConstants.ALLOCLT:
1048        case TagConstants.ALLOCLE:
1049        case TagConstants.ANYEQ:
1050        case TagConstants.ANYNE:
1051        case TagConstants.ARRAYLENGTH:
1052        case TagConstants.ARRAYFRESH:
1053        case TagConstants.ARRAYMAKE:
1054        case TagConstants.ARRAYSHAPEMORE:
1055        case TagConstants.ARRAYSHAPEONE:
1056        case TagConstants.ASELEMS:
1057        case TagConstants.ASFIELD:
1058        case TagConstants.ASLOCKSET:
1059        case TagConstants.BOOLAND:
1060        case TagConstants.BOOLANDX:
1061        case TagConstants.BOOLEQ:
1062        case TagConstants.BOOLIMPLIES:
1063        case TagConstants.BOOLNE:
1064        case TagConstants.BOOLNOT:
1065        case TagConstants.BOOLOR:
1066        case TagConstants.CAST:
1067        case TagConstants.CLASSLITERALFUNC:
1068        case TagConstants.CONDITIONAL:
1069        case TagConstants.ECLOSEDTIME:
1070        case TagConstants.FCLOSEDTIME:
1071        case TagConstants.FLOATINGADD:
1072        case TagConstants.FLOATINGDIV:
1073        case TagConstants.FLOATINGEQ:
1074        case TagConstants.FLOATINGGE:
1075        case TagConstants.FLOATINGGT:
1076        case TagConstants.FLOATINGLE:
1077        case TagConstants.FLOATINGLT:
1078        case TagConstants.FLOATINGMOD:
1079        case TagConstants.FLOATINGMUL:
1080        case TagConstants.FLOATINGNE:
1081        case TagConstants.FLOATINGNEG:
1082        case TagConstants.FLOATINGSUB:
1083        case TagConstants.INTEGRALADD:
1084        case TagConstants.INTEGRALAND:
1085        case TagConstants.INTEGRALDIV:
1086        case TagConstants.INTEGRALEQ:
1087        case TagConstants.INTEGRALGE:
1088        case TagConstants.INTEGRALGT:
1089        case TagConstants.INTEGRALLE:
1090        case TagConstants.INTEGRALLT:
1091        case TagConstants.INTEGRALMOD:
1092        case TagConstants.INTEGRALMUL:
1093        case TagConstants.INTEGRALNE:
1094        case TagConstants.INTEGRALNEG:
1095        case TagConstants.INTEGRALNOT:
1096        case TagConstants.INTEGRALOR:
1097        case TagConstants.INTSHIFTL:
1098        case TagConstants.LONGSHIFTL:
1099        case TagConstants.INTSHIFTR:
1100        case TagConstants.LONGSHIFTR:
1101        case TagConstants.INTSHIFTRU:
1102        case TagConstants.LONGSHIFTRU:
1103        case TagConstants.INTEGRALSUB:
1104        case TagConstants.INTEGRALXOR:
1105        case TagConstants.INTERN:
1106        case TagConstants.INTERNED:
1107        case TagConstants.IS:
1108        case TagConstants.ISALLOCATED:
1109        case TagConstants.ISNEWARRAY:
1110        case TagConstants.LOCKLE:
1111        case TagConstants.LOCKLT:
1112        case TagConstants.REFEQ:
1113        case TagConstants.REFNE:
1114        case TagConstants.SELECT:
1115        case TagConstants.STORE:
1116        case TagConstants.STRINGCAT:
1117        case TagConstants.STRINGCATP:
1118        case TagConstants.TYPEEQ:
1119        case TagConstants.TYPENE:
1120        case TagConstants.TYPELE:
1121        case TagConstants.UNSET:
1122        case TagConstants.VALLOCTIME:
1123          write(o, TagConstants.toString(tag));
1124          self.print(o, ind, ((NaryExpr)e).exprs);
1125          break;
1126          
1127        case TagConstants.METHODCALL:
1128          write(o, ((NaryExpr)e).methodName.toString());
1129          self.print(o, ind, ((NaryExpr)e).exprs);
1130          break;
1131          
1132        case TagConstants.NOTMODIFIEDEXPR:
1133          write(o, TagConstants.toString(TagConstants.NOT_MODIFIED));
1134          write(o, "(");
1135          self.print(o, ind, ((NotModifiedExpr)e).expr);
1136          write(o, ")");
1137          break;
1138          
1139        case TagConstants.EVERYTHINGEXPR:
1140          write(o, TagConstants.toString(TagConstants.EVERYTHING));
1141          break;
1142        case TagConstants.NOTHINGEXPR:
1143          write(o, TagConstants.toString(TagConstants.NOTHING));
1144          break;
1145        case TagConstants.NOTSPECIFIEDEXPR:
1146          write(o, TagConstants.toString(TagConstants.NOT_SPECIFIED));
1147          break;
1148          
1149        default:
1150          Assert.notFalse(tag<=javafe.tc.TagConstants.LAST_TAG,
1151                          "illegal attempt to pass tag #" + tag + " (" +
1152                          TagConstants.toString(tag) + ") to javafe");
1153          super.print(o, ind, e);
1154          break;
1155        }
1156      }
1157      
1158      //@ also
1159      //@ requires o != null;
1160      //@ requires t != null;
1161      public void print(OutputStream o, Type t) {
1162        
1163        switch ( t.getTag()) {
1164        case TagConstants.ANY:
1165          write(o, "anytype" );
1166          break;
1167          
1168        case TagConstants.TYPECODE:
1169        case TagConstants.LOCKSET:
1170        case TagConstants.OBJECTSET:
1171          write(o, TagConstants.toString(t.getTag()) );
1172          break;
1173          
1174        case TagConstants.BIGINTTYPE:
1175          write(o, "bigint");
1176          break;
1177          
1178        case TagConstants.REALTYPE:
1179          write(o, "real");
1180          break;
1181          
1182        default:
1183          super.print( o, t );
1184        }
1185      }
1186      
1187      /* (non-Javadoc)
1188       * @see javafe.ast.PrettyPrint#toString(int)
1189       */
1190      public /*@ non_null @*/ String toString(int tag) {
1191        // Best version available in the back end:
1192        return escjava.ast.TagConstants.toString(tag);
1193      }
1194      
1195    }