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 18.01.2005
011: */package de.uka.ilkd.key.logic.op;
012:
013: import java.util.HashMap;
014: import java.util.Iterator;
015: import java.util.List;
016:
017: import de.uka.ilkd.key.java.Services;
018: import de.uka.ilkd.key.logic.Name;
019: import de.uka.ilkd.key.logic.ProgramElementName;
020: import de.uka.ilkd.key.logic.sort.ArrayOfSort;
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: * Non Rigid Fucntion with explicit dependencies. This means a list of
027: * location of whose and only whose value the interpretation of the
028: * function symbol depends.
029: * (May be generalized to more than locations in future)
030: *
031: * The list of dependencies may be partitioned into several lists.
032: */
033: public class NRFunctionWithExplicitDependencies extends
034: NonRigidFunction {
035:
036: public static final char DEPENDENCY_LIST_STARTER = '[';
037: public static final char DEPENDENCY_ELEMENT_SEPARATOR = ';';
038: public static final char DEPENDENCY_LIST_SEPARATOR = '|';
039: public static final char DEPENDENCY_LIST_END = ']';
040:
041: /**
042: * Pseudo-location used to separate the partitions of the dependency list.
043: * (this is necessary because currently all partitions are stored in a
044: * single ArrayOfLocation; when/if immutable lists of ArrayOfLocation
045: * become possible, one of these should be used instead)
046: */
047: private static final Location PARTITION_SEPARATOR = new LocationVariable(
048: new ProgramElementName(""), Sort.NULL);
049:
050: // HACK. Need more general framework for creating such functions see also
051: // ArrayOp, AttributeOp
052: // maps name -> mapDep2Op, where
053: // mapDep2Op maps dependency-array -> op
054: private static HashMap pool = new HashMap();
055:
056: /**
057: * retrieves the non-rigid function with the given name and dependencies
058: * or returns null if no such function symbol exists
059: * @param name the Name of the function symbol to look for
060: * @param dependencies the ArrayOfLocation with the dependencies
061: * @return the non-rigid function symbol
062: */
063: public static NRFunctionWithExplicitDependencies getSymbol(
064: Name name, ArrayOfLocation dependencies) {
065: HashMap mapDep2Op = (HashMap) pool.get(name);
066: NRFunctionWithExplicitDependencies op = (NRFunctionWithExplicitDependencies) mapDep2Op
067: .get(dependencies);
068: return op;
069: }
070:
071: /**
072: * retrieves the non-rigid function with the given name and dependencies
073: * and creates one if not available
074: * @param name the Name of the function symbol to look for
075: * @param sort the Sort of the function symbol
076: * @param argSorts the array of Sorts for the arguments
077: * @param dependencies the array of Locations describing the dependencies
078: * @return the non-rigid function symbol
079: */
080: public static NRFunctionWithExplicitDependencies getSymbol(
081: Name name, Sort sort, Sort[] argSorts,
082: Location[] dependencies) {
083: return getSymbol(name, sort, new ArrayOfSort(argSorts),
084: new ArrayOfLocation(dependencies));
085: }
086:
087: /**
088: * retrieves the non-rigid function with the given name and dependencies
089: * and creates one if not available
090: * @param name the Name of the function symbol to look for
091: * @param sort the Sort of the function symbol
092: * @param argSorts the ArrayOfSort for the arguments
093: * @param depList partitioned dependencies as a list of ArrayOfLocation
094: * @return the non-rigid function symbol
095: */
096: public static NRFunctionWithExplicitDependencies getSymbol(
097: Name name, Sort sort, ArrayOfSort argSorts,
098: List /*ArrayOfLocation*/depList) {
099: ListOfLocation deps = SLListOfLocation.EMPTY_LIST;
100: Iterator it = depList.iterator();
101: while (it.hasNext()) {
102: ArrayOfLocation partition = (ArrayOfLocation) it.next();
103: for (int i = 0; i < partition.size(); i++) {
104: deps = deps.append(partition.getLocation(i));
105: }
106: if (it.hasNext()) {
107: deps = deps.append(PARTITION_SEPARATOR);
108: }
109: }
110: return getSymbol(name, sort, argSorts, new ArrayOfLocation(deps
111: .toArray()));
112: }
113:
114: /**
115: * retrieves the non-rigid function with the given name and dependencies
116: * and creates one if not available
117: * @param name the Name of the function symbol to look for
118: * @param sort the Sort of the function symbol
119: * @param argSorts the ArrayOfSort for the arguments
120: * @param dependencies the ArrayOfLocation with the dependencies
121: * @return the non-rigid function symbol
122: */
123: public static NRFunctionWithExplicitDependencies getSymbol(
124: Name name, Sort sort, ArrayOfSort argSorts,
125: ArrayOfLocation dependencies) {
126:
127: HashMap mapDep2Op = (HashMap) pool.get(name);
128: if (mapDep2Op == null) {
129: mapDep2Op = new HashMap();
130: pool.put(name, mapDep2Op);
131: }
132: NRFunctionWithExplicitDependencies op = (NRFunctionWithExplicitDependencies) mapDep2Op
133: .get(dependencies);
134:
135: if (op == null) {
136: op = new NRFunctionWithExplicitDependencies(name, sort,
137: argSorts, dependencies);
138: mapDep2Op.put(name, op);
139: }
140:
141: return op;
142: }
143:
144: /**
145: * the meaning of this function symbol depends on the values of the
146: * locations contained in this array;
147: */
148: private final ArrayOfLocation dependencies;
149:
150: /**
151: * the list of dependencies *without* markers for partition boundaries
152: */
153: private final ArrayOfLocation unpartitionedDependencies;
154:
155: /** the common name of the class of symbols */
156: private final String classifier;
157:
158: /**
159: * creates a non rigid function with given signaturen and dependencies
160: * @param name the Name of the non-rigid function symbol
161: * @param sort the Sort of the symbol
162: * @param argSorts the ArrayOfSort defining the argument sorts
163: * @param dependencies the ArrayOfLocation whose values influence
164: * the meaning of this symbol
165: */
166: private NRFunctionWithExplicitDependencies(Name name, Sort sort,
167: ArrayOfSort argSorts, ArrayOfLocation dependencies) {
168: super (name, sort, argSorts);
169: this .dependencies = dependencies;
170: this .classifier = name.toString().substring(0,
171: name.toString().indexOf(DEPENDENCY_LIST_STARTER));
172:
173: ListOfLocation unpartitionedDeps = SLListOfLocation.EMPTY_LIST;
174: for (int i = 0; i < dependencies.size(); i++) {
175: Location dep = dependencies.getLocation(i);
176: if (dep != PARTITION_SEPARATOR) {
177: unpartitionedDeps = unpartitionedDeps.append(dep);
178: }
179: }
180: unpartitionedDependencies = new ArrayOfLocation(
181: unpartitionedDeps.toArray());
182: }
183:
184: public String classifier() {
185: return classifier;
186: }
187:
188: /**
189: * two non-rigid function symbols can be matched if their list of
190: * dependencies match
191: */
192: public MatchConditions match(SVSubstitute subst,
193: MatchConditions mc, Services services) {
194: MatchConditions result = mc;
195: if (this == subst)
196: return result;
197: if (subst.getClass() != getClass()) {
198: Debug.out("FAILED matching. Incomaptible operators "
199: + "(template, operator)", this , subst);
200: return null;
201: }
202:
203: final NRFunctionWithExplicitDependencies nrFunc = (NRFunctionWithExplicitDependencies) subst;
204:
205: if (!(nrFunc.classifier.equals(classifier))) {
206: Debug.out("Operator do not belong to the same category:",
207: this , nrFunc);
208: return null;
209: }
210:
211: if (dependencies.size() == nrFunc.dependencies.size()) {
212: for (int i = 0, locs = dependencies.size(); i < locs; i++) {
213: result = dependencies.getLocation(i).match(
214: nrFunc.dependencies.getLocation(i), result,
215: services);
216: if (result == null) { // fail fast
217: Debug.out(
218: "FAILED. NRFuncWithExplicitDependences mismatch "
219: + "(template, operator)", this ,
220: nrFunc);
221: return null;
222: }
223: }
224: return result;
225: }
226: Debug
227: .out(
228: "FAILED matching. NRWithExplicitDependencies match "
229: + "failed because of incompatible locations (template, operator)",
230: this , subst);
231: return null;
232: }
233:
234: /**
235: * returns an array of all locations this function depends on
236: * @return the array of locations this function depends on
237: */
238: public ArrayOfLocation dependencies() {
239: return unpartitionedDependencies;
240: }
241:
242: public int getNumPartitions() {
243: int result = 1;
244: for (int i = 0; i < dependencies.size(); i++) {
245: if (dependencies.getLocation(i) == PARTITION_SEPARATOR) {
246: result++;
247: }
248: }
249: return result;
250: }
251:
252: /**
253: * returns the i-th partition of the locations this function depends on
254: */
255: public ArrayOfLocation getDependencies(int i) {
256: Debug.assertTrue(i >= 0);
257: ListOfLocation result = SLListOfLocation.EMPTY_LIST;
258: for (int j = 0; j < dependencies.size(); j++) {
259: if (dependencies.getLocation(j) == PARTITION_SEPARATOR) {
260: if (i == 0) {
261: break;
262: } else {
263: i--;
264: continue;
265: }
266: }
267: if (i == 0) {
268: result = result.append(dependencies.getLocation(j));
269: }
270: }
271: Debug.assertTrue(i == 0);
272: return new ArrayOfLocation(result.toArray());
273: }
274:
275: /**
276: * toString
277: */
278: public String toString() {
279: StringBuffer sb = new StringBuffer();
280: sb.append(name().toString());
281: sb.append(DEPENDENCY_LIST_STARTER);
282: for (int i = 0; i < dependencies.size(); i++) {
283: Location dep = dependencies.getLocation(i);
284: if (dep == PARTITION_SEPARATOR) {
285: sb.append(DEPENDENCY_LIST_SEPARATOR);
286: } else {
287: sb.append(dep);
288: sb.append(DEPENDENCY_ELEMENT_SEPARATOR);
289: }
290: }
291: sb.append(DEPENDENCY_LIST_END);
292: sb.append("(");
293: for (int i = 0; i < argSort().size(); i++) {
294: sb.append(argSort().getSort(i));
295: if (i < argSort().size() - 1) {
296: sb.append(",");
297: }
298: }
299: sb.append("):");
300: sb.append(sort());
301: return sb.toString();
302: }
303: }
|