Großteil der Modelpaket-Klassen samt Javadoc hizugefügt

src/main/java/edu/kit/typicalc/model/Conclusion.java

@@ -0,0 +1,43 @@
+package edu.kit.typicalc.model;
+
+/**
+ * Models the conclusion of an inference rule and consists of a list of type assumptions, a lambda term and a type.
+ * This class is used in inference steps to represent the conclusion of that specific application of the inference rule.
+ */
+public class Conclusion {
+
+    /**
+     * Initializes a new Conclusion with the given type assumptions, lambda term and type.
+     *
+     * @param typeAssumptions the type assumptions used in the conclusion
+     * @param lambdaTerm the lambda term in the conclusion
+     * @param type the type assigned to the lambda term in the conclusion
+     */
+    protected Conclusion(Map<VarTerm, TypeAbstraction> typeAssumptions, LambdaTerm lambdaTerm, Type type) {
+        // TODO
+    }
+
+    /**
+     * @return the type assumptions used in the conclusion
+     */
+    public Map<VarTerm, TypeAbstraction> getTypeAssumptions() {
+        return null;
+        // TODO
+    }
+
+    /**
+     * @return the lambda term in the conclusion
+     */
+    public LambdaTerm getLambdaTerm() {
+        return null;
+        // TODO
+    }
+
+    /**
+     * @return the type assigned to the lambda term in the conclusion
+     */
+    public Type getType() {
+        return null;
+        // TODO
+    }
+}

src/main/java/edu/kit/typicalc/model/Constraint.java

@@ -0,0 +1,33 @@
+package edu.kit.typicalc.model;
+
+/**
+ * Constrains two types to be equal.
+ */
+public class Constraint {
+    /**
+     * Creates a new constraint using the two types.
+     *
+     * @param a first type
+     * @param b second type
+     */
+    public Constraint(Type a, Type b) {
+        // TODO
+    }
+
+    /**
+     * @return the first type
+     */
+    public Type getFirstType() {
+        return null;
+        // TODO
+    }
+
+    /**
+     * @return the second type
+     */
+    public Type getSecondType() {
+        return null;
+        // TODO
+    }
+
+}

src/main/java/edu/kit/typicalc/model/Substitution.java

@@ -0,0 +1,33 @@
+package edu.kit.typicalc.model;
+
+/**
+ * A substitution specifies that some type should be replaced by a different type.
+ */
+public class Substitution {
+    /**
+     * Creates a new substitution using a type variable a and a type b. When the substitution is applied to a type,
+     * all occurring instances of a should be substituted with b.
+     *
+     * @param a variable to be replaced
+     * @param b type to insert
+     */
+    public Substitution(TypeVariable a, Type b) {
+        // TODO
+    }
+
+    /**
+     * @return the type variable
+     */
+    public TypeVariable getVariable() {
+        return null;
+        // TODO
+    }
+
+    /**
+     * @return the replacement type
+     */
+    Type getType() {
+        return null;
+        // TODO
+    }
+}

src/main/java/edu/kit/typicalc/model/Tree.java

@@ -0,0 +1,63 @@
+package edu.kit.typicalc.model;
+
+import java.util.List;
+
+/**
+ * Models the proof tree formed when the type of a lambda term is inferred.
+ * A Tree consists of a tree-like structure of inference steps and a list of constraints that
+ * are part of these steps. It is guaranteed that these members can be accessed right after
+ * instantiation (no additional initialization is required).
+ */
+public class Tree implements TermVisitor {
+
+    /**
+     * 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
+     * and constraint list are generated here.
+     *
+     * @param typeAssumptions  the type assumptions to consider when generating the tree
+     * @param lambdaTerm the lambda term to generate the tree for
+     */
+    protected Tree(Map<VarTerm, TypeAbstraction> typeAssumptions, LambdaTerm lambdaTerm) {
+        // TODO
+    }
+
+    /**
+     * Initializes a new Tree representing the proof tree for the type inference of the given
+     * lambda term considering the given type assumptions. This constructor is supposed
+     * to be used if the lambda term is part of a let term. To generate unique type
+     * variable names, a type variable factory is provided as a parameter. The inference
+     * step structure and constraint list are generated here.
+     *
+     * @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
+     */
+    protected Tree(Map<VarTerm, TypeAbstraction> typeAssumptions, LambdaTerm lambdaTerm,
+                   TypeVariableFactory typeVariableFactory) {
+        // TODO
+    }
+
+    /**
+     * Returns the first (on the undermost level) inference step of the proof tree, containing
+     * the original lambda term that is being type-inferred in this tree and presenting an
+     * entry point for the tree-like inference step structure.
+     *
+     * @return the first inference step of the tree
+     */
+    protected InferenceStep getFirstInferenceStep() {
+        return null;
+        // TODO;
+    }
+
+    /**
+     * Returns the list of constraints that formed while generating the inference step tree
+     * structure, needed for the subsequent unification.
+     *
+     * @return the constraint list of the tree
+     */
+    protected List<Constraint> getConstraints() {
+        return null;
+        // TODO
+    }
+}

