diff --git a/src/main/java/edu/kit/typicalc/model/Substitution.java b/src/main/java/edu/kit/typicalc/model/Substitution.java index 0063819..7865612 100644 --- a/src/main/java/edu/kit/typicalc/model/Substitution.java +++ b/src/main/java/edu/kit/typicalc/model/Substitution.java @@ -35,7 +35,7 @@ public class Substitution { /** * @return the replacement type */ - Type getType() { + public Type getType() { return b; } diff --git a/src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java b/src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java index 3f06f59..8337057 100644 --- a/src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java +++ b/src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java @@ -3,7 +3,7 @@ package edu.kit.typicalc.model; import edu.kit.typicalc.model.type.Type; import edu.kit.typicalc.model.type.TypeVariable; -import java.util.Collections; +import java.util.ArrayList; import java.util.List; /** @@ -12,6 +12,10 @@ import java.util.List; * accessed right after instantiation (no additional initialization is required). */ public class TypeInferenceResult { + + private final List MGU; + private final Type finalType; + /** * Initializes a new TypeInferenceResult for the given substitutions (resulting from * the unification) and the given type variable belonging to the original lambda term @@ -22,7 +26,39 @@ public class TypeInferenceResult { * @param typeVar the type variable belonging to the original lambda term */ protected TypeInferenceResult(List substitutions, TypeVariable typeVar) { - // TODO + MGU = new ArrayList<>(substitutions); + findMGU(); + finalType = findFinalType(typeVar); + } + + private void findMGU() { + for (int i = 0; i < MGU.size(); i++) { + Substitution applySub = MGU.get(i); + for (int j = 0; j < MGU.size(); j++) { + Substitution toSub = MGU.get(j); + if (i == j) { + continue; + } else if (applySub.getVariable().equals(toSub.getVariable())) { + throw new IllegalStateException( + "MGU cannot be calculated for two substitutions with same Variable:\n" + + applySub.toString() + "\n" + + toSub.toString()); + } + + Substitution resultSub = new Substitution(toSub.getVariable(), toSub.getType().substitute(applySub)); + MGU.set(j, resultSub); + } + } + } + + private Type findFinalType(TypeVariable typeVar) { + for (Substitution substitution : MGU) { + if (substitution.getVariable().equals(typeVar)) { + return substitution.getType(); + } + } + throw new IllegalStateException("MGU has to contain substitution for original type variable: " + + typeVar.toString()); } /** @@ -32,8 +68,7 @@ public class TypeInferenceResult { * @return the most general unifier, null if there is no valid mgu */ protected List getMGU() { - return Collections.emptyList(); - // TODO + return MGU; } /** @@ -44,7 +79,6 @@ public class TypeInferenceResult { * @return the final type of the lambda term, null if there is no valid type */ protected Type getType() { - return null; - // TODO + return finalType; } } diff --git a/src/main/java/edu/kit/typicalc/model/type/Type.java b/src/main/java/edu/kit/typicalc/model/type/Type.java index 63c3199..9139c0c 100644 --- a/src/main/java/edu/kit/typicalc/model/type/Type.java +++ b/src/main/java/edu/kit/typicalc/model/type/Type.java @@ -1,5 +1,6 @@ package edu.kit.typicalc.model.type; +import edu.kit.typicalc.model.Substitution; import edu.kit.typicalc.model.UnificationError; import edu.kit.typicalc.util.Result; @@ -15,13 +16,22 @@ public abstract class Type { public abstract boolean contains(Type x); /** - * Substitutes a type Variable for a different type + * Substitutes a type Variable for a different type. * @param a the type to replace * @param b the type to insert * @return a Type that is created by replacing a with b */ public abstract Type substitute(TypeVariable a, Type b); + /** + * Applies the given substitution to the type. + * @param substitution the substitution to apply to the type + * @return the substituted type + */ + public Type substitute(Substitution substitution) { + return substitute(substitution.getVariable(), substitution.getType()); + } + /** * Accepts a visitor * @param typeVisitor the visitor that wants to visit this diff --git a/src/test/java/edu/kit/typicalc/model/TypeInferenceResultTest.java b/src/test/java/edu/kit/typicalc/model/TypeInferenceResultTest.java new file mode 100644 index 0000000..a4cdbfd --- /dev/null +++ b/src/test/java/edu/kit/typicalc/model/TypeInferenceResultTest.java @@ -0,0 +1,4 @@ +package edu.kit.typicalc.model; + +class TypeInferenceResultTest { +}