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 GeneralizedQuantifiedExpr extends GCExpr
031    {
032      // Sum, Product, Max, Min
033      public int quantifier;
034    
035      public /*@ non_null @*/ GenericVarDeclVec vars;
036    
037      public /*@ non_null @*/ Expr expr;
038    
039      public /*@ non_null @*/ Expr rangeExpr;
040    
041      public ExprVec nopats;
042    
043    
044      public final int getTag() { return quantifier; }
045    
046      private void postCheck() {
047        boolean goodtag =
048          (quantifier == TagConstants.MIN
049           || quantifier == TagConstants.PRODUCT
050           || quantifier == TagConstants.MAXQUANT
051           || quantifier == TagConstants.SUM);
052        Assert.notFalse(goodtag);
053      }
054    
055    
056    // Generated boilerplate constructors:
057    
058      /**
059       * Construct a raw GeneralizedQuantifiedExpr 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 GeneralizedQuantifiedExpr() {}    //@ 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         return sz + 2;
075      }
076    
077      public final Object childAt(int index) {
078              /*throws IndexOutOfBoundsException*/
079         if (index < 0)
080            throw new IndexOutOfBoundsException("AST child index " + index);
081         int indexPre = index;
082    
083         int sz;
084    
085         sz = (this.vars == null ? 0 : this.vars.size());
086         if (0 <= index && index < sz)
087            return this.vars.elementAt(index);
088         else index -= sz;
089    
090         if (index == 0) return this.expr;
091         else index--;
092    
093         if (index == 0) return this.rangeExpr;
094         else index--;
095    
096         sz = (this.nopats == null ? 0 : this.nopats.size());
097         if (0 <= index && index < sz)
098            return this.nopats.elementAt(index);
099         else index -= sz;
100    
101         throw new IndexOutOfBoundsException("AST child index " + indexPre);
102      }   //@ nowarn Exception;
103    
104      public final String toString() {
105         return "[GeneralizedQuantifiedExpr"
106            + " sloc = " + this.sloc
107            + " eloc = " + this.eloc
108            + " quantifier = " + this.quantifier
109            + " vars = " + this.vars
110            + " expr = " + this.expr
111            + " rangeExpr = " + this.rangeExpr
112            + " nopats = " + this.nopats
113            + "]";
114      }
115    
116      public final void accept(javafe.ast.Visitor v) { 
117        if (v instanceof Visitor) ((Visitor)v).visitGeneralizedQuantifiedExpr(this);
118      }
119    
120      public final Object accept(javafe.ast.VisitorArgResult v, Object o) { 
121        if (v instanceof VisitorArgResult) return ((VisitorArgResult)v).visitGeneralizedQuantifiedExpr(this, o); else return null;
122      }
123    
124      public void check() {
125         super.check();
126         for(int i = 0; i < this.vars.size(); i++)
127            this.vars.elementAt(i).check();
128         this.expr.check();
129         this.rangeExpr.check();
130         if (this.nopats != null)
131            for(int i = 0; i < this.nopats.size(); i++)
132               this.nopats.elementAt(i).check();
133         postCheck();
134      }
135    
136      //@ ensures \result != null;
137      public static GeneralizedQuantifiedExpr make(int sloc, int eloc, int quantifier, /*@ non_null @*/ GenericVarDeclVec vars, /*@ non_null @*/ Expr expr, /*@ non_null @*/ Expr rangeExpr, ExprVec nopats) {
138         //@ set I_will_establish_invariants_afterwards = true;
139         GeneralizedQuantifiedExpr result = new GeneralizedQuantifiedExpr();
140         result.sloc = sloc;
141         result.eloc = eloc;
142         result.quantifier = quantifier;
143         result.vars = vars;
144         result.expr = expr;
145         result.rangeExpr = rangeExpr;
146         result.nopats = nopats;
147         return result;
148      }
149    }