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

Reject duplicate quantified type variables

Browse Source
This commit is contained in:
Arne Keller 2021-07-09 12:26:18 +02:00
parent df218d8be8
commit 394b5a3d23
2 changed files with 17 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -441,7 +441,12 @@ public class TypeAssumptionParser {
.withToken(t, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR)); .withToken(t, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR));
} }
int i = Integer.parseInt(input.substring(1)); int i = Integer.parseInt(input.substring(1));
variables.add(new TypeVariable(TypeVariableKind.USER_INPUT, i)); TypeVariable variable = new TypeVariable(TypeVariableKind.USER_INPUT, i);
if (variables.contains(variable)) {
return new ParserResult<>(ParseError.UNEXPECTED_TOKEN
.withToken(t, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR));
}
variables.add(variable);
expectCommaOrDot = true; expectCommaOrDot = true;
return new ParserResult<>(this); return new ParserResult<>(this);
case COMMA: case COMMA:

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

@ -228,6 +228,17 @@ class TypeAssumptionParserTest {
assertTrue(expected.contains(Token.TokenType.COMMA)); assertTrue(expected.contains(Token.TokenType.COMMA));
} }
@Test
void doesntAcceptDuplicateQuantifiedVariables() {
TypeAssumptionParser parser = new TypeAssumptionParser();
Result<Map<VarTerm, TypeAbstraction>, ParseError> type = parser.parse("id: ∀ t1, t1 : t1 -> t1");
assertTrue(type.isError());
ParseError error = type.unwrapError();
assertEquals(ParseError.UNEXPECTED_TOKEN, error);
assertEquals(Token.TokenType.VARIABLE, error.getCause().get().getType());
assertEquals(10, error.getCause().get().getPos());
}
@Test @Test
void errors() { void errors() {
Map<String, ParseError> tests = new HashMap<>(); Map<String, ParseError> tests = new HashMap<>();