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.Services;
014: import de.uka.ilkd.key.logic.*;
015: import de.uka.ilkd.key.logic.op.*;
016: import de.uka.ilkd.key.proof.Goal;
017: import de.uka.ilkd.key.proof.IteratorOfGoal;
018: import de.uka.ilkd.key.proof.ListOfGoal;
019:
020: /**
021: * An abstract class to represent Taclets with a find part. This means, they
022: * have to be attached to a formula or term of the sequent. This class is
023: * extended by several subclasses to distinct between taclets that have to
024: * attached to a top level formula of the antecedent ({@link AntecTaclet}),
025: * to the succedent ({@link SuccTaclet}) or to an arbitrary term that matches
026: * the find part somewhere in the sequent ({@link RewriteTaclet}).
027: */
028: public abstract class FindTaclet extends Taclet {
029:
030: /** contains the find term */
031: protected Term find;
032:
033: /** Set of schemavariables of the if and the (optional) find part */
034: private SetOfSchemaVariable ifFindVariables = null;
035:
036: /** this method is used to determine if top level updates are
037: * allowed to be ignored. This is the case if we have an Antec or
038: * SuccTaclet but not for a RewriteTaclet
039: * @return true if top level updates shall be ignored
040: */
041: protected abstract boolean ignoreTopLevelUpdates();
042:
043: /** creates a FindTaclet
044: * @param name the Name of the taclet
045: * @param applPart the TacletApplPart that contains the if-sequent, the
046: * not-free and new-vars conditions
047: * @param goalTemplates a ListOfTacletGoalTemplate that contains all goaltemplates of
048: * the taclet (these are the instructions used to create new goals when
049: * applying the Taclet)
050: * @param ruleSets a ListOfRuleSet that contains all rule sets the Taclet
051: * is attached to
052: * @param constraint the Constraint of the Taclet (has to be fulfilled in
053: * order to achieve this Taclet)
054: * @param attrs the TacletAttributes encoding if the Taclet is non-interactive,
055: * recursive or something like that
056: * @param find the Term that is the pattern that has to be found in a
057: * sequent and the places where it matches the Taclet can be applied
058: * @param prefixMap a MapFromSchemaVariableToTacletPrefix that contains the
059: * prefix for each SchemaVariable in the Taclet
060: */
061: public FindTaclet(Name name, TacletApplPart applPart,
062: ListOfTacletGoalTemplate goalTemplates,
063: ListOfRuleSet ruleSets, Constraint constraint,
064: TacletAttributes attrs, Term find,
065: MapFromSchemaVariableToTacletPrefix prefixMap,
066: SetOfChoice choices) {
067: super (name, applPart, goalTemplates, ruleSets, constraint,
068: attrs, prefixMap, choices);
069: this .find = find;
070: }
071:
072: /** returns the find term of the taclet to be matched */
073: public Term find() {
074: return find;
075: }
076:
077: /**
078: * matches the given term against the taclet's find term and
079: * @param term the Term to be matched against the find expression
080: * of the taclet
081: * @param matchCond the MatchConditions with side conditions to be
082: * satisfied, eg. partial instantiations of schema variables; before
083: * calling this method the constraint contained in the match conditions
084: * must be ensured to be satisfiable, i.e.
085: * <tt> matchCond.getConstraint ().isSatisfiable () </tt>
086: * must return true
087: * @param services the Services
088: * @param userConstraint a Constraint derived from user defined
089: * instantiations of meta variables
090: * @return the found schema variable mapping or <tt>null</tt> if
091: * the matching failed
092: */
093: public MatchConditions matchFind(Term term,
094: MatchConditions matchCond, Services services,
095: Constraint userConstraint) {
096: return match(term, find(), ignoreTopLevelUpdates(), matchCond,
097: services, userConstraint);
098: }
099:
100: /** CONSTRAINT NOT USED
101: * applies the replacewith part of Taclets
102: * @param gt TacletGoalTemplate used to get the replaceexpression
103: * in the Taclet
104: * @param goal the Goal where the rule is applied
105: * @param posOfFind the PosInOccurrence belonging to the find expression
106: * @param services the Services encapsulating all java information
107: * @param matchCond the MatchConditions with all required instantiations
108: */
109: protected abstract void applyReplacewith(TacletGoalTemplate gt,
110: Goal goal, PosInOccurrence posOfFind, Services services,
111: MatchConditions matchCond);
112:
113: /**
114: * adds the sequent of the add part of the Taclet to the goal sequent
115: * @param add the Sequent to be added
116: * @param goal the Goal to be updated
117: * @param posOfFind the PosInOccurrence describes the place where to add
118: * the semisequent
119: * @param services the Services encapsulating all java information
120: * @param matchCond the MatchConditions with all required instantiations
121: */
122: protected abstract void applyAdd(Sequent add, Goal goal,
123: PosInOccurrence posOfFind, Services services,
124: MatchConditions matchCond);
125:
126: /**
127: * the rule is applied on the given goal using the
128: * information of rule application.
129: * @param goal the goal that the rule application should refer to.
130: * @param services the Services encapsulating all java information
131: * @param ruleApp the taclet application that is executed.
132: */
133: public ListOfGoal apply(Goal goal, Services services,
134: RuleApp ruleApp) {
135:
136: // Number without the if-goal eventually needed
137: int numberOfNewGoals = goalTemplates().size();
138:
139: TacletApp tacletApp = (TacletApp) ruleApp;
140: MatchConditions mc = tacletApp.matchConditions();
141:
142: // Restrict introduced metavariables to the subtree
143: setRestrictedMetavariables(goal, mc);
144:
145: ListOfGoal newGoals = checkIfGoals(goal, tacletApp
146: .ifFormulaInstantiations(), mc, numberOfNewGoals);
147:
148: IteratorOfTacletGoalTemplate it = goalTemplates().iterator();
149: IteratorOfGoal goalIt = newGoals.iterator();
150:
151: while (it.hasNext()) {
152: TacletGoalTemplate gt = it.next();
153: Goal currentGoal = goalIt.next();
154: // add first because we want to use pos information that
155: // is lost applying replacewith
156: applyAdd(gt.sequent(), currentGoal, tacletApp
157: .posInOccurrence(), services, mc);
158:
159: applyReplacewith(gt, currentGoal, tacletApp
160: .posInOccurrence(), services, mc);
161:
162: applyAddrule(gt.rules(), currentGoal, services, mc);
163:
164: applyAddProgVars(gt.addedProgVars(), currentGoal, tacletApp
165: .posInOccurrence(), services, mc);
166:
167: currentGoal.setBranchLabel(gt.name());
168: }
169:
170: return newGoals;
171: }
172:
173: StringBuffer toStringFind(StringBuffer sb) {
174: return sb.append("\\find(").append(find().toString()).append(
175: ")\n");
176: }
177:
178: /**
179: * returns a representation of the Taclet with find part as String
180: * @return string representation
181: */
182: public String toString() {
183: if (tacletAsString == null) {
184: StringBuffer sb = new StringBuffer();
185: sb = sb.append(name()).append(" {\n");
186: sb = toStringIf(sb);
187: sb = toStringFind(sb);
188: sb = toStringVarCond(sb);
189: sb = toStringGoalTemplates(sb);
190: sb = toStringRuleSets(sb);
191: sb = toStringAttribs(sb);
192: tacletAsString = sb.append("}").toString();
193: }
194: return tacletAsString;
195: }
196:
197: /**
198: * @return Set of schemavariables of the if and the (optional)
199: * find part
200: */
201: public SetOfSchemaVariable getIfFindVariables() {
202: if (ifFindVariables == null) {
203: TacletSchemaVariableCollector svc = new TacletSchemaVariableCollector();
204: find().execPostOrder(svc);
205:
206: ifFindVariables = getIfVariables();
207: IteratorOfSchemaVariable it = svc.varIterator();
208: while (it.hasNext())
209: ifFindVariables = ifFindVariables.add(it.next());
210: }
211:
212: return ifFindVariables;
213: }
214:
215: protected Taclet setName(String s, FindTacletBuilder b) {
216: return super .setName(s, b);
217: }
218:
219: /**
220: * Determine whether a replacewith-part is really supposed to modify
221: * concerned formulas when applying a taclet (otherwise copies of the
222: * formulas are created). Copies are created whenever the constraint of the
223: * new formulas is stronger than the conjunction of the original
224: * find-formula constraint and the user constraint. (Taking the user
225: * constraint into account at this point ensures that the existence of the
226: * user constraint is transparent to the user, and is a temporary solution
227: * to cope with the absence of disunification constraints).
228: *
229: * UPDATE: for the time being we are only considering the old constraint of
230: * the formula (as the user constraint is more or less disable in
231: * <code>TacletApp. canUseMVAPosteriori</code> right now)
232: *
233: * @param goal
234: * the goal to which the taclet is applied
235: * @param posOfFind
236: * position of the find-formula (which is the formula whose
237: * constraint is considered as the original formula constraint)
238: * @param matchCond
239: * results of matching the taclet, in particular the new
240: * constraint that is attached to formulas added by replacewith
241: * @return true iff replacewith is supposed to create copies of concerned
242: * formulas
243: */
244: protected boolean createCopies(Goal goal,
245: PosInOccurrence posOfFind, MatchConditions matchCond) {
246: // final Proof proof = goal.proof ();
247: // final Constraint userConstraint =
248: // proof.getUserConstraint ().getConstraint ();
249: final Constraint oriConstraint = posOfFind.constrainedFormula()
250: .constraint();
251: // final Constraint combinedConstraint =
252: // userConstraint.join ( oriConstraint, proof.getServices() );
253: final Constraint newConstraint = matchCond.getConstraint();
254: return !newConstraint.isAsWeakAs(oriConstraint);
255: }
256:
257: /** returns the variables in a Taclet with a read access
258: */
259: public ListOfSchemaVariable readSet() {
260:
261: //List variables have to be collected to
262: ListOfSchemaVariable readFromVarialbes = SLListOfSchemaVariable.EMPTY_LIST;
263:
264: //List of Variables in find-part
265: TacletSchemaVariableCollector tvarColl1 = new TacletSchemaVariableCollector() {
266: public void visit(Term t) {
267: if (t.op() instanceof Modality
268: || t.op() instanceof ModalOperatorSV) {
269: varList = collectSVInProgram(t.javaBlock(), varList);
270: }
271: for (int j = 0; j < t.arity(); j++) {
272: for (int i = 0; i < t.varsBoundHere(j).size(); i++) {
273: if (t.varsBoundHere(j).getQuantifiableVariable(
274: i) instanceof SchemaVariable) {
275: varList = varList
276: .prepend((SchemaVariable) t
277: .varsBoundHere(j)
278: .getQuantifiableVariable(i));
279: }
280: }
281: }
282: }
283: };
284: tvarColl1.visit(find());
285:
286: //List of variables im add & replaceWith-Part
287: TacletSchemaVariableCollector tvarColl2 = new TacletSchemaVariableCollector() {
288: public void visit(Term t) {
289: if (t.op() instanceof SchemaVariable)
290: varList = varList.prepend((SchemaVariable) t.op());
291: }
292: };
293: tvarColl2.visitGoalTemplates(this , false);
294:
295: // build intersection
296: IteratorOfSchemaVariable it1 = tvarColl1.varIterator();
297: while (it1.hasNext()) {
298: SchemaVariable sv1 = it1.next();
299: IteratorOfSchemaVariable it2 = tvarColl2.varIterator();
300:
301: while (it2.hasNext()) {
302: SchemaVariable sv2 = it2.next();
303:
304: if (sv1 == sv2) {
305: if (writeSet().head() != null) {
306: //if the variable belongs to the WriteSet,
307: //remove it from the ReadSet
308: if (writeSet().head() != sv1)
309: readFromVarialbes = readFromVarialbes
310: .prepend(sv1);
311: } else
312: readFromVarialbes = readFromVarialbes
313: .prepend(sv1);
314: break; //variable found, no need to keep searching
315: }
316: }
317: }
318: return readFromVarialbes;
319: }
320:
321: /**
322: * returns the variable in a Taclet to which is written to
323: */
324: public ListOfSchemaVariable writeSet() {
325: IteratorOfTacletGoalTemplate it = goalTemplates().iterator();
326: ListOfSchemaVariable updateVar = SLListOfSchemaVariable.EMPTY_LIST;
327: Term replWith = null;
328:
329: while (it.hasNext()) {
330: TacletGoalTemplate goalTemp = it.next();
331:
332: if (goalTemp instanceof RewriteTacletGoalTemplate) {
333: replWith = ((RewriteTacletGoalTemplate) goalTemp)
334: .replaceWith();
335:
336: if (replWith.op() instanceof IUpdateOperator) {
337: try {
338: updateVar = updateVar
339: .prepend((SchemaVariable) replWith.sub(
340: 0).op());
341: } catch (ClassCastException e) {
342: System.err.println(name() + " "
343: + replWith.sub(0).op().getClass());
344: }
345: }
346: }
347: }
348: return updateVar;
349: }
350:
351: /**
352: * returns the variables that occur bound in the find part
353: * @return the variables that occur bound in the find part
354: */
355: protected SetOfQuantifiableVariable getBoundVariablesHelper() {
356: final BoundVarsVisitor bvv = new BoundVarsVisitor();
357: bvv.visit(find());
358: return bvv.getBoundVariables();
359: }
360:
361: }
|