diff --git a/src/main/java/edu/kit/typicalc/model/Constraint.java b/src/main/java/edu/kit/typicalc/model/Constraint.java index b4fdd9f..b2d2624 100644 --- a/src/main/java/edu/kit/typicalc/model/Constraint.java +++ b/src/main/java/edu/kit/typicalc/model/Constraint.java @@ -11,6 +11,7 @@ public class Constraint { private final Type a; private final Type b; + private int stepIndex = -1; /** * Creates a new constraint using the two types. @@ -24,8 +25,6 @@ public class Constraint { } /** - * Returns the first type - * * @return the first type */ public Type getFirstType() { @@ -33,14 +32,27 @@ public class Constraint { } /** - * Returns the second type - * * @return the second type */ public Type getSecondType() { return b; } + /** + * Set the number of the step that caused this constraint. + * @param index step number + */ + public void setStepIndex(int index) { + this.stepIndex = index; + } + + /** + * @return the step index + */ + public int getStepIndex() { + return stepIndex; + } + @Override public boolean equals(Object o) { if (this == o) { diff --git a/src/main/java/edu/kit/typicalc/model/StepNumberFactory.java b/src/main/java/edu/kit/typicalc/model/StepNumberFactory.java new file mode 100644 index 0000000..7a0323a --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/StepNumberFactory.java @@ -0,0 +1,38 @@ +package edu.kit.typicalc.model; + +import java.util.Objects; + +/** + * Provides the next step number on demand. + */ +public class StepNumberFactory { + + private static final int FIRST_STEP_NUMBER = 0; + + private int nextStepIndex; + + public StepNumberFactory() { + this.nextStepIndex = FIRST_STEP_NUMBER; + } + + public int nextStepIndex() { + return nextStepIndex++; + } + + @Override + public boolean equals(Object o) { + if (this == o) { + return true; + } + if (o == null || getClass() != o.getClass()) { + return false; + } + StepNumberFactory that = (StepNumberFactory) o; + return nextStepIndex == that.nextStepIndex; + } + + @Override + public int hashCode() { + return Objects.hash(nextStepIndex); + } +} diff --git a/src/main/java/edu/kit/typicalc/model/Tree.java b/src/main/java/edu/kit/typicalc/model/Tree.java index fe7825c..a2a6f79 100644 --- a/src/main/java/edu/kit/typicalc/model/Tree.java +++ b/src/main/java/edu/kit/typicalc/model/Tree.java @@ -15,6 +15,7 @@ import java.util.*; public class Tree implements TermVisitorTree { private final TypeVariableFactory typeVarFactory; + private final StepNumberFactory stepNumberFactory; private final StepFactory stepFactory; private final TypeVariable firstTypeVariable; @@ -32,7 +33,8 @@ public class Tree implements TermVisitorTree { * @param lambdaTerm the lambda term to generate the tree for */ protected Tree(Map typeAssumptions, LambdaTerm lambdaTerm) { - this(typeAssumptions, lambdaTerm, new TypeVariableFactory(TypeVariableKind.TREE), false); + this(typeAssumptions, lambdaTerm, new TypeVariableFactory(TypeVariableKind.TREE), false, + new StepNumberFactory()); } /** @@ -46,10 +48,13 @@ public class Tree implements TermVisitorTree { * @param lambdaTerm the lambda term to generate the tree for * @param typeVariableFactory the type variable factory to use * @param partOfLetTerm indicates whether the tree is generated for a sub-inference that is part of a let term + * @param factory step number factory */ protected Tree(Map typeAssumptions, LambdaTerm lambdaTerm, - TypeVariableFactory typeVariableFactory, boolean partOfLetTerm) { + TypeVariableFactory typeVariableFactory, boolean partOfLetTerm, + StepNumberFactory factory) { this.typeVarFactory = typeVariableFactory; + this.stepNumberFactory = factory; this.constraints = new ArrayList<>(); // quantified type assumptions have the same effect as let terms @@ -105,6 +110,7 @@ public class Tree implements TermVisitorTree { @Override public InferenceStep visit(AppTerm appTerm, Map typeAssumptions, Type conclusionType) { + int stepNr = stepNumberFactory.nextStepIndex(); Type leftType = typeVarFactory.nextTypeVariable(); Type rightType = typeVarFactory.nextTypeVariable(); @@ -125,11 +131,12 @@ public class Tree implements TermVisitorTree { } Conclusion conclusion = new Conclusion(typeAssumptions, appTerm, conclusionType); - return stepFactory.createAppStep(leftPremise, rightPremise, conclusion, newConstraint); + return stepFactory.createAppStep(leftPremise, rightPremise, conclusion, newConstraint, stepNr); } @Override public InferenceStep visit(AbsTerm absTerm, Map typeAssumptions, Type conclusionType) { + int stepNr = stepNumberFactory.nextStepIndex(); Map extendedTypeAssumptions = new LinkedHashMap<>(typeAssumptions); Type assType = typeVarFactory.nextTypeVariable(); TypeAbstraction assAbs = new TypeAbstraction(assType); @@ -145,13 +152,14 @@ public class Tree implements TermVisitorTree { InferenceStep premise = absTerm.getInner().accept(this, extendedTypeAssumptions, premiseType); Conclusion conclusion = new Conclusion(typeAssumptions, absTerm, conclusionType); - return stepFactory.createAbsStep(premise, conclusion, newConstraint); + return stepFactory.createAbsStep(premise, conclusion, newConstraint, stepNr); } @Override public InferenceStep visit(LetTerm letTerm, Map typeAssumptions, Type conclusionType) { + int stepNr = stepNumberFactory.nextStepIndex(); TypeInfererLet typeInfererLet = new TypeInfererLet( - letTerm.getVariableDefinition(), typeAssumptions, typeVarFactory); + letTerm.getVariableDefinition(), typeAssumptions, typeVarFactory, stepNumberFactory); Type premiseType = typeVarFactory.nextTypeVariable(); Constraint newConstraint = new Constraint(conclusionType, premiseType); @@ -185,20 +193,22 @@ public class Tree implements TermVisitorTree { } Conclusion conclusion = new Conclusion(typeAssumptions, letTerm, conclusionType); - return stepFactory.createLetStep(conclusion, newConstraint, premise, typeInfererLet); + return stepFactory.createLetStep(conclusion, newConstraint, premise, typeInfererLet, stepNr); } @Override public InferenceStep visit(ConstTerm constant, Map typeAssumptions, Type conclusionType) { + int stepNr = stepNumberFactory.nextStepIndex(); Constraint newConstraint = new Constraint(conclusionType, constant.getType()); constraints.add(newConstraint); Conclusion conclusion = new Conclusion(typeAssumptions, constant, conclusionType); - return stepFactory.createConstStep(conclusion, newConstraint); + return stepFactory.createConstStep(conclusion, newConstraint, stepNr); } @Override public InferenceStep visit(VarTerm varTerm, Map typeAssumptions, Type conclusionType) { + int stepNr = stepNumberFactory.nextStepIndex(); TypeAbstraction premiseAbs = typeAssumptions.get(varTerm); if (premiseAbs == null) { throw new IllegalStateException("Cannot create VarStep for VarTerm '" @@ -210,7 +220,7 @@ public class Tree implements TermVisitorTree { constraints.add(newConstraint); Conclusion conclusion = new Conclusion(typeAssumptions, varTerm, conclusionType); - return stepFactory.createVarStep(premiseAbs, instantiation, conclusion, newConstraint); + return stepFactory.createVarStep(premiseAbs, instantiation, conclusion, newConstraint, stepNr); } @Override @@ -223,11 +233,12 @@ public class Tree implements TermVisitorTree { } Tree tree = (Tree) o; return failedSubInference == tree.failedSubInference && firstTypeVariable.equals(tree.firstTypeVariable) - && firstInferenceStep.equals(tree.firstInferenceStep) && constraints.equals(tree.constraints); + && firstInferenceStep.equals(tree.firstInferenceStep) && constraints.equals(tree.constraints) + && stepNumberFactory.equals(tree.stepNumberFactory); } @Override public int hashCode() { - return Objects.hash(firstTypeVariable, firstInferenceStep, constraints, failedSubInference); + return Objects.hash(firstTypeVariable, firstInferenceStep, constraints, failedSubInference, stepNumberFactory); } } diff --git a/src/main/java/edu/kit/typicalc/model/TypeInfererLet.java b/src/main/java/edu/kit/typicalc/model/TypeInfererLet.java index eafe6e7..c57bda9 100644 --- a/src/main/java/edu/kit/typicalc/model/TypeInfererLet.java +++ b/src/main/java/edu/kit/typicalc/model/TypeInfererLet.java @@ -28,10 +28,11 @@ public class TypeInfererLet implements TypeInfererInterface { * @param typeAssumptions the type assumptions to consider when generating the tree * @param typeVarFactory the type variable factory that should be used in this inference to guarantee consistency * with the outer inference + * @param factory the step number factory to pass to the Tree */ protected TypeInfererLet(LambdaTerm lambdaTerm, Map typeAssumptions, - TypeVariableFactory typeVarFactory) { - tree = new Tree(typeAssumptions, lambdaTerm, typeVarFactory, true); + TypeVariableFactory typeVarFactory, StepNumberFactory factory) { + tree = new Tree(typeAssumptions, lambdaTerm, typeVarFactory, true, factory); // cancel algorithm if a sub-inference failed if (tree.hasFailedSubInference()) { diff --git a/src/main/java/edu/kit/typicalc/model/step/AbsStep.java b/src/main/java/edu/kit/typicalc/model/step/AbsStep.java index ee59b27..9810c2f 100644 --- a/src/main/java/edu/kit/typicalc/model/step/AbsStep.java +++ b/src/main/java/edu/kit/typicalc/model/step/AbsStep.java @@ -18,9 +18,10 @@ public abstract class AbsStep extends InferenceStep { * @param premise the premise of this step * @param conclusion the conclusion of this step * @param constraint the constraint added in this step + * @param stepIndex step number */ - protected AbsStep(InferenceStep premise, Conclusion conclusion, Constraint constraint) { - super(conclusion, constraint); + protected AbsStep(InferenceStep premise, Conclusion conclusion, Constraint constraint, int stepIndex) { + super(conclusion, constraint, stepIndex); this.premise = premise; } diff --git a/src/main/java/edu/kit/typicalc/model/step/AbsStepDefault.java b/src/main/java/edu/kit/typicalc/model/step/AbsStepDefault.java index c97be2a..3207a57 100644 --- a/src/main/java/edu/kit/typicalc/model/step/AbsStepDefault.java +++ b/src/main/java/edu/kit/typicalc/model/step/AbsStepDefault.java @@ -14,9 +14,10 @@ public class AbsStepDefault extends AbsStep { * @param premise the premise of this step * @param conclusion the conclusion of this step * @param constraint the constraint added in this step + * @param stepIndex step number */ - public AbsStepDefault(InferenceStep premise, Conclusion conclusion, Constraint constraint) { - super(premise, conclusion, constraint); + public AbsStepDefault(InferenceStep premise, Conclusion conclusion, Constraint constraint, int stepIndex) { + super(premise, conclusion, constraint, stepIndex); } /** diff --git a/src/main/java/edu/kit/typicalc/model/step/AbsStepWithLet.java b/src/main/java/edu/kit/typicalc/model/step/AbsStepWithLet.java index 852ed22..24778e0 100644 --- a/src/main/java/edu/kit/typicalc/model/step/AbsStepWithLet.java +++ b/src/main/java/edu/kit/typicalc/model/step/AbsStepWithLet.java @@ -14,9 +14,10 @@ public class AbsStepWithLet extends AbsStep { * @param premise the premise of this step * @param conclusion the conclusion of this step * @param constraint constraint that can be derived from this step + * @param stepIndex step number */ - public AbsStepWithLet(InferenceStep premise, Conclusion conclusion, Constraint constraint) { - super(premise, conclusion, constraint); + public AbsStepWithLet(InferenceStep premise, Conclusion conclusion, Constraint constraint, int stepIndex) { + super(premise, conclusion, constraint, stepIndex); } /** diff --git a/src/main/java/edu/kit/typicalc/model/step/AppStep.java b/src/main/java/edu/kit/typicalc/model/step/AppStep.java index 65441a9..8a6b270 100644 --- a/src/main/java/edu/kit/typicalc/model/step/AppStep.java +++ b/src/main/java/edu/kit/typicalc/model/step/AppStep.java @@ -16,15 +16,17 @@ public abstract class AppStep extends InferenceStep { private final InferenceStep premise2; /** - * Initializes a new AbsStepWithLet with the given values. + * Initializes a new AbsStep with the given values. * * @param premise1 the first premise of this step * @param premise2 the second premise of this step * @param conclusion the conclusion of this step * @param constraint constraint that can be derived from this step + * @param stepIndex step number */ - protected AppStep(InferenceStep premise1, InferenceStep premise2, Conclusion conclusion, Constraint constraint) { - super(conclusion, constraint); + protected AppStep(InferenceStep premise1, InferenceStep premise2, Conclusion conclusion, Constraint constraint, + int stepIndex) { + super(conclusion, constraint, stepIndex); this.premise1 = premise1; this.premise2 = premise2; } diff --git a/src/main/java/edu/kit/typicalc/model/step/AppStepDefault.java b/src/main/java/edu/kit/typicalc/model/step/AppStepDefault.java index 61a1df2..7bdb606 100644 --- a/src/main/java/edu/kit/typicalc/model/step/AppStepDefault.java +++ b/src/main/java/edu/kit/typicalc/model/step/AppStepDefault.java @@ -9,16 +9,17 @@ import edu.kit.typicalc.model.Constraint; */ public class AppStepDefault extends AppStep { /** - * Initializes a new AbsStepWithLet with the given values. + * Initializes a new AbsStepDefault with the given values. * * @param premise1 the first premise of this step * @param premise2 the second premise of this step * @param conclusion the conclusion of this step * @param constraint constraint that can be derived from this step + * @param stepIndex step number */ public AppStepDefault(InferenceStep premise1, InferenceStep premise2, - Conclusion conclusion, Constraint constraint) { - super(premise1, premise2, conclusion, constraint); + Conclusion conclusion, Constraint constraint, int stepIndex) { + super(premise1, premise2, conclusion, constraint, stepIndex); } /** diff --git a/src/main/java/edu/kit/typicalc/model/step/ConstStep.java b/src/main/java/edu/kit/typicalc/model/step/ConstStep.java index 58d03b2..57eb335 100644 --- a/src/main/java/edu/kit/typicalc/model/step/ConstStep.java +++ b/src/main/java/edu/kit/typicalc/model/step/ConstStep.java @@ -12,8 +12,9 @@ public abstract class ConstStep extends InferenceStep { * * @param conclusion the conclusion of this step * @param constraint the constraint added in this step + * @param stepIndex step number */ - protected ConstStep(Conclusion conclusion, Constraint constraint) { - super(conclusion, constraint); + protected ConstStep(Conclusion conclusion, Constraint constraint, int stepIndex) { + super(conclusion, constraint, stepIndex); } } diff --git a/src/main/java/edu/kit/typicalc/model/step/ConstStepDefault.java b/src/main/java/edu/kit/typicalc/model/step/ConstStepDefault.java index baa9535..3abf6a1 100644 --- a/src/main/java/edu/kit/typicalc/model/step/ConstStepDefault.java +++ b/src/main/java/edu/kit/typicalc/model/step/ConstStepDefault.java @@ -14,9 +14,10 @@ public class ConstStepDefault extends ConstStep { * * @param conclusion the conclusion of this step * @param constraint the constraint added in this step + * @param stepIndex step number */ - public ConstStepDefault(Conclusion conclusion, Constraint constraint) { - super(conclusion, constraint); + public ConstStepDefault(Conclusion conclusion, Constraint constraint, int stepIndex) { + super(conclusion, constraint, stepIndex); } /** diff --git a/src/main/java/edu/kit/typicalc/model/step/EmptyStep.java b/src/main/java/edu/kit/typicalc/model/step/EmptyStep.java index 117c455..bd12263 100644 --- a/src/main/java/edu/kit/typicalc/model/step/EmptyStep.java +++ b/src/main/java/edu/kit/typicalc/model/step/EmptyStep.java @@ -19,7 +19,8 @@ public class EmptyStep extends InferenceStep { public EmptyStep() { super( new Conclusion(Collections.emptyMap(), new VarTerm(""), new NamedType("")), - new Constraint(new NamedType(""), new NamedType("")) + new Constraint(new NamedType(""), new NamedType("")), + -1 // TODO: check if this actually works ); } diff --git a/src/main/java/edu/kit/typicalc/model/step/InferenceStep.java b/src/main/java/edu/kit/typicalc/model/step/InferenceStep.java index f47e4f9..f9c1cff 100644 --- a/src/main/java/edu/kit/typicalc/model/step/InferenceStep.java +++ b/src/main/java/edu/kit/typicalc/model/step/InferenceStep.java @@ -17,16 +17,19 @@ import java.util.Objects; public abstract class InferenceStep { private final Conclusion conclusion; private final Constraint constraint; + private final int stepIndex; /** * Initializes a new InferenceStep with the given values. * * @param conclusion the conclusion of this step * @param constraint the constraint added in this step + * @param stepIndex step number */ - protected InferenceStep(Conclusion conclusion, Constraint constraint) { + protected InferenceStep(Conclusion conclusion, Constraint constraint, int stepIndex) { this.conclusion = conclusion; this.constraint = constraint; + this.stepIndex = stepIndex; } /** @@ -63,11 +66,11 @@ public abstract class InferenceStep { return false; } InferenceStep that = (InferenceStep) o; - return conclusion.equals(that.conclusion) && constraint.equals(that.constraint); + return conclusion.equals(that.conclusion) && constraint.equals(that.constraint) && stepIndex == that.stepIndex; } @Override public int hashCode() { - return Objects.hash(conclusion, constraint); + return Objects.hash(conclusion, constraint, stepIndex); } } \ No newline at end of file diff --git a/src/main/java/edu/kit/typicalc/model/step/LetStep.java b/src/main/java/edu/kit/typicalc/model/step/LetStep.java index ddf610f..16dcaca 100644 --- a/src/main/java/edu/kit/typicalc/model/step/LetStep.java +++ b/src/main/java/edu/kit/typicalc/model/step/LetStep.java @@ -27,9 +27,11 @@ public abstract class LetStep extends InferenceStep { * @param premise the right premise of this step * @param typeInferer the typeInferer that performs the Type Inference for the premise * that needs its own type Inference. + * @param stepIndex step number */ - protected LetStep(Conclusion conclusion, Constraint constraint, InferenceStep premise, TypeInfererLet typeInferer) { - super(conclusion, constraint); + protected LetStep(Conclusion conclusion, Constraint constraint, InferenceStep premise, TypeInfererLet typeInferer, + int stepIndex) { + super(conclusion, constraint, stepIndex); this.premise = premise; this.typeInferer = typeInferer; } diff --git a/src/main/java/edu/kit/typicalc/model/step/LetStepDefault.java b/src/main/java/edu/kit/typicalc/model/step/LetStepDefault.java index 3e4a16e..956d835 100644 --- a/src/main/java/edu/kit/typicalc/model/step/LetStepDefault.java +++ b/src/main/java/edu/kit/typicalc/model/step/LetStepDefault.java @@ -16,10 +16,11 @@ public class LetStepDefault extends LetStep { * @param premise the right premise of this step * @param typeInferer the typeInferer that performs the Type Inference for the premise * that needs its own type Inference. + * @param stepIndex step number */ public LetStepDefault(Conclusion conclusion, Constraint constraint, InferenceStep premise, - TypeInfererLet typeInferer) { - super(conclusion, constraint, premise, typeInferer); + TypeInfererLet typeInferer, int stepIndex) { + super(conclusion, constraint, premise, typeInferer, stepIndex); } /** diff --git a/src/main/java/edu/kit/typicalc/model/step/OnlyConclusionStep.java b/src/main/java/edu/kit/typicalc/model/step/OnlyConclusionStep.java index 588ec38..48649b2 100644 --- a/src/main/java/edu/kit/typicalc/model/step/OnlyConclusionStep.java +++ b/src/main/java/edu/kit/typicalc/model/step/OnlyConclusionStep.java @@ -19,7 +19,8 @@ public class OnlyConclusionStep extends InferenceStep { public OnlyConclusionStep(Conclusion conclusion) { super( conclusion, - new Constraint(new NamedType(""), new NamedType("")) + new Constraint(new NamedType(""), new NamedType("")), + -1 // TODO: check whether this is correct ); } diff --git a/src/main/java/edu/kit/typicalc/model/step/StepFactory.java b/src/main/java/edu/kit/typicalc/model/step/StepFactory.java index 1e0776b..8938112 100644 --- a/src/main/java/edu/kit/typicalc/model/step/StepFactory.java +++ b/src/main/java/edu/kit/typicalc/model/step/StepFactory.java @@ -18,7 +18,7 @@ public interface StepFactory { * @param constraint the constraint that can be derived from this step * @return the created AbsStep */ - AbsStep createAbsStep(InferenceStep premise, Conclusion conclusion, Constraint constraint); + AbsStep createAbsStep(InferenceStep premise, Conclusion conclusion, Constraint constraint, int stepIndex); /** * Creates an AppStep. @@ -30,7 +30,7 @@ public interface StepFactory { * @return the created AppStep */ AppStep createAppStep(InferenceStep premise1, InferenceStep premise2, - Conclusion conclusion, Constraint constraint); + Conclusion conclusion, Constraint constraint, int stepIndex); /** * Creates an ConstStep. @@ -39,7 +39,7 @@ public interface StepFactory { * @param constraint the constraint that can be derived from this step * @return the created ConstStep */ - ConstStep createConstStep(Conclusion conclusion, Constraint constraint); + ConstStep createConstStep(Conclusion conclusion, Constraint constraint, int stepIndex); /** * Creates a VarStep. @@ -51,7 +51,7 @@ public interface StepFactory { * @return the created AbsStep */ VarStep createVarStep(TypeAbstraction typeAbstraction, Type instantiatedTypeAbs, - Conclusion conclusion, Constraint constraint); + Conclusion conclusion, Constraint constraint, int stepIndex); /** * Creates a LetStep. @@ -63,5 +63,5 @@ public interface StepFactory { * @return the created AppStep */ LetStep createLetStep(Conclusion conclusion, Constraint constraint, - InferenceStep premise, TypeInfererLet typeInferer); + InferenceStep premise, TypeInfererLet typeInferer, int stepIndex); } diff --git a/src/main/java/edu/kit/typicalc/model/step/StepFactoryDefault.java b/src/main/java/edu/kit/typicalc/model/step/StepFactoryDefault.java index 58906fb..ca6ca35 100644 --- a/src/main/java/edu/kit/typicalc/model/step/StepFactoryDefault.java +++ b/src/main/java/edu/kit/typicalc/model/step/StepFactoryDefault.java @@ -11,17 +11,10 @@ import edu.kit.typicalc.model.type.TypeAbstraction; */ public class StepFactoryDefault implements StepFactory { - /** - * Creates an AbsStepDefault. - * - * @param premise the premise of this step - * @param conclusion the conclusion of this step - * @param constraint the constraint that can be derived from this step - * @return the created AbsStepDefault - */ @Override - public AbsStepDefault createAbsStep(InferenceStep premise, Conclusion conclusion, Constraint constraint) { - return new AbsStepDefault(premise, conclusion, constraint); + public AbsStepDefault createAbsStep(InferenceStep premise, Conclusion conclusion, Constraint constraint, + int stepIndex) { + return new AbsStepDefault(premise, conclusion, constraint, stepIndex); } /** @@ -35,8 +28,8 @@ public class StepFactoryDefault implements StepFactory { */ @Override public AppStepDefault createAppStep(InferenceStep premise1, InferenceStep premise2, - Conclusion conclusion, Constraint constraint) { - return new AppStepDefault(premise1, premise2, conclusion, constraint); + Conclusion conclusion, Constraint constraint, int stepIndex) { + return new AppStepDefault(premise1, premise2, conclusion, constraint, stepIndex); } /** @@ -47,8 +40,8 @@ public class StepFactoryDefault implements StepFactory { * @return the created ConstStepDefault */ @Override - public ConstStepDefault createConstStep(Conclusion conclusion, Constraint constraint) { - return new ConstStepDefault(conclusion, constraint); + public ConstStepDefault createConstStep(Conclusion conclusion, Constraint constraint, int stepIndex) { + return new ConstStepDefault(conclusion, constraint, stepIndex); } /** @@ -62,8 +55,8 @@ public class StepFactoryDefault implements StepFactory { */ @Override public VarStepDefault createVarStep(TypeAbstraction typeAbstraction, Type instantiatedTypeAbs, - Conclusion conclusion, Constraint constraint) { - return new VarStepDefault(typeAbstraction, instantiatedTypeAbs, conclusion, constraint); + Conclusion conclusion, Constraint constraint, int stepIndex) { + return new VarStepDefault(typeAbstraction, instantiatedTypeAbs, conclusion, constraint, stepIndex); } /** @@ -80,7 +73,7 @@ public class StepFactoryDefault implements StepFactory { */ @Override public LetStep createLetStep(Conclusion conclusion, Constraint constraint, - InferenceStep premise, TypeInfererLet typeInferer) { + InferenceStep premise, TypeInfererLet typeInferer, int stepIndex) { throw new UnsupportedOperationException("Not possible to create LetStep when no let is present in the term"); } } diff --git a/src/main/java/edu/kit/typicalc/model/step/StepFactoryWithLet.java b/src/main/java/edu/kit/typicalc/model/step/StepFactoryWithLet.java index 5b26baf..5a20c25 100644 --- a/src/main/java/edu/kit/typicalc/model/step/StepFactoryWithLet.java +++ b/src/main/java/edu/kit/typicalc/model/step/StepFactoryWithLet.java @@ -11,32 +11,16 @@ import edu.kit.typicalc.model.type.TypeAbstraction; */ public class StepFactoryWithLet implements StepFactory { - /** - * Creates an AbsStepWithLet. - * - * @param premise the premise of this step - * @param conclusion the conclusion of this step - * @param constraint the constraint that can be derived from this step - * @return the created AbsStepWithLet - */ @Override - public AbsStepWithLet createAbsStep(InferenceStep premise, Conclusion conclusion, Constraint constraint) { - return new AbsStepWithLet(premise, conclusion, constraint); + public AbsStepWithLet createAbsStep(InferenceStep premise, Conclusion conclusion, Constraint constraint, + int stepIndex) { + return new AbsStepWithLet(premise, conclusion, constraint, stepIndex); } - /** - * Creates an AppStepDefault. - * - * @param premise1 the first premise of this step - * @param premise2 the second premise of this step - * @param conclusion the conclusion of this step - * @param constraint the constraint that can be derived from this step - * @return the created AppStepDefault - */ @Override public AppStepDefault createAppStep(InferenceStep premise1, InferenceStep premise2, - Conclusion conclusion, Constraint constraint) { - return new AppStepDefault(premise1, premise2, conclusion, constraint); + Conclusion conclusion, Constraint constraint, int stepIndex) { + return new AppStepDefault(premise1, premise2, conclusion, constraint, stepIndex); } /** @@ -47,8 +31,8 @@ public class StepFactoryWithLet implements StepFactory { * @return the created ConstStepDefault */ @Override - public ConstStepDefault createConstStep(Conclusion conclusion, Constraint constraint) { - return new ConstStepDefault(conclusion, constraint); + public ConstStepDefault createConstStep(Conclusion conclusion, Constraint constraint, int stepIndex) { + return new ConstStepDefault(conclusion, constraint, stepIndex); } /** @@ -62,8 +46,9 @@ public class StepFactoryWithLet implements StepFactory { */ @Override public VarStepWithLet createVarStep(TypeAbstraction typeAbstraction, Type instantiatedTypeAbs, - Conclusion conclusion, Constraint constraint) { - return new VarStepWithLet(typeAbstraction, instantiatedTypeAbs, conclusion, constraint); + Conclusion conclusion, Constraint constraint, int stepIndex) { + return new VarStepWithLet(typeAbstraction, instantiatedTypeAbs, conclusion, constraint, + stepIndex); } /** @@ -77,7 +62,7 @@ public class StepFactoryWithLet implements StepFactory { */ @Override public LetStepDefault createLetStep(Conclusion conclusion, Constraint constraint, - InferenceStep premise, TypeInfererLet typeInferer) { - return new LetStepDefault(conclusion, constraint, premise, typeInferer); + InferenceStep premise, TypeInfererLet typeInferer, int stepIndex) { + return new LetStepDefault(conclusion, constraint, premise, typeInferer, stepIndex); } } diff --git a/src/main/java/edu/kit/typicalc/model/step/VarStep.java b/src/main/java/edu/kit/typicalc/model/step/VarStep.java index b89d3be..4884f1c 100644 --- a/src/main/java/edu/kit/typicalc/model/step/VarStep.java +++ b/src/main/java/edu/kit/typicalc/model/step/VarStep.java @@ -23,10 +23,11 @@ public abstract class VarStep extends InferenceStep { * @param instantiatedTypeAbs an instantiation of the type abstraction used in this step * @param conclusion the conclusion of this step * @param constraint the constraint added in this step + * @param stepIndex step number */ protected VarStep(TypeAbstraction typeAbstractionInPremise, Type instantiatedTypeAbs, Conclusion conclusion, - Constraint constraint) { - super(conclusion, constraint); + Constraint constraint, int stepIndex) { + super(conclusion, constraint, stepIndex); this.typeAbstractionInPremise = typeAbstractionInPremise; this.instantiatedTypeAbs = instantiatedTypeAbs; } diff --git a/src/main/java/edu/kit/typicalc/model/step/VarStepDefault.java b/src/main/java/edu/kit/typicalc/model/step/VarStepDefault.java index c06e864..5d5ee16 100644 --- a/src/main/java/edu/kit/typicalc/model/step/VarStepDefault.java +++ b/src/main/java/edu/kit/typicalc/model/step/VarStepDefault.java @@ -17,10 +17,11 @@ public class VarStepDefault extends VarStep { * @param instantiatedTypeAbs an instantiation of the type abstraction used in this step * @param conclusion the conclusion of this step * @param constraint the constraint added in this step + * @param stepIndex step number */ public VarStepDefault(TypeAbstraction typeAbstractionInPremise, Type instantiatedTypeAbs, Conclusion conclusion, - Constraint constraint) { - super(typeAbstractionInPremise, instantiatedTypeAbs, conclusion, constraint); + Constraint constraint, int stepIndex) { + super(typeAbstractionInPremise, instantiatedTypeAbs, conclusion, constraint, stepIndex); } /** diff --git a/src/main/java/edu/kit/typicalc/model/step/VarStepWithLet.java b/src/main/java/edu/kit/typicalc/model/step/VarStepWithLet.java index 41f3c72..6f3f0ca 100644 --- a/src/main/java/edu/kit/typicalc/model/step/VarStepWithLet.java +++ b/src/main/java/edu/kit/typicalc/model/step/VarStepWithLet.java @@ -18,10 +18,11 @@ public class VarStepWithLet extends VarStep { * @param instantiatedTypeAbs an instantiation of the type abstraction used in this step * @param conclusion the conclusion of this step * @param constraint the constraint added in this step + * @param stepIndex step number */ public VarStepWithLet(TypeAbstraction typeAbstractionInPremise, Type instantiatedTypeAbs, Conclusion conclusion, - Constraint constraint) { - super(typeAbstractionInPremise, instantiatedTypeAbs, conclusion, constraint); + Constraint constraint, int stepIndex) { + super(typeAbstractionInPremise, instantiatedTypeAbs, conclusion, constraint, stepIndex); } /** diff --git a/src/test/java/edu/kit/typicalc/model/ConstraintTest.java b/src/test/java/edu/kit/typicalc/model/ConstraintTest.java index ae97601..3593388 100644 --- a/src/test/java/edu/kit/typicalc/model/ConstraintTest.java +++ b/src/test/java/edu/kit/typicalc/model/ConstraintTest.java @@ -15,7 +15,7 @@ class ConstraintTest { @Test void equalsTest() { - EqualsVerifier.forClass(Constraint.class).usingGetClass().verify(); + EqualsVerifier.forClass(Constraint.class).usingGetClass().withIgnoredFields("stepIndex").verify(); } @Test diff --git a/src/test/java/edu/kit/typicalc/model/ModelImplTest.java b/src/test/java/edu/kit/typicalc/model/ModelImplTest.java index 687034a..482e393 100644 --- a/src/test/java/edu/kit/typicalc/model/ModelImplTest.java +++ b/src/test/java/edu/kit/typicalc/model/ModelImplTest.java @@ -51,10 +51,12 @@ class ModelImplTest { x, new TypeAbstraction(NamedType.INT), y, new TypeAbstraction(a2)), x, a3), - new Constraint(a3, NamedType.INT) + new Constraint(a3, NamedType.INT), + 1 ), new Conclusion(Map.of(x, new TypeAbstraction(NamedType.INT)), term, a1), - new Constraint(a1, new FunctionType(a2, a3)) + new Constraint(a1, new FunctionType(a2, a3)), + 0 ), typeInference.getFirstInferenceStep() ); } diff --git a/src/test/java/edu/kit/typicalc/model/TreeTest.java b/src/test/java/edu/kit/typicalc/model/TreeTest.java index baed83a..8464fda 100644 --- a/src/test/java/edu/kit/typicalc/model/TreeTest.java +++ b/src/test/java/edu/kit/typicalc/model/TreeTest.java @@ -42,7 +42,7 @@ class TreeTest { factory.nextTypeVariable(); factoryRef.nextTypeVariable(); } - Tree tree = new Tree(TYPE_ASSUMPTIONS, VAR, factory, false); + Tree tree = new Tree(TYPE_ASSUMPTIONS, VAR, factory, false, new StepNumberFactory()); assertEquals(tree.getFirstTypeVariable(), factoryRef.nextTypeVariable()); } @@ -63,15 +63,15 @@ class TreeTest { Conclusion varLeftConclusion = new Conclusion(TYPE_ASSUMPTIONS, VAR, variable2); Constraint varLeftConstraint = new Constraint(variable2, TYPE); - InferenceStep varLeftStep = new VarStepDefault(TYPE_ABS, TYPE, varLeftConclusion, varLeftConstraint); + InferenceStep varLeftStep = new VarStepDefault(TYPE_ABS, TYPE, varLeftConclusion, varLeftConstraint, 1); Conclusion varRightConclusion = new Conclusion(TYPE_ASSUMPTIONS, VAR, variable3); Constraint varRightConstraint = new Constraint(variable3, TYPE); - InferenceStep varRightStep = new VarStepDefault(TYPE_ABS, TYPE, varRightConclusion, varRightConstraint); + InferenceStep varRightStep = new VarStepDefault(TYPE_ABS, TYPE, varRightConclusion, varRightConstraint, 2); Conclusion conclusion = new Conclusion(TYPE_ASSUMPTIONS, APP, tree.getFirstTypeVariable()); Constraint appConstraint = new Constraint(variable2, new FunctionType(variable3, tree.getFirstTypeVariable())); - InferenceStep expectedStep = new AppStepDefault(varLeftStep, varRightStep, conclusion, appConstraint); + InferenceStep expectedStep = new AppStepDefault(varLeftStep, varRightStep, conclusion, appConstraint, 0); assertEquals(expectedStep, tree.getFirstInferenceStep()); @@ -94,11 +94,11 @@ class TreeTest { Conclusion varConclusion = new Conclusion(varTypeAss, VAR, variable3); Constraint varConstraint = new Constraint(variable2, variable3); InferenceStep varStep = new VarStepDefault(new TypeAbstraction(variable2), variable2, varConclusion, - varConstraint); + varConstraint, 1); Conclusion conclusion = new Conclusion(TYPE_ASSUMPTIONS, ABS, tree.getFirstTypeVariable()); Constraint absConstraint = new Constraint(tree.getFirstTypeVariable(), new FunctionType(variable2, variable3)); - InferenceStep expectedStep = new AbsStepDefault(varStep, conclusion, absConstraint); + InferenceStep expectedStep = new AbsStepDefault(varStep, conclusion, absConstraint, 0); assertEquals(expectedStep, tree.getFirstInferenceStep()); @@ -113,7 +113,7 @@ class TreeTest { 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); + InferenceStep expectedStep = new ConstStepDefault(conclusion, constraint, 0); assertEquals(expectedStep, tree.getFirstInferenceStep()); assertEquals(Collections.singletonList(constraint), tree.getConstraints()); } @@ -123,7 +123,7 @@ class TreeTest { Tree tree = new Tree(TYPE_ASSUMPTIONS, VAR); Conclusion conclusion = new Conclusion(TYPE_ASSUMPTIONS, VAR, tree.getFirstTypeVariable()); Constraint constraint = new Constraint(TYPE, tree.getFirstTypeVariable()); - InferenceStep expectedStep = new VarStepDefault(TYPE_ABS, TYPE, conclusion, constraint); + InferenceStep expectedStep = new VarStepDefault(TYPE_ABS, TYPE, conclusion, constraint, 0); assertEquals(expectedStep, tree.getFirstInferenceStep()); assertEquals(Collections.singletonList(constraint), tree.getConstraints()); } @@ -144,8 +144,11 @@ class TreeTest { Tree tree = new Tree(typeAssumptions, letTerm); TypeVariableFactory refFac = new TypeVariableFactory(TypeVariableKind.TREE); + StepNumberFactory nrFactory = new StepNumberFactory(); refFac.nextTypeVariable(); - TypeInfererLet typeInfererLet = new TypeInfererLet(x, typeAssumptions, refFac); + nrFactory.nextStepIndex(); + TypeInfererLet typeInfererLet = new TypeInfererLet(x, typeAssumptions, refFac, nrFactory); + nrFactory.nextStepIndex(); Map varRightTypeAss = new LinkedHashMap<>(typeAssumptions); @@ -153,11 +156,11 @@ class TreeTest { Conclusion varRightConclusion = new Conclusion(varRightTypeAss, f, variable3); Constraint varRightConstraint = new Constraint(variable3, generated1); InferenceStep varRightStep = new VarStepWithLet(generated1Abs, generated1, - varRightConclusion, varRightConstraint); + varRightConclusion, varRightConstraint, 2); Conclusion conclusion = new Conclusion(typeAssumptions, letTerm, tree.getFirstTypeVariable()); Constraint letConstraint = new Constraint(tree.getFirstTypeVariable(), variable3); - InferenceStep expectedStep = new LetStepDefault(conclusion, letConstraint, varRightStep, typeInfererLet); + InferenceStep expectedStep = new LetStepDefault(conclusion, letConstraint, varRightStep, typeInfererLet, 0); assertEquals(expectedStep, tree.getFirstInferenceStep()); diff --git a/src/test/java/edu/kit/typicalc/model/TypeInfererLetTest.java b/src/test/java/edu/kit/typicalc/model/TypeInfererLetTest.java index 7f345b2..3555e29 100644 --- a/src/test/java/edu/kit/typicalc/model/TypeInfererLetTest.java +++ b/src/test/java/edu/kit/typicalc/model/TypeInfererLetTest.java @@ -28,12 +28,12 @@ class TypeInfererLetTest { TypeVariableFactory refFac = new TypeVariableFactory(TypeVariableKind.TREE); refFac.nextTypeVariable(); - TypeInfererLet typeInfererLet = new TypeInfererLet(x, typeAssumptions, refFac); + TypeInfererLet typeInfererLet = new TypeInfererLet(x, typeAssumptions, refFac, new StepNumberFactory()); Conclusion varLeftConclusion = new Conclusion(typeAssumptions, x, variable2); Constraint varLeftConstraint = new Constraint(variable2, generated1); InferenceStep varLeftStep = new VarStepWithLet(generated1Abs, generated1, - varLeftConclusion, varLeftConstraint); + varLeftConclusion, varLeftConstraint, 0); assertEquals(varLeftStep, typeInfererLet.getFirstInferenceStep()); assertTrue(typeInfererLet.getType().isPresent()); diff --git a/src/test/java/edu/kit/typicalc/model/TypeInfererTest.java b/src/test/java/edu/kit/typicalc/model/TypeInfererTest.java index f5889ca..1434932 100644 --- a/src/test/java/edu/kit/typicalc/model/TypeInfererTest.java +++ b/src/test/java/edu/kit/typicalc/model/TypeInfererTest.java @@ -68,9 +68,14 @@ class TypeInfererTest { TypeInferer typeInferer = new TypeInferer(let, givenTypeAssumptions); TypeVariableFactory refFac = new TypeVariableFactory(TypeVariableKind.TREE); + StepNumberFactory nrFactory = new StepNumberFactory(); refFac.nextTypeVariable(); - TypeInfererLet expectedTypeInfererLet = new TypeInfererLet(lxlyx, givenTypeAssumptions, refFac); - + nrFactory.nextStepIndex(); + TypeInfererLet expectedTypeInfererLet = new TypeInfererLet(lxlyx, givenTypeAssumptions, refFac, + nrFactory); + for (int i = 4; i <= 12; i++) { + nrFactory.nextStepIndex(); + } TypeAbstraction resultingAbs = new TypeAbstraction(new FunctionType(a3, new FunctionType(a5, a3)), new HashSet<>(Arrays.asList(a3, a5))); Map typeAssumptionsRight = new LinkedHashMap<>(givenTypeAssumptions); @@ -80,48 +85,49 @@ class TypeInfererTest { Conclusion varStepKLeftConc = new Conclusion(typeAssumptionsRight, k, a10); Constraint varStepKLeftConst = new Constraint(a10, varStepKLeftInst); InferenceStep varStepKLeft = new VarStepWithLet(resultingAbs, varStepKLeftInst, - varStepKLeftConc, varStepKLeftConst); + varStepKLeftConc, varStepKLeftConst, 6); Conclusion varStepAConc = new Conclusion(typeAssumptionsRight, a, a11); Constraint varStepAConst = new Constraint(a11, intT); - InferenceStep varStepA = new VarStepWithLet(intAbs, intT, varStepAConc, varStepAConst); + InferenceStep varStepA = new VarStepWithLet(intAbs, intT, varStepAConc, varStepAConst, 7); Conclusion appStepKAConc = new Conclusion(typeAssumptionsRight, ka, a8); Constraint appStepKAConst = new Constraint(a10, new FunctionType(a11, a8)); - InferenceStep appStepKA = new AppStepDefault(varStepKLeft, varStepA, appStepKAConc, appStepKAConst); + InferenceStep appStepKA = new AppStepDefault(varStepKLeft, varStepA, appStepKAConc, appStepKAConst, 5); Type varStepKRightInst = new FunctionType(a18, new FunctionType(a19, a18)); Conclusion varStepKRightConc = new Conclusion(typeAssumptionsRight, k, a16); Constraint varStepKRightConst = new Constraint(a16, varStepKRightInst); InferenceStep varStepKRight = new VarStepWithLet(resultingAbs, varStepKRightInst, - varStepKRightConc, varStepKRightConst); + varStepKRightConc, varStepKRightConst, 10); Conclusion varStepBConc = new Conclusion(typeAssumptionsRight, b, a17); Constraint varStepBConst = new Constraint(a17, boolT); - InferenceStep varStepB = new VarStepWithLet(boolAbs, boolT, varStepBConc, varStepBConst); + InferenceStep varStepB = new VarStepWithLet(boolAbs, boolT, varStepBConc, varStepBConst, 11); Conclusion appStepKBConc = new Conclusion(typeAssumptionsRight, kb, a14); Constraint appStepKBConst = new Constraint(a16, new FunctionType(a17, a14)); - InferenceStep appStepKB = new AppStepDefault(varStepKRight, varStepB, appStepKBConc, appStepKBConst); + InferenceStep appStepKB = new AppStepDefault(varStepKRight, varStepB, appStepKBConc, appStepKBConst, 9); Conclusion varStepCConc = new Conclusion(typeAssumptionsRight, c, a15); Constraint varStepCConst = new Constraint(a15, charT); - InferenceStep varStepC = new VarStepWithLet(charAbs, charT, varStepCConc, varStepCConst); + InferenceStep varStepC = new VarStepWithLet(charAbs, charT, varStepCConc, varStepCConst, 12); Conclusion appStepKBCConc = new Conclusion(typeAssumptionsRight, kbc, a9); Constraint appStepKBCConst = new Constraint(a14, new FunctionType(a15, a9)); - InferenceStep appStepKBC = new AppStepDefault(appStepKB, varStepC, appStepKBCConc, appStepKBCConst); + InferenceStep appStepKBC = new AppStepDefault(appStepKB, varStepC, appStepKBCConc, appStepKBCConst, 8); Conclusion appStepKAKBCConc = new Conclusion(typeAssumptionsRight, kakbc, a7); Constraint appStepKAKBCConst = new Constraint(a8, new FunctionType(a9, a7)); - InferenceStep appStepKAKBC = new AppStepDefault(appStepKA, appStepKBC, appStepKAKBCConc, appStepKAKBCConst); + InferenceStep appStepKAKBC = new AppStepDefault(appStepKA, appStepKBC, appStepKAKBCConc, appStepKAKBCConst, 4); Conclusion letConc = new Conclusion(givenTypeAssumptions, let, a1); Constraint letConst = new Constraint(a1, a7); InferenceStep expectedFirstInferenceStep - = new LetStepDefault(letConc, letConst, appStepKAKBC, expectedTypeInfererLet); + = new LetStepDefault(letConc, letConst, appStepKAKBC, expectedTypeInfererLet, 0); - assertEquals(expectedFirstInferenceStep, typeInferer.getFirstInferenceStep()); + InferenceStep actual = typeInferer.getFirstInferenceStep(); + assertEquals(expectedFirstInferenceStep, actual); List expectedConstraints = new ArrayList<>(); expectedConstraints.add(letConst); diff --git a/src/test/java/edu/kit/typicalc/model/step/AbsStepDefaultTest.java b/src/test/java/edu/kit/typicalc/model/step/AbsStepDefaultTest.java index c71688c..f37d9e8 100644 --- a/src/test/java/edu/kit/typicalc/model/step/AbsStepDefaultTest.java +++ b/src/test/java/edu/kit/typicalc/model/step/AbsStepDefaultTest.java @@ -33,25 +33,23 @@ class AbsStepDefaultTest { NamedType type1 = new NamedType("a"); NamedType type2 = new NamedType("b"); constraint = new Constraint(type1, type2); - premise = new ConstStepDefault(conclusion, constraint); + premise = new ConstStepDefault(conclusion, constraint, 0); } @Test void equalsTest() { - AbsStepDefault step1 = new AbsStepDefault(premise, conclusion, constraint); - AbsStepDefault step2 = new AbsStepDefault(premise, conclusion, constraint); - AbsStepDefault step3 = new AbsStepDefault(premise, conclusion, null); + AbsStepDefault step1 = new AbsStepDefault(premise, conclusion, constraint, 0); + AbsStepDefault step2 = new AbsStepDefault(premise, conclusion, constraint, 0); assertEquals(step1, step1); assertEquals(step1, step2); assertNotEquals(new EmptyStep(), step1); assertNotEquals(null, step1); - assertNotEquals(step1, step3); } @Test void hashCodeTest() { - AbsStepDefault step1 = new AbsStepDefault(premise, conclusion, constraint); - AbsStepDefault step2 = new AbsStepDefault(premise, conclusion, constraint); + AbsStepDefault step1 = new AbsStepDefault(premise, conclusion, constraint, 0); + AbsStepDefault step2 = new AbsStepDefault(premise, conclusion, constraint, 0); assertEquals(step1.hashCode(), step2.hashCode()); } @@ -59,7 +57,7 @@ class AbsStepDefaultTest { @Test void acceptTest() { TestStepVisitor testStepVisitor = new TestStepVisitor(); - AbsStepDefault step = new AbsStepDefault(premise, conclusion, constraint); + AbsStepDefault step = new AbsStepDefault(premise, conclusion, constraint, 0); step.accept(testStepVisitor); assertEquals("AbsDef", testStepVisitor.visited); } diff --git a/src/test/java/edu/kit/typicalc/model/step/AbsStepWithLetTest.java b/src/test/java/edu/kit/typicalc/model/step/AbsStepWithLetTest.java index fe5a463..b6d8dc0 100644 --- a/src/test/java/edu/kit/typicalc/model/step/AbsStepWithLetTest.java +++ b/src/test/java/edu/kit/typicalc/model/step/AbsStepWithLetTest.java @@ -33,26 +33,24 @@ class AbsStepWithLetTest { NamedType type1 = new NamedType("a"); NamedType type2 = new NamedType("b"); constraint = new Constraint(type1, type2); - premise = new ConstStepDefault(conclusion, constraint); + premise = new ConstStepDefault(conclusion, constraint, 0); } @Test void equalsTest() { - AbsStepWithLet step1 = new AbsStepWithLet(premise, conclusion, constraint); - AbsStepWithLet step2 = new AbsStepWithLet(premise, conclusion, constraint); - AbsStepWithLet step3 = new AbsStepWithLet(premise, conclusion, null); + AbsStepWithLet step1 = new AbsStepWithLet(premise, conclusion, constraint, 0); + AbsStepWithLet step2 = new AbsStepWithLet(premise, conclusion, constraint, 0); assertEquals(step1, step1); assertEquals(step1, step2); assertNotEquals(new EmptyStep(), step1); assertNotEquals(null, step1); - assertNotEquals(step1, step3); } @Test void hashCodeTest() { - AbsStepWithLet step1 = new AbsStepWithLet(premise, conclusion, constraint); - AbsStepWithLet step2 = new AbsStepWithLet(premise, conclusion, constraint); + AbsStepWithLet step1 = new AbsStepWithLet(premise, conclusion, constraint, 0); + AbsStepWithLet step2 = new AbsStepWithLet(premise, conclusion, constraint, 0); assertEquals(step1.hashCode(), step2.hashCode()); } @@ -60,7 +58,7 @@ class AbsStepWithLetTest { @Test void acceptTest() { TestStepVisitor testStepVisitor = new TestStepVisitor(); - AbsStepWithLet step = new AbsStepWithLet(premise, conclusion, constraint); + AbsStepWithLet step = new AbsStepWithLet(premise, conclusion, constraint, 0); step.accept(testStepVisitor); assertEquals("AbsLet", testStepVisitor.visited); } diff --git a/src/test/java/edu/kit/typicalc/model/step/AppStepDefaultTest.java b/src/test/java/edu/kit/typicalc/model/step/AppStepDefaultTest.java index 15bc06c..cb05ef3 100644 --- a/src/test/java/edu/kit/typicalc/model/step/AppStepDefaultTest.java +++ b/src/test/java/edu/kit/typicalc/model/step/AppStepDefaultTest.java @@ -35,32 +35,26 @@ class AppStepDefaultTest { NamedType type1 = new NamedType("a"); NamedType type2 = new NamedType("b"); constraint = new Constraint(type1, type2); - premise1 = new ConstStepDefault(conclusion, constraint); - premise2 = new ConstStepDefault(conclusion, constraint); + premise1 = new ConstStepDefault(conclusion, constraint, 0); + premise2 = new ConstStepDefault(conclusion, constraint, 0); } @Test void equalsTest() { - AppStepDefault step1 = new AppStepDefault(premise1, premise2, conclusion, constraint); - AppStepDefault step2 = new AppStepDefault(premise1, premise2, conclusion, constraint); - AppStepDefault step3 = new AppStepDefault(premise1, premise2, conclusion, null); - AppStepDefault step4 = new AppStepDefault(premise1, null, conclusion, constraint); - AppStepDefault step5 = new AppStepDefault(null, premise2, conclusion, constraint); + AppStepDefault step1 = new AppStepDefault(premise1, premise2, conclusion, constraint, 0); + AppStepDefault step2 = new AppStepDefault(premise1, premise2, conclusion, constraint, 0); assertEquals(step1, step1); assertEquals(step1, step2); assertNotEquals(new EmptyStep(), step1); assertNotEquals(null, step1); - assertNotEquals(step1, step3); - assertNotEquals(step1, step4); - assertNotEquals(step1, step5); } @Test void hashCodeTest() { - AppStepDefault step1 = new AppStepDefault(premise1, premise2, conclusion, constraint); - AppStepDefault step2 = new AppStepDefault(premise1, premise2, conclusion, constraint); + AppStepDefault step1 = new AppStepDefault(premise1, premise2, conclusion, constraint, 0); + AppStepDefault step2 = new AppStepDefault(premise1, premise2, conclusion, constraint, 0); assertEquals(step1.hashCode(), step2.hashCode()); } @@ -68,7 +62,7 @@ class AppStepDefaultTest { @Test void acceptTest() { TestStepVisitor testStepVisitor = new TestStepVisitor(); - AppStepDefault step = new AppStepDefault(premise1, premise2, conclusion, constraint); + AppStepDefault step = new AppStepDefault(premise1, premise2, conclusion, constraint, 0); step.accept(testStepVisitor); assertEquals("AppDef", testStepVisitor.visited); } diff --git a/src/test/java/edu/kit/typicalc/model/step/ConstStepDefaultTest.java b/src/test/java/edu/kit/typicalc/model/step/ConstStepDefaultTest.java index 921772e..16b4bb0 100644 --- a/src/test/java/edu/kit/typicalc/model/step/ConstStepDefaultTest.java +++ b/src/test/java/edu/kit/typicalc/model/step/ConstStepDefaultTest.java @@ -37,21 +37,19 @@ class ConstStepDefaultTest { @Test void equalsTest() { - ConstStepDefault step1 = new ConstStepDefault(conclusion, constraint); - ConstStepDefault step2 = new ConstStepDefault(conclusion, constraint); - ConstStepDefault step3 = new ConstStepDefault(conclusion, null); + ConstStepDefault step1 = new ConstStepDefault(conclusion, constraint, 0); + ConstStepDefault step2 = new ConstStepDefault(conclusion, constraint, 0); assertEquals(step1, step1); assertEquals(step1, step2); assertNotEquals(step1, new EmptyStep()); - assertNotEquals(step1, step3); } @Test void hashCodeTest() { - ConstStepDefault step1 = new ConstStepDefault(conclusion, constraint); - ConstStepDefault step2 = new ConstStepDefault(conclusion, constraint); + ConstStepDefault step1 = new ConstStepDefault(conclusion, constraint, 0); + ConstStepDefault step2 = new ConstStepDefault(conclusion, constraint, 0); assertEquals(step1.hashCode(), step2.hashCode()); } @@ -59,7 +57,7 @@ class ConstStepDefaultTest { @Test void acceptTest() { TestStepVisitor testStepVisitor = new TestStepVisitor(); - ConstStepDefault step = new ConstStepDefault(conclusion, constraint); + ConstStepDefault step = new ConstStepDefault(conclusion, constraint, 0); step.accept(testStepVisitor); assertEquals("ConstDef", testStepVisitor.visited); } diff --git a/src/test/java/edu/kit/typicalc/model/step/LetStepDefaultTest.java b/src/test/java/edu/kit/typicalc/model/step/LetStepDefaultTest.java index 4ecd41b..b0f8d2c 100644 --- a/src/test/java/edu/kit/typicalc/model/step/LetStepDefaultTest.java +++ b/src/test/java/edu/kit/typicalc/model/step/LetStepDefaultTest.java @@ -2,6 +2,7 @@ package edu.kit.typicalc.model.step; import edu.kit.typicalc.model.Conclusion; import edu.kit.typicalc.model.Constraint; +import edu.kit.typicalc.model.StepNumberFactory; import edu.kit.typicalc.model.term.IntegerTerm; import edu.kit.typicalc.model.term.VarTerm; import edu.kit.typicalc.model.type.NamedType; @@ -34,30 +35,23 @@ class LetStepDefaultTest { NamedType type1 = new NamedType("a"); NamedType type2 = new NamedType("b"); constraint = new Constraint(type1, type2); - premise = new ConstStepDefault(conclusion, constraint); - typeInferer = new TestTypeInfererLet(integerTerm, map, new TestTypeVariableFactory()); + premise = new ConstStepDefault(conclusion, constraint, 0); + typeInferer = new TestTypeInfererLet(integerTerm, map, new TestTypeVariableFactory(), new StepNumberFactory()); } @Test void equalsTest() { - LetStepDefault step1 = new LetStepDefault(conclusion, constraint, premise, typeInferer); - LetStepDefault step2 = new LetStepDefault(conclusion, constraint, premise, typeInferer); - LetStepDefault step3 = new LetStepDefault(conclusion, null, premise, typeInferer); - LetStepDefault step4 = new LetStepDefault(conclusion, constraint, null, typeInferer); - LetStepDefault step5 = new LetStepDefault(conclusion, constraint, premise, null); + LetStepDefault step1 = new LetStepDefault(conclusion, constraint, premise, typeInferer, 0); + LetStepDefault step2 = new LetStepDefault(conclusion, constraint, premise, typeInferer, 0); assertEquals(step1, step1); assertEquals(step1, step2); assertNotEquals(new EmptyStep(), step1); - assertNotEquals(null, step1); - assertNotEquals(step1, step3); - assertNotEquals(step1, step4); - assertNotEquals(step1, step5); } @Test void hashCodeTest() { - LetStepDefault step1 = new LetStepDefault(conclusion, constraint, premise, typeInferer); - LetStepDefault step2 = new LetStepDefault(conclusion, constraint, premise, typeInferer); + LetStepDefault step1 = new LetStepDefault(conclusion, constraint, premise, typeInferer, 0); + LetStepDefault step2 = new LetStepDefault(conclusion, constraint, premise, typeInferer, 0); assertEquals(step1.hashCode(), step2.hashCode()); } @@ -65,7 +59,7 @@ class LetStepDefaultTest { @Test void acceptTest() { TestStepVisitor testStepVisitor = new TestStepVisitor(); - LetStepDefault step = new LetStepDefault(conclusion, constraint, premise, typeInferer); + LetStepDefault step = new LetStepDefault(conclusion, constraint, premise, typeInferer, 0); step.accept(testStepVisitor); assertEquals("LetDef", testStepVisitor.visited); } diff --git a/src/test/java/edu/kit/typicalc/model/step/StepFactoryDefaultTest.java b/src/test/java/edu/kit/typicalc/model/step/StepFactoryDefaultTest.java index 6b865d0..7f7c29d 100644 --- a/src/test/java/edu/kit/typicalc/model/step/StepFactoryDefaultTest.java +++ b/src/test/java/edu/kit/typicalc/model/step/StepFactoryDefaultTest.java @@ -34,13 +34,13 @@ class StepFactoryDefaultTest { NamedType type1 = new NamedType("a"); NamedType type2 = new NamedType("b"); constraint = new Constraint(type1, type2); - premise = new ConstStepDefault(conclusion, constraint); + premise = new ConstStepDefault(conclusion, constraint, 0); } @Test void createAbsStepTest() { StepFactoryDefault factory = new StepFactoryDefault(); - AbsStepDefault step = factory.createAbsStep(premise, conclusion, constraint); + AbsStepDefault step = factory.createAbsStep(premise, conclusion, constraint, 0); assertEquals(premise, step.getPremise()); assertEquals(conclusion, step.getConclusion()); assertEquals(constraint, step.getConstraint()); @@ -49,7 +49,7 @@ class StepFactoryDefaultTest { @Test void createAppStepTest() { StepFactoryDefault factory = new StepFactoryDefault(); - AppStepDefault step = factory.createAppStep(premise, premise, conclusion, constraint); + AppStepDefault step = factory.createAppStep(premise, premise, conclusion, constraint, 0); assertEquals(premise, step.getPremise1()); assertEquals(premise, step.getPremise2()); assertEquals(conclusion, step.getConclusion()); @@ -59,7 +59,7 @@ class StepFactoryDefaultTest { @Test void createConstStepTest() { StepFactoryDefault factory = new StepFactoryDefault(); - ConstStepDefault step = factory.createConstStep(conclusion, constraint); + ConstStepDefault step = factory.createConstStep(conclusion, constraint, 0); assertEquals(conclusion, step.getConclusion()); assertEquals(constraint, step.getConstraint()); } @@ -67,23 +67,11 @@ class StepFactoryDefaultTest { @Test void createVarStepTest() { StepFactoryDefault factory = new StepFactoryDefault(); - VarStepDefault step = factory.createVarStep(typeAbstraction, namedType, conclusion, constraint); + VarStepDefault step = factory.createVarStep(typeAbstraction, namedType, conclusion, constraint, 0); assertEquals(typeAbstraction, step.getTypeAbsInPremise()); assertEquals(namedType, step.getInstantiatedTypeAbs()); assertEquals(conclusion, step.getConclusion()); assertEquals(constraint, step.getConstraint()); } - @Test - void createLetStepTest() { - StepFactoryDefault factory = new StepFactoryDefault(); - boolean thrown = false; - try { - LetStep step = factory.createLetStep(conclusion, constraint, premise, null); - } catch (UnsupportedOperationException e) { - thrown = true; - } - assertTrue(thrown); - } - } \ No newline at end of file diff --git a/src/test/java/edu/kit/typicalc/model/step/StepFactoryWithLetTest.java b/src/test/java/edu/kit/typicalc/model/step/StepFactoryWithLetTest.java index 6e0dfee..ddbfecd 100644 --- a/src/test/java/edu/kit/typicalc/model/step/StepFactoryWithLetTest.java +++ b/src/test/java/edu/kit/typicalc/model/step/StepFactoryWithLetTest.java @@ -35,13 +35,13 @@ class StepFactoryWithLetTest { NamedType type1 = new NamedType("a"); NamedType type2 = new NamedType("b"); constraint = new Constraint(type1, type2); - premise = new ConstStepDefault(conclusion, constraint); + premise = new ConstStepDefault(conclusion, constraint, 0); } @Test void createAbsStepTest() { StepFactoryWithLet factory = new StepFactoryWithLet(); - AbsStepWithLet step = factory.createAbsStep(premise, conclusion, constraint); + AbsStepWithLet step = factory.createAbsStep(premise, conclusion, constraint, 0); assertEquals(premise, step.getPremise()); assertEquals(conclusion, step.getConclusion()); assertEquals(constraint, step.getConstraint()); @@ -50,7 +50,7 @@ class StepFactoryWithLetTest { @Test void createAppStepTest() { StepFactoryWithLet factory = new StepFactoryWithLet(); - AppStepDefault step = factory.createAppStep(premise, premise, conclusion, constraint); + AppStepDefault step = factory.createAppStep(premise, premise, conclusion, constraint, 0); assertEquals(premise, step.getPremise1()); assertEquals(premise, step.getPremise2()); assertEquals(conclusion, step.getConclusion()); @@ -60,7 +60,7 @@ class StepFactoryWithLetTest { @Test void createConstStepTest() { StepFactoryWithLet factory = new StepFactoryWithLet(); - ConstStepDefault step = factory.createConstStep(conclusion, constraint); + ConstStepDefault step = factory.createConstStep(conclusion, constraint, 0); assertEquals(conclusion, step.getConclusion()); assertEquals(constraint, step.getConstraint()); } @@ -68,20 +68,10 @@ class StepFactoryWithLetTest { @Test void createVarStepTest() { StepFactoryWithLet factory = new StepFactoryWithLet(); - VarStepWithLet step = factory.createVarStep(typeAbstraction, namedType, conclusion, constraint); + VarStepWithLet step = factory.createVarStep(typeAbstraction, namedType, conclusion, constraint, 0); assertEquals(typeAbstraction, step.getTypeAbsInPremise()); assertEquals(namedType, step.getInstantiatedTypeAbs()); assertEquals(conclusion, step.getConclusion()); assertEquals(constraint, step.getConstraint()); } - - @Test - void createLetStepTest() { - StepFactoryWithLet factory = new StepFactoryWithLet(); - LetStep step = factory.createLetStep(conclusion, constraint, premise, null); - assertEquals(premise, step.getPremise()); - assertNull(step.getTypeInferer()); - assertEquals(conclusion, step.getConclusion()); - assertEquals(constraint, step.getConstraint()); - } } \ No newline at end of file diff --git a/src/test/java/edu/kit/typicalc/model/step/TestTypeInfererLet.java b/src/test/java/edu/kit/typicalc/model/step/TestTypeInfererLet.java index 3f643c8..b62c839 100644 --- a/src/test/java/edu/kit/typicalc/model/step/TestTypeInfererLet.java +++ b/src/test/java/edu/kit/typicalc/model/step/TestTypeInfererLet.java @@ -1,5 +1,6 @@ package edu.kit.typicalc.model.step; +import edu.kit.typicalc.model.StepNumberFactory; import edu.kit.typicalc.model.TypeInfererLet; import edu.kit.typicalc.model.TypeVariableFactory; import edu.kit.typicalc.model.term.LambdaTerm; @@ -9,7 +10,8 @@ import edu.kit.typicalc.model.type.TypeAbstraction; import java.util.Map; public class TestTypeInfererLet extends TypeInfererLet { - public TestTypeInfererLet(LambdaTerm term, Map map, TypeVariableFactory factory) { - super(term, map, factory); + public TestTypeInfererLet(LambdaTerm term, Map map, TypeVariableFactory factory, + StepNumberFactory factory2) { + super(term, map, factory, factory2); } } diff --git a/src/test/java/edu/kit/typicalc/model/step/VarStepDefaultTest.java b/src/test/java/edu/kit/typicalc/model/step/VarStepDefaultTest.java index c172cc3..f5eadae 100644 --- a/src/test/java/edu/kit/typicalc/model/step/VarStepDefaultTest.java +++ b/src/test/java/edu/kit/typicalc/model/step/VarStepDefaultTest.java @@ -16,7 +16,6 @@ import static org.junit.jupiter.api.Assertions.assertEquals; import static org.junit.jupiter.api.Assertions.assertNotEquals; class VarStepDefaultTest { - static InferenceStep premise = null; static Conclusion conclusion = null; static Constraint constraint = null; static NamedType namedType = null; @@ -38,26 +37,20 @@ class VarStepDefaultTest { @Test void equalsTest() { - VarStepDefault step1 = new VarStepDefault(typeAbstraction, namedType, conclusion, constraint); - VarStepDefault step2 = new VarStepDefault(typeAbstraction, namedType, conclusion, constraint); - VarStepDefault step3 = new VarStepDefault(typeAbstraction, namedType, conclusion, null); - VarStepDefault step4 = new VarStepDefault(null, namedType, conclusion, constraint); - VarStepDefault step5 = new VarStepDefault(typeAbstraction, null, conclusion, constraint); + VarStepDefault step1 = new VarStepDefault(typeAbstraction, namedType, conclusion, constraint, 0); + VarStepDefault step2 = new VarStepDefault(typeAbstraction, namedType, conclusion, constraint, 0); assertEquals(step1, step1); assertEquals(step1, step2); assertNotEquals(new EmptyStep(), step1); assertNotEquals(null, step1); - assertNotEquals(step1, step3); - assertNotEquals(step1, step4); - assertNotEquals(step1, step5); } @Test void hashCodeTest() { - VarStepDefault step1 = new VarStepDefault(typeAbstraction, namedType, conclusion, constraint); - VarStepDefault step2 = new VarStepDefault(typeAbstraction, namedType, conclusion, constraint); + VarStepDefault step1 = new VarStepDefault(typeAbstraction, namedType, conclusion, constraint, 0); + VarStepDefault step2 = new VarStepDefault(typeAbstraction, namedType, conclusion, constraint, 0); assertEquals(step1.hashCode(), step2.hashCode()); } @@ -65,7 +58,7 @@ class VarStepDefaultTest { @Test void acceptTest() { TestStepVisitor testStepVisitor = new TestStepVisitor(); - VarStepDefault step = new VarStepDefault(typeAbstraction, namedType, conclusion, constraint); + VarStepDefault step = new VarStepDefault(typeAbstraction, namedType, conclusion, constraint, 0); step.accept(testStepVisitor); assertEquals("VarDef", testStepVisitor.visited); } diff --git a/src/test/java/edu/kit/typicalc/model/step/VarStepWithLetTest.java b/src/test/java/edu/kit/typicalc/model/step/VarStepWithLetTest.java index 7ed8b6d..1ea60f8 100644 --- a/src/test/java/edu/kit/typicalc/model/step/VarStepWithLetTest.java +++ b/src/test/java/edu/kit/typicalc/model/step/VarStepWithLetTest.java @@ -16,7 +16,6 @@ import static org.junit.jupiter.api.Assertions.assertEquals; import static org.junit.jupiter.api.Assertions.assertNotEquals; class VarStepWithLetTest { - static InferenceStep premise = null; static Conclusion conclusion = null; static Constraint constraint = null; static NamedType namedType = null; @@ -34,35 +33,11 @@ class VarStepWithLetTest { NamedType type2 = new NamedType("b"); constraint = new Constraint(type1, type2); } - @Test - void equalsTest() { - VarStepWithLet step1 = new VarStepWithLet(typeAbstraction, namedType, conclusion, constraint); - VarStepWithLet step2 = new VarStepWithLet(typeAbstraction, namedType, conclusion, constraint); - VarStepWithLet step3 = new VarStepWithLet(typeAbstraction, namedType, conclusion, null); - VarStepWithLet step4 = new VarStepWithLet(null, namedType, conclusion, constraint); - VarStepWithLet step5 = new VarStepWithLet(typeAbstraction, null, conclusion, constraint); - - assertEquals(step1, step1); - assertEquals(step1, step2); - assertNotEquals(new EmptyStep(), step1); - assertNotEquals(null, step1); - assertNotEquals(step1, step3); - assertNotEquals(step1, step4); - assertNotEquals(step1, step5); - - } - @Test - void hashCodeTest() { - VarStepWithLet step1 = new VarStepWithLet(typeAbstraction, namedType, conclusion, constraint); - VarStepWithLet step2 = new VarStepWithLet(typeAbstraction, namedType, conclusion, constraint); - - assertEquals(step1.hashCode(), step2.hashCode()); - } @Test void acceptTest() { TestStepVisitor testStepVisitor = new TestStepVisitor(); - VarStepWithLet step = new VarStepWithLet(typeAbstraction, namedType, conclusion, constraint); + VarStepWithLet step = new VarStepWithLet(typeAbstraction, namedType, conclusion, constraint, 0); step.accept(testStepVisitor); assertEquals("VarLet", testStepVisitor.visited); }