diff --git a/src/main/java/edu/kit/typicalc/model/Tree.java b/src/main/java/edu/kit/typicalc/model/Tree.java index 76cbd4b..e2ae0ac 100644 --- a/src/main/java/edu/kit/typicalc/model/Tree.java +++ b/src/main/java/edu/kit/typicalc/model/Tree.java @@ -103,14 +103,14 @@ public class Tree implements TermVisitorTree { public InferenceStep visit(AppTerm appTerm, Map typeAssumptions, Type conclusionType) { Type leftType = typeVarFactory.nextTypeVariable(); Type rightType = typeVarFactory.nextTypeVariable(); - InferenceStep leftPremise = appTerm.getFunction().accept(this, typeAssumptions, leftType); - - InferenceStep rightPremise = appTerm.getParameter().accept(this, typeAssumptions, rightType); Type function = new FunctionType(rightType, conclusionType); Constraint newConstraint = new Constraint(leftType, function); constraints.add(newConstraint); + InferenceStep leftPremise = appTerm.getFunction().accept(this, typeAssumptions, leftType); + InferenceStep rightPremise = appTerm.getParameter().accept(this, typeAssumptions, rightType); + Conclusion conclusion = new Conclusion(typeAssumptions, appTerm, conclusionType); return stepFactory.createAppStep(leftPremise, rightPremise, conclusion, newConstraint); } @@ -123,12 +123,13 @@ public class Tree implements TermVisitorTree { extendedTypeAssumptions.put(absTerm.getVariable(), assAbs); Type premiseType = typeVarFactory.nextTypeVariable(); - InferenceStep premise = absTerm.getInner().accept(this, extendedTypeAssumptions, premiseType); Type function = new FunctionType(assType, premiseType); Constraint newConstraint = new Constraint(conclusionType, function); constraints.add(newConstraint); + InferenceStep premise = absTerm.getInner().accept(this, extendedTypeAssumptions, premiseType); + Conclusion conclusion = new Conclusion(typeAssumptions, absTerm, conclusionType); return stepFactory.createAbsStep(premise, conclusion, newConstraint); } @@ -159,10 +160,10 @@ public class Tree implements TermVisitorTree { typeInfererLet.getType().orElseThrow(IllegalStateException::new), extendedTypeAssumptions); extendedTypeAssumptions.put(letTerm.getVariable(), newTypeAbstraction); - premise = letTerm.getInner().accept(this, extendedTypeAssumptions, premiseType); - constraints.add(newConstraint); constraints.addAll(typeInfererLet.getLetConstraints()); + + premise = letTerm.getInner().accept(this, extendedTypeAssumptions, premiseType); } else { premise = new EmptyStep(); failedSubInference = true; @@ -196,4 +197,22 @@ public class Tree implements TermVisitorTree { Conclusion conclusion = new Conclusion(typeAssumptions, varTerm, conclusionType); return stepFactory.createVarStep(premiseAbs, instantiation, conclusion, newConstraint); } + + @Override + public boolean equals(Object o) { + if (this == o) { + return true; + } + if (o == null || getClass() != o.getClass()) { + return false; + } + Tree tree = (Tree) o; + return failedSubInference == tree.failedSubInference && firstTypeVariable.equals(tree.firstTypeVariable) + && firstInferenceStep.equals(tree.firstInferenceStep) && constraints.equals(tree.constraints); + } + + @Override + public int hashCode() { + return Objects.hash(firstTypeVariable, firstInferenceStep, constraints, failedSubInference); + } } diff --git a/src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java b/src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java index d565f40..cdaecac 100644 --- a/src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java +++ b/src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java @@ -6,6 +6,7 @@ import edu.kit.typicalc.model.type.TypeVariable; import java.util.ArrayList; import java.util.Comparator; import java.util.List; +import java.util.Objects; /** * Models the final result of the type inference with the most general unifier (mgu) and @@ -85,4 +86,21 @@ public class TypeInferenceResult { protected Type getType() { return finalType; } + + @Override + public boolean equals(Object o) { + if (this == o) { + return true; + } + if (o == null || getClass() != o.getClass()) { + return false; + } + TypeInferenceResult that = (TypeInferenceResult) o; + return mgu.equals(that.mgu) && finalType.equals(that.finalType); + } + + @Override + public int hashCode() { + return Objects.hash(mgu, finalType); + } } diff --git a/src/main/java/edu/kit/typicalc/model/TypeInferer.java b/src/main/java/edu/kit/typicalc/model/TypeInferer.java index 696f07f..b144cf8 100644 --- a/src/main/java/edu/kit/typicalc/model/TypeInferer.java +++ b/src/main/java/edu/kit/typicalc/model/TypeInferer.java @@ -87,4 +87,21 @@ public class TypeInferer implements TypeInfererInterface { public Optional getType() { return typeInfResult.map(TypeInferenceResult::getType); } + + @Override + public boolean equals(Object o) { + if (this == o) { + return true; + } + if (o == null || getClass() != o.getClass()) { + return false; + } + TypeInferer that = (TypeInferer) o; + return tree.equals(that.tree) && unification.equals(that.unification) && typeInfResult.equals(that.typeInfResult); + } + + @Override + public int hashCode() { + return Objects.hash(tree, unification, typeInfResult); + } } diff --git a/src/main/java/edu/kit/typicalc/model/TypeInfererLet.java b/src/main/java/edu/kit/typicalc/model/TypeInfererLet.java index 8bec539..6e910ac 100644 --- a/src/main/java/edu/kit/typicalc/model/TypeInfererLet.java +++ b/src/main/java/edu/kit/typicalc/model/TypeInfererLet.java @@ -6,11 +6,7 @@ import edu.kit.typicalc.model.term.VarTerm; import edu.kit.typicalc.model.type.Type; import edu.kit.typicalc.model.type.TypeAbstraction; -import java.util.ArrayDeque; -import java.util.ArrayList; -import java.util.List; -import java.util.Map; -import java.util.Optional; +import java.util.*; /** * Instances of this implementation of TypeInfererInterface are used to execute the sub-inference starting in let steps. @@ -92,4 +88,21 @@ public class TypeInfererLet implements TypeInfererInterface { public Optional getType() { return typeInfResult.map(TypeInferenceResult::getType); } + + @Override + public boolean equals(Object o) { + if (this == o) { + return true; + } + if (o == null || getClass() != o.getClass()) { + return false; + } + TypeInfererLet that = (TypeInfererLet) o; + return tree.equals(that.tree) && unification.equals(that.unification) && typeInfResult.equals(that.typeInfResult); + } + + @Override + public int hashCode() { + return Objects.hash(tree, unification, typeInfResult); + } } \ No newline at end of file diff --git a/src/main/java/edu/kit/typicalc/model/Unification.java b/src/main/java/edu/kit/typicalc/model/Unification.java index 0ec9fe8..09685a7 100644 --- a/src/main/java/edu/kit/typicalc/model/Unification.java +++ b/src/main/java/edu/kit/typicalc/model/Unification.java @@ -4,12 +4,7 @@ import edu.kit.typicalc.model.type.Type; import edu.kit.typicalc.model.type.UnificationActions; import edu.kit.typicalc.util.Result; -import java.util.ArrayDeque; -import java.util.ArrayList; -import java.util.Collections; -import java.util.Deque; -import java.util.List; -import java.util.Optional; +import java.util.*; /** * Models the unification of a type inference with its individual steps. @@ -82,4 +77,20 @@ public class Unification { return substitutionsResult; } + @Override + public boolean equals(Object o) { + if (this == o) { + return true; + } + if (o == null || getClass() != o.getClass()) { + return false; + } + Unification that = (Unification) o; + return steps.equals(that.steps) && substitutionsResult.equals(that.substitutionsResult); + } + + @Override + public int hashCode() { + return Objects.hash(steps, substitutionsResult); + } } diff --git a/src/main/java/edu/kit/typicalc/model/step/LetStep.java b/src/main/java/edu/kit/typicalc/model/step/LetStep.java index db0dbd9..45236de 100644 --- a/src/main/java/edu/kit/typicalc/model/step/LetStep.java +++ b/src/main/java/edu/kit/typicalc/model/step/LetStep.java @@ -41,7 +41,7 @@ public abstract class LetStep extends InferenceStep { return premise; } - /** + /**typeInferer.equals(letStep.typeInferer) * Returns the TypeInferer for the premise which needs its own type Inference. * @return typeInferer the type inferer of the sub-inference */ diff --git a/src/test/java/edu/kit/typicalc/model/TreeTest.java b/src/test/java/edu/kit/typicalc/model/TreeTest.java index 27106fc..2ff3687 100644 --- a/src/test/java/edu/kit/typicalc/model/TreeTest.java +++ b/src/test/java/edu/kit/typicalc/model/TreeTest.java @@ -8,8 +8,7 @@ import org.junit.jupiter.api.Test; import java.util.*; -import static org.junit.jupiter.api.Assertions.assertEquals; -import static org.junit.jupiter.api.Assertions.assertThrows; +import static org.junit.jupiter.api.Assertions.*; class TreeTest { @@ -74,9 +73,9 @@ class TreeTest { assertEquals(expectedStep, tree.getFirstInferenceStep()); List constraints = new ArrayList<>(); + constraints.add(appConstraint); constraints.add(varLeftConstraint); constraints.add(varRightConstraint); - constraints.add(appConstraint); assertEquals(constraints, tree.getConstraints()); } @@ -101,8 +100,8 @@ class TreeTest { assertEquals(expectedStep, tree.getFirstInferenceStep()); List constraints = new ArrayList<>(); - constraints.add(varConstraint); constraints.add(absConstraint); + constraints.add(varConstraint); assertEquals(constraints, tree.getConstraints()); } @@ -125,4 +124,44 @@ class TreeTest { assertEquals(expectedStep, tree.getFirstInferenceStep()); assertEquals(Collections.singletonList(constraint), tree.getConstraints()); } + + @Test + void visitLet() { + VarTerm x = new VarTerm("x"); + VarTerm f = new VarTerm("f"); + TypeVariable generated1 = new TypeVariable(TypeVariableKind.GENERATED_TYPE_ASSUMPTION, 1); + TypeVariable variable2 = new TypeVariable(TypeVariableKind.TREE, 2); + TypeVariable variable3 = new TypeVariable(TypeVariableKind.TREE, 3); + TypeAbstraction generated1Abs = new TypeAbstraction(generated1); + + Map typeAssumptions = new LinkedHashMap<>(); + typeAssumptions.put(x, generated1Abs); + + LetTerm letTerm = new LetTerm(f, x, f); + Tree tree = new Tree(typeAssumptions, letTerm); + + TypeVariableFactory refFac = new TypeVariableFactory(TypeVariableKind.TREE); + refFac.nextTypeVariable(); + TypeInfererLet typeInfererLet = new TypeInfererLet(x, typeAssumptions, refFac); + + + Map varRightTypeAss = new LinkedHashMap<>(typeAssumptions); + varRightTypeAss.put(f, generated1Abs); + Conclusion varRightConclusion = new Conclusion(varRightTypeAss, f, variable3); + Constraint varRightConstraint = new Constraint(variable3, generated1); + InferenceStep varRightStep = new VarStepWithLet(generated1Abs, generated1, + varRightConclusion, varRightConstraint); + + Conclusion conclusion = new Conclusion(typeAssumptions, letTerm, tree.getFirstTypeVariable()); + Constraint letConstraint = new Constraint(tree.getFirstTypeVariable(), variable3); + InferenceStep expectedStep = new LetStepDefault(conclusion, letConstraint, varRightStep, typeInfererLet); + + assertEquals(expectedStep, tree.getFirstInferenceStep()); + + List constraints = new ArrayList<>(); + constraints.add(letConstraint); + constraints.add(new Constraint(variable2, generated1)); + constraints.add(varRightConstraint); + assertEquals(constraints, tree.getConstraints()); + } } diff --git a/src/test/java/edu/kit/typicalc/model/TypeInfererLetTest.java b/src/test/java/edu/kit/typicalc/model/TypeInfererLetTest.java new file mode 100644 index 0000000..7b1c3c2 --- /dev/null +++ b/src/test/java/edu/kit/typicalc/model/TypeInfererLetTest.java @@ -0,0 +1,48 @@ +package edu.kit.typicalc.model; + +import edu.kit.typicalc.model.step.InferenceStep; +import edu.kit.typicalc.model.step.VarStepWithLet; +import edu.kit.typicalc.model.term.VarTerm; +import edu.kit.typicalc.model.type.TypeAbstraction; +import edu.kit.typicalc.model.type.TypeVariable; +import edu.kit.typicalc.model.type.TypeVariableKind; +import org.junit.jupiter.api.Test; + +import java.util.*; + +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertTrue; + +class TypeInfererLetTest { + + @Test + void createTypeInfererLet() { + VarTerm x = new VarTerm("x"); + TypeVariable generated1 = new TypeVariable(TypeVariableKind.GENERATED_TYPE_ASSUMPTION, 1); + TypeVariable variable2 = new TypeVariable(TypeVariableKind.TREE, 2); + TypeAbstraction generated1Abs = new TypeAbstraction(generated1); + + Map typeAssumptions = new LinkedHashMap<>(); + typeAssumptions.put(x, generated1Abs); + + TypeVariableFactory refFac = new TypeVariableFactory(TypeVariableKind.TREE); + refFac.nextTypeVariable(); + TypeInfererLet typeInfererLet = new TypeInfererLet(x, typeAssumptions, refFac); + + Conclusion varLeftConclusion = new Conclusion(typeAssumptions, x, variable2); + Constraint varLeftConstraint = new Constraint(variable2, generated1); + InferenceStep varLeftStep = new VarStepWithLet(generated1Abs, generated1, + varLeftConclusion, varLeftConstraint); + + assertEquals(varLeftStep, typeInfererLet.getFirstInferenceStep()); + assertTrue(typeInfererLet.getType().isPresent()); + assertEquals(generated1, typeInfererLet.getType().get()); + List expectedMGU + = new ArrayList<>(Collections.singletonList(new Substitution(variable2, generated1))); + assertTrue(typeInfererLet.getMGU().isPresent()); + assertEquals(expectedMGU, typeInfererLet.getMGU().get()); + List expectedLetConstraints + = new ArrayList<>(Collections.singletonList(new Constraint(variable2, generated1))); + assertEquals(expectedLetConstraints, typeInfererLet.getLetConstraints()); + } +}