public class TacletAppIntermediate extends AppIntermediate
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.
|
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() |
getLineNr, setLineNr
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)
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.public java.lang.String getRuleName()
getRuleName
in class AppIntermediate
public java.util.LinkedList<java.lang.String> getInsts()
public ImmutableList<java.lang.String> getIfSeqFormulaList()
public ImmutableList<java.lang.String> getIfDirectFormulaList()
public ImmutableList<Name> getNewNames()
getNewNames
in class AppIntermediate
Copyright © 2003-2019 The KeY-Project.