de.uka.ilkd.key.control

Class AbstractProofControl

java.lang.Object

de.uka.ilkd.key.control.AbstractProofControl

All Implemented Interfaces:

ProofControl

Direct Known Subclasses:

DefaultProofControl, MediatorProofControl

public abstract class AbstractProofControl
extends java.lang.Object
implements ProofControl

Provides a basic implementation of ProofControl.

Author:

Martin Hentschel

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	AbstractProofControl.FocussedAutoModeTaskListener TODO

Field Summary

Fields

Modifier and Type	Field and Description
private java.util.List<AutoModeListener>	autoModeListener Contains all available AutoModeListener.
private ProverTaskListener	defaultProverTaskListener The default ProverTaskListener which will be added to all started ApplyStrategy instances.
protected java.util.List<InteractionListener>	interactionListeners
private boolean	minimizeInteraction
private RuleCompletionHandler	ruleCompletionHandler Optionally, the RuleCompletionHandler to use.

Constructor Summary

Constructors

Constructor and Description
AbstractProofControl(ProverTaskListener defaultProverTaskListener) Constructor.
AbstractProofControl(ProverTaskListener defaultProverTaskListener, RuleCompletionHandler ruleCompletionHandler) Constructor.

Method Summary

Modifier and Type	Method and Description
void	addAutoModeListener(AutoModeListener p)
void	addInteractionListener(InteractionListener listener)
void	applyInteractive(RuleApp app, Goal goal) Apply a RuleApp and continue with update simplification or strategy application according to current settings.
TacletInstantiationModel[]	completeAndApplyApp(java.util.List<TacletApp> apps, Goal goal)
protected void	completeAndApplyTacletMatch(TacletInstantiationModel[] models, Goal goal)
protected IBuiltInRuleApp	completeBuiltInRuleApp(IBuiltInRuleApp app, Goal goal, boolean forced)
static IBuiltInRuleApp	completeBuiltInRuleAppByDefault(IBuiltInRuleApp app, Goal goal, boolean forced) Default implementation of RuleCompletionHandler.completeBuiltInRuleApp(IBuiltInRuleApp, Goal, boolean).
TacletInstantiationModel	createModel(TacletApp app, Goal goal)
protected void	emitInteractivePrune(Node node)
protected void	emitInteractiveRuleApplication(Goal goal, RuleApp app)
private ImmutableList<TacletApp>	filterTaclet(Goal focusedGoal, ImmutableList<NoPosTacletApp> tacletInstances, PosInOccurrence pos) takes NoPosTacletApps as arguments and returns a duplicate free list of the contained TacletApps
protected void	fireAutoModeStarted(ProofEvent e) fires the event that automatic execution has started
protected void	fireAutoModeStopped(ProofEvent e) fires the event that automatic execution has stopped
protected ImmutableSet<TacletApp>	getAppsForName(Goal goal, java.lang.String name, PosInOccurrence pos) collects all Taclet applications at the given position of the specified taclet
protected ImmutableSet<TacletApp>	getAppsForName(Goal goal, java.lang.String name, PosInOccurrence pos, TacletFilter filter) collects all taclet applications for the given position and taclet (identified by its name) matching the filter condition
ImmutableList<BuiltInRule>	getBuiltInRule(Goal focusedGoal, PosInOccurrence pos) collects all built-in rules that are applicable at the given sequent position 'pos'.
ImmutableSet<IBuiltInRuleApp>	getBuiltInRuleApp(Goal focusedGoal, BuiltInRule rule, PosInOccurrence pos) collects all built-in rule applications for the given rule that are applicable at position 'pos' and the current user constraint
protected ImmutableSet<IBuiltInRuleApp>	getBuiltInRuleAppsForName(Goal focusedGoal, java.lang.String name, PosInOccurrence pos) collects all applications of a rule given by its name at a give position in the sequent
ProverTaskListener	getDefaultProverTaskListener() Returns the default ProverTaskListener which will be added to all started ApplyStrategy instances.
ImmutableList<TacletApp>	getFindTaclet(Goal focusedGoal, PosInOccurrence pos) collects all applicable FindTaclets of the current goal (called by the SequentViewer)
ImmutableList<TacletApp>	getNoFindTaclet(Goal focusedGoal) collects all applicable NoFindTaclets of the current goal (called by the SequentViewer)
ImmutableList<TacletApp>	getRewriteTaclet(Goal focusedGoal, PosInOccurrence pos) collects all applicable RewriteTaclets of the current goal (called by the SequentViewer)
boolean	isAutoModeSupported(Proof proof) Checks if the auto mode of this UserInterfaceControl supports the given Proof.
boolean	isMinimizeInteraction()
void	pruneTo(Goal goal) Undo the last rule application on the given goal.
void	pruneTo(Node node) Prunes a proof to the given node.
void	removeAutoModeListener(AutoModeListener p)
void	removeInteractionListener(InteractionListener listener)
void	selectedBuiltInRule(Goal goal, BuiltInRule rule, PosInOccurrence pos, boolean forced) selected rule to apply
boolean	selectedTaclet(Taclet taclet, Goal goal, PosInOccurrence pos)
void	setMinimizeInteraction(boolean minimizeInteraction)
void	startAndWaitForAutoMode(Proof proof) Starts the auto mode for the given proof which must be contained in this user interface and blocks the current thread until it has finished.
void	startAndWaitForAutoMode(Proof proof, ImmutableList<Goal> goals) Starts the auto mode for the given proof which must be contained in this user interface and blocks the current thread until it has finished.
void	startAutoMode(Proof proof) Starts the auto mode for the given Proof.
void	startAutoMode(Proof proof, ImmutableList<Goal> goals) Starts the auto mode for the given Proof and the given Goals.
protected abstract void	startAutoMode(Proof proof, ImmutableList<Goal> goals, ProverTaskListener ptl)
void	startFocussedAutoMode(PosInOccurrence focus, Goal goal) starts the execution of rules with active strategy.
void	stopAndWaitAutoMode() Stops the currently running auto mode and blocks the current Thread until auto mode has stopped.

