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

Class BuiltInAppIntermediate

java.lang.Object

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

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

Direct Known Subclasses:

MergeAppIntermediate, MergePartnerAppIntermediate

public class BuiltInAppIntermediate
extends AppIntermediate

Encapsulates intermediate information for constructing a built-in rule application.

Author:

Dominic Scheurer

Field Summary

Fields

Modifier and Type	Field and Description
private ImmutableList<Pair<java.lang.Integer,PosInTerm>>	builtInIfInsts
private java.lang.String	contract
private ImmutableList<Name>	newNames
private Pair<java.lang.Integer,PosInTerm>	posInfo
private java.lang.String	ruleName

Constructor Summary

Constructors

Constructor and Description
BuiltInAppIntermediate(java.lang.String ruleName, Pair<java.lang.Integer,PosInTerm> pos, java.lang.String contract, ImmutableList<Pair<java.lang.Integer,PosInTerm>> builtInIfInsts, ImmutableList<Name> newNames)

Method Summary

Modifier and Type	Method and Description
ImmutableList<Pair<java.lang.Integer,PosInTerm>>	getBuiltInIfInsts()
java.lang.String	getContract()
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

ruleName

private java.lang.String ruleName

posInfo

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

contract

private java.lang.String contract

builtInIfInsts

private ImmutableList<Pair<java.lang.Integer,PosInTerm>> builtInIfInsts

newNames

private ImmutableList<Name> newNames

Constructor Detail

BuiltInAppIntermediate

public BuiltInAppIntermediate(java.lang.String ruleName,
                              Pair<java.lang.Integer,PosInTerm> pos,
                              java.lang.String contract,
                              ImmutableList<Pair<java.lang.Integer,PosInTerm>> builtInIfInsts,
                              ImmutableList<Name> newNames)

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()

getContract

public java.lang.String getContract()

getBuiltInIfInsts

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

getNewNames

public ImmutableList<Name> getNewNames()

Specified by:

getNewNames in class AppIntermediate

Returns:

The new names registered in the course of this app.