mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-08 10:20:41 +00:00
parent
c3deae0bcc
commit
9797d13041
@ -0,0 +1,8 @@
|
||||
package edu.kit.typicalc.model.parser;
|
||||
|
||||
public enum AdditionalInformation {
|
||||
/**
|
||||
* Duplicate VarType after Universal Quantifier.
|
||||
*/
|
||||
DUPLICATETYPE
|
||||
}
|
@ -12,5 +12,9 @@ public enum ExpectedInput {
|
||||
/**
|
||||
* Any kind of type.
|
||||
*/
|
||||
TYPE
|
||||
TYPE,
|
||||
/**
|
||||
* // t[0-9]+
|
||||
*/
|
||||
VARTYPE
|
||||
}
|
||||
|
@ -62,6 +62,7 @@ public final class ParseError {
|
||||
private Optional<Token> cause = Optional.empty();
|
||||
private Optional<Collection<Token.TokenType>> needed = Optional.empty();
|
||||
private Optional<ExpectedInput> expected = Optional.empty();
|
||||
private Optional<AdditionalInformation> additional = Optional.empty();
|
||||
private String term = "";
|
||||
private char wrongChar = '\0';
|
||||
private char correctChar = '\0';
|
||||
@ -93,6 +94,17 @@ public final class ParseError {
|
||||
return this;
|
||||
}
|
||||
|
||||
/**
|
||||
* Attach additional information to this error.
|
||||
*
|
||||
* @param additional the additional information
|
||||
* @return this object
|
||||
*/
|
||||
public ParseError additionalInformation(AdditionalInformation additional) {
|
||||
this.additional = Optional.of(additional);
|
||||
return this;
|
||||
}
|
||||
|
||||
/**
|
||||
* Set expected token types of this error.
|
||||
*
|
||||
@ -210,6 +222,13 @@ public final class ParseError {
|
||||
return errorType;
|
||||
}
|
||||
|
||||
/**
|
||||
* @return the additional information
|
||||
*/
|
||||
public Optional<AdditionalInformation> getAdditionalInformation() {
|
||||
return additional;
|
||||
}
|
||||
|
||||
protected void setErrorType(ErrorType errorType) {
|
||||
this.errorType = Optional.of(errorType);
|
||||
}
|
||||
|
@ -10,6 +10,14 @@ import java.util.regex.Matcher;
|
||||
import java.util.regex.Pattern;
|
||||
/**
|
||||
* Parser for type assumptions.
|
||||
* Parses according to the following grammar:
|
||||
*
|
||||
* TypeEnvironment --> ɛ | TypeAbstraction, TypeEnvironment | TypeAbstraction
|
||||
* TypeAbstraction --> Variable | Type
|
||||
* Type --> ∀ VarType.SingleType | SingleType
|
||||
* SingleType --> SimpleType Rest
|
||||
* SimpleType --> Variable | (SingleType)
|
||||
* Rest --> ɛ | -> SingleType
|
||||
*/
|
||||
public class TypeAssumptionParser {
|
||||
|
||||
@ -47,14 +55,14 @@ public class TypeAssumptionParser {
|
||||
public Result<Map<VarTerm, TypeAbstraction>, ParseError> parse(String assumptions) {
|
||||
lexer = new LambdaLexer(
|
||||
cleanAssumptionText(assumptions), ParseError.ErrorType.TYPE_ASSUMPTION_ERROR);
|
||||
return parseTU();
|
||||
return parseTE();
|
||||
}
|
||||
|
||||
/**
|
||||
* parses Type Environment
|
||||
* @return if successful, a map of the type assumptions, otherwise an error
|
||||
*/
|
||||
public Result<Map<VarTerm, TypeAbstraction>, ParseError> parseTU() {
|
||||
public Result<Map<VarTerm, TypeAbstraction>, ParseError> parseTE() {
|
||||
HashMap<VarTerm, TypeAbstraction> map = new HashMap<>();
|
||||
while (true) {
|
||||
Result<Token, ParseError> nextLexerToken = lexer.nextToken();
|
||||
@ -115,6 +123,11 @@ public class TypeAssumptionParser {
|
||||
return new Result<>(new MapEntry<>(term, result.unwrap()));
|
||||
}
|
||||
|
||||
|
||||
/**
|
||||
* Parses a Type
|
||||
* @return if successful a type abstraction, otherwise an error.
|
||||
*/
|
||||
public Result<TypeAbstraction, ParseError> parseType() {
|
||||
Result<Token, ParseError> nextLexerToken = lexer.nextToken();
|
||||
if (nextLexerToken.isError()) {
|
||||
@ -139,7 +152,8 @@ public class TypeAssumptionParser {
|
||||
String input = currentToken.getText();
|
||||
if (!TYPE_VARIABLE_PATTERN.matcher(input).matches()) {
|
||||
return new Result<>(null,
|
||||
ParseError.unexpectedToken(currentToken, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR));
|
||||
ParseError.unexpectedToken(currentToken, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR)
|
||||
.expectedInput(ExpectedInput.VARTYPE));
|
||||
}
|
||||
int i = Integer.parseInt(input.substring(1));
|
||||
TypeVariable v = new TypeVariable(TypeVariableKind.USER_INPUT, i);
|
||||
@ -148,7 +162,8 @@ public class TypeAssumptionParser {
|
||||
for (TypeVariable var : quantifiedVariables) {
|
||||
if (var.equals(v)) {
|
||||
return new Result<>(null,
|
||||
ParseError.unexpectedToken(currentToken, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR));
|
||||
ParseError.unexpectedToken(currentToken, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR)
|
||||
.additionalInformation(AdditionalInformation.DUPLICATETYPE));
|
||||
}
|
||||
}
|
||||
quantifiedVariables.add(v);
|
||||
@ -190,6 +205,10 @@ public class TypeAssumptionParser {
|
||||
return new Result<>(new TypeAbstraction(result.unwrap(), quantifiedVariables));
|
||||
}
|
||||
|
||||
/**
|
||||
* parses a single Type
|
||||
* @return if successful a type, otherwise an error
|
||||
*/
|
||||
public Result<Type, ParseError> parseSingleType() {
|
||||
|
||||
Result<Type, ParseError> result = parseSimpleType();
|
||||
@ -216,6 +235,10 @@ public class TypeAssumptionParser {
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* parses a simple type
|
||||
* @return if successful a type, otherwise an error
|
||||
*/
|
||||
public Result<Type, ParseError> parseSimpleType() {
|
||||
if (currentToken.getType() == Token.TokenType.VARIABLE) {
|
||||
Type type = parseLiteral(currentToken.getText());
|
||||
@ -244,6 +267,10 @@ public class TypeAssumptionParser {
|
||||
ParseError.ErrorType.TYPE_ASSUMPTION_ERROR).expectedInput(ExpectedInput.TYPE));
|
||||
}
|
||||
|
||||
/**
|
||||
* parses the rest of a single type
|
||||
* @return if successful a type or an empty optional, otherwise an error
|
||||
*/
|
||||
public Result<Optional<Type>, ParseError> parseRest() {
|
||||
switch (currentToken.getType()) {
|
||||
case ARROW:
|
||||
|
@ -10,6 +10,7 @@ import com.vaadin.flow.component.html.Pre;
|
||||
import com.vaadin.flow.component.orderedlayout.VerticalLayout;
|
||||
import com.vaadin.flow.i18n.LocaleChangeEvent;
|
||||
import com.vaadin.flow.i18n.LocaleChangeObserver;
|
||||
import edu.kit.typicalc.model.parser.AdditionalInformation;
|
||||
import edu.kit.typicalc.model.parser.ExpectedInput;
|
||||
import edu.kit.typicalc.model.parser.ParseError;
|
||||
import edu.kit.typicalc.model.parser.Token;
|
||||
@ -130,6 +131,15 @@ public class ErrorView extends VerticalLayout implements LocaleChangeObserver {
|
||||
getTranslation("error.expectedToken", correct))));
|
||||
}
|
||||
|
||||
// state more additional information, if available
|
||||
Optional<AdditionalInformation> moreAdditionalInformation = error.getAdditionalInformation();
|
||||
if (moreAdditionalInformation.isPresent()) {
|
||||
AdditionalInformation e = moreAdditionalInformation.get();
|
||||
additionalInformation.add(new Span(new Pre(
|
||||
getTranslation("error.additionalInformation",
|
||||
getTranslation("additionalInformation." + e)))));
|
||||
}
|
||||
|
||||
return new Div(additionalInformation);
|
||||
}
|
||||
|
||||
|
@ -110,6 +110,7 @@ error.termForError=Term:\u0020
|
||||
error.typeAssumptionForError=Typannahme:\u0020
|
||||
error.wrongCharacter=Falsches Zeichen:\u0020
|
||||
error.expectedToken=Erwartet: {0}
|
||||
error.additionalInformation = Information: {0}
|
||||
error.hint=Die Grammatiken, die die korrekte Syntax eines Terms und der Typannahmen beschreiben, \
|
||||
sind auch über das Info-Symbol zu erreichen.
|
||||
tokentype.UNIVERSAL_QUANTIFIER=Allquantor
|
||||
@ -128,6 +129,8 @@ tokentype.COLON=:
|
||||
tokentype.EQUALS==
|
||||
tokentype.ARROW=->
|
||||
tokentype.EOF=Ende der Eingabe
|
||||
expectedinput.VARTYPE= Variable der Form t[0-9]+
|
||||
additionalInformation.DUPLICATETYPE= Duplikat
|
||||
expectedinput.TERM=beliebiger Term
|
||||
expectedinput.TYPE=beliebiger Typ
|
||||
root.or=oder
|
||||
|
@ -102,6 +102,7 @@ error.wrongCharacter=Wrong character:\u0020
|
||||
error.termForError=Term:\u0020
|
||||
error.typeAssumptionForError=Type assumption:\u0020
|
||||
error.expectedToken=Expected: {0}
|
||||
error.additionalInformation = Information: {0}
|
||||
error.hint=The grammars describing the correct syntax of a term or a type assumption can also be reached \
|
||||
via the info icon.
|
||||
tokentype.UNIVERSAL_QUANTIFIER=universal quantifier
|
||||
@ -120,6 +121,8 @@ tokentype.COLON=:
|
||||
tokentype.EQUALS==
|
||||
tokentype.ARROW=->
|
||||
tokentype.EOF=End of input
|
||||
additionalInformation.DUPLICATETYPE= Duplicate
|
||||
expectedinput.VARTYPE= Variable of the form t[0-9]+
|
||||
expectedinput.TERM=any lambda term
|
||||
expectedinput.TYPE=any type
|
||||
root.or=or
|
||||
|
Loading…
Reference in New Issue
Block a user