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