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

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

@@ -11,6 +11,7 @@ import edu.kit.typicalc.model.term.VarTerm;
 import edu.kit.typicalc.model.type.Type;
 import edu.kit.typicalc.model.type.TypeAbstraction;
 import edu.kit.typicalc.model.type.TypeAssumption;
+import edu.kit.typicalc.model.type.TypeVariable;
 
 import java.util.List;
 import java.util.Map;
@@ -63,6 +64,16 @@ public class Tree implements TermVisitorTree {
         // TODO;
     }
 
+    /**
+     * Returns the first type variable the original lambda term was assigned in the first inference step.
+     *
+     * @return the first type variable
+     */
+    protected TypeVariable getFirstTypeVariable() {
+        return null;
+        // TODO;
+    }
+
     /**
      * Returns the list of constraints that formed while generating the inference step tree
      * structure, needed for the subsequent unification.

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

@@ -19,6 +19,10 @@ import java.util.Map;
  */
 public class TypeInferer implements TypeInfererInterface {
 
+    private final Tree tree;
+    private final Unification unification;
+    private final TypeInferenceResult typeInfResult;
+
     /**
      * Initializes a new TypeInferer for the given type assumptions and lambda term.
      * The inference step structure, unification steps, the most general unifier and the
@@ -28,31 +32,41 @@ public class TypeInferer implements TypeInfererInterface {
      * @param typeAssumptions the type assumptions to consider when generating the tree
      */
     protected TypeInferer(LambdaTerm lambdaTerm, Map<VarTerm, TypeAbstraction> typeAssumptions) {
-        // TODO
+        tree = new Tree(typeAssumptions, lambdaTerm);
+        // TODO: Abbrechen bei fehlgeschlagener let-Teilinferenz, evtl. getUnificationSteps() anpassen
+
+        unification = new Unification(tree.getConstraints());
+
+        // cancel algorithm if term can't be typified
+        if (!unification.getSubstitutions().isOk()) {
+            typeInfResult = null;
+            // TODO: schönere Methode, mit nicht typisierbar umzugehen?
+            //  getter unten anpassen!
+            return;
+        }
+
+        List<Substitution> substitutions = unification.getSubstitutions().getValue();
+        typeInfResult = new TypeInferenceResult(substitutions, tree.getFirstTypeVariable());
     }
 
 
     @Override
     public InferenceStep getFirstInferenceStep() {
-        return null;
-        // TODO
+        return tree.getFirstInferenceStep();
     }
 
     @Override
     public List<UnificationStep> getUnificationSteps() {
-        return null;
-        // TODO
+        return unification.getUnificationSteps();
     }
 
     @Override
     public List<Substitution> getMGU() {
-        return null;
-        // TODO
+        return typeInfResult.getMGU();
     }
 
     @Override
     public Type getType() {
-        return null;
-        // TODO
+        return typeInfResult.getType();
     }
 }

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

@@ -0,0 +1,20 @@
+package edu.kit.typicalc.model;
+
+import edu.kit.typicalc.util.Result;
+
+import java.util.List;
+
+public class Unification {
+    protected Unification(List<Constraint> constraints) {
+
+    }
+
+    protected List<UnificationStep> getUnificationSteps() {
+        return null;
+    }
+
+    protected Result<List<Substitution>, UnificationError> getSubstitutions() {
+        return null;
+    }
+
+}

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

@@ -0,0 +1,4 @@
+package edu.kit.typicalc.model;
+
+public enum UnificationError {
+}