mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-08 18:30:42 +00:00
Fix parsing of (λx.x)λx.x
This commit is contained in:
parent
b87e444f0b
commit
62d7c9f5e1
@ -107,6 +107,8 @@ public class LambdaParser {
|
||||
return new Result<>(let);
|
||||
}
|
||||
return new Result<>(let.unwrap());
|
||||
case VARIABLE:
|
||||
return new Result<>(parseApplication());
|
||||
case EOF:
|
||||
return new Result<>(null, ParseError.TOO_FEW_TOKENS);
|
||||
default:
|
||||
@ -140,8 +142,13 @@ public class LambdaParser {
|
||||
if (left.isError()) {
|
||||
return left;
|
||||
}
|
||||
while (ATOM_START_TOKENS.contains(token.getType())) {
|
||||
Result<LambdaTerm, ParseError> atom = parseAtom();
|
||||
while (ATOM_START_TOKENS.contains(token.getType()) || token.getType() == TokenType.LAMBDA) {
|
||||
Result<LambdaTerm, ParseError> atom;
|
||||
if (token.getType() == TokenType.LAMBDA) {
|
||||
atom = new Result<>(parseAbstraction());
|
||||
} else {
|
||||
atom = parseAtom();
|
||||
}
|
||||
if (atom.isError()) {
|
||||
return atom;
|
||||
}
|
||||
|
@ -71,7 +71,7 @@ public class Result<T, E> {
|
||||
*/
|
||||
public T unwrap() throws IllegalStateException {
|
||||
if (value == null) {
|
||||
throw new IllegalStateException("tried to unwrap an error");
|
||||
throw new IllegalStateException("tried to unwrap a result, but error = " + error);
|
||||
}
|
||||
return value;
|
||||
}
|
||||
@ -85,7 +85,7 @@ public class Result<T, E> {
|
||||
*/
|
||||
public E unwrapError() {
|
||||
if (error == null) {
|
||||
throw new IllegalStateException("tried to unwrap a value");
|
||||
throw new IllegalStateException("tried to unwrap the error, but value = " + value);
|
||||
}
|
||||
return error;
|
||||
}
|
||||
|
@ -15,6 +15,8 @@ import nl.jqno.equalsverifier.EqualsVerifier;
|
||||
import org.junit.jupiter.api.Test;
|
||||
|
||||
class LambdaParserTest {
|
||||
private static final VarTerm X = new VarTerm("x");
|
||||
|
||||
@Test
|
||||
void varTerm() {
|
||||
LambdaParser parser = new LambdaParser("x");
|
||||
@ -63,6 +65,11 @@ class LambdaParserTest {
|
||||
@Test
|
||||
void complicatedTerm() {
|
||||
LambdaParser parser = new LambdaParser("(λx.λy.x y 5)(λz.z)(true)");
|
||||
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(
|
||||
@ -86,7 +93,7 @@ class LambdaParserTest {
|
||||
),
|
||||
new BooleanTerm(true)
|
||||
),
|
||||
parser.parse().unwrap()
|
||||
term.unwrap()
|
||||
);
|
||||
}
|
||||
@Test
|
||||
@ -139,6 +146,17 @@ class LambdaParserTest {
|
||||
assertEquals(new Token(TokenType.RIGHT_PARENTHESIS, ")", 13), error.getCause());
|
||||
}
|
||||
|
||||
@Test
|
||||
void bugFoundByThomas() {
|
||||
LambdaParser parser = new LambdaParser("(λ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 AbsTerm(X, X), new AbsTerm(X, X)), term.unwrap());
|
||||
}
|
||||
|
||||
@Test
|
||||
void equality() {
|
||||
EqualsVerifier.forClass(Token.class).usingGetClass().verify();
|
||||
|
Loading…
Reference in New Issue
Block a user