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.termProjection;
12:
13: import de.uka.ilkd.key.java.Services;
14: import de.uka.ilkd.key.logic.Constraint;
15: import de.uka.ilkd.key.logic.Name;
16: import de.uka.ilkd.key.logic.PosInOccurrence;
17: import de.uka.ilkd.key.logic.Term;
18: import de.uka.ilkd.key.proof.Goal;
19: import de.uka.ilkd.key.rule.RuleApp;
20: import de.uka.ilkd.key.rule.SyntacticalReplaceVisitor;
21: import de.uka.ilkd.key.rule.TacletApp;
22: import de.uka.ilkd.key.util.Debug;
23:
24: /**
25: * Projection of taclet apps to the instantiation of a schema variable. The
26: * projection can either be partial and undefined for those apps that do not
27: * instantiate the schema variable in question, or it can raise an error for
28: * such applications
29: */
30: public class SVInstantiationProjection implements ProjectionToTerm {
31:
32: private final Name svName;
33: private final boolean demandInst;
34:
35: private SVInstantiationProjection(Name svName, boolean demandInst) {
36: this .svName = svName;
37: this .demandInst = demandInst;
38: }
39:
40: public static SVInstantiationProjection create(Name svName,
41: boolean demandInst) {
42: return new SVInstantiationProjection(svName, demandInst);
43: }
44:
45: public Term toTerm(RuleApp app, PosInOccurrence pos, Goal goal) {
46: if (!(app instanceof TacletApp))
47: Debug.fail("Projection is only applicable to taclet apps,"
48: + " but got " + app);
49:
50: final TacletApp tapp = (TacletApp) app;
51: final Object instObj = tapp.instantiations()
52: .lookupValue(svName);
53: if (!(instObj instanceof Term)) {
54: Debug.assertFalse(demandInst,
55: "Did not find schema variable " + svName
56: + " that I was supposed to examine"
57: + " (taclet " + tapp.taclet().name() + ")");
58: return null;
59: }
60: return instMVs((Term) instObj, tapp, goal);
61: }
62:
63: private static Term instMVs(Term te, TacletApp tacletApp, Goal goal) {
64: final Services services = goal.proof().getServices();
65: final Constraint uc = goal.proof().getUserConstraint()
66: .getConstraint();
67: final Constraint tacletConstraint = tacletApp.constraint();
68: final Constraint displayConstraint = tacletConstraint.join(uc,
69: services);
70:
71: if (displayConstraint.isBottom())
72: return te;
73:
74: // Substitute metavariables of the term
75: final SyntacticalReplaceVisitor srv = new SyntacticalReplaceVisitor(
76: displayConstraint);
77: te.execPostOrder(srv);
78: return srv.getTerm();
79: }
80:
81: }
|