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

Test for TypeInferenceResult::getMGU(), order MGU after indices, the kind

Browse Source
This commit is contained in:
Johanna Stuber 2021-01-31 14:21:13 +01:00
parent b09b52e5df
commit d8f6baf615
4 changed files with 67 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -4,6 +4,7 @@ import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeVariable;
import java.util.ArrayList;
import java.util.Comparator;
import java.util.List;
/**
@ -28,6 +29,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()));
finalType = findFinalType(typeVar);
}

5
src/main/java/edu/kit/typicalc/model/type/FunctionType.java
View File

@ -114,6 +114,11 @@ public class FunctionType extends Type {
return parameter;
}
@Override
public String toString() {
return "FunctionType[" + parameter + " -> " + output + ']';
}
@Override
public boolean equals(Object o) {
if (this == o) {

10
src/main/java/edu/kit/typicalc/model/type/TypeVariableKind.java
View File

@ -5,16 +5,16 @@ package edu.kit.typicalc.model.type;
*/
public enum TypeVariableKind {
/**
* Used if the type variable was created from user input.
*/
USER_INPUT,
/**
* Used if the type variable was generated while building the proof tree.
*/
TREE,
/**
* Used if the type variable was created from user input.
*/
USER_INPUT,
/**
* Used if the type variable was generated for a type assumption of a free variable in the input lambda term.
*/

54
src/test/java/edu/kit/typicalc/model/TypeInferenceResultTest.java
View File

@ -1,4 +1,58 @@
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 org.junit.jupiter.api.Test;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.List;
import static org.junit.jupiter.api.Assertions.assertEquals;
class TypeInferenceResultTest {
private static final TypeVariable A_1 = new TypeVariable(TypeVariableKind.TREE, 1);
private static final TypeVariable A_2 = new TypeVariable(TypeVariableKind.TREE, 2);
private static final TypeVariable A_3 = new TypeVariable(TypeVariableKind.TREE, 3);
private static final TypeVariable A_4 = new TypeVariable(TypeVariableKind.TREE, 4);
private static final TypeVariable A_5 = new TypeVariable(TypeVariableKind.TREE, 5);
private static final TypeVariable A_6 = new TypeVariable(TypeVariableKind.TREE, 6);
private static final TypeVariable A_7 = new TypeVariable(TypeVariableKind.TREE, 7);
@Test
void getMGU() {
// rectified example from introduction slides
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);
List<Substitution> expectedMGU = new ArrayList<>(Arrays.asList(
new Substitution(A_1, new FunctionType(A_2, new FunctionType(new FunctionType(A_2, A_5), A_5))),
new Substitution(A_3, new FunctionType(new FunctionType(A_2, A_5), A_5)),
new Substitution(A_4, new FunctionType(A_2, A_5)),
new Substitution(A_6, new FunctionType(A_2, A_5)),
new Substitution(A_7, A_2)
));
assertEquals(expectedMGU, result.getMGU());
// tests if mgu-generation works for substitutions given in reverse order
List<Substitution> substitutions2 = new ArrayList<>(Arrays.asList(
new Substitution(A_1, new FunctionType(A_2, A_3)),
new Substitution(A_3, new FunctionType(A_4, A_5)),
new Substitution(A_6, new FunctionType(A_7, A_5)),
new Substitution(A_4, new FunctionType(A_7, A_5)),
new Substitution(A_7, A_2)
));
TypeInferenceResult result2 = new TypeInferenceResult(substitutions2, A_1);
assertEquals(expectedMGU, result2.getMGU());
}
}