001    /* Copyright 2000, 2001, Compaq Computer Corporation */
002    
003    /* IF THIS IS A JAVA FILE, DO NOT EDIT IT!  
004    
005       Most Java files in this directory which are part of the Javafe AST
006       are automatically generated using the astgen comment (see
007       ESCTools/Javafe/astgen) from the input file 'hierarchy.h'.  If you
008       wish to modify AST classes or introduce new ones, modify
009       'hierarchy.j.'
010     */
011    
012    package escjava.ast;
013    
014    import java.util.Hashtable;
015    import java.util.Set;
016    import java.util.ArrayList;
017    
018    import javafe.ast.*;
019    import javafe.util.Assert;
020    import javafe.util.Location;
021    import escjava.ParsedRoutineSpecs;
022    
023    // Convention: unless otherwise noted, integer fields named "loc" refer
024    // to the location of the first character of the syntactic unit
025    
026    //# TagBase javafe.tc.TagConstants.LAST_TAG + 1
027    //# VisitorRoot javafe.ast.Visitor
028    
029    
030    public class QuantifiedExpr extends GCExpr
031    {
032      public int quantifier;
033    
034      public /*@ non_null @*/ GenericVarDeclVec vars;
035    
036      public /*@ non_null @*/ Expr rangeExpr;
037    
038      public /*@ non_null @*/ Expr expr;
039    
040      public ExprVec nopats;
041    
042      public ExprVec pats;
043    
044    
045      public final int getTag() { return quantifier; }
046    
047      private void postCheck() {
048        boolean goodtag =
049          (quantifier == TagConstants.FORALL
050           || quantifier == TagConstants.EXISTS);
051        Assert.notFalse(goodtag);
052      }
053      
054    
055    
056    // Generated boilerplate constructors:
057    
058      /**
059       * Construct a raw QuantifiedExpr whose class invariant(s) have not
060       * yet been established.  It is the caller's job to
061       * initialize the returned node's fields so that any
062       * class invariants hold.
063       */
064      //@ requires I_will_establish_invariants_afterwards;
065      protected QuantifiedExpr() {}    //@ nowarn Invariant,NonNullInit;
066    
067    
068    // Generated boilerplate methods:
069    
070      public final int childCount() {
071         int sz = 0;
072         if (this.vars != null) sz += this.vars.size();
073         if (this.nopats != null) sz += this.nopats.size();
074         if (this.pats != null) sz += this.pats.size();
075         return sz + 2;
076      }
077    
078      public final Object childAt(int index) {
079              /*throws IndexOutOfBoundsException*/
080         if (index < 0)
081            throw new IndexOutOfBoundsException("AST child index " + index);
082         int indexPre = index;
083    
084         int sz;
085    
086         sz = (this.vars == null ? 0 : this.vars.size());
087         if (0 <= index && index < sz)
088            return this.vars.elementAt(index);
089         else index -= sz;
090    
091         if (index == 0) return this.rangeExpr;
092         else index--;
093    
094         if (index == 0) return this.expr;
095         else index--;
096    
097         sz = (this.nopats == null ? 0 : this.nopats.size());
098         if (0 <= index && index < sz)
099            return this.nopats.elementAt(index);
100         else index -= sz;
101    
102         sz = (this.pats == null ? 0 : this.pats.size());
103         if (0 <= index && index < sz)
104            return this.pats.elementAt(index);
105         else index -= sz;
106    
107         throw new IndexOutOfBoundsException("AST child index " + indexPre);
108      }   //@ nowarn Exception;
109    
110      public final String toString() {
111         return "[QuantifiedExpr"
112            + " sloc = " + this.sloc
113            + " eloc = " + this.eloc
114            + " quantifier = " + this.quantifier
115            + " vars = " + this.vars
116            + " rangeExpr = " + this.rangeExpr
117            + " expr = " + this.expr
118            + " nopats = " + this.nopats
119            + " pats = " + this.pats
120            + "]";
121      }
122    
123      public final void accept(javafe.ast.Visitor v) { 
124        if (v instanceof Visitor) ((Visitor)v).visitQuantifiedExpr(this);
125      }
126    
127      public final Object accept(javafe.ast.VisitorArgResult v, Object o) { 
128        if (v instanceof VisitorArgResult) return ((VisitorArgResult)v).visitQuantifiedExpr(this, o); else return null;
129      }
130    
131      public void check() {
132         super.check();
133         for(int i = 0; i < this.vars.size(); i++)
134            this.vars.elementAt(i).check();
135         this.rangeExpr.check();
136         this.expr.check();
137         if (this.nopats != null)
138            for(int i = 0; i < this.nopats.size(); i++)
139               this.nopats.elementAt(i).check();
140         if (this.pats != null)
141            for(int i = 0; i < this.pats.size(); i++)
142               this.pats.elementAt(i).check();
143         postCheck();
144      }
145    
146      //@ ensures \result != null;
147      public static QuantifiedExpr make(int sloc, int eloc, int quantifier, /*@ non_null @*/ GenericVarDeclVec vars, /*@ non_null @*/ Expr rangeExpr, /*@ non_null @*/ Expr expr, ExprVec nopats, ExprVec pats) {
148         //@ set I_will_establish_invariants_afterwards = true;
149         QuantifiedExpr result = new QuantifiedExpr();
150         result.sloc = sloc;
151         result.eloc = eloc;
152         result.quantifier = quantifier;
153         result.vars = vars;
154         result.rangeExpr = rangeExpr;
155         result.expr = expr;
156         result.nopats = nopats;
157         result.pats = pats;
158         return result;
159      }
160    }