Skip to content

Commit 0e87021

Browse files
rcosta358rcosta358
committed
SimplifiedPredicate Follow-Up
1 parent 22e89b8 commit 0e87021

2 files changed

Lines changed: 43 additions & 44 deletions

File tree

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java‎

Lines changed: 16 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -6,9 +6,9 @@
66

77
import liquidjava.processor.VCImplication;
88
import liquidjava.rj_language.Predicate;
9+
import liquidjava.rj_language.SimplifiedPredicate;
910
import liquidjava.rj_language.ast.BinaryExpression;
1011
import liquidjava.rj_language.ast.Expression;
11-
import liquidjava.rj_language.ast.SimplifiedExpression;
1212
import liquidjava.rj_language.ast.Var;
1313

1414
/**
@@ -80,13 +80,12 @@ private static VCImplication substitute(VCImplication implication, VCImplication
8080
* Substitutes a source binder inside one predicate while preserving simplification metadata
8181
*/
8282
private static Predicate substituteRefinement(Predicate refinement, VCImplication source, Expression value) {
83-
Expression expression = refinement.getExpression();
84-
Expression active = activeExpression(expression);
85-
SimplifiedExpression.Binder binder = new SimplifiedExpression.Binder(source.getName(), source.getType());
83+
Expression active = activeExpression(refinement);
84+
SimplifiedPredicate.Binder binder = new SimplifiedPredicate.Binder(source.getName(), source.getType());
8685
Expression substituted = active.substitute(new Var(binder.getName()), value.clone());
8786

88-
return new Predicate(new SimplifiedExpression(substituted, originExpression(expression),
89-
bindersAfterSubstitution(expression, active, binder)));
87+
return new SimplifiedPredicate(new Predicate(substituted), originPredicate(refinement),
88+
bindersAfterSubstitution(refinement, active, binder));
9089
}
9190

