Repository navigation
Add Constant Propagation And Folding To Predicates #58
Description
Why
Adding constant propagation and constant folding to predicates would greatly simplify the error messages in many cases.
Example
public class Example {
public static void handleNegative(@Refinement("x < 0") int x) {}
public static void example() {
int a = 6;
int b = 2;
int result = a / b;
handleNegative(result);
}
}Current error message:
Type expected: (#result_4 < 0)
Refinement found: #result_4 == #a_2 / #b_3 && #a_2 == #a_0 && #a_0 == 6 && #b_3 == #b_1 && #b_1 == 2
Intended error message:
Type expected: (#result_4 < 0)
Refinement found: #result_4 == 3
So, the variables a and b should be propagated with their constant values to 6 / 2 and then this should be folded to 3.
This should also work for booleans, e.g. !true => false.
Activity
alcides commentedon Sep 28, 2025
One point that might influence how you architect this change:
In the future we might want the IDE to be able to expand 3 to 6 / 2 and the 6 and 2 to their variables, respectively. So the IDE should provide either HTML or JSON (json sounds better) that includes all of these contractions, so it can revert them when requested by the user.
In practice, this means that either:
rcosta358 commentedon Sep 28, 2025
Noted!