Fix type parser bug

This commit is contained in:
Arne Keller 2021-02-10 15:01:03 +01:00
parent f1fe6fce02
commit c1ce7a9181
2 changed files with 26 additions and 7 deletions

View File

@ -12,10 +12,12 @@ import java.util.Map;
import java.util.regex.Matcher; import java.util.regex.Matcher;
import java.util.regex.Pattern; import java.util.regex.Pattern;
public class TypeAssumptionParser { /**
* Parser for type assumptions.
*/
public class TypeAssumptionParser { // TODO: document type syntax? or refer to other documents
private static final String TYPE_VARIABLE_PATTERN = "t(\\d+)"; private static final Pattern TYPE_VARIABLE_PATTERN = Pattern.compile("t(\\d+)");
private static final int GRPUP_CONTAINING_INDEX = 1;
public Result<Map<VarTerm, TypeAbstraction>, ParseError> parse(Map<String, String> oldAssumptions) { public Result<Map<VarTerm, TypeAbstraction>, ParseError> parse(Map<String, String> oldAssumptions) {
Map<VarTerm, TypeAbstraction> typeAssumptions = new HashMap<>(); Map<VarTerm, TypeAbstraction> typeAssumptions = new HashMap<>();
@ -61,10 +63,9 @@ public class TypeAssumptionParser {
} }
break; break;
case VARIABLE: case VARIABLE:
Pattern typeVariablePattern = Pattern.compile(TYPE_VARIABLE_PATTERN); Matcher typeVariableMatcher = TYPE_VARIABLE_PATTERN.matcher(t.getText());
Matcher typeVariableMatcher = typeVariablePattern.matcher(t.getText());
if (typeVariableMatcher.matches()) { if (typeVariableMatcher.matches()) {
int typeVariableIndex = Integer.parseInt(typeVariableMatcher.group(GRPUP_CONTAINING_INDEX)); int typeVariableIndex = Integer.parseInt(typeVariableMatcher.group(1));
type = new TypeVariable(TypeVariableKind.USER_INPUT, typeVariableIndex); type = new TypeVariable(TypeVariableKind.USER_INPUT, typeVariableIndex);
} else { } else {
type = new NamedType(t.getText()); type = new NamedType(t.getText());
@ -100,7 +101,7 @@ public class TypeAssumptionParser {
type = new FunctionType(type, nextType.unwrap().getLeft()); type = new FunctionType(type, nextType.unwrap().getLeft());
removedParens += nextType.unwrap().getRight(); removedParens += nextType.unwrap().getRight();
parenCount -= nextType.unwrap().getRight(); parenCount -= nextType.unwrap().getRight();
if (parenCount < 0) { if (parenCount <= 0) {
return new Result<>(new ImmutablePair<>(type, removedParens)); return new Result<>(new ImmutablePair<>(type, removedParens));
} }
} }

View File

@ -174,4 +174,22 @@ class TypeAssumptionParserTest {
) )
)), assumption.getValue()); )), assumption.getValue());
} }
@Test
void longFunction() {
TypeAssumptionParser parser = new TypeAssumptionParser();
HashMap<String, String> assumptions = new HashMap<>();
assumptions.put("fun", "(a -> b -> c) -> d");
Result<Map<VarTerm, TypeAbstraction>, ParseError> type = parser.parse(assumptions);
assertTrue(type.isOk());
Map<VarTerm, TypeAbstraction> types = type.unwrap();
assertEquals(1, types.size());
Map.Entry<VarTerm, TypeAbstraction> assumption = types.entrySet().stream().findFirst().get();
assertEquals(new VarTerm("fun"), assumption.getKey());
assertEquals(new TypeAbstraction(
new FunctionType(
new FunctionType(new NamedType("a"), new FunctionType(new NamedType("b"), new NamedType("c"))),
new NamedType("d")
)), assumption.getValue());
}
} }