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

Generate steps withLet in every sub-inference of let terms

Browse Source
This commit is contained in:
Johanna Stuber 2021-02-04 19:31:06 +01:00
parent 5c9f916a6c
commit ee18a3cba1
3 changed files with 7 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
src/main/java/edu/kit/typicalc/model/Tree.java
View File

@ -41,7 +41,7 @@ public class Tree implements TermVisitorTree {
* @param lambdaTerm the lambda term to generate the tree for
*/
protected Tree(Map<VarTerm, TypeAbstraction> typeAssumptions, LambdaTerm lambdaTerm) {
this(typeAssumptions, lambdaTerm, new TypeVariableFactory(TypeVariableKind.TREE));
this(typeAssumptions, lambdaTerm, new TypeVariableFactory(TypeVariableKind.TREE), false);
}
/**
@ -54,13 +54,14 @@ public class Tree implements TermVisitorTree {
* @param typeAssumptions the type assumptions to consider when generating the tree
* @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
*/
protected Tree(Map<VarTerm, TypeAbstraction> typeAssumptions, LambdaTerm lambdaTerm,
TypeVariableFactory typeVariableFactory) {
TypeVariableFactory typeVariableFactory, boolean partOfLetTerm) {
this.typeVarFactory = typeVariableFactory;
this.constraints = new ArrayList<>();
this.stepFactory = lambdaTerm.hasLet() ? new StepFactoryWithLet() : new StepFactoryDefault();
this.stepFactory = lambdaTerm.hasLet() || partOfLetTerm ? new StepFactoryWithLet() : new StepFactoryDefault();
this.firstTypeVariable = typeVarFactory.nextTypeVariable();
this.firstInferenceStep = lambdaTerm.accept(this, typeAssumptions, firstTypeVariable);

4
src/main/java/edu/kit/typicalc/model/TypeInfererLet.java
View File

@ -27,12 +27,12 @@ public class TypeInfererLet implements TypeInfererInterface {
*
* @param lambdaTerm the lambda term to generate the tree for
* @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 consistecy
* @param typeVarFactory the type variable factory that should be used in this inference to guarantee consistency
* with the outer inference
*/
protected TypeInfererLet(LambdaTerm lambdaTerm, Map<VarTerm, TypeAbstraction> typeAssumptions,
TypeVariableFactory typeVarFactory) {
tree = new Tree(typeAssumptions, lambdaTerm, typeVarFactory);
tree = new Tree(typeAssumptions, lambdaTerm, typeVarFactory, true);
// cancel algorithm if a sub-inference failed
if (tree.hasFailedSubInference()) {

2
src/test/java/edu/kit/typicalc/model/TreeTest.java
View File

@ -40,7 +40,7 @@ class TreeTest {
factory.nextTypeVariable();
factoryRef.nextTypeVariable();
}
Tree tree = new Tree(TYPE_ASSUMPTIONS, VAR, factory);
Tree tree = new Tree(TYPE_ASSUMPTIONS, VAR, factory, false);
assertEquals(tree.getFirstTypeVariable(), factoryRef.nextTypeVariable());
}