createLetStep hinzugefügt

This commit is contained in:
uogau 2021-02-01 14:14:18 +01:00
parent 64312cd172
commit 8929a59e82
3 changed files with 44 additions and 2 deletions

View File

@ -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.TypeInfererLet;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAbstraction;
@ -46,5 +47,14 @@ public interface StepFactory {
*/
VarStep createVarStep(TypeAbstraction typeAbstraction, Type instantiatedTypeAbs,
Conclusion conclusion, Constraint constraint);
//TODO LetStep
/**
* Creates a LetStep.
* @param conclusion the conclusion of this step
* @param constraint the constraint that can be derived from this step
* @param premise the premise that doesn't need its own type inference
* @param typeInferer the typeInferer for the premise that needs its own type inference
* @return the created AppStep
*/
LetStep createLetStep(Conclusion conclusion, Constraint constraint,
InferenceStep premise, TypeInfererLet typeInferer);
}

View File

@ -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.TypeInfererLet;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAbstraction;
@ -60,4 +61,21 @@ public class StepFactoryDefault implements StepFactory {
Conclusion conclusion, Constraint constraint) {
return new VarStepDefault(typeAbstraction, instantiatedTypeAbs, conclusion, constraint);
}
/**
* Throws an UnsupportedOperationException.
* This method should never be called, as a StepFactoryDefault should only be used
* for lambda terms without any let polymorphism and therefore should never have
* to create a step where the let rule is applied.
* @param conclusion the conclusion of this step
* @param constraint the constraint that can be derived from this step
* @param premise the premise that doesn't need its own type inference
* @param typeInferer the typeInferer for the premise that needs its own type inference
* @return nothing
*/
@Override
public LetStep createLetStep(Conclusion conclusion, Constraint constraint,
InferenceStep premise, TypeInfererLet typeInferer) {
throw new UnsupportedOperationException("Not possible to create LetStep when no let is present in the term");
}
}

View File

@ -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.TypeInfererLet;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAbstraction;
@ -49,7 +50,6 @@ public class StepFactoryWithLet implements StepFactory {
/**
* Creates a VarStepWithLet.
*
* @param typeAbstraction the type abstraction of this step
* @param instantiatedTypeAbs an instantiation of the type abstraction used in this step
* @param conclusion the conclusion of this step
@ -61,4 +61,18 @@ public class StepFactoryWithLet implements StepFactory {
Conclusion conclusion, Constraint constraint) {
return new VarStepWithLet(typeAbstraction, instantiatedTypeAbs, conclusion, constraint);
}
/**
* Creates a LetStepDefault.
* @param conclusion the conclusion of this step
* @param constraint the constraint that can be derived from this step
* @param premise the premise that doesn't need its own type inference
* @param typeInferer the typeInferer for the premise that needs its own type inference
* @return the created LetStepDefault
*/
@Override
public LetStepDefault createLetStep(Conclusion conclusion, Constraint constraint,
InferenceStep premise, TypeInfererLet typeInferer) {
return new LetStepDefault(conclusion, constraint, premise, typeInferer);
}
}