001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.java.reference;
012:
013: import de.uka.ilkd.key.java.*;
014: import de.uka.ilkd.key.java.visitor.Visitor;
015: import de.uka.ilkd.key.logic.ProgramElementName;
016: import de.uka.ilkd.key.logic.op.ProgramSV;
017: import de.uka.ilkd.key.logic.op.SchemaVariable;
018: import de.uka.ilkd.key.rule.MatchConditions;
019: import de.uka.ilkd.key.util.Debug;
020: import de.uka.ilkd.key.util.ExtList;
021:
022: /**
023: * Field reference.
024: * @author <TT>AutoDoc</TT>
025: */
026: public class SchematicFieldReference extends FieldReference implements
027: MemberReference, ReferenceSuffix, TypeReferenceContainer,
028: ExpressionContainer {
029:
030: /**
031: * Reference suffix
032: */
033: protected final SchemaVariable schemaVariable;
034:
035: public SchematicFieldReference(SchemaVariable pe,
036: ReferencePrefix prefix) {
037: this .schemaVariable = pe;
038: this .prefix = prefix;
039: }
040:
041: public SchematicFieldReference(ExtList children,
042: ReferencePrefix prefix) {
043: this .schemaVariable = (SchemaVariable) children
044: .get(SchemaVariable.class);
045: this .prefix = prefix;
046: }
047:
048: /**
049: * Returns the number of children of this node.
050: * @return an int giving the number of children of this node
051: */
052: public int getChildCount() {
053: int result = 0;
054: if (prefix != null)
055: result++;
056: if (schemaVariable != null)
057: result++;
058: return result;
059: }
060:
061: /**
062: * Returns the child at the specified index in this node's "virtual"
063: * child array
064: * @param index an index into this node's "virtual" child array
065: * @return the program element at the given position
066: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
067: * of bounds
068: */
069: public ProgramElement getChildAt(int index) {
070: if (prefix != null) {
071: if (index == 0)
072: return prefix;
073: index--;
074: }
075: if (schemaVariable != null) {
076: if (index == 0)
077: return (ProgramSV) schemaVariable;
078: }
079: throw new ArrayIndexOutOfBoundsException();
080: }
081:
082: /**
083: * Get reference prefix.
084: * @return the reference prefix.
085: */
086: public ReferencePrefix getReferencePrefix() {
087: return prefix;
088: }
089:
090: /**
091: * Get reference prefix.
092: * @return the reference prefix.
093: */
094: public ReferenceSuffix getReferenceSuffix() {
095: return (ProgramSV) schemaVariable;
096: }
097:
098: /**
099: * Set reference prefix.
100: * @author VK
101: */
102: public ReferencePrefix setReferencePrefix(ReferencePrefix rp) {
103: return new SchematicFieldReference(schemaVariable, rp);
104: }
105:
106: /**
107: * Get the number of type references in this container.
108: * @return the number of type references.
109: */
110:
111: public int getTypeReferenceCount() {
112: return (prefix instanceof TypeReference) ? 1 : 0;
113: }
114:
115: /**
116: * Return the type reference at the specified index in this node's
117: * "virtual" type reference array.
118: * @param index an index for a type reference.
119: * @return the type reference with the given index.
120: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
121: * of bounds.
122: */
123: public TypeReference getTypeReferenceAt(int index) {
124: if (prefix instanceof TypeReference && index == 0) {
125: return (TypeReference) prefix;
126: }
127: throw new ArrayIndexOutOfBoundsException();
128: }
129:
130: /**
131: * Get the number of expressions in this container.
132: * @return the number of expressions.
133: */
134: public int getExpressionCount() {
135: return (prefix instanceof Expression) ? 1 : 0;
136: }
137:
138: /**
139: * Return the expression at the specified index in this node's
140: * "virtual" expression array.
141: * @param index an index for an expression.
142: * @return the expression with the given index.
143: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
144: * of bounds.
145: */
146: public Expression getExpressionAt(int index) {
147: if (prefix instanceof Expression && index == 0) {
148: return (Expression) prefix;
149: }
150: throw new ArrayIndexOutOfBoundsException();
151: }
152:
153: public SourceElement getFirstElement() {
154: return (prefix == null) ? (ProgramSV) schemaVariable : prefix
155: .getFirstElement();
156: }
157:
158: public ProgramElementName getProgramElementName() {
159: return (ProgramElementName) schemaVariable.name();
160: }
161:
162: /**
163: * pretty print
164: */
165: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
166: p.printFieldReference((FieldReference) this );
167: }
168:
169: /**
170: * calls the corresponding method of a visitor in order to
171: * perform some action/transformation on this element
172: * @param v the Visitor
173: */
174: public void visit(Visitor v) {
175: v.performActionOnSchematicFieldReference(this );
176: }
177:
178: public MatchConditions match(SourceData source,
179: MatchConditions matchCond) {
180: ProgramElement src = source.getSource();
181: if (!(src instanceof FieldReference)) {
182: Debug
183: .out(
184: "Program match failed. SchematicFieldReferences matches only FieldReferences (pattern, source)",
185: this , src);
186: return null;
187: }
188:
189: final SourceData newSource = new SourceData(src, 0, source
190: .getServices());
191:
192: matchCond = super .matchChildren(newSource, matchCond, 0);
193:
194: if (matchCond == null) {
195: return null;
196: }
197: source.next();
198: return matchCond;
199: }
200:
201: }
|