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.logic;
009:
010: import de.uka.ilkd.key.logic.op.MapAsListFromQuantifiableVariableToInteger;
011: import de.uka.ilkd.key.logic.op.MapFromQuantifiableVariableToInteger;
012: import de.uka.ilkd.key.logic.op.QuantifiableVariable;
013:
014: public class RenameTable {
015:
016: public static final RenameTable EMPTY_TABLE = new EmptyRenameTable();
017:
018: /**
019: * local map mapping a QuantifiableVariable object to an abstract name. This map
020: * is allowed to hide bound renaming of the parent table.
021: */
022: private final MapFromQuantifiableVariableToInteger localRenamingTable;
023:
024: /**
025: * the maximal value of an abstract name
026: */
027: private final int max;
028:
029: /** the parent renaming table */
030: private final RenameTable parent;
031:
032: public RenameTable(RenameTable parent,
033: MapFromQuantifiableVariableToInteger localTable, int newMax) {
034: this .parent = parent;
035: this .localRenamingTable = localTable;
036: max = newMax;
037: }
038:
039: /**
040: * returns true iff the given variable is mapped to an abstract name.
041: * The test is performed in the local as well as in the parent
042: * renaming table.
043: * @param n the QuantifiableVariable object the existence of an abstract name is
044: * checked.
045: * @return true if <code>n</code> has been already assigned to an
046: * abstract name
047: */
048: public boolean contains(QuantifiableVariable n) {
049: return localRenamingTable.containsKey(n) || parent.contains(n);
050: }
051:
052: /**
053: * does nearly the same as {@link #contains(QuantifiableVariable)} but performs
054: * the test only on the local table
055: * @param n the QuantifiableVariable object the existence of an abstract name is
056: * checked.
057: * @return true if <code>n</code> has been already locally
058: * assigned to an abstract name
059: */
060: public boolean containsLocally(QuantifiableVariable n) {
061: return localRenamingTable.containsKey(n);
062: }
063:
064: /**
065: * tests if both QuantifiableVariables are assigned to the same abstract
066: * name (locally or by the parent)
067: * @param n1 one of the QuantifiableVariables to be tested iff they have
068: * been assigned the same abstract name
069: * @param n2 one of the QuantifiableVariables to be tested
070: * @return true iff <code>n1</code> and <code>n2</code> are mapped
071: * to the same abstract name
072: */
073: public boolean sameAbstractName(QuantifiableVariable n1,
074: QuantifiableVariable n2) {
075: if (containsLocally(n1)) {
076: return localRenamingTable.get(n1) == localRenamingTable
077: .get(n2);
078: } else {
079: return parent.sameAbstractName(n1, n2);
080: }
081: }
082:
083: private Integer createNewAbstractName() {
084: if (max == Integer.MAX_VALUE) {
085: throw new IllegalStateException(
086: "Overflow in renaming table. Why on earth "
087: + "are there " + Integer.MAX_VALUE
088: + " + 1 variables to be renamed?");
089: }
090:
091: return new Integer(max + 1);
092: }
093:
094: /**
095: * assigns both QuantifiableVariable objects the same abstract name
096: */
097: public RenameTable assign(QuantifiableVariable n1,
098: QuantifiableVariable n2) {
099: final Integer newAbstractName = createNewAbstractName();
100: return new RenameTable(parent, localRenamingTable.put(n1,
101: newAbstractName).put(n2, newAbstractName),
102: newAbstractName.intValue());
103: }
104:
105: /**
106: * creates a nested renaimg table with <code>this</code>
107: * as parent
108: */
109: public RenameTable extend() {
110: return new RenameTable(this ,
111: MapAsListFromQuantifiableVariableToInteger.EMPTY_MAP,
112: createNewAbstractName().intValue());
113: }
114:
115: /**
116: * toString
117: */
118: public String toString() {
119: return localRenamingTable + " \n parent:" + parent;
120: }
121:
122: private static class EmptyRenameTable extends RenameTable {
123:
124: private EmptyRenameTable() {
125: super (
126: null,
127: MapAsListFromQuantifiableVariableToInteger.EMPTY_MAP,
128: 0);
129: }
130:
131: /**
132: * returns true iff the given name is mapped to an abstract name.
133: * The test is performed in the local as well as in the parent
134: * renaming table.
135: * @param n the QuantifiableVariable object the existence of an abstract name is
136: * checked.
137: * @return true if <code>n</code> has been already assigned to an
138: * abstract name
139: */
140: public boolean contains(QuantifiableVariable n) {
141: return false;
142: }
143:
144: /**
145: * does nearly the same as {@link #contains(QuantifiableVariable)} but performs
146: * the test only on the local table-
147: * @param n the QuantifiableVariable object the existence of an abstract name is
148: * checked.
149: * @return true if <code>n</code> has been already locally
150: * assigned to an abstract name
151: */
152: public boolean containsLocally(QuantifiableVariable n) {
153: return false;
154: }
155:
156: /**
157: * tests if both QuantifiableVariable object are assigned to the same abstract
158: * name (locally or by the parent)
159: * @param n1 one of the QuantifiableVariable objects to be tested iff they have
160: * been assigned the same abstract name
161: * @param n2 one of the QuantifiableVariable objects to be tested
162: * @return true iff <code>n1</code> and <code>n2</code> are mapped
163: * to the same abstract name
164: */
165: public boolean sameAbstractName(QuantifiableVariable n1,
166: QuantifiableVariable n2) {
167: return false;
168: }
169:
170: public String toString() {
171: return "empty";
172: }
173: }
174:
175: public RenameTable parent() {
176: return parent;
177: }
178: }
|