Skip to content

Commit a8c4314

Browse files
wadoonwadoon
committed
wip
1 parent 41f9a03 commit a8c4314

17 files changed

+90
-97
lines changed

‎key.core/src/main/java/de/uka/ilkd/key/scripts/AbstractCommand.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,7 @@ public List<ProofScriptArgument> getArguments() {
6161

6262

6363
@Override
64-
public void execute(AbstractUserInterfaceControl uiControl, ScriptCommandAst args,
64+
public final void execute(AbstractUserInterfaceControl uiControl, ScriptCommandAst args,
6565
EngineState stateMap)
6666
throws ScriptException, InterruptedException {
6767
proof = stateMap.getProof();

‎key.core/src/main/java/de/uka/ilkd/key/scripts/CutCommand.java‎

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -41,11 +41,9 @@ public String getDocumentation() {
4141
}
4242

4343
@Override
44-
public void execute(AbstractUserInterfaceControl uiControl, ScriptCommandAst arguments,
45-
EngineState state)
46-
throws ScriptException, InterruptedException {
47-
var args = state.getValueInjector().inject(new Parameters(), arguments);
48-
execute(state, args);
44+
public void execute(ScriptCommandAst arguments) throws ScriptException, InterruptedException {
45+
var args = state().getValueInjector().inject(new Parameters(), arguments);
46+
execute(state(), args);
4947
}
5048

5149
static void execute(EngineState state, Parameters args) throws ScriptException {

‎key.core/src/main/java/de/uka/ilkd/key/scripts/EchoCommand.java‎

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -23,12 +23,11 @@ public String getName() {
2323
}
2424

2525
@Override
26-
public void execute(AbstractUserInterfaceControl uiControl, ScriptCommandAst args,
27-
EngineState state)
26+
public void execute(ScriptCommandAst args)
2827
throws ScriptException, InterruptedException {
29-
var params = state.getValueInjector().inject(new Parameters(), args);
28+
var params = state().getValueInjector().inject(new Parameters(), args);
3029

31-
var obs = state.getObserver();
30+
var obs = state().getObserver();
3231
if (obs != null) {
3332
obs.accept(new ProofScriptEngine.EchoMessage(params.message));
3433
}

‎key.core/src/main/java/de/uka/ilkd/key/scripts/EngineState.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -302,7 +302,7 @@ public void setMaxAutomaticSteps(int steps) {
302302
ProofSettings.DEFAULT_SETTINGS.getStrategySettings().setMaxSteps(steps);
303303
}
304304

305-
public Consumer<ProofScriptEngine.Message> getObserver() {
305+
public @Nullable Consumer<ProofScriptEngine.Message> getObserver() {
306306
return observer;
307307
}
308308

‎key.core/src/main/java/de/uka/ilkd/key/scripts/InstantiateCommand.java‎

Lines changed: 14 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,8 @@
3131

3232
import org.jspecify.annotations.Nullable;
3333

34+
import java.util.Objects;
35+
3436
import static de.uka.ilkd.key.logic.equality.RenamingTermProperty.RENAMING_TERM_PROPERTY;
3537

3638
/**
@@ -47,11 +49,10 @@ public InstantiateCommand() {
4749
}
4850

4951
@Override
50-
public void execute(AbstractUserInterfaceControl uiControl, ScriptCommandAst args,
51-
EngineState stateMap) throws ScriptException, InterruptedException {
52-
var params = state.getValueInjector().inject(new Parameters(), args);
52+
public void execute(ScriptCommandAst args) throws ScriptException, InterruptedException {
53+
var params = state().getValueInjector().inject(new Parameters(), args);
5354

54-
Goal goal = state.getFirstOpenAutomaticGoal();
55+
Goal goal = state().getFirstOpenAutomaticGoal();
5556

5657
if ((params.var == null) == (params.formula == null)) {
5758
throw new ScriptException("One of 'var' or 'formula' must be specified");
@@ -79,7 +80,7 @@ public void execute(AbstractUserInterfaceControl uiControl, ScriptCommandAst arg
7980
g.apply(theApp);
8081
}
8182

82-
private TacletApp findTacletApp(Parameters p, EngineState state) throws ScriptException {
83+
private @Nullable TacletApp findTacletApp(Parameters p, EngineState state) throws ScriptException {
8384
ImmutableList<TacletApp> allApps = findAllTacletApps(p, state);
8485
TacletApp matchingApp = filterList(p, allApps);
8586

@@ -134,7 +135,7 @@ private ImmutableList<TacletApp> findAllTacletApps(Parameters p, EngineState sta
134135
/*
135136
* Filter those apps from a list that are according to the parameters.
136137
*/
137-
private TacletApp filterList(Parameters p, ImmutableList<TacletApp> list) {
138+
private @Nullable TacletApp filterList(Parameters p, ImmutableList<TacletApp> list) {
138139
for (TacletApp tacletApp : list) {
139140
if (tacletApp instanceof PosTacletApp pta) {
140141
JTerm term = (JTerm) pta.posInOccurrence().subTerm();
@@ -155,7 +156,7 @@ private void computeFormula(Parameters params, Goal goal) throws ScriptException
155156
var stripped = stripUpdates(term);
156157
if (stripped.op() == Quantifier.ALL) {
157158
String varName = stripped.boundVars().get(0).name().toString();
158-
if (params.var.equals(varName)) {
159+
if (Objects.equals(params.var, varName)) {
159160
occ--;
160161
if (occ == 0) {
161162
params.formula = (JTerm) term;
@@ -170,7 +171,7 @@ private void computeFormula(Parameters params, Goal goal) throws ScriptException
170171
var stripped = stripUpdates(term);
171172
if (stripped.op() == Quantifier.EX) {
172173
String varName = stripped.boundVars().get(0).name().toString();
173-
if (params.var.equals(varName)) {
174+
if (Objects.equals(params.var, varName)) {
174175
occ--;
175176
if (occ == 0) {
176177
params.formula = (JTerm) term;
@@ -181,7 +182,7 @@ private void computeFormula(Parameters params, Goal goal) throws ScriptException
181182
}
182183

183184
throw new ScriptException(
184-
"Variable '" + params.var + "' has no occurrence no. '" + params.occ + "'.");
185+
"Variable '%s' has no occurrence no. '%d'.".formatted(params.var, params.occ));
185186
}
186187

187188
private Term stripUpdates(Term term) {
@@ -232,10 +233,12 @@ public String getDocumentation() {
232233
*
233234
*/
234235
public static class Parameters {
235-
@Option(value = "formula")
236+
@Option(value = "formula") @Nullable
236237
public JTerm formula;
237-
@Option(value = "var")
238+
239+
@Option(value = "var") @Nullable
238240
public String var;
241+
239242
@Option(value = "occ")
240243
public @Nullable int occ = 1;
241244

‎key.core/src/main/java/de/uka/ilkd/key/scripts/MacroCommand.java‎

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -54,12 +54,11 @@ public String getName() {
5454
}
5555

5656
@Override
57-
public void execute(AbstractUserInterfaceControl uiControl, ScriptCommandAst arguments,
58-
EngineState state)
57+
public void execute(ScriptCommandAst arguments)
5958
throws ScriptException, InterruptedException {
60-
var args = state.getValueInjector().inject(new Parameters(), arguments);
59+
var args = state().getValueInjector().inject(new Parameters(), arguments);
6160

62-
final Services services = state.getProof().getServices();
61+
final Services services = state().getProof().getServices();
6362
// look up macro name
6463
ProofMacro macro = macroMap.get(args.macroName);
6564
if (macro == null) {

‎key.core/src/main/java/de/uka/ilkd/key/scripts/ProofScriptEngine.java‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -177,6 +177,8 @@ public void execute(AbstractUserInterfaceControl uiControl, List<ScriptCommandAs
177177
LOGGER.debug("GOALS: {}", proof.getSubtreeGoals(proof.root()).size());
178178
proof.getSubtreeGoals(stateMap.getProof().root())
179179
.forEach(g -> LOGGER.debug("{}", g.sequent()));
180+
181+
180182
throw new ScriptException(
181183
String.format("Error while executing script: %s%n%nCommand: %s%nPosition: %s%n",
182184
e.getMessage(), ast.asCommandLine(), ast.location()),

‎key.core/src/main/java/de/uka/ilkd/key/scripts/RewriteCommand.java‎

Lines changed: 7 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -76,26 +76,25 @@ public String getName() {
7676
}
7777

7878
@Override
79-
public void execute(AbstractUserInterfaceControl uiControl, ScriptCommandAst arguments,
80-
EngineState state)
79+
public void execute(ScriptCommandAst arguments)
8180
throws ScriptException, InterruptedException {
82-
var args = state.getValueInjector().inject(new Parameters(), arguments);
81+
var args = state().getValueInjector().inject(new Parameters(), arguments);
8382

84-
Proof proof = state.getProof();
83+
Proof proof = state().getProof();
8584
assert proof != null;
8685

87-
ImmutableList<TacletApp> allApps = findAllTacletApps(args, state);
86+
ImmutableList<TacletApp> allApps = findAllTacletApps(args, state());
8887

8988
// filter all taclets for being applicable on the find term
9089
List<PosInOccurrence> failposInOccs =
91-
findAndExecReplacement(args, allApps, state);
90+
findAndExecReplacement(args, allApps, state());
9291

9392
// if not all find terms successfully replaced, apply cut
9493
if (!failposInOccs.isEmpty()) {
9594

9695
CutCommand.Parameters param = new CutCommand.Parameters();
9796
param.formula = args.replace;
98-
CutCommand.execute(state, param);
97+
CutCommand.execute(state(), param);
9998
}
10099

101100
}
@@ -152,7 +151,7 @@ private List<PosInOccurrence> findAndExecReplacement(Parameters p,
152151
// Find taclet that transforms find term to replace term, when applied on find term
153152
for (TacletApp tacletApp : list) {
154153
if (tacletApp instanceof PosTacletApp pta) {
155-
if (pta.taclet() instanceof RewriteTaclet) {
154+
if (pta.taclet() instanceof RewriteTaclet rw) {
156155
if (pta.taclet().displayName().equals("cut_direct")) {
157156
continue;
158157
}
@@ -164,8 +163,6 @@ private List<PosInOccurrence> findAndExecReplacement(Parameters p,
164163

165164
try { // Term not already successfully replaced
166165
Goal goalold = state.getFirstOpenAutomaticGoal();
167-
168-
RewriteTaclet rw = (RewriteTaclet) pta.taclet();
169166
if (pta.complete()) {
170167
SequentFormula rewriteResult =
171168
((RewriteTacletExecutor) rw.getExecutor()).getRewriteResult(

‎key.core/src/main/java/de/uka/ilkd/key/scripts/RuleCommand.java‎

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -77,13 +77,12 @@ public String getDocumentation() {
7777
}
7878

7979
@Override
80-
public void execute(AbstractUserInterfaceControl uiControl, ScriptCommandAst params,
81-
EngineState state)
80+
public void execute( ScriptCommandAst params)
8281
throws ScriptException, InterruptedException {
83-
var args = state.getValueInjector().inject(new Parameters(), params);
82+
var args = state().getValueInjector().inject(new Parameters(), params);
8483

85-
RuleApp theApp = makeRuleApp(args, state);
86-
Goal g = state.getFirstOpenAutomaticGoal();
84+
RuleApp theApp = makeRuleApp(args, state());
85+
Goal g = state().getFirstOpenAutomaticGoal();
8786

8887
if (theApp instanceof TacletApp tacletApp) {
8988

‎key.core/src/main/java/de/uka/ilkd/key/scripts/SaveInstCommand.java‎

Lines changed: 5 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -3,18 +3,16 @@
33
* SPDX-License-Identifier: GPL-2.0-only */
44
package de.uka.ilkd.key.scripts;
55

6-
import java.util.Map;
7-
8-
import de.uka.ilkd.key.control.AbstractUserInterfaceControl;
96
import de.uka.ilkd.key.logic.JTerm;
107
import de.uka.ilkd.key.pp.AbbrevMap;
118
import de.uka.ilkd.key.rule.TacletApp;
12-
139
import org.key_project.logic.Name;
1410
import org.key_project.logic.op.Function;
1511
import org.key_project.logic.op.sv.SchemaVariable;
1612
import org.key_project.prover.rules.RuleApp;
1713

14+
import java.util.Map;
15+
1816
/**
1917
* Special "Let" usually to be applied immediately after a manual rule application. Saves the
2018
* instantiation of a {@link SchemaVariable} by the last {@link TacletApp} into an abbreviation for
@@ -31,10 +29,9 @@ public SaveInstCommand() {
3129
}
3230

3331
@Override
34-
public void execute(AbstractUserInterfaceControl uiControl, ScriptCommandAst args,
35-
EngineState stateMap) throws ScriptException, InterruptedException {
32+
public void execute(ScriptCommandAst args) throws ScriptException, InterruptedException {
3633

37-
AbbrevMap abbrMap = stateMap.getAbbreviations();
34+
AbbrevMap abbrMap = state().getAbbreviations();
3835
for (Map.Entry<String, Object> entry : args.namedArgs().entrySet()) {
3936
String key = entry.getKey();
4037
final var value = entry.getValue();
@@ -56,7 +53,7 @@ public void execute(AbstractUserInterfaceControl uiControl, ScriptCommandAst arg
5653
}
5754

5855
try {
59-
var parentNode = stateMap.getFirstOpenAutomaticGoal().node().parent();
56+
var parentNode = state().getFirstOpenAutomaticGoal().node().parent();
6057
if (parentNode != null) {
6158
final RuleApp ruleApp = parentNode.getAppliedRuleApp();
6259
if (ruleApp instanceof TacletApp tacletApp) {

0 commit comments

Comments
 (0)