9291
/**
@@ -101,18 +100,18 @@ private static VCImplication copyWithRefinement(VCImplication implication, Predi
101100
/**
102101
* Returns the expression that should be shown as the original formula
103102
*/
104-
private static Expression originExpression(Expression expression) {
105-
if (expression instanceof SimplifiedExpression simplified)
103+
private static Predicate originPredicate(Predicate refinement) {
104+
if (refinement instanceof SimplifiedPredicate simplified)
106105
return simplified.getOrigin().clone();
107-
return expression.clone();
106+
return refinement.clone();
108107
}
109108

110109
/**
111110
* Builds the binder metadata after one substitution
112111
*/
113-
private static List<SimplifiedExpression.Binder> bindersAfterSubstitution(Expression expression, Expression active,
114-
SimplifiedExpression.Binder binder) {
115-
List<SimplifiedExpression.Binder> binders = expression instanceof SimplifiedExpression previous
112+
private static List<SimplifiedPredicate.Binder> bindersAfterSubstitution(Predicate refinement, Expression active,
113+
SimplifiedPredicate.Binder binder) {
114+
List<SimplifiedPredicate.Binder> binders = refinement instanceof SimplifiedPredicate previous
116115
? new ArrayList<>(previous.getBinders()) : new ArrayList<>();
117116
if (containsVariable(active, binder.getName()) && !binders.contains(binder))
118117
binders.add(binder);
@@ -140,7 +139,7 @@ private static Optional<Substitution> getSubstitution(VCImplication implication)
140139
if (!implication.hasBinder())
141140
return Optional.empty();
142141

143-
Expression refinement = activeExpression(implication.getRefinement().getExpression());
142+
Expression refinement = activeExpression(implication.getRefinement());
144143
if (!(refinement instanceof BinaryExpression binary) || !"==".equals(binary.getOperator()))
145144
return Optional.empty();
146145

@@ -175,9 +174,9 @@ private static boolean containsVariable(Expression expression, String name) {
175174
/**
176175
* Returns the expression used for matching and substitution
177176
*/
178-
private static Expression activeExpression(Expression expression) {
179-
if (expression instanceof SimplifiedExpression simplified)
180-
return simplified.getSimplifiedExpression().clone();
181-
return expression.clone();
177+
private static Expression activeExpression(Predicate refinement) {
178+
if (refinement instanceof SimplifiedPredicate simplified)
179+
return simplified.getSimplifiedPredicate().getExpression().clone();
180+
return refinement.getExpression().clone();
182181
}
183182
}

‎liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java‎

Lines changed: 27 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,8 @@
66

77
import liquidjava.processor.VCImplication;
88
import liquidjava.rj_language.Predicate;
9+
import liquidjava.rj_language.SimplifiedPredicate;
910
import liquidjava.rj_language.ast.Expression;
10-
import liquidjava.rj_language.ast.SimplifiedExpression;
1111
import liquidjava.rj_language.parsing.RefinementsParser;
1212
import spoon.Launcher;
1313
import spoon.reflect.reference.CtTypeReference;
@@ -52,39 +52,39 @@ private static CtTypeReference<?> type(String name) {
5252
}
5353

5454
public static void assertSimplifiedVC(VCImplication implication, String... expected) {
55-
ExpectedSimplifiedExpression[] expressions = java.util.Arrays.stream(expected)
56-
.map(VCTestUtils::parseExpectedSimplifiedExpression).toArray(ExpectedSimplifiedExpression[]::new);
57-
assertSimplifiedVC(implication, expressions);
55+
ExpectedSimplifiedPredicate[] predicates = java.util.Arrays.stream(expected)
56+
.map(VCTestUtils::parseExpectedSimplifiedPredicate).toArray(ExpectedSimplifiedPredicate[]::new);
57+
assertSimplifiedVC(implication, predicates);
5858
}
5959

60-
public static void assertSimplifiedVC(VCImplication implication, ExpectedSimplifiedExpression... expected) {
60+
public static void assertSimplifiedVC(VCImplication implication, ExpectedSimplifiedPredicate... expected) {
6161
VCImplication current = implication;
6262
for (int i = 0; i < expected.length; i++) {
63-
ExpectedSimplifiedExpression expectedExpression = expected[i];
64-
SimplifiedExpression expression = simplifiedExpression(current, i);
65-
assertEquals(expectedExpression.simplified(), expression.getSimplifiedExpression().toString(),
63+
ExpectedSimplifiedPredicate expectedPredicate = expected[i];
64+
SimplifiedPredicate predicate = simplifiedPredicate(current, i);
65+
assertEquals(expectedPredicate.simplified(), predicate.getSimplifiedPredicate().toString(),
6666
"Unexpected simplified expression at implication " + i);
67-
if (expectedExpression.origin() != null)
68-
assertEquals(expectedExpression.origin(), expression.getOrigin().toString(),
67+
if (expectedPredicate.origin() != null)
68+
assertEquals(expectedPredicate.origin(), predicate.getOrigin().toString(),
6969
"Unexpected origin expression at implication " + i);
70-
if (expectedExpression.binders() != null)
71-
assertEquals(expectedExpression.binders(), formatBinders(expression),
70+
if (expectedPredicate.binders() != null)
71+
assertEquals(expectedPredicate.binders(), formatBinders(predicate),
7272
"Unexpected binders at implication " + i);
7373
current = current.getNext();
7474
}
7575
assertNull(current, "Expected VC chain to end after " + expected.length + " implications");
7676
}
7777

78-
public static ExpectedSimplifiedExpression simplified(String simplified) {
79-
return new ExpectedSimplifiedExpression(simplified, null, null);
78+
public static ExpectedSimplifiedPredicate simplified(String simplified) {
79+
return new ExpectedSimplifiedPredicate(simplified, null, null);
8080
}
8181

82-
public static ExpectedSimplifiedExpression simplified(String simplified, String origin) {
83-
return new ExpectedSimplifiedExpression(simplified, origin, null);
82+
public static ExpectedSimplifiedPredicate simplified(String simplified, String origin) {
83+
return new ExpectedSimplifiedPredicate(simplified, origin, null);
8484
}
8585

86-
public static ExpectedSimplifiedExpression simplified(String simplified, String origin, String binders) {
87-
return new ExpectedSimplifiedExpression(simplified, origin, binders);
86+
public static ExpectedSimplifiedPredicate simplified(String simplified, String origin, String binders) {
87+
return new ExpectedSimplifiedPredicate(simplified, origin, binders);
8888
}
8989

9090
public static void assertVC(VCImplication implication, String... expected) {
@@ -97,18 +97,18 @@ public static void assertVC(VCImplication implication, String... expected) {
9797
assertNull(current, "Expected VC chain to end after " + expected.length + " implications");
9898
}
9999

100-
public static SimplifiedExpression simplifiedExpression(VCImplication implication, int index) {
101-
assertInstanceOf(SimplifiedExpression.class, implication.getRefinement().getExpression(),
102-
"Expected implication " + index + " to contain a SimplifiedExpression");
103-
return (SimplifiedExpression) implication.getRefinement().getExpression();
100+
public static SimplifiedPredicate simplifiedPredicate(VCImplication implication, int index) {
101+
assertInstanceOf(SimplifiedPredicate.class, implication.getRefinement(),
102+
"Expected implication " + index + " to contain a SimplifiedPredicate");
103+
return (SimplifiedPredicate) implication.getRefinement();
104104
}
105105

106-
private static String formatBinders(SimplifiedExpression expression) {
107-
return expression.getBinders().stream().map(binder -> binder.getName() + ":" + binder.getType())
106+
private static String formatBinders(SimplifiedPredicate predicate) {
107+
return predicate.getBinders().stream().map(binder -> binder.getName() + ":" + binder.getType())
108108
.collect(java.util.stream.Collectors.joining(", "));
109109
}
110110

111-
private static ExpectedSimplifiedExpression parseExpectedSimplifiedExpression(String expected) {
111+
private static ExpectedSimplifiedPredicate parseExpectedSimplifiedPredicate(String expected) {
112112
String binders = null;
113113
String expression = expected.trim();
114114
int binderStart = expression.lastIndexOf('[');
@@ -121,9 +121,9 @@ private static ExpectedSimplifiedExpression parseExpectedSimplifiedExpression(St
121121
String[] parts = expression.split("<-", 2);
122122
String simplified = parts[0].trim();
123123
String origin = parts.length > 1 ? parts[1].trim() : null;
124-
return new ExpectedSimplifiedExpression(simplified, origin, binders);
124+
return new ExpectedSimplifiedPredicate(simplified, origin, binders);
125125
}
126126

127-
public record ExpectedSimplifiedExpression(String simplified, String origin, String binders) {
127+
public record ExpectedSimplifiedPredicate(String simplified, String origin, String binders) {
128128
}
129129
}

0 commit comments

Comments
 (0)