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: * Created on 14.12.2004
011: */
012: package de.uka.ilkd.key.logic.op;
013:
014: import java.lang.ref.WeakReference;
015: import java.math.BigInteger;
016: import java.util.WeakHashMap;
017:
018: import de.uka.ilkd.key.java.Services;
019: import de.uka.ilkd.key.logic.Name;
020: import de.uka.ilkd.key.logic.Term;
021: import de.uka.ilkd.key.logic.sort.Sort;
022: import de.uka.ilkd.key.rule.MatchConditions;
023: import de.uka.ilkd.key.util.Debug;
024:
025: /**
026: * @author bubel
027: */
028: public class AnonymousUpdate implements IUpdateOperator {
029:
030: private final Name name;
031:
032: private static WeakHashMap operatorPool = new WeakHashMap(20);
033: private static BigInteger globalCounter = BigInteger.ZERO;
034:
035: /**
036: *
037: */
038: private AnonymousUpdate(Name name) {
039: this .name = name;
040: }
041:
042: /**
043: * returns the anonymous update of the given name or creates a
044: * new one if it does not exist
045: * @param name the Name of the anon update operator to look for
046: * @return the anonymous update operator
047: */
048: public static AnonymousUpdate getAnonymousOperator(Name name) {
049: WeakReference anonymousUpdateReference = (WeakReference) operatorPool
050: .get(name);
051: if (anonymousUpdateReference == null
052: || anonymousUpdateReference.get() == null) {
053: // wrapping attributeOp in a weak reference is necessary as
054: // it contains a strong reference to its key
055: anonymousUpdateReference = new WeakReference(
056: new AnonymousUpdate(name));
057: operatorPool.put(name, anonymousUpdateReference);
058: }
059: return (AnonymousUpdate) anonymousUpdateReference.get();
060: }
061:
062: /**
063: * returns a new anonymous update
064: * @return a new anonymous update
065: */
066: public static AnonymousUpdate getNewAnonymousOperator() {
067: WeakReference anonymousUpdateReference = null;
068: Name uniqueName;
069: do {
070: globalCounter = globalCounter.add(BigInteger.ONE);
071: uniqueName = new Name("*:=*" + globalCounter);
072: anonymousUpdateReference = (WeakReference) operatorPool
073: .get(uniqueName);
074: } while (anonymousUpdateReference != null);
075: // wrapping attributeOp in a weak reference is necessary as
076: // it contains a strong reference to its key
077: anonymousUpdateReference = new WeakReference(
078: new AnonymousUpdate(uniqueName));
079: operatorPool.put(uniqueName, anonymousUpdateReference);
080: return (AnonymousUpdate) anonymousUpdateReference.get();
081: }
082:
083: /** @return name of the operator */
084: public Name name() {
085: return name;
086: }
087:
088: /**
089: * returns the arity of the operator
090: */
091: public int arity() {
092: return 1;
093: }
094:
095: /**
096: * returns the sort a term would have if constructed with this operator and
097: * the given sunterms. It is assumed that the term would be allowed if
098: * constructed.
099: *
100: * @param term
101: * an array of Term containing the subterms of a (potential)
102: * simultaneous update term
103: * @return sort of the simultaneous update term consisting of the given
104: * subterms, if this op would be the top symbol
105: */
106: public Sort sort(Term[] term) {
107: return term[targetPos()].sort();
108: }
109:
110: /**
111: * @return true if the value of "term" having this operator as top-level
112: * operator and may not be changed by modalities
113: */
114: public boolean isRigid(Term term) {
115: return true;
116: }
117:
118: /**
119: * checks whether the top level structure of the given {@link Term}is
120: * syntactically valid, given the assumption that the top level operator of
121: * the term is the same as this Operator. The assumption that the top level
122: * operator and the operator are equal is NOT checked.
123: *
124: * @return true iff the top level structure of the {@link Term}is valid.
125: */
126: public boolean validTopLevel(Term term) {
127: return true;
128: }
129:
130: public int entryBegin(int locPos) {
131: Debug.fail("Method not implemented for anonymous update");
132: return 0; // unreachable
133: }
134:
135: public int entryEnd(int locPos) {
136: Debug.fail("Method not implemented for anonymous update");
137: return 0; // unreachable
138: }
139:
140: public int[] getLocationPos(Operator loc) {
141: Debug.fail("Method not implemented for anonymous update");
142: return null; // unreachable
143: }
144:
145: public Location location(int n) {
146: Debug.fail("Method not implemented for anonymous update");
147: return null; // unreachable
148: }
149:
150: public Term location(Term t, int n) {
151: Debug.fail("Method not implemented for anonymous update");
152: return null; // unreachable
153: }
154:
155: public int locationCount() {
156: return 0;
157: }
158:
159: public ArrayOfLocation locationsAsArray() {
160: return new ArrayOfLocation();
161: }
162:
163: public int locationSubtermsBegin(int locPos) {
164: Debug.fail("Method not implemented for anonymous update");
165: return 0; // unreachable
166: }
167:
168: public int locationSubtermsEnd(int locPos) {
169: Debug.fail("Method not implemented for anonymous update");
170: return 0; // unreachable
171: }
172:
173: public IUpdateOperator replaceLocations(Location[] newLocs) {
174: return this ;
175: }
176:
177: public Term value(Term t, int n) {
178: Debug.fail("Method not implemented for anonymous update");
179: return null; // unreachable
180: }
181:
182: public int valuePos(int locPos) {
183: Debug.fail("Method not implemented for anonymous update");
184: return 0; // unreachable
185: }
186:
187: /**
188: * the position of the term the anonymous update is applied to
189: * @return the sub term position of the target term
190: */
191: public int targetPos() {
192: return arity() - 1;
193: }
194:
195: /**
196: * @return the index of the subterm representing the formula/term the update
197: * is applied to
198: */
199: public Term target(Term t) {
200: return t.sub(targetPos());
201: }
202:
203: public MatchConditions match(SVSubstitute subst,
204: MatchConditions mc, Services services) {
205: if (this == subst)
206: return mc;
207: return null;
208: }
209:
210: public String toString() {
211: return "anonUpdate(" + name() + ")";
212: }
213: }
|