Methods inherited from class java.lang.Object

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

Methods inherited from interface de.uka.ilkd.key.control.ProofControl

isInAutoMode, runMacro, stopAutoMode, waitWhileAutoMode

Field Detail

ruleCompletionHandler

private final RuleCompletionHandler ruleCompletionHandler

Optionally, the RuleCompletionHandler to use.

defaultProverTaskListener

private final ProverTaskListener defaultProverTaskListener

The default ProverTaskListener which will be added to all started ApplyStrategy instances.

autoModeListener

private final java.util.List<AutoModeListener> autoModeListener

Contains all available AutoModeListener.

minimizeInteraction

private boolean minimizeInteraction

interactionListeners

protected final java.util.List<InteractionListener> interactionListeners

Constructor Detail

AbstractProofControl

public AbstractProofControl(ProverTaskListener defaultProverTaskListener)

Constructor.

Parameters:

defaultProverTaskListener - The default ProverTaskListener which will be added to all started ApplyStrategy instances.

AbstractProofControl

public AbstractProofControl(ProverTaskListener defaultProverTaskListener,
                            RuleCompletionHandler ruleCompletionHandler)

Constructor.

Parameters:

defaultProverTaskListener - The default ProverTaskListener which will be added to all started ApplyStrategy instances.

ruleCompletionHandler - An optional RuleCompletionHandler.

Method Detail

getDefaultProverTaskListener

public ProverTaskListener getDefaultProverTaskListener()

Returns the default ProverTaskListener which will be added to all started ApplyStrategy instances.

Specified by:

getDefaultProverTaskListener in interface ProofControl

Returns:

The default ProverTaskListener which will be added to all started ApplyStrategy instances.

isMinimizeInteraction

public boolean isMinimizeInteraction()

Specified by:

isMinimizeInteraction in interface ProofControl

setMinimizeInteraction

public void setMinimizeInteraction(boolean minimizeInteraction)

Specified by:

setMinimizeInteraction in interface ProofControl

getBuiltInRule

public ImmutableList<BuiltInRule> getBuiltInRule(Goal focusedGoal,
                                                 PosInOccurrence pos)

Description copied from interface: ProofControl

collects all built-in rules that are applicable at the given sequent position 'pos'.

Specified by:

getBuiltInRule in interface ProofControl

pos - the PosInSequent where to look for applicable rules

getNoFindTaclet

public ImmutableList<TacletApp> getNoFindTaclet(Goal focusedGoal)

