diff --git a/src/main/java/edu/kit/typicalc/model/TypeInferer.java b/src/main/java/edu/kit/typicalc/model/TypeInferer.java index 3028cbb..bc5571d 100644 --- a/src/main/java/edu/kit/typicalc/model/TypeInferer.java +++ b/src/main/java/edu/kit/typicalc/model/TypeInferer.java @@ -7,6 +7,7 @@ import edu.kit.typicalc.model.type.Type; import edu.kit.typicalc.model.type.TypeAbstraction; import edu.kit.typicalc.model.type.TypeVariableKind; +import java.util.ArrayDeque; import java.util.HashMap; import java.util.List; import java.util.Map; @@ -42,7 +43,7 @@ public class TypeInferer implements TypeInfererInterface { // TODO: Abbrechen bei fehlgeschlagener let-Teilinferenz, evtl. getUnificationSteps() anpassen - unification = new Unification(tree.getConstraints()); + unification = new Unification(new ArrayDeque<>(tree.getConstraints())); // cancel algorithm if term can't be typified if (unification.getSubstitutions().isError()) { diff --git a/src/main/java/edu/kit/typicalc/model/Unification.java b/src/main/java/edu/kit/typicalc/model/Unification.java index e4c2c63..3520f9c 100644 --- a/src/main/java/edu/kit/typicalc/model/Unification.java +++ b/src/main/java/edu/kit/typicalc/model/Unification.java @@ -1,21 +1,80 @@ package edu.kit.typicalc.model; +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; +/** + * Models the unification of a type inference with its individual steps. + * It grants access to the list of unification steps and a list of the substitutions that result from the unification. + */ public class Unification { - protected Unification(List constraints) { + private final List steps; + private final Result, UnificationError> substitutionsResult; + /** + * Initializes a new {@link Unification} for the given constraints. + * The list of unification steps and the resulting substitutions are generated here. + * @param constraints constraints to execute the unification for + */ + protected Unification(Deque constraints) { // TODO: document List->Deque + steps = new ArrayList<>(); + List substitutions = new ArrayList<>(); + + steps.add(new UnificationStep(new Result<>(Collections.emptyList()), new ArrayList<>(constraints))); + while (!constraints.isEmpty()) { + Constraint c = constraints.removeFirst(); + Type a = c.getFirstType(); + Type b = c.getSecondType(); + Result actions = a.constrainEqualTo(b); + if (actions.isError()) { + steps.add(new UnificationStep(new Result<>(actions), new ArrayList<>(constraints))); + substitutionsResult = new Result<>(actions); + return; + } + UnificationActions thisStep = actions.unwrap(); + Optional substitution = thisStep.getSubstitution(); + if (substitution.isPresent()) { + Deque updateConstraints = new ArrayDeque<>(); + for (Constraint constraint : constraints) { + Type first = constraint.getFirstType(); + Type second = constraint.getSecondType(); + updateConstraints.add(new Constraint( + first.substitute(substitution.get()), + second.substitute(substitution.get()) + )); + } + constraints = updateConstraints; + substitutions.add(substitution.get()); + } + constraints.addAll(thisStep.getConstraints()); + steps.add(new UnificationStep(new Result<>(new ArrayList<>(substitutions)), new ArrayList<>(constraints))); + } + + substitutionsResult = new Result<>(substitutions); } + /** + * @return list of the unification steps the unification performs. + */ protected List getUnificationSteps() { - return new ArrayList<>(); // TODO + return Collections.unmodifiableList(steps); } + /** + * 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}. + */ protected Result, UnificationError> getSubstitutions() { - return new Result<>(null, UnificationError.INFINITE_TYPE); // TODO + return substitutionsResult; } } diff --git a/src/main/java/edu/kit/typicalc/model/UnificationStep.java b/src/main/java/edu/kit/typicalc/model/UnificationStep.java index ee9bbff..01230ea 100644 --- a/src/main/java/edu/kit/typicalc/model/UnificationStep.java +++ b/src/main/java/edu/kit/typicalc/model/UnificationStep.java @@ -2,7 +2,9 @@ package edu.kit.typicalc.model; import edu.kit.typicalc.util.Result; +import java.util.Arrays; import java.util.List; +import java.util.Objects; /** * Models one step of the unification algorithm with a list of constraints and a list of substitutions. @@ -42,4 +44,29 @@ public class UnificationStep { public List getConstraints() { return constraints; } + + @Override + public String toString() { + return "UnificationStep{" + + "substitutions=" + substitutions + + ", constraints=" + Arrays.toString(constraints.toArray()) + + '}'; + } + + @Override + public boolean equals(Object o) { + if (this == o) { + return true; + } + if (o == null || getClass() != o.getClass()) { + return false; + } + UnificationStep that = (UnificationStep) o; + return substitutions.equals(that.substitutions) && constraints.equals(that.constraints); + } + + @Override + public int hashCode() { + return Objects.hash(substitutions, constraints); + } } diff --git a/src/main/java/edu/kit/typicalc/util/Result.java b/src/main/java/edu/kit/typicalc/util/Result.java index 2de26dc..639eff9 100644 --- a/src/main/java/edu/kit/typicalc/util/Result.java +++ b/src/main/java/edu/kit/typicalc/util/Result.java @@ -1,5 +1,7 @@ package edu.kit.typicalc.util; +import java.util.Objects; + /** * Can be a value of type T or an error of type E (if the computation failed). * @@ -25,7 +27,7 @@ public class Result { * * @param other the result */ - public Result(Result other) { + public Result(Result other) { this.value = (T) other.value; this.error = (E) other.error; } @@ -87,4 +89,30 @@ public class Result { } return error; } + + @Override + public String toString() { + if (isOk()) { + return "Ok(" + value + ")"; + } else { + return "Error(" + error + ")"; + } + } + + @Override + public boolean equals(Object o) { + if (this == o) { + return true; + } + if (o == null || getClass() != o.getClass()) { + return false; + } + Result result = (Result) o; + return Objects.equals(value, result.value) && Objects.equals(error, result.error); + } + + @Override + public int hashCode() { + return Objects.hash(value, error); + } } diff --git a/src/test/java/edu/kit/typicalc/model/UnificationTest.java b/src/test/java/edu/kit/typicalc/model/UnificationTest.java new file mode 100644 index 0000000..3ee1b54 --- /dev/null +++ b/src/test/java/edu/kit/typicalc/model/UnificationTest.java @@ -0,0 +1,104 @@ +package edu.kit.typicalc.model; + +import edu.kit.typicalc.model.type.FunctionType; +import edu.kit.typicalc.model.type.TypeVariable; +import edu.kit.typicalc.model.type.TypeVariableKind; +import edu.kit.typicalc.util.Result; +import org.junit.jupiter.api.Test; + +import java.util.ArrayDeque; +import java.util.ArrayList; +import java.util.Deque; +import java.util.List; + +import static org.junit.jupiter.api.Assertions.assertEquals; + +class UnificationTest { + private static final TypeVariable a = new TypeVariable(TypeVariableKind.TREE, 1); + private static final TypeVariable b = new TypeVariable(TypeVariableKind.TREE, 2); + private static final TypeVariable c = new TypeVariable(TypeVariableKind.TREE, 3); + private static final TypeVariable a4 = new TypeVariable(TypeVariableKind.TREE, 4); + private static final TypeVariable a5 = new TypeVariable(TypeVariableKind.TREE, 5); + private static final TypeVariable a6 = new TypeVariable(TypeVariableKind.TREE, 6); + private static final TypeVariable a7 = new TypeVariable(TypeVariableKind.TREE, 7); + + @Test + void simpleConstraints() { + Deque constraints = new ArrayDeque<>(); + constraints.add(new Constraint(a, new FunctionType(b, c))); + Deque initialConstraints = new ArrayDeque<>(constraints); + Unification u = new Unification(constraints); + List steps = u.getUnificationSteps(); + assertEquals(2, steps.size()); + assertEquals(new UnificationStep(new Result<>(new ArrayList<>()), new ArrayList<>(initialConstraints)), steps.get(0)); + List substitutions = new ArrayList<>(List.of(new Substitution(a, new FunctionType(b, c)))); + assertEquals(new UnificationStep(new Result<>( + substitutions + ), new ArrayList<>()), steps.get(1)); + assertEquals(substitutions, u.getSubstitutions().unwrap()); + } + + @Test + void manyConstraints() { + Deque constraints = new ArrayDeque<>(); + constraints.add(new Constraint(a, new FunctionType(b, c))); + constraints.add(new Constraint(c, new FunctionType(a4, a5))); + constraints.add(new Constraint(a6, new FunctionType(a7, a5))); + constraints.add(new Constraint(a6, a4)); + constraints.add(new Constraint(a7, b)); + Deque initialConstraints = new ArrayDeque<>(constraints); + + Unification u = new Unification(constraints); + List steps = u.getUnificationSteps(); + assertEquals(6, steps.size()); + assertEquals(new UnificationStep(new Result<>(new ArrayList<>()), new ArrayList<>(initialConstraints)), steps.get(0)); + + initialConstraints.removeFirst(); + List substitutions = new ArrayList<>(List.of(new Substitution(a, new FunctionType(b, c)))); + assertEquals(new UnificationStep(new Result<>( + substitutions + ), new ArrayList<>(initialConstraints)), steps.get(1)); + + initialConstraints.removeFirst(); + substitutions.add(new Substitution(c, new FunctionType(a4, a5))); + assertEquals(new UnificationStep(new Result<>( + substitutions + ), new ArrayList<>(initialConstraints)), steps.get(2)); + + initialConstraints.removeFirst(); + initialConstraints.removeFirst(); + initialConstraints.addFirst(new Constraint(new FunctionType(a7, a5), a4)); + substitutions.add(new Substitution(a6, new FunctionType(a7, a5))); + assertEquals(new UnificationStep(new Result<>( + substitutions + ), new ArrayList<>(initialConstraints)), steps.get(3)); + + initialConstraints.removeFirst(); + substitutions.add(new Substitution(a4, new FunctionType(a7, a5))); + assertEquals(new UnificationStep(new Result<>( + substitutions + ), new ArrayList<>(initialConstraints)), steps.get(4)); + + initialConstraints.removeFirst(); + substitutions.add(new Substitution(a7, b)); + assertEquals(new UnificationStep(new Result<>( + substitutions + ), new ArrayList<>(initialConstraints)), steps.get(5)); + + assertEquals(substitutions, u.getSubstitutions().unwrap()); + } + + @Test + void infiniteType() { + Deque constraints = new ArrayDeque<>(); + constraints.add(new Constraint(a, new FunctionType(a, a))); + Deque initialConstraints = new ArrayDeque<>(constraints); + Unification u = new Unification(constraints); + List steps = u.getUnificationSteps(); + assertEquals(2, steps.size()); + assertEquals(new UnificationStep(new Result<>(new ArrayList<>()), new ArrayList<>(initialConstraints)), steps.get(0)); + assertEquals(new UnificationStep(new Result<>(null, + UnificationError.INFINITE_TYPE + ), new ArrayList<>()), steps.get(1)); + } +} diff --git a/src/test/resources/checkstyle.xml b/src/test/resources/checkstyle.xml index 893d8bd..5d17ad8 100644 --- a/src/test/resources/checkstyle.xml +++ b/src/test/resources/checkstyle.xml @@ -37,7 +37,7 @@ - +