public abstract class AbstractProofMacro extends java.lang.Object implements ProofMacro
#finishAfterMacro()
for compound macros
(see description in ProofMacro#finishAfterMacro()
).ProofMacro.ProgressBarListener
Constructor and Description |
---|
AbstractProofMacro() |
Modifier and Type | Method and Description |
---|---|
ProofMacroFinishedInfo |
applyTo(UserInterfaceControl uic,
Node node,
PosInOccurrence posInOcc,
ProverTaskListener listener)
Apply this macro on the given node.
|
boolean |
canApplyTo(Node node,
PosInOccurrence posInOcc)
Can this macro be applied on the given node?
|
private static ImmutableList<Goal> |
getGoals(Node node) |
protected int |
getMaxSteps(Proof proof)
Gets the maximum number of rule applications allowed for a macro.
|
java.lang.String |
getScriptCommandName()
Gets a unique short name for this macro that can be used in proof
scripts.
|
boolean |
hasParameter(java.lang.String paramName)
Checks whether this
ProofMacro has a parameter named
paramName . |
void |
resetParams()
Resets the macro parameters to their defaults.
|
void |
setParameter(java.lang.String paramName,
java.lang.String paramValue)
Sets the parameter named
paramName to the given String
representation in paramValue . |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
applyTo, canApplyTo, getCategory, getDescription, getName
private static ImmutableList<Goal> getGoals(Node node)
public java.lang.String getScriptCommandName()
null
is returned, the macro cannot be addressed from
within scripts.
By default, proof macros do not support scripts, thus null
is returned.getScriptCommandName
in interface ProofMacro
null
if not supported, or a non-null
constant string as the short namepublic boolean hasParameter(java.lang.String paramName)
ProofMacro
ProofMacro
has a parameter named
paramName
. For use in proof scripts.hasParameter
in interface ProofMacro
paramName
- The name to check.ProofMacro
has a parameter named
paramName
.public void setParameter(java.lang.String paramName, java.lang.String paramValue) throws java.lang.IllegalArgumentException
ProofMacro
paramName
to the given String
representation in paramValue
. For use in proof scripts.setParameter
in interface ProofMacro
paramName
- The name of the parameter.paramValue
- The value of the parameter.java.lang.IllegalArgumentException
- if there is no parameter of that name or the value is
incorrectly formatted (e.g., cannot be converted to a
number).public void resetParams()
ProofMacro
resetParams
in interface ProofMacro
public boolean canApplyTo(Node node, PosInOccurrence posInOcc)
ProofMacro
ProofMacro.canApplyTo(Proof, ImmutableList, PosInOccurrence)
with
node.proof()
as proof and all open goals below
node
.canApplyTo
in interface ProofMacro
node
- the node (not null
)posInOcc
- the position in occurrence (may be null
)true
, if the macro is allowed to be appliedpublic ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Node node, PosInOccurrence posInOcc, ProverTaskListener listener) throws java.lang.InterruptedException, java.lang.Exception
ProofMacro
InterruptedException
.
A ProverTaskListener
can be provided to which the progress will
be reported. If no reports are desired, null
can be used for
this parameter. If more than one listener is needed, consider combining
them using a single listener object using the composite pattern.applyTo
in interface ProofMacro
uic
- the UserInterfaceControl
to usenode
- the node (not null
)posInOcc
- the position in occurrence (may be null
)listener
- the listener to use for progress reports (may be
null
)java.lang.InterruptedException
- if the application of the macro has been interrupted.java.lang.Exception
protected final int getMaxSteps(Proof proof)