Description copied from interface: ProofControl

collects all applicable NoFindTaclets of the current goal (called by the SequentViewer)

Specified by:

getNoFindTaclet in interface ProofControl

Returns:

a list of Taclets with all applicable NoFindTaclets

getFindTaclet

public ImmutableList<TacletApp> getFindTaclet(Goal focusedGoal,
                                              PosInOccurrence pos)

Description copied from interface: ProofControl

collects all applicable FindTaclets of the current goal (called by the SequentViewer)

Specified by:

getFindTaclet in interface ProofControl

Returns:

a list of Taclets with all applicable FindTaclets

getRewriteTaclet

public ImmutableList<TacletApp> getRewriteTaclet(Goal focusedGoal,
                                                 PosInOccurrence pos)

Description copied from interface: ProofControl

collects all applicable RewriteTaclets of the current goal (called by the SequentViewer)

Specified by:

getRewriteTaclet in interface ProofControl

Returns:

a list of Taclets with all applicable RewriteTaclets

filterTaclet

private ImmutableList<TacletApp> filterTaclet(Goal focusedGoal,
                                              ImmutableList<NoPosTacletApp> tacletInstances,
                                              PosInOccurrence pos)

takes NoPosTacletApps as arguments and returns a duplicate free list of the contained TacletApps

selectedTaclet

public boolean selectedTaclet(Taclet taclet,
                              Goal goal,
                              PosInOccurrence pos)

Specified by:

selectedTaclet in interface ProofControl

applyInteractive

public void applyInteractive(RuleApp app,
                             Goal goal)

Description copied from interface: ProofControl

Apply a RuleApp and continue with update simplification or strategy application according to current settings.

Specified by:

applyInteractive in interface ProofControl

pruneTo

public void pruneTo(Node node)

Prunes a proof to the given node.

Parameters:

node -

See Also:

Proof#pruneProof(Node)}

pruneTo

public void pruneTo(Goal goal)

Undo the last rule application on the given goal.

Parameters:

goal - a non-null goal

See Also:

Proof#pruneProof(Goal)}

emitInteractivePrune

protected void emitInteractivePrune(Node node)

emitInteractiveRuleApplication

protected void emitInteractiveRuleApplication(Goal goal,
                                              RuleApp app)

getAppsForName

protected ImmutableSet<TacletApp> getAppsForName(Goal goal,
                                                 java.lang.String name,
                                                 PosInOccurrence pos)

collects all Taclet applications at the given position of the specified taclet

Parameters:

goal - the Goal for which the applications should be returned

name - the String with the taclet names whose applications are looked for

pos - the PosInOccurrence describing the position

Returns:

a list of all found rule applications of the given rule at position pos

getAppsForName

protected ImmutableSet<TacletApp> getAppsForName(Goal goal,
                                                 java.lang.String name,
                                                 PosInOccurrence pos,
                                                 TacletFilter filter)

collects all taclet applications for the given position and taclet (identified by its name) matching the filter condition

Parameters:

goal - the Goal for which the applications should be returned

name - the String with the taclet names whose applications are looked for

pos - the PosInOccurrence describing the position

filter - the TacletFilter expressing restrictions

Returns:

a list of all found rule applications of the given rule at position pos passing the filter

completeAndApplyApp

public TacletInstantiationModel[] completeAndApplyApp(java.util.List<TacletApp> apps,
                                                      Goal goal)

createModel

public TacletInstantiationModel createModel(TacletApp app,
                                            Goal goal)

selectedBuiltInRule

public void selectedBuiltInRule(Goal goal,
                                BuiltInRule rule,
                                PosInOccurrence pos,
                                boolean forced)

Description copied from interface: ProofControl

selected rule to apply

Specified by:

selectedBuiltInRule in interface ProofControl

rule - the selected built-in rule

pos - the PosInSequent describes the position where to apply the rule

forced - a boolean indicating that if the rule is complete or can be made complete automatically then the rule should be applied automatically without asking the user at all (e.g. if a loop invariant is available do not ask the user to provide one)

getBuiltInRuleApp

public ImmutableSet<IBuiltInRuleApp> getBuiltInRuleApp(Goal focusedGoal,
                                                       BuiltInRule rule,
                                                       PosInOccurrence pos)

