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;
012:
013: import de.uka.ilkd.key.rule.MatchConditions;
014: import de.uka.ilkd.key.util.Debug;
015: import de.uka.ilkd.key.util.ExtList;
016:
017: /**
018: * Top level implementation of a Java {@link NonTerminalProgramElement}.
019: * taken from COMPOST and changed to achieve an immutable structure
020: */
021: public abstract class JavaNonTerminalProgramElement extends
022: JavaProgramElement implements NonTerminalProgramElement {
023:
024: private int hashCode;
025:
026: /**
027: * Java program element.
028: */
029:
030: public JavaNonTerminalProgramElement() {
031: }
032:
033: /**
034: * Java program element.
035: * @param list as ExtList with children of the node
036: */
037:
038: public JavaNonTerminalProgramElement(ExtList list) {
039: super (list);
040: }
041:
042: public JavaNonTerminalProgramElement(PositionInfo pos) {
043: super (pos);
044: }
045:
046: public JavaNonTerminalProgramElement(ExtList children,
047: PositionInfo pos) {
048: super (children, pos);
049: }
050:
051: /**
052: * returns the index of element el in array arr
053: * @param arr the array where the element is looked for
054: * @param el the element to look for
055: * @return the index of the element (-1 if not found)
056: */
057: protected int getArrayPos(ArrayOfProgramElement arr,
058: ProgramElement el) {
059: for (int i = 0, sz = arr.size(); i < sz; i++) {
060: if (arr.getProgramElement(i) == el) {
061: return i;
062: }
063: }
064: return -1;
065: }
066:
067: /** commented in interface SourceElement. Overwrites the default
068: * method implementation in ProgramElement by descending down to
069: * the children.
070: */
071: public boolean equalsModRenaming(SourceElement se,
072: NameAbstractionTable nat) {
073: if (this .getClass() != se.getClass()) {
074: return false;
075: }
076: final JavaNonTerminalProgramElement jnte = (JavaNonTerminalProgramElement) se;
077:
078: if (jnte.getChildCount() != getChildCount()) {
079: return false;
080: }
081:
082: for (int i = 0, cc = getChildCount(); i < cc; i++) {
083: if (!getChildAt(i).equalsModRenaming(jnte.getChildAt(i),
084: nat)) {
085: return false;
086: }
087: }
088: return true;
089: }
090:
091: public boolean equals(Object o) {
092: return super .equals(o);
093: }
094:
095: public int hashCode() {
096: if (hashCode == 0) {
097: int result = 17;
098: result = 37 * result + getChildCount();
099: for (int i = 0, cc = getChildCount(); i < cc; i++) {
100: result = 37 * result + getChildAt(i).hashCode();
101: }
102: if (result == 0) {
103: hashCode = 1;
104: } else {
105: hashCode = result;
106: }
107: }
108: return hashCode;
109: }
110:
111: /**
112: * matches the source "text" (@link SourceData#getSource()) against the pattern represented
113: * by this object. In case of a successful match the resulting {@link MatchConditions} with
114: * the found instantiations of the schemavariables. If the match
115: * failed, <tt>null</tt> is returned instead.
116: *
117: * @param source the SourceData with the program element to match
118: * @param matchCond the MatchConditions found up to this point
119: * @return the resulting match conditions or <tt>null</tt> if the match failed
120: */
121: public MatchConditions match(SourceData source,
122: MatchConditions matchCond) {
123: final ProgramElement src = source.getSource();
124:
125: Debug.out("Program match start (template, source)", this , src);
126:
127: if (src == null) {
128: return null;
129: }
130:
131: if (src.getClass() != this .getClass()) {
132: Debug.out("Incompatible AST nodes (template, source)",
133: this , src);
134: Debug.out("Incompatible AST nodes (template, source)", this
135: .getClass(), src.getClass());
136: return null;
137: }
138:
139: final NonTerminalProgramElement ntSrc = (NonTerminalProgramElement) src;
140: final SourceData newSource = new SourceData(ntSrc, 0, source
141: .getServices());
142:
143: matchCond = matchChildren(newSource, matchCond, 0);
144:
145: if (matchCond == null) {
146: return null;
147: }
148:
149: source.next();
150: return matchCond;
151:
152: }
153:
154: /**
155: * used by @link matchChildren to decide if a found match is valid or if there are remaining
156: * source elements that have not been matched (in which case the match failed)
157: */
158: protected boolean compatibleBlockSize(int pos, int max) {
159: return pos >= max;
160: }
161:
162: /**
163: * matches successively all children of this current node. Thereby the
164: * <tt>offset</tt>-th child is matched against <code>source.getSource()</code>. The call
165: * <tt>source.next</tt> has to be done in the @link ProgramElement#match method
166: * of the currently matched child in case of a successful match. This is
167: * <em>not</em> done here (rationale: schemavariables matching on lists can be
168: * implemented easy).
169: *
170: *
171: * @param source the SourceData with the children to be matched
172: * @param matchCond the MatchConditions found so far
173: * @param offset the int denoting the index of the child to start with
174: * @return the resulting match conditions or <tt>null</tt> if matching failed
175: */
176: protected MatchConditions matchChildren(SourceData source,
177: MatchConditions matchCond, int offset) {
178:
179: for (int i = offset, sz = getChildCount(); i < sz; i++) {
180: matchCond = getChildAt(i).match(source, matchCond);
181: if (matchCond == null) {
182: return null;
183: }
184: }
185:
186: final NonTerminalProgramElement ntSrc = (NonTerminalProgramElement) source
187: .getElement();
188:
189: if (!compatibleBlockSize(source.getChildPos(), ntSrc
190: .getChildCount())) {
191: Debug.out("Source has unmatched elements.");
192: return null;
193: }
194:
195: return matchCond;
196: }
197: }
|