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.PosInTerm;
15: import de.uka.ilkd.key.logic.Term;
16: import de.uka.ilkd.key.proof.Goal;
17: import de.uka.ilkd.key.rule.RuleApp;
18:
19: /**
20: * Projection for computing a subterm of a given term. The position of the
21: * subterm within the complete term is described using a <code>PosInTerm</code>.
22: */
23: public class SubtermProjection implements ProjectionToTerm {
24:
25: private final PosInTerm pit;
26: private final ProjectionToTerm completeTerm;
27:
28: public static ProjectionToTerm create(
29: ProjectionToTerm completeTerm, PosInTerm pit) {
30: return new SubtermProjection(completeTerm, pit);
31: }
32:
33: private SubtermProjection(ProjectionToTerm completeTerm,
34: PosInTerm pit) {
35: this .completeTerm = completeTerm;
36: this .pit = pit;
37: }
38:
39: public Term toTerm(RuleApp app, PosInOccurrence pos, Goal goal) {
40: return completeTerm.toTerm(app, pos, goal).subAt(pit);
41: }
42: }
|