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 DefPredApplExpr extends Expr
032    {
033        public /*@ non_null @*/ Identifier predId;
034    
035        public /*@ non_null @*/ ExprVec args;
036    
037    
038      //@ public represents startLoc <- Location.NULL;
039        public /*@ pure @*/ int getStartLoc() { return Location.NULL; }
040    
041    
042    // Generated boilerplate constructors:
043    
044        //@ ensures this.predId == predId;
045        //@ ensures this.args == args;
046        protected DefPredApplExpr(/*@ non_null @*/ Identifier predId, /*@ non_null @*/ ExprVec args) {
047           this.predId = predId;
048           this.args = args;
049        }
050    
051    // Generated boilerplate methods:
052    
053        public final int childCount() {
054           int sz = 0;
055           if (this.args != null) sz += this.args.size();
056           return sz + 1;
057        }
058    
059        public final Object childAt(int index) {
060                /*throws IndexOutOfBoundsException*/
061           if (index < 0)
062              throw new IndexOutOfBoundsException("AST child index " + index);
063           int indexPre = index;
064    
065           int sz;
066    
067           if (index == 0) return this.predId;
068           else index--;
069    
070           sz = (this.args == null ? 0 : this.args.size());
071           if (0 <= index && index < sz)
072              return this.args.elementAt(index);
073           else index -= sz;
074    
075           throw new IndexOutOfBoundsException("AST child index " + indexPre);
076        }   //@ nowarn Exception;
077    
078        public final /*@non_null*/String toString() {
079           return "[DefPredApplExpr"
080              + " predId = " + this.predId
081              + " args = " + this.args
082              + "]";
083        }
084    
085        public final int getTag() {
086           return TagConstants.DEFPREDAPPLEXPR;
087        }
088    
089        public final void accept(javafe.ast.Visitor v) { 
090            if (v instanceof Visitor) ((Visitor)v).visitDefPredApplExpr(this);
091        }
092    
093        public final Object accept(javafe.ast.VisitorArgResult v, Object o) { 
094            if (v instanceof VisitorArgResult) return ((VisitorArgResult)v).visitDefPredApplExpr(this, o); else return null;
095        }
096    
097        public void check() {
098           this.predId.check();
099           for(int i = 0; i < this.args.size(); i++)
100              this.args.elementAt(i).check();
101        }
102    
103        //@ ensures \result != null;
104        public static DefPredApplExpr make(/*@ non_null @*/ Identifier predId, /*@ non_null @*/ ExprVec args) {
105           DefPredApplExpr result = new DefPredApplExpr(predId, args);
106           return result;
107        }
108    }