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 }