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: package de.uka.ilkd.key.java;
009:
010: /**
011: * This class keeps track of the next element to match, which is provided by
012: * calling method {@link #getSource()}. The rough idea is to store the parent ast
013: * node and the index of the child which has to be matched (for convenience reasons
014: * <tt>-1</tt> encodes that the parent node itself has to be matched).
015: *
016: * This kind of wrapping is useful when matching list schemavariables.
017: */
018: public class SourceData {
019:
020: /**
021: * the program element being either the parent of the program element to be matched or
022: * the element itself depending on the value of childPos
023: */
024: private ProgramElement element;
025:
026: /** the position of the children of element which has to be matched
027: * against the pattern. If <tt>childPos</tt> is <tt>-1</tt> then <tt>element</tt> has to be matched.
028: */
029: private int childPos;
030:
031: /** the services */
032: private final Services services;
033:
034: /**
035: * creates a new source data object with parent node <tt>element</tt> whose
036: * <tt>childPos</tt>-th child has to be matched (-1 denotes <tt>element</tt> itself
037: * has to be matched
038: * @param element the ProgramElement
039: * @param childPos the int giving the index of the child of <tt>element</tt> to be matched
040: * @param services the Services
041: */
042: public SourceData(ProgramElement element, int childPos,
043: Services services) {
044: this .services = services;
045: this .element = element;
046: this .childPos = childPos;
047: }
048:
049: /**
050: * returns index of the child to be matched
051: * @return an int which is <tt>-1</tt> if @link #getElement()
052: * has to be matched itself otherwise it refers to the index of the child
053: * of <tt>element</tt> to be matched
054: */
055: public int getChildPos() {
056: return childPos;
057: }
058:
059: /**
060: * sets the index of the child to be matched
061: * @param childPos the int with the new index
062: */
063: public void setChildPos(int childPos) {
064: this .childPos = childPos;
065: }
066:
067: /**
068: * returns always the parent node
069: * @return the parent node
070: */
071: public ProgramElement getElement() {
072: return element;
073: }
074:
075: /**
076: * sets the parent node
077: * @param element the ProgramElement used as new parent node
078: */
079: public void setElement(ProgramElement element) {
080: this .element = element;
081: }
082:
083: /**
084: * returns the element to be matched, i.e. if @link #getChildPos() is <tt>-1</tt>
085: * it returns @link #getElement()
086: * otherwise it returns the getChildPos()-th child or <tt>null</tt> if the returned
087: * child position is out of bound.
088: * @return the ProgramElement to be matched next or <tt>null</tt> if there is no such
089: * element
090: */
091: public ProgramElement getSource() {
092: if (childPos == -1)
093: return element;
094:
095: final NonTerminalProgramElement ntpe = (NonTerminalProgramElement) element;
096:
097: if (childPos < ntpe.getChildCount()) {
098: return ntpe.getChildAt(childPos);
099: } else {
100: return null;
101: }
102: }
103:
104: /**
105: * increments the child position by one, this means moving on to the next sibling
106: * (or the first child if childPos has been <tt>-1</tt> before
107: */
108: public void next() {
109: childPos++;
110: }
111:
112: /**
113: * returns the services object
114: * @return the services object
115: */
116: public Services getServices() {
117: return services;
118: }
119:
120: /**
121: * toString
122: */
123: public String toString() {
124: return "Source:" + element + " child: " + childPos;
125: }
126:
127: }
|