Unification tests, miscellaneous code style fixes

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);
+    }
 }

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);
+    }
 }

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
 }

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);
                 }
         }

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<ParseError> expect(TokenType type) {
+        Token lastToken = token;
         TokenType current = token.getType();
         Optional<ParseError> error = nextToken();
         if (current != type) {
-            return Optional.of(ParseError.UNEXPECTED_TOKEN.withToken(token));
+            return Optional.of(ParseError.UNEXPECTED_TOKEN.withToken(lastToken));
         }
         return error;
     }

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);
     }
 }

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<TypeVariable> quantifiedVariables;
+    private final Type type;
+    private final List<TypeVariable> 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();
     }
 
     /**

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

@@ -115,7 +115,12 @@ public class TypeVariable extends Type {
      */
     @Override
     public Result<UnificationActions, UnificationError> constrainEqualToVariable(TypeVariable type) {
-        return UnificationUtil.variableVariable(this, type);
+        return UnificationUtil.variableVariable(type, this);
+    }
+
+    @Override
+    public String toString() {
+        return "TypeVariable[" + kind + "_" + index + "]";
     }
 
     @Override

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

@@ -18,8 +18,6 @@ final class UnificationUtil {
 
     }
 
-    // TODO: check for infinite types
-
     static Result<UnificationActions, UnificationError> 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<UnificationActions, UnificationError> 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<UnificationActions, UnificationError> variableVariable(TypeVariable a, TypeVariable 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<UnificationActions, UnificationError> namedNamed(NamedType a, NamedType 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());
     }
 }

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<Constraint> 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());
+    }
+}