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 QuantifiedExpr extends GCExpr
032 {
033 public int quantifier;
034
035 public /*@ non_null @*/ GenericVarDeclVec vars;
036
037 public /*@ non_null @*/ Expr rangeExpr;
038
039 public /*@ non_null @*/ Expr expr;
040
041 public ExprVec nopats;
042
043 public ExprVec pats;
044
045
046 //@ public represents startLoc <- sloc; //FIXME should not have to repeat this (because its in GCExpr)
047
048 public final int getTag() { return quantifier; }
049
050 private void postCheck() {
051 boolean goodtag =
052 (quantifier == TagConstants.FORALL
053 || quantifier == TagConstants.EXISTS);
054 Assert.notFalse(goodtag);
055 }
056
057
058
059 // Generated boilerplate constructors:
060
061 //@ ensures this.sloc == sloc;
062 //@ ensures this.eloc == eloc;
063 //@ ensures this.quantifier == quantifier;
064 //@ ensures this.vars == vars;
065 //@ ensures this.rangeExpr == rangeExpr;
066 //@ ensures this.expr == expr;
067 //@ ensures this.nopats == nopats;
068 //@ ensures this.pats == pats;
069 protected QuantifiedExpr(int sloc, int eloc, int quantifier, /*@ non_null @*/ GenericVarDeclVec vars, /*@ non_null @*/ Expr rangeExpr, /*@ non_null @*/ Expr expr, ExprVec nopats, ExprVec pats) {
070 super(sloc, eloc);
071 this.quantifier = quantifier;
072 this.vars = vars;
073 this.rangeExpr = rangeExpr;
074 this.expr = expr;
075 this.nopats = nopats;
076 this.pats = pats;
077 }
078
079 // Generated boilerplate methods:
080
081 public final int childCount() {
082 int sz = 0;
083 if (this.vars != null) sz += this.vars.size();
084 if (this.nopats != null) sz += this.nopats.size();
085 if (this.pats != null) sz += this.pats.size();
086 return sz + 2;
087 }
088
089 public final Object childAt(int index) {
090 /*throws IndexOutOfBoundsException*/
091 if (index < 0)
092 throw new IndexOutOfBoundsException("AST child index " + index);
093 int indexPre = index;
094
095 int sz;
096
097 sz = (this.vars == null ? 0 : this.vars.size());
098 if (0 <= index && index < sz)
099 return this.vars.elementAt(index);
100 else index -= sz;
101
102 if (index == 0) return this.rangeExpr;
103 else index--;
104
105 if (index == 0) return this.expr;
106 else index--;
107
108 sz = (this.nopats == null ? 0 : this.nopats.size());
109 if (0 <= index && index < sz)
110 return this.nopats.elementAt(index);
111 else index -= sz;
112
113 sz = (this.pats == null ? 0 : this.pats.size());
114 if (0 <= index && index < sz)
115 return this.pats.elementAt(index);
116 else index -= sz;
117
118 throw new IndexOutOfBoundsException("AST child index " + indexPre);
119 } //@ nowarn Exception;
120
121 public final /*@non_null*/String toString() {
122 return "[QuantifiedExpr"
123 + " sloc = " + this.sloc
124 + " eloc = " + this.eloc
125 + " quantifier = " + this.quantifier
126 + " vars = " + this.vars
127 + " rangeExpr = " + this.rangeExpr
128 + " expr = " + this.expr
129 + " nopats = " + this.nopats
130 + " pats = " + this.pats
131 + "]";
132 }
133
134 public final void accept(javafe.ast.Visitor v) {
135 if (v instanceof Visitor) ((Visitor)v).visitQuantifiedExpr(this);
136 }
137
138 public final Object accept(javafe.ast.VisitorArgResult v, Object o) {
139 if (v instanceof VisitorArgResult) return ((VisitorArgResult)v).visitQuantifiedExpr(this, o); else return null;
140 }
141
142 public void check() {
143 super.check();
144 for(int i = 0; i < this.vars.size(); i++)
145 this.vars.elementAt(i).check();
146 this.rangeExpr.check();
147 this.expr.check();
148 if (this.nopats != null)
149 for(int i = 0; i < this.nopats.size(); i++)
150 this.nopats.elementAt(i).check();
151 if (this.pats != null)
152 for(int i = 0; i < this.pats.size(); i++)
153 this.pats.elementAt(i).check();
154 postCheck();
155 }
156
157 //@ ensures \result != null;
158 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) {
159 QuantifiedExpr result = new QuantifiedExpr(sloc, eloc, quantifier, vars, rangeExpr, expr, nopats, pats);
160 return result;
161 }
162 }