diff --git a/src/main/java/edu/kit/typicalc/model/parser/TypeAssumptionParser.java b/src/main/java/edu/kit/typicalc/model/parser/TypeAssumptionParser.java index b9ff37d..7e30cf8 100644 --- a/src/main/java/edu/kit/typicalc/model/parser/TypeAssumptionParser.java +++ b/src/main/java/edu/kit/typicalc/model/parser/TypeAssumptionParser.java @@ -441,7 +441,12 @@ public class TypeAssumptionParser { .withToken(t, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR)); } 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; return new ParserResult<>(this); case COMMA: diff --git a/src/test/java/edu/kit/typicalc/model/parser/TypeAssumptionParserTest.java b/src/test/java/edu/kit/typicalc/model/parser/TypeAssumptionParserTest.java index ac37554..9cc99b5 100644 --- a/src/test/java/edu/kit/typicalc/model/parser/TypeAssumptionParserTest.java +++ b/src/test/java/edu/kit/typicalc/model/parser/TypeAssumptionParserTest.java @@ -228,6 +228,17 @@ class TypeAssumptionParserTest { assertTrue(expected.contains(Token.TokenType.COMMA)); } + @Test + void doesntAcceptDuplicateQuantifiedVariables() { + TypeAssumptionParser parser = new TypeAssumptionParser(); + Result, 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 void errors() { Map tests = new HashMap<>();