public abstract class AbstractProofControl extends java.lang.Object implements ProofControl
ProofControl
.Modifier and Type | Class and Description |
---|---|
static class |
AbstractProofControl.FocussedAutoModeTaskListener
TODO
|
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 and Description |
---|
AbstractProofControl(ProverTaskListener defaultProverTaskListener)
Constructor.
|
AbstractProofControl(ProverTaskListener defaultProverTaskListener,
RuleCompletionHandler ruleCompletionHandler)
Constructor.
|
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)
|
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. |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
isInAutoMode, runMacro, stopAutoMode, waitWhileAutoMode
private final RuleCompletionHandler ruleCompletionHandler
RuleCompletionHandler
to use.private final ProverTaskListener defaultProverTaskListener
ProverTaskListener
which will be added to all started ApplyStrategy
instances.private final java.util.List<AutoModeListener> autoModeListener
AutoModeListener
.private boolean minimizeInteraction
protected final java.util.List<InteractionListener> interactionListeners
public AbstractProofControl(ProverTaskListener defaultProverTaskListener)
defaultProverTaskListener
- The default ProverTaskListener
which will be added to all started ApplyStrategy
instances.public AbstractProofControl(ProverTaskListener defaultProverTaskListener, RuleCompletionHandler ruleCompletionHandler)
defaultProverTaskListener
- The default ProverTaskListener
which will be added to all started ApplyStrategy
instances.ruleCompletionHandler
- An optional RuleCompletionHandler
.public ProverTaskListener getDefaultProverTaskListener()
ProverTaskListener
which will be added to all started ApplyStrategy
instances.getDefaultProverTaskListener
in interface ProofControl
ProverTaskListener
which will be added to all started ApplyStrategy
instances.public boolean isMinimizeInteraction()
isMinimizeInteraction
in interface ProofControl
public void setMinimizeInteraction(boolean minimizeInteraction)
setMinimizeInteraction
in interface ProofControl
public ImmutableList<BuiltInRule> getBuiltInRule(Goal focusedGoal, PosInOccurrence pos)
ProofControl
getBuiltInRule
in interface ProofControl
pos
- the PosInSequent where to look for applicable rulespublic ImmutableList<TacletApp> getNoFindTaclet(Goal focusedGoal)
ProofControl
getNoFindTaclet
in interface ProofControl
public ImmutableList<TacletApp> getFindTaclet(Goal focusedGoal, PosInOccurrence pos)
ProofControl
getFindTaclet
in interface ProofControl
public ImmutableList<TacletApp> getRewriteTaclet(Goal focusedGoal, PosInOccurrence pos)
ProofControl
getRewriteTaclet
in interface ProofControl
private ImmutableList<TacletApp> filterTaclet(Goal focusedGoal, ImmutableList<NoPosTacletApp> tacletInstances, PosInOccurrence pos)
public boolean selectedTaclet(Taclet taclet, Goal goal, PosInOccurrence pos)
selectedTaclet
in interface ProofControl
public void applyInteractive(RuleApp app, Goal goal)
ProofControl
applyInteractive
in interface ProofControl
public void pruneTo(Node node)
node
- Proof#pruneProof(Node)}
public void pruneTo(Goal goal)
goal
- a non-null goalProof#pruneProof(Goal)}
protected void emitInteractivePrune(Node node)
protected void emitInteractiveRuleApplication(Goal goal, RuleApp app)
protected ImmutableSet<TacletApp> getAppsForName(Goal goal, java.lang.String name, PosInOccurrence pos)
goal
- the Goal for which the applications should be returnedname
- the String with the taclet names whose applications are
looked forpos
- the PosInOccurrence describing the positionprotected ImmutableSet<TacletApp> getAppsForName(Goal goal, java.lang.String name, PosInOccurrence pos, TacletFilter filter)
goal
- the Goal for which the applications should be returnedname
- the String with the taclet names whose applications are
looked forpos
- the PosInOccurrence describing the positionfilter
- the TacletFilter expressing restrictionspublic TacletInstantiationModel[] completeAndApplyApp(java.util.List<TacletApp> apps, Goal goal)
public TacletInstantiationModel createModel(TacletApp app, Goal goal)
public void selectedBuiltInRule(Goal goal, BuiltInRule rule, PosInOccurrence pos, boolean forced)
ProofControl
selectedBuiltInRule
in interface ProofControl
rule
- the selected built-in rulepos
- the PosInSequent describes the position where to apply the
ruleforced
- 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)public ImmutableSet<IBuiltInRuleApp> getBuiltInRuleApp(Goal focusedGoal, BuiltInRule rule, PosInOccurrence pos)
rule
- the BuiltInRule for which the applications are collectedpos
- the PosInSequent the position informationprotected ImmutableSet<IBuiltInRuleApp> getBuiltInRuleAppsForName(Goal focusedGoal, java.lang.String name, PosInOccurrence pos)
name
- the name of the BuiltInRule for which applications are
collected.pos
- the position in the sequent where the BuiltInRule should be
appliedprotected void completeAndApplyTacletMatch(TacletInstantiationModel[] models, Goal goal)
protected IBuiltInRuleApp completeBuiltInRuleApp(IBuiltInRuleApp app, Goal goal, boolean forced)
public static IBuiltInRuleApp completeBuiltInRuleAppByDefault(IBuiltInRuleApp app, Goal goal, boolean forced)
RuleCompletionHandler.completeBuiltInRuleApp(IBuiltInRuleApp, Goal, boolean)
.public boolean isAutoModeSupported(Proof proof)
UserInterfaceControl
supports the given Proof
.isAutoModeSupported
in interface ProofControl
proof
- The Proof
to check.true
auto mode support proofs, false
auto mode don't support proof.public void addAutoModeListener(AutoModeListener p)
addAutoModeListener
in interface ProofControl
public void removeAutoModeListener(AutoModeListener p)
removeAutoModeListener
in interface ProofControl
protected void fireAutoModeStarted(ProofEvent e)
protected void fireAutoModeStopped(ProofEvent e)
public void startAutoMode(Proof proof)
Proof
.startAutoMode
in interface ProofControl
proof
- The Proof
to start auto mode of.public void startAndWaitForAutoMode(Proof proof)
startAndWaitForAutoMode
in interface ProofControl
proof
- The Proof
to start auto mode and to wait for.public void startAndWaitForAutoMode(Proof proof, ImmutableList<Goal> goals)
startAndWaitForAutoMode
in interface ProofControl
proof
- The Proof
to start auto mode and to wait for.goals
- The Goal
s to close.public void stopAndWaitAutoMode()
Thread
until auto mode has stopped.stopAndWaitAutoMode
in interface ProofControl
public void startAutoMode(Proof proof, ImmutableList<Goal> goals)
startAutoMode
in interface ProofControl
proof
- The Proof
to start auto mode of.goals
- The Goal
s to close.protected abstract void startAutoMode(Proof proof, ImmutableList<Goal> goals, ProverTaskListener ptl)
public void startFocussedAutoMode(PosInOccurrence focus, Goal goal)
focus!=null
) to a particular subterm or subformula of that
goalstartFocussedAutoMode
in interface ProofControl
public void addInteractionListener(InteractionListener listener)
public void removeInteractionListener(InteractionListener listener)