This commit is contained in:
ucrhh 2021-01-31 13:33:48 +01:00
commit 9acc8fed98
4 changed files with 56 additions and 8 deletions

View File

@ -35,7 +35,7 @@ public class Substitution {
/**
* @return the replacement type
*/
Type getType() {
public Type getType() {
return b;
}

View File

@ -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<Substitution> 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<Substitution> 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<Substitution> 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;
}
}

View File

@ -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

View File

@ -0,0 +1,4 @@
package edu.kit.typicalc.model;
class TypeInferenceResultTest {
}