    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 DefPredLetExpr extends Expr
    031    {
    032        public /*@ non_null @*/ DefPredVec preds;
    033
    034        public /*@ non_null @*/ Expr body;
    035
    036
    037        public int getStartLoc() { return body.getStartLoc(); }
    038
    039
    040    // Generated boilerplate constructors:
    041
    042        /**
    043         * Construct a raw DefPredLetExpr whose class invariant(s) have not
    044         * yet been established.  It is the caller's job to
    045         * initialize the returned node's fields so that any
    046         * class invariants hold.
    047         */
    048        //@ requires I_will_establish_invariants_afterwards;
    049        protected DefPredLetExpr() {}    //@ nowarn Invariant,NonNullInit;
    050
    051
    052    // Generated boilerplate methods:
    053
    054        public final int childCount() {
    055           int sz = 0;
    056           if (this.preds != null) sz += this.preds.size();
    057           return sz + 1;
    058        }
    059
    060        public final Object childAt(int index) {
    061                /*throws IndexOutOfBoundsException*/
    062           if (index < 0)
    063              throw new IndexOutOfBoundsException("AST child index " + index);
    064           int indexPre = index;
    065
    066           int sz;
    067
    068           sz = (this.preds == null ? 0 : this.preds.size());
    069           if (0 <= index && index < sz)
    070              return this.preds.elementAt(index);
    071           else index -= sz;
    072
    073           if (index == 0) return this.body;
    074           else index--;
    075
    076           throw new IndexOutOfBoundsException("AST child index " + indexPre);
    077        }   //@ nowarn Exception;
    078
    079        public final String toString() {
    080           return "[DefPredLetExpr"
    081              + " preds = " + this.preds
    082              + " body = " + this.body
    083              + "]";
    084        }
    085
    086        public final int getTag() {
    087           return TagConstants.DEFPREDLETEXPR;
    088        }
    089
    090        public final void accept(javafe.ast.Visitor v) {
    091            if (v instanceof Visitor) ((Visitor)v).visitDefPredLetExpr(this);
    092        }
    093
    094        public final Object accept(javafe.ast.VisitorArgResult v, Object o) {
    095            if (v instanceof VisitorArgResult) return ((VisitorArgResult)v).visitDefPredLetExpr(this, o); else return null;
    096        }
    097
    098        public void check() {
    099           for(int i = 0; i < this.preds.size(); i++)
    100              this.preds.elementAt(i).check();
    101           this.body.check();
    102        }
    103
    104        //@ ensures \result != null;
    105        public static DefPredLetExpr make(/*@ non_null @*/ DefPredVec preds, /*@ non_null @*/ Expr body) {
    106           //@ set I_will_establish_invariants_afterwards = true;
    107           DefPredLetExpr result = new DefPredLetExpr();
    108           result.preds = preds;
    109           result.body = body;
    110           return result;
    111        }
    112    }