Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc

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

@@ -31,8 +31,8 @@ public class TypeInferenceResult {
     protected TypeInferenceResult(List<Substitution> substitutions, TypeVariable typeVar) {
         mgu = new ArrayList<>(substitutions);
         findMGU();
-        mgu.sort(Comparator.comparingInt((Substitution o) ->
-                o.getVariable().getIndex()).thenComparing(o -> o.getVariable().getKind()));
+        mgu.sort(Comparator.comparing((Substitution o) -> o.getVariable().getKind()).
+                thenComparingInt(o -> o.getVariable().getIndex()));
         finalType = findFinalType(typeVar);
     }
 

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

@@ -1,18 +1,27 @@
 package edu.kit.typicalc.model;
 
+import edu.kit.typicalc.model.step.InferenceStep;
 import edu.kit.typicalc.model.term.LambdaTerm;
 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;
 
 /**
  * Instances of this subclass of TypeInferer are used to execute the sub-inference starting in let steps.
  * They provide an extended constructor to make sure this sub-inference is consistent with the „outer“ inference.
  */
-public class TypeInfererLet extends TypeInferer {
+public class TypeInfererLet implements TypeInfererInterface {
+
+    private final Tree tree;
+    private final Unification unification;
+    private final Optional<TypeInferenceResult> typeInfResult;
+
     /**
      * Initializes a new TypeInfererLet for the given type assumptions, lambda term and type variable factory.
      *
@@ -23,8 +32,20 @@ public class TypeInfererLet extends TypeInferer {
      */
     protected TypeInfererLet(LambdaTerm lambdaTerm, Map<VarTerm, TypeAbstraction> typeAssumptions,
                              TypeVariableFactory typeVarFactory) {
-        super(lambdaTerm, typeAssumptions);
-        // TODO
+        tree = new Tree(typeAssumptions, lambdaTerm, typeVarFactory);
+
+        // TODO: Abbrechen bei fehlgeschlagener let-Teilinferenz, evtl. getUnificationSteps() anpassen
+
+        unification = new Unification(new ArrayDeque<>(tree.getConstraints()));
+
+        // cancel algorithm if term can't be typified
+        if (unification.getSubstitutions().isError()) {
+            typeInfResult = Optional.empty();
+            return;
+        }
+
+        List<Substitution> substitutions = unification.getSubstitutions().unwrap();
+        typeInfResult = Optional.of(new TypeInferenceResult(substitutions, tree.getFirstTypeVariable()));
     }
 
     /**
@@ -47,4 +68,23 @@ public class TypeInfererLet extends TypeInferer {
         return letConstraints;
     }
 
-}
+    @Override
+    public InferenceStep getFirstInferenceStep() {
+        return tree.getFirstInferenceStep();
+    }
+
+    @Override
+    public List<UnificationStep> getUnificationSteps() {
+        return unification.getUnificationSteps();
+    }
+
+    @Override
+    public Optional<List<Substitution>> getMGU() {
+        return typeInfResult.map(TypeInferenceResult::getMGU);
+    }
+
+    @Override
+    public Optional<Type> getType() {
+        return typeInfResult.map(TypeInferenceResult::getType);
+    }
+}

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

@@ -72,6 +72,8 @@ public class Unification {
      * Returns as a {@link Result} either the list of substitutions that result from the unification,
      * needed for the subsequent calculation of the most general unifier and final type.
      * Or, in case of a constraint list that can't be unified, a {@link UnificationError}.
+     *
+     * @return a {@link Result} containing either the list of the resulting substitutions or a {@link UnificationError}
      */
     protected Result<List<Substitution>, UnificationError> getSubstitutions() {
         return substitutionsResult;

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

@@ -33,6 +33,8 @@ public class UnificationStep {
      * Returns as a {@link Result} either the list of all substitutions
      * of the unification (in the state resulting from this step).
      * Or, in case of a detected contradiction or infinite type, a {@link UnificationError}.
+     *
+     * @return a {@link Result} containing either the list of all resulting substitutions or a {@link UnificationError}
      */
     public Result<List<Substitution>, UnificationError> getSubstitutions() {
         return substitutions;

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

@@ -1,6 +1,7 @@
 package edu.kit.typicalc.model;
 
 import edu.kit.typicalc.model.type.FunctionType;
+import edu.kit.typicalc.model.type.Type;
 import edu.kit.typicalc.model.type.TypeVariable;
 import edu.kit.typicalc.model.type.TypeVariableKind;
 import org.junit.jupiter.api.Test;
@@ -55,4 +56,19 @@ class TypeInferenceResultTest {
 
         assertEquals(expectedMGU, result2.getMGU());
     }
+
+    @Test
+    void getType() {
+        List<Substitution> 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);
+
+        Type expectedType = new FunctionType(A_2, new FunctionType(new FunctionType(A_2, A_5), A_5));
+        assertEquals(expectedType, result.getType());
+    }
 }

src/test/java/edu/kit/typicalc/model/parser/TypeAssumptionParserTest.java

@@ -1,6 +1,5 @@
 package edu.kit.typicalc.model.parser;
 
-import edu.kit.typicalc.model.term.LambdaTerm;
 import edu.kit.typicalc.model.term.VarTerm;
 import edu.kit.typicalc.model.type.FunctionType;
 import edu.kit.typicalc.model.type.NamedType;
@@ -62,7 +61,8 @@ public class TypeAssumptionParserTest {
     @Test
     void complicatedTypes() {
         TypeAssumptionParser parser = new TypeAssumptionParser();
-        Result<Map<VarTerm, TypeAbstraction>, ParseError> type = parser.parse("id", "(int -> int) -> (boolean -> boolean)");
+        Result<Map<VarTerm, TypeAbstraction>, ParseError> type = parser.parse(
+                "id", "(int -> int) -> (boolean -> boolean)");
         if (type.isError()) {
             System.err.println(type.unwrapError());
             System.err.println(type.unwrapError().getCause());
@@ -79,7 +79,8 @@ public class TypeAssumptionParserTest {
                 ),
                 Collections.emptyList()), assumption.getValue());
         parser = new TypeAssumptionParser();
-        type = parser.parse("id", "((int -> int) -> (boolean -> boolean)) -> ((int2 -> boolean2) -> (boolean2 -> int2))");
+        type = parser.parse(
+                "id", "((int -> int) -> (boolean -> boolean)) -> ((int2 -> boolean2) -> (boolean2 -> int2))");
         if (type.isError()) {
             System.err.println(type.unwrapError());
             System.err.println(type.unwrapError().getCause());