src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java

@@ -0,0 +1,46 @@
+package edu.kit.typicalc.model;
+
+import java.util.List;
+
+/**
+ * Models the final result of the type inference with the most general unifier (mgu) and
+ * the final inferred type of the lambda term. It is guaranteed that these members can be
+ * accessed right after instantiation (no additional initialization is required).
+ */
+public class TypeInferenceResult {
+    /**
+     * Initializes a new TypeInferenceResult for the given substitutions (resulting from
+     * the unification) and the given type variable belonging to the original lambda term
+     * of the type inference. The final type is obtained by applying the most general unifier
+     * to this given type variable. The mgu and the final type are generated here.
+     *
+     * @param substitutions the substitutions to generate the mgu and the final type
+     * @param typeVar the type variable belonging to the original lambda term
+     */
+    protected TypeInferenceResult(List<Substitution> substitutions, TypeVariable typeVar) {
+        // TODO
+    }
+
+    /**
+     * Returns the most general unifier (mgu), as a list of substitutions. If no valid type
+     * (correlating with no valid mgu) can be found for the lambda term to type-infer, null is returned.
+     *
+     * @return the most general unifier, null if there is no valid mgu
+     */
+    protected List<Substitution> getMGU() {
+        return null;
+        // TODO
+    }
+
+    /**
+     * Returns the type that is the result of the type inference. It is obtained by applying
+     * the mgu to the type variable the type inference result was given in its construstor.
+     * If no valid type can be found for the lambda term to type-infer, null is returned.
+     *
+     * @return the final type of the lambda term, null if there is no valid type
+     */
+    protected Type getType() {
+        return null;
+        // TODO
+    }
+}

src/main/java/edu/kit/typicalc/model/TypeInferer.java

@@ -0,0 +1,51 @@
+package edu.kit.typicalc.model;
+
+import java.util.List;
+
+/**
+ * The type inferer is responsible for the whole type inference of a given lambda term, taking
+ * into account the given type assumptions. It implements the TypeInfererInterface and
+ * therefore can hand out an inference step structure, a list of unification steps, the most
+ * general unifier and the final type suiting the type inference of the given lambda term. It is
+ * guaranteed that this information can be accessed right after instantiation (no additional
+ * initialization is required).
+ */
+public class TypeInferer implements TypeInfererInterface {
+
+    /**
+     * Initializes a new TypeInferer for the given type assumptions and lambda term.
+     * The inference step structure, unification steps, the most general unifier and the
+     * final type are generated and calculated here.
+     *
+     * @param lambdaTerm the lambda term to generate the tree for
+     * @param typeAssumptions the type assumptions to consider when generating the tree
+     */
+    protected TypeInferer(LambdaTerm lambdaTerm, Map<VarTerm, TypeAbstraction> typeAssumptions) {
+        // TODO
+    }
+
+
+    @Override
+    public InferenceStep getFirstInferenceStep() {
+        return null;
+        // TODO
+    }
+
+    @Override
+    public List<UnificationStep> getUnificationSteps() {
+        return null;
+        // TODO
+    }
+
+    @Override
+    public List<Substitution> getMGU() {
+        return null;
+        // TODO
+    }
+
+    @Override
+    public Type getType() {
+        return null;
+        // TODO
+    }
+}

src/main/java/edu/kit/typicalc/model/TypeInfererInterface.java

@@ -0,0 +1,41 @@
+package edu.kit.typicalc.model;
+
+import java.util.List;
+
+/**
+ * Interface for a type inferer with getter methods used to extract the information about
+ * the type inference that is needed to visualize it step by step.
+ */
+public interface TypeInfererInterface {
+    /**
+     * Returns the first (on the undermost level) inference step of the proof tree of the
+     * type inference, presenting an entry point for the tree-like inference step structure.
+     *
+     * @return the first inference step of the proof tree
+     */
+    InferenceStep getFirstInferenceStep();
+
+    /**
+     * Returns the list of unification steps of this type inference.
+     *
+     * @return the list of unification steps
+     */
+    List<UnificationStep> getUnificationSteps();
+
+    /**
+     * Returns the most general unifier (mgu) for the lambda term that is type-inferred,
+     * as a list of substitutions. If no valid type (correlating with no valid mgu) can be
+     * found for the lambda term to type-infer, null is returned.
+     *
+     * @return the most general unifier, null if there is no valid mgu
+     */
+    List<Substitution> getMGU();
+
+    /**
+     * Returns the type that is the result of the type inference.
+     * If no valid type can be found for the lambda term to type-infer, null is returned.
+     *
+     * @return the final type of the lambda term, null if there is no valid type
+     */
+    Type getType();
+}

src/main/java/edu/kit/typicalc/model/TypeInfererLet.java

@@ -0,0 +1,36 @@
+package edu.kit.typicalc.model;
+
+import java.util.List;
+
+/**
+ * Instances of this subclass of TypeInferer are used to execute the sub-inference starting in let steps.
+ * They provide an extended constructor to make sure this sub-inference is consistent with the „outer“ inference.
+ */
+public class TypeInfererLet extends TypeInferer {
+    /**
+     * Initializes a new TypeInfererLet for the given type assumptions, lambda term and type variable factory.
+     *
+     * @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
+     *                       with the outer inference
+     */
+    protected TypeInfererLet(LambdaTerm lambdaTerm, Map<VarTerm, TypeAbstraction> typeAssumptions,
+                             TypeVariableFactory typeVarFactory) {
+        super(lambdaTerm, typeAssumptions);
+        // TODO
+    }
+
+    /**
+     * Let σ be the most general unifier resulting from this type inference.
+     * The following set of constraints is then returned (needed in the outer inference):
+     * C := { αi = σ(αi) | σ defined for αi }
+     *
+     * @return the constraints needed in the outer inference
+     */
+    public List<Constraint> getLetConstraints() {
+        return null;
+        // TODO
+    }
+
+}

src/main/java/edu/kit/typicalc/model/TypeVariableFactory.java

@@ -0,0 +1,24 @@
+package edu.kit.typicalc.model;
+
+/**
+ * Provides unique type variables on demand.
+ */
+public class TypeVariableFactory {
+
+    /**
+     * Initializes a new type variable factory.
+     */
+    protected TypeVariableFactory() {
+        // TODO
+    }
+
+    /**
+     * Creates a new unique type variable. This method will never return the same variable twice.
+     *
+     * @return a new unique type variable
+     */
+    public TypeVariable nextTypeVariable() {
+        return null;
+        // TODO
+    }
+}

src/main/java/edu/kit/typicalc/view/content/type_inference_content/TypeInferenceView.java

@@ -11,14 +11,14 @@ import edu.kit.typicalc.view.main.MainViewImpl;
 
 @Route(value = "visualize", layout = MainViewImpl.class)
 @PageTitle("TypeInferenceView")
-@CssImport("./styles/views/typeinferenceview/type-inference-view-view.css")
+@CssImport("./styles/views/typeinferenceview/type-inference-view.css")
-public class TypeInferenceViewView extends HorizontalLayout {
+public class TypeInferenceView extends HorizontalLayout {
 
     private TextField name;
     private Button sayHello;
 
-    public TypeInferenceViewView() {
+    public TypeInferenceView() {
-        setId("type-inference-view-view");
+        setId("type-inference-view");
         name = new TextField("Your name");
         sayHello = new Button("Say hello");
         add(name, sayHello);

src/main/java/edu/kit/typicalc/view/main/MainViewImpl.java

@@ -17,7 +17,7 @@ import com.vaadin.flow.component.tabs.Tabs;
 import com.vaadin.flow.component.tabs.TabsVariant;
 import com.vaadin.flow.router.PageTitle;
 import com.vaadin.flow.router.RouterLink;
-import edu.kit.typicalc.view.content.type_inference_content.TypeInferenceViewView;
+import edu.kit.typicalc.view.content.type_inference_content.TypeInferenceView;
 
 import java.util.Optional;
 
@@ -78,7 +78,7 @@ public class MainViewImpl extends AppLayout {
     }
 
     private Component[] createMenuItems() {
-        return new Tab[]{createTab("TypeInferenceView", TypeInferenceViewView.class)};
+        return new Tab[]{createTab("TypeInferenceView", TypeInferenceView.class)};
     }
 
     private static Tab createTab(String text, Class<? extends Component> navigationTarget) {