Tree test visit(varTerm), implement TypeAbstraction::instantiate()

src/main/java/edu/kit/typicalc/model/Conclusion.java

@@ -6,6 +6,7 @@ import edu.kit.typicalc.model.type.Type;
 import edu.kit.typicalc.model.type.TypeAbstraction;
 
 import java.util.Map;
+import java.util.Objects;
 
 /**
  * Models the conclusion of an inference rule and consists of a list of type assumptions, a lambda term and a type.
@@ -50,4 +51,22 @@ public class Conclusion {
     public Type getType() {
         return type;
     }
+
+    @Override
+    public boolean equals(Object o) {
+        if (this == o) {
+            return true;
+        }
+        if (o == null || getClass() != o.getClass()) {
+            return false;
+        }
+        Conclusion that = (Conclusion) o;
+        return typeAssumptions.equals(that.typeAssumptions)
+                && lambdaTerm.equals(that.lambdaTerm) && type.equals(that.type);
+    }
+
+    @Override
+    public int hashCode() {
+        return Objects.hash(typeAssumptions, lambdaTerm, type);
+    }
 }

src/main/java/edu/kit/typicalc/model/Tree.java

@@ -146,8 +146,7 @@ public class Tree implements TermVisitorTree {
     }
 
     @Override
-    public InferenceStep visit(VarTerm varTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType)
-            throws IllegalStateException {
+    public InferenceStep visit(VarTerm varTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType) {
         TypeAbstraction premiseAbs = typeAssumptions.get(varTerm);
         if (premiseAbs == null) {
             throw new IllegalStateException("Cannot create VarStep for VarTerm '"

src/main/java/edu/kit/typicalc/model/step/InferenceStep.java

@@ -3,6 +3,8 @@ package edu.kit.typicalc.model.step;
 import edu.kit.typicalc.model.Conclusion;
 import edu.kit.typicalc.model.Constraint;
 
+import java.util.Objects;
+
 /**
  * Models one step of the inference tree.
  * Depending on the inference rule that is applied in a step,
@@ -51,4 +53,21 @@ public abstract class InferenceStep {
      * @param stepVisitor the visitor that wants to visit this object
      */
     public abstract void accept(StepVisitor stepVisitor);
+
+    @Override
+    public boolean equals(Object o) {
+        if (this == o) {
+            return true;
+        }
+        if (o == null || getClass() != o.getClass()) {
+            return false;
+        }
+        InferenceStep that = (InferenceStep) o;
+        return conclusion.equals(that.conclusion) && constraint.equals(that.constraint);
+    }
+
+    @Override
+    public int hashCode() {
+        return Objects.hash(conclusion, constraint);
+    }
 }

src/main/java/edu/kit/typicalc/model/step/VarStep.java

@@ -5,6 +5,8 @@ import edu.kit.typicalc.model.Constraint;
 import edu.kit.typicalc.model.type.Type;
 import edu.kit.typicalc.model.type.TypeAbstraction;
 
