Error messages now show whether the error is in the Term or the Type Assumptions

This commit is contained in:
uogau 2021-07-02 16:46:01 +02:00
parent 7243719667
commit 6f2c6b3481
8 changed files with 92 additions and 36 deletions

View File

@ -90,7 +90,7 @@ public class LambdaLexer {
return new Result<>(t); return new Result<>(t);
} else { } else {
return new Result<>(null, ParseError.UNEXPECTED_CHARACTER return new Result<>(null, ParseError.UNEXPECTED_CHARACTER
.withCharacter(term.charAt(pos + 1), pos + 1, term)); .withCharacter(term.charAt(pos + 1), pos + 1, term, ParseError.ErrorType.TERM_ERROR));
} }
} else { } else {
return new Result<>(null, ParseError.TOO_FEW_TOKENS); // actually too few *characters* .. return new Result<>(null, ParseError.TOO_FEW_TOKENS); // actually too few *characters* ..
@ -135,7 +135,7 @@ public class LambdaLexer {
&& (int) term.charAt(pos) < 128); && (int) term.charAt(pos) < 128);
if (pos < term.length() && (int) term.charAt(pos) >= 128) { if (pos < term.length() && (int) term.charAt(pos) >= 128) {
return new Result<>(null, ParseError.UNEXPECTED_CHARACTER return new Result<>(null, ParseError.UNEXPECTED_CHARACTER
.withCharacter(term.charAt(pos), pos, term)); .withCharacter(term.charAt(pos), pos, term, ParseError.ErrorType.TERM_ERROR));
} }
String s = sb.toString(); String s = sb.toString();
TokenType type; TokenType type;
@ -167,7 +167,8 @@ public class LambdaLexer {
} while (pos < term.length() && Character.isDigit(term.charAt(pos))); } while (pos < term.length() && Character.isDigit(term.charAt(pos)));
return new Result<>(new Token(TokenType.NUMBER, sb.toString(), startPos)); return new Result<>(new Token(TokenType.NUMBER, sb.toString(), startPos));
} else { } else {
return new Result<>(null, ParseError.UNEXPECTED_CHARACTER.withCharacter(c, pos, term)); return new Result<>(null, ParseError.UNEXPECTED_CHARACTER.withCharacter(c, pos, term,
ParseError.ErrorType.TERM_ERROR));
} }
} }

View File

