public interface ProofControl
ProofControl
provides the user interface independent logic to apply rules on a proof.
This includes:
isMinimizeInteraction()
and setMinimizeInteraction(boolean)
).Thread
.Modifier and Type | Method and Description |
---|---|
void |
addAutoModeListener(AutoModeListener p) |
void |
applyInteractive(RuleApp app,
Goal goal)
Apply a RuleApp and continue with update simplification or strategy
application according to current settings.
|
ImmutableList<BuiltInRule> |
getBuiltInRule(Goal focusedGoal,
PosInOccurrence pos)
collects all built-in rules that are applicable at the given sequent
position 'pos'.
|
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 |
isInAutoMode()
Checks if the auto mode is currently running.
|
boolean |
isMinimizeInteraction() |
void |
removeAutoModeListener(AutoModeListener p) |
void |
runMacro(Node node,
ProofMacro macro,
PosInOccurrence posInOcc)
|
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)
|
void |
startFocussedAutoMode(PosInOccurrence focus,
Goal goal) |
void |
stopAndWaitAutoMode()
Stops the currently running auto mode and blocks the current
Thread until auto mode has stopped. |
void |
stopAutoMode()
Requests to stop the current auto mode without blocking the current
Thread until the auto mode has stopped. |
void |
waitWhileAutoMode()
Blocks the current
Thread while the auto mode of this
UserInterfaceControl is active. |
boolean isMinimizeInteraction()
void setMinimizeInteraction(boolean minimizeInteraction)
ImmutableList<TacletApp> getRewriteTaclet(Goal focusedGoal, PosInOccurrence pos)
ImmutableList<TacletApp> getFindTaclet(Goal focusedGoal, PosInOccurrence pos)
ImmutableList<TacletApp> getNoFindTaclet(Goal focusedGoal)
ImmutableList<BuiltInRule> getBuiltInRule(Goal focusedGoal, PosInOccurrence pos)
pos
- the PosInSequent where to look for applicable rulesboolean selectedTaclet(Taclet taclet, Goal goal, PosInOccurrence pos)
void applyInteractive(RuleApp app, Goal goal)
app
- goal
- void selectedBuiltInRule(Goal goal, BuiltInRule rule, PosInOccurrence pos, boolean forced)
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)ProverTaskListener getDefaultProverTaskListener()
ProverTaskListener
which will be added to all started ApplyStrategy
instances.ProverTaskListener
which will be added to all started ApplyStrategy
instances.void addAutoModeListener(AutoModeListener p)
void removeAutoModeListener(AutoModeListener p)
boolean isAutoModeSupported(Proof proof)
UserInterfaceControl
supports the given Proof
.proof
- The Proof
to check.true
auto mode support proofs, false
auto mode don't support proof.boolean isInAutoMode()
true
auto mode is running, false
auto mode is not running.void startAutoMode(Proof proof)
Proof
.proof
- The Proof
to start auto mode of.void startAutoMode(Proof proof, ImmutableList<Goal> goals)
void stopAutoMode()
Thread
until the auto mode has stopped.void stopAndWaitAutoMode()
Thread
until auto mode has stopped.void waitWhileAutoMode()
Thread
while the auto mode of this
UserInterfaceControl
is active.void startAndWaitForAutoMode(Proof proof, ImmutableList<Goal> goals)
void startAndWaitForAutoMode(Proof proof)
proof
- The Proof
to start auto mode and to wait for.void startFocussedAutoMode(PosInOccurrence focus, Goal goal)
void runMacro(Node node, ProofMacro macro, PosInOccurrence posInOcc)
node
- The Node
to start macro at.macro
- The ProofMacro
to execute.posInOcc
- The exact PosInOccurrence
at which the ProofMacro
is started at.