From 1b70e374acbc835d8c39d3be12c47c00d1be861f Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Fri, 9 Jul 2021 12:46:04 +0200 Subject: [PATCH] Correctly scope variables in type assumptions --- .../model/parser/TypeAssumptionParser.java | 33 +++++++++++++++---- .../kit/typicalc/model/type/TypeVariable.java | 13 ++++++++ .../parser/TypeAssumptionParserTest.java | 18 ++++++++++ 3 files changed, 58 insertions(+), 6 deletions(-) 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 7e30cf8..0c853a2 100644 --- a/src/main/java/edu/kit/typicalc/model/parser/TypeAssumptionParser.java +++ b/src/main/java/edu/kit/typicalc/model/parser/TypeAssumptionParser.java @@ -213,7 +213,7 @@ public class TypeAssumptionParser { } } // attempt to parse as type - ParserResult result = new ParseTypeState1().handle(t); + ParserResult 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 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 { private Optional> state = Optional.empty(); + /** + * Attached to any parsed type variables. + */ + private final int typeVariableUniqueIndex; + + ParseTypeStateExpectArrow(int typeVariableUniqueIndex) { + this.typeVariableUniqueIndex = typeVariableUniqueIndex; + } + @Override public ParserResult 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); diff --git a/src/main/java/edu/kit/typicalc/model/type/TypeVariable.java b/src/main/java/edu/kit/typicalc/model/type/TypeVariable.java index dedf1ae..8e61c64 100644 --- a/src/main/java/edu/kit/typicalc/model/type/TypeVariable.java +++ b/src/main/java/edu/kit/typicalc/model/type/TypeVariable.java @@ -13,6 +13,11 @@ public class TypeVariable extends Type implements Comparable { 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 { return index; } + public void setUniqueIndex(int uniqueIndex) { + this.uniqueIndex = uniqueIndex; + } + + public int getUniqueIndex() { + return uniqueIndex; + } + /** * Checks whether some type occurs in this type. * 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 9cc99b5..cb7bd50 100644 --- a/src/test/java/edu/kit/typicalc/model/parser/TypeAssumptionParserTest.java +++ b/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, ParseError> type = + parser.parse("id: ∀ t1 . t1 -> t1, fun: ∀t1,t2.t1->t2 "); + assertTrue(type.isOk()); + Map 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 tests = new HashMap<>();