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:
11: package de.uka.ilkd.key.strategy.feature;
12:
13: import de.uka.ilkd.key.logic.PosInOccurrence;
14: import de.uka.ilkd.key.logic.Term;
15: import de.uka.ilkd.key.proof.Goal;
16: import de.uka.ilkd.key.rule.RuleApp;
17: import de.uka.ilkd.key.strategy.RuleAppCost;
18: import de.uka.ilkd.key.strategy.TopRuleAppCost;
19: import de.uka.ilkd.key.strategy.termProjection.ProjectionToTerm;
20: import de.uka.ilkd.key.strategy.termfeature.TermFeature;
21: import de.uka.ilkd.key.util.Debug;
22:
23: /**
24: * Feature for invoking a term feature on the instantiation of a schema variable
25: */
26: public class ApplyTFFeature implements Feature {
27:
28: private final ProjectionToTerm proj;
29: private final TermFeature termFeature;
30: private final RuleAppCost noInstCost;
31: private final boolean demandInst;
32:
33: /**
34: * @param schemaVar
35: * the schema variable whose instantiation is supposed to be
36: * inspected
37: * @param termFeature
38: * the term feature to use
39: * @param noInstCost
40: * result if <code>schemaVar</code> is not instantiated
41: * @param demandInst
42: * if <code>true</code> then raise an exception if
43: * <code>schemaVar</code> is not instantiated (otherwise:
44: * return <code>noInstCost</code>)
45: */
46: private ApplyTFFeature(ProjectionToTerm proj,
47: TermFeature termFeature, RuleAppCost noInstCost,
48: boolean demandInst) {
49: this .proj = proj;
50: this .termFeature = termFeature;
51: this .noInstCost = noInstCost;
52: this .demandInst = demandInst;
53: }
54:
55: public static Feature createNonStrict(ProjectionToTerm proj,
56: TermFeature tf, RuleAppCost noInstCost) {
57: return new ApplyTFFeature(proj, tf, noInstCost, false);
58: }
59:
60: public static Feature create(ProjectionToTerm proj, TermFeature tf) {
61: return new ApplyTFFeature(proj, tf, TopRuleAppCost.INSTANCE,
62: true);
63: }
64:
65: public RuleAppCost compute(RuleApp app, PosInOccurrence pos,
66: Goal goal) {
67: final Term te = proj.toTerm(app, pos, goal);
68: if (te == null) {
69: Debug.assertFalse(demandInst,
70: "ApplyTFFeature: got undefined argument (null)");
71: return noInstCost;
72: }
73:
74: return termFeature.compute(te);
75: }
76:
77: }
|