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.rule.inst;
012:
013: import de.uka.ilkd.key.java.JavaProgramElement;
014: import de.uka.ilkd.key.logic.op.SchemaVariable;
015:
016: /** this class wrapps a MapFromSchemaVariableToJavaProgramElement and
017: * is used to store instantiations of schemavariables. The class is
018: * immutable, this means changing its content will result in creating
019: * a new object.
020: */
021: public class ProgramSVInstantiation {
022:
023: /** the empty instantiation */
024: public static final ProgramSVInstantiation EMPTY_PROGRAMSVINSTANTIATION = new ProgramSVInstantiation();
025:
026: /** the map with the instantiations */
027: private ListOfProgramSVEntry list = SLListOfProgramSVEntry.EMPTY_LIST;
028:
029: /** integer to cache the hashcode */
030: private int hashcode = 0;
031:
032: /** creates a new ProgramSVInstantiation object with an empty list */
033: private ProgramSVInstantiation() {
034: }
035:
036: /** creates a new ProgramSVInstantiation object using the given list
037: * @param list the ListFromSchemaVariableToJavaProgramElement with the
038: * instantiations
039: */
040: private ProgramSVInstantiation(ListOfProgramSVEntry list) {
041: this .list = list;
042: }
043:
044: /** adds the given pair to the instantiations. If the given
045: * SchemaVariable has been instantiated already, the new pair is
046: * taken without a warning.
047: * @param sv the SchemaVariable to be instantiated
048: * @param prgElement the JavaProgramElement The SchemaVariable is
049: * instantiated with
050: * @return ProgramSVInstantiation the new ProgramSVInstantiation
051: * containing the given pair
052: */
053: public ProgramSVInstantiation add(SchemaVariable sv,
054: JavaProgramElement prgElement) {
055: if (!isInstantiated(sv)) {
056: return new ProgramSVInstantiation(list
057: .prepend(new ProgramSVEntry(sv, prgElement)));
058: } else {
059: return replace(sv, prgElement);
060: }
061: }
062:
063: /** replaces the given pair in the instantiations. If the given
064: * SchemaVariable has been instantiated already, the new pair is
065: * taken without a warning.
066: * @param sv the SchemaVariable to be instantiated
067: * @param prgElement the JavaProgramElement The SchemaVariable is
068: * instantiated with
069: * @return ProgramSVInstantiation the new ProgramSVInstantiation
070: * containing the given pair
071: */
072: public ProgramSVInstantiation replace(SchemaVariable sv,
073: JavaProgramElement prgElement) {
074: ListOfProgramSVEntry result = SLListOfProgramSVEntry.EMPTY_LIST
075: .prepend(new ProgramSVEntry(sv, prgElement));
076: IteratorOfProgramSVEntry it = list.iterator();
077: while (it.hasNext()) {
078: ProgramSVEntry entry = it.next();
079: if (entry.key() != sv) {
080: result = result.prepend(entry);
081: }
082: }
083: return new ProgramSVInstantiation(result);
084: }
085:
086: /** returns true iff the sv has been instantiated already
087: * @return true iff the sv has been instantiated already
088: */
089: public boolean isInstantiated(SchemaVariable sv) {
090: IteratorOfProgramSVEntry it = list.iterator();
091: while (it.hasNext()) {
092: ProgramSVEntry entry = it.next();
093: if (entry.key() == sv) {
094: return true;
095: }
096: }
097: return false;
098: }
099:
100: /** returns the instantiation of the given SchemaVariable
101: * @return the JavaProgramElement the SchemaVariable will be
102: * instantiated with, null if no instantiation is stored
103: */
104: public JavaProgramElement getInstantiation(SchemaVariable sv) {
105: IteratorOfProgramSVEntry it = list.iterator();
106: while (it.hasNext()) {
107: ProgramSVEntry entry = it.next();
108: if (entry.key() == sv) {
109: return entry.value();
110: }
111: }
112: return null;
113: }
114:
115: /** returns iterator of the listped pair (SchemaVariables,
116: * JavaProgramElement)
117: * @return the
118: * IteratorOfEntryOfSchemaVariableAndJavaProgramElement
119: */
120: public IteratorOfProgramSVEntry iterator() {
121: return list.iterator();
122: }
123:
124: /** returns the number of SchemaVariables of which an
125: * instantiation is known
126: * @return int that is the number of SchemaVariables of which an
127: * instantiation is known
128: */
129: public int size() {
130: return list.size();
131: }
132:
133: /** returns true if the given object and this one have the same
134: * listpings
135: * @return true if the given object and this one have the same
136: * listpings
137: */
138: public boolean equals(Object obj) {
139: ProgramSVInstantiation cmp = null;
140: if (!(obj instanceof ProgramSVInstantiation)) {
141: return false;
142: } else {
143: cmp = (ProgramSVInstantiation) obj;
144: }
145: if (size() != cmp.size()) {
146: return false;
147: } else {
148: final IteratorOfProgramSVEntry it = iterator();
149: while (it.hasNext()) {
150: final ProgramSVEntry psv = it.next();
151: if (!psv.value()
152: .equals(cmp.getInstantiation(psv.key()))) {
153: return false;
154: }
155: }
156: return true;
157: }
158: }
159:
160: public int hashCode() {
161: if (hashcode == 0) {
162: int result = 17;
163: final IteratorOfProgramSVEntry it = iterator();
164: while (it.hasNext()) {
165: final ProgramSVEntry psv = it.next();
166: result = 37 * result + psv.key().hashCode()
167: + psv.value().hashCode();
168: }
169: hashcode = result;
170: }
171: return hashcode;
172: }
173:
174: /** toString */
175: public String toString() {
176: StringBuffer result = new StringBuffer(
177: "ProgramSVInstantiation:\n");
178: return (result.append(list.toString())).toString();
179: }
180: }
|