+import java.util.Objects;
+
 /**
  * Models one step of the inference tree where the variable rule is applied. It contains a type
  * abstraction that is identified as the type of the variable in the premise of the step.
@@ -46,4 +48,25 @@ public abstract class VarStep extends InferenceStep {
     public Type getInstantiatedTypeAbs() {
         return instantiatedTypeAbs;
     }
+
+    @Override
+    public boolean equals(Object o) {
+        if (this == o) {
+            return true;
+        }
+        if (o == null || getClass() != o.getClass()) {
+            return false;
+        }
+        if (!super.equals(o)) {
+            return false;
+        }
+        VarStep varStep = (VarStep) o;
+        return typeAbstractionInPremise.equals(varStep.typeAbstractionInPremise)
+                && instantiatedTypeAbs.equals(varStep.instantiatedTypeAbs);
+    }
+
+    @Override
+    public int hashCode() {
+        return Objects.hash(super.hashCode(), typeAbstractionInPremise, instantiatedTypeAbs);
+    }
 }

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

@@ -38,13 +38,17 @@ public class TypeAbstraction {
     /**
      * Instantiates the type abstraction with a new type and returns it. The new type
      * contains new type variables generated by the given type variable factory.
-     * @param typeVarFactory  the type variable factory used to generate the new type
-     * variables
+     *
+     * @param typeVarFactory  the type variable factory used to generate the new type variables
      * @return the new type resulting from the instantiation of the type abstraction
      */
     public Type instantiate(TypeVariableFactory typeVarFactory) {
-        //TODO
-        return null;
+        Type instantiatedType = this.type;
+        for (TypeVariable var : this.quantifiedVariables) {
+            TypeVariable newVariable = typeVarFactory.nextTypeVariable();
+            instantiatedType = instantiatedType.substitute(var, newVariable);
+        }
+        return instantiatedType;
     }
 
     /**

src/test/java/edu/kit/typicalc/model/ConclusionTest.java

@@ -5,6 +5,7 @@ import edu.kit.typicalc.model.term.VarTerm;
 import edu.kit.typicalc.model.type.NamedType;
 import edu.kit.typicalc.model.type.Type;
 import edu.kit.typicalc.model.type.TypeAbstraction;
+import nl.jqno.equalsverifier.EqualsVerifier;
 import org.junit.jupiter.api.BeforeAll;
 import org.junit.jupiter.api.Test;
 
@@ -25,6 +26,12 @@ class ConclusionTest {
         typeAssumptions.put(new VarTerm("var2"), new TypeAbstraction(new NamedType("type2"), new ArrayList<>()));
     }
 
+    @Test
+    void equalsTest() {
+        EqualsVerifier.forClass(Conclusion.class).usingGetClass().verify();
+    }
+
+
     @Test
     void getTypeAssumptionsTest() {
         Conclusion conclusion = new Conclusion(typeAssumptions, lambdaTerm, type);

src/test/java/edu/kit/typicalc/model/TreeTest.java

@@ -1,5 +1,7 @@
 package edu.kit.typicalc.model;
 
+import edu.kit.typicalc.model.step.InferenceStep;
+import edu.kit.typicalc.model.step.VarStepDefault;
 import edu.kit.typicalc.model.term.VarTerm;
 import edu.kit.typicalc.model.type.NamedType;
 import edu.kit.typicalc.model.type.TypeAbstraction;
@@ -12,19 +14,23 @@ import java.util.HashMap;
 import java.util.Map;
 
 import static org.junit.jupiter.api.Assertions.assertEquals;
+import static org.junit.jupiter.api.Assertions.assertThrows;
 
 class TreeTest {
 
-    private static final Map<VarTerm, TypeAbstraction> typeAssumptions = new HashMap<>();
+    private static final Map<VarTerm, TypeAbstraction> TYPE_ASSUMPTIONS = new HashMap<>();
+    private static final VarTerm VAR = new VarTerm("var");
+    private static final NamedType TYPE = new NamedType("type");
+    private static final TypeAbstraction TYPE_ABS = new TypeAbstraction(TYPE, new ArrayList<>());
 
     @BeforeAll
     static void setUp() {
-        typeAssumptions.put(new VarTerm("var"), new TypeAbstraction(new NamedType("type"), new ArrayList<>()));
+        TYPE_ASSUMPTIONS.put(VAR, TYPE_ABS);
     }
 
     @Test
     void firstTypeVariableNewFactory() {
-        Tree tree = new Tree(typeAssumptions, new VarTerm("var"));
+        Tree tree = new Tree(TYPE_ASSUMPTIONS, VAR);
         assertEquals(tree.getFirstTypeVariable(), new TypeVariableFactory(TypeVariableKind.TREE).nextTypeVariable());
     }
 
@@ -36,7 +42,24 @@ class TreeTest {
             factory.nextTypeVariable();
             factoryRef.nextTypeVariable();
         }
-        Tree tree = new Tree(typeAssumptions, new VarTerm("var"), factory);
+        Tree tree = new Tree(TYPE_ASSUMPTIONS, VAR, factory);
         assertEquals(tree.getFirstTypeVariable(), factoryRef.nextTypeVariable());
     }
+
+    @Test
+    void missingTypeAssumptionForVar() {
+        Map<VarTerm, TypeAbstraction> ass = new HashMap<>();
+        assertThrows(IllegalStateException.class, () -> {
+                new Tree(ass, VAR);
+        });
+    }
+
+    @Test
+    void visitVar() {
+        Tree tree = new Tree(TYPE_ASSUMPTIONS, VAR);
+        Conclusion conclusion = new Conclusion(TYPE_ASSUMPTIONS, VAR, tree.getFirstTypeVariable());
+        InferenceStep expectedStep = new VarStepDefault(TYPE_ABS, TYPE, conclusion,
+                new Constraint(TYPE, tree.getFirstTypeVariable()));
+        assertEquals(expectedStep, tree.getFirstInferenceStep());
+    }
 }