01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: /*
10: * Created on 26.11.2004
11: *
12: * TODO To change the template for this generated file go to
13: * Window - Preferences - Java - Code Style - Code Templates
14: */
15: package de.uka.ilkd.key.rule.updatesimplifier;
16:
17: import de.uka.ilkd.key.java.Services;
18: import de.uka.ilkd.key.logic.Term;
19: import de.uka.ilkd.key.logic.op.ArrayOfQuantifiableVariable;
20: import de.uka.ilkd.key.logic.op.Location;
21: import de.uka.ilkd.key.logic.op.NonRigid;
22: import de.uka.ilkd.key.rule.AbstractUpdateRule;
23: import de.uka.ilkd.key.rule.UpdateSimplifier;
24: import de.uka.ilkd.key.util.Debug;
25:
26: /**
27: * Applies an update on a term whose top level operator is
28: * a rigid operator. In fact, the update is and needs only be
29: * passed through to the subterms
30: */
31: public class ApplyOnRigidOperatorTerm extends AbstractUpdateRule {
32:
33: /**
34: * @param updateSimplifier
35: */
36: public ApplyOnRigidOperatorTerm(UpdateSimplifier us) {
37: super (us);
38: }
39:
40: /* (non-Javadoc)
41: * @see de.uka.ilkd.key.rule.UpdateRule#isApplicable(de.uka.ilkd.key.rule.updatesimplifier.Update, de.uka.ilkd.key.logic.Term)
42: */
43: public boolean isApplicable(Update update, Term target) {
44: return !(target.op() instanceof NonRigid);
45: }
46:
47: /*
48: * (non-Javadoc)
49: *
50: * @see de.uka.ilkd.key.rule.UpdateRule#apply(de.uka.ilkd.key.rule.updatesimplifier.Update,
51: * de.uka.ilkd.key.logic.Term)
52: */
53: public Term apply(Update update, Term target, Services services) {
54: final Term result;
55:
56: final PropagationResult pr = propagateUpdateToSubterms(update,
57: target, services);
58: final Term[] subs = pr.getSimplifiedSubterms();
59: final ArrayOfQuantifiableVariable[] vars = pr
60: .getBoundVariables();
61:
62: if (pr.hasChanged()) {
63: result = UpdateSimplifierTermFactory.DEFAULT
64: .getBasicTermFactory().createTerm(target.op(),
65: subs, vars, target.javaBlock());
66: } else {
67: result = target;
68: }
69:
70: return result;
71: }
72:
73: public Term matchingCondition(Update update, Term target,
74: Services services) {
75: // these rigid operators should not be locations,
76: // otherwise something is very wrong
77: Debug.assertFalse(target.op() instanceof Location,
78: "Rewrite me!");
79: Debug
80: .fail("matchingCondition(...) must not be called for target "
81: + target);
82: return null; // unreachable
83: }
84: }
|