de.uka.ilkd.key.macros

Class TryCloseMacro

java.lang.Object

de.uka.ilkd.key.macros.AbstractProofMacro

de.uka.ilkd.key.macros.TryCloseMacro

All Implemented Interfaces:

ProofMacro

public class TryCloseMacro
extends AbstractProofMacro

The Class TryCloseMacro tries to close goals. Goals are either closed or left untouched. This uses the code provided by Michael Kirsten in InteractiveProver$AutoWorker. Unlike many macros, this macros has got a parameter (numberSteps), such that several instances of the class may exist with different semantics. The number of autosteps may be temporarily altered for this macro.

Author:

mattias ulbrich

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private static class	TryCloseMacro.TryCloseProgressBarListener

Nested classes/interfaces inherited from interface de.uka.ilkd.key.macros.ProofMacro

ProofMacro.ProgressBarListener

Field Summary

Fields

Modifier and Type	Field and Description
private int	numberSteps The max number of steps to be applied.

Constructor Summary

Constructors

Constructor and Description
TryCloseMacro() Instantiates a new try close macro.
TryCloseMacro(int numberSteps) Instantiates a new try close macro.

Method Summary

Modifier and Type	Method and Description
ProofMacroFinishedInfo	applyTo(UserInterfaceControl uic, Proof proof, ImmutableList<Goal> goals, PosInOccurrence posInOcc, ProverTaskListener listener) Apply this macro on the given goals.
boolean	canApplyTo(Proof proof, ImmutableList<Goal> goals, PosInOccurrence posInOcc) Can this macro be applied on the given goals?
java.lang.String	getCategory() Gets the category of this macro.
java.lang.String	getDescription() Gets the description of this macro.
java.lang.String	getName() Gets the name of this macro.
java.lang.String	getScriptCommandName() Gets a unique short name for this macro that can be used in proof scripts.
private static ImmutableList<Goal>	setDifference(ImmutableList<Goal> goals1, ImmutableList<Goal> goals2)

Methods inherited from class de.uka.ilkd.key.macros.AbstractProofMacro

applyTo, canApplyTo, getMaxSteps, hasParameter, resetParams, setParameter

Methods inherited from class java.lang.Object

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

Field Detail

numberSteps

private final int numberSteps

The max number of steps to be applied. A value of -1 means no changes. This value may differ between instances of this class;

Constructor Detail

TryCloseMacro

public TryCloseMacro()

Instantiates a new try close macro. No changes to the max number of steps.

TryCloseMacro

public TryCloseMacro(int numberSteps)

Instantiates a new try close macro.

Parameters:

numberSteps - the max number of steps. -1 means no change.

Method Detail

getName

public java.lang.String getName()

Description copied from interface: ProofMacro

Gets the name of this macro. Used as menu entry

Returns:

a non-null constant string

getScriptCommandName

public java.lang.String getScriptCommandName()

Description copied from class: AbstractProofMacro

Gets a unique short name for this macro that can be used in proof scripts. If null is returned, the macro cannot be addressed from within scripts. By default, proof macros do not support scripts, thus null is returned.

Specified by:

getScriptCommandName in interface ProofMacro

Overrides:

getScriptCommandName in class AbstractProofMacro

Returns:

null if not supported, or a non-null constant string as the short name

getCategory

public java.lang.String getCategory()

Description copied from interface: ProofMacro

Gets the category of this macro. Used as name of the menu under which the macro is sorted. Return null if no submenu is to be created.

Returns:

a constant string, or null

getDescription

public java.lang.String getDescription()

Description copied from interface: ProofMacro

Gets the description of this macro. Used as tooltip.

Returns:

a non-null constant string

canApplyTo

public boolean canApplyTo(Proof proof,
                          ImmutableList<Goal> goals,
                          PosInOccurrence posInOcc)

Description copied from interface: ProofMacro

Can this macro be applied on the given goals? This method should not make any changes but check if the macro can be applied or not on the given goals. This method may be called from within the GUI thread and be compatible with that fact.

Parameters:

proof - the current Proof (not null)

goals - the goals (not null)

posInOcc - the position in occurrence (may be null)

Returns:

true, if the macro is allowed to be applied

applyTo

public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic,
                                      Proof proof,
                                      ImmutableList<Goal> goals,
                                      PosInOccurrence posInOcc,
                                      ProverTaskListener listener)
                               throws java.lang.InterruptedException

Description copied from interface: ProofMacro

Apply this macro on the given goals. This method can change the proof by applying rules to it. This method is usually called from a dedicated thread and not the GUI thread. The thread it runs on may be interrupted. In this case, the macro may report the interruption by an InterruptedException. A ProverTaskListener can be provided to which the progress will be reported. If no reports are desired, null cna be used for this parameter. If more than one listener is needed, consider combining them using a single listener object using the composite pattern.

Parameters:

uic - the UserInterfaceControl to use

proof - the current Proof (not null)

goals - the goals (not null)

posInOcc - the position in occurrence (may be null)

listener - the listener to use for progress reports (may be null)

Throws:

java.lang.InterruptedException - if the application of the macro has been interrupted.

setDifference

private static ImmutableList<Goal> setDifference(ImmutableList<Goal> goals1,
                                                 ImmutableList<Goal> goals2)