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;
012:
013: import de.uka.ilkd.key.java.ProgramElement;
014: import de.uka.ilkd.key.logic.Constraint;
015: import de.uka.ilkd.key.logic.PosInOccurrence;
016: import de.uka.ilkd.key.logic.Term;
017: import de.uka.ilkd.key.logic.op.*;
018: import de.uka.ilkd.key.rule.inst.SVInstantiations;
019: import de.uka.ilkd.key.util.Debug;
020:
021: /**
022: * A position taclet application object, contains already the information to
023: * which term/formula of the sequent the taclet is attached. The position
024: * information has been determined by matching the find-part of the
025: * corresponding taclet against the term described by the position
026: * information. If such a match has not been performed or a taclet is a no find
027: * taclet, a no position taclet object ({@link
028: * de.uka.ilkd.key.rule.NoPosTacletApp}) is used to keep track of the (partial)
029: * instantiation information.
030: */
031: public class PosTacletApp extends TacletApp {
032:
033: /** stores the information where the Taclet is to be applied. This means where
034: * the find section of the taclet matches
035: */
036: private PosInOccurrence pos;
037:
038: /** creates a PosTacletApp for the given taclet
039: * and a position information and CHECKS variable conditions as well as it
040: * resolves collisions
041: * @param taclet the FindTaclet
042: * @param pos the PosInOccurrence storing the position where to apply the
043: * Taclet
044: * @return new PosTacletApp or null if conditions (assertions) have been hurted
045: */
046: public static PosTacletApp createPosTacletApp(FindTaclet taclet,
047: PosInOccurrence pos) {
048: // no instantiations no checks are needed
049: return new PosTacletApp(taclet, pos);
050: }
051:
052: /** creates a PosTacletApp for the given taclet with some known instantiations
053: * and a position information
054: * and CHECKS variable conditions as well as it resolves
055: * collisions
056: * The ifInstantiations parameter is not
057: * matched against the if sequence, but only stored. For matching
058: * use the method "setIfFormulaInstantiations".
059: * @param taclet the FindTaclet
060: * @param instantiations the SVInstantiations
061: * @param pos the PosInOccurrence storing the position where to apply the
062: * Taclet
063: * @return new PosTacletApp or null if conditions (assertions) have been hurted
064: */
065: public static PosTacletApp createPosTacletApp(FindTaclet taclet,
066: SVInstantiations instantiations, PosInOccurrence pos) {
067: return createPosTacletApp(taclet, instantiations,
068: Constraint.BOTTOM, SetAsListOfMetavariable.EMPTY_SET,
069: null, pos);
070: }
071:
072: public static PosTacletApp createPosTacletApp(FindTaclet taclet,
073: SVInstantiations instantiations,
074: Constraint matchConstraint,
075: SetOfMetavariable matchNewMetavariables, PosInOccurrence pos) {
076: return createPosTacletApp(taclet, instantiations,
077: matchConstraint, matchNewMetavariables, null, pos);
078: }
079:
080: public static PosTacletApp createPosTacletApp(FindTaclet taclet,
081: SVInstantiations instantiations,
082: Constraint matchConstraint,
083: SetOfMetavariable matchNewMetavariables,
084: ListOfIfFormulaInstantiation ifInstantiations,
085: PosInOccurrence pos) {
086: Debug.assertTrue(ifInstsCorrectSize(taclet, ifInstantiations),
087: "If instantiations list has wrong size");
088:
089: if (!matchConstraint.isSatisfiable())
090: return null;
091:
092: instantiations = resolveCollisionWithContext(taclet,
093: resolveCollisionVarSV(taclet, instantiations), pos);
094: if (checkVarCondNotFreeIn(taclet, instantiations, pos)) {
095: return new PosTacletApp(taclet, instantiations,
096: matchConstraint, matchNewMetavariables,
097: ifInstantiations, pos);
098: }
099:
100: return null;
101: }
102:
103: public static PosTacletApp createPosTacletApp(FindTaclet taclet,
104: MatchConditions matchCond, PosInOccurrence pos) {
105: return createPosTacletApp(taclet,
106: matchCond.getInstantiations(), matchCond
107: .getConstraint(), matchCond
108: .getNewMetavariables(), null, pos);
109: }
110:
111: /** creates a PosTacletApp for the given taclet
112: * and a position information
113: * @param taclet the FindTaclet
114: * @param pos the PosInOccurrence storing the position where to apply the
115: * Taclet
116: */
117: private PosTacletApp(FindTaclet taclet, PosInOccurrence pos) {
118: super (taclet);
119: this .pos = pos;
120: }
121:
122: /** creates a PosTacletApp for the given taclet with some known instantiations
123: * and a position information
124: * @param taclet the FindTaclet
125: * @param pos the PosInOccurrence storing the position where to apply the
126: * Taclet
127: * @param instantiations the SVInstantiations
128: */
129: private PosTacletApp(FindTaclet taclet,
130: SVInstantiations instantiations,
131: Constraint matchConstraint,
132: SetOfMetavariable matchNewMetavariables,
133: ListOfIfFormulaInstantiation ifInstantiations,
134: PosInOccurrence pos) {
135: super (taclet, instantiations, matchConstraint,
136: matchNewMetavariables, ifInstantiations);
137: this .pos = pos;
138: }
139:
140: /**
141: * returns the LogicVariables that are bound above the
142: * PositionInOccurrence of the PosTacletApp. __OPTIMIZE__ If this method
143: * is needed
144: * more than once caching the result should be considered.
145: *
146: * @return the set of the logicvariables that are bound for the
147: * indicated application position of the TacletApp.
148: */
149: private static SetOfQuantifiableVariable varsBoundAboveFindPos(
150: Taclet taclet, PosInOccurrence pos) {
151:
152: if (!(taclet instanceof RewriteTaclet)) {
153: return SetAsListOfQuantifiableVariable.EMPTY_SET;
154: }
155:
156: return collectBoundVarsAbove(pos);
157: }
158:
159: private static IteratorOfSchemaVariable allVariableSV(Taclet taclet) {
160: TacletVariableSVCollector coll = new TacletVariableSVCollector();
161: coll.visit(taclet, true); //__CHANGE__ true or false???
162: return coll.varIterator();
163: }
164:
165: protected SetOfQuantifiableVariable contextVars(SchemaVariable sv) {
166: if (!taclet().getPrefix(sv).context()) {
167: return SetAsListOfQuantifiableVariable.EMPTY_SET;
168: }
169: return varsBoundAboveFindPos(taclet(), posInOccurrence());
170: }
171:
172: /**
173: * resolves collisions with the context
174: * in an SVInstantiation
175: *
176: * @param insts the original SVInstantiations
177: * @return the resolved SVInstantiations
178: */
179: private static SVInstantiations resolveCollisionWithContext(
180: Taclet taclet, SVInstantiations insts, PosInOccurrence pos) {
181:
182: if (taclet.isContextInPrefix()) {
183: SetOfQuantifiableVariable k = varsBoundAboveFindPos(taclet,
184: pos);
185: IteratorOfSchemaVariable it = allVariableSV(taclet);
186: while (it.hasNext()) {
187: SchemaVariable varSV = it.next();
188: Term inst = (Term) insts.getInstantiation(varSV);
189: if (inst != null
190: && k.contains((QuantifiableVariable) inst.op())) {
191: insts = replaceInstantiation(taclet, insts, varSV);
192: }
193: }
194: }
195: return insts;
196: }
197:
198: /** adds a new instantiation to this TacletApp
199: * @param sv the SchemaVariable to be instantiated
200: * @param term the Term the SchemaVariable is instantiated with
201: * @return the new TacletApp
202: */
203: public TacletApp addInstantiation(SchemaVariable sv, Term term,
204: boolean interesting) {
205:
206: if (interesting)
207: return createPosTacletApp((FindTaclet) taclet(),
208: instantiations().addInteresting(sv, term),
209: constraint(), newMetavariables(),
210: ifFormulaInstantiations(), posInOccurrence());
211: else
212: return createPosTacletApp((FindTaclet) taclet(),
213: instantiations().add(sv, term), constraint(),
214: newMetavariables(), ifFormulaInstantiations(),
215: posInOccurrence());
216: }
217:
218: /** adds a new instantiation to this TacletApp
219: * @param sv the SchemaVariable to be instantiated
220: * @param pe the ProgramElement the SV is instantiated with
221: * @return the new TacletApp
222: */
223: public TacletApp addInstantiation(SchemaVariable sv,
224: ProgramElement pe, boolean interesting) {
225: if (interesting)
226: return createPosTacletApp((FindTaclet) taclet(),
227: instantiations().addInteresting(sv, pe),
228: constraint(), newMetavariables(),
229: ifFormulaInstantiations(), posInOccurrence());
230: else
231: return createPosTacletApp((FindTaclet) taclet(),
232: instantiations().add(sv, pe), constraint(),
233: newMetavariables(), ifFormulaInstantiations(),
234: posInOccurrence());
235: }
236:
237: public TacletApp addInstantiation(SchemaVariable sv, Object[] list,
238: boolean interesting) {
239: if (interesting)
240: return createPosTacletApp((FindTaclet) taclet(),
241: instantiations().addInterestingList(sv, list),
242: constraint(), newMetavariables(),
243: ifFormulaInstantiations(), posInOccurrence());
244: else
245: return createPosTacletApp((FindTaclet) taclet(),
246: instantiations().addList(sv, list), constraint(),
247: newMetavariables(), ifFormulaInstantiations(),
248: posInOccurrence());
249: }
250:
251: /**
252: * creates a new Taclet application containing all the
253: * instantiations given
254: * by the SVInstantiations and the ones of this TacletApp
255: * @param svi the SVInstantiations whose entries are the needed
256: * instantiations
257: * @return the new Taclet application
258: */
259: public TacletApp addInstantiation(SVInstantiations svi) {
260: return createPosTacletApp((FindTaclet) taclet(), svi
261: .union(instantiations()), constraint(),
262: newMetavariables(), ifFormulaInstantiations(),
263: posInOccurrence());
264: }
265:
266: /**
267: * creates a new Taclet application containing all the
268: * instantiations given
269: * by the SVInstantiations and forget the old ones.
270: * @param svi the SVInstantiations whose entries are the needed
271: * instantiations
272: * @return the new Taclet application
273: */
274: protected TacletApp setInstantiation(SVInstantiations svi) {
275: return createPosTacletApp((FindTaclet) taclet(), svi,
276: constraint(), newMetavariables(),
277: ifFormulaInstantiations(), posInOccurrence());
278: }
279:
280: /**
281: * creates a new Taclet application containing all the
282: * instantiations, constraints and new metavariables given
283: * by the mc object and forget the old ones
284: */
285: protected TacletApp setMatchConditions(MatchConditions mc) {
286: return createPosTacletApp((FindTaclet) taclet(), mc
287: .getInstantiations(), mc.getConstraint(), mc
288: .getNewMetavariables(), ifFormulaInstantiations(),
289: posInOccurrence());
290: }
291:
292: /**
293: * creates a new Taclet application containing all the
294: * instantiations, constraints, new metavariables and if formula
295: * instantiations given and forget the old ones
296: */
297: protected TacletApp setAllInstantiations(MatchConditions mc,
298: ListOfIfFormulaInstantiation ifInstantiations) {
299: return createPosTacletApp((FindTaclet) taclet(), mc
300: .getInstantiations(), mc.getConstraint(), mc
301: .getNewMetavariables(), ifInstantiations,
302: posInOccurrence());
303: }
304:
305: /** returns true iff all necessary informations are collected, so
306: * that the Taclet can be applied.
307: * @return true iff all necessary informations are collected, so
308: * that the Taclet can be applied.
309: */
310: public boolean complete() {
311: return posInOccurrence() != null
312: && uninstantiatedVars() == SetAsListOfSchemaVariable.EMPTY_SET
313: && ifInstsComplete();
314: }
315:
316: /**
317: * @return true iff the taclet instantiation can be made complete
318: * using metavariables
319: */
320: public boolean sufficientlyComplete() {
321: return posInOccurrence() != null && instsSufficientlyComplete()
322: && ifInstsComplete();
323: }
324:
325: /**
326: * returns the PositionInOccurrence (representing a ConstrainedFormula and
327: * a position in the corresponding formula)
328: * @return the PosInOccurrence
329: */
330: public PosInOccurrence posInOccurrence() {
331: return pos;
332: }
333:
334: public boolean equals(Object o) {
335: return super .equals(o)
336: && ((PosTacletApp) o).posInOccurrence().equals(
337: posInOccurrence());
338: }
339:
340: public int hashCode() {
341: int result = 17;
342: result = 37 * result + super .hashCode();
343: result = 37 * result + posInOccurrence().hashCode();
344: return result;
345: }
346:
347: public String toString() {
348: return super .toString() + " at " + posInOccurrence();
349: }
350:
351: }
|