collects all built-in rule applications for the given rule that are applicable at position 'pos' and the current user constraint

Parameters:

rule - the BuiltInRule for which the applications are collected

pos - the PosInSequent the position information

Returns:

a SetOf with all possible rule applications

getBuiltInRuleAppsForName

protected ImmutableSet<IBuiltInRuleApp> getBuiltInRuleAppsForName(Goal focusedGoal,
                                                                  java.lang.String name,
                                                                  PosInOccurrence pos)

collects all applications of a rule given by its name at a give position in the sequent

Parameters:

name - the name of the BuiltInRule for which applications are collected.

pos - the position in the sequent where the BuiltInRule should be applied

Returns:

a SetOf with all possible applications of the rule

completeAndApplyTacletMatch

protected void completeAndApplyTacletMatch(TacletInstantiationModel[] models,
                                           Goal goal)

completeBuiltInRuleApp

protected IBuiltInRuleApp completeBuiltInRuleApp(IBuiltInRuleApp app,
                                                 Goal goal,
                                                 boolean forced)

completeBuiltInRuleAppByDefault

public static IBuiltInRuleApp completeBuiltInRuleAppByDefault(IBuiltInRuleApp app,
                                                              Goal goal,
                                                              boolean forced)

Default implementation of RuleCompletionHandler.completeBuiltInRuleApp(IBuiltInRuleApp, Goal, boolean).

isAutoModeSupported

public boolean isAutoModeSupported(Proof proof)

Checks if the auto mode of this UserInterfaceControl supports the given Proof.

Specified by:

isAutoModeSupported in interface ProofControl

Parameters:

proof - The Proof to check.

Returns:

true auto mode support proofs, false auto mode don't support proof.

addAutoModeListener

public void addAutoModeListener(AutoModeListener p)

Specified by:

addAutoModeListener in interface ProofControl

removeAutoModeListener

public void removeAutoModeListener(AutoModeListener p)

Specified by:

removeAutoModeListener in interface ProofControl

fireAutoModeStarted

protected void fireAutoModeStarted(ProofEvent e)

fires the event that automatic execution has started

fireAutoModeStopped

protected void fireAutoModeStopped(ProofEvent e)

fires the event that automatic execution has stopped

startAutoMode

public void startAutoMode(Proof proof)

Starts the auto mode for the given Proof.

Specified by:

startAutoMode in interface ProofControl

Parameters:

proof - The Proof to start auto mode of.

startAndWaitForAutoMode

public void startAndWaitForAutoMode(Proof proof)

Starts the auto mode for the given proof which must be contained in this user interface and blocks the current thread until it has finished.

Specified by:

startAndWaitForAutoMode in interface ProofControl

Parameters:

proof - The Proof to start auto mode and to wait for.

startAndWaitForAutoMode

public void startAndWaitForAutoMode(Proof proof,
                                    ImmutableList<Goal> goals)

Starts the auto mode for the given proof which must be contained in this user interface and blocks the current thread until it has finished.

Specified by:

startAndWaitForAutoMode in interface ProofControl

Parameters:

proof - The Proof to start auto mode and to wait for.

goals - The Goals to close.

stopAndWaitAutoMode

public void stopAndWaitAutoMode()

Stops the currently running auto mode and blocks the current Thread until auto mode has stopped.

Specified by:

stopAndWaitAutoMode in interface ProofControl

startAutoMode

public void startAutoMode(Proof proof,
                          ImmutableList<Goal> goals)

Starts the auto mode for the given Proof and the given Goals.

Specified by:

startAutoMode in interface ProofControl

Parameters:

proof - The Proof to start auto mode of.

goals - The Goals to close.

startAutoMode

protected abstract void startAutoMode(Proof proof,
                                      ImmutableList<Goal> goals,
                                      ProverTaskListener ptl)

startFocussedAutoMode

public void startFocussedAutoMode(PosInOccurrence focus,
                                  Goal goal)

starts the execution of rules with active strategy. Restrict the application of rules to a particular goal and (for focus!=null) to a particular subterm or subformula of that goal

Specified by:

startFocussedAutoMode in interface ProofControl

addInteractionListener

public void addInteractionListener(InteractionListener listener)

removeInteractionListener

public void removeInteractionListener(InteractionListener listener)