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 22.12.2004
11: */
12: package de.uka.ilkd.key.rule.updatesimplifier;
13:
14: import de.uka.ilkd.key.java.Services;
15: import de.uka.ilkd.key.logic.Term;
16: import de.uka.ilkd.key.logic.op.NonRigid;
17: import de.uka.ilkd.key.rule.AbstractUpdateRule;
18: import de.uka.ilkd.key.rule.UpdateSimplifier;
19: import de.uka.ilkd.key.util.Debug;
20:
21: /**
22: * @author bubel
23: * This rule is fall back rule for "unknown" terms with non rigid
24: * top level symbol and just prepends the Update.
25: */
26: public class ApplyOnNonRigidTerm extends AbstractUpdateRule {
27:
28: /**
29: * @param updateSimplifier the UpdateSimplifier to which this
30: * rule is attached
31: */
32: public ApplyOnNonRigidTerm(UpdateSimplifier updateSimplifier) {
33: super (updateSimplifier);
34: }
35:
36: /**
37: * this rule is applicable if the top level operator is a non rigid
38: * symbol
39: */
40: public boolean isApplicable(Update update, Term target) {
41: return target.op() instanceof NonRigid;
42: }
43:
44: /**
45: * implementation of the fall back rule for terms with an "unknown"
46: * non rigid top level symbol
47: */
48: public Term apply(Update update, Term target, Services services) {
49:
50: return UpdateSimplifierTermFactory.DEFAULT.createUpdateTerm(
51: update.getAllAssignmentPairs(), updateSimplifier()
52: .simplify(target, services));
53: }
54:
55: public Term matchingCondition(Update update, Term target,
56: Services services) {
57: // we don't really know what to do here ;-)
58: Debug.fail("no default implementation of "
59: + "matchingCondition(...) available");
60: return null; // unreachable
61: }
62: }
|