de.uka.ilkd.key.rule

Class Taclet.TacletLabelHint

java.lang.Object

de.uka.ilkd.key.rule.Taclet.TacletLabelHint

Enclosing class:

Taclet

public static class Taclet.TacletLabelHint
extends java.lang.Object

Instances of this class are used as hints to maintain TermLabels.

Author:

Martin Hentschel

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	Taclet.TacletLabelHint.TacletOperation Defines the possible operations a Taclet performs.

Field Summary

Fields

Modifier and Type	Field and Description
private Sequent	sequent The optional Sequent of the add or replace part of the taclet.
private SequentFormula	sequentFormula The optional SequentFormula contained in getSequent().
private Taclet.TacletLabelHint.TacletOperation	tacletOperation The currently performed operation.
private java.util.Deque<Term>	tacletTermStack The stack maintained during application of a taclet Term.
private Term	term The optional replace Term of the taclet.

Constructor Summary

Constructors

Constructor and Description
TacletLabelHint(Taclet.TacletLabelHint.TacletOperation tacletOperation, Sequent sequent) Constructor.
TacletLabelHint(Taclet.TacletLabelHint labelHint, SequentFormula sequentFormula) Constructor.
TacletLabelHint(Term term) Constructor.

Method Summary

Modifier and Type	Method and Description
Sequent	getSequent() Returns the optional Sequent of the add or replace part of the taclet.
SequentFormula	getSequentFormula() Returns the optional SequentFormula contained in getSequent().
Taclet.TacletLabelHint.TacletOperation	getTacletOperation() Returns the currently performed operation.
java.util.Deque<Term>	getTacletTermStack() Returns the stack maintained during application of a taclet Term.
Term	getTerm() Returns the optional replace Term of the taclet.
void	setTacletTermStack(java.util.Deque<Term> tacletTermStack) Sets the stack maintained during application of a taclet Term.
java.lang.String	toString()

Methods inherited from class java.lang.Object

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

Field Detail

tacletOperation

private final Taclet.TacletLabelHint.TacletOperation tacletOperation

The currently performed operation.

sequent

private final Sequent sequent

The optional Sequent of the add or replace part of the taclet.

sequentFormula

private final SequentFormula sequentFormula

The optional SequentFormula contained in getSequent().

term

private final Term term

The optional replace Term of the taclet.

tacletTermStack

private java.util.Deque<Term> tacletTermStack

The stack maintained during application of a taclet Term.

Constructor Detail

TacletLabelHint

public TacletLabelHint(Taclet.TacletLabelHint.TacletOperation tacletOperation,
                       Sequent sequent)

Constructor.

Parameters:

tacletOperation - The currently performed operation.

sequent - The optional Sequent of the add or replace part of the taclet.

TacletLabelHint

public TacletLabelHint(Term term)

Constructor.

Parameters:

tacletOperation - The currently performed operation.

term - The optional replace Term of the taclet.

TacletLabelHint

public TacletLabelHint(Taclet.TacletLabelHint labelHint,
                       SequentFormula sequentFormula)

Constructor.

Parameters:

labelHint - The previous Taclet.TacletLabelHint which is now specialised.

sequentFormula - The optional SequentFormula contained in getSequent().

Method Detail

getTacletOperation

public Taclet.TacletLabelHint.TacletOperation getTacletOperation()

Returns the currently performed operation.

Returns:

The currently performed operation.

getSequent

public Sequent getSequent()

Returns the optional Sequent of the add or replace part of the taclet.

Returns:

The optional Sequent of the add or replace part of the taclet.

getSequentFormula

public SequentFormula getSequentFormula()

Returns the optional SequentFormula contained in getSequent().

Returns:

The optional SequentFormula contained in getSequent().

getTacletTermStack

public java.util.Deque<Term> getTacletTermStack()

Returns the stack maintained during application of a taclet Term.

Returns:

The stack maintained during application of a taclet Term.

setTacletTermStack

public void setTacletTermStack(java.util.Deque<Term> tacletTermStack)

Sets the stack maintained during application of a taclet Term.

Parameters:

tacletTermStack - The stack maintained during application of a taclet Term.

getTerm

public Term getTerm()

Returns the optional replace Term of the taclet.

Returns:

The optional replace Term of the taclet.

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object