arnekeller/Typicalc
1
0
Fork 0
mirror of https://gitlab.kit.edu/uskyk/typicalc.git synced 2024-11-08 18:30:42 +00:00
Code Issues Packages Projects Releases Wiki Activity

Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc

Browse Source
This commit is contained in:
ucrhh 2021-01-29 10:16:27 +01:00
commit 47a1a36de6
10 changed files with 157 additions and 56 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
frontend/styles/view/main/input-bar.css
View File

@ -9,3 +9,7 @@
width: 30em;
}
}
#inputField {
height: 2.3em;
}

15
pom.xml
View File

@ -8,7 +8,7 @@
<packaging>jar</packaging>
<properties>
<maven.compiler.source>1.8</maven.compiler.source>
<maven.compiler.source>11</maven.compiler.source>
<project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
<project.reporting.outputEncoding>UTF-8</project.reporting.outputEncoding>
@ -116,6 +116,19 @@
<version>5.7.0</version>
<scope>test</scope>
</dependency>
<!-- need these for IntelliJ -->
<dependency>
<groupId>org.junit.platform</groupId>
<artifactId>junit-platform-launcher</artifactId>
<version>1.7.0</version>
<scope>test</scope>
</dependency>
<dependency>
<groupId>org.junit.vintage</groupId>
<artifactId>junit-vintage-engine</artifactId>
<version>5.7.0</version>
<scope>test</scope>
</dependency>
<dependency>
<groupId>com.vaadin.componentfactory</groupId>
<artifactId>tooltip</artifactId>

79
src/main/java/edu/kit/typicalc/model/parser/LambdaParser.java
View File

