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

Friendly error message for "λx.x in x"

Browse Source
This commit is contained in:
Arne Keller 2021-07-19 11:24:57 +02:00
parent 35013bd819
commit ed7ce73679
3 changed files with 20 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -92,7 +92,7 @@ public class LambdaParser {
} }
return new Result<>(null, return new Result<>(null,
ParseError.unexpectedToken(last, ParseError.ErrorType.TERM_ERROR) ParseError.unexpectedToken(last, ParseError.ErrorType.TERM_ERROR)
.expectedTypes(ATOM_START_TOKENS)); .expectedInput(ExpectedInput.TERM));
} }
/** /**

4
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreator.java
View File

@ -126,8 +126,8 @@ public class LatexCreator implements StepVisitor {
public void visit(AbsStepWithLet absL) { public void visit(AbsStepWithLet absL) {
tree.insert(0, generateConclusion(absL, tree.insert(0, generateConclusion(absL,
mode == LatexCreatorMode.MATHJAX mode == LatexCreatorMode.MATHJAX
? "\\LeftLabel{\\class{typicalc-label typicalc-label-abs-let typicalc-step-" + absL.getStepIndex() ? "\\LeftLabel{\\class{typicalc-label typicalc-label-abs-let typicalc-step-"
+ "}{\\textrm A{\\small BS}}}" : LABEL_ABS, + absL.getStepIndex() + "}{\\textrm A{\\small BS}}}" : LABEL_ABS,
UIC)); UIC));
absL.getPremise().accept(this); absL.getPremise().accept(this);
} }

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

@ -21,6 +21,7 @@ class LambdaParserTest {
term = parser.parse(); term = parser.parse();
assertEquals(new AppTerm(new VarTerm("b1"), new VarTerm("a1")), term.unwrap()); assertEquals(new AppTerm(new VarTerm("b1"), new VarTerm("a1")), term.unwrap());
} }
@Test @Test
void absTerm() { void absTerm() {
LambdaParser parser = new LambdaParser("λx.x"); LambdaParser parser = new LambdaParser("λx.x");
@ -28,6 +29,7 @@ class LambdaParserTest {
assertEquals(new AbsTerm(new VarTerm("x"), new VarTerm("x")), term); assertEquals(new AbsTerm(new VarTerm("x"), new VarTerm("x")), term);
assertEquals("λx.x", term.toString()); assertEquals("λx.x", term.toString());
} }
@Test @Test
void appTerm() { void appTerm() {
LambdaParser parser = new LambdaParser("(λx.x)(λx.x)"); LambdaParser parser = new LambdaParser("(λx.x)(λx.x)");
@ -39,6 +41,7 @@ class LambdaParserTest {
); );
assertEquals("(λx.x)(λx.x)", term.toString()); assertEquals("(λx.x)(λx.x)", term.toString());
} }
@Test @Test
void letTerm() { void letTerm() {
LambdaParser parser = new LambdaParser("let id = λx.x in id 1"); LambdaParser parser = new LambdaParser("let id = λx.x in id 1");
@ -57,6 +60,7 @@ class LambdaParserTest {
parser.parse().unwrap() parser.parse().unwrap()
); );
} }
@Test @Test
void complicatedTerm() { void complicatedTerm() {
LambdaParser parser = new LambdaParser("(λx.λy.x y 5)(λz.z)(true)"); LambdaParser parser = new LambdaParser("(λx.λy.x y 5)(λz.z)(true)");
@ -144,7 +148,7 @@ class LambdaParserTest {
parser = new LambdaParser("let x = )"); parser = new LambdaParser("let x = )");
error = parser.parse().unwrapError(); error = parser.parse().unwrapError();
assertEquals(ParseError.ErrorCause.UNEXPECTED_TOKEN, error.getCauseEnum()); assertEquals(ParseError.ErrorCause.UNEXPECTED_TOKEN, error.getCauseEnum());
assertEquals(new Token(TokenType.RIGHT_PARENTHESIS, ")", "let x = )",8), error.getCause().get()); assertEquals(new Token(TokenType.RIGHT_PARENTHESIS, ")", "let x = )", 8), error.getCause().get());
parser = new LambdaParser("let x = y )"); parser = new LambdaParser("let x = y )");
error = parser.parse().unwrapError(); error = parser.parse().unwrapError();
assertEquals(ParseError.ErrorCause.UNEXPECTED_TOKEN, error.getCauseEnum()); assertEquals(ParseError.ErrorCause.UNEXPECTED_TOKEN, error.getCauseEnum());
@ -177,8 +181,8 @@ class LambdaParserTest {
System.err.println(term.unwrapError().getCause()); System.err.println(term.unwrapError().getCause());
} }
assertEquals(new AppTerm( assertEquals(new AppTerm(
new AbsTerm(X, X), new AbsTerm(X, X),
new LetTerm(new VarTerm("id"), new AbsTerm(Y, Y), new VarTerm("id")) new LetTerm(new VarTerm("id"), new AbsTerm(Y, Y), new VarTerm("id"))
), ),
term.unwrap()); term.unwrap());
} }
@ -246,6 +250,16 @@ class LambdaParserTest {
assertNotEquals(err2, err3); assertNotEquals(err2, err3);
} }
@Test
void errorCase4() {
ParseError err = getParseError("λx.x in x");
assertEquals(ParseError
.unexpectedToken(
new Token(TokenType.IN, "in", "λx.x in x", 5),
ParseError.ErrorType.TERM_ERROR)
.expectedInput(ExpectedInput.TERM), err);
}
@Test @Test
void equality() { void equality() {
EqualsVerifier.forClass(Token.class).usingGetClass().verify(); EqualsVerifier.forClass(Token.class).usingGetClass().verify();