Add Counterexamples (#60)

Author: rcosta358

client/server/language-server-liquidjava.jar

@@ -68,6 +68,7 @@ export type RefinementError = BaseDiagnostic & {
     expected: ValDerivationNode;
     found: ValDerivationNode;
     customMessage: string;
+    counterexample: string;
 }
 
 export type StateConflictError = BaseDiagnostic & {

client/src/types/diagnostics.ts

@@ -33,6 +33,7 @@ const errorContentRenderers: Partial<Record<LJError['type'], (error: LJError) =>
         ${e.customMessage ? renderSection('Message', e.customMessage) : ''}
         ${renderSection('Expected', e.expected.value)}
         ${renderCustomSection('Found', renderDerivationNode(e, e.found))}
+        ${e.counterexample ? renderSection('Counterexample', e.counterexample) : ''}
     `,
     'state-refinement-error': (e: StateRefinementError) => /*html*/`
         ${e.customMessage ? renderSection('Message', e.customMessage) : ''}

client/src/webview/views/verification/errors.ts

@@ -179,7 +179,7 @@
 		<dependency>
 			<groupId>io.github.liquid-java</groupId>
 			<artifactId>liquidjava-verifier</artifactId>
-			<version>0.0.12</version>
+			<version>0.0.14</version>
 		</dependency>
 		<dependency>
 			<groupId>tools.aqua</groupId>

server/pom.xml

@@ -9,10 +9,10 @@
  * DTO for serializing RefinementError instances to JSON
  */
 public record RefinementErrorDTO(String category, String type, String title, String message, String file, ErrorPosition position,
-        TranslationTableDTO translationTable, ValDerivationNode expected, ValDerivationNode found, String customMessage) {
+        TranslationTableDTO translationTable, ValDerivationNode expected, ValDerivationNode found, String customMessage, String counterexample) {
 
     public static RefinementErrorDTO from(RefinementError error) {
         return new RefinementErrorDTO("error", "refinement-error", error.getTitle(), error.getMessage(), error.getFile(),
-                error.getPosition(), TranslationTableDTO.from(error.getTranslationTable()), error.getExpected(), error.getFound(), error.getCustomMessage());
+                error.getPosition(), TranslationTableDTO.from(error.getTranslationTable()), error.getExpected(), error.getFound(), error.getCustomMessage(), error.getCounterExampleString());
     }
 }