de.uka.ilkd.key.strategy.termProjection

Class FocusProjection

java.lang.Object

de.uka.ilkd.key.strategy.termProjection.FocusProjection

All Implemented Interfaces:

ProjectionToTerm

public class FocusProjection
extends java.lang.Object
implements ProjectionToTerm

Projection of a rule application to its focus (the term or formula that the rule operates on, that for taclets is described using \find, and that can be modified by the rule). Optionally, the projection can walk "upwards" towards the root of the term/formula

Field Summary

Fields

Modifier and Type	Field and Description
static ProjectionToTerm	INSTANCE
private int	stepsUpwards

Constructor Summary

Constructors

Modifier	Constructor and Description
private	FocusProjection(int stepsUpwards)

Method Summary

Modifier and Type	Method and Description
static ProjectionToTerm	create(int stepsUpwards)
Term	toTerm(RuleApp app, PosInOccurrence pos, Goal goal)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

INSTANCE

public static final ProjectionToTerm INSTANCE

stepsUpwards

private final int stepsUpwards

Constructor Detail

FocusProjection

private FocusProjection(int stepsUpwards)

Method Detail

create

public static ProjectionToTerm create(int stepsUpwards)

toTerm

public Term toTerm(RuleApp app,
                   PosInOccurrence pos,
                   Goal goal)

Specified by:

toTerm in interface ProjectionToTerm