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 15.12.2004
011: */
012: package de.uka.ilkd.key.rule.updatesimplifier;
013:
014: import de.uka.ilkd.key.java.Services;
015: import de.uka.ilkd.key.logic.Term;
016: import de.uka.ilkd.key.logic.op.*;
017: import de.uka.ilkd.key.rule.AbstractUpdateRule;
018: import de.uka.ilkd.key.rule.UpdateSimplifier;
019:
020: /**
021: * Applies an anonymous update on a term with a non-rigid operator as top
022: * level symbol. The update is added in front of the terms and also recursively
023: * applied on the subterms.
024: */
025: public class ApplyAnonymousUpdateOnNonRigid extends AbstractUpdateRule {
026:
027: /**
028: * @param updateSimplifier
029: */
030: public ApplyAnonymousUpdateOnNonRigid(
031: UpdateSimplifier updateSimplifier) {
032: super (updateSimplifier);
033: }
034:
035: /* (non-Javadoc)
036: * @see de.uka.ilkd.key.rule.UpdateRule#isApplicable(de.uka.ilkd.key.rule.updatesimplifier.Update, de.uka.ilkd.key.logic.Term)
037: */
038: public boolean isApplicable(Update update, Term target) {
039: final Operator op = target.op();
040: return update.isAnonymousUpdate() && op instanceof NonRigid
041: && !(op instanceof AnonymousUpdate);
042: }
043:
044: /**
045: * in case of a non-state changing non rigid top level operator, the anonymous update is also
046: * propagated to the subterm
047: * @param Term target the Term where to apply the anonymous update
048: * @return the term after pushing the update to the subterms
049: */
050: private Term pushToSubterms(Update update, Term target,
051: Services services) {
052: Term result = target;
053: final PropagationResult pr = propagateUpdateToSubterms(update,
054: target, services);
055: final Term[] subs = pr.getSimplifiedSubterms();
056: final ArrayOfQuantifiableVariable[] vars = pr
057: .getBoundVariables();
058:
059: if (pr.hasChanged()) {
060: result = UpdateSimplifierTermFactory.DEFAULT
061: .getBasicTermFactory().createTerm(target.op(),
062: subs, vars, target.javaBlock());
063: } else {
064: result = target;
065: }
066:
067: return result;
068: }
069:
070: /**
071: * applies the annonymous update on the target term
072: */
073: public Term apply(Update update, Term target, Services services) {
074: // use update simplifier termfactory in particular to be sure to create correct
075: // anonymous updates
076: logEnter(update, target);
077:
078: Term result = updateSimplifier().simplify(target, services);
079:
080: if (result.op() != target.op() && !isApplicable(update, result)) {
081: result = updateSimplifier().simplify(update, result,
082: services);
083: logExit(result);
084: return result;
085: }
086:
087: // push to sub terms if no state changing operator
088: if (!(result.op() instanceof Modality || result.op() instanceof IUpdateOperator)) {
089: result = pushToSubterms(update, result, services);
090: }
091:
092: // add anonymous update in front of the term
093:
094: result = UpdateSimplifierTermFactory.DEFAULT.createUpdateTerm(
095: update.getAllAssignmentPairs(), result);
096:
097: logExit(result);
098: return result;
099: }
100:
101: public Term matchingCondition(Update update, Term target,
102: Services services) {
103: // anonymous updates will always affect the value of a non-rigid symbol
104: // ... really? /PR
105: return UpdateSimplifierTermFactory.DEFAULT.getValidGuard();
106: }
107: }
|