mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-08 18:30:42 +00:00
TypeAssumptionParser tests
This commit is contained in:
parent
d6bc8bb9cd
commit
27aff112bb
@ -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,14 +87,20 @@ 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) {
|
||||
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));
|
||||
}
|
||||
}
|
||||
|
@ -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();
|
||||
|
@ -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));
|
||||
|
Loading…
Reference in New Issue
Block a user