Skip to content

Commit b1e6df1

Browse files
wadoonwadoon
committed
update to main
1 parent 250eb47 commit b1e6df1

File tree

7 files changed

+69
-44
lines changed

7 files changed

+69
-44
lines changed

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

Lines changed: 9 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -283,15 +283,18 @@ private static List<ScriptCommandAst> asAst(URI file,
283283
return cmds.stream().map(it -> asAst(file, it)).toList();
284284
}
285285

286-
public static @NonNull ScriptBlock asAst(URI file, KeYParser.ProofScriptCodeBlockContext ctx) {
286+
public static @NonNull ScriptBlock asAst(URI file,
287+
KeYParser.ProofScriptCodeBlockContext ctx) {
287288
var loc = new Location(file, Position.fromToken(ctx.start));
288289
return new ScriptBlock(
289-
ctx.proofScript().proofScriptCommand().stream()
290-
.map(it -> asAst(file, it))
291-
.toList(), loc);
290+
ctx.proofScript().proofScriptCommand().stream()
291+
.map(it -> asAst(file, it))
292+
.toList(),
293+
loc);
292294
}
293295

294-
private static @NonNull ScriptCommandAst asAst(URI file, KeYParser.ProofScriptCommandContext it) {
296+
private static @NonNull ScriptCommandAst asAst(URI file,
297+
KeYParser.ProofScriptCommandContext it) {
295298
var loc = new Location(file, Position.fromToken(it.start));
296299
var nargs = new HashMap<String, Object>();
297300
var pargs = new ArrayList<>();
@@ -300,7 +303,7 @@ private static List<ScriptCommandAst> asAst(URI file,
300303
for (var param : it.proofScriptParameters().proofScriptParameter()) {
301304
var expr = param.expr;
302305
Object value = expr;
303-
if(expr.proofScriptCodeBlock() != null) {
306+
if (expr.proofScriptCodeBlock() != null) {
304307
value = asAst(file, expr.proofScriptCodeBlock());
305308
}
306309

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

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

6+
import java.util.List;
7+
68
import de.uka.ilkd.key.control.AbstractUserInterfaceControl;
79
import de.uka.ilkd.key.proof.Goal;
810
import de.uka.ilkd.key.scripts.meta.ProofScriptArgument;
911

10-
import java.util.List;
11-
1212
public class AllCommand implements ProofScriptCommand {
1313
@Override
1414
public List<ProofScriptArgument> getArguments() {
@@ -17,15 +17,16 @@ public List<ProofScriptArgument> getArguments() {
1717

1818
@Override
1919
public void execute(AbstractUserInterfaceControl uiControl, ScriptCommandAst args,
20-
EngineState stateMap) throws ScriptException, InterruptedException {
20+
EngineState stateMap) throws ScriptException, InterruptedException {
2121
if (args.positionalArgs().size() != 1) {
22-
throw new ScriptException("Invalid number of positional arguments to 'onAll'. Pos. arguments: "
22+
throw new ScriptException(
23+
"Invalid number of positional arguments to 'onAll'. Pos. arguments: "
2324
+ args.positionalArgs().size());
2425
}
2526

2627
var block = stateMap.getValueInjector().convert(
27-
args.positionalArgs().getFirst(),
28-
ScriptBlock.class);
28+
args.positionalArgs().getFirst(),
29+
ScriptBlock.class);
2930

3031
var proof = stateMap.getProof();
3132
for (Goal g : proof.openGoals()) {

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

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

6+
import java.net.URI;
7+
68
import de.uka.ilkd.key.nparser.KeYParser;
79
import de.uka.ilkd.key.nparser.KeYParser.*;
810
import de.uka.ilkd.key.nparser.KeYParserBaseVisitor;
@@ -15,8 +17,6 @@
1517
import org.slf4j.Logger;
1618
import org.slf4j.LoggerFactory;
1719

18-
import java.net.URI;
19-
2020
import static org.key_project.util.java.StringUtil.trim;
2121

2222
/// Evaluates expression inside of proof script to their appropriate type.

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

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

6+
import java.util.List;
7+
68
import de.uka.ilkd.key.parser.Location;
9+
710
import org.jspecify.annotations.NullMarked;
811
import org.jspecify.annotations.Nullable;
912

10-
import java.util.List;
11-
1213
import static java.util.stream.Collectors.joining;
1314

14-
/// This class represents is the AST of a proof script command.
15+
/// This class represents a block `{ c1; c2; ... ck; }` of proof scripts.
1516
@NullMarked
1617
public record ScriptBlock(
1718
List<ScriptCommandAst> commands,
1819
@Nullable Location location) {
1920

21+
/// Renders this command a parsable string representation. The order of the arguments is as
22+
/// follows:
23+
/// key-value arguments, positional arguments and the additional script block.
24+
///
25+
/// @see de.uka.ilkd.key.nparser.ParsingFacade#parseScript(org.antlr.v4.runtime.CharStream)
2026
public String asCommandLine() {
21-
return " {"
22-
+ commands.stream().map(ScriptCommandAst::asCommandLine).collect(joining("\n"))
23-
+ "\n}";
27+
if (commands.isEmpty()) {
28+
return " {}";
29+
}
30+
if (commands.size() == 1) {
31+
return " {" + commands.getFirst().asCommandLine() + "}";
32+
}
33+
34+
return " {\n"
35+
+ commands.stream().map(ScriptCommandAst::asCommandLine).collect(joining("\n"))
36+
+ "\n}";
2437
}
2538
}

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

Lines changed: 30 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -21,17 +21,24 @@
2121
///
2222
/// It is an abstraction to the commands of following structure:
2323
/// ```
24-
/// <commandName> key_1:value_1 ... key_m:value_m positionalArgs_1 ... positionalArgs_n {
25-
/// commands_0; ...; commands_k;
26-
///}
27-
///```
24+
/// integer-split
25+
/// "<0" : { auto; }
26+
/// "=0" : { instantiate; }
27+
/// ">0" : { tryclose; }
28+
/// ;
29+
/// ```
30+
/// or
31+
/// ```
32+
/// <commandName> key_1:value_1 ... key_m:value_m positionalArgs_1 ... positionalArgs_n;
33+
/// ```
34+
/// where `value_X` and `positionalArgs_X` can also be scripts.
2835
///
29-
/// @param commandName the name of the command, e.g., "macro" for `macro auto;`
30-
/// @param namedArgs a map of the given named arguments and values.
31-
/// If a named argument is not given, the entry should be missing in the map. Null-values are not
32-
/// allowed.
36+
/// @param commandName the name of the command, e.g., "macro" for `macro auto;`
37+
/// @param namedArgs a map of the given named arguments and values.
38+
/// If a named argument is not given, the entry should be missing in the map. Null-values are not
39+
/// allowed.
3340
/// @param positionalArgs the list of given positional arguments
34-
/// @param location the location of this command for error reporting. **excluded from equality**
41+
/// @param location the location of this command for error reporting. **excluded from equality**
3542
/// @author Alexander Weigl
3643
/// @version 1 (14.03.25)
3744
@NullMarked
@@ -42,7 +49,7 @@ public record ScriptCommandAst(
4249
@Nullable Location location) {
4350

4451
public ScriptCommandAst(String commandName, Map<String, Object> namedArgs,
45-
List<Object> positionalArgs) {
52+
List<Object> positionalArgs) {
4653
this(commandName, namedArgs, positionalArgs, null);
4754
}
4855

@@ -53,13 +60,13 @@ public ScriptCommandAst(String commandName, Map<String, Object> namedArgs,
5360
/// @see de.uka.ilkd.key.nparser.ParsingFacade#parseScript(CharStream)
5461
public String asCommandLine() {
5562
return commandName + ' ' +
56-
namedArgs.entrySet().stream()
57-
.map(it -> it.getKey() + ": " + asReadableString(it.getValue()))
58-
.collect(joining(" "))
59-
+ ' '
60-
+ positionalArgs.stream().map(ScriptCommandAst::asReadableString)
61-
.collect(joining(" "))
62-
+ ";";
63+
namedArgs.entrySet().stream()
64+
.map(it -> it.getKey() + ": " + asReadableString(it.getValue()))
65+
.collect(joining(" "))
66+
+ ' '
67+
+ positionalArgs.stream().map(ScriptCommandAst::asReadableString)
68+
.collect(joining(" "))
69+
+ ";";
6370
}
6471

6572
public static String asReadableString(Object value) {
@@ -83,8 +90,12 @@ public int hashCode() {
8390

8491
@Override
8592
public boolean equals(Object obj) {
86-
if (this == obj) { return true; }
87-
if(obj == null || getClass() != obj.getClass()) { return false; }
93+
if (this == obj) {
94+
return true;
95+
}
96+
if (obj == null || getClass() != obj.getClass()) {
97+
return false;
98+
}
8899
ScriptCommandAst other = (ScriptCommandAst) obj;
89100
return Objects.equals(commandName, other.commandName)
90101
&& Objects.equals(positionalArgs, other.positionalArgs)

‎key.core/src/test/java/de/uka/ilkd/key/scripts/ProofScriptParserTest.java‎

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,10 +5,7 @@
55

66
import de.uka.ilkd.key.nparser.ParsingFacade;
77

8-
import org.assertj.core.api.Assertions;
98
import org.junit.jupiter.api.Test;
10-
import org.slf4j.Logger;
11-
import org.slf4j.LoggerFactory;
129

1310
import static org.assertj.core.api.Assertions.assertThat;
1411

‎key.core/src/test/java/de/uka/ilkd/key/scripts/meta/ValueInjectorTest.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ public void testInjectionSimple() throws Exception {
2929
PP pp = new PP();
3030
Map<String, Object> args = new HashMap<>();
3131
ScriptCommandAst ast = new ScriptCommandAst("pp", args, new LinkedList<>(),
32-
null);
32+
null);
3333
args.put("b", true);
3434
args.put("i", 42);
3535

@@ -51,7 +51,7 @@ public void testRequired() {
5151
PP pp = new PP();
5252
Map<String, Object> args = new HashMap<>();
5353
ScriptCommandAst ast = new ScriptCommandAst("pp", args, new LinkedList<>(),
54-
null);
54+
null);
5555
args.put("b", "true");
5656
args.put("s", "blubb");
5757
assertThrows(ArgumentRequiredException.class,

0 commit comments

Comments
 (0)