diff --git a/src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java b/src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java index 8337057..0dd73bc 100644 --- a/src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java +++ b/src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java @@ -4,6 +4,7 @@ import edu.kit.typicalc.model.type.Type; import edu.kit.typicalc.model.type.TypeVariable; import java.util.ArrayList; +import java.util.Comparator; import java.util.List; /** @@ -28,6 +29,8 @@ public class TypeInferenceResult { protected TypeInferenceResult(List substitutions, TypeVariable typeVar) { MGU = new ArrayList<>(substitutions); findMGU(); + MGU.sort(Comparator.comparingInt((Substitution o) -> + o.getVariable().getIndex()).thenComparing(o -> o.getVariable().getKind())); finalType = findFinalType(typeVar); } diff --git a/src/main/java/edu/kit/typicalc/model/type/FunctionType.java b/src/main/java/edu/kit/typicalc/model/type/FunctionType.java index b905c6c..1d84a00 100644 --- a/src/main/java/edu/kit/typicalc/model/type/FunctionType.java +++ b/src/main/java/edu/kit/typicalc/model/type/FunctionType.java @@ -114,6 +114,11 @@ public class FunctionType extends Type { return parameter; } + @Override + public String toString() { + return "FunctionType[" + parameter + " -> " + output + ']'; + } + @Override public boolean equals(Object o) { if (this == o) { diff --git a/src/main/java/edu/kit/typicalc/model/type/TypeVariableKind.java b/src/main/java/edu/kit/typicalc/model/type/TypeVariableKind.java index f7824cc..53dd92b 100644 --- a/src/main/java/edu/kit/typicalc/model/type/TypeVariableKind.java +++ b/src/main/java/edu/kit/typicalc/model/type/TypeVariableKind.java @@ -5,16 +5,16 @@ package edu.kit.typicalc.model.type; */ public enum TypeVariableKind { - /** - * Used if the type variable was created from user input. - */ - USER_INPUT, - /** * Used if the type variable was generated while building the proof tree. */ TREE, + /** + * Used if the type variable was created from user input. + */ + USER_INPUT, + /** * Used if the type variable was generated for a type assumption of a free variable in the input lambda term. */ diff --git a/src/test/java/edu/kit/typicalc/model/TypeInferenceResultTest.java b/src/test/java/edu/kit/typicalc/model/TypeInferenceResultTest.java index a4cdbfd..df6953c 100644 --- a/src/test/java/edu/kit/typicalc/model/TypeInferenceResultTest.java +++ b/src/test/java/edu/kit/typicalc/model/TypeInferenceResultTest.java @@ -1,4 +1,58 @@ package edu.kit.typicalc.model; +import edu.kit.typicalc.model.type.FunctionType; +import edu.kit.typicalc.model.type.TypeVariable; +import edu.kit.typicalc.model.type.TypeVariableKind; +import org.junit.jupiter.api.Test; + +import java.util.ArrayList; +import java.util.Arrays; +import java.util.List; + +import static org.junit.jupiter.api.Assertions.assertEquals; + class TypeInferenceResultTest { + + private static final TypeVariable A_1 = new TypeVariable(TypeVariableKind.TREE, 1); + private static final TypeVariable A_2 = new TypeVariable(TypeVariableKind.TREE, 2); + private static final TypeVariable A_3 = new TypeVariable(TypeVariableKind.TREE, 3); + private static final TypeVariable A_4 = new TypeVariable(TypeVariableKind.TREE, 4); + private static final TypeVariable A_5 = new TypeVariable(TypeVariableKind.TREE, 5); + private static final TypeVariable A_6 = new TypeVariable(TypeVariableKind.TREE, 6); + private static final TypeVariable A_7 = new TypeVariable(TypeVariableKind.TREE, 7); + + @Test + void getMGU() { + // rectified example from introduction slides + List substitutions = new ArrayList<>(Arrays.asList( + new Substitution(A_7, A_2), + new Substitution(A_4, new FunctionType(A_7, A_5)), + new Substitution(A_6, new FunctionType(A_7, A_5)), + new Substitution(A_3, new FunctionType(A_4, A_5)), + new Substitution(A_1, new FunctionType(A_2, A_3)) + )); + TypeInferenceResult result = new TypeInferenceResult(substitutions, A_1); + + List expectedMGU = new ArrayList<>(Arrays.asList( + new Substitution(A_1, new FunctionType(A_2, new FunctionType(new FunctionType(A_2, A_5), A_5))), + new Substitution(A_3, new FunctionType(new FunctionType(A_2, A_5), A_5)), + new Substitution(A_4, new FunctionType(A_2, A_5)), + new Substitution(A_6, new FunctionType(A_2, A_5)), + new Substitution(A_7, A_2) + )); + + assertEquals(expectedMGU, result.getMGU()); + + // tests if mgu-generation works for substitutions given in reverse order + List substitutions2 = new ArrayList<>(Arrays.asList( + new Substitution(A_1, new FunctionType(A_2, A_3)), + new Substitution(A_3, new FunctionType(A_4, A_5)), + new Substitution(A_6, new FunctionType(A_7, A_5)), + new Substitution(A_4, new FunctionType(A_7, A_5)), + new Substitution(A_7, A_2) + )); + TypeInferenceResult result2 = new TypeInferenceResult(substitutions2, A_1); + + assertEquals(expectedMGU, result2.getMGU()); + } }