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: package de.uka.ilkd.key.logic;
011:
012: /**
013: * A Namespace keeps track of already used {@link Name}s and the objects
014: * carrying these names. These objects have to implement the interface
015: * {@link Named}. It is possible to have nested namespaces in order to
016: * represent different visibility scopes. An instance of Namespace can
017: * operate in normal and protocoled mode, where the protocoled mode
018: * keeps track of all new added names since the last call of {@link
019: * Namespace#startProtocol}.
020: */
021: public class Namespace implements java.io.Serializable {
022:
023: /**
024: * The fall-back namespace for symbols not present in this
025: * Namespace.
026: */
027: protected Namespace parent = null;
028:
029: /** The hashmap that maps a name to a symbols of that name if it
030: * is defined in this Namespace. */
031: protected HashMapFromNameToNamed symbols = null;
032:
033: /** One defined symbol. Many Namespaces, e.g. those generated when
034: * a quantified formula is parsed, define only one new symbol,
035: * and it would be a waste of time and space to create a hashmap for that.
036: * So {@link #symbols} is only initialized when there is more than one
037: * symbol in this namespace. Otherwise, <code>localSym</code> contains
038: * that symbol. */
039: protected Named localSym = null;
040:
041: /** The number of symbols defined in this namespace. This is different
042: * from <code>symbols.size()</code> because symbols might be null if
043: * there is only one symbol in this Namespace. */
044: protected int numLocalSyms = 0;
045:
046: /** Additions can be "recorded" here */
047: protected HashMapFromNameToNamed protocol = null;
048:
049: /** Construct an empty Namespace without a parent namespace. */
050: public Namespace() {
051: this .parent = null;
052: }
053:
054: /** Construct an empty Namespace with protocol <code>protocol</code>
055: * and without a parent namespace. */
056: public Namespace(HashMapFromNameToNamed protocol) {
057: this .parent = null;
058: this .protocol = protocol;
059: }
060:
061: /** Construct a Namespace that uses <code>parent</code> as a fallback
062: * for finding symbols not defined in this one. */
063: public Namespace(Namespace parent) {
064: this .parent = parent;
065: }
066:
067: /** Construct a Namespace that uses <code>parent</code> as a fallback
068: * for finding symbols not defined in this one. Put an entry for
069: * <code>sym</code> in this one. */
070: public Namespace(Namespace parent, Named sym) {
071: this .parent = parent;
072: add(sym);
073: }
074:
075: /** Adds the object <code>sym</code> to this Namespace.
076: * If an object with the same name is already there, it is quietly
077: * replaced by <code>sym</code>. Use addSafely() instead if possible.*/
078: public void add(Named sym) {
079: if (numLocalSyms > 0) {
080: if (symbols == null) {
081: symbols = new HashMapFromNameToNamed();
082: symbols.put(localSym.name(), localSym);
083: localSym = null;
084: }
085: symbols.put(sym.name(), sym);
086: } else
087: localSym = sym;
088: numLocalSyms++;
089: if (protocol != null) {
090: protocol.put(sym.name(), sym);
091: }
092: }
093:
094: /** Adds the object <code>sym</code> to this namespace.
095: * Throws a runtime exception if an object with the same name is
096: * already there. */
097: public void addSafely(Named sym) {
098: if (lookup(sym.name()) != null) {
099: throw new RuntimeException("Name already in namespace: "
100: + sym.name());
101: }
102: add(sym);
103: }
104:
105: /** "remember" all additions from now on */
106: public void startProtocol() {
107: protocol = new HashMapFromNameToNamed();
108: }
109:
110: /** gets symbols added since last <code>startProtocol()</code>;
111: * resets the protocol */
112: public IteratorOfNamed getProtocolled() {
113: if (protocol == null) {
114: return SLListOfNamed.EMPTY_LIST.iterator();
115: }
116: IteratorOfNamed it = protocol.values();
117: protocol = null;
118: return it;
119: }
120:
121: protected Named lookupLocally(Name name) {
122: if (numLocalSyms == 0)
123: return null;
124: if (numLocalSyms > 1)
125: return symbols.get(name);
126: if (localSym.name().equals(name)) {
127: return localSym;
128: } else
129: return null;
130: }
131:
132: /** creates a new Namespace that has this as parent, and contains
133: * an entry for <code>sym</code>.
134: * @return the new Namespace
135: */
136: public Namespace extended(Named sym) {
137: return new Namespace(this , sym);
138: }
139:
140: public Namespace extended(ListOfNamed ext) {
141: Namespace res = new Namespace(this );
142: IteratorOfNamed it = ext.iterator();
143: while (it.hasNext()) {
144: res.add(it.next());
145: }
146: return res;
147: }
148:
149: /**
150: * looks if a registered object is declared in this namespace, if
151: * negative it asks its parent
152: * @param name a Name representing the name of the symbol to look for
153: * @return Object with name "name" or null if no such an object
154: * has been found
155: */
156: public Named lookup(Name name) {
157: Named symbol = lookupLocally(name);
158: if (symbol == null && parent != null) {
159: return parent.lookup(name);
160: } else {
161: return symbol;
162: }
163: }
164:
165: /** returns list of the elements (not the keys) in this
166: * namespace (not about the one of the parent)
167: * @return the list of the named objects
168: */
169: public ListOfNamed elements() {
170: ListOfNamed list = SLListOfNamed.EMPTY_LIST;
171:
172: if (numLocalSyms == 1) {
173: list = list.prepend(localSym);
174: } else if (numLocalSyms > 1) {
175: IteratorOfNamed it = symbols.values();
176: while (it.hasNext()) {
177: list = list.prepend(it.next());
178: }
179: }
180:
181: return list;
182: }
183:
184: public ListOfNamed allElements() {
185: if (parent == null) {
186: return elements();
187: } else {
188: return elements().append(parent().allElements());
189: }
190: }
191:
192: /** returns the fall-back Namespace of this Namespace, i.e. the one
193: * where symbols are looked up that are not found in this one.
194: */
195: public Namespace parent() {
196: return parent;
197: }
198:
199: public String toString() {
200: String res = "Namespace: [local:" + localSym + ", " + symbols;
201: if (parent != null)
202: res = res + "; parent:" + parent;
203: return res + "]";
204: }
205:
206: public void add(Namespace source) {
207: IteratorOfNamed it = source.elements().iterator();
208: while (it.hasNext()) {
209: add(it.next());
210: }
211:
212: }
213:
214: public void add(ListOfNamed l) {
215: IteratorOfNamed it = l.iterator();
216: while (it.hasNext()) {
217: add(it.next());
218: }
219: }
220:
221: public Namespace copy() {
222: Namespace copy;
223: if (protocol != null) {
224: copy = new Namespace((HashMapFromNameToNamed) protocol
225: .clone());
226: } else {
227: copy = new Namespace();
228: }
229: //%%%%make more efficient!!!
230: IteratorOfNamed it = allElements().iterator();
231: while (it.hasNext()) {
232: copy.add(it.next());
233: }
234: return copy;
235: }
236:
237: public void reset() {
238: parent = null;
239: symbols = null;
240: localSym = null;
241: numLocalSyms = 0;
242: }
243:
244: }
|