mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-08 18:30:42 +00:00
Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc
This commit is contained in:
commit
cab3fcc4aa
@ -103,14 +103,14 @@ public class Tree implements TermVisitorTree {
|
||||
public InferenceStep visit(AppTerm appTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType) {
|
||||
Type leftType = typeVarFactory.nextTypeVariable();
|
||||
Type rightType = typeVarFactory.nextTypeVariable();
|
||||
InferenceStep leftPremise = appTerm.getFunction().accept(this, typeAssumptions, leftType);
|
||||
|
||||
InferenceStep rightPremise = appTerm.getParameter().accept(this, typeAssumptions, rightType);
|
||||
|
||||
Type function = new FunctionType(rightType, conclusionType);
|
||||
Constraint newConstraint = new Constraint(leftType, function);
|
||||
constraints.add(newConstraint);
|
||||
|
||||
InferenceStep leftPremise = appTerm.getFunction().accept(this, typeAssumptions, leftType);
|
||||
InferenceStep rightPremise = appTerm.getParameter().accept(this, typeAssumptions, rightType);
|
||||
|
||||
Conclusion conclusion = new Conclusion(typeAssumptions, appTerm, conclusionType);
|
||||
return stepFactory.createAppStep(leftPremise, rightPremise, conclusion, newConstraint);
|
||||
}
|
||||
@ -123,12 +123,13 @@ public class Tree implements TermVisitorTree {
|
||||
extendedTypeAssumptions.put(absTerm.getVariable(), assAbs);
|
||||
|
||||
Type premiseType = typeVarFactory.nextTypeVariable();
|
||||
InferenceStep premise = absTerm.getInner().accept(this, extendedTypeAssumptions, premiseType);
|
||||
|
||||
Type function = new FunctionType(assType, premiseType);
|
||||
Constraint newConstraint = new Constraint(conclusionType, function);
|
||||
constraints.add(newConstraint);
|
||||
|
||||
InferenceStep premise = absTerm.getInner().accept(this, extendedTypeAssumptions, premiseType);
|
||||
|
||||
Conclusion conclusion = new Conclusion(typeAssumptions, absTerm, conclusionType);
|
||||
return stepFactory.createAbsStep(premise, conclusion, newConstraint);
|
||||
}
|
||||
@ -159,10 +160,10 @@ public class Tree implements TermVisitorTree {
|
||||
typeInfererLet.getType().orElseThrow(IllegalStateException::new), extendedTypeAssumptions);
|
||||
extendedTypeAssumptions.put(letTerm.getVariable(), newTypeAbstraction);
|
||||
|
||||
premise = letTerm.getInner().accept(this, extendedTypeAssumptions, premiseType);
|
||||
|
||||
constraints.add(newConstraint);
|
||||
constraints.addAll(typeInfererLet.getLetConstraints());
|
||||
|
||||
premise = letTerm.getInner().accept(this, extendedTypeAssumptions, premiseType);
|
||||
} else {
|
||||
premise = new EmptyStep();
|
||||
failedSubInference = true;
|
||||
@ -196,4 +197,22 @@ public class Tree implements TermVisitorTree {
|
||||
Conclusion conclusion = new Conclusion(typeAssumptions, varTerm, conclusionType);
|
||||
return stepFactory.createVarStep(premiseAbs, instantiation, conclusion, newConstraint);
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object o) {
|
||||
if (this == o) {
|
||||
return true;
|
||||
}
|
||||
if (o == null || getClass() != o.getClass()) {
|
||||
return false;
|
||||
}
|
||||
Tree tree = (Tree) o;
|
||||
return failedSubInference == tree.failedSubInference && firstTypeVariable.equals(tree.firstTypeVariable)
|
||||
&& firstInferenceStep.equals(tree.firstInferenceStep) && constraints.equals(tree.constraints);
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
return Objects.hash(firstTypeVariable, firstInferenceStep, constraints, failedSubInference);
|
||||
}
|
||||
}
|
||||
|
@ -6,6 +6,7 @@ import edu.kit.typicalc.model.type.TypeVariable;
|
||||
import java.util.ArrayList;
|
||||
import java.util.Comparator;
|
||||
import java.util.List;
|
||||
import java.util.Objects;
|
||||
|
||||
/**
|
||||
* Models the final result of the type inference with the most general unifier (mgu) and
|
||||
@ -85,4 +86,21 @@ public class TypeInferenceResult {
|
||||
protected Type getType() {
|
||||
return finalType;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object o) {
|
||||
if (this == o) {
|
||||
return true;
|
||||
}
|
||||
if (o == null || getClass() != o.getClass()) {
|
||||
return false;
|
||||
}
|
||||
TypeInferenceResult that = (TypeInferenceResult) o;
|
||||
return mgu.equals(that.mgu) && finalType.equals(that.finalType);
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
return Objects.hash(mgu, finalType);
|
||||
}
|
||||
}
|
||||
|
@ -87,4 +87,22 @@ public class TypeInferer implements TypeInfererInterface {
|
||||
public Optional<Type> getType() {
|
||||
return typeInfResult.map(TypeInferenceResult::getType);
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object o) {
|
||||
if (this == o) {
|
||||
return true;
|
||||
}
|
||||
if (o == null || getClass() != o.getClass()) {
|
||||
return false;
|
||||
}
|
||||
TypeInferer that = (TypeInferer) o;
|
||||
return tree.equals(that.tree) && unification.equals(that.unification)
|
||||
&& typeInfResult.equals(that.typeInfResult);
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
return Objects.hash(tree, unification, typeInfResult);
|
||||
}
|
||||
}
|
||||
|
@ -6,11 +6,7 @@ import edu.kit.typicalc.model.term.VarTerm;
|
||||
import edu.kit.typicalc.model.type.Type;
|
||||
import edu.kit.typicalc.model.type.TypeAbstraction;
|
||||
|
||||
import java.util.ArrayDeque;
|
||||
import java.util.ArrayList;
|
||||
import java.util.List;
|
||||
import java.util.Map;
|
||||
import java.util.Optional;
|
||||
import java.util.*;
|
||||
|
||||
/**
|
||||
* Instances of this implementation of TypeInfererInterface are used to execute the sub-inference starting in let steps.
|
||||
@ -92,4 +88,22 @@ public class TypeInfererLet implements TypeInfererInterface {
|
||||
public Optional<Type> getType() {
|
||||
return typeInfResult.map(TypeInferenceResult::getType);
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object o) {
|
||||
if (this == o) {
|
||||
return true;
|
||||
}
|
||||
if (o == null || getClass() != o.getClass()) {
|
||||
return false;
|
||||
}
|
||||
TypeInfererLet that = (TypeInfererLet) o;
|
||||
return tree.equals(that.tree) && unification.equals(that.unification)
|
||||
&& typeInfResult.equals(that.typeInfResult);
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
return Objects.hash(tree, unification, typeInfResult);
|
||||
}
|
||||
}
|
@ -4,12 +4,7 @@ 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;
|
||||
import java.util.*;
|
||||
|
||||
/**
|
||||
* Models the unification of a type inference with its individual steps.
|
||||
@ -82,4 +77,20 @@ public class Unification {
|
||||
return substitutionsResult;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object o) {
|
||||
if (this == o) {
|
||||
return true;
|
||||
}
|
||||
if (o == null || getClass() != o.getClass()) {
|
||||
return false;
|
||||
}
|
||||
Unification that = (Unification) o;
|
||||
return steps.equals(that.steps) && substitutionsResult.equals(that.substitutionsResult);
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
return Objects.hash(steps, substitutionsResult);
|
||||
}
|
||||
}
|
||||
|
@ -8,8 +8,7 @@ import org.junit.jupiter.api.Test;
|
||||
|
||||
import java.util.*;
|
||||
|
||||
import static org.junit.jupiter.api.Assertions.assertEquals;
|
||||
import static org.junit.jupiter.api.Assertions.assertThrows;
|
||||
import static org.junit.jupiter.api.Assertions.*;
|
||||
|
||||
class TreeTest {
|
||||
|
||||
@ -74,9 +73,9 @@ class TreeTest {
|
||||
assertEquals(expectedStep, tree.getFirstInferenceStep());
|
||||
|
||||
List<Constraint> constraints = new ArrayList<>();
|
||||
constraints.add(appConstraint);
|
||||
constraints.add(varLeftConstraint);
|
||||
constraints.add(varRightConstraint);
|
||||
constraints.add(appConstraint);
|
||||
assertEquals(constraints, tree.getConstraints());
|
||||
}
|
||||
|
||||
@ -101,8 +100,8 @@ class TreeTest {
|
||||
assertEquals(expectedStep, tree.getFirstInferenceStep());
|
||||
|
||||
List<Constraint> constraints = new ArrayList<>();
|
||||
constraints.add(varConstraint);
|
||||
constraints.add(absConstraint);
|
||||
constraints.add(varConstraint);
|
||||
assertEquals(constraints, tree.getConstraints());
|
||||
}
|
||||
|
||||
@ -125,4 +124,44 @@ class TreeTest {
|
||||
assertEquals(expectedStep, tree.getFirstInferenceStep());
|
||||
assertEquals(Collections.singletonList(constraint), tree.getConstraints());
|
||||
}
|
||||
|
||||
@Test
|
||||
void visitLet() {
|
||||
VarTerm x = new VarTerm("x");
|
||||
VarTerm f = new VarTerm("f");
|
||||
TypeVariable generated1 = new TypeVariable(TypeVariableKind.GENERATED_TYPE_ASSUMPTION, 1);
|
||||
TypeVariable variable2 = new TypeVariable(TypeVariableKind.TREE, 2);
|
||||
TypeVariable variable3 = new TypeVariable(TypeVariableKind.TREE, 3);
|
||||
TypeAbstraction generated1Abs = new TypeAbstraction(generated1);
|
||||
|
||||
Map<VarTerm, TypeAbstraction> typeAssumptions = new LinkedHashMap<>();
|
||||
typeAssumptions.put(x, generated1Abs);
|
||||
|
||||
LetTerm letTerm = new LetTerm(f, x, f);
|
||||
Tree tree = new Tree(typeAssumptions, letTerm);
|
||||
|
||||
TypeVariableFactory refFac = new TypeVariableFactory(TypeVariableKind.TREE);
|
||||
refFac.nextTypeVariable();
|
||||
TypeInfererLet typeInfererLet = new TypeInfererLet(x, typeAssumptions, refFac);
|
||||
|
||||
|
||||
Map<VarTerm, TypeAbstraction> varRightTypeAss = new LinkedHashMap<>(typeAssumptions);
|
||||
varRightTypeAss.put(f, generated1Abs);
|
||||
Conclusion varRightConclusion = new Conclusion(varRightTypeAss, f, variable3);
|
||||
Constraint varRightConstraint = new Constraint(variable3, generated1);
|
||||
InferenceStep varRightStep = new VarStepWithLet(generated1Abs, generated1,
|
||||
varRightConclusion, varRightConstraint);
|
||||
|
||||
Conclusion conclusion = new Conclusion(typeAssumptions, letTerm, tree.getFirstTypeVariable());
|
||||
Constraint letConstraint = new Constraint(tree.getFirstTypeVariable(), variable3);
|
||||
InferenceStep expectedStep = new LetStepDefault(conclusion, letConstraint, varRightStep, typeInfererLet);
|
||||
|
||||
assertEquals(expectedStep, tree.getFirstInferenceStep());
|
||||
|
||||
List<Constraint> constraints = new ArrayList<>();
|
||||
constraints.add(letConstraint);
|
||||
constraints.add(new Constraint(variable2, generated1));
|
||||
constraints.add(varRightConstraint);
|
||||
assertEquals(constraints, tree.getConstraints());
|
||||
}
|
||||
}
|
||||
|
48
src/test/java/edu/kit/typicalc/model/TypeInfererLetTest.java
Normal file
48
src/test/java/edu/kit/typicalc/model/TypeInfererLetTest.java
Normal file
@ -0,0 +1,48 @@
|
||||
package edu.kit.typicalc.model;
|
||||
|
||||
import edu.kit.typicalc.model.step.InferenceStep;
|
||||
import edu.kit.typicalc.model.step.VarStepWithLet;
|
||||
import edu.kit.typicalc.model.term.VarTerm;
|
||||
import edu.kit.typicalc.model.type.TypeAbstraction;
|
||||
import edu.kit.typicalc.model.type.TypeVariable;
|
||||
import edu.kit.typicalc.model.type.TypeVariableKind;
|
||||
import org.junit.jupiter.api.Test;
|
||||
|
||||
import java.util.*;
|
||||
|
||||
import static org.junit.jupiter.api.Assertions.assertEquals;
|
||||
import static org.junit.jupiter.api.Assertions.assertTrue;
|
||||
|
||||
class TypeInfererLetTest {
|
||||
|
||||
@Test
|
||||
void createTypeInfererLet() {
|
||||
VarTerm x = new VarTerm("x");
|
||||
TypeVariable generated1 = new TypeVariable(TypeVariableKind.GENERATED_TYPE_ASSUMPTION, 1);
|
||||
TypeVariable variable2 = new TypeVariable(TypeVariableKind.TREE, 2);
|
||||
TypeAbstraction generated1Abs = new TypeAbstraction(generated1);
|
||||
|
||||
Map<VarTerm, TypeAbstraction> typeAssumptions = new LinkedHashMap<>();
|
||||
typeAssumptions.put(x, generated1Abs);
|
||||
|
||||
TypeVariableFactory refFac = new TypeVariableFactory(TypeVariableKind.TREE);
|
||||
refFac.nextTypeVariable();
|
||||
TypeInfererLet typeInfererLet = new TypeInfererLet(x, typeAssumptions, refFac);
|
||||
|
||||
Conclusion varLeftConclusion = new Conclusion(typeAssumptions, x, variable2);
|
||||
Constraint varLeftConstraint = new Constraint(variable2, generated1);
|
||||
InferenceStep varLeftStep = new VarStepWithLet(generated1Abs, generated1,
|
||||
varLeftConclusion, varLeftConstraint);
|
||||
|
||||
assertEquals(varLeftStep, typeInfererLet.getFirstInferenceStep());
|
||||
assertTrue(typeInfererLet.getType().isPresent());
|
||||
assertEquals(generated1, typeInfererLet.getType().get());
|
||||
List<Substitution> expectedMGU
|
||||
= new ArrayList<>(Collections.singletonList(new Substitution(variable2, generated1)));
|
||||
assertTrue(typeInfererLet.getMGU().isPresent());
|
||||
assertEquals(expectedMGU, typeInfererLet.getMGU().get());
|
||||
List<Constraint> expectedLetConstraints
|
||||
= new ArrayList<>(Collections.singletonList(new Constraint(variable2, generated1)));
|
||||
assertEquals(expectedLetConstraints, typeInfererLet.getLetConstraints());
|
||||
}
|
||||
}
|
@ -25,7 +25,8 @@ class LatexCreatorTypeTest {
|
||||
@Test
|
||||
void generatedTypeTest() {
|
||||
typeInferer = model.getTypeInferer("x", new HashMap<>()).unwrap();
|
||||
assertEquals(GENERATED_ASSUMPTION_VARIABLE + "_{1}", new LatexCreatorType(typeInferer.getType().get()).getLatex());
|
||||
assertEquals(GENERATED_ASSUMPTION_VARIABLE + "_{1}",
|
||||
new LatexCreatorType(typeInferer.getType().get()).getLatex());
|
||||
}
|
||||
|
||||
@Test
|
||||
|
Loading…
Reference in New Issue
Block a user