Add hint for implies (using --> and not ->)

liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariablePropagation.java

@@ -23,7 +23,7 @@ public class VariablePropagation {
      */
     public static ValDerivationNode propagate(Expression exp, ValDerivationNode previousOrigin) {
         Map<String, Expression> substitutions = VariableResolver.resolve(exp);
-        Map<String, Expression> directSubstitutions = new HashMap<>(); // var == literal or var == var 
+        Map<String, Expression> directSubstitutions = new HashMap<>(); // var == literal or var == var
         Map<String, Expression> expressionSubstitutions = new HashMap<>(); // var == expression
         for (Map.Entry<String, Expression> entry : substitutions.entrySet()) {
             Expression value = entry.getValue();

liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RJErrorListener.java

@@ -8,13 +8,15 @@
 import org.antlr.v4.runtime.Parser;
 import org.antlr.v4.runtime.RecognitionException;
 import org.antlr.v4.runtime.Recognizer;
+import org.antlr.v4.runtime.Token;
 import org.antlr.v4.runtime.atn.ATNConfigSet;
 import org.antlr.v4.runtime.dfa.DFA;
 
 public class RJErrorListener implements ANTLRErrorListener {
 
     private int errors;
     public List<String> msgs;
+    private String hint;
 
     public RJErrorListener() {
         super();
@@ -25,16 +27,30 @@ public RJErrorListener() {
     @Override
     public void syntaxError(Recognizer<?, ?> recognizer, Object offendingSymbol, int line, int charPositionInLine,
             String msg, RecognitionException e) {
-        // Hint for == instead of =
-        String hint = null;
-        if (e instanceof LexerNoViableAltException l) {
-            char c = l.getInputStream().toString().charAt(charPositionInLine);
-            if (c == '=')
-                hint = "Predicates must be compared with == instead of =";
+        if (hint == null) {
+            String input = inputFor(offendingSymbol, e);
+            int pos = charPositionInLine;
+            if (input != null && pos >= 0 && pos < input.length()) {
+                char c = input.charAt(pos);
+                // Hint for == instead of =
+                if (c == '=')
+                    hint = "Predicates must be compared with == instead of =";
+                // Hint for -> instead of --> (logical implication)
+                else if (c == '>' && pos >= 1 && input.charAt(pos - 1) == '-'
+                        && (pos < 2 || input.charAt(pos - 2) != '-'))
+                    hint = "Logical implication is --> (two dashes), not ->";
+            }
         }
         errors++;
-        String ms = "Error in " + msg + ", in the position " + charPositionInLine;
-        msgs.add(ms + (hint == null ? "" : "\n\tHint: " + hint));
+        msgs.add("Error in " + msg + ", in the position " + charPositionInLine);
+    }
+
+    private static String inputFor(Object offendingSymbol, RecognitionException e) {
+        if (e instanceof LexerNoViableAltException l)
+            return l.getInputStream().toString();
+        if (offendingSymbol instanceof Token t && t.getInputStream() != null)
+            return t.getInputStream().toString();
+        return null;
     }
 
     @Override
@@ -56,6 +72,10 @@ public int getErrors() {
         return errors;
     }
 
+    public String getHint() {
+        return hint;
+    }
+
     public String getMessages() {
         StringBuilder sb = new StringBuilder();
         String pl = errors == 1 ? "" : "s";

liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RefinementsParser.java

@@ -1,7 +1,5 @@
 package liquidjava.rj_language.parsing;
 
-import java.util.Optional;
-
 import liquidjava.diagnostics.errors.SyntaxError;
 import liquidjava.processor.facade.AliasDTO;
 import liquidjava.processor.facade.GhostDTO;
@@ -56,25 +54,14 @@ public static AliasDTO parseAliasDefinition(String toParse) throws SyntaxError {
      * Compiles the given string into a parse tree
      */
     private static ParseTree compile(String toParse, String errorMessage) throws SyntaxError {
-        Optional<String> s = getErrors(toParse);
-        if (s.isPresent())
-            throw new SyntaxError(errorMessage, toParse);
-
-        RJErrorListener err = new RJErrorListener();
-        RJParser parser = createParser(toParse, err);
-        return parser.prog();
-    }
-
-    /**
-     * Checks if the given string can be parsed without syntax errors, returning the error messages if any
-     */
-    private static Optional<String> getErrors(String toParse) {
         RJErrorListener err = new RJErrorListener();
-        RJParser parser = createParser(toParse, err);
-        parser.prog(); // all consumed
-        if (err.getErrors() > 0)
-            return Optional.of(err.getMessages());
-        return Optional.empty();
+        ParseTree tree = createParser(toParse, err).prog();
+        if (err.getErrors() > 0) {
+            SyntaxError e = new SyntaxError(errorMessage, toParse);
+            e.setHint(err.getHint());
+            throw e;
+        }
+        return tree;
     }
 
     /**

liquidjava-verifier/src/test/java/liquidjava/rj_language/parsing/RefinementsParserTest.java

@@ -0,0 +1,36 @@
+package liquidjava.rj_language.parsing;
+
+import static org.junit.jupiter.api.Assertions.assertEquals;
+import static org.junit.jupiter.api.Assertions.assertThrows;
+
+import org.junit.jupiter.api.Test;
+
+import liquidjava.diagnostics.errors.SyntaxError;
+
+class RefinementsParserTest {
+
+    @Test
+    void hintsArrowVsImplication() {
+        SyntaxError e = assertThrows(SyntaxError.class,
+                () -> RefinementsParser.createAST("_ == true -> markSupported(this)", ""));
+        assertEquals("Logical implication is --> (two dashes), not ->", e.getDetails());
+    }
+
+    @Test
+    void hintsAssignVsEquals() {
+        SyntaxError e = assertThrows(SyntaxError.class, () -> RefinementsParser.createAST("_ = 1", ""));
+        assertEquals("Predicates must be compared with == instead of =", e.getDetails());
+    }
+
+    @Test
+    void noHintForValidImplication() {
+        // double-dash is the real operator — should parse cleanly, no exception
+        RefinementsParser.createAST("_ == true --> markSupported(this)", "");
+    }
+
+    @Test
+    void noHintForUnrelatedSyntaxError() {
+        SyntaxError e = assertThrows(SyntaxError.class, () -> RefinementsParser.createAST("a +", ""));
+        assertEquals("", e.getDetails());
+    }
+}