From b716b204b3e183e6b3ae7bc0ae1b1290fa1a535a Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Sat, 30 Jan 2021 10:32:15 +0100 Subject: [PATCH] Unification tests, miscellaneous code style fixes --- .../edu/kit/typicalc/model/Constraint.java | 19 +++++ .../edu/kit/typicalc/model/Substitution.java | 24 ++++++ .../kit/typicalc/model/UnificationError.java | 12 +++ .../typicalc/model/parser/LambdaLexer.java | 7 +- .../typicalc/model/parser/LambdaParser.java | 3 +- .../edu/kit/typicalc/model/parser/Token.java | 21 ++++- .../typicalc/model/type/TypeAbstraction.java | 7 +- .../kit/typicalc/model/type/TypeVariable.java | 7 +- .../typicalc/model/type/UnificationUtil.java | 13 +++- .../model/parser/LambdaParserTest.java | 9 ++- .../typicalc/model/type/UnificationTest.java | 77 +++++++++++++++++++ 11 files changed, 184 insertions(+), 15 deletions(-) create mode 100644 src/test/java/edu/kit/typicalc/model/type/UnificationTest.java diff --git a/src/main/java/edu/kit/typicalc/model/Constraint.java b/src/main/java/edu/kit/typicalc/model/Constraint.java index e26d32b..761bf6f 100644 --- a/src/main/java/edu/kit/typicalc/model/Constraint.java +++ b/src/main/java/edu/kit/typicalc/model/Constraint.java @@ -2,6 +2,8 @@ package edu.kit.typicalc.model; import edu.kit.typicalc.model.type.Type; +import java.util.Objects; + /** * Constrains two types to be equal. */ @@ -35,4 +37,21 @@ public class Constraint { return b; } + @Override + public boolean equals(Object o) { + if (this == o) { + return true; + } + if (o == null || getClass() != o.getClass()) { + return false; + } + Constraint that = (Constraint) o; + return (a.equals(that.a) && b.equals(that.b)) + || (a.equals(that.b) && b.equals(that.a)); + } + + @Override + public int hashCode() { + return Objects.hash(a, b); + } } diff --git a/src/main/java/edu/kit/typicalc/model/Substitution.java b/src/main/java/edu/kit/typicalc/model/Substitution.java index e1782b7..0063819 100644 --- a/src/main/java/edu/kit/typicalc/model/Substitution.java +++ b/src/main/java/edu/kit/typicalc/model/Substitution.java @@ -3,6 +3,8 @@ package edu.kit.typicalc.model; import edu.kit.typicalc.model.type.Type; import edu.kit.typicalc.model.type.TypeVariable; +import java.util.Objects; + /** * A substitution specifies that some type should be replaced by a different type. */ @@ -36,4 +38,26 @@ public class Substitution { Type getType() { return b; } + + @Override + public String toString() { + return "Substitution[" + a + " => " + b + "]"; + } + + @Override + public boolean equals(Object o) { + if (this == o) { + return true; + } + if (o == null || getClass() != o.getClass()) { + return false; + } + Substitution that = (Substitution) o; + return a.equals(that.a) && b.equals(that.b); + } + + @Override + public int hashCode() { + return Objects.hash(a, b); + } } diff --git a/src/main/java/edu/kit/typicalc/model/UnificationError.java b/src/main/java/edu/kit/typicalc/model/UnificationError.java index ec69459..070dec4 100644 --- a/src/main/java/edu/kit/typicalc/model/UnificationError.java +++ b/src/main/java/edu/kit/typicalc/model/UnificationError.java @@ -1,6 +1,18 @@ package edu.kit.typicalc.model; +/** + * Errors that can occur during unification. + * + * @see Unification + * @see UnificationStep + */ public enum UnificationError { + /** + * Unification would lead to an infinite type. + */ INFINITE_TYPE, + /** + * Some {@link edu.kit.typicalc.model.type.NamedType} is not equal to another type. + */ DIFFERENT_TYPES } diff --git a/src/main/java/edu/kit/typicalc/model/parser/LambdaLexer.java b/src/main/java/edu/kit/typicalc/model/parser/LambdaLexer.java index 09847f1..61989e9 100644 --- a/src/main/java/edu/kit/typicalc/model/parser/LambdaLexer.java +++ b/src/main/java/edu/kit/typicalc/model/parser/LambdaLexer.java @@ -108,6 +108,7 @@ public class LambdaLexer { return new Result<>(t); default: if (Character.isLetter(c)) { + int startPos = pos; // identifier StringBuilder sb = new StringBuilder(); do { @@ -133,17 +134,17 @@ public class LambdaLexer { type = TokenType.VARIABLE; break; } - return new Result<>(new Token(type, sb.toString(), pos)); + return new Result<>(new Token(type, sb.toString(), startPos)); } else if (Character.isDigit(c)) { + int startPos = pos; // number literal StringBuilder sb = new StringBuilder(); do { sb.append(term.charAt(pos)); advance(); } while (pos < term.length() && Character.isDigit(term.charAt(pos))); - return new Result<>(new Token(TokenType.NUMBER, sb.toString(), pos)); + return new Result<>(new Token(TokenType.NUMBER, sb.toString(), startPos)); } else { - //throw new ParseException("Illegal character '" + term.charAt(pos) + "'"); return new Result<>(null, ParseError.UNEXPECTED_CHARACTER); } } diff --git a/src/main/java/edu/kit/typicalc/model/parser/LambdaParser.java b/src/main/java/edu/kit/typicalc/model/parser/LambdaParser.java index 64d693c..7249298 100644 --- a/src/main/java/edu/kit/typicalc/model/parser/LambdaParser.java +++ b/src/main/java/edu/kit/typicalc/model/parser/LambdaParser.java @@ -58,10 +58,11 @@ public class LambdaParser { * @param type the token type to compare the current token type to */ private Optional expect(TokenType type) { + Token lastToken = token; TokenType current = token.getType(); Optional error = nextToken(); if (current != type) { - return Optional.of(ParseError.UNEXPECTED_TOKEN.withToken(token)); + return Optional.of(ParseError.UNEXPECTED_TOKEN.withToken(lastToken)); } return error; } diff --git a/src/main/java/edu/kit/typicalc/model/parser/Token.java b/src/main/java/edu/kit/typicalc/model/parser/Token.java index 3394e28..5b6c20e 100644 --- a/src/main/java/edu/kit/typicalc/model/parser/Token.java +++ b/src/main/java/edu/kit/typicalc/model/parser/Token.java @@ -1,5 +1,7 @@ package edu.kit.typicalc.model.parser; +import java.util.Objects; + /** * A token of the Prolog language. */ @@ -73,6 +75,23 @@ public class Token { @Override public String toString() { - return type + "(\"" + text + "\")"; + return type + "(\"" + text + "\")[" + pos + "]"; + } + + @Override + public boolean equals(Object o) { + if (this == o) { + return true; + } + if (o == null || getClass() != o.getClass()) { + return false; + } + Token token = (Token) o; + return pos == token.pos && type == token.type && Objects.equals(text, token.text); + } + + @Override + public int hashCode() { + return Objects.hash(type, text, pos); } } diff --git a/src/main/java/edu/kit/typicalc/model/type/TypeAbstraction.java b/src/main/java/edu/kit/typicalc/model/type/TypeAbstraction.java index 805773b..ed96d32 100644 --- a/src/main/java/edu/kit/typicalc/model/type/TypeAbstraction.java +++ b/src/main/java/edu/kit/typicalc/model/type/TypeAbstraction.java @@ -2,6 +2,7 @@ package edu.kit.typicalc.model.type; import edu.kit.typicalc.model.TypeVariableFactory; +import java.util.Collections; import java.util.List; import java.util.Objects; @@ -11,8 +12,8 @@ import java.util.Objects; */ public class TypeAbstraction { - private Type type; - private List quantifiedVariables; + private final Type type; + private final List quantifiedVariables; /** * Initializes a new type abstraction with its type and the type variables bound by * the for-all quantifier. @@ -31,7 +32,7 @@ public class TypeAbstraction { */ public TypeAbstraction(Type type) { this.type = type; - this.quantifiedVariables = null; + this.quantifiedVariables = Collections.emptyList(); } /** 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 0233585..536f4bd 100644 --- a/src/main/java/edu/kit/typicalc/model/type/TypeVariable.java +++ b/src/main/java/edu/kit/typicalc/model/type/TypeVariable.java @@ -115,7 +115,12 @@ public class TypeVariable extends Type { */ @Override public Result constrainEqualToVariable(TypeVariable type) { - return UnificationUtil.variableVariable(this, type); + return UnificationUtil.variableVariable(type, this); + } + + @Override + public String toString() { + return "TypeVariable[" + kind + "_" + index + "]"; } @Override diff --git a/src/main/java/edu/kit/typicalc/model/type/UnificationUtil.java b/src/main/java/edu/kit/typicalc/model/type/UnificationUtil.java index 064489c..fca61d6 100644 --- a/src/main/java/edu/kit/typicalc/model/type/UnificationUtil.java +++ b/src/main/java/edu/kit/typicalc/model/type/UnificationUtil.java @@ -18,8 +18,6 @@ final class UnificationUtil { } - // TODO: check for infinite types - static Result functionFunction(FunctionType a, FunctionType b) { return new Result<>(new UnificationActions(List.of( new Constraint(a.getParameter(), b.getParameter()), @@ -31,6 +29,9 @@ final class UnificationUtil { } static Result functionVariable(FunctionType a, TypeVariable b) { + if (a.contains(b)) { + return new Result<>(null, UnificationError.INFINITE_TYPE); + } return new Result<>(new UnificationActions(Collections.emptyList(), Optional.of(new Substitution(b, a)))); } @@ -41,8 +42,12 @@ final class UnificationUtil { } static Result variableVariable(TypeVariable a, TypeVariable b) { - return new Result<>(new UnificationActions(Collections.emptyList(), - Optional.of(new Substitution(a, b)))); + if (!a.equals(b)) { + return new Result<>(new UnificationActions(Collections.emptyList(), + Optional.of(new Substitution(a, b)))); + } else { + return new Result<>(new UnificationActions()); + } } static Result namedNamed(NamedType a, NamedType b) { diff --git a/src/test/java/edu/kit/typicalc/model/parser/LambdaParserTest.java b/src/test/java/edu/kit/typicalc/model/parser/LambdaParserTest.java index 60fe4f7..7a0f433 100644 --- a/src/test/java/edu/kit/typicalc/model/parser/LambdaParserTest.java +++ b/src/test/java/edu/kit/typicalc/model/parser/LambdaParserTest.java @@ -9,6 +9,7 @@ import edu.kit.typicalc.model.term.IntegerTerm; import edu.kit.typicalc.model.term.LambdaTerm; import edu.kit.typicalc.model.term.LetTerm; import edu.kit.typicalc.model.term.VarTerm; +import edu.kit.typicalc.model.parser.Token.TokenType; import edu.kit.typicalc.util.Result; import org.junit.jupiter.api.Test; @@ -85,12 +86,16 @@ class LambdaParserTest { LambdaParser parser = new LambdaParser(""); assertEquals(ParseError.TOO_FEW_TOKENS, parser.parse().unwrapError()); parser = new LambdaParser("x)"); - assertEquals(ParseError.UNEXPECTED_TOKEN, parser.parse().unwrapError()); + ParseError error = parser.parse().unwrapError(); + assertEquals(ParseError.UNEXPECTED_TOKEN, error); + assertEquals(new Token(TokenType.RP, ")", 1), error.getCause()); parser = new LambdaParser("??"); assertEquals(ParseError.UNEXPECTED_CHARACTER, parser.parse().unwrapError()); parser = new LambdaParser("123333333333333"); assertEquals(ParseError.UNEXPECTED_CHARACTER, parser.parse().unwrapError()); parser = new LambdaParser("x 123333333333333"); - assertEquals(ParseError.UNEXPECTED_CHARACTER, parser.parse().unwrapError()); + error = parser.parse().unwrapError(); + assertEquals(ParseError.UNEXPECTED_CHARACTER, error); + assertEquals(new Token(TokenType.NUMBER, "123333333333333", 2), error.getCause()); } } diff --git a/src/test/java/edu/kit/typicalc/model/type/UnificationTest.java b/src/test/java/edu/kit/typicalc/model/type/UnificationTest.java new file mode 100644 index 0000000..f6ff460 --- /dev/null +++ b/src/test/java/edu/kit/typicalc/model/type/UnificationTest.java @@ -0,0 +1,77 @@ +package edu.kit.typicalc.model.type; + +import edu.kit.typicalc.model.Constraint; +import edu.kit.typicalc.model.Substitution; +import edu.kit.typicalc.model.UnificationError; +import org.junit.jupiter.api.Test; + +import java.util.Collection; + +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertTrue; + +class UnificationTest { + @Test + void all() { + TypeVariable a1 = new TypeVariable(TypeVaribaleKind.TREE, 1); + TypeVariable a2 = new TypeVariable(TypeVaribaleKind.TREE, 2); + TypeVariable a3 = new TypeVariable(TypeVaribaleKind.TREE, 3); + FunctionType id = new FunctionType(a1, a1); + FunctionType fun = new FunctionType(a2, a3); + NamedType string = new NamedType("string"); + NamedType object = new NamedType("object"); + + // Function constraints + UnificationError error = id.constrainEqualTo(a1).unwrapError(); + assertEquals(UnificationError.INFINITE_TYPE, error); + + UnificationActions actions = id.constrainEqualTo(a2).unwrap(); + assertEquals(new Substitution(a2, id), actions.getSubstitution().get()); + assertTrue(actions.getConstraints().isEmpty()); + + error = id.constrainEqualTo(string).unwrapError(); + assertEquals(UnificationError.DIFFERENT_TYPES, error); + + actions = id.constrainEqualTo(fun).unwrap(); + assertTrue(actions.getSubstitution().isEmpty()); + Collection constraints = actions.getConstraints(); + assertEquals(2, constraints.size()); + assertTrue(constraints.contains(new Constraint(a1, a2))); + assertTrue(constraints.contains(new Constraint(a1, a3))); + + // Variable constraints + actions = a1.constrainEqualTo(a1).unwrap(); + assertTrue(actions.getConstraints().isEmpty()); + assertTrue(actions.getSubstitution().isEmpty()); + + actions = a1.constrainEqualTo(a2).unwrap(); + assertTrue(actions.getConstraints().isEmpty()); + assertEquals(new Substitution(a1, a2), actions.getSubstitution().get()); + + error = a1.constrainEqualTo(id).unwrapError(); + assertEquals(UnificationError.INFINITE_TYPE, error); + + actions = a2.constrainEqualTo(id).unwrap(); + assertEquals(new Substitution(a2, id), actions.getSubstitution().get()); + assertTrue(actions.getConstraints().isEmpty()); + + actions = a1.constrainEqualTo(string).unwrap(); + assertTrue(actions.getConstraints().isEmpty()); + assertEquals(new Substitution(a1, string), actions.getSubstitution().get()); + + // Named type constraints + actions = string.constrainEqualTo(string).unwrap(); + assertTrue(actions.getConstraints().isEmpty()); + assertTrue(actions.getSubstitution().isEmpty()); + + error = string.constrainEqualTo(object).unwrapError(); + assertEquals(UnificationError.DIFFERENT_TYPES, error); + + error = string.constrainEqualTo(id).unwrapError(); + assertEquals(UnificationError.DIFFERENT_TYPES, error); + + actions = string.constrainEqualTo(a1).unwrap(); + assertTrue(actions.getConstraints().isEmpty()); + assertEquals(new Substitution(a1, string), actions.getSubstitution().get()); + } +}