Commit b26f71e8 authored by Arne Keller's avatar Arne Keller
Browse files

Miscellaneous cleanups and corrections

parent b5e15767
Pipeline #171100 passed with stages
in 3 minutes and 11 seconds
......@@ -122,7 +122,7 @@ Copy the `typicalc.service` file into your systemd configuration and enable the
## License
Check the third-party libraries in `frontend/src/` for their respective license.
Check the third-party libraries ([MathJax](https://www.mathjax.org/), [svg-pan-zoom](https://github.com/bumbu/svg-pan-zoom), [Hammer.JS](https://hammerjs.github.io/)) in `frontend/src/` for their respective license.
Typicalc itself is licensed under the GPL 3.0 or (at your option) any later version.
......
......@@ -32,8 +32,6 @@ public class Conclusion {
}
/**
* Returns the type assumptions used in the conclusion
*
* @return the type assumptions used in the conclusion
*/
public Map<VarTerm, TypeAbstraction> getTypeAssumptions() {
......@@ -41,8 +39,6 @@ public class Conclusion {
}
/**
* Returns the lambda term in the conclusion
*
* @return the lambda term in the conclusion
*/
public LambdaTerm getLambdaTerm() {
......@@ -50,8 +46,6 @@ public class Conclusion {
}
/**
* Returns the type assigned to the lambda term in the conclusion
*
* @return the type assigned to the lambda term in the conclusion
*/
public Type getType() {
......
package edu.kit.typicalc.model.parser;
/**
* Can be attached to a parse error to indicate a specific error condition.
*
* @see ParseError
*/
public enum AdditionalInformation {
/**
* Duplicate VarType after Universal Quantifier.
*/
DUPLICATETYPE
DUPLICATETYPE,
/**
* An integer constant overflows the storage type.
*/
INT_OVERFLOW
}
......@@ -16,7 +16,7 @@ public class LambdaLexer {
* the given term as a String
*/
private final String term;
private final ParseError.ErrorType errorType;
private final ParseError.ErrorSource errorType;
/**
* current position in the term
*/
......@@ -28,7 +28,7 @@ public class LambdaLexer {
*
* @param term the term to lex
*/
public LambdaLexer(String term, ParseError.ErrorType errorType) {
public LambdaLexer(String term, ParseError.ErrorSource errorType) {
this.term = term;
this.errorType = errorType;
Deque<Token> tokens = new ArrayDeque<>();
......@@ -61,7 +61,7 @@ public class LambdaLexer {
*/
public Result<Token, ParseError> nextToken() {
if (result.isError()) {
return new Result<>(null, result.unwrapError());
return result.castError();
}
Deque<Token> tokens = result.unwrap();
if (!tokens.isEmpty()) {
......@@ -91,12 +91,12 @@ public class LambdaLexer {
advance();
return new Result<>(t);
} else {
return new Result<>(null, ParseError.unexpectedCharacter2(
return new Result<>(null, ParseError.unexpectedCharacter(
term.charAt(pos + 1), pos + 1, term, errorType).expectedCharacter('>'));
}
} else {
return new Result<>(null,
ParseError.unexpectedCharacter2(' ', term.length(), term, errorType)
ParseError.unexpectedCharacter(' ', term.length(), term, errorType)
.expectedCharacter('>'));
}
// bunch of single-character tokens
......@@ -152,7 +152,7 @@ public class LambdaLexer {
&& term.charAt(pos) < 128);
if (pos < term.length() && term.charAt(pos) >= 128) {
return new Result<>(null,
ParseError.unexpectedCharacter2(term.charAt(pos), pos, term, errorType)
ParseError.unexpectedCharacter(term.charAt(pos), pos, term, errorType)
.expectedType(TokenType.VARIABLE));
}
String s = sb.toString();
......@@ -185,15 +185,8 @@ public class LambdaLexer {
} while (pos < term.length() && Character.isDigit(term.charAt(pos)));
return new Result<>(new Token(TokenType.NUMBER, sb.toString(), term, startPos));
} else {
return new Result<>(null, ParseError.unexpectedCharacter2(c, pos, term,
return new Result<>(null, ParseError.unexpectedCharacter(c, pos, term,
errorType));
}
}
/**
* @return the term that is parsed
*/
public String getTerm() {
return term;
}
}
\ No newline at end of file
......@@ -42,7 +42,7 @@ public class LambdaParser {
* @param term String to parse
*/
public LambdaParser(String term) {
this.lexer = new LambdaLexer(term, ParseError.ErrorType.TERM_ERROR);
this.lexer = new LambdaLexer(term, ParseError.ErrorSource.TERM_ERROR);
}
/**
......@@ -70,7 +70,7 @@ public class LambdaParser {
Optional<ParseError> error = nextToken();
if (current != type) {
return Optional.of(ParseError.unexpectedToken(lastToken,
ParseError.ErrorType.TERM_ERROR).expectedType(type));
ParseError.ErrorSource.TERM_ERROR).expectedType(type));
}
return error;
}
......@@ -91,7 +91,7 @@ public class LambdaParser {
return t;
}
return new Result<>(null,
ParseError.unexpectedToken(last, ParseError.ErrorType.TERM_ERROR)
ParseError.unexpectedToken(last, ParseError.ErrorSource.TERM_ERROR)
.expectedInput(ExpectedInput.TERM));
}
......@@ -108,7 +108,7 @@ public class LambdaParser {
}
}
if (token.getType() == TokenType.EOF) {
return new Result<>(null, ParseError.unexpectedToken(token, ParseError.ErrorType.TERM_ERROR)
return new Result<>(null, ParseError.unexpectedToken(token, ParseError.ErrorSource.TERM_ERROR)
.expectedInput(ExpectedInput.TERM));
}
return parseApplication();
......@@ -208,8 +208,9 @@ public class LambdaParser {
try {
n = Integer.parseInt(number);
} catch (NumberFormatException e) {
return new Result<>(null, ParseError.unexpectedCharacter(
token, ParseError.ErrorType.TERM_ERROR));
return new Result<>(null, ParseError.unexpectedToken(
token, ParseError.ErrorSource.TERM_ERROR)
.additionalInformation(AdditionalInformation.INT_OVERFLOW));
}
error = nextToken();
if (error.isEmpty()) {
......
......@@ -14,9 +14,12 @@ public final class ParseError {
this.causeEnum = unexpectedToken;
}
/**
* The reason for this error.
*/
public enum ErrorCause {
/**
* the lambda term didn't meet the specified syntax
* the input contains that a token that is not allowed in that context
*/
UNEXPECTED_TOKEN,
......@@ -28,26 +31,43 @@ public final class ParseError {
private final ErrorCause causeEnum;
/**
* @return the cause of this parse error
*/
public ErrorCause getCauseEnum() {
return causeEnum;
}
public static ParseError unexpectedToken(Token cause, ErrorType source) {
/**
* Construct a new ParseError that signals an unexpected token.
*
* @param cause the incorrect token
* @param source kind of input parsed
* @return a new error
*/
public static ParseError unexpectedToken(Token cause, ErrorSource source) {
var self = new ParseError(ErrorCause.UNEXPECTED_TOKEN);
return self.withToken(cause, source);
}
public static ParseError unexpectedCharacter(Token cause, ErrorType source) {
var self = new ParseError(ErrorCause.UNEXPECTED_CHARACTER);
return self.withToken(cause, source);
}
public static ParseError unexpectedCharacter2(char cause, int position, String term, ErrorType errorType) {
/**
* Construct a new ParseError that signals an unexpected character.
*
* @param cause the invalid character
* @param position position in the input string
* @param term input string
* @param errorType kind of input parsed
* @return
*/
public static ParseError unexpectedCharacter(char cause, int position, String term, ErrorSource errorType) {
var self = new ParseError(ErrorCause.UNEXPECTED_CHARACTER);
return self.withCharacter(cause, position, term, errorType);
}
public enum ErrorType {
/**
* Indicates the error source.
*/
public enum ErrorSource {
/**
* This error was created when parsing the input term
*/
......@@ -67,7 +87,7 @@ public final class ParseError {
private char wrongChar = '\0';
private char correctChar = '\0';
private int position = -1;
private Optional<ErrorType> errorType = Optional.empty();
private Optional<ErrorSource> errorType = Optional.empty();
/**
* Attach a token to this error.
......@@ -75,7 +95,7 @@ public final class ParseError {
* @param cause the token that caused the error
* @return this object
*/
public ParseError withToken(Token cause, ErrorType errorType) {
public ParseError withToken(Token cause, ErrorSource errorType) {
this.cause = Optional.of(cause);
this.term = cause.getSourceText();
this.position = cause.getPos();
......@@ -165,7 +185,7 @@ public final class ParseError {
* @param term the term that is parsed
* @return this object
*/
public ParseError withCharacter(char cause, int position, String term, ErrorType errorType) {
public ParseError withCharacter(char cause, int position, String term, ErrorSource errorType) {
this.wrongChar = cause;
this.position = position;
this.term = term;
......@@ -218,7 +238,7 @@ public final class ParseError {
/**
* @return the error type
*/
public Optional<ErrorType> getErrorType() {
public Optional<ErrorSource> getErrorType() {
return errorType;
}
......@@ -229,10 +249,6 @@ public final class ParseError {
return additional;
}
protected void setErrorType(ErrorType errorType) {
this.errorType = Optional.of(errorType);
}
@Override
public String toString() {
return "ParseError{"
......
......@@ -54,7 +54,7 @@ public class TypeAssumptionParser {
public Result<Map<VarTerm, TypeAbstraction>, ParseError> parse(String assumptions) {
lexer = new LambdaLexer(
cleanAssumptionText(assumptions), ParseError.ErrorType.TYPE_ASSUMPTION_ERROR);
cleanAssumptionText(assumptions), ParseError.ErrorSource.TYPE_ASSUMPTION_ERROR);
return parseTE();
}
......@@ -86,7 +86,7 @@ public class TypeAssumptionParser {
typeVariableUniqueIndex++;
if (currentToken.getType() != Token.TokenType.COMMA) {
return new Result<>(null, ParseError.unexpectedToken(currentToken,
ParseError.ErrorType.TYPE_ASSUMPTION_ERROR)
ParseError.ErrorSource.TYPE_ASSUMPTION_ERROR)
.expectedTypes(List.of(Token.TokenType.COMMA, Token.TokenType.EOF)));
}
}
......@@ -102,7 +102,7 @@ public class TypeAssumptionParser {
term = new VarTerm(currentToken.getText());
} else {
return new Result<>(null, ParseError.unexpectedToken(currentToken,
ParseError.ErrorType.TYPE_ASSUMPTION_ERROR).expectedType(Token.TokenType.VARIABLE));
ParseError.ErrorSource.TYPE_ASSUMPTION_ERROR).expectedType(Token.TokenType.VARIABLE));
}
Result<Token, ParseError> nextLexerToken = lexer.nextToken();
......@@ -113,7 +113,7 @@ public class TypeAssumptionParser {
if (currentToken.getType() != Token.TokenType.COLON) {
return new Result<>(null, ParseError.unexpectedToken(currentToken,
ParseError.ErrorType.TYPE_ASSUMPTION_ERROR).expectedType(Token.TokenType.COLON));
ParseError.ErrorSource.TYPE_ASSUMPTION_ERROR).expectedType(Token.TokenType.COLON));
}
Result<TypeAbstraction, ParseError> result = parseType();
......@@ -146,13 +146,13 @@ public class TypeAssumptionParser {
if (currentToken.getType() != Token.TokenType.VARIABLE) {
return new Result<>(null,
ParseError.unexpectedToken(currentToken, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR)
ParseError.unexpectedToken(currentToken, ParseError.ErrorSource.TYPE_ASSUMPTION_ERROR)
.expectedType(Token.TokenType.VARIABLE));
}
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.ErrorSource.TYPE_ASSUMPTION_ERROR)
.expectedInput(ExpectedInput.VARTYPE));
}
int i = Integer.parseInt(input.substring(1));
......@@ -162,7 +162,7 @@ public class TypeAssumptionParser {
for (TypeVariable variable : quantifiedVariables) {
if (variable.equals(v)) {
return new Result<>(null,
ParseError.unexpectedToken(currentToken, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR)
ParseError.unexpectedToken(currentToken, ParseError.ErrorSource.TYPE_ASSUMPTION_ERROR)
.additionalInformation(AdditionalInformation.DUPLICATETYPE));
}
}
......@@ -177,7 +177,7 @@ public class TypeAssumptionParser {
if (currentToken.getType() != Token.TokenType.COMMA) {
if (currentToken.getType() != Token.TokenType.DOT) {
return new Result<>(null,
ParseError.unexpectedToken(currentToken, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR)
ParseError.unexpectedToken(currentToken, ParseError.ErrorSource.TYPE_ASSUMPTION_ERROR)
.expectedTypes(List.of(Token.TokenType.COMMA, Token.TokenType.DOT)));
}
nextLexerToken = lexer.nextToken();
......@@ -193,7 +193,7 @@ public class TypeAssumptionParser {
if (currentToken.getType() != Token.TokenType.VARIABLE && currentToken.getType()
!= Token.TokenType.LEFT_PARENTHESIS) {
return new Result<>(null,
ParseError.unexpectedToken(currentToken, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR)
ParseError.unexpectedToken(currentToken, ParseError.ErrorSource.TYPE_ASSUMPTION_ERROR)
.expectedInput(ExpectedInput.TYPE)
.expectedType(Token.TokenType.UNIVERSAL_QUANTIFIER));
}
......@@ -258,13 +258,13 @@ public class TypeAssumptionParser {
if (currentToken.getType() != Token.TokenType.RIGHT_PARENTHESIS) {
return new Result<>(null, ParseError.unexpectedToken(currentToken,
ParseError.ErrorType.TYPE_ASSUMPTION_ERROR)
ParseError.ErrorSource.TYPE_ASSUMPTION_ERROR)
.expectedTypes(List.of(Token.TokenType.ARROW, Token.TokenType.RIGHT_PARENTHESIS)));
}
return new Result<>(type);
}
return new Result<>(null, ParseError.unexpectedToken(currentToken,
ParseError.ErrorType.TYPE_ASSUMPTION_ERROR).expectedInput(ExpectedInput.TYPE));
ParseError.ErrorSource.TYPE_ASSUMPTION_ERROR).expectedInput(ExpectedInput.TYPE));
}
/**
......@@ -288,7 +288,7 @@ public class TypeAssumptionParser {
case VARIABLE:
case NUMBER:
return new Result<>(null, ParseError.unexpectedToken(currentToken,
ParseError.ErrorType.TYPE_ASSUMPTION_ERROR).expectedType(Token.TokenType.ARROW));
ParseError.ErrorSource.TYPE_ASSUMPTION_ERROR).expectedType(Token.TokenType.ARROW));
default:
return new Result<>(Optional.empty(), null);
}
......
......@@ -39,7 +39,7 @@ public class Presenter implements MainViewListener {
ParseError e = result.unwrapError();
view.displayError(e);
// focus the corresponding input field
String inputFieldId = e.getErrorType().equals(Optional.of(ParseError.ErrorType.TERM_ERROR))
String inputFieldId = e.getErrorType().equals(Optional.of(ParseError.ErrorSource.TERM_ERROR))
? TERM_INPUT_FIELD_ID : ASS_INPUT_FIELD_ID;
UI.getCurrent().getPage().executeJs(
"setTimeout(() => document.getElementById('" + inputFieldId + "').focus(), 0)");
......
......@@ -116,6 +116,13 @@ public class Result<T, E> {
return new Result<>(value != null ? mapping.apply(value) : null, error);
}
/**
* This function should only be used on error results and will change the second type parameter to any desired
* value.
*
* @param <U> the desired type
* @return a copy of this object
*/
public <U> Result<U, E> castError() {
return new Result<>(null, this.error);
}
......
package edu.kit.typicalc.view;
import com.vaadin.flow.component.dependency.JsModule;
/**
* Represents an HTML element that uses MathJax and custom TypeScript modules to render its contents.
* Provides an interface between Java code and said TypeScript modules.
* Multiple steps can be shown using the getStepCount and showStep methods.
*/
@JsModule("./src/mathjax-adapter.ts")
public interface MathjaxAdapter {
/**
......
......@@ -64,13 +64,13 @@ public class ErrorView extends VerticalLayout implements LocaleChangeObserver {
summary.setId(ERROR_SUMMARY_ID);
String term = error.getTerm();
String descriptionForError = null;
Optional<ParseError.ErrorType> errorType = error.getErrorType();
Optional<ParseError.ErrorSource> errorType = error.getErrorType();
if (errorType.isEmpty()) {
throw new IllegalStateException();
}
if (errorType.get() == ParseError.ErrorType.TERM_ERROR) {
if (errorType.get() == ParseError.ErrorSource.TERM_ERROR) {
descriptionForError = "error.termForError";
} else if (errorType.get() == ParseError.ErrorType.TYPE_ASSUMPTION_ERROR) {
} else if (errorType.get() == ParseError.ErrorSource.TYPE_ASSUMPTION_ERROR) {
descriptionForError = "error.typeAssumptionForError";
}
switch (error.getCauseEnum()) {
......
......@@ -17,7 +17,6 @@ import java.util.List;
* step revealing. Relies on MathjaxUnificationTS to interact with MathJax.
*/
@Tag("tc-explanation")
@JsModule("./src/mathjax-adapter.ts")
@JsModule("./src/mathjax-explanation.ts")
@CssImport("./styles/view/explanation.css")
public class MathjaxExplanation extends LitTemplate implements MathjaxAdapter {
......
......@@ -17,7 +17,6 @@ import java.util.List;
* with MathJax.
*/
@Tag("tc-proof-tree")
@JsModule("./src/mathjax-adapter.ts")
@JsModule("./src/mathjax-proof-tree.ts")
public class MathjaxProofTree extends LitTemplate implements MathjaxAdapter {
......
......@@ -13,7 +13,6 @@ import edu.kit.typicalc.view.MathjaxAdapter;
* step revealing. Relies on MathjaxUnificationTS to interact with MathJax.
*/
@Tag("tc-unification")
@JsModule("./src/mathjax-adapter.ts")
@JsModule("./src/mathjax-unification.ts")
@CssImport("./styles/view/unification.css")
public class MathjaxUnification extends LitTemplate implements MathjaxAdapter {
......
......@@ -53,7 +53,7 @@ public class ExplanationCreator implements StepVisitor {
/**
* Generate the LaTeX code from the type inferer for the language of the provided locale.
*
*
* @param typeInferer the TypeInfererInterface to create the LaTeX-code from
* @param locale the language of the explanatory texts
*/
......@@ -65,13 +65,13 @@ public class ExplanationCreator implements StepVisitor {
typeInferer.getFirstInferenceStep().accept(this);
if (!errorOccurred) {
explanationTexts.addAll(new ExplanationCreatorUnification(typeInferer, locale, provider, MODE,
letCounter, false, Optional.empty()).getUnificationsTexts().getLeft());
letCounter, Optional.empty()).getUnificationsTexts().getLeft());
}
}
/**
* Returns a list of strings with an entry for every step of the algorithm.
*
*
* @return list of strings containing the explanatory texts
*/
public List<String> getExplanationTexts() {
......@@ -196,13 +196,13 @@ public class ExplanationCreator implements StepVisitor {
// skip creation of unification texts if nested let produced an error
if (!errorOccurred) {
ExplanationCreatorUnification unification =
new ExplanationCreatorUnification(letD.getTypeInferer(), locale, provider, MODE, letCounter, true,
new ExplanationCreatorUnification(letD.getTypeInferer(), locale, provider, MODE, letCounter,
Optional.of(variable));
explanationTexts.addAll(unification.getUnificationsTexts().getLeft());
errorOccurred = unification.getUnificationsTexts().getRight();
letCounter--;
}
if (!errorOccurred) {
letD.getPremise().accept(this);
}
......
......@@ -65,11 +65,10 @@ public class ExplanationCreatorUnification {
* @param provider I18NProvider to get the templates from the resources bundle
* @param mode the used LaTeX generation method
* @param letCounter counter needed for nested let terms
* @param isLetUnification variable to indicate if it is the final unification or a let unification
* @param letVariable optional containing the let variable in case of a let unification
*/
protected ExplanationCreatorUnification(TypeInfererInterface typeInferer, Locale locale, I18NProvider provider,
LatexCreatorMode mode, int letCounter, boolean isLetUnification, Optional<LambdaTerm> letVariable) {
LatexCreatorMode mode, int letCounter, Optional<LambdaTerm> letVariable) {
this.typeInferer = typeInferer;
this.locale = locale;
this.provider = provider;
......@@ -77,7 +76,7 @@ public class ExplanationCreatorUnification {
this.letCounter = letCounter;
this.letVariable = letVariable;
buildTexts(isLetUnification);
buildTexts();
}
/**
......@@ -90,28 +89,26 @@ public class ExplanationCreatorUnification {
return Pair.of(unificationTexts, errorOccurred);
}
private void buildTexts(boolean isLetUnification) {
String initialPrefix = isLetUnification ? LET_KEY_PREFIX : KEY_PREFIX;
String letVariableName = isLetUnification
? toLatex(new LatexCreatorTerm(this.letVariable.get(), mode).getLatex()) : "";
private void buildTexts() {
String initialPrefix = this.letVariable.isPresent() ? LET_KEY_PREFIX : KEY_PREFIX;
String letVariableName = this.letVariable.map(
it -> toLatex(new LatexCreatorTerm(it, mode).getLatex())).orElse("");
String constraintSet = toLatex(letCounterToLatex(CONSTRAINT_SET));
String finalText = provider.getTranslation(initialPrefix + "initial", locale, constraintSet, letVariableName);
unificationTexts.add(finalText);
createUnficationTexts();
createUnificationTexts();
if (!errorOccurred) {
createMGU();
createFinalType(isLetUnification);
if (isLetUnification) {
createLetUnificationFinish();
}
createFinalType();
this.letVariable.ifPresent(this::createLetUnificationFinish);
}
}
private void createLetUnificationFinish() {
private void createLetUnificationFinish(LambdaTerm letTerm) {
String typeAssumptions =
typeAssumptionsToLatex(typeInferer.getFirstInferenceStep().getConclusion().getTypeAssumptions(), mode);
String letVariableLatex = toLatex(new LatexCreatorTerm(this.letVariable.get(), mode).getLatex());
String letVariableLatex = toLatex(new LatexCreatorTerm(letTerm, mode).getLatex());
String gamma = toLatex(GAMMA + APOSTROPHE);
String sigma = toLatex(letCounterToLatex(SIGMA));
String finalType = toLatex(new LatexCreatorType(typeInferer.getType().get(), mode).getLatex());
......@@ -135,8 +132,8 @@ public class ExplanationCreatorUnification {
+ typeAssumptions + PAREN_RIGHT + PAREN_RIGHT;
}
private void createFinalType(boolean isLetUnification) {
String keyPrefix = isLetUnification ? LET_KEY_PREFIX : KEY_PREFIX;
private void createFinalType() {
String keyPrefix = this.letVariable.isPresent() ? LET_KEY_PREFIX : KEY_PREFIX;