Merge remote-tracking branch 'origin/master'

This commit is contained in:
Arne Keller 2021-07-05 12:28:45 +02:00
commit c28576175a
8 changed files with 110 additions and 47 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* ..
@ -148,7 +148,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;
@ -180,7 +180,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(), term, startPos)); return new Result<>(new Token(TokenType.NUMBER, sb.toString(), term, 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).expectedType(type)); return Optional.of(ParseError.UNEXPECTED_TOKEN.withToken(lastToken,
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) .withToken(last, 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)); return new Result<>(null, ParseError.UNEXPECTED_CHARACTER.withToken(
token, ParseError.ErrorType.TERM_ERROR));
} }
error = nextToken(); error = nextToken();
if (error.isEmpty()) { if (error.isEmpty()) {

View File

@ -30,6 +30,23 @@ 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 Optional<ExpectedInput> expected = Optional.empty(); private Optional<ExpectedInput> expected = Optional.empty();
@ -37,6 +54,7 @@ public enum ParseError {
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.
@ -44,10 +62,11 @@ public enum ParseError {
* @param cause the token that caused the error * @param cause the token that caused the error
* @return this object * @return this object
*/ */
public ParseError withToken(Token cause) { public ParseError withToken(Token cause, ErrorType errorType) {
this.cause = Optional.of(cause); this.cause = Optional.of(cause);
this.term = cause.getSourceText(); this.term = cause.getSourceText();
this.position = cause.getPos(); this.position = cause.getPos();
this.errorType = errorType;
return this; return this;
} }
@ -108,10 +127,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;
} }
@ -157,6 +177,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

@ -143,7 +143,8 @@ public class TypeAssumptionParser {
case EOF: case EOF:
return new ParserResult<>(alreadyParsed); return new ParserResult<>(alreadyParsed);
default: default:
return new ParserResult<>(ParseError.UNEXPECTED_TOKEN.withToken(t)); return new ParserResult<>(ParseError.UNEXPECTED_TOKEN
.withToken(t, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR));
} }
} }
} }
@ -162,7 +163,8 @@ public class TypeAssumptionParser {
case COLON: case COLON:
return new ParserResult<>(new ExpectingTypeDef(alreadyParsed, var)); return new ParserResult<>(new ExpectingTypeDef(alreadyParsed, var));
default: default:
return new ParserResult<>(ParseError.UNEXPECTED_TOKEN.withToken(t)); return new ParserResult<>(ParseError.UNEXPECTED_TOKEN
.withToken(t, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR));
} }
} }
} }
@ -191,7 +193,8 @@ public class TypeAssumptionParser {
if (typeVariables.isEmpty()) { if (typeVariables.isEmpty()) {
return new ParserResult<>(new ExpectingTypeVariables(alreadyParsed, var)); return new ParserResult<>(new ExpectingTypeVariables(alreadyParsed, var));
} else { } else {
return new ParserResult<>(ParseError.UNEXPECTED_TOKEN.withToken(t)); return new ParserResult<>(ParseError.UNEXPECTED_TOKEN
.withToken(t, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR));
} }
default: default:
if (state.isPresent()) { if (state.isPresent()) {
@ -235,7 +238,8 @@ public class TypeAssumptionParser {
case COMMA: case COMMA:
return new ParserResult<>(new InitialState(alreadyParsed)); return new ParserResult<>(new InitialState(alreadyParsed));
default: default:
return new ParserResult<>(ParseError.UNEXPECTED_TOKEN.withToken(t)); return new ParserResult<>(ParseError.UNEXPECTED_TOKEN
.withToken(t, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR));
} }
} }
} }
@ -261,7 +265,8 @@ public class TypeAssumptionParser {
return handleInnerParenthesis(t); return handleInnerParenthesis(t);
} }
if (parsedType.isPresent()) { if (parsedType.isPresent()) {
return new ParserResult<>(ParseError.UNEXPECTED_TOKEN.withToken(t)); return new ParserResult<>(ParseError.UNEXPECTED_TOKEN
.withToken(t, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR));
} }
Type type = parseLiteral(t.getText()); Type type = parseLiteral(t.getText());
// try parsing function type (see below) // try parsing function type (see below)
@ -275,7 +280,8 @@ public class TypeAssumptionParser {
return handleInnerParenthesis(t); return handleInnerParenthesis(t);
} }
if (parsedType.isEmpty()) { if (parsedType.isEmpty()) {
return new ParserResult<>(ParseError.UNEXPECTED_TOKEN.withToken(t)); return new ParserResult<>(ParseError.UNEXPECTED_TOKEN
.withToken(t, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR));
} }
// parse function type // parse function type
state = Optional.of(new ParseTypeStateExpectArrow().handle(t).getState()); state = Optional.of(new ParseTypeStateExpectArrow().handle(t).getState());
@ -314,7 +320,8 @@ public class TypeAssumptionParser {
if (parsedType.isPresent()) { if (parsedType.isPresent()) {
return new ParserResult<>(this); // parenthesized part may be start of function return new ParserResult<>(this); // parenthesized part may be start of function
} }
return new ParserResult<>(ParseError.UNEXPECTED_TOKEN.withToken(t)); return new ParserResult<>(ParseError.UNEXPECTED_TOKEN
.withToken(t, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR));
case COMMA: case COMMA:
case EOF: case EOF:
if (state.isPresent()) { if (state.isPresent()) {
@ -326,12 +333,14 @@ public class TypeAssumptionParser {
if (parsedType.isPresent() && openParens == parenthesisInitial) { if (parsedType.isPresent() && openParens == parenthesisInitial) {
return new ParserResult<>(parsedType.get()).attachToken(t); return new ParserResult<>(parsedType.get()).attachToken(t);
} }
return new ParserResult<>(ParseError.UNEXPECTED_TOKEN.withToken(t)); return new ParserResult<>(ParseError.UNEXPECTED_TOKEN
.withToken(t, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR));
default: default:
if (state.isPresent()) { if (state.isPresent()) {
return handleInner(t); return handleInner(t);
} }
return new ParserResult<>(ParseError.UNEXPECTED_TOKEN.withToken(t)); return new ParserResult<>(ParseError.UNEXPECTED_TOKEN
.withToken(t, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR));
} }
} }
@ -400,7 +409,8 @@ public class TypeAssumptionParser {
return new ParserResult<>(this); return new ParserResult<>(this);
} }
} else { } else {
return new ParserResult<>(ParseError.UNEXPECTED_TOKEN.withToken(t)); return new ParserResult<>(ParseError.UNEXPECTED_TOKEN
.withToken(t, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR));
} }
} }
} }
@ -422,13 +432,13 @@ public class TypeAssumptionParser {
case VARIABLE: case VARIABLE:
if (expectCommaOrDot) { if (expectCommaOrDot) {
return new ParserResult<>(ParseError.UNEXPECTED_TOKEN return new ParserResult<>(ParseError.UNEXPECTED_TOKEN
.withToken(t) .withToken(t, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR)
.expectedTypes(List.of(TokenType.COMMA, Token.TokenType.DOT))); .expectedTypes(List.of(TokenType.COMMA, Token.TokenType.DOT)));
} }
String input = t.getText(); String input = t.getText();
if (!TYPE_VARIABLE_PATTERN.matcher(input).matches()) { if (!TYPE_VARIABLE_PATTERN.matcher(input).matches()) {
return new ParserResult<>(ParseError.UNEXPECTED_TOKEN.withToken(t)); return new ParserResult<>(ParseError.UNEXPECTED_TOKEN
// TODO: somehow convey the expected format .withToken(t, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR));
} }
int i = Integer.parseInt(input.substring(1)); int i = Integer.parseInt(input.substring(1));
variables.add(new TypeVariable(TypeVariableKind.USER_INPUT, i)); variables.add(new TypeVariable(TypeVariableKind.USER_INPUT, i));
@ -440,7 +450,7 @@ public class TypeAssumptionParser {
return new ParserResult<>(this); return new ParserResult<>(this);
} else { } else {
return new ParserResult<>(ParseError.UNEXPECTED_TOKEN return new ParserResult<>(ParseError.UNEXPECTED_TOKEN
.withToken(t) .withToken(t, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR)
.expectedType(TokenType.VARIABLE)); .expectedType(TokenType.VARIABLE));
} }
case DOT: case DOT:
@ -450,15 +460,17 @@ public class TypeAssumptionParser {
return new ParserResult<>(new ExpectingTypeDef(alreadyParsed, variables, var)); return new ParserResult<>(new ExpectingTypeDef(alreadyParsed, variables, var));
} else { } else {
return new ParserResult<>(ParseError.UNEXPECTED_TOKEN return new ParserResult<>(ParseError.UNEXPECTED_TOKEN
.withToken(t) .withToken(t, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR)
.expectedType(TokenType.VARIABLE)); .expectedType(TokenType.VARIABLE));
} }
default: default:
if (expectCommaOrDot) { if (expectCommaOrDot) {
return new ParserResult<>(ParseError.UNEXPECTED_TOKEN.withToken(t) return new ParserResult<>(ParseError.UNEXPECTED_TOKEN
.withToken(t, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR)
.expectedTypes(List.of(TokenType.COMMA, TokenType.DOT))); .expectedTypes(List.of(TokenType.COMMA, TokenType.DOT)));
} }
return new ParserResult<>(ParseError.UNEXPECTED_TOKEN.withToken(t)); return new ParserResult<>(ParseError.UNEXPECTED_TOKEN
.withToken(t, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR));
} }
} }
} }