@ -69,7 +69,8 @@ public class LambdaParser {
TokenType current = token.getType(); TokenType current = token.getType();
Optional<ParseError> error = nextToken(); Optional<ParseError> error = nextToken();
if (current != type) { if (current != type) {
return Optional.of(ParseError.UNEXPECTED_TOKEN.withToken(lastToken, lexer.getTerm()).expectedType(type)); return Optional.of(ParseError.UNEXPECTED_TOKEN.withToken(lastToken, lexer.getTerm(),
ParseError.ErrorType.TERM_ERROR).expectedType(type));
} }
return error; return error;
} }
@ -91,7 +92,7 @@ public class LambdaParser {
} }
return new Result<>(null, return new Result<>(null,
(last.getType() == TokenType.EOF ? ParseError.TOO_FEW_TOKENS : ParseError.UNEXPECTED_TOKEN) (last.getType() == TokenType.EOF ? ParseError.TOO_FEW_TOKENS : ParseError.UNEXPECTED_TOKEN)
.withToken(last, lexer.getTerm()) .withToken(last, lexer.getTerm(), ParseError.ErrorType.TERM_ERROR)
.expectedTypes(ATOM_START_TOKENS)); .expectedTypes(ATOM_START_TOKENS));
} }
@ -207,7 +208,8 @@ public class LambdaParser {
try { try {
n = Integer.parseInt(number); n = Integer.parseInt(number);
} catch (NumberFormatException e) { } catch (NumberFormatException e) {
return new Result<>(null, ParseError.UNEXPECTED_CHARACTER.withToken(token, lexer.getTerm())); return new Result<>(null, ParseError.UNEXPECTED_CHARACTER.withToken(
token, lexer.getTerm(), ParseError.ErrorType.TERM_ERROR));
} }
error = nextToken(); error = nextToken();
if (error.isEmpty()) { if (error.isEmpty()) {

View File

@ -27,12 +27,30 @@ public enum ParseError {
*/ */
UNEXPECTED_CHARACTER; UNEXPECTED_CHARACTER;
public enum ErrorType {
/**
* This error was created when parsing the input term
*/
TERM_ERROR,
/**
* This error was created when parsing the type assumptions
*/
TYPE_ASSUMPTION_ERROR,
/**
* initial error type
*/
INITIAL_ERROR
}
private Optional<Token> cause = Optional.empty(); private Optional<Token> cause = Optional.empty();
private Optional<Collection<Token.TokenType>> needed = Optional.empty(); private Optional<Collection<Token.TokenType>> needed = Optional.empty();
private String term = ""; private String term = "";
private char wrongChar = '\0'; private char wrongChar = '\0';
private char correctChar = '\0'; private char correctChar = '\0';
private int position = -1; private int position = -1;
private ErrorType errorType = ErrorType.INITIAL_ERROR;
/** /**
* Attach a token to this error. * Attach a token to this error.
@ -41,9 +59,10 @@ public enum ParseError {
* @param term the term that is parsed * @param term the term that is parsed
* @return this object * @return this object
*/ */
public ParseError withToken(Token cause, String term) { public ParseError withToken(Token cause, String term, ErrorType errorType) {
this.cause = Optional.of(cause); this.cause = Optional.of(cause);
this.term = term; this.term = term;
this.errorType = errorType;
return this; return this;
} }
@ -88,10 +107,11 @@ public enum ParseError {
* @param term the term that is parsed * @param term the term that is parsed
* @return this object * @return this object
*/ */
public ParseError withCharacter(char cause, int position, String term) { public ParseError withCharacter(char cause, int position, String term, ErrorType errorType) {
this.wrongChar = cause; this.wrongChar = cause;
this.position = position; this.position = position;
this.term = term; this.term = term;
this.errorType = errorType;
return this; return this;
} }
@ -137,6 +157,17 @@ public enum ParseError {
return term; return term;
} }
/**
* @return the error type
*/
public ErrorType getErrorType() {
return errorType;
}
protected void setErrorType(ErrorType errorType) {
this.errorType = errorType;
}
ParseError() { ParseError() {
} }

View File

@ -37,7 +37,8 @@ public class TypeAssumptionParser {
Matcher matcher = NEGATED_TYPE_NAME_PATTERN.matcher(typeName); Matcher matcher = NEGATED_TYPE_NAME_PATTERN.matcher(typeName);
if (matcher.find()) { if (matcher.find()) {
return new Result<>(null, ParseError.UNEXPECTED_CHARACTER.withCharacter( return new Result<>(null, ParseError.UNEXPECTED_CHARACTER.withCharacter(
typeName.charAt(matcher.start()), matcher.start(), typeName)); typeName.charAt(matcher.start()), matcher.start(), typeName,
ParseError.ErrorType.TYPE_ASSUMPTION_ERROR));
} }
} }
VarTerm var = new VarTerm(typeName); VarTerm var = new VarTerm(typeName);
@ -64,20 +65,22 @@ public class TypeAssumptionParser {
int colonIndex = definition.indexOf(':'); int colonIndex = definition.indexOf(':');
if (colonIndex >= 0) { if (colonIndex >= 0) {
return new Result<>(null, ParseError.UNEXPECTED_CHARACTER.withCharacter( return new Result<>(null, ParseError.UNEXPECTED_CHARACTER.withCharacter(
':', colonIndex, definition).expectedCharacter('.') ':', colonIndex, definition, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR)
.expectedCharacter('.')
); );
} }
return new Result<>(null, ParseError.TOO_FEW_TOKENS.expectedType(TokenType.DOT)); return new Result<>(null, ParseError.TOO_FEW_TOKENS.expectedType(TokenType.DOT));
} else if (parts.length > 2) { } else if (parts.length > 2) {
return new Result<>(null, ParseError.UNEXPECTED_CHARACTER.withCharacter( return new Result<>(null, ParseError.UNEXPECTED_CHARACTER.withCharacter(
'.', parts[0].length() + 1 + parts[1].length(), definition)); '.', parts[0].length() + 1 + parts[1].length(),
definition, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR));
} }
for (String quantified : parts[0].substring(1).split(",")) { for (String quantified : parts[0].substring(1).split(",")) {
quantified = quantified.trim(); quantified = quantified.trim();
if (!quantified.matches("t\\d+")) { if (!quantified.matches("t\\d+")) {
return new Result<>(null, ParseError.UNEXPECTED_TOKEN.withToken( return new Result<>(null, ParseError.UNEXPECTED_TOKEN.withToken(
new Token(TokenType.VARIABLE, quantified, parts[0].indexOf(quantified)), parts[0] new Token(TokenType.VARIABLE, quantified, parts[0].indexOf(quantified)),
)); parts[0], ParseError.ErrorType.TYPE_ASSUMPTION_ERROR));
} }
int i = Integer.parseInt(quantified.substring(1)); int i = Integer.parseInt(quantified.substring(1));
allQuantified.add(new TypeVariable(TypeVariableKind.USER_INPUT, i)); allQuantified.add(new TypeVariable(TypeVariableKind.USER_INPUT, i));
@ -117,6 +120,7 @@ public class TypeAssumptionParser {
while (true) { while (true) {
Result<Token, ParseError> token = lexer.nextToken(); Result<Token, ParseError> token = lexer.nextToken();
if (token.isError()) { if (token.isError()) {
token.unwrapError().setErrorType(ParseError.ErrorType.TYPE_ASSUMPTION_ERROR);
return new Result<>(token); return new Result<>(token);
} }
Token t = token.unwrap(); Token t = token.unwrap();
@ -138,7 +142,8 @@ public class TypeAssumptionParser {
case ARROW: case ARROW:
if (type == null) { if (type == null) {
// there was no type in front of the arrow // there was no type in front of the arrow
return new Result<>(null, ParseError.UNEXPECTED_TOKEN.withToken(t, lexer.getTerm())); return new Result<>(null, ParseError.UNEXPECTED_TOKEN.withToken(
t, lexer.getTerm(), ParseError.ErrorType.TYPE_ASSUMPTION_ERROR));
} }
// recursive call, keep open parentheses count // recursive call, keep open parentheses count
Result<Pair<Type, Integer>, ParseError> nextType = parseType(lexer, parenCount); Result<Pair<Type, Integer>, ParseError> nextType = parseType(lexer, parenCount);
@ -149,7 +154,8 @@ public class TypeAssumptionParser {
case EOF: case EOF:
break; break;
default: default:
return new Result<>(null, ParseError.UNEXPECTED_TOKEN.withToken(t, lexer.getTerm())); return new Result<>(null, ParseError.UNEXPECTED_TOKEN.withToken(
t, lexer.getTerm(), ParseError.ErrorType.TYPE_ASSUMPTION_ERROR));
} }
// update type based on Result // update type based on Result
if (typeResult != null && typeResult.isError()) { if (typeResult != null && typeResult.isError()) {
@ -163,7 +169,8 @@ public class TypeAssumptionParser {
} }
if (parenCount - removedParens < 0) { if (parenCount - removedParens < 0) {
// too many closing parenthesis // too many closing parenthesis
return new Result<>(null, ParseError.UNEXPECTED_TOKEN.withToken(t, lexer.getTerm())); return new Result<>(null, ParseError.UNEXPECTED_TOKEN.withToken(
t, lexer.getTerm(), ParseError.ErrorType.TYPE_ASSUMPTION_ERROR));
} else if (END_TOKENS.contains(t.getType())) { } else if (END_TOKENS.contains(t.getType())) {
// potential end of type // potential end of type
if (parenCount - removedParens == 0) { if (parenCount - removedParens == 0) {

View File

@ -53,27 +53,36 @@ public class ErrorView extends VerticalLayout implements LocaleChangeObserver {
Paragraph summary = new Paragraph(getTranslation("root." + error.toString())); Paragraph summary = new Paragraph(getTranslation("root." + error.toString()));
summary.setId(ERROR_SUMMARY_ID); summary.setId(ERROR_SUMMARY_ID);
String term = error.getTerm(); String term = error.getTerm();
String descriptionForError;
ParseError.ErrorType errorType = error.getErrorType();
if (errorType == ParseError.ErrorType.TERM_ERROR) {
descriptionForError = "error.termForError";
} else if (errorType == ParseError.ErrorType.TYPE_ASSUMPTION_ERROR) {
descriptionForError = "error.typeAssumptionForError";
} else {
//should never happen
descriptionForError = "error";
}
switch (error) { switch (error) {
case TOO_FEW_TOKENS: case TOO_FEW_TOKENS:
additionalInformation.add(new Span(getTranslation("root.tooFewTokensHelp"))); additionalInformation.add(new Span(getTranslation("error.tooFewTokensHelp")));
break; break;
case UNEXPECTED_TOKEN: case UNEXPECTED_TOKEN:
Optional<Token> cause = error.getCause(); Optional<Token> cause = error.getCause();
if (cause.isPresent()) { if (cause.isPresent()) {
additionalInformation.add(new Span(new Pre(getTranslation("root.termForError") + term additionalInformation.add(new Span(new Pre(getTranslation(descriptionForError) + term
+ "\n" + " ".repeat(Math.max(getTranslation("root.termForError").length(), + "\n" + " ".repeat(Math.max(getTranslation(descriptionForError).length(),
cause.get().getPos() + getTranslation("root.termForError").length())) cause.get().getPos() + getTranslation(descriptionForError).length()))
+ "^ " + getTranslation("root.wrongCharacter") + cause.get().getText()))); + "^ " + getTranslation("error.wrongCharacter") + cause.get().getText())));
} }
break; break;
case UNEXPECTED_CHARACTER: case UNEXPECTED_CHARACTER:
char c = error.getWrongCharacter(); char c = error.getWrongCharacter();
if (c != '\0') { if (c != '\0') {
additionalInformation.add(new Span(new Pre(getTranslation("root.termForError") + term additionalInformation.add(new Span(new Pre(getTranslation(descriptionForError) + term
+ "\n" + " ".repeat(Math.max(getTranslation("root.termForError").length(), + "\n" + " ".repeat(Math.max(getTranslation(descriptionForError).length(),
error.getPosition() + getTranslation("root.termForError").length())) error.getPosition() + getTranslation(descriptionForError).length()))
+ "^ " + getTranslation("root.wrongCharacter") + c))); + "^ " + getTranslation("error.wrongCharacter") + c)));
} else { } else {
return summary; return summary;
} }

View File

@ -101,12 +101,13 @@ help.typicalcInfo=\
Johanna Stuber<br> Johanna Stuber<br>
root.TOO_FEW_TOKENS=Falsche Eingabe! Die Eingabe endet abrupt. root.TOO_FEW_TOKENS=Falsche Eingabe! Die Eingabe endet abrupt.
root.tooFewTokensHelp=Überprüfe, ob alle Let-, Abs- und App-Terme über die nötigen Argumente verfügen. error.tooFewTokensHelp=Überprüfe, ob alle Let-, Abs- und App-Terme über die nötigen Argumente verfügen.
root.UNEXPECTED_TOKEN=Die Eingabe entspricht nicht der im Info-Dialog spezifizierten Syntax! root.UNEXPECTED_TOKEN=Die Eingabe entspricht nicht der im Info-Dialog spezifizierten Syntax!
root.UNEXPECTED_CHARACTER=Die Eingabe enthält ein Zeichen, welches an dieser Stelle nicht erlaubt ist! root.UNEXPECTED_CHARACTER=Die Eingabe enthält ein Zeichen, welches an dieser Stelle nicht erlaubt ist!
error.heading=Syntaktisch falsche Eingabe! error.heading=Syntaktisch falsche Eingabe!
root.termForError=Term:\u0020 error.termForError=Term:\u0020
root.wrongCharacter=Falsches Zeichen:\u0020 error.typeAssumptionForError=Typannahme:\u0020
error.wrongCharacter=Falsches Zeichen:\u0020
error.expectedToken=Erwartet: {0} error.expectedToken=Erwartet: {0}
error.hint=Die Grammatiken, die die korrekte Syntax eines Terms und der Typannahmen beschreiben, \ error.hint=Die Grammatiken, die die korrekte Syntax eines Terms und der Typannahmen beschreiben, \
sind auch über das Info-Symbol zu erreichen. sind auch über das Info-Symbol zu erreichen.

View File

@ -94,12 +94,13 @@ help.typicalcInfo=\
Johanna Stuber Johanna Stuber
root.TOO_FEW_TOKENS=Wrong input! The term ends abruptly. root.TOO_FEW_TOKENS=Wrong input! The term ends abruptly.
root.tooFewTokensHelp=Check if all let, abstraction and application terms consist of the required arguments. error.tooFewTokensHelp=Check if all let, abstraction and application terms consist of the required arguments.
root.UNEXPECTED_TOKEN=The input does not match the syntax specified in the info dialog. root.UNEXPECTED_TOKEN=The input does not match the syntax specified in the info dialog.
root.UNEXPECTED_CHARACTER=The input contains a character which is not allowed at this position. root.UNEXPECTED_CHARACTER=The input contains a character which is not allowed at this position.
error.heading=Input is syntactically wrong! error.heading=Input is syntactically wrong!
root.wrongCharacter=Wrong character:\u0020 error.wrongCharacter=Wrong character:\u0020
root.termForError=Term:\u0020 error.termForError=Term:\u0020
error.typeAssumptionForError=Type Assumption:\u0020
error.expectedToken=Expected: {0} error.expectedToken=Expected: {0}
error.hint=The grammars describing the correct syntax of a term or a type assumption can also be reached \ error.hint=The grammars describing the correct syntax of a term or a type assumption can also be reached \
via the info icon. via the info icon.

View File

@ -233,11 +233,15 @@ class TypeAssumptionParserTest {
tests.put("", ParseError.TOO_FEW_TOKENS); tests.put("", ParseError.TOO_FEW_TOKENS);
tests.put("ö", ParseError.UNEXPECTED_CHARACTER); tests.put("ö", ParseError.UNEXPECTED_CHARACTER);
tests.put("(x", ParseError.TOO_FEW_TOKENS); tests.put("(x", ParseError.TOO_FEW_TOKENS);
tests.put("-> x", ParseError.UNEXPECTED_TOKEN.withToken(new Token(Token.TokenType.ARROW, "->", 0), "")); tests.put("-> x", ParseError.UNEXPECTED_TOKEN.withToken(new Token(Token.TokenType.ARROW, "->", 0),
tests.put("x 11", ParseError.UNEXPECTED_TOKEN.withToken(new Token(Token.TokenType.NUMBER, "11", 2), "")); "", ParseError.ErrorType.TYPE_ASSUMPTION_ERROR));
tests.put("x )", ParseError.UNEXPECTED_TOKEN.withToken(new Token(Token.TokenType.RIGHT_PARENTHESIS, ")", 2), "")); tests.put("x 11", ParseError.UNEXPECTED_TOKEN.withToken(new Token(Token.TokenType.NUMBER, "11", 2),
"", ParseError.ErrorType.TYPE_ASSUMPTION_ERROR));
tests.put("x )", ParseError.UNEXPECTED_TOKEN.withToken(new Token(Token.TokenType.RIGHT_PARENTHESIS, ")",
2), "", ParseError.ErrorType.TYPE_ASSUMPTION_ERROR));
tests.put("x -> (x) )", ParseError.UNEXPECTED_TOKEN tests.put("x -> (x) )", ParseError.UNEXPECTED_TOKEN
.withToken(new Token(Token.TokenType.RIGHT_PARENTHESIS, ")", 9), "")); .withToken(new Token(Token.TokenType.RIGHT_PARENTHESIS, ")", 9), "",
ParseError.ErrorType.TYPE_ASSUMPTION_ERROR));
for (Map.Entry<String, ParseError> entry : tests.entrySet()) { for (Map.Entry<String, ParseError> entry : tests.entrySet()) {
TypeAssumptionParser parser = new TypeAssumptionParser(); TypeAssumptionParser parser = new TypeAssumptionParser();
Result<Map<VarTerm, TypeAbstraction>, ParseError> type = parser.parse(Map.of("type1", entry.getKey())); Result<Map<VarTerm, TypeAbstraction>, ParseError> type = parser.parse(Map.of("type1", entry.getKey()));