arnekeller/Typicalc
1
0
Fork 0
mirror of https://gitlab.kit.edu/uskyk/typicalc.git synced 2024-11-10 03:10:44 +00:00
Code Issues Packages Projects Releases Wiki Activity

Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc

Browse Source
This commit is contained in:
ucrhh 2021-02-01 14:42:50 +01:00
commit 07f16ed2d0
3 changed files with 44 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
src/main/java/edu/kit/typicalc/model/step/StepFactory.java
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);
}

18
src/main/java/edu/kit/typicalc/model/step/StepFactoryDefault.java
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");
}
}

16
src/main/java/edu/kit/typicalc/model/step/StepFactoryWithLet.java
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);
}
}