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

Browse Source
This commit is contained in:
Johanna Stuber 2021-02-20 21:16:27 +01:00
commit c115baa4d4
6 changed files with 58 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
src/main/java/edu/kit/typicalc/model/parser/TypeAssumptionParser.java
View File

@ -15,13 +15,19 @@ import java.util.regex.Pattern;
/**
* Parser for type assumptions.
*/
public class TypeAssumptionParser { // TODO: document type syntax? or refer to other documents
public class TypeAssumptionParser {
private static final Pattern TYPE_VARIABLE_PATTERN = Pattern.compile("t(\\d+)");
public Result<Map<VarTerm, TypeAbstraction>, ParseError> parse(Map<String, String> oldAssumptions) {
/**
* Parse the given type assumptions.
*
* @param assumptions the type assumptions
* @return if successful, a map of the type assumptions, otherwise an error
*/
public Result<Map<VarTerm, TypeAbstraction>, ParseError> parse(Map<String, String> assumptions) {
Map<VarTerm, TypeAbstraction> typeAssumptions = new LinkedHashMap<>();
for (Map.Entry<String, String> entry : oldAssumptions.entrySet()) {
for (Map.Entry<String, String> entry : assumptions.entrySet()) {
VarTerm var = new VarTerm(entry.getKey());
Result<TypeAbstraction, ParseError> typeAbs = parseType(entry.getValue());
if (typeAbs.isError()) {
@ -81,13 +87,19 @@ public class TypeAssumptionParser { // TODO: document type syntax? or refer to o
t = token.unwrap();
if (t.getType() == TokenType.RIGHT_PARENTHESIS) {
removedParens += 1;
if (parenCount - removedParens <= 0) {
if (parenCount - removedParens < 0) {
return new Result<>(null, ParseError.UNEXPECTED_TOKEN.withToken(t));
} else if (parenCount - removedParens == 0) {
return new Result<>(new ImmutablePair<>(type, removedParens));
}
continue;
}
if (t.getType() == TokenType.EOF) {
return new Result<>(new ImmutablePair<>(type, removedParens));
if (parenCount - removedParens > 0) {
return new Result<>(null, ParseError.TOO_FEW_TOKENS);
} else {
return new Result<>(new ImmutablePair<>(type, removedParens));
}
}
if (t.getType() != TokenType.ARROW) {
return new Result<>(null, ParseError.UNEXPECTED_TOKEN.withToken(t));
@ -98,7 +110,9 @@ public class TypeAssumptionParser { // TODO: document type syntax? or refer to o
}
type = new FunctionType(type, nextType.unwrap().getLeft());
removedParens += nextType.unwrap().getRight();
if (parenCount - removedParens <= 0) {
if (parenCount - removedParens < 0) {
return new Result<>(null, ParseError.UNEXPECTED_TOKEN.withToken(t));
} else if (parenCount - removedParens == 0) {
return new Result<>(new ImmutablePair<>(type, removedParens));
}
}

12
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/ShareDialog.java
View File

@ -2,6 +2,7 @@ package edu.kit.typicalc.view.content.typeinferencecontent;
import com.vaadin.flow.component.dependency.CssImport;
import com.vaadin.flow.component.dialog.Dialog;
import com.vaadin.flow.component.html.H3;
import com.vaadin.flow.component.orderedlayout.VerticalLayout;
import com.vaadin.flow.component.textfield.TextArea;
import com.vaadin.flow.component.textfield.TextField;
@ -20,6 +21,7 @@ public class ShareDialog extends Dialog implements LocaleChangeObserver {
private final TextField urlField;
private final TextField packageField;
private final TextArea latexArea;
private final H3 heading;
/**
* Sets up three GUI elements, one for each parameter. The content of each element is equal
@ -35,9 +37,10 @@ public class ShareDialog extends Dialog implements LocaleChangeObserver {
layout.setId(LAYOUT_ID);
add(layout);
urlField = new TextField(getTranslation("share.url.label"));
packageField = new TextField(getTranslation("share.packages.label"));
latexArea = new TextArea(getTranslation("share.latex.label"));
heading = new H3();
urlField = new TextField();
packageField = new TextField();
latexArea = new TextArea();
urlField.setValue(url);
urlField.setClassName(FIELD_CLASS);
@ -46,12 +49,13 @@ public class ShareDialog extends Dialog implements LocaleChangeObserver {
latexArea.setValue(latexCode);
latexArea.setClassName(FIELD_CLASS);
layout.add(urlField, packageField, latexArea);
layout.add(heading, urlField, packageField, latexArea);
}
@Override
public void localeChange(LocaleChangeEvent localeChangeEvent) {
heading.setText(getTranslation("share.heading"));
urlField.setLabel(getTranslation("share.url.label"));
packageField.setLabel(getTranslation("share.packages.label"));
latexArea.setLabel(getTranslation("share.latex.label"));

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

@ -117,6 +117,7 @@ root.infinite_type = Der eingegebene Term ist nicht typisierbar: \
root.different_types = Der eingegebene Term ist nicht typisierbar: \
In dem hervorgehobenen Constraint werden zwei unvereinbare Typen gleichgesetzt!
share.heading=Teilen
share.url.label=URL
share.packages.label=Pakete
share.latex.label=LaTeX-Code

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

@ -110,6 +110,7 @@ root.infinite_type = The entered term cannot be typed: \
root.different_types = The entered term cannot be typed: \
The highlighted Constraint contains two incompatible types!
share.heading=Share
share.url.label=URL
share.packages.label=Packages
share.latex.label=LaTeX code

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

@ -155,6 +155,17 @@ class LambdaParserTest {
assertEquals(new AppTerm(new AbsTerm(X, X), new AbsTerm(X, X)), term.unwrap());
}
@Test
void complicatedIdentity() {
LambdaParser parser = new LambdaParser("(λx. x) (λx. x) λx. x");
Result<LambdaTerm, ParseError> term = parser.parse();
if (term.isError()) {
System.err.println(term.unwrapError());
System.err.println(term.unwrapError().getCause());
}
assertEquals(new AppTerm(new AppTerm(new AbsTerm(X, X), new AbsTerm(X, X)), new AbsTerm(X, X)), term.unwrap());
}
@Test
void equality() {
EqualsVerifier.forClass(Token.class).usingGetClass().verify();

17
src/test/java/edu/kit/typicalc/model/parser/TypeAssumptionParserTest.java
View File

@ -194,6 +194,22 @@ class TypeAssumptionParserTest {
)), assumption.getValue());
}
@Test
void errors() {
Map<String, ParseError> tests = new HashMap<>();
tests.put("ö", ParseError.UNEXPECTED_CHARACTER);
tests.put("(x", ParseError.TOO_FEW_TOKENS);
tests.put("x 11", ParseError.UNEXPECTED_TOKEN.withToken(new Token(Token.TokenType.NUMBER, "11", 2)));
tests.put("x )", ParseError.UNEXPECTED_TOKEN.withToken(new Token(Token.TokenType.RIGHT_PARENTHESIS, ")", 2)));
tests.put("x -> (x) )", ParseError.UNEXPECTED_TOKEN.withToken(new Token(Token.TokenType.RIGHT_PARENTHESIS, ")", 9)));
for (Map.Entry<String, ParseError> entry : tests.entrySet()) {
TypeAssumptionParser parser = new TypeAssumptionParser();
Result<Map<VarTerm, TypeAbstraction>, ParseError> type = parser.parse(Map.of("type1", entry.getKey()));
assertTrue(type.isError());
assertEquals(entry.getValue(), type.unwrapError());
}
}
@Test
void variousTypes() {
Type x = new NamedType("x");
@ -204,6 +220,7 @@ class TypeAssumptionParserTest {
Type xxxxxx = new FunctionType(xxx, xxx);
Map<String, TypeAbstraction> tests = new HashMap<>();
tests.put("x", new TypeAbstraction(x));
tests.put("( ( x ) )", new TypeAbstraction(x));
tests.put("x -> x", new TypeAbstraction(xx));
tests.put("x -> (x)", new TypeAbstraction(xx));
tests.put("x -> ((x))", new TypeAbstraction(xx));