View File

@ -54,27 +54,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

@ -232,17 +232,23 @@ class TypeAssumptionParserTest {
void errors() { void errors() {
Map<String, ParseError> tests = new HashMap<>(); Map<String, ParseError> tests = new HashMap<>();
tests.put("", tests.put("",
ParseError.UNEXPECTED_TOKEN.withToken(new Token(Token.TokenType.EOF, "", "", 0))); ParseError.UNEXPECTED_TOKEN.withToken(new Token(Token.TokenType.EOF, "", "", 0),
ParseError.ErrorType.TYPE_ASSUMPTION_ERROR));
tests.put("ö", ParseError.UNEXPECTED_CHARACTER); tests.put("ö", ParseError.UNEXPECTED_CHARACTER);
tests.put("(x", tests.put("(x",
ParseError.UNEXPECTED_TOKEN.withToken(new Token(Token.TokenType.EOF, "", "(x", 2))); ParseError.UNEXPECTED_TOKEN.withToken(new Token(Token.TokenType.EOF, "", "(x", 2),
ParseError.ErrorType.TYPE_ASSUMPTION_ERROR));
tests.put("-> x", tests.put("-> x",
ParseError.UNEXPECTED_TOKEN.withToken(new Token(Token.TokenType.ARROW, "->", "-> x", 0))); ParseError.UNEXPECTED_TOKEN.withToken(new Token(Token.TokenType.ARROW, "->", "-> x", 0),
ParseError.ErrorType.TYPE_ASSUMPTION_ERROR));
tests.put("x 11", tests.put("x 11",
ParseError.UNEXPECTED_TOKEN.withToken(new Token(Token.TokenType.NUMBER, "11", "x 11", 2))); ParseError.UNEXPECTED_TOKEN.withToken(new Token(Token.TokenType.NUMBER, "11", "x 11", 2),
tests.put("x )", ParseError.UNEXPECTED_TOKEN.withToken(new Token(Token.TokenType.RIGHT_PARENTHESIS, ")", "x )", 2))); ParseError.ErrorType.TYPE_ASSUMPTION_ERROR));
tests.put("x )", ParseError.UNEXPECTED_TOKEN.withToken(new Token(Token.TokenType.RIGHT_PARENTHESIS, ")", "x )", 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, ")", "x -> (x) )", 9))); .withToken(new Token(Token.TokenType.RIGHT_PARENTHESIS, ")", "x -> (x) )", 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("type1:" + entry.getKey()); Result<Map<VarTerm, TypeAbstraction>, ParseError> type = parser.parse("type1:" + entry.getKey());