Add Constant Propagation And Folding To Predicates

[rcosta358]

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.

[alcides]

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:

• each new AST node contains a reference to the original, or
• there is a datastructure with a mapping between the new and original nodes, or
• a better alternative that I can't think of.

[rcosta358]

Noted!