Skip to content

Commit 0ca3f3f

Browse files
wadoonwadoon
committed
Introduce ScriptCommandAst to keep the ProofEngine separated from ANTLR's parse tree
1 parent 76cfef2 commit 0ca3f3f

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

48 files changed

+423
-514
lines changed

‎key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java‎

Lines changed: 42 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -6,14 +6,18 @@
66
import java.net.URI;
77
import java.net.URISyntaxException;
88
import java.net.URL;
9+
import java.util.ArrayList;
10+
import java.util.HashMap;
911
import java.util.List;
1012

13+
import de.uka.ilkd.key.java.Position;
1114
import de.uka.ilkd.key.nparser.builder.BuilderHelpers;
1215
import de.uka.ilkd.key.nparser.builder.ChoiceFinder;
1316
import de.uka.ilkd.key.nparser.builder.FindProblemInformation;
1417
import de.uka.ilkd.key.nparser.builder.IncludeFinder;
1518
import de.uka.ilkd.key.parser.Location;
1619
import de.uka.ilkd.key.proof.init.Includes;
20+
import de.uka.ilkd.key.scripts.ScriptCommandAst;
1721
import de.uka.ilkd.key.settings.Configuration;
1822
import de.uka.ilkd.key.settings.ProofSettings;
1923
import de.uka.ilkd.key.speclang.njml.JmlParser;
@@ -48,7 +52,7 @@ protected KeyAst(@NonNull T ctx) {
4852
this.ctx = ctx;
4953
}
5054

51-
public <T> T accept(ParseTreeVisitor<T> visitor) {
55+
public <R> R accept(ParseTreeVisitor<R> visitor) {
5256
return ctx.accept(visitor);
5357
}
5458

@@ -100,7 +104,6 @@ public ProofSettings findProofSettings() {
100104
if (ctx.problem() != null && ctx.problem().proofScriptEntry() != null) {
101105
KeYParser.ProofScriptEntryContext pctx = ctx.problem().proofScriptEntry();
102106

103-
KeYParser.ProofScriptContext ps;
104107
if (pctx.STRING_LITERAL() != null) {
105108
var ctx = pctx.STRING_LITERAL().getSymbol();
106109
String text = pctx.STRING_LITERAL().getText();
@@ -177,7 +180,7 @@ public Configuration asConfiguration() {
177180
final var cfg = new ConfigurationBuilder();
178181
List<Object> res = cfg.visitCfile(ctx);
179182
if (!res.isEmpty())
180-
return (Configuration) res.get(0);
183+
return (Configuration) res.getFirst();
181184
else
182185
throw new RuntimeException("Error in configuration. Source: "
183186
+ ctx.start.getTokenSource().getSourceName());
@@ -234,7 +237,7 @@ public static class ProofScript extends KeyAst<KeYParser.ProofScriptContext> {
234237
super(ctx);
235238
}
236239

237-
public URI getUrl() {
240+
public URI getUri() {
238241
final var sourceName = ctx.start.getTokenSource().getSourceName();
239242
try {
240243
if (sourceName.startsWith("file:") || sourceName.startsWith("http:")
@@ -244,5 +247,40 @@ public URI getUrl() {
244247
}
245248
return new java.io.File(sourceName).toURI();
246249
}
250+
251+
/**
252+
* Translates this parse tree into an AST usable for the proof script engine.
253+
*
254+
* @return a non-null list of the parsed commands.
255+
*/
256+
public List<ScriptCommandAst> asAst() {
257+
var fileUri = getUri();
258+
return asAst(fileUri, ctx.proofScriptCommand());
259+
}
260+
261+
private List<ScriptCommandAst> asAst(URI file,
262+
List<KeYParser.ProofScriptCommandContext> cmds) {
263+
return cmds.stream().map(it -> {
264+
var loc = new Location(file, Position.fromToken(it.start));
265+
var sub = it.sub != null
266+
? asAst(file, it.sub.proofScriptCommand())
267+
: null;
268+
269+
var nargs = new HashMap<String, Object>();
270+
var pargs = new ArrayList<>();
271+
272+
if (it.proofScriptParameters() != null) {
273+
for (var param : it.proofScriptParameters().proofScriptParameter()) {
274+
if (param.pname != null) {
275+
nargs.put(param.pname.getText(), param.expr);
276+
} else {
277+
pargs.add(param.expr);
278+
}
279+
}
280+
}
281+
282+
return new ScriptCommandAst(it.cmd.getText(), nargs, pargs, sub, loc);
283+
}).toList();
284+
}
247285
}
248286
}

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

Lines changed: 15 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55

66
import java.util.ArrayList;
77
import java.util.List;
8-
import java.util.Map;
8+
import java.util.Objects;
99

1010
import de.uka.ilkd.key.control.AbstractUserInterfaceControl;
1111
import de.uka.ilkd.key.java.Services;
@@ -26,10 +26,9 @@
2626
/// {@link AbstractCommand}. You need to override [AbstractCommand#execute(Object)] to implement the
2727
/// command logic.
2828
///
29-
/// @param <T> the expected parameter class
3029
/// @author Alexander Weigl
3130
@NullMarked
32-
public abstract class AbstractCommand<T> implements ProofScriptCommand<T> {
31+
public abstract class AbstractCommand implements ProofScriptCommand {
3332
protected @Nullable Proof proof;
3433
protected @Nullable Services service;
3534
protected @Nullable EngineState state;
@@ -40,34 +39,39 @@ public abstract class AbstractCommand<T> implements ProofScriptCommand<T> {
4039
*/
4140
protected @Nullable String documentation = null;
4241

42+
protected final EngineState state() {
43+
return Objects.requireNonNull(state);
44+
}
45+
4346
/**
4447
* ...
4548
*/
46-
private final Class<T> parameterClazz;
49+
private final @Nullable Class<?> parameterClazz;
4750

48-
protected AbstractCommand(Class<T> clazz) {
51+
protected AbstractCommand(@Nullable Class<?> clazz) {
4952
this.parameterClazz = clazz;
5053
}
5154

52-
public List<ProofScriptArgument<T>> getArguments() {
55+
public List<ProofScriptArgument> getArguments() {
5356
if (parameterClazz == null) {
5457
return new ArrayList<>();
5558
}
5659
return ArgumentsLifter.inferScriptArguments(parameterClazz, this);
5760
}
5861

5962

60-
@Override
61-
public T evaluateArguments(EngineState state, Map<String, Object> arguments) throws Exception {
63+
public @Nullable Object evaluateArguments(EngineState state, ScriptCommandAst arguments)
64+
throws Exception {
6265
if (parameterClazz != null) {
63-
T obj = parameterClazz.getDeclaredConstructor().newInstance();
66+
Object obj = parameterClazz.getDeclaredConstructor().newInstance();
6467
return state.getValueInjector().inject(this, obj, arguments);
6568
}
6669
return null;
6770
}
6871

6972
@Override
70-
public void execute(AbstractUserInterfaceControl uiControl, T args, EngineState stateMap)
73+
public void execute(AbstractUserInterfaceControl uiControl, ScriptCommandAst args,
74+
EngineState stateMap)
7175
throws ScriptException, InterruptedException {
7276
proof = stateMap.getProof();
7377
service = proof.getServices();
@@ -89,7 +93,7 @@ public void execute(AbstractUserInterfaceControl uiControl, T args, EngineState
8993
/// @param args an instance of the parameters
9094
/// @throws ScriptException if something happened during execution
9195
/// @throws InterruptedException if thread was interrupted during execution
92-
protected void execute(T args) throws ScriptException, InterruptedException {
96+
public void execute(ScriptCommandAst args) throws ScriptException, InterruptedException {
9397
}
9498

9599
@Override

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,8 @@ public String getDocumentation() {
2525
}
2626

2727
@Override
28-
public void execute(AbstractUserInterfaceControl uiControl, Void args, EngineState state)
28+
public void execute(AbstractUserInterfaceControl uiControl, ScriptCommandAst args,
29+
EngineState state)
2930
throws ScriptException, InterruptedException {
3031
Goal goal = state.getFirstOpenGoal(false);
3132
goal.setEnabled(true);

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

Lines changed: 5 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -4,30 +4,23 @@
44
package de.uka.ilkd.key.scripts;
55

66
import java.util.List;
7-
import java.util.Map;
87

98
import de.uka.ilkd.key.control.AbstractUserInterfaceControl;
10-
import de.uka.ilkd.key.nparser.KeYParser;
119
import de.uka.ilkd.key.proof.Goal;
1210
import de.uka.ilkd.key.scripts.meta.ProofScriptArgument;
1311

14-
public class AllCommand implements ProofScriptCommand<Map<String, Object>> {
12+
public class AllCommand implements ProofScriptCommand {
1513
private String documentation;
1614

1715
@Override
18-
public List<ProofScriptArgument<Map<String, Object>>> getArguments() {
16+
public List<ProofScriptArgument> getArguments() {
1917
return List.of();
2018
}
2119

2220
@Override
23-
public Map<String, Object> evaluateArguments(EngineState state, Map<String, Object> arguments) {
24-
return arguments;
25-
}
26-
27-
@Override
28-
public void execute(AbstractUserInterfaceControl uiControl, Map<String, Object> args,
21+
public void execute(AbstractUserInterfaceControl uiControl, ScriptCommandAst args,
2922
EngineState stateMap) throws ScriptException, InterruptedException {
30-
var block = (KeYParser.ProofScriptContext) args.get(ProofScriptEngine.KEY_SUB_SCRIPT);
23+
var block = args.commands();
3124

3225
if (block == null) {
3326
throw new ScriptException("Missing command to apply onAll to");
@@ -38,7 +31,7 @@ public void execute(AbstractUserInterfaceControl uiControl, Map<String, Object>
3831
for (Goal g : proof.openGoals()) {
3932
// if (isBelow(g, selectedNode)) {
4033
stateMap.setGoal(g);
41-
stateMap.getEngine().execute(uiControl, block.proofScriptCommand());
34+
stateMap.getEngine().execute(uiControl, block);
4235
// }
4336
}
4437
// state.setGoal(selectedNode);

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

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

6-
import java.util.Map;
76

87
import de.uka.ilkd.key.scripts.meta.Option;
98

@@ -12,7 +11,7 @@
1211
*
1312
* @author lanzinger
1413
*/
15-
public class AssertCommand extends AbstractCommand<AssertCommand.Parameters> {
14+
public class AssertCommand extends AbstractCommand {
1615

1716
/**
1817
* Instantiates a new assert command.
@@ -22,19 +21,14 @@ public AssertCommand() {
2221
}
2322

2423
@Override
25-
public Parameters evaluateArguments(EngineState state,
26-
Map<String, Object> arguments) throws Exception {
27-
return state.getValueInjector().inject(this, new Parameters(),
28-
arguments);
29-
}
24+
public void execute(ScriptCommandAst arguments) throws ScriptException, InterruptedException {
25+
var args = state().getValueInjector().inject(this, new Parameters(), arguments);
3026

31-
@Override
32-
public void execute(Parameters args) throws ScriptException, InterruptedException {
3327
if (args.goals == null) {
3428
throw new ScriptException("No parameter specified!");
3529
}
3630

37-
if (state.getProof().openEnabledGoals().size() != args.goals) {
31+
if (state().getProof().openEnabledGoals().size() != args.goals) {
3832
throw new ScriptException("Assertion failed: number of open goals is "
3933
+ state.getProof().openGoals().size() + ", but should be " + args.goals);
4034
}

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

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

6-
import java.util.Map;
76

87
import de.uka.ilkd.key.logic.Term;
98
import de.uka.ilkd.key.rule.NoPosTacletApp;
@@ -17,19 +16,13 @@
1716
/**
1817
* The assume command takes one argument: * a formula to which the command is applied
1918
*/
20-
public class AssumeCommand extends AbstractCommand<AssumeCommand.FormulaParameter> {
19+
public class AssumeCommand extends AbstractCommand {
2120
private static final Name TACLET_NAME = new Name("UNSOUND_ASSUME");
2221

2322
public AssumeCommand() {
2423
super(FormulaParameter.class);
2524
}
2625

27-
@Override
28-
public FormulaParameter evaluateArguments(EngineState state, Map<String, Object> arguments)
29-
throws Exception {
30-
return state.getValueInjector().inject(this, new FormulaParameter(), arguments);
31-
}
32-
3326
@Override
3427
public String getName() {
3528
return "assume";
@@ -45,15 +38,18 @@ public String getDocumentation() {
4538
}
4639

4740
@Override
48-
public void execute(FormulaParameter parameter) throws ScriptException, InterruptedException {
41+
public void execute(ScriptCommandAst arguments) throws ScriptException, InterruptedException {
42+
var parameter = state().getValueInjector()
43+
.inject(this, new FormulaParameter(), arguments);
4944
Taclet cut =
50-
state.getProof().getEnv().getInitConfigForEnvironment().lookupActiveTaclet(TACLET_NAME);
45+
state().getProof().getEnv().getInitConfigForEnvironment()
46+
.lookupActiveTaclet(TACLET_NAME);
5147
TacletApp app = NoPosTacletApp.createNoPosTacletApp(cut);
5248
SchemaVariable sv = app.uninstantiatedVars().iterator().next();
5349

54-
app = app.addCheckedInstantiation(sv, parameter.formula, state.getProof().getServices(),
50+
app = app.addCheckedInstantiation(sv, parameter.formula, state().getProof().getServices(),
5551
true);
56-
state.getFirstOpenAutomaticGoal().apply(app);
52+
state().getFirstOpenAutomaticGoal().apply(app);
5753
}
5854

5955
public static class FormulaParameter {

0 commit comments

Comments
 (0)