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.logic.sort.AbstractSort;
017: import de.uka.ilkd.key.logic.sort.Sort;
018: import de.uka.ilkd.key.logic.util.TermHelper;
019: import de.uka.ilkd.key.proof.Goal;
020: import de.uka.ilkd.key.rule.inst.SVInstantiations;
021: import de.uka.ilkd.key.rule.updatesimplifier.Update;
022:
023: /**
024: * A RewriteTaclet represents a taclet, whose find can be matched against any
025: * term in the sequent no matter where it occurs. The only constraint to be
026: * fulfilled is that the term matches the structure described by the term of the
027: * find-part.
028: */
029: public class RewriteTaclet extends FindTaclet {
030:
031: /** does not pose state restrictions on valid matchings */
032: public static final int NONE = 0;
033:
034: /** all taclet consituents must appear in the same state
035: * (and not below a modality (for efficiency reasons)) */
036: public static final int SAME_UPDATE_LEVEL = 1;
037:
038: /** all taclet consituents must be in the same state
039: * as the sequent */
040: public static final int IN_SEQUENT_STATE = 2;
041:
042: /**
043: * encodes restrictions on the state where a rewrite taclet is applicable
044: * If the value is equal to
045: * <ul>
046: * <li> {@link RewriteTaclet#NONE} no state restrictions are posed</li>
047: * <li> {@link RewriteTaclet#SAME_UPDATE_LEVEL} then <code>\assumes</code>
048: * must match on a formula within the same state as <code>\find</code>
049: * rsp. <code>\add</code>. For efficiency no modalities are allowed above
050: * the <code>\find</code> position </li>
051: * <li> {@link RewriteTaclet#IN_SEQUENT_STATE} the <code>\find</code> part is
052: * only allowed to match on formulas which are evaulated in the same state as
053: * the sequent</li>
054: *</ul>
055: */
056: private int stateRestriction;
057:
058: /**
059: * creates a Schematic Theory Specific Rule (Taclet) with the given
060: * parameters that represents a rewrite rule.
061: * @param name the Name of the Taclet
062: * @param applPart the TacletApplPart that contains the application part of an Taclet that is
063: * the if-sequent, the variable conditions
064: * @param goalTemplates a list of goal descriptions.
065: * @param ruleSets a list of rule sets for the Taclet
066: * @param constraint the Constraint under which the Taclet is valid
067: * @param attrs the TacletAttributes; these are boolean values
068: * indicating a noninteractive or recursive use of the Taclet.
069: * @param find the find term of the Taclet
070: * @param prefixMap a MapFromSchemaVariableToTacletPrefix that contains the
071: * prefix for each SchemaVariable in the Taclet
072: * @param p_stateRestriction an int defining state restrictions of the taclet
073: * (required for location check)
074: * @param choices the SetOfChoices to which this taclet belongs to
075: */
076: public RewriteTaclet(Name name, TacletApplPart applPart,
077: ListOfTacletGoalTemplate goalTemplates,
078: ListOfRuleSet ruleSets, Constraint constraint,
079: TacletAttributes attrs, Term find,
080: MapFromSchemaVariableToTacletPrefix prefixMap,
081: int p_stateRestriction, SetOfChoice choices) {
082: super (name, applPart, goalTemplates, ruleSets, constraint,
083: attrs, find, prefixMap, choices);
084: stateRestriction = p_stateRestriction;
085:
086: cacheMatchInfo();
087: }
088:
089: /**
090: * this method is used to determine if top level updates are
091: * allowed to be ignored. This is the case if we have an Antec or
092: * SuccTaclet but not for a RewriteTaclet
093: * @return true if top level updates shall be ignored
094: */
095: protected boolean ignoreTopLevelUpdates() {
096: return false;
097: }
098:
099: /**
100: * returns the int encoding the kind of state restriction this rewrite
101: * taclet must obey
102: * @return the int encoding the kind of state restriction this rewrite
103: * taclet must obey
104: */
105: public int getStateRestriction() {
106: return stateRestriction;
107: }
108:
109: /**
110: * the top level operator has to be a simultaneous update. This method
111: * checks if the assignment pairs of the update contain free logic
112: * variables and gives a veto if positive
113: * @param t the Term to check
114: * @return false if vetoing
115: */
116: private boolean veto(Term t) {
117: return Update.createUpdate(t).freeVars().size() > 0;
118: }
119:
120: /**
121: * For taclets with <code>getSameUpdatePrefix ()</code>, collect
122: * the updates above <code>p_pos</code> and add them to the update
123: * context of the instantiations object <code>p_mc</code>.
124: * @return the new instantiations with the additional updates, or
125: * <code>null</code>, if program modalities appear above
126: * <code>p_pos</code>
127: */
128: public MatchConditions checkUpdatePrefix(PosInOccurrence p_pos,
129: MatchConditions p_mc, Services p_services,
130: Constraint p_userConstraint) {
131: if (getStateRestriction() == NONE)
132: return p_mc;
133:
134: SVInstantiations svi = p_mc.getInstantiations();
135: if (p_pos.posInTerm() != null) {
136: PIOPathIterator it = p_pos.iterator();
137: Operator op;
138:
139: while (it.next() != -1) {
140: final Term t = it.getSubTerm();
141: op = t.op();
142:
143: if (op instanceof IUpdateOperator
144: && it.getChild() == ((IUpdateOperator) op)
145: .targetPos()) {
146: if (getStateRestriction() == IN_SEQUENT_STATE
147: || veto(t)) {
148: return null;
149: } else {
150: svi = svi.addUpdate(it.getSubTerm());
151: }
152:
153: } else if (op instanceof Modality
154: || op instanceof ModalOperatorSV)
155: return null;
156: }
157: }
158:
159: return p_mc.setInstantiations(svi);
160: }
161:
162: /**
163: * does the work for applyReplacewith (wraps recursion)
164: */
165: private Term replace(Term term, Term with, IntIterator it,
166: Services services, MatchConditions mc, Sort maxSort) {
167: if (it.hasNext()) {
168: int sub = it.next();
169:
170: ArrayOfQuantifiableVariable[] origvars = new ArrayOfQuantifiableVariable[term
171: .arity()];
172: final Term[] subs = new Term[term.arity()];
173:
174: for (int i = 0, arity = term.arity(); i < arity; i++) {
175:
176: if (i != sub) {
177: subs[i] = term.sub(i);
178: } else {
179: final Sort newMaxSort = TermHelper.getMaxSort(term,
180: i, services);
181: subs[i] = replace(term.sub(i), with, it, services,
182: mc, newMaxSort);
183: }
184: origvars[i] = term.varsBoundHere(i);
185: }
186:
187: return TermFactory.DEFAULT.createTerm(term.op(), subs,
188: origvars, term.javaBlock());
189: }
190:
191: with = syntacticalReplace(with, services, mc);
192:
193: if (maxSort instanceof AbstractSort) {
194: final boolean noCastNecessary = with.sort().extendsTrans(
195: maxSort);
196: if (!noCastNecessary) {
197: with = TermFactory.DEFAULT.createCastTerm(
198: (AbstractSort) maxSort, with);
199: }
200:
201: } else {
202: // maybe move getCastSymbol to sort interface
203: // in the meantime no casts are inserted
204: }
205:
206: return with;
207: }
208:
209: /**
210: * Check if p_pos contains an explicit metavariable instantiation,
211: * and creates in this case a new simple term by replacing the
212: * metavariable with the instantiation
213: */
214: private PosInOccurrence flatten(PosInOccurrence p_pos,
215: Services p_services) {
216: if (p_pos.termBelowMetavariable() != null) {
217: Term flatTerm = replace(p_pos.constrainedFormula()
218: .formula(), p_pos.termBelowMetavariable(), p_pos
219: .posInTerm().iterator(), p_services,
220: MatchConditions.EMPTY_MATCHCONDITIONS, Sort.FORMULA);
221:
222: PosInOccurrence pos = new PosInOccurrence(
223: new ConstrainedFormula(flatTerm, p_pos
224: .constrainedFormula().constraint()), p_pos
225: .posInTerm(), p_pos.isInAntec());
226:
227: IntIterator it = p_pos.posInTermBelowMetavariable()
228: .iterator();
229: while (it.hasNext())
230: pos = pos.down(it.next());
231:
232: return pos;
233: }
234:
235: return p_pos;
236: }
237:
238: /** CONSTRAINT NOT USED
239: * applies the replacewith part of Taclets
240: * @param gt TacletGoalTemplate used to get the replaceexpression in the Taclet
241: * @param goal the Goal where the rule is applied
242: * @param posOfFind the PosInOccurrence belonging to the find expression
243: * @param services the Services encapsulating all java information
244: * @param matchCond the MatchConditions with all required instantiations
245: */
246: protected void applyReplacewith(TacletGoalTemplate gt, Goal goal,
247: PosInOccurrence posOfFind, Services services,
248: MatchConditions matchCond) {
249: if (gt instanceof RewriteTacletGoalTemplate) {
250: PosInOccurrence flatPos = flatten(posOfFind, services);
251:
252: Term term = flatPos.constrainedFormula().formula();
253: IntIterator it = flatPos.posInTerm().iterator();
254: Term rwTemplate = ((RewriteTacletGoalTemplate) gt)
255: .replaceWith();
256:
257: Term result = replace(term, rwTemplate, it, services,
258: matchCond, term.sort());
259: Constraint c = matchCond.getConstraint();
260: if (createCopies(goal, posOfFind, matchCond))
261: goal.addFormula(new ConstrainedFormula(result, c),
262: posOfFind);
263: else
264: goal.changeFormula(new ConstrainedFormula(result, c),
265: posOfFind);
266: } else {
267: // Then there was no replacewith...
268: // This is strange in a RewriteTaclet, but who knows...
269: }
270: }
271:
272: /**
273: * adds the sequent of the add part of the Taclet to the goal sequent
274: * @param add the Sequent to be added
275: * @param goal the Goal to be updated
276: * @param posOfFind the PosInOccurrence describes the place where to add
277: * the semisequent
278: * @param services the Services encapsulating all java information
279: * @param matchCond the MatchConditions with all required instantiations
280: */
281: protected void applyAdd(Sequent add, Goal goal,
282: PosInOccurrence posOfFind, Services services,
283: MatchConditions matchCond) {
284: if (posOfFind.isInAntec()) {
285: addToAntec(add.antecedent(), goal, posOfFind, services,
286: matchCond);
287: addToSucc(add.succedent(), goal, null, services, matchCond);
288: } else {
289: addToAntec(add.antecedent(), goal, null, services,
290: matchCond);
291: addToSucc(add.succedent(), goal, posOfFind, services,
292: matchCond);
293: }
294: }
295:
296: protected Taclet setName(String s) {
297: final RewriteTacletBuilder b = new RewriteTacletBuilder();
298: b.setFind(find());
299: b.setStateRestriction(getStateRestriction());
300: return super .setName(s, b);
301: }
302:
303: StringBuffer toStringFind(StringBuffer sb) {
304: StringBuffer res = super .toStringFind(sb);
305: if (getStateRestriction() == SAME_UPDATE_LEVEL)
306: res.append("\\sameUpdateLevel\n");
307: else if (getStateRestriction() == IN_SEQUENT_STATE)
308: res.append("\\inSequentState\n");
309: return res;
310: }
311:
312: }
|