From 8a7497fadafdf29cedab480bfae33adf3d3732ba Mon Sep 17 00:00:00 2001 From: Johanna Stuber Date: Thu, 28 Jan 2021 00:37:48 +0100 Subject: [PATCH] TypeAssumption entfernen, Konstruktoren und getter von Tree --- .../java/edu/kit/typicalc/model/Tree.java | 42 ++++++++++++------- .../edu/kit/typicalc/model/TypeInferer.java | 1 + .../kit/typicalc/model/term/LambdaTerm.java | 10 +++++ .../typicalc/model/term/TermVisitorTree.java | 14 +++---- .../typicalc/model/type/TypeAssumption.java | 4 -- .../kit/typicalc/model/type/TypeVariable.java | 2 +- 6 files changed, 47 insertions(+), 26 deletions(-) delete mode 100644 src/main/java/edu/kit/typicalc/model/type/TypeAssumption.java diff --git a/src/main/java/edu/kit/typicalc/model/Tree.java b/src/main/java/edu/kit/typicalc/model/Tree.java index 8142133..e2cd868 100644 --- a/src/main/java/edu/kit/typicalc/model/Tree.java +++ b/src/main/java/edu/kit/typicalc/model/Tree.java @@ -1,6 +1,9 @@ package edu.kit.typicalc.model; import edu.kit.typicalc.model.step.InferenceStep; +import edu.kit.typicalc.model.step.StepFactory; +import edu.kit.typicalc.model.step.StepFactoryDefault; +import edu.kit.typicalc.model.step.StepFactoryWithLet; import edu.kit.typicalc.model.term.AbsTerm; import edu.kit.typicalc.model.term.AppTerm; import edu.kit.typicalc.model.term.ConstTerm; @@ -10,9 +13,9 @@ import edu.kit.typicalc.model.term.TermVisitorTree; import edu.kit.typicalc.model.term.VarTerm; import edu.kit.typicalc.model.type.Type; import edu.kit.typicalc.model.type.TypeAbstraction; -import edu.kit.typicalc.model.type.TypeAssumption; import edu.kit.typicalc.model.type.TypeVariable; +import java.util.ArrayList; import java.util.List; import java.util.Map; @@ -24,6 +27,13 @@ import java.util.Map; */ public class Tree implements TermVisitorTree { + private final TypeVariableFactory typeVarFactory; + private final StepFactory stepFactory; + + private final TypeVariable firstTypeVariable; + private final InferenceStep firstInferenceStep; + private final List constraints; + /** * Initializes a new Tree representing the proof tree for the type inference of the given * lambda term considering the given type assumptions. The inference step structure @@ -33,7 +43,7 @@ public class Tree implements TermVisitorTree { * @param lambdaTerm the lambda term to generate the tree for */ protected Tree(Map typeAssumptions, LambdaTerm lambdaTerm) { - // TODO + this(typeAssumptions, lambdaTerm, new TypeVariableFactory()); } /** @@ -49,7 +59,14 @@ public class Tree implements TermVisitorTree { */ protected Tree(Map typeAssumptions, LambdaTerm lambdaTerm, TypeVariableFactory typeVariableFactory) { - // TODO + // TODO: null checks + this.typeVarFactory = typeVariableFactory; + this.constraints = new ArrayList<>(); + + this.stepFactory = lambdaTerm.hasLet() ? new StepFactoryWithLet() : new StepFactoryDefault(); + + this.firstTypeVariable = typeVarFactory.nextTypeVariable(); + this.firstInferenceStep = lambdaTerm.accept(this, typeAssumptions, firstTypeVariable); } /** @@ -60,8 +77,7 @@ public class Tree implements TermVisitorTree { * @return the first inference step of the tree */ protected InferenceStep getFirstInferenceStep() { - return null; - // TODO; + return firstInferenceStep; } /** @@ -70,8 +86,7 @@ public class Tree implements TermVisitorTree { * @return the first type variable */ protected TypeVariable getFirstTypeVariable() { - return null; - // TODO; + return firstTypeVariable; } /** @@ -81,32 +96,31 @@ public class Tree implements TermVisitorTree { * @return the constraint list of the tree */ protected List getConstraints() { - return null; - // TODO + return constraints; } @Override - public InferenceStep visit(AppTerm appTerm, List typeAssumptions, Type conclusionType) { + public InferenceStep visit(AppTerm appTerm, Map typeAssumptions, Type conclusionType) { return null; // TODO } @Override - public InferenceStep visit(AbsTerm absTerm, List typeAssumptions, Type conclusionType) { + public InferenceStep visit(AbsTerm absTerm, Map typeAssumptions, Type conclusionType) { return null; // TODO } @Override - public InferenceStep visit(LetTerm letTerm, List typeAssumptions, Type conclusionType) { + public InferenceStep visit(LetTerm letTerm, Map typeAssumptions, Type conclusionType) { return null; // TODO } @Override - public InferenceStep visit(ConstTerm constTerm, List typeAssumptions, Type conclusionType) { + public InferenceStep visit(ConstTerm constTerm, Map typeAssumptions, Type conclusionType) { return null; // TODO } @Override - public InferenceStep visit(VarTerm varTerm, List typeAssumptions, Type conclusionType) { + public InferenceStep visit(VarTerm varTerm, Map typeAssumptions, Type conclusionType) { return null; // TODO } } diff --git a/src/main/java/edu/kit/typicalc/model/TypeInferer.java b/src/main/java/edu/kit/typicalc/model/TypeInferer.java index 4402862..6f111e5 100644 --- a/src/main/java/edu/kit/typicalc/model/TypeInferer.java +++ b/src/main/java/edu/kit/typicalc/model/TypeInferer.java @@ -32,6 +32,7 @@ public class TypeInferer implements TypeInfererInterface { * @param typeAssumptions the type assumptions to consider when generating the tree */ protected TypeInferer(LambdaTerm lambdaTerm, Map typeAssumptions) { + // TODO: null checks tree = new Tree(typeAssumptions, lambdaTerm); // TODO: Abbrechen bei fehlgeschlagener let-Teilinferenz, evtl. getUnificationSteps() anpassen diff --git a/src/main/java/edu/kit/typicalc/model/term/LambdaTerm.java b/src/main/java/edu/kit/typicalc/model/term/LambdaTerm.java index dde58fe..2ef8c5c 100644 --- a/src/main/java/edu/kit/typicalc/model/term/LambdaTerm.java +++ b/src/main/java/edu/kit/typicalc/model/term/LambdaTerm.java @@ -1,5 +1,11 @@ package edu.kit.typicalc.model.term; +import edu.kit.typicalc.model.step.InferenceStep; +import edu.kit.typicalc.model.type.Type; +import edu.kit.typicalc.model.type.TypeAbstraction; + +import java.util.Map; + public abstract class LambdaTerm { /** * @return whether the lambda term contains a let expression @@ -11,4 +17,8 @@ public abstract class LambdaTerm { * @param termVisitor a visitor */ public abstract void accept(TermVisitor termVisitor); + + public abstract InferenceStep accept(TermVisitorTree termVisitorTree, + Map assumptions, Type type); + } diff --git a/src/main/java/edu/kit/typicalc/model/term/TermVisitorTree.java b/src/main/java/edu/kit/typicalc/model/term/TermVisitorTree.java index 7a2bc89..1c743de 100644 --- a/src/main/java/edu/kit/typicalc/model/term/TermVisitorTree.java +++ b/src/main/java/edu/kit/typicalc/model/term/TermVisitorTree.java @@ -2,9 +2,9 @@ package edu.kit.typicalc.model.term; import edu.kit.typicalc.model.step.InferenceStep; import edu.kit.typicalc.model.type.Type; -import edu.kit.typicalc.model.type.TypeAssumption; +import edu.kit.typicalc.model.type.TypeAbstraction; -import java.util.List; +import java.util.Map; public interface TermVisitorTree { /** @@ -19,7 +19,7 @@ public interface TermVisitorTree { * of the returned inference step will be assigned * @return an {@link edu.kit.typicalc.model.step.AppStep} */ - InferenceStep visit(AppTerm appTerm, List typeAssumptions, Type conclusionType); + InferenceStep visit(AppTerm appTerm, Map typeAssumptions, Type conclusionType); /** * Returns an {@link edu.kit.typicalc.model.step.AbsStep} suiting the given abstraction (lambda term) @@ -33,7 +33,7 @@ public interface TermVisitorTree { * of the returned inference step will be assigned * @return an {@link edu.kit.typicalc.model.step.AbsStep} */ - InferenceStep visit(AbsTerm absTerm, List typeAssumptions, Type conclusionType); + InferenceStep visit(AbsTerm absTerm, Map typeAssumptions, Type conclusionType); /** * Returns an {@link edu.kit.typicalc.model.step.LetStep} suiting the given let expression (lambda term) @@ -47,7 +47,7 @@ public interface TermVisitorTree { * of the returned inference step will be assigned * @return an {@link edu.kit.typicalc.model.step.LetStep} */ - InferenceStep visit(LetTerm letTerm, List typeAssumptions, Type conclusionType); + InferenceStep visit(LetTerm letTerm, Map typeAssumptions, Type conclusionType); /** * Returns an {@link edu.kit.typicalc.model.step.ConstStep} suiting the given constant @@ -61,7 +61,7 @@ public interface TermVisitorTree { * of the returned inference step will be assigned * @return an {@link edu.kit.typicalc.model.step.ConstStep} */ - InferenceStep visit(ConstTerm constTerm, List typeAssumptions, Type conclusionType); + InferenceStep visit(ConstTerm constTerm, Map typeAssumptions, Type conclusionType); /** * Returns an {@link edu.kit.typicalc.model.step.VarStep} suiting the given variable (lambda term) @@ -75,5 +75,5 @@ public interface TermVisitorTree { * of the returned inference step will be assigned * @return an {@link edu.kit.typicalc.model.step.VarStep} */ - InferenceStep visit(VarTerm varTerm, List typeAssumptions, Type conclusionType); + InferenceStep visit(VarTerm varTerm, Map typeAssumptions, Type conclusionType); } diff --git a/src/main/java/edu/kit/typicalc/model/type/TypeAssumption.java b/src/main/java/edu/kit/typicalc/model/type/TypeAssumption.java deleted file mode 100644 index ea5bdfd..0000000 --- a/src/main/java/edu/kit/typicalc/model/type/TypeAssumption.java +++ /dev/null @@ -1,4 +0,0 @@ -package edu.kit.typicalc.model.type; - -public class TypeAssumption { -} diff --git a/src/main/java/edu/kit/typicalc/model/type/TypeVariable.java b/src/main/java/edu/kit/typicalc/model/type/TypeVariable.java index 9e92658..2e88734 100644 --- a/src/main/java/edu/kit/typicalc/model/type/TypeVariable.java +++ b/src/main/java/edu/kit/typicalc/model/type/TypeVariable.java @@ -1,6 +1,6 @@ package edu.kit.typicalc.model.type; -public class TypeVariable { +public class TypeVariable extends Type { public TypeVariable(int index) { }