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.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.rule.TacletApp;
18:
19: /**
20: * Term projection that delivers the assumptions of a taclet application
21: * (the formulas that the \assumes clause of the taclet refers to).
22: */
23: public class AssumptionProjection implements ProjectionToTerm {
24:
25: private final int no;
26:
27: private AssumptionProjection(int no) {
28: this .no = no;
29: }
30:
31: public static ProjectionToTerm create(int no) {
32: return new AssumptionProjection(no);
33: }
34:
35: public Term toTerm(RuleApp app, PosInOccurrence pos, Goal goal) {
36: assert app instanceof TacletApp : "Projection is only applicable to taclet apps,"
37: + " but got " + app;
38: final TacletApp tapp = (TacletApp) app;
39:
40: assert tapp.ifFormulaInstantiations() != null : "Projection is only applicable to taclet apps with assumptions,"
41: + " but got " + app;
42:
43: return tapp.ifFormulaInstantiations().take(no).head()
44: .getConstrainedFormula().formula();
45: }
46: }
|