Use DerivationNodes in Expected of Refinement Error

Author: rcosta358

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java

@@ -12,19 +12,19 @@
  */
 public class RefinementError extends LJError {
 
-    private final String expected;
+    private final ValDerivationNode expected;
     private final ValDerivationNode found;
 
-    public RefinementError(SourcePosition position, Expression expected, ValDerivationNode found,
+    public RefinementError(SourcePosition position, ValDerivationNode expected, ValDerivationNode found,
             TranslationTable translationTable) {
         super("Refinement Error",
-                String.format("%s is not a subtype of %s", found.getValue(), expected.toSimplifiedString()), position,
+                String.format("%s is not a subtype of %s", found.getValue(), expected.getValue()), position,
                 translationTable);
-        this.expected = expected.toSimplifiedString();
+        this.expected = expected;
         this.found = found;
     }
 
-    public String getExpected() {
+    public ValDerivationNode getExpected() {
         return expected;
     }
 

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java

@@ -51,7 +51,7 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
             premises = premisesBeforeChange.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f);
             et = expectedType.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f);
         } catch (Exception e) {
-            throw new RefinementError(element.getPosition(), expectedType.getExpression(), premises.simplify(), map);
+            throw new RefinementError(element.getPosition(), expectedType.simplify(), premises.simplify(), map);
         }
 
         try {
@@ -267,7 +267,7 @@ private TranslationTable createMap(Predicate expectedType) {
     protected void raiseError(Exception e, SourcePosition position, Predicate found, Predicate expected,
             TranslationTable map) throws LJError {
         if (e instanceof TypeCheckError) {
-            throw new RefinementError(position, expected.getExpression(), found.simplify(), map);
+            throw new RefinementError(position, expected.simplify(), found.simplify(), map);
         } else if (e instanceof liquidjava.smt.errors.NotFoundError nfe) {
             throw new NotFoundError(position, e.getMessage(), nfe.getName(), nfe.getKind(), map);
         } else {
@@ -288,7 +288,7 @@ protected void raiseSubtypingError(SourcePosition position, Predicate expected,
         gatherVariables(found, lrv, mainVars);
         TranslationTable map = new TranslationTable();
         Predicate premises = joinPredicates(expected, mainVars, lrv, map).toConjunctions();
-        throw new RefinementError(position, expected.getExpression(), premises.simplify(), map);
+        throw new RefinementError(position, expected.simplify(), premises.simplify(), map);
     }
 
     protected void raiseSameStateError(SourcePosition position, Predicate expected, String klass) throws LJError {