mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-08 18:30:42 +00:00
Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc
This commit is contained in:
commit
0c2836a27f
@ -69,7 +69,7 @@ public class LambdaParser {
|
||||
TokenType current = token.getType();
|
||||
Optional<ParseError> error = nextToken();
|
||||
if (current != type) {
|
||||
return Optional.of(ParseError.UNEXPECTED_TOKEN.withToken(lastToken));
|
||||
return Optional.of(ParseError.UNEXPECTED_TOKEN.withToken(lastToken).expectedType(type));
|
||||
}
|
||||
return error;
|
||||
}
|
||||
@ -84,11 +84,15 @@ public class LambdaParser {
|
||||
if (t.isError()) {
|
||||
return t;
|
||||
}
|
||||
Token last = token;
|
||||
Optional<ParseError> next = expect(TokenType.EOF);
|
||||
if (next.isEmpty()) {
|
||||
return t;
|
||||
}
|
||||
return new Result<>(null, next.get());
|
||||
return new Result<>(null,
|
||||
(last.getType() == TokenType.EOF ? ParseError.TOO_FEW_TOKENS : ParseError.UNEXPECTED_TOKEN)
|
||||
.withToken(last)
|
||||
.expectedTypes(ATOM_START_TOKENS));
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -1,7 +1,11 @@
|
||||
package edu.kit.typicalc.model.parser;
|
||||
|
||||
import java.util.Collection;
|
||||
import java.util.List;
|
||||
import java.util.Optional;
|
||||
|
||||
/**
|
||||
* Errors that can occur when parsing a lambda term.
|
||||
* Errors that can occur when parsing a lambda term or type assumption.
|
||||
*
|
||||
* @see LambdaLexer
|
||||
* @see LambdaParser
|
||||
@ -23,7 +27,8 @@ public enum ParseError {
|
||||
*/
|
||||
UNEXPECTED_CHARACTER;
|
||||
|
||||
private Token cause = new Token(Token.TokenType.EOF, "", -1);
|
||||
private Optional<Token> cause = Optional.empty();
|
||||
private Optional<Collection<Token.TokenType>> needed = Optional.empty();
|
||||
private char wrongChar = '\0';
|
||||
private int position = -1;
|
||||
|
||||
@ -34,7 +39,29 @@ public enum ParseError {
|
||||
* @return this object
|
||||
*/
|
||||
public ParseError withToken(Token cause) {
|
||||
this.cause = cause;
|
||||
this.cause = Optional.of(cause);
|
||||
return this;
|
||||
}
|
||||
|
||||
/**
|
||||
* Attach an expected token type to this error.
|
||||
*
|
||||
* @param needed the required token type
|
||||
* @return this object
|
||||
*/
|
||||
public ParseError expectedType(Token.TokenType needed) {
|
||||
this.needed = Optional.of(List.of(needed));
|
||||
return this;
|
||||
}
|
||||
|
||||
/**
|
||||
* Attach expected token types to this error.
|
||||
*
|
||||
* @param needed the possible token types
|
||||
* @return this object
|
||||
*/
|
||||
public ParseError expectedTypes(Collection<Token.TokenType> needed) {
|
||||
this.needed = Optional.of(needed);
|
||||
return this;
|
||||
}
|
||||
|
||||
@ -52,16 +79,29 @@ public enum ParseError {
|
||||
}
|
||||
|
||||
/**
|
||||
* @return the token associated with this error, or null if none
|
||||
* @return the token associated with this error
|
||||
*/
|
||||
public Token getCause() {
|
||||
public Optional<Token> getCause() {
|
||||
return cause;
|
||||
}
|
||||
|
||||
/**
|
||||
* @return the expected/possible token(s) if this error is UNEXPECTED_TOKEN
|
||||
*/
|
||||
public Optional<Collection<Token.TokenType>> getExpected() {
|
||||
return needed;
|
||||
}
|
||||
|
||||
/**
|
||||
* @return the wrong character if this error is UNEXPECTED_CHARACTER ('\0' otherwise)
|
||||
*/
|
||||
public char getWrongCharacter() {
|
||||
return wrongChar;
|
||||
}
|
||||
|
||||
/**
|
||||
* @return the character position if this error is UNEXPECTED_CHARACTER
|
||||
*/
|
||||
public int getPosition() {
|
||||
return position;
|
||||
}
|
||||
|
@ -12,7 +12,7 @@ public class Token {
|
||||
* VARIABLE and NUMBER have a regular expression associated with them.
|
||||
* EOF is a special token to indicate that the end of file is reached.
|
||||
*/
|
||||
enum TokenType {
|
||||
public enum TokenType {
|
||||
LAMBDA, // λ or a backslash
|
||||
VARIABLE, // [a-z][a-zA-Z0-9]* except "let" or "in" or constants
|
||||
LET, // let
|
||||
@ -25,7 +25,7 @@ public class Token {
|
||||
DOT, // .
|
||||
EQUALS, // =
|
||||
ARROW, // ->
|
||||
EOF // pseudo token if end of file is reached
|
||||
EOF // pseudo token if end of input is reached
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -38,16 +38,22 @@ public class TypicalcI18NProvider implements I18NProvider {
|
||||
public String getTranslation(String key, Locale locale, Object... params) {
|
||||
ResourceBundle bundle = ResourceBundle.getBundle(LANGUAGE_BUNDLE_PREFIX, locale);
|
||||
|
||||
String result;
|
||||
if (bundle.containsKey(key)) {
|
||||
return bundle.getString(key);
|
||||
result = bundle.getString(key);
|
||||
} else {
|
||||
try {
|
||||
return this.generalBundle.getString(key);
|
||||
result = this.generalBundle.getString(key);
|
||||
} catch (MissingResourceException exception) {
|
||||
// this is only the case for untranslated texts
|
||||
return "?[" + key + "]?";
|
||||
}
|
||||
}
|
||||
// replace placeholders {0} ...
|
||||
for (int i = 0; i < params.length; i++) {
|
||||
result = result.replace(String.format("{%d}", i), params[i].toString());
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
}
|
||||
|
@ -2,7 +2,6 @@ package edu.kit.typicalc.view.content.errorcontent;
|
||||
|
||||
import com.vaadin.flow.component.Component;
|
||||
import com.vaadin.flow.component.dependency.CssImport;
|
||||
import com.vaadin.flow.component.details.Details;
|
||||
import com.vaadin.flow.component.html.Div;
|
||||
import com.vaadin.flow.component.html.H3;
|
||||
import com.vaadin.flow.component.html.Paragraph;
|
||||
@ -11,8 +10,12 @@ 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.ParseError;
|
||||
import edu.kit.typicalc.model.parser.Token;
|
||||
import edu.kit.typicalc.view.main.InfoContent;
|
||||
|
||||
import java.util.Collection;
|
||||
import java.util.Optional;
|
||||
|
||||
@CssImport("./styles/view/error-view.css")
|
||||
public class ErrorView extends VerticalLayout implements LocaleChangeObserver {
|
||||
private static final long serialVersionUID = 239587L;
|
||||
@ -21,8 +24,6 @@ public class ErrorView extends VerticalLayout implements LocaleChangeObserver {
|
||||
private static final String ADDITIONAL_INFO_ID = "errorAdditionalInfo";
|
||||
private static final String ERROR_SUMMARY_ID = "errorSummary";
|
||||
|
||||
private static final int NO_ADDITIONAL_INFO = -1;
|
||||
|
||||
private final H3 heading;
|
||||
private final Div errorMessage;
|
||||
private final ParseError error;
|
||||
@ -44,9 +45,18 @@ public class ErrorView extends VerticalLayout implements LocaleChangeObserver {
|
||||
Paragraph summary = new Paragraph(getTranslation("root." + error.toString()));
|
||||
summary.setId(ERROR_SUMMARY_ID);
|
||||
|
||||
if (error == ParseError.TOO_FEW_TOKENS) {
|
||||
switch (error) {
|
||||
case TOO_FEW_TOKENS:
|
||||
additionalInformation.add(new Span(getTranslation("root.tooFewTokensHelp")));
|
||||
} else if (error == ParseError.UNEXPECTED_CHARACTER) {
|
||||
break;
|
||||
case UNEXPECTED_TOKEN:
|
||||
Optional<Token> cause = error.getCause();
|
||||
if (cause.isPresent()) {
|
||||
additionalInformation.add(new Span(getTranslation("root.wrongCharacter") + cause.get().getText()));
|
||||
additionalInformation.add(new Span(getTranslation("root.position") + cause.get().getPos()));
|
||||
}
|
||||
break;
|
||||
case UNEXPECTED_CHARACTER:
|
||||
char c = error.getWrongCharacter();
|
||||
if (c != '\0') {
|
||||
additionalInformation.add(new Span(getTranslation("root.wrongCharacter") + c));
|
||||
@ -54,16 +64,29 @@ public class ErrorView extends VerticalLayout implements LocaleChangeObserver {
|
||||
} else {
|
||||
return summary;
|
||||
}
|
||||
} else {
|
||||
if (error.getCause().getPos() == NO_ADDITIONAL_INFO) {
|
||||
return summary;
|
||||
} else {
|
||||
additionalInformation.add(new Span(getTranslation("root.wrongCharacter") + error.getCause().getText()));
|
||||
additionalInformation.add(new Span(getTranslation("root.position") + error.getCause().getPos()));
|
||||
}
|
||||
break;
|
||||
default:
|
||||
throw new IllegalStateException(); // delete when updating to Java 12+
|
||||
}
|
||||
|
||||
return new Details(summary, additionalInformation);
|
||||
// add expected tokens, if available
|
||||
Optional<Collection<Token.TokenType>> expected = error.getExpected();
|
||||
if (expected.isPresent()) {
|
||||
Collection<Token.TokenType> possible = expected.get();
|
||||
StringBuilder sb = new StringBuilder();
|
||||
for (Token.TokenType t : possible) {
|
||||
if (sb.length() > 0) {
|
||||
sb.append(' ');
|
||||
sb.append(getTranslation("root.or"));
|
||||
sb.append(' ');
|
||||
}
|
||||
sb.append(getTranslation("tokentype." + t));
|
||||
}
|
||||
additionalInformation.add(new Span(
|
||||
getTranslation("error.expectedToken", sb.toString())));
|
||||
}
|
||||
|
||||
return new Div(summary, additionalInformation);
|
||||
}
|
||||
|
||||
@Override
|
||||
|
@ -55,12 +55,13 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
|
||||
protected InputBar(Consumer<Pair<String, Map<String, String>>> callback) {
|
||||
this.callback = callback;
|
||||
|
||||
setId(INPUT_BAR_ID);
|
||||
|
||||
infoIcon = new Button(new Icon(VaadinIcon.INFO_CIRCLE));
|
||||
infoIcon.addClickListener(event -> onInfoIconClick());
|
||||
|
||||
inputField = new TextField();
|
||||
inputField.getElement().setAttribute("autofocus", "");
|
||||
inputField.setPlaceholder(getTranslation("root.inputFieldPlaceholder"));
|
||||
inputField.getElement().setAttribute("autofocus", ""); // focus on page load
|
||||
inputField.setId(INPUT_FIELD_ID);
|
||||
inputField.setClearButtonVisible(true);
|
||||
inputField.setMaxLength(MAX_INPUT_LENGTH);
|
||||
@ -72,10 +73,11 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
|
||||
Button lambdaButton = new Button(getTranslation("root.lambda"));
|
||||
lambdaButton.setId(LAMBDA_BUTTON_ID);
|
||||
UI.getCurrent().getPage().executeJs("window.lambdaButtonListener($0, $1);", LAMBDA_BUTTON_ID, INPUT_FIELD_ID);
|
||||
|
||||
typeAssumptions = new Button("", event -> onTypeAssumptionsButton());
|
||||
typeAssumptions.setId(ASS_BUTTON_ID);
|
||||
typeAssumptionsArea = new TypeAssumptionsArea();
|
||||
exampleButton = new Button(VaadinIcon.PAPERCLIP.create(), event -> onExampleButtonClick());
|
||||
exampleButton = new Button(getTranslation("root.exampleButton"), event -> onExampleButtonClick());
|
||||
exampleButton.setId(EXAMPLE_BUTTON_ID);
|
||||
inferTypeButton = new Button("", event -> onTypeInferButtonClick());
|
||||
inferTypeButton.addClickShortcut(Key.ENTER).listenOn(this);
|
||||
@ -83,7 +85,6 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
|
||||
inferTypeButton.setId(INFER_BUTTON_ID);
|
||||
|
||||
add(infoIcon, typeAssumptions, lambdaButton, inputField, exampleButton, inferTypeButton);
|
||||
setId(INPUT_BAR_ID);
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -53,7 +53,6 @@ public class MainViewImpl extends AppLayout
|
||||
* Creates a new MainViewImpl.
|
||||
*/
|
||||
public MainViewImpl() {
|
||||
setDrawerOpened(false);
|
||||
MainViewListener presenter = new Presenter(new ModelImpl(), this);
|
||||
upperBar = new UpperBar(presenter, this::processInput);
|
||||
addToNavbar(upperBar);
|
||||
|
@ -1,6 +1,5 @@
|
||||
package edu.kit.typicalc.view.main;
|
||||
|
||||
import com.vaadin.flow.component.applayout.DrawerToggle;
|
||||
import com.vaadin.flow.component.button.Button;
|
||||
import com.vaadin.flow.component.dependency.CssImport;
|
||||
import com.vaadin.flow.component.html.Anchor;
|
||||
@ -36,7 +35,6 @@ public class UpperBar extends HorizontalLayout implements LocaleChangeObserver {
|
||||
private static final String UPPER_BAR_ID = "header";
|
||||
|
||||
private final InputBar inputBar;
|
||||
private final Button toggle;
|
||||
private final Button helpButton;
|
||||
|
||||
private final transient MainViewListener presenter;
|
||||
@ -53,7 +51,6 @@ public class UpperBar extends HorizontalLayout implements LocaleChangeObserver {
|
||||
this.presenter = presenter;
|
||||
this.inputConsumer = inputConsumer;
|
||||
|
||||
toggle = new DrawerToggle();
|
||||
H1 viewTitle = new H1(new Anchor("/", getTranslation("root.typicalc")));
|
||||
viewTitle.setId(VIEW_TITLE_ID);
|
||||
this.inputBar = new InputBar(this::typeInfer);
|
||||
@ -62,7 +59,7 @@ public class UpperBar extends HorizontalLayout implements LocaleChangeObserver {
|
||||
helpButton.addClickListener(event -> new HelpDialog().open());
|
||||
helpButton.setId(HELP_ICON_ID);
|
||||
|
||||
add(/*toggle, */viewTitle, inputBar, helpButton);
|
||||
add(viewTitle, inputBar, helpButton);
|
||||
setId(UPPER_BAR_ID);
|
||||
getThemeList().set("dark", true);
|
||||
setSpacing(false);
|
||||
@ -96,7 +93,6 @@ public class UpperBar extends HorizontalLayout implements LocaleChangeObserver {
|
||||
|
||||
@Override
|
||||
public void localeChange(LocaleChangeEvent event) {
|
||||
toggle.getElement().setAttribute("title", getTranslation("root.drawerToggleTooltip"));
|
||||
helpButton.getElement().setAttribute("title", getTranslation("root.helpIconTooltip"));
|
||||
}
|
||||
}
|
||||
|
@ -1,6 +1,7 @@
|
||||
root.close=Schließen
|
||||
root.save=Speichern
|
||||
root.copied=LaTeX-Code in Zwischenablage kopiert.
|
||||
root.exampleButton=📂 Beispiele
|
||||
root.selectExample=Beispiel auswählen:
|
||||
root.typeInfer=Typisieren
|
||||
root.operatingHelp=Hilfe
|
||||
@ -100,6 +101,21 @@ root.UNEXPECTED_CHARACTER=Die Eingabe enthält ein Zeichen, welches an dieser St
|
||||
error.heading=Syntaktisch falsche Eingabe!
|
||||
root.wrongCharacter=Falsches Zeichen: \u0020
|
||||
root.position=An Position: \u0020
|
||||
error.expectedToken=Erwartet: {0}
|
||||
tokentype.LAMBDA=λ
|
||||
tokentype.VARIABLE=Variable
|
||||
tokentype.LET=let
|
||||
tokentype.IN=in
|
||||
tokentype.TRUE=true
|
||||
tokentype.FALSE=false
|
||||
tokentype.NUMBER=Zahl
|
||||
tokentype.LEFT_PARENTHESIS=(
|
||||
tokentype.RIGHT_PARENTHESIS=)
|
||||
tokentype.DOT=.
|
||||
tokentype.EQUALS==
|
||||
tokentype.ARROW=->
|
||||
tokentype.EOF=Ende der Eingabe
|
||||
root.or=oder
|
||||
root.slideExp=Typicalc ist eine Anwendung zur Visualisierung von Typinferenz. In der folgenden Slideshow wird ein \
|
||||
Beispielszenario mit den wichtigsten Funktionen der Website vorgeführt. Das relevante Bedienelement ist jeweils mit \
|
||||
einem roten Rahmen hervorgehoben. Zwischen einzelnen Slides kann mithilfe der Knöpfe am unteren Ende der Seite \
|
||||
@ -129,7 +145,6 @@ verwendeten Pakete aufgelistet.
|
||||
root.correctAssumptions=Korrigiere oder lösche die ungültigen Typannahmen (rot hinterlegt) \
|
||||
vor dem Schließen des Dialogs.
|
||||
root.copyLatexTooltip=Kopiere LaTeX-code
|
||||
root.drawerToggleTooltip=Ableitungsregeln
|
||||
root.helpIconTooltip=Hilfe und Sprachwechsel
|
||||
root.exampleTooltip=Beispielterme
|
||||
root.shareButtonTooltip=LaTeX-Code und Permalink
|
||||
|
@ -1,6 +1,7 @@
|
||||
root.close=Close
|
||||
root.save=Save
|
||||
root.copied=LaTeX code copied to clipboard.
|
||||
root.exampleButton=📂 Examples
|
||||
root.selectExample=Select example:
|
||||
root.typeInfer=Type
|
||||
root.operatingHelp=Help
|
||||
@ -121,7 +122,6 @@ root.text8=The dialog contains a permalink to the current page, the LaTeX-code o
|
||||
to compile the code.
|
||||
root.correctAssumptions=Correct or delete the invalid type assumptions (red background) before closing the dialog.
|
||||
root.copyLatexTooltip=Copy LaTeX code
|
||||
root.drawerToggleTooltip=Type inference rules
|
||||
root.helpIconTooltip=Help and language switch
|
||||
root.exampleTooltip=Example terms
|
||||
root.shareButtonTooltip=LaTeX code and permalink
|
||||
|
@ -98,7 +98,7 @@ class LambdaParserTest {
|
||||
parser = new LambdaParser("x)");
|
||||
ParseError error = parser.parse().unwrapError();
|
||||
assertEquals(ParseError.UNEXPECTED_TOKEN, error);
|
||||
assertEquals(new Token(TokenType.RIGHT_PARENTHESIS, ")", 1), error.getCause());
|
||||
assertEquals(new Token(TokenType.RIGHT_PARENTHESIS, ")", 1), error.getCause().get());
|
||||
parser = new LambdaParser("??");
|
||||
assertEquals(ParseError.UNEXPECTED_CHARACTER, parser.parse().unwrapError());
|
||||
parser = new LambdaParser("aλ");
|
||||
@ -110,39 +110,39 @@ class LambdaParserTest {
|
||||
parser = new LambdaParser("x 123333333333333");
|
||||
error = parser.parse().unwrapError();
|
||||
assertEquals(ParseError.UNEXPECTED_CHARACTER, error);
|
||||
assertEquals(new Token(TokenType.NUMBER, "123333333333333", 2), error.getCause());
|
||||
assertEquals(new Token(TokenType.NUMBER, "123333333333333", 2), error.getCause().get());
|
||||
parser = new LambdaParser("λ)");
|
||||
error = parser.parse().unwrapError();
|
||||
assertEquals(ParseError.UNEXPECTED_TOKEN, error);
|
||||
assertEquals(new Token(TokenType.RIGHT_PARENTHESIS, ")", 1), error.getCause());
|
||||
assertEquals(new Token(TokenType.RIGHT_PARENTHESIS, ")", 1), error.getCause().get());
|
||||
parser = new LambdaParser("λx=");
|
||||
error = parser.parse().unwrapError();
|
||||
assertEquals(ParseError.UNEXPECTED_TOKEN, error);
|
||||
assertEquals(new Token(TokenType.EQUALS, "=", 2), error.getCause());
|
||||
assertEquals(new Token(TokenType.EQUALS, "=", 2), error.getCause().get());
|
||||
parser = new LambdaParser("λx..");
|
||||
error = parser.parse().unwrapError();
|
||||
assertEquals(ParseError.UNEXPECTED_TOKEN, error);
|
||||
assertEquals(new Token(TokenType.DOT, ".", 3), error.getCause());
|
||||
assertEquals(new Token(TokenType.DOT, ".", 3), error.getCause().get());
|
||||
parser = new LambdaParser("let ) =");
|
||||
error = parser.parse().unwrapError();
|
||||
assertEquals(ParseError.UNEXPECTED_TOKEN, error);
|
||||
assertEquals(new Token(TokenType.RIGHT_PARENTHESIS, ")", 4), error.getCause());
|
||||
assertEquals(new Token(TokenType.RIGHT_PARENTHESIS, ")", 4), error.getCause().get());
|
||||
parser = new LambdaParser("let x .");
|
||||
error = parser.parse().unwrapError();
|
||||
assertEquals(ParseError.UNEXPECTED_TOKEN, error);
|
||||
assertEquals(new Token(TokenType.DOT, ".", 6), error.getCause());
|
||||
assertEquals(new Token(TokenType.DOT, ".", 6), error.getCause().get());
|
||||
parser = new LambdaParser("let x = )");
|
||||
error = parser.parse().unwrapError();
|
||||
assertEquals(ParseError.UNEXPECTED_TOKEN, error);
|
||||
assertEquals(new Token(TokenType.RIGHT_PARENTHESIS, ")", 8), error.getCause());
|
||||
assertEquals(new Token(TokenType.RIGHT_PARENTHESIS, ")", 8), error.getCause().get());
|
||||
parser = new LambdaParser("let x = y )");
|
||||
error = parser.parse().unwrapError();
|
||||
assertEquals(ParseError.UNEXPECTED_TOKEN, error);
|
||||
assertEquals(new Token(TokenType.RIGHT_PARENTHESIS, ")", 10), error.getCause());
|
||||
assertEquals(new Token(TokenType.RIGHT_PARENTHESIS, ")", 10), error.getCause().get());
|
||||
parser = new LambdaParser("let x = y in )");
|
||||
error = parser.parse().unwrapError();
|
||||
assertEquals(ParseError.UNEXPECTED_TOKEN, error);
|
||||
assertEquals(new Token(TokenType.RIGHT_PARENTHESIS, ")", 13), error.getCause());
|
||||
assertEquals(new Token(TokenType.RIGHT_PARENTHESIS, ")", 13), error.getCause().get());
|
||||
}
|
||||
|
||||
@Test
|
||||
|
@ -210,7 +210,7 @@ class TypeAssumptionParserTest {
|
||||
Result<Map<VarTerm, TypeAbstraction>, ParseError> type = parser.parse(Map.of("type1", entry.getKey()));
|
||||
assertTrue(type.isError());
|
||||
assertEquals(entry.getValue(), type.unwrapError());
|
||||
if (entry.getValue().getCause().getPos() != -1) {
|
||||
if (entry.getValue().getCause().isPresent()) {
|
||||
assertEquals(entry.getValue().getCause(), type.unwrapError().getCause());
|
||||
}
|
||||
}
|
||||
|
Loading…
Reference in New Issue
Block a user