de.uka.ilkd.key.proof.io.intermediate

Class TacletAppIntermediate

java.lang.Object

de.uka.ilkd.key.proof.io.intermediate.AppIntermediate

de.uka.ilkd.key.proof.io.intermediate.TacletAppIntermediate

public class TacletAppIntermediate
extends AppIntermediate

Encapsulates intermediate information for constructing a taclet application.

Author:

Dominic Scheurer

Field Summary

Fields

Modifier and Type	Field and Description
private ImmutableList<java.lang.String>	ifDirectFormulaList
private ImmutableList<java.lang.String>	ifSeqFormulaList
private java.util.LinkedList<java.lang.String>	insts
private ImmutableList<Name>	newNames
private Pair<java.lang.Integer,PosInTerm>	posInfo
private java.lang.String	tacletName

Constructor Summary

Constructors

Constructor and Description
TacletAppIntermediate(java.lang.String tacletName, Pair<java.lang.Integer,PosInTerm> posInfo, java.util.LinkedList<java.lang.String> insts, ImmutableList<java.lang.String> ifSeqFormulaList, ImmutableList<java.lang.String> ifDirectFormulaList, ImmutableList<Name> newNames) Constructs a new intermediate taclet application.

Method Summary

Modifier and Type	Method and Description
ImmutableList<java.lang.String>	getIfDirectFormulaList()
ImmutableList<java.lang.String>	getIfSeqFormulaList()
java.util.LinkedList<java.lang.String>	getInsts()
ImmutableList<Name>	getNewNames()
Pair<java.lang.Integer,PosInTerm>	getPosInfo()
java.lang.String	getRuleName()

Methods inherited from class de.uka.ilkd.key.proof.io.intermediate.AppIntermediate

getLineNr, setLineNr

Methods inherited from class java.lang.Object

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

Field Detail

tacletName

private java.lang.String tacletName

posInfo

private Pair<java.lang.Integer,PosInTerm> posInfo

insts

private java.util.LinkedList<java.lang.String> insts

ifSeqFormulaList

private ImmutableList<java.lang.String> ifSeqFormulaList

ifDirectFormulaList

private ImmutableList<java.lang.String> ifDirectFormulaList

newNames

private ImmutableList<Name> newNames

Constructor Detail

TacletAppIntermediate

public TacletAppIntermediate(java.lang.String tacletName,
                             Pair<java.lang.Integer,PosInTerm> posInfo,
                             java.util.LinkedList<java.lang.String> insts,
                             ImmutableList<java.lang.String> ifSeqFormulaList,
                             ImmutableList<java.lang.String> ifDirectFormulaList,
                             ImmutableList<Name> newNames)

Constructs a new intermediate taclet application.

Parameters:

tacletName - Name of the taclet.

posInfo - Position information (Integer representing position of the target formula, PosInTerm for relevant term inside the formula).

insts - Schema variable instantiations.

ifSeqFormulaList -

ifDirectFormulaList -

newNames - New names registered during taclet application.

Method Detail

getRuleName

public java.lang.String getRuleName()

Specified by:

getRuleName in class AppIntermediate

Returns:

The name of this taclet / built in rule.

getPosInfo

public Pair<java.lang.Integer,PosInTerm> getPosInfo()

getInsts

public java.util.LinkedList<java.lang.String> getInsts()

getIfSeqFormulaList

public ImmutableList<java.lang.String> getIfSeqFormulaList()

getIfDirectFormulaList

public ImmutableList<java.lang.String> getIfDirectFormulaList()

getNewNames

public ImmutableList<Name> getNewNames()

Specified by:

getNewNames in class AppIntermediate

Returns:

The new names registered in the course of this app.