Skip to content

Commit e841235

Browse files
wadoonwadoon
committed
reformat and fix compilation error
1 parent 5eec835 commit e841235

18 files changed

Lines changed: 140 additions & 112 deletions

File tree

‎key.core/src/main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java‎

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

6-
import java.io.IOException;
76
import java.util.*;
7+
import java.util.ArrayList;
88
import java.util.stream.Collectors;
99

1010
import de.uka.ilkd.key.control.AbstractUserInterfaceControl;
@@ -44,8 +44,6 @@
4444
import org.slf4j.Logger;
4545
import org.slf4j.LoggerFactory;
4646

47-
import java.util.ArrayList;
48-
4947
public class ApplyScriptsMacro extends AbstractProofMacro {
5048

5149
private static final Logger LOGGER = LoggerFactory.getLogger(ApplyScriptsMacro.class);
@@ -86,7 +84,8 @@ private static JmlAssert getJmlAssert(Node node) {
8684
target = UpdateApplication.getTarget(target);
8785
}
8886
final SourceElement activeStatement = JavaTools.getActiveStatement(target.javaBlock());
89-
if (activeStatement instanceof JmlAssert jmlAssert && jmlAssert.getAssertionProof() != null) {
87+
if (activeStatement instanceof JmlAssert jmlAssert
88+
&& jmlAssert.getAssertionProof() != null) {
9089
return jmlAssert;
9190
}
9291
}
@@ -96,7 +95,7 @@ private static JmlAssert getJmlAssert(Node node) {
9695
private static @Nullable JTerm getUpdate(Goal goal) {
9796
RuleApp ruleApp = goal.node().parent().getAppliedRuleApp();
9897
Term appliedOn = ruleApp.posInOccurrence().subTerm();
99-
if(appliedOn.op() instanceof UpdateApplication) {
98+
if (appliedOn.op() instanceof UpdateApplication) {
10099
return UpdateApplication.getUpdate((JTerm) appliedOn);
101100
}
102101
return null;
@@ -118,7 +117,8 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof,
118117
continue;
119118
}
120119

121-
listener.taskStarted(new DefaultTaskStartedInfo(TaskStartedInfo.TaskKind.Other, "Running attached script from goal " + goal.node().serialNr(), 0));
120+
listener.taskStarted(new DefaultTaskStartedInfo(TaskStartedInfo.TaskKind.Other,
121+
"Running attached script from goal " + goal.node().serialNr(), 0));
122122

123123
KeyAst.JMLProofScript proofScript = jmlAssert.getAssertionProof();
124124
Map<ParserRuleContext, JTerm> termMap = getTermMap(jmlAssert, proof.getServices());
@@ -127,17 +127,19 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof,
127127
renderProof(proofScript, termMap, update, proof.getServices());
128128
ProofScriptEngine pse = new ProofScriptEngine(renderedProof, goal);
129129
LOGGER.debug("---- Script");
130-
LOGGER.debug(renderedProof.stream().map(ScriptCommandAst::asCommandLine).collect(Collectors.joining("\n")));
130+
LOGGER.debug(renderedProof.stream().map(ScriptCommandAst::asCommandLine)
131+
.collect(Collectors.joining("\n")));
131132
LOGGER.debug("---- End Script");
132133

133134
pse.execute((AbstractUserInterfaceControl) uic, proof);
134135
}
135-
listener.taskStarted(new DefaultTaskStartedInfo(TaskStartedInfo.TaskKind.Other, "Running fallback macro on the remaining goals", 0));
136+
listener.taskStarted(new DefaultTaskStartedInfo(TaskStartedInfo.TaskKind.Other,
137+
"Running fallback macro on the remaining goals", 0));
136138
for (Goal goal : laterGoals) {
137139
if (Thread.interrupted()) {
138140
throw new InterruptedException();
139141
}
140-
if(fallBackMacro != null) {
142+
if (fallBackMacro != null) {
141143
fallBackMacro.applyTo(uic, proof, ImmutableList.of(goal), posInOcc, listener);
142144
}
143145

@@ -165,8 +167,8 @@ private Map<ParserRuleContext, JTerm> getTermMap(JmlAssert jmlAssert, Services s
165167
return result;
166168
}
167169

168-
private static List<ScriptCommandAst> renderProof(KeyAst.JMLProofScript script,
169-
Map<ParserRuleContext, JTerm> termMap, JTerm update, Services services) {
170+
private static List<ScriptCommandAst> renderProof(KeyAst.JMLProofScript script,
171+
Map<ParserRuleContext, JTerm> termMap, JTerm update, Services services) {
170172
List<ScriptCommandAst> result = new ArrayList<>();
171173
// Do not fail on open proofs
172174
// TODO Migrate into SetCommand
@@ -182,7 +184,7 @@ private static List<ScriptCommandAst> renderProof(KeyAst.JMLProofScript script,
182184
}
183185

184186
private static List<ScriptCommandAst> renderProofCmd(ProofCmdContext ctx,
185-
Map<ParserRuleContext, JTerm> termMap, JTerm update, Services services) {
187+
Map<ParserRuleContext, JTerm> termMap, JTerm update, Services services) {
186188
List<ScriptCommandAst> result = new ArrayList<>();
187189

188190
// Push the current branch context
@@ -198,9 +200,9 @@ private static List<ScriptCommandAst> renderProofCmd(ProofCmdContext ctx,
198200
value = StringUtil.stripQuotes(exp.getText());
199201
} else {
200202
value = termMap.get(exp);
201-
if(update != null) {
203+
if (update != null) {
202204
// Wrap in update application if an update is present
203-
value = services.getTermBuilder().apply(update, (JTerm)value);
205+
value = services.getTermBuilder().apply(update, (JTerm) value);
204206
}
205207
}
206208
if (argContext.argLabel != null) {

‎key.core/src/main/java/de/uka/ilkd/key/macros/ScriptAwarePrepMacro.java‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,6 @@
1+
/* This file is part of KeY - https://key-project.org
2+
* KeY is licensed under the GNU General Public License Version 2
3+
* SPDX-License-Identifier: GPL-2.0-only */
14
// This file is part of KeY - Integrated Deductive Software Design
25
//
36
// Copyright (C) 2001-2011 Universitaet Karlsruhe (TH), Germany

‎key.core/src/main/java/de/uka/ilkd/key/parser/Location.java‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,6 @@
66
import java.net.MalformedURLException;
77
import java.net.URI;
88
import java.net.URISyntaxException;
9-
import java.net.URL;
109
import java.util.Comparator;
1110
import java.util.Objects;
1211
import java.util.Optional;
@@ -72,7 +71,7 @@ public static Location fromToken(Token token) {
7271

7372
public static Location fromPositionInfo(PositionInfo info) {
7473
Optional<URI> uri = info.getURI();
75-
if(uri.isEmpty()) {
74+
if (uri.isEmpty()) {
7675
return UNDEFINED;
7776
} else {
7877
Position pos = info.getStartPosition();

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,8 @@ public abstract class AbstractCommand implements ProofScriptCommand {
4848
}
4949

5050
/**
51-
* The POJO class of the parameter object, or null if this command does not take any parameters via
51+
* The POJO class of the parameter object, or null if this command does not take any parameters
52+
* via
5253
* a POJO.
5354
*/
5455
private final @Nullable Class<?> parameterClazz;

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

Lines changed: 22 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -1,31 +1,35 @@
1-
///* This file is part of KeY - https://key-project.org
1+
/* This file is part of KeY - https://key-project.org
2+
* KeY is licensed under the GNU General Public License Version 2
3+
* SPDX-License-Identifier: GPL-2.0-only */
4+
/// * This file is part of KeY - https://key-project.org
25
// * KeY is licensed under the GNU General Public License Version 2
36
// * SPDX-License-Identifier: GPL-2.0-only */
4-
//package de.uka.ilkd.key.scripts;
7+
// package de.uka.ilkd.key.scripts;
58
//
6-
///**
9+
/// **
710
// * An assertion which essentially performs a cut.
811
// *
9-
// * The only difference is that this implementation tampers with the labels of the resulting goals to
12+
// * The only difference is that this implementation tampers with the labels of the resulting goals
13+
/// to
1014
// * allow them to be
1115
// * better recognized in the script engine.
1216
// *
1317
// * (Unlike in other systems, in KeY the assertion does not remove the original goal formula since
1418
// * that is not well-defined in sequent calculus.)
1519
// */
16-
//public class AssertCommand extends CutCommand {
20+
// public class AssertCommand extends CutCommand {
1721
//
18-
// @Override
19-
// public String getName() {
20-
// return "assert";
21-
// }
22+
// @Override
23+
// public String getName() {
24+
// return "assert";
25+
// }
2226
//
23-
// @Override
24-
// public void execute(ScriptCommandAst arguments) throws ScriptException, InterruptedException {
25-
// var args = state().getValueInjector().inject(new Parameters(), arguments);
26-
// var node = state().getFirstOpenAutomaticGoal().node();
27-
// execute(state(), args);
28-
// // node.proof().getGoal(node.child(0)).setBranchLabel("Validity");
29-
// // node.proof().getGoal(node.child(1)).setBranchLabel("Usage");
30-
// }
31-
//}
27+
// @Override
28+
// public void execute(ScriptCommandAst arguments) throws ScriptException, InterruptedException {
29+
// var args = state().getValueInjector().inject(new Parameters(), arguments);
30+
// var node = state().getFirstOpenAutomaticGoal().node();
31+
// execute(state(), args);
32+
// // node.proof().getGoal(node.child(0)).setBranchLabel("Validity");
33+
// // node.proof().getGoal(node.child(1)).setBranchLabel("Usage");
34+
// }
35+
// }

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

Lines changed: 8 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -11,20 +11,18 @@
1111
import java.util.Optional;
1212
import java.util.Stack;
1313

14-
import de.uka.ilkd.key.logic.op.SortDependingFunction;
1514
import de.uka.ilkd.key.proof.Goal;
1615
import de.uka.ilkd.key.proof.Node;
1716
import de.uka.ilkd.key.proof.Proof;
1817
import de.uka.ilkd.key.rule.TacletApp;
1918
import de.uka.ilkd.key.scripts.meta.Argument;
20-
import de.uka.ilkd.key.scripts.meta.InjectionException;
2119
import de.uka.ilkd.key.scripts.meta.Option;
2220

23-
import de.uka.ilkd.key.scripts.meta.ValueInjector;
24-
import org.jspecify.annotations.Nullable;
2521
import org.key_project.prover.rules.tacletbuilder.TacletGoalTemplate;
2622
import org.key_project.util.collection.ImmutableList;
2723

24+
import org.jspecify.annotations.Nullable;
25+
2826
public class BranchesCommand extends AbstractCommand {
2927

3028
public BranchesCommand() {
@@ -46,7 +44,7 @@ public void execute(ScriptCommandAst arguments) throws ScriptException, Interrup
4644
state.putUserData("_branchStack", stack);
4745
}
4846

49-
if(args.mode == null) {
47+
if (args.mode == null) {
5048
throw new ScriptException("For 'branches', a mode must be specified");
5149
}
5250

@@ -77,8 +75,8 @@ public void execute(ScriptCommandAst arguments) throws ScriptException, Interrup
7775
int no = 0;
7876
int found = -1;
7977
for (TacletGoalTemplate template : templates) {
80-
if(!"main".equals(template.tag())) {
81-
if(found != -1) {
78+
if (!"main".equals(template.tag())) {
79+
if (found != -1) {
8280
throw new ScriptException("More than one non-main goal found");
8381
}
8482
found = no;
@@ -95,12 +93,13 @@ public void execute(ScriptCommandAst arguments) throws ScriptException, Interrup
9593
state.setGoal(goal);
9694
break;
9795
default:
98-
throw new ScriptException("Unknown mode " + args.mode + " for the 'branches' command" );
96+
throw new ScriptException(
97+
"Unknown mode " + args.mode + " for the 'branches' command");
9998
}
10099
}
101100

102101
private void ensureSingleGoal() {
103-
//state.
102+
// state.
104103
}
105104

106105
private Goal findGoalByName(Node root, String branch) throws ScriptException {

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

Lines changed: 15 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,6 @@
1+
/* This file is part of KeY - https://key-project.org
2+
* KeY is licensed under the GNU General Public License Version 2
3+
* SPDX-License-Identifier: GPL-2.0-only */
14
package de.uka.ilkd.key.scripts;
25

36
import de.uka.ilkd.key.control.AbstractUserInterfaceControl;
@@ -6,6 +9,7 @@
69
import de.uka.ilkd.key.rule.NoPosTacletApp;
710
import de.uka.ilkd.key.rule.Taclet;
811
import de.uka.ilkd.key.rule.TacletApp;
12+
913
import org.key_project.logic.ChoiceExpr;
1014
import org.key_project.logic.Name;
1115
import org.key_project.prover.rules.ApplicationRestriction;
@@ -19,10 +23,14 @@ public class CheatCommand extends NoArgumentCommand {
1923
private static final Taclet CHEAT_TACLET;
2024

2125
static {
22-
TacletApplPart applPart = new TacletApplPart(JavaDLSequentKit.getInstance().getEmptySequent(),
23-
ApplicationRestriction.NONE, ImmutableList.of(), ImmutableList.of(), ImmutableList.of(), ImmutableList.of());
24-
CHEAT_TACLET = new NoFindTaclet(new Name("CHEAT"), applPart, ImmutableList.of(), ImmutableList.of(),
25-
new TacletAttributes("cheat", null), DefaultImmutableMap.nilMap(), ChoiceExpr.TRUE, ImmutableSet.empty());
26+
TacletApplPart applPart =
27+
new TacletApplPart(JavaDLSequentKit.getInstance().getEmptySequent(),
28+
ApplicationRestriction.NONE, ImmutableList.of(), ImmutableList.of(),
29+
ImmutableList.of(), ImmutableList.of());
30+
CHEAT_TACLET =
31+
new NoFindTaclet(new Name("CHEAT"), applPart, ImmutableList.of(), ImmutableList.of(),
32+
new TacletAttributes("cheat", null), DefaultImmutableMap.nilMap(), ChoiceExpr.TRUE,
33+
ImmutableSet.empty());
2634
}
2735

2836
@Override
@@ -33,13 +41,13 @@ public String getName() {
3341
@Override
3442
public String getDocumentation() {
3543
return "Use this to close a goal unconditionally. This is unsound and should only " +
36-
"be used for testing and proof debugging purposes. It is similar to 'sorry' " +
37-
"in Isabelle or 'admit' in Rocq.";
44+
"be used for testing and proof debugging purposes. It is similar to 'sorry' " +
45+
"in Isabelle or 'admit' in Rocq.";
3846
}
3947

4048
@Override
4149
public void execute(AbstractUserInterfaceControl uiControl, ScriptCommandAst ast,
42-
EngineState state)
50+
EngineState state)
4351
throws ScriptException, InterruptedException {
4452
TacletApp app = NoPosTacletApp.createNoPosTacletApp(CHEAT_TACLET);
4553
state.getFirstOpenAutomaticGoal().apply(app);

‎key.core/src/main/java/de/uka/ilkd/key/scripts/CutCommand.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.util.List;
7+
68
import de.uka.ilkd.key.logic.JTerm;
79
import de.uka.ilkd.key.rule.NoPosTacletApp;
810
import de.uka.ilkd.key.rule.Taclet;
@@ -14,8 +16,6 @@
1416

1517
import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
1618

17-
import java.util.List;
18-
1919
/**
2020
* The command object CutCommand has as scriptcommand name "cut" As parameters: a formula with the
2121
* id "#2"

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

Lines changed: 14 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,18 @@
1+
/* This file is part of KeY - https://key-project.org
2+
* KeY is licensed under the GNU General Public License Version 2
3+
* SPDX-License-Identifier: GPL-2.0-only */
14
package de.uka.ilkd.key.scripts;
25

6+
import java.util.ArrayList;
7+
import java.util.List;
8+
39
import de.uka.ilkd.key.java.Services;
410
import de.uka.ilkd.key.logic.JTerm;
5-
import de.uka.ilkd.key.scripts.meta.Option;
611
import de.uka.ilkd.key.proof.Goal;
712
import de.uka.ilkd.key.rule.IBuiltInRuleApp;
813
import de.uka.ilkd.key.rule.UseDependencyContractApp;
9-
import org.jspecify.annotations.Nullable;
14+
import de.uka.ilkd.key.scripts.meta.Option;
15+
1016
import org.key_project.logic.PosInTerm;
1117
import org.key_project.logic.Term;
1218
import org.key_project.prover.sequent.PosInOccurrence;
@@ -15,8 +21,7 @@
1521
import org.key_project.util.collection.ImmutableArray;
1622
import org.key_project.util.collection.ImmutableList;
1723

18-
import java.util.ArrayList;
19-
import java.util.List;
24+
import org.jspecify.annotations.Nullable;
2025

2126
public class DependencyContractCommand extends AbstractCommand {
2227

@@ -38,12 +43,13 @@ public void execute(ScriptCommandAst command) throws ScriptException, Interrupte
3843

3944
if (arguments.heap == null) {
4045
Services services = goal.proof().getServices();
41-
arguments.heap = services.getTermFactory().createTerm(services.getTypeConverter().getHeapLDT().getHeap());
46+
arguments.heap = services.getTermFactory()
47+
.createTerm(services.getTypeConverter().getHeapLDT().getHeap());
4248
}
4349

4450
List<PosInOccurrence> pios = find(arguments.on, goal.sequent());
4551

46-
if(pios.isEmpty()) {
52+
if (pios.isEmpty()) {
4753
throw new ScriptException("dependency contract not applicable.");
4854
} else if (pios.size() > 1) {
4955
throw new ScriptException("no unique application");
@@ -90,7 +96,8 @@ private void apply(Goal goal, UseDependencyContractApp ruleApp, Parameters argum
9096
JTerm[] subs = on.subs().toArray(new JTerm[0]);
9197
subs[0] = arguments.heap;
9298
Services services = goal.proof().getServices();
93-
JTerm replaced = services.getTermFactory().createTerm(on.op(), subs, on.boundVars(), on.getLabels());
99+
JTerm replaced =
100+
services.getTermFactory().createTerm(on.op(), subs, on.boundVars(), on.getLabels());
94101
List<PosInOccurrence> pios = find(replaced, goal.sequent());
95102
ruleApp = ruleApp.setStep(pios.get(0));
96103
ruleApp = ruleApp.tryToInstantiateContract(services);

0 commit comments

Comments
 (0)