mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-08 18:30:42 +00:00
Tree test visit(absTerm)
This commit is contained in:
parent
71b4a1ab8c
commit
83f34eb00b
@ -3,6 +3,8 @@ package edu.kit.typicalc.model.step;
|
||||
import edu.kit.typicalc.model.Conclusion;
|
||||
import edu.kit.typicalc.model.Constraint;
|
||||
|
||||
import java.util.Objects;
|
||||
|
||||
/**
|
||||
* Models one step of the inference tree where the abstraction rule is applied.
|
||||
*/
|
||||
@ -29,4 +31,23 @@ public abstract class AbsStep extends InferenceStep {
|
||||
return this.premise;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object o) {
|
||||
if (this == o) {
|
||||
return true;
|
||||
}
|
||||
if (o == null || getClass() != o.getClass()) {
|
||||
return false;
|
||||
}
|
||||
if (!super.equals(o)) {
|
||||
return false;
|
||||
}
|
||||
AbsStep absStep = (AbsStep) o;
|
||||
return premise.equals(absStep.premise);
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
return Objects.hash(super.hashCode(), premise);
|
||||
}
|
||||
}
|
||||
|
@ -1,17 +1,18 @@
|
||||
package edu.kit.typicalc.model;
|
||||
|
||||
import edu.kit.typicalc.model.step.AbsStepDefault;
|
||||
import edu.kit.typicalc.model.step.ConstStepDefault;
|
||||
import edu.kit.typicalc.model.step.InferenceStep;
|
||||
import edu.kit.typicalc.model.step.VarStepDefault;
|
||||
import edu.kit.typicalc.model.term.AbsTerm;
|
||||
import edu.kit.typicalc.model.term.ConstTerm;
|
||||
import edu.kit.typicalc.model.term.IntegerTerm;
|
||||
import edu.kit.typicalc.model.term.VarTerm;
|
||||
import edu.kit.typicalc.model.type.NamedType;
|
||||
import edu.kit.typicalc.model.type.TypeAbstraction;
|
||||
import edu.kit.typicalc.model.type.TypeVariableKind;
|
||||
import edu.kit.typicalc.model.type.*;
|
||||
import org.junit.jupiter.api.BeforeAll;
|
||||
import org.junit.jupiter.api.Test;
|
||||
|
||||
import java.util.ArrayList;
|
||||
import java.util.HashMap;
|
||||
import java.util.Map;
|
||||
import java.util.*;
|
||||
|
||||
import static org.junit.jupiter.api.Assertions.assertEquals;
|
||||
import static org.junit.jupiter.api.Assertions.assertThrows;
|
||||
@ -19,9 +20,11 @@ import static org.junit.jupiter.api.Assertions.assertThrows;
|
||||
class TreeTest {
|
||||
|
||||
private static final Map<VarTerm, TypeAbstraction> TYPE_ASSUMPTIONS = new HashMap<>();
|
||||
private static final ConstTerm CONST = new IntegerTerm(10);
|
||||
private static final VarTerm VAR = new VarTerm("var");
|
||||
private static final AbsTerm ABS = new AbsTerm(VAR, VAR);
|
||||
private static final NamedType TYPE = new NamedType("type");
|
||||
private static final TypeAbstraction TYPE_ABS = new TypeAbstraction(TYPE, new ArrayList<>());
|
||||
private static final TypeAbstraction TYPE_ABS = new TypeAbstraction(TYPE);
|
||||
|
||||
@BeforeAll
|
||||
static void setUp() {
|
||||
@ -54,12 +57,41 @@ class TreeTest {
|
||||
});
|
||||
}
|
||||
|
||||
@Test
|
||||
void visitAbs() {
|
||||
TypeVariable variable2 = new TypeVariable(TypeVariableKind.TREE, 2);
|
||||
TypeVariable variable3 = new TypeVariable(TypeVariableKind.TREE, 3);
|
||||
|
||||
Tree tree = new Tree(TYPE_ASSUMPTIONS, ABS);
|
||||
Map<VarTerm, TypeAbstraction> varTypeAss = new HashMap<>(TYPE_ASSUMPTIONS);
|
||||
varTypeAss.put(VAR, new TypeAbstraction(variable2));
|
||||
Conclusion varConclusion = new Conclusion(varTypeAss, VAR, variable3);
|
||||
InferenceStep varStep = new VarStepDefault(new TypeAbstraction(variable2), variable2, varConclusion,
|
||||
new Constraint(variable2, variable3));
|
||||
|
||||
Conclusion conclusion = new Conclusion(TYPE_ASSUMPTIONS, ABS, tree.getFirstTypeVariable());
|
||||
InferenceStep expectedStep = new AbsStepDefault(varStep, conclusion,
|
||||
new Constraint(tree.getFirstTypeVariable(), new FunctionType(variable2, variable3)));
|
||||
assertEquals(expectedStep, tree.getFirstInferenceStep());
|
||||
}
|
||||
|
||||
@Test
|
||||
void visitConst() {
|
||||
Tree tree = new Tree(TYPE_ASSUMPTIONS, CONST);
|
||||
Conclusion conclusion = new Conclusion(TYPE_ASSUMPTIONS, CONST, tree.getFirstTypeVariable());
|
||||
Constraint constraint = new Constraint(NamedType.INT, tree.getFirstTypeVariable());
|
||||
InferenceStep expectedStep = new ConstStepDefault(conclusion, constraint);
|
||||
assertEquals(expectedStep, tree.getFirstInferenceStep());
|
||||
assertEquals(Collections.singletonList(constraint), tree.getConstraints());
|
||||
}
|
||||
|
||||
@Test
|
||||
void visitVar() {
|
||||
Tree tree = new Tree(TYPE_ASSUMPTIONS, VAR);
|
||||
Conclusion conclusion = new Conclusion(TYPE_ASSUMPTIONS, VAR, tree.getFirstTypeVariable());
|
||||
InferenceStep expectedStep = new VarStepDefault(TYPE_ABS, TYPE, conclusion,
|
||||
new Constraint(TYPE, tree.getFirstTypeVariable()));
|
||||
Constraint constraint = new Constraint(TYPE, tree.getFirstTypeVariable());
|
||||
InferenceStep expectedStep = new VarStepDefault(TYPE_ABS, TYPE, conclusion, constraint);
|
||||
assertEquals(expectedStep, tree.getFirstInferenceStep());
|
||||
assertEquals(Collections.singletonList(constraint), tree.getConstraints());
|
||||
}
|
||||
}
|
||||
|
Loading…
Reference in New Issue
Block a user