arnekeller/Typicalc
1
0
Fork 0
mirror of https://gitlab.kit.edu/uskyk/typicalc.git synced 2024-11-08 18:30:42 +00:00
Code Issues Packages Projects Releases Wiki Activity

Unification implementation

Browse Source
This commit is contained in:
Arne Keller 2021-02-02 10:29:45 +01:00
parent 72d7523070
commit 87eaad1d5a
6 changed files with 225 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
src/main/java/edu/kit/typicalc/model/TypeInferer.java
View File

@ -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()) {

65
src/main/java/edu/kit/typicalc/model/Unification.java
View File

@ -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<Constraint> constraints) {
private final List<UnificationStep> steps;
private final Result<List<Substitution>, 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<Constraint> constraints) { // TODO: document List->Deque
steps = new ArrayList<>();
List<Substitution> 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<UnificationActions, UnificationError> 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> substitution = thisStep.getSubstitution();
if (substitution.isPresent()) {
Deque<Constraint> 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<UnificationStep> 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<List<Substitution>, UnificationError> getSubstitutions() {
return new Result<>(null, UnificationError.INFINITE_TYPE); // TODO
return substitutionsResult;
}
}

27
src/main/java/edu/kit/typicalc/model/UnificationStep.java
View File

@ -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<Constraint> 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);
}
}

30
src/main/java/edu/kit/typicalc/util/Result.java
View File

@ -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<T, E> {
*
* @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<T, E> {
}
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);
}
}

104
src/test/java/edu/kit/typicalc/model/UnificationTest.java Normal file
View File

@ -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<Constraint> constraints = new ArrayDeque<>();
constraints.add(new Constraint(a, new FunctionType(b, c)));
Deque<Constraint> initialConstraints = new ArrayDeque<>(constraints);
Unification u = new Unification(constraints);
List<UnificationStep> steps = u.getUnificationSteps();
assertEquals(2, steps.size());
assertEquals(new UnificationStep(new Result<>(new ArrayList<>()), new ArrayList<>(initialConstraints)), steps.get(0));
List<Substitution> 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<Constraint> 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<Constraint> initialConstraints = new ArrayDeque<>(constraints);
Unification u = new Unification(constraints);
List<UnificationStep> steps = u.getUnificationSteps();
assertEquals(6, steps.size());
assertEquals(new UnificationStep(new Result<>(new ArrayList<>()), new ArrayList<>(initialConstraints)), steps.get(0));
initialConstraints.removeFirst();
List<Substitution> 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<Constraint> constraints = new ArrayDeque<>();
constraints.add(new Constraint(a, new FunctionType(a, a)));
Deque<Constraint> initialConstraints = new ArrayDeque<>(constraints);
Unification u = new Unification(constraints);
List<UnificationStep> 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));
}
}

2
src/test/resources/checkstyle.xml
View File

@ -37,7 +37,7 @@
<module name="RedundantImport"/>
<module name="UnusedImports"/>
<module name="ExecutableStatementCount">
<property name="max" value="20"/>
<property name="max" value="25"/>
<property name="tokens" value="CTOR_DEF"/>
</module>
<module name="ExecutableStatementCount">