    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 javafe.ast;
    013
    014    import javafe.util.Assert;
    015    import javafe.util.Location;
    016    import javafe.util.ErrorSet;
    017
    018    // Convention: unless otherwise noted, integer fields named "loc" refer
    019    // to the location of the first character of the syntactic unit
    020
    021
    022    /* ---------------------------------------------------------------------- */
    023
    024    /**
    025     * Treated as an immutable type. <p>
    026     *
    027     * Invariant: There is always at least one element in a Name.
    028     */
    029
    030    public abstract class Name extends ASTNode
    031    {
    032        /**
    033         * Return our printname, which will be of one of the forms X, X.Y,
    034         * X.Y.Z, ...
    035         */
    036        //@ ensures \result != null;
    037        //@ pure
    038        public abstract String printName();
    039
    040        /**
    041         * Return a hash code for <code>this</code> such that two
    042         * <code>Name</code>s that are <code>equals</code> have the same
    043         * hash code.
    044         */
    045        public abstract int hashCode();
    046
    047        /**
    048         * Return true if <code>other</code> is a <code>Name</code> that
    049         * is component-wise equal to <code>this</code>.
    050         */
    051        public abstract boolean equals(Object other);
    052
    053        /**
    054         * The number of identifiers we contain.
    055         */
    056        //@ invariant length >= 1;
    057        /*@ ghost public int length; */
    058
    059        /** Return the number of identifiers in <code>this</code>. */
    060        //@ ensures \result==length;
    061        //@ pure
    062        public abstract int size();
    063
    064        /**
    065         * Return the ith identifier of <code>this</code>.
    066         */
    067        //@ requires 0 <= i && i<length;
    068        //@ ensures \result != null;
    069        //@ pure
    070        public abstract Identifier identifierAt(int i);
    071
    072        /**
    073         * Return the location of the ith identifier of <code>this</code>.
    074         */
    075        //@ requires 0 <= i && i<length;
    076        //@ ensures \result != Location.NULL;
    077        //@ pure
    078        public abstract int locIdAt(int i);
    079
    080        /**
    081         * Return the location of the dot after the ith identifier of
    082         * <code>this</code>.
    083         */
    084        //@ requires 0 <= i && i<length-1;
    085        //@ ensures \result != Location.NULL;
    086        //@ pure
    087        public abstract int locDotAfter(int i);
    088
    089        /**
    090         * Return the first <code>len</code> identifiers in
    091         * <code>this</code> in an array.  Requires that <code>len</code>
    092         * be between 0 and length of <code>this</code> inclusive.
    093         */
    094        //@ requires 0 <= len && len <= length;
    095        //@ ensures \nonnullelements(\result);
    096        //@ ensures \result.length == len;
    097        //@ pure
    098        public abstract String[] toStrings(int len);
    099
    100        /**
    101         * Return all identifiers in <code>this</code> in an array.
    102         */
    103        //@ ensures \nonnullelements(\result);
    104        //@ ensures \result.length == length;
    105        //@ pure
    106        public String[] toStrings() {
    107            return toStrings(size());
    108        }
    109
    110        /**
    111         * Make a <code>Name</code> with the given identifiers and
    112         * locations.  Caller must forget about the Vecs/arrays passed
    113         * here.
    114         */
    115        //@ requires ids != null && locIds != null && locDots != null;
    116        //@ requires ids.count>0;
    117        //@ requires ids.count==locIds.length && ids.count==locDots.length+1;
    118        /*@ requires (\forall int i; (0 <= i && i<locIds.length)
    119                            ==> locIds[i] != Location.NULL); */
    120        /*@ requires (\forall int i; (0 <= i && i<locDots.length)
    121                            ==> locDots[i] != Location.NULL); */
    122        //@ ensures \result != null;
    123        //@ pure
    124        public static Name make(int[] locIds, int[] locDots, IdentifierVec ids) {
    125            int sz = ids.size();
    126            Assert.precondition(sz > 0 && locIds.length == sz
    127                            && locDots.length + 1 == sz);
    128            if (sz == 1)
    129                return SimpleName.make(ids.elementAt(0), locIds[0]);
    130            else
    131                return CompoundName.make(ids, locIds, locDots);
    132        }
    133
    134        /**
    135         * Make a <code>Name</code> whose locations are all
    136         * <code>loc</code> from a <code>String</code>.
    137         *
    138         * <p> This routine parses a non-empty <code>String</code> consisting
    139         * of a series of dot-separated components into a <code>Name</code>.
    140         *
    141         * precondition: <code>N.length()>0</code><p>
    142         */
    143        //@ requires N != null;
    144        //@ requires N.length()>0;
    145        //@ requires loc != Location.NULL;
    146        //@ ensures \result != null;
    147        //@ pure
    148        public static Name make(String N, int loc) {
    149            // Convert N to a list of its components:
    150            String[] components = javafe.filespace.StringUtil.parseList(N, '.');
    151            int sz = components.length;
    152            Assert.notFalse(sz>0);          //@ nowarn Pre;
    153
    154            // Convert the components to Identifiers:
    155            IdentifierVec ids = IdentifierVec.make();
    156            for(int i = 0; i < sz; i++)
    157                ids.addElement(Identifier.intern(components[i]));
    158
    159            if (sz == 1)
    160                return SimpleName.make(ids.elementAt(0), loc);
    161
    162            int[] newLocIds = new int[sz];
    163            int[] newLocDots = new int[sz-1];
    164            for(int i = 0; i < sz; i++)
    165                newLocIds[i] = loc;
    166            for(int i = 0; i < sz-1; i++)
    167                newLocDots[i] = loc;
    168
    169            return make(newLocIds, newLocDots, ids);
    170        }
    171
    172        /**
    173         * Return a <code>Name</code> consisting of the first
    174         * <code>len</code> identifiers of <code>this</code>.  Requires
    175         * that <code>len</code> is greater than zero and less than or
    176         * equal to the length of <code>this</code>.
    177         */
    178        //@ requires 0<len && len <= length;
    179        //@ ensures \result != null;
    180        //@ pure
    181        public abstract Name prefix(int len);
    182
    183        /**
    184         * Override getEndLoc so it refers to the actual end of us.
    185         */
    186        //@ pure
    187        public int getEndLoc() {
    188            return Location.inc(getStartLoc(),
    189                                Math.max(0, printName().length()-1));
    190        }
    191
    192        /**
    193         * Avoid allocating more than one of these.
    194         */
    195        //@ invariant \nonnullelements(emptyStringArray);
    196        //@ invariant emptyStringArray.length == 0;
    197        final protected static String[] emptyStringArray = new String[0];
    198
    199
    200
    201    // Generated boilerplate constructors:
    202
    203       /**
    204        * Construct a raw Name whose class invariant(s) have not
    205        * yet been established.  It is the caller's job to
    206        * initialize the returned node's fields so that any
    207        * class invariants hold.
    208        */
    209       //@ requires I_will_establish_invariants_afterwards;
    210       protected Name() {}    //@ nowarn Invariant,NonNullInit;
    211
    212       public void check() {
    213          super.check();
    214       }
    215
    216    }