@ -37,7 +37,6 @@ public class LambdaParser {
*/
public LambdaParser(String term) {
this.lexer = new LambdaLexer(term);
nextToken();
}
/**
@ -58,10 +57,13 @@ public class LambdaParser {
* Returns false otherwise.
* @param type the token type to compare the current token type to
*/
private boolean expect(TokenType type) {
private Optional<ParseError> expect(TokenType type) {
TokenType current = token.getType();
nextToken(); // TODO: Fehlerbehandlung
return current == type;
Optional<ParseError> error = nextToken();
if (current != type) {
return Optional.of(ParseError.UNEXPECTED_TOKEN.withToken(token));
}
return error;
}
/**
@ -69,9 +71,13 @@ public class LambdaParser {
* @return the term given by the String
*/
public Result<LambdaTerm, ParseError> parse() {
Result<LambdaTerm, ParseError> t = parseTerm();
if (!expect(TokenType.EOF)) {
return new Result<>(null, ParseError.TOO_MANY_TOKENS);
Result<LambdaTerm, ParseError> t = parseTerm(true);
if (t.isError()) {
return t;
}
Optional<ParseError> next = expect(TokenType.EOF);
if (next.isPresent()) {
return new Result<>(null, next.get());
}
return t;
}
@ -80,7 +86,13 @@ public class LambdaParser {
* Parses a term.
* @return the term, or an error
*/
private Result<LambdaTerm, ParseError> parseTerm() {
private Result<LambdaTerm, ParseError> parseTerm(boolean next) {
if (next) {
Optional<ParseError> error = nextToken();
if (error.isPresent()) {
return new Result<>(null, error.get());
}
}
switch (token.getType()) {
case LAMBDA:
Result<AbsTerm, ParseError> abs = parseAbstraction();
@ -98,10 +110,11 @@ public class LambdaParser {
private Result<AbsTerm, ParseError> parseAbstraction() {
nextToken();
Result<VarTerm, ParseError> var = parseVar();
if (!expect(TokenType.DOT)) {
return new Result<>(null, ParseError.UNEXPECTED_TOKEN);
Optional<ParseError> next = expect(TokenType.DOT);
if (next.isPresent()) {
return new Result<>(null, next.get());
}
Result<LambdaTerm, ParseError> body = parseTerm();
Result<LambdaTerm, ParseError> body = parseTerm(false);
// TODO: Fehlerbehandlung
return new Result<>(new AbsTerm(var.unwrap(), body.unwrap()));
}
@ -111,22 +124,37 @@ public class LambdaParser {
* @return the term, or an error
*/
private Result<LambdaTerm, ParseError> parseApplication() {
LambdaTerm left = parseAtom().unwrap(); // TODO: Fehlerbehandlung
while (ATOM_START_TOKENS.contains(token.getType())) {
LambdaTerm atom = parseAtom().unwrap(); // TODO: Fehlerbehandlung
left = new AppTerm(left, atom);
Result<LambdaTerm, ParseError> left = parseAtom();
if (left.isError()) {
return left;
}
return new Result<>(left);
while (ATOM_START_TOKENS.contains(token.getType())) {
Result<LambdaTerm, ParseError> atom = parseAtom();
if (atom.isError()) {
return atom;
}
left = new Result<>(new AppTerm(left.unwrap(), atom.unwrap()));
}
return left;
}
private Result<LetTerm, ParseError> parseLet() {
// TODO: Fehlerbehandlung
expect(TokenType.LET);
Optional<ParseError> error = expect(TokenType.LET);
if (error.isPresent()) {
return new Result<>(null, error.get());
}
VarTerm var = parseVar().unwrap();
expect(TokenType.EQ);
LambdaTerm def = parseTerm().unwrap();
expect(TokenType.IN);
LambdaTerm body = parseTerm().unwrap();
error = expect(TokenType.EQ);
if (error.isPresent()) {
return new Result<>(null, error.get());
}
LambdaTerm def = parseTerm(false).unwrap();
error = expect(TokenType.IN);
if (error.isPresent()) {
return new Result<>(null, error.get());
}
LambdaTerm body = parseTerm(false).unwrap();
return new Result<>(new LetTerm(var, def, body));
}
@ -145,7 +173,7 @@ public class LambdaParser {
try {
n = Integer.parseInt(number);
} catch (NumberFormatException e) {
return new Result<>(null, ParseError.UNEXPECTED_CHARACTER);
return new Result<>(null, ParseError.UNEXPECTED_CHARACTER.withToken(token));
}
nextToken();
return new Result<>(new IntegerTerm(n));
@ -157,7 +185,7 @@ public class LambdaParser {
return new Result<>(new BooleanTerm(b));
default:
expect(TokenType.LP);
Result<LambdaTerm, ParseError> term = parseTerm();
Result<LambdaTerm, ParseError> term = parseTerm(false);
expect(TokenType.RP);
return term;
}
@ -165,8 +193,9 @@ public class LambdaParser {
private Result<VarTerm, ParseError> parseVar() {
String s = token.getText();
if (!expect(TokenType.VARIABLE)) {
return new Result<>(null, ParseError.UNEXPECTED_TOKEN);
Optional<ParseError> next = expect(TokenType.VARIABLE);
if (next.isPresent()) {
return new Result<>(null, next.get());
}
return new Result<>(new VarTerm(s));
}

25
src/main/java/edu/kit/typicalc/model/parser/ParseError.java
View File

@ -7,11 +7,6 @@ public enum ParseError {
*/
UNEXPECTED_TOKEN,
/**
* some tokens were remaining after parsing a full lambda term
*/
TOO_MANY_TOKENS,
/**
* some tokens were required, but not provided
*/
@ -20,5 +15,23 @@ public enum ParseError {
/**
* the string contained a character not allowed in that context
*/
UNEXPECTED_CHARACTER
UNEXPECTED_CHARACTER;
private Token cause;
public ParseError withToken(Token cause) {
this.cause = cause;
return this;
}
/**
* @return the token associated with this error, or null if none
*/
public Token getCause() { // TODO: document
return cause;
}
ParseError() {
}
}

2
src/main/java/edu/kit/typicalc/view/TypicalcI18NProvider.java
View File

@ -51,7 +51,7 @@ public class TypicalcI18NProvider implements I18NProvider {
translation = this.generalBundle.getString(key);
} catch (final MissingResourceException exception) {
// this should never be the case
return key;
return "?[" + key + "]?";
}
}

32
src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java Normal file
View File

@ -0,0 +1,32 @@
package edu.kit.typicalc.view.main;
import com.vaadin.flow.component.button.Button;
import com.vaadin.flow.component.dialog.Dialog;
import com.vaadin.flow.component.html.Paragraph;
import com.vaadin.flow.component.orderedlayout.VerticalLayout;
import com.vaadin.flow.i18n.LocaleChangeEvent;
import com.vaadin.flow.i18n.LocaleChangeObserver;
import java.util.List;
import java.util.function.Consumer;
public class ExampleDialog extends Dialog implements LocaleChangeObserver {
private static final List<String> EXAMPLES =
List.of("λx.x", "λx.λy.y x", "λx.λy.y (x x)", "let f = λx. g y y in f 3", "(λx.x x) (λx.x x)");
public ExampleDialog(Consumer<String> callback) {
VerticalLayout layout = new VerticalLayout();
layout.add(new Paragraph(getTranslation("root.selectExample")));
for (String term : EXAMPLES) {
Button button = new Button(term);
button.addClickListener(click -> callback.accept(term));
layout.add(button);
}
add(layout);
}
@Override
public void localeChange(LocaleChangeEvent event) {
// TODO
}
}

41
src/main/java/edu/kit/typicalc/view/main/InputBar.java
View File

@ -2,13 +2,14 @@ package edu.kit.typicalc.view.main;
import java.util.Optional;
import java.util.function.Consumer;
import com.vaadin.flow.component.textfield.TextArea;
import org.apache.commons.lang3.StringUtils;
import com.vaadin.componentfactory.Tooltip;
import com.vaadin.componentfactory.TooltipAlignment;
import com.vaadin.componentfactory.TooltipPosition;
import com.vaadin.flow.component.button.Button;
import com.vaadin.flow.component.button.ButtonVariant;
import com.vaadin.flow.component.combobox.ComboBox;
import com.vaadin.flow.component.dependency.CssImport;
import com.vaadin.flow.component.html.H5;
import com.vaadin.flow.component.icon.Icon;
@ -26,8 +27,9 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
private final Tooltip infoTooltip;
private final Icon infoIcon;
private final Button exampleButton;
private final Button lambdaButton;
private final ComboBox<String> inputField;
private final TextArea inputField;
private final Button inferTypeButton;
/**
@ -45,13 +47,23 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
infoTooltip.setPosition(TooltipPosition.BOTTOM);
infoTooltip.setAlignment(TooltipAlignment.TOP);
inputField = new ComboBox<>();
initComboBox();
inputField = new TextArea();
inputField.setId("inputField");
inputField.setClearButtonVisible(true);
//TODO seems to be the only solution to "immediately" parse backslash
inputField.addValueChangeListener(event -> {
if (inputField.getOptionalValue().isPresent()) {
String value = inputField.getValue();
value = value.replace("\\", "λ");
inputField.setValue(value);
}
});
lambdaButton = new Button(getTranslation("root.lambda"), event -> onlambdaButtonClick());
exampleButton = new Button(getTranslation("root.examplebutton"), event -> onExampleButtonClick());
inferTypeButton = new Button(getTranslation("root.typeInfer"), event -> onTypeInferButtonClick(callback));
inferTypeButton.addThemeVariants(ButtonVariant.LUMO_PRIMARY);
add(infoIcon, infoTooltip, lambdaButton, inputField, inferTypeButton);
add(infoIcon, infoTooltip, exampleButton, lambdaButton, inputField, inferTypeButton);
setAlignItems(FlexComponent.Alignment.CENTER);
}
@ -69,22 +81,9 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
inputField.focus();
}
private void initComboBox() {
//TODO remove magic string in this method (used for demo)
inputField.setId("inputField");
inputField.setClearButtonVisible(true);
inputField.setAllowCustomValue(true);
inputField.setItems("λx.x", "λx.λy.y x", "λx.λy.y (x x)", "let f = λx. g y y in f 3", "(λx.x x) (λx.x x)");
inputField.addCustomValueSetListener(event -> inputField.setValue(event.getDetail()));
//TODO seems to be the only solution to "immediately" parse backslash
inputField.addValueChangeListener(event -> {
if (inputField.getOptionalValue().isPresent()) {
String value = inputField.getValue();
value = value.replace("\\", "λ");
inputField.setValue(value);
}
});
private void onExampleButtonClick() {
ExampleDialog exampleDialog = new ExampleDialog(inputField::setValue);
exampleDialog.open();
}
private void initInfoTooltip() {

2
src/main/resources/language/translation_de.properties
View File

@ -2,6 +2,8 @@ root.close=Schließen
root.copyLatex=Kopiere Latex-Code
root.typicalc=Typicalc
root.lambda=\u03BB
root.examplebutton=📂
root.selectExample=Beispiel auswählen:
root.typeInfer=Typisieren
abs-rule=\

4
src/main/resources/language/translation_en.properties
View File

@ -2,7 +2,9 @@ root.close=Close
root.copyLatex=Copy latex code
root.typicalc=Typicalc
root.lambda=\u03BB
root.typeInfer=Typisieren
root.examplebutton=📂
root.selectExample=Select example:
root.typeInfer=Type
abs-rule=\
\\begin{prooftree}\n\

9
src/test/java/edu/kit/typicalc/model/parser/LambdaParserTest.java
View File

@ -17,7 +17,6 @@ class LambdaParserTest {
void varTerm() {
LambdaParser parser = new LambdaParser("x");
Result<LambdaTerm, ParseError> term = parser.parse();
System.out.println(term);
assertEquals(new VarTerm("x"), term.unwrap());
}
@Test
@ -85,5 +84,13 @@ class LambdaParserTest {
void miscellaneousTerms() {
LambdaParser parser = new LambdaParser("");
assertEquals(ParseError.TOO_FEW_TOKENS, parser.parse().unwrapError());
parser = new LambdaParser("x)");
assertEquals(ParseError.UNEXPECTED_TOKEN, parser.parse().unwrapError());
parser = new LambdaParser("??");
assertEquals(ParseError.UNEXPECTED_CHARACTER, parser.parse().unwrapError());
parser = new LambdaParser("123333333333333");
assertEquals(ParseError.UNEXPECTED_CHARACTER, parser.parse().unwrapError());
parser = new LambdaParser("x 123333333333333");
assertEquals(ParseError.UNEXPECTED_CHARACTER, parser.parse().unwrapError());
}
}