Try to achieve a better parser error message

[wadoon]

This PR removes the LL(*) fallback from the ParsingFacade to achieve better error message.

[codecov]

Codecov Report

All modified and coverable lines are covered by tests ✅

Comparison is base (1064b30) 37.72% compared to head (d9de961) 37.72%.

Additional details and impacted files

@@             Coverage Diff              @@
##               main    #3406      +/-   ##
============================================
- Coverage     37.72%   37.72%   -0.01%     
  Complexity    17017    17017              
============================================
  Files          2076     2076              
  Lines        126944   126939       -5     
  Branches      21379    21379              
============================================
- Hits          47891    47886       -5     
  Misses        73155    73155              
  Partials       5898     5898              

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[mattulbrich]

In your example the totally unclear SLL error message is still shown. Why? If the other is the "real" error message, can we restrict ourselves to it?

[wadoon]

In your example the totally unclear SLL error message is still shown. Why? If the other is the "real" error message, can we restrict ourselves to it?

It is not final as I did not understand much of ANTLR internals.

Error messages are now caught up in the ErrorStrategy, so e.g., I lose have the ANTLR error messages not available anymore.

[wadoon]

The main question is: Is the KeY grammar within SLL?
The internet says:

Strong LL Grammar (SLL):SLL grammars are a subset of LL(k) grammars, which are a more powerful class of grammars than CFGs.LL(k) grammars are capable of describing languages that are not context-free, as they can consider a limited amount of lookahead tokens (k tokens) to make parsing decisions based on context.SLL grammars are a strict subset of LL(k) grammars that are characterized by having a unique alternative for each production when the parser looks at the first k tokens of input.SLL parsers can be more efficient than general LL(k) parsers, but they are more restricted in the grammars they can parse.

I would guess so.

[mattulbrich]

Rosenkrantz,Stearns: Properties of deterministic top-down grammars

[wadoon]

SLL is sufficient for the KeY taclet base.

Should we just drop LL mode?

[wadoon]

KaKeY decision: Fallback to LL(*) will be removed.

[wadoon]

    @Override
    public Token recoverInline(Parser recognizer) throws RecognitionException {
        InputMismatchException e = new InputMismatchException(recognizer);
        for (ParserRuleContext context = recognizer.getContext(); context != null; context = context.getParent()) {
            context.exception = e;
        }
        var tok = e.getOffendingToken();

        var message = "I got offended by the token '%s'. Expected tokens are: %s".formatted(tok,
                e.getExpectedTokens().toString(recognizer.getVocabulary()));

        syntaxError(recognizer, e.getOffendingToken(),
                tok.getLine(), tok.getCharPositionInLine(), message, e);
        throw new ParseCancellationException(e);
    }

    @Override
    public void recover(Parser recognizer, RecognitionException e) throws RecognitionException {
        for (ParserRuleContext context = recognizer.getContext(); context != null; context = context.getParent()) {
            context.exception = e;
        }
        var tok = e.getOffendingToken();
        final var parseCancellationException = new ParseCancellationException(e);

        syntaxError(recognizer, e.getOffendingToken(),
                tok.getLine(), tok.getCharPositionInLine(), parseCancellationException.getMessage(), e);

        throw parseCancellationException;
    }

[wadoon]

closed in favor of hekeython2 approaches.