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.java.Services;
015: import de.uka.ilkd.key.logic.Constraint;
016: import de.uka.ilkd.key.logic.PosInOccurrence;
017: import de.uka.ilkd.key.logic.RenameTable;
018: import de.uka.ilkd.key.logic.Term;
019: import de.uka.ilkd.key.logic.op.*;
020: import de.uka.ilkd.key.proof.mgt.Contractable;
021: import de.uka.ilkd.key.rule.inst.SVInstantiations;
022: import de.uka.ilkd.key.util.Debug;
023:
024: /**
025: * A no position taclet application has no position information yet. This can
026: * have different reasons: <ul>
027: * <li> the taclet application belongs to a no find taclet, this means it is
028: * attached to a sequent and not to a formula or term. </li>
029: * <li> the taclet application has not been matched against a term or formula,
030: * but may already contain instantiation information for some of its
031: * schemavariables. This is the case, if the taclet of this application object
032: * has been inserted by an addrule part of another taclet. For this reason
033: * the {@link de.uka.ilkd.key.proof.TacletIndex} manages no position taclet
034: * application objects instead of the taclets itself.
035: * </li> </ul>
036: *
037: */
038: public class NoPosTacletApp extends TacletApp implements Contractable {
039:
040: /** creates a NoPosTacletApp for the given taclet and no instantiation
041: * information and CHECKS variable conditions as well as it resolves
042: * collisions
043: * @param taclet the Taclet
044: */
045: public static NoPosTacletApp createNoPosTacletApp(Taclet taclet) {
046: return new UninstantiatedNoPosTacletApp(taclet);
047: }
048:
049: /** creates a NoPosTacletApp for the given taclet with some known
050: * instantiations and CHECKS variable conditions as well as it
051: * resolves collisions
052: * The ifInstantiations parameter is not
053: * matched against the if sequence, but only stored. For matching
054: * use the method "setIfFormulaInstantiations".
055: * @param taclet the Taclet
056: * @param instantiations the SVInstantiations
057: */
058: public static NoPosTacletApp createNoPosTacletApp(Taclet taclet,
059: SVInstantiations instantiations) {
060: return createNoPosTacletApp(taclet, instantiations,
061: Constraint.BOTTOM, SetAsListOfMetavariable.EMPTY_SET,
062: null);
063: }
064:
065: public static NoPosTacletApp createNoPosTacletApp(Taclet taclet,
066: SVInstantiations instantiations,
067: Constraint matchConstraint,
068: SetOfMetavariable matchNewMetavariables) {
069: return createNoPosTacletApp(taclet, instantiations,
070: matchConstraint, matchNewMetavariables, null);
071: }
072:
073: public static NoPosTacletApp createNoPosTacletApp(Taclet taclet,
074: SVInstantiations instantiations,
075: Constraint matchConstraint,
076: SetOfMetavariable matchNewMetavariables,
077: ListOfIfFormulaInstantiation ifInstantiations) {
078: Debug.assertTrue(ifInstsCorrectSize(taclet, ifInstantiations),
079: "If instantiations list has wrong size");
080:
081: if (!matchConstraint.isSatisfiable())
082: return null;
083:
084: SVInstantiations inst = resolveCollisionVarSV(taclet,
085: instantiations);
086: if (checkVarCondNotFreeIn(taclet, inst)) {
087: return new NoPosTacletApp(taclet, inst, matchConstraint,
088: matchNewMetavariables, ifInstantiations);
089: }
090: return null;
091: }
092:
093: public static NoPosTacletApp createNoPosTacletApp(Taclet taclet,
094: MatchConditions matchCond) {
095: return createNoPosTacletApp(taclet, matchCond
096: .getInstantiations(), matchCond.getConstraint(),
097: matchCond.getNewMetavariables(), null);
098: }
099:
100: /**
101: * Create TacletApp with immutable "instantiations", i.e. this
102: * instantiations must not be modified later (e.g. by
103: * "addInstantiation"). However, this information is currently
104: * only used to decide about introduction of
105: * metavariables. Immutable instantiations are important for the
106: * "addrules" part of taclets.
107: */
108: public static NoPosTacletApp createFixedNoPosTacletApp(
109: Taclet taclet, SVInstantiations instantiations,
110: Constraint constraint) {
111: NoPosTacletApp res = createNoPosTacletApp(taclet,
112: instantiations, constraint,
113: SetAsListOfMetavariable.EMPTY_SET, null);
114: // Make the given SVs fixed
115: if (res != null) {
116: final IteratorOfSchemaVariable it = instantiations
117: .svIterator();
118: while (it.hasNext()) {
119: res.fixedVars = res.fixedVars.add(it.next());
120: }
121: res.updateContextFixed = true;
122: }
123: return res;
124: }
125:
126: /** creates a NoPosTacletApp for the given taclet and no instantiation
127: * information
128: * @param taclet the Taclet
129: */
130: protected NoPosTacletApp(Taclet taclet) {
131: super (taclet);
132: }
133:
134: /** creates a NoPosTacletApp for the given taclet with some known instantiations
135: * @param taclet the Taclet
136: * @param instantiations the SVInstantiations
137: */
138: private NoPosTacletApp(Taclet taclet,
139: SVInstantiations instantiations,
140: Constraint matchConstraint,
141: SetOfMetavariable matchNewMetavariables,
142: ListOfIfFormulaInstantiation ifInstantiations) {
143: super (taclet, instantiations, matchConstraint,
144: matchNewMetavariables, ifInstantiations);
145: }
146:
147: /** checks if the variable conditions of type 'x not free in y' are
148: * hold by the found instantiations. The variable conditions is used
149: * implicit in the prefix. (Used to calculate the prefix)
150: * @param taclet the Taclet that is tried to be instantiated. A match for the
151: * find (or/and if) has been found.
152: * @param instantiations the SVInstantiations so that the find(if) matches
153: * @return true iff all variable conditions x not free in y are hold
154: */
155: protected static boolean checkVarCondNotFreeIn(Taclet taclet,
156: SVInstantiations instantiations) {
157: final IteratorOfSchemaVariable it = instantiations.svIterator();
158: while (it.hasNext()) {
159: final SchemaVariable sv = it.next();
160:
161: if (sv.isOperatorSV() || sv.isProgramSV()
162: || sv.isVariableSV() || sv.isSkolemTermSV()
163: || sv.isListSV() || sv.isNameSV())
164: continue;
165:
166: final TacletPrefix prefix = taclet.getPrefix(sv);
167: if (prefix.context())
168: continue;
169:
170: final SetOfQuantifiableVariable boundVarSet = boundAtOccurrenceSet(
171: prefix, instantiations);
172: final Term inst = (Term) instantiations
173: .getInstantiation(sv);
174: if (!inst.freeVars().subset(boundVarSet))
175: return false;
176: }
177:
178: return true;
179: }
180:
181: /** adds a new instantiation to this TacletApp
182: * @param sv the SchemaVariable to be instantiated
183: * @param term the Term the SchemaVariable is instantiated with
184: * @return the new TacletApp
185: */
186: public TacletApp addInstantiation(SchemaVariable sv, Term term,
187: boolean interesting) {
188: if (interesting)
189: return createNoPosTacletApp(taclet(), instantiations()
190: .addInteresting(sv, term), constraint(),
191: newMetavariables(), ifFormulaInstantiations());
192: else
193: return createNoPosTacletApp(taclet(), instantiations().add(
194: sv, term), constraint(), newMetavariables(),
195: ifFormulaInstantiations());
196: }
197:
198: public TacletApp addInstantiation(SchemaVariable sv, Object[] list,
199: boolean interesting) {
200: if (interesting)
201: return createNoPosTacletApp(taclet(), instantiations()
202: .addInterestingList(sv, list), constraint(),
203: newMetavariables(), ifFormulaInstantiations());
204: else
205: return createNoPosTacletApp(taclet(), instantiations()
206: .addList(sv, list), constraint(),
207: newMetavariables(), ifFormulaInstantiations());
208: }
209:
210: /**
211: * adds a new instantiation to this TacletApp
212: *
213: * @param sv
214: * the SchemaVariable to be instantiated
215: * @param pe
216: * the ProgramElement the SV is instantiated with
217: * @return the new TacletApp
218: */
219: public TacletApp addInstantiation(SchemaVariable sv,
220: ProgramElement pe, boolean interesting) {
221: if (interesting)
222: return createNoPosTacletApp(taclet(), instantiations()
223: .addInteresting(sv, pe), constraint(),
224: newMetavariables(), ifFormulaInstantiations());
225: else
226: return createNoPosTacletApp(taclet(), instantiations().add(
227: sv, pe), constraint(), newMetavariables(),
228: ifFormulaInstantiations());
229: }
230:
231: /**
232: * creates a new Taclet application containing all the
233: * instantiations given
234: * by the SVInstantiations and hold the old ones
235: * @param svi the SVInstantiations whose entries are the needed
236: * instantiations
237: * @return the new Taclet application
238: */
239: public TacletApp addInstantiation(SVInstantiations svi) {
240: return new NoPosTacletApp(taclet(),
241: svi.union(instantiations()), constraint(),
242: newMetavariables(), ifFormulaInstantiations());
243: }
244:
245: /**
246: * creates a new Taclet application containing all the
247: * instantiations given
248: * by the SVInstantiations and forget the ones in this TacletApp
249: * @param svi the SVInstantiations whose entries are the needed
250: * instantiations
251: * @return the new Taclet application
252: */
253: protected TacletApp setInstantiation(SVInstantiations svi) {
254: return new NoPosTacletApp(taclet(), svi, constraint(),
255: newMetavariables(), ifFormulaInstantiations());
256: }
257:
258: /**
259: * creates a new Taclet application containing all the
260: * instantiations, constraints and new metavariables given
261: * by the mc object and forget the old ones
262: */
263: protected TacletApp setMatchConditions(MatchConditions mc) {
264: return createNoPosTacletApp(taclet(), mc.getInstantiations(),
265: mc.getConstraint(), mc.getNewMetavariables(),
266: ifFormulaInstantiations());
267: }
268:
269: /**
270: * creates a new Taclet application containing all the
271: * instantiations, constraints, new metavariables and if formula
272: * instantiations given and forget the old ones
273: */
274: protected TacletApp setAllInstantiations(MatchConditions mc,
275: ListOfIfFormulaInstantiation ifInstantiations) {
276: return createNoPosTacletApp(taclet(), mc.getInstantiations(),
277: mc.getConstraint(), mc.getNewMetavariables(),
278: ifInstantiations);
279: }
280:
281: /** returns true iff all necessary informations are collected, so
282: * that the Taclet can be applied.
283: * @return true iff all necessary informations are collected, so
284: * that the Taclet can be applied.
285: */
286: public boolean complete() {
287: return (uninstantiatedVars() == SetAsListOfSchemaVariable.EMPTY_SET
288: && taclet() instanceof NoFindTaclet && ifInstsComplete());
289:
290: }
291:
292: /**
293: * @return true iff the taclet instantiation can be made complete
294: * using metavariables
295: */
296: public boolean sufficientlyComplete() {
297: return (taclet() instanceof NoFindTaclet)
298: && instsSufficientlyComplete() && ifInstsComplete();
299: }
300:
301: protected SetOfQuantifiableVariable contextVars(SchemaVariable sv) {
302: return SetAsListOfQuantifiableVariable.EMPTY_SET;
303: }
304:
305: /**
306: * returns the PositionInOccurrence (representing a ConstrainedFormula and
307: * a position in the corresponding formula)
308: * @return the PosInOccurrence
309: */
310: public PosInOccurrence posInOccurrence() {
311: return null;
312: }
313:
314: /**
315: * PRECONDITION: ifFormulaInstantiations () == null &&
316: * ( pos == null || termConstraint.isSatisfiable () )
317: * @return TacletApp with the resulting instantiations or null
318: */
319: public NoPosTacletApp matchFind(PosInOccurrence pos,
320: Constraint termConstraint, Services services,
321: Constraint userConstraint) {
322: return matchFind(pos, termConstraint, services, userConstraint,
323: null);
324: }
325:
326: /* This is a short-circuit version of matchFind(). It helps eliminate
327: numerous calls to the expensive pos.subTerm() while matching during
328: a recursive descent in a term (where the current subterm is known
329: anyway).
330: */
331: public NoPosTacletApp matchFind(PosInOccurrence pos,
332: Constraint termConstraint, Services services,
333: Constraint userConstraint, Term t) {
334:
335: if ((t == null) && (pos != null))
336: t = pos.subTerm();
337:
338: MatchConditions mc = setupMatchConditions(pos, services,
339: userConstraint);
340:
341: if (mc == null)
342: return null;
343:
344: MatchConditions res = null;
345: if (taclet() instanceof FindTaclet) {
346: Constraint c = mc.getConstraint().join(termConstraint,
347: services);
348: if (c.isSatisfiable()) {
349: res = ((FindTaclet) taclet()).matchFind(t, mc
350: .setConstraint(c), services, userConstraint);
351: // the following check will partly be repeated within the
352: // constructor; this could be optimised
353: if (res == null
354: || !checkVarCondNotFreeIn(taclet(), res
355: .getInstantiations(), pos))
356: return null;
357: }
358: } else {
359: res = mc;
360: }
361:
362: return evalCheckRes(res);
363: }
364:
365: private NoPosTacletApp evalCheckRes(MatchConditions res) {
366: if (res == null)
367: return null;
368:
369: if (updateContextFixed && !updateContextCompatible(res)) {
370: /* Debug.out("NoPosTacletApp: Incompatible context", instantiations.getUpdateContext (),
371: res.matchConditions().getInstantiations().getUpdateContext());*/
372: return null;
373: }
374:
375: return (NoPosTacletApp) setMatchConditions(res);
376: }
377:
378: protected MatchConditions setupMatchConditions(PosInOccurrence pos,
379: Services services, Constraint userConstraint) {
380: SVInstantiations svInst = taclet() instanceof NoFindTaclet ? instantiations()
381: : instantiations().clearUpdateContext();
382:
383: MatchConditions mc = new MatchConditions(svInst, constraint(),
384: newMetavariables(), RenameTable.EMPTY_TABLE);
385:
386: if (taclet() instanceof RewriteTaclet) {
387: mc = ((RewriteTaclet) taclet()).checkUpdatePrefix(pos, mc,
388: services, userConstraint);
389: if (mc == null) {
390: Debug
391: .out("NoPosTacletApp: Update prefix check failed.");
392: }
393: }
394:
395: return mc;
396: }
397:
398: private boolean updateContextCompatible(MatchConditions p_mc) {
399: return instantiations.getUpdateContext().equals(
400: p_mc.getInstantiations().getUpdateContext());
401: }
402:
403: public boolean equals(Object o) {
404: if (o == this )
405: return true;
406: if (!(o instanceof NoPosTacletApp))
407: return false;
408: return super .equals(o);
409: }
410:
411: public int hashCode() {
412: return super .hashCode();
413: }
414:
415: public boolean equalContractable(Contractable c) {
416: return equals(c);
417: }
418: }
|