Correctly scope variables in type assumptions

src/main/java/edu/kit/typicalc/model/parser/TypeAssumptionParser.java

@@ -213,7 +213,7 @@ public class TypeAssumptionParser {
                         }
                     }
                     // attempt to parse as type
-                    ParserResult<Type> result = new ParseTypeState1().handle(t);
+                    ParserResult<Type> result = new ParseTypeState1(alreadyParsed.size()).handle(t);
                     if (result.isError()) {
                         return result.castError();
                     }
@@ -254,6 +254,15 @@ public class TypeAssumptionParser {
         private int parenthesisInitial = 0;
         private int openParens = 0;
 
+        /**
+         * Attached to any parsed type variables.
+         */
+        private final int typeVariableUniqueIndex;
+
+        ParseTypeState1(int typeVariableUniqueIndex) {
+            this.typeVariableUniqueIndex = typeVariableUniqueIndex;
+        }
+
         @Override
         public ParserResult<Type> handle(Token t) {
             switch (t.getType()) {
@@ -284,7 +293,7 @@ public class TypeAssumptionParser {
                                 .withToken(t, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR));
                     }
                     // parse function type
-                    state = Optional.of(new ParseTypeStateExpectArrow().handle(t).getState());
+                    state = Optional.of(new ParseTypeStateExpectArrow(typeVariableUniqueIndex).handle(t).getState());
                     return new ParserResult<>(this);
                 case LEFT_PARENTHESIS:
                     openParens += 1;
@@ -294,7 +303,7 @@ public class TypeAssumptionParser {
                     if (stateParenthesis.isPresent()) {
                         return handleInnerParenthesis(t);
                     }
-                    stateParenthesis = Optional.of(new ParseTypeState1());
+                    stateParenthesis = Optional.of(new ParseTypeState1(typeVariableUniqueIndex));
                     parenthesisInitial = openParens - 1;
                     return new ParserResult<>(this);
                 case RIGHT_PARENTHESIS:
@@ -372,11 +381,13 @@ public class TypeAssumptionParser {
             }
         }
 
-        private static Type parseLiteral(String text) {
+        private Type parseLiteral(String text) {
             Matcher typeVariableMatcher = TYPE_VARIABLE_PATTERN.matcher(text);
             if (typeVariableMatcher.matches()) {
                 int typeVariableIndex = Integer.parseInt(typeVariableMatcher.group(1));
-                return new TypeVariable(TypeVariableKind.USER_INPUT, typeVariableIndex);
+                TypeVariable var = new TypeVariable(TypeVariableKind.USER_INPUT, typeVariableIndex);
+                var.setUniqueIndex(typeVariableUniqueIndex);
+                return var;
             } else {
                 return new NamedType(text);
             }
@@ -386,13 +397,22 @@ public class TypeAssumptionParser {
     private static class ParseTypeStateExpectArrow implements ParserState<Type> {
         private Optional<ParserState<Type>> state = Optional.empty();
 
+        /**
+         * Attached to any parsed type variables.
+         */
+        private final int typeVariableUniqueIndex;
+
+        ParseTypeStateExpectArrow(int typeVariableUniqueIndex) {
+            this.typeVariableUniqueIndex = typeVariableUniqueIndex;
+        }
+
         @Override
         public ParserResult<Type> handle(Token t) {
             switch (t.getType()) {
                 case ARROW:
                     if (state.isEmpty()) {
                         // try parsing remainder as type
-                        state = Optional.of(new ParseTypeState1());
+                        state = Optional.of(new ParseTypeState1(typeVariableUniqueIndex));
                         return new ParserResult<>(this);
                     }
                 default:
@@ -446,6 +466,7 @@ public class TypeAssumptionParser {
                         return new ParserResult<>(ParseError.UNEXPECTED_TOKEN
                                 .withToken(t, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR));
                     }
+                    variable.setUniqueIndex(alreadyParsed.size());
                     variables.add(variable);
                     expectCommaOrDot = true;
                     return new ParserResult<>(this);

src/main/java/edu/kit/typicalc/model/type/TypeVariable.java

@@ -13,6 +13,11 @@ public class TypeVariable extends Type implements Comparable<TypeVariable> {
     private final TypeVariableKind kind;
     private final int index;
 
+    /**
+     * The same type variable can be universally quantified multiple times, but this index will differ.
+     */
+    private int uniqueIndex;
+
     /**
      * Initializes a new TypeVariable with the given index.
      *
@@ -42,6 +47,14 @@ public class TypeVariable extends Type implements Comparable<TypeVariable> {
         return index;
     }
 
+    public void setUniqueIndex(int uniqueIndex) {
+        this.uniqueIndex = uniqueIndex;
+    }
+
+    public int getUniqueIndex() {
+        return uniqueIndex;
+    }
+
     /**
      * Checks whether some type occurs in this type.
      *

src/test/java/edu/kit/typicalc/model/parser/TypeAssumptionParserTest.java

@@ -239,6 +239,24 @@ class TypeAssumptionParserTest {
         assertEquals(10, error.getCause().get().getPos());
     }
 
+    @Test
+    void correctlyScopesQuantifiedTypeVariables() {
+        TypeAssumptionParser parser = new TypeAssumptionParser();
+        Result<Map<VarTerm, TypeAbstraction>, ParseError> type =
+                parser.parse("id: ∀ t1 . t1 -> t1, fun: ∀t1,t2.t1->t2 ");
+        assertTrue(type.isOk());
+        Map<VarTerm, TypeAbstraction> res = type.unwrap();
+        TypeAbstraction id = res.get(new VarTerm("id"));
+        TypeVariable[] idVariables = id.getQuantifiedVariables().toArray(new TypeVariable[0]);
+        assertEquals(0, idVariables[0].getUniqueIndex());
+        TypeAbstraction fun = res.get(new VarTerm("fun"));
+        TypeVariable[] funVariables = fun.getQuantifiedVariables().toArray(new TypeVariable[0]);
+        assertEquals(1, funVariables[0].getUniqueIndex());
+        assertEquals(1, funVariables[1].getUniqueIndex());
+        assertEquals(1, ((TypeVariable) ((FunctionType) fun.getInnerType()).getParameter()).getUniqueIndex());
+        assertEquals(1, ((TypeVariable) ((FunctionType) fun.getInnerType()).getOutput()).getUniqueIndex());
+    }
+
     @Test
     void errors() {
         Map<String, ParseError> tests = new HashMap<>();