Skip to content

Commit 6152973

Browse files
wadoonwadoon
committed
rename enum
1 parent 31a5a1b commit 6152973

14 files changed

Lines changed: 103 additions & 105 deletions

File tree

‎key.core/src/main/java/de/uka/ilkd/key/java/KeYJavaASTFactory.java‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -289,7 +289,7 @@ public static ProgramVariable localVariable(final Services services, final Strin
289289
* @return a new {@link LogicalAnd} of <code>left</code> and <code>right</code>
290290
*/
291291
public static BinaryOperator logicalAndOperator(final Expression left, final Expression right) {
292-
return new BinaryOperator(BinaryOperatorKind.LogicalAnd, left, right);
292+
return new BinaryOperator(BinaryOperatorKind.LOGICAL_AND, left, right);
293293
}
294294

295295
/**
@@ -304,7 +304,7 @@ public static BinaryOperator logicalAndOperator(final Expression left, final Exp
304304
* @return a new {@link LogicalOr} of <code>left</code> and <code>right</code>
305305
*/
306306
public static BinaryOperator logicalOrOperator(final Expression left, final Expression right) {
307-
return new BinaryOperator(BinaryOperatorKind.LogicalOr, left, right);
307+
return new BinaryOperator(BinaryOperatorKind.LOGICAL_OR, left, right);
308308

309309
}
310310

@@ -692,7 +692,7 @@ public static BinaryOperator equalsNullOperator(final Expression expression) {
692692
* @return a new {@link Equals} of <code>left</code> and <code>right</code>
693693
*/
694694
public static BinaryOperator equalsOperator(final Expression left, final Expression right) {
695-
return new BinaryOperator(BinaryOperatorKind.Equals, left, right);
695+
return new BinaryOperator(BinaryOperatorKind.EQUALS, left, right);
696696
}
697697

698698
/**
@@ -706,7 +706,7 @@ public static BinaryOperator equalsOperator(final Expression left, final Express
706706
* @return a new {@link Equals} of <code>operands</code>
707707
*/
708708
public static BinaryOperator equalsOperator(final ExtList operands) {
709-
return new BinaryOperator(BinaryOperatorKind.Equals, operands);
709+
return new BinaryOperator(BinaryOperatorKind.EQUALS, operands);
710710
}
711711

712712
/**
@@ -1073,7 +1073,7 @@ public static IGuard lessThanGuard(final Expression left, final Expression right
10731073
* @return a new {@link LessThan} that compares <code>left</code> less than <code>right</code>
10741074
*/
10751075
public static BinaryOperator lessThanOperator(final Expression left, final Expression right) {
1076-
return new BinaryOperator(BinaryOperatorKind.LessThan, left, right);
1076+
return new BinaryOperator(BinaryOperatorKind.LESS_THAN, left, right);
10771077
}
10781078

10791079
/**
@@ -1140,7 +1140,7 @@ public static IForUpdates forUpdates(final Expression update) {
11401140
*/
11411141
public static IForUpdates postIncrementForUpdates(final ProgramVariable variable) {
11421142
final Expression update =
1143-
new UnaryOperator(UnaryOperator.UnaryOperatorKind.PostIncrement, variable);
1143+
new UnaryOperator(UnaryOperator.UnaryOperatorKind.POST_INCREMENT, variable);
11441144
return forUpdates(update);
11451145
}
11461146

@@ -2124,7 +2124,7 @@ public static New newOperator(final KeYJavaType type) {
21242124
* @return a new {@link NotEquals} of <code>operands</code>
21252125
*/
21262126
public static BinaryOperator notEqualsOperator(final ExtList operands) {
2127-
return new BinaryOperator(BinaryOperatorKind.NotEquals, operands);
2127+
return new BinaryOperator(BinaryOperatorKind.NOT_EQUALS, operands);
21282128
}
21292129

21302130
/**

‎key.core/src/main/java/de/uka/ilkd/key/java/TypeConverter.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -151,11 +151,11 @@ private JTerm translateOperator(Operator op, ExecutionContext ec) {
151151
if (responsibleLDT != null) {
152152
return tb.func(responsibleLDT.getFunctionFor(op, services, ec), subs);
153153
} else if (op instanceof BinaryOperator bo
154-
&& bo.getKind() == BinaryOperator.BinaryOperatorKind.Equals) {
154+
&& bo.getKind() == BinaryOperator.BinaryOperatorKind.EQUALS) {
155155
assert subs.length == 2;
156156
return tb.equals(subs[0], subs[1]);
157157
} else if (op instanceof BinaryOperator bo
158-
&& bo.getKind() == BinaryOperator.BinaryOperatorKind.NotEquals) {
158+
&& bo.getKind() == BinaryOperator.BinaryOperatorKind.NOT_EQUALS) {
159159
assert subs.length == 2;
160160
return tb.not(tb.equals(subs[0], subs[1]));
161161
} else if (op instanceof Conditional) {

‎key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/BinaryOperator.java‎

Lines changed: 24 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -26,32 +26,30 @@ public BinaryOperator(BinaryOperatorKind binaryOperatorKind, ExtList operands) {
2626
}
2727

2828
public enum BinaryOperatorKind {
29-
Divide(2, "/"),
30-
Modulo(2, "%"),
31-
Times(2, "*"),
32-
Minus(3, "-"),
33-
Plus(3, "+"),
34-
Subtype(3, "<:"),
35-
36-
ShiftLeft(4, "<<"),
37-
ShiftRight(4, ">>"),
38-
UnsignedShiftRight(4, ">>>"),
39-
40-
GreaterOrEquals(5, ">="),
41-
LessOrEquals(5, "<="),
42-
GreaterThan(5, ">"),
43-
LessThan(5, "<"),
44-
Equals(6, "=="),
45-
NotEquals(6, "!="),
46-
47-
48-
BinaryAnd(7, "&"),
49-
BinaryXOr(8, "^"),
50-
BinaryOr(9, "|"),
51-
52-
53-
LogicalAnd(10, "&&"),
54-
LogicalOr(11, "||");
29+
DIVIDE(2, "/"),
30+
MODULO(2, "%"),
31+
TIMES(2, "*"),
32+
MINUS(3, "-"),
33+
PLUS(3, "+"),
34+
SUBTYPE(3, "<:"),
35+
36+
SHIFT_LEFT(4, "<<"),
37+
SHIFT_RIGHT(4, ">>"),
38+
UNSIGNED_SHIFT_RIGHT(4, ">>>"),
39+
40+
GREATER_OR_EQUALS(5, ">="),
41+
LESS_OR_EQUALS(5, "<="),
42+
GREATER_THAN(5, ">"),
43+
LESS_THAN(5, "<"),
44+
EQUALS(6, "=="),
45+
NOT_EQUALS(6, "!="),
46+
47+
48+
BINARY_AND(7, "&"),
49+
BINARY_XOR(8, "^"),
50+
BINARY_OR(9, "|"),
51+
LOGICAL_AND(10, "&&"),
52+
LOGICAL_OR(11, "||");
5553

5654

5755
public final int precedence;

‎key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/UnaryOperator.java‎

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -29,15 +29,15 @@ public UnaryOperator(UnaryOperatorKind kind, Expression arg) {
2929
}
3030

3131
public enum UnaryOperatorKind {
32-
LogicalNot("!", 1),
33-
Negative("-", 1),
34-
Positive("+", 1),
35-
BinaryNot("~", 1),
36-
37-
PreIncrement("++", 0),
38-
PreDecrement("--", 0),
39-
PostIncrement("++", 0, POSTFIX),
40-
PostDecrement("--", 0, POSTFIX);
32+
LOGICAL_NOT("!", 1),
33+
NEGATIVE("-", 1),
34+
POSITIVE("+", 1),
35+
BINARY_NOT("~", 1),
36+
37+
PRE_INCREMENT("++", 0),
38+
PRE_DECREMENT("--", 0),
39+
POST_INCREMENT("++", 0, POSTFIX),
40+
POST_DECREMENT("--", 0, POSTFIX);
4141

4242

4343
public final String symbol;

‎key.core/src/main/java/de/uka/ilkd/key/java/loader/CreateArrayMethodBuilder.java‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -50,8 +50,8 @@
5050
import org.key_project.util.collection.ImmutableList;
5151
import org.key_project.util.collection.ImmutableSLList;
5252

53-
import static de.uka.ilkd.key.java.ast.expression.operator.BinaryOperator.BinaryOperatorKind.LessThan;
54-
import static de.uka.ilkd.key.java.ast.expression.operator.UnaryOperator.UnaryOperatorKind.PostIncrement;
53+
import static de.uka.ilkd.key.java.ast.expression.operator.BinaryOperator.BinaryOperatorKind.LESS_THAN;
54+
import static de.uka.ilkd.key.java.ast.expression.operator.UnaryOperator.UnaryOperatorKind.POST_INCREMENT;
5555

5656
/**
5757
* This class creates the <code>&lt;createArray&gt;</code> method for array creation and in
@@ -384,8 +384,8 @@ public IProgramMethod getPrepareArrayMethod(TypeRef arrayRef, ProgramVariable le
384384
(ProgramVariable) forInit.getVariables().get(0).getProgramVariable();
385385

386386
final For forLoop = new For(new LoopInitializer[] { forInit },
387-
new BinaryOperator(LessThan, pv, new FieldReference(length, new ThisReference())),
388-
new Expression[] { new UnaryOperator(PostIncrement, pv) },
387+
new BinaryOperator(LESS_THAN, pv, new FieldReference(length, new ThisReference())),
388+
new Expression[] { new UnaryOperator(POST_INCREMENT, pv) },
389389
assign(new ArrayReference(new ThisReference(), new Expression[] { pv }), defaultValue));
390390

391391
final StatementBlock body = new StatementBlock(new Statement[] { forLoop });

‎key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java‎

Lines changed: 29 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -84,7 +84,7 @@
8484
import static com.github.javaparser.ast.Modifier.DefaultKeyword.*;
8585
import static de.uka.ilkd.key.java.ast.declaration.Modifier.createModifierList;
8686
import static de.uka.ilkd.key.java.ast.expression.operator.LogicFunctionalOperator.LogicFunction.*;
87-
import static de.uka.ilkd.key.java.ast.expression.operator.UnaryOperator.UnaryOperatorKind.Negative;
87+
import static de.uka.ilkd.key.java.ast.expression.operator.UnaryOperator.UnaryOperatorKind.NEGATIVE;
8888
import static java.lang.String.format;
8989

9090
/**
@@ -254,25 +254,25 @@ public Object visit(BinaryExpr n, Void arg) {
254254
var pi = createPositionInfo(n);
255255
var c = createComments(n);
256256
var op = switch (n.getOperator()) {
257-
case OR -> BinaryOperatorKind.LogicalOr;
258-
case AND -> BinaryOperatorKind.LogicalAnd;
259-
case BINARY_OR -> BinaryOperatorKind.BinaryOr;
260-
case BINARY_AND -> BinaryOperatorKind.BinaryAnd;
261-
case XOR -> BinaryOperatorKind.BinaryXOr;
262-
case EQUALS -> BinaryOperatorKind.Equals;
263-
case NOT_EQUALS -> BinaryOperatorKind.NotEquals;
264-
case LESS -> BinaryOperatorKind.LessThan;
265-
case GREATER -> BinaryOperatorKind.GreaterThan;
266-
case LESS_EQUALS -> BinaryOperatorKind.LessOrEquals;
267-
case GREATER_EQUALS -> BinaryOperatorKind.GreaterOrEquals;
268-
case LEFT_SHIFT -> BinaryOperatorKind.ShiftLeft;
269-
case SIGNED_RIGHT_SHIFT -> BinaryOperatorKind.ShiftRight;
270-
case UNSIGNED_RIGHT_SHIFT -> BinaryOperatorKind.UnsignedShiftRight;
271-
case PLUS -> BinaryOperatorKind.Plus;
272-
case MINUS -> BinaryOperatorKind.Minus;
273-
case MULTIPLY -> BinaryOperatorKind.Times;
274-
case DIVIDE -> BinaryOperatorKind.Divide;
275-
case REMAINDER -> BinaryOperatorKind.Modulo;
257+
case OR -> BinaryOperatorKind.LOGICAL_OR;
258+
case AND -> BinaryOperatorKind.LOGICAL_AND;
259+
case BINARY_OR -> BinaryOperatorKind.BINARY_OR;
260+
case BINARY_AND -> BinaryOperatorKind.BINARY_AND;
261+
case XOR -> BinaryOperatorKind.BINARY_XOR;
262+
case EQUALS -> BinaryOperatorKind.EQUALS;
263+
case NOT_EQUALS -> BinaryOperatorKind.NOT_EQUALS;
264+
case LESS -> BinaryOperatorKind.LESS_THAN;
265+
case GREATER -> BinaryOperatorKind.GREATER_THAN;
266+
case LESS_EQUALS -> BinaryOperatorKind.LESS_OR_EQUALS;
267+
case GREATER_EQUALS -> BinaryOperatorKind.GREATER_OR_EQUALS;
268+
case LEFT_SHIFT -> BinaryOperatorKind.SHIFT_LEFT;
269+
case SIGNED_RIGHT_SHIFT -> BinaryOperatorKind.SHIFT_RIGHT;
270+
case UNSIGNED_RIGHT_SHIFT -> BinaryOperatorKind.UNSIGNED_SHIFT_RIGHT;
271+
case PLUS -> BinaryOperatorKind.PLUS;
272+
case MINUS -> BinaryOperatorKind.MINUS;
273+
case MULTIPLY -> BinaryOperatorKind.TIMES;
274+
case DIVIDE -> BinaryOperatorKind.DIVIDE;
275+
case REMAINDER -> BinaryOperatorKind.MODULO;
276276
};
277277
return new BinaryOperator(pi, c, op, lhs, rhs);
278278
}
@@ -1345,19 +1345,19 @@ public Object visit(UnaryExpr n, Void arg) {
13451345
}
13461346
return new IntLiteral(pi, c, -num.intValue());
13471347
}
1348-
return new UnaryOperator(pi, c, Negative, accept(expr));
1348+
return new UnaryOperator(pi, c, NEGATIVE, accept(expr));
13491349
}
13501350

13511351
Expression child = accept(n.getExpression());
13521352
var op = switch (n.getOperator()) {
1353-
case PLUS -> UnaryOperatorKind.Positive;
1354-
case MINUS -> UnaryOperatorKind.Negative;
1355-
case PREFIX_INCREMENT -> UnaryOperatorKind.PreIncrement;
1356-
case PREFIX_DECREMENT -> UnaryOperatorKind.PreDecrement;
1357-
case LOGICAL_COMPLEMENT -> UnaryOperatorKind.LogicalNot;
1358-
case BITWISE_COMPLEMENT -> UnaryOperatorKind.BinaryNot;
1359-
case POSTFIX_INCREMENT -> UnaryOperatorKind.PostIncrement;
1360-
case POSTFIX_DECREMENT -> UnaryOperatorKind.PostDecrement;
1353+
case PLUS -> UnaryOperatorKind.POSITIVE;
1354+
case MINUS -> UnaryOperatorKind.NEGATIVE;
1355+
case PREFIX_INCREMENT -> UnaryOperatorKind.PRE_INCREMENT;
1356+
case PREFIX_DECREMENT -> UnaryOperatorKind.PRE_DECREMENT;
1357+
case LOGICAL_COMPLEMENT -> UnaryOperatorKind.LOGICAL_NOT;
1358+
case BITWISE_COMPLEMENT -> UnaryOperatorKind.BINARY_NOT;
1359+
case POSTFIX_INCREMENT -> UnaryOperatorKind.POST_INCREMENT;
1360+
case POSTFIX_DECREMENT -> UnaryOperatorKind.POST_DECREMENT;
13611361
};
13621362
return new UnaryOperator(pi, c, op, child);
13631363
}

‎key.core/src/main/java/de/uka/ilkd/key/ldt/DoubleLDT.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -143,7 +143,7 @@ public boolean isResponsible(Operator op, JTerm sub,
143143
TermServices services, ExecutionContext ec) {
144144
if (sub != null && sub.sort().extendsTrans(targetSort())) {
145145
return op instanceof UnaryOperator uo
146-
&& uo.getKind() == UnaryOperator.UnaryOperatorKind.Negative;
146+
&& uo.getKind() == UnaryOperator.UnaryOperatorKind.NEGATIVE;
147147
}
148148
return false;
149149
}
@@ -189,7 +189,7 @@ public Function getFunctionFor(Operator op,
189189
Services services,
190190
ExecutionContext ec) {
191191
if (op instanceof UnaryOperator u
192-
&& u.getKind() == UnaryOperator.UnaryOperatorKind.Negative) {
192+
&& u.getKind() == UnaryOperator.UnaryOperatorKind.NEGATIVE) {
193193
return getJavaUnaryMinus();
194194
} else {
195195
return null;

‎key.core/src/main/java/de/uka/ilkd/key/ldt/FloatLDT.java‎

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -121,7 +121,7 @@ public boolean isResponsible(Operator op, JTerm sub,
121121
TermServices services, ExecutionContext ec) {
122122
return sub != null && sub.sort().extendsTrans(targetSort()) &&
123123
op instanceof UnaryOperator u
124-
&& u.getKind() == UnaryOperator.UnaryOperatorKind.Negative;
124+
&& u.getKind() == UnaryOperator.UnaryOperatorKind.NEGATIVE;
125125

126126
}
127127

@@ -138,7 +138,7 @@ public Function getFunctionFor(Operator op,
138138
Services services,
139139
ExecutionContext ec) {
140140
if ((op instanceof UnaryOperator u)
141-
&& u.getKind() == UnaryOperator.UnaryOperatorKind.Negative) {
141+
&& u.getKind() == UnaryOperator.UnaryOperatorKind.NEGATIVE) {
142142
return getJavaUnaryMinus();
143143
}
144144

@@ -147,15 +147,15 @@ public Function getFunctionFor(Operator op,
147147
}
148148

149149
return switch (b.getKind()) {
150-
case GreaterThan -> getGreaterThan();
151-
case LessThan -> getLessThan();
152-
case GreaterOrEquals -> getGreaterOrEquals();
153-
case LessOrEquals -> getLessOrEquals();
154-
case Plus -> getJavaAdd();
155-
case Minus -> getJavaSub();
156-
case Times -> getJavaMul();
157-
case Divide -> getJavaDiv();
158-
case Modulo -> getJavaMod();
150+
case GREATER_THAN -> getGreaterThan();
151+
case LESS_THAN -> getLessThan();
152+
case GREATER_OR_EQUALS -> getGreaterOrEquals();
153+
case LESS_OR_EQUALS -> getLessOrEquals();
154+
case PLUS -> getJavaAdd();
155+
case MINUS -> getJavaSub();
156+
case TIMES -> getJavaMul();
157+
case DIVIDE -> getJavaDiv();
158+
case MODULO -> getJavaMod();
159159
default -> null;
160160
};
161161
}

‎key.core/src/main/java/de/uka/ilkd/key/ldt/SortLDT.java‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -47,23 +47,23 @@ public boolean isResponsible(Operator op, JTerm[] subs,
4747
Services services,
4848
ExecutionContext ec) {
4949
return op instanceof BinaryOperator lfo
50-
&& lfo.getKind() == BinaryOperator.BinaryOperatorKind.Subtype;
50+
&& lfo.getKind() == BinaryOperator.BinaryOperatorKind.SUBTYPE;
5151
}
5252

5353
@Override
5454
public boolean isResponsible(Operator op, JTerm left, JTerm right,
5555
Services services,
5656
ExecutionContext ec) {
5757
return op instanceof BinaryOperator lfo
58-
&& lfo.getKind() == BinaryOperator.BinaryOperatorKind.Subtype;
58+
&& lfo.getKind() == BinaryOperator.BinaryOperatorKind.SUBTYPE;
5959
}
6060

6161
@Override
6262
public boolean isResponsible(Operator op, JTerm sub,
6363
TermServices services,
6464
ExecutionContext ec) {
6565
return op instanceof BinaryOperator lfo
66-
&& lfo.getKind() == BinaryOperator.BinaryOperatorKind.Subtype;
66+
&& lfo.getKind() == BinaryOperator.BinaryOperatorKind.SUBTYPE;
6767
}
6868

6969
@Override
@@ -76,7 +76,7 @@ public JTerm translateLiteral(Literal lit, Services services) {
7676
public Function getFunctionFor(Operator op, Services services,
7777
ExecutionContext ec) {
7878
if (op instanceof BinaryOperator lfo
79-
&& lfo.getKind() == BinaryOperator.BinaryOperatorKind.Subtype) {
79+
&& lfo.getKind() == BinaryOperator.BinaryOperatorKind.SUBTYPE) {
8080
return ssubsort;
8181
}
8282

‎key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@
2929
import org.slf4j.Logger;
3030
import org.slf4j.LoggerFactory;
3131

32-
import static de.uka.ilkd.key.java.ast.expression.operator.UnaryOperator.UnaryOperatorKind.Negative;
32+
import static de.uka.ilkd.key.java.ast.expression.operator.UnaryOperator.UnaryOperatorKind.NEGATIVE;
3333

3434
/**
3535
* Special "sorts" used for schema variables matching program constructs (class ProgramSV). Not
@@ -437,7 +437,7 @@ protected SimpleExpressionSort(Name n) {
437437

438438
@Override
439439
protected boolean canStandFor(ProgramElement pe, Services services) {
440-
if (pe instanceof UnaryOperator uo && uo.getKind() == Negative) {
440+
if (pe instanceof UnaryOperator uo && uo.getKind() == NEGATIVE) {
441441
return uo.getChildAt(0) instanceof Literal;
442442
}
443443

0 commit comments

Comments
 (0)