Abstrakte Steps auch commited

src/main/java/edu/kit/typicalc/model/step/AbsStep.java

@@ -0,0 +1,32 @@
+package edu.kit.typicalc.model.step;
+
+import edu.kit.typicalc.model.Conclusion;
+import edu.kit.typicalc.model.Constraint;
+
+/**
+ * Models one step of the inference tree where the abstraction rule is applied.
+ */
+public abstract class AbsStep extends InferenceStep {
+
+    private InferenceStep premise;
+
+    /**
+     * Initializes a new AbsStep with the given values.
+     * @param premise the premise of this step
+     * @param conclusion the conclusion of this step
+     * @param constraint the constraint added in this step
+     */
+    protected AbsStep(InferenceStep premise, Conclusion conclusion, Constraint constraint) {
+        super(conclusion, constraint);
+        this.premise = premise;
+    }
+
+    /**
+     * Getter for the premise of this step.
+     * @return premise the premise of this step
+     */
+    public InferenceStep getPremise() {
+        return this.premise;
+    }
+
+}

src/main/java/edu/kit/typicalc/model/step/AppStep.java

@@ -0,0 +1,36 @@
+package edu.kit.typicalc.model.step;
+
+import edu.kit.typicalc.model.Conclusion;
+import edu.kit.typicalc.model.Constraint;
+
+/**
+ * Models one step of the inference tree where the application rule is applied. The first
+ * premise contains the sub-tree of inference steps for the function of the application term.
+ * The second premise contains the sub-tree of inference steps for the input of the application
+ * term.
+ */
+public abstract class AppStep extends InferenceStep {
+    private InferenceStep premise1;
+    private InferenceStep premise2;
+
+    protected AppStep(InferenceStep premise1, InferenceStep premise2, Conclusion conclusion, Constraint constraint) {
+        super(conclusion, constraint);
+        this.premise1 = premise1;
+        this.premise2 = premise2;
+    }
+
+    /**
+     * Getter for the first premise of this Step.
+     * @return premise1 the first premise of this Step.
+     */
+    public InferenceStep getPremise1() {
+        return premise1;
+    }
+    /**
+     * Getter for the second premise of this Step.
+     * @return premise2 the second premise of this Step.
+     */
+    public InferenceStep getPremise2() {
+        return premise2;
+    }
+}

src/main/java/edu/kit/typicalc/model/step/ConstStep.java

@@ -0,0 +1,18 @@
+package edu.kit.typicalc.model.step;
+
+import edu.kit.typicalc.model.Conclusion;
+import edu.kit.typicalc.model.Constraint;
+
+/**
+ * Models one step of the inference tree where the constant rule is applied.
+ */
+public abstract class ConstStep extends InferenceStep {
+    /**
+     * Initializes a new ConstStep with the given values.
+     * @param conclusion the conclusion of this step
+     * @param constraint the constraint added in this step
+     */
+    protected ConstStep(Conclusion conclusion, Constraint constraint) {
+        super(conclusion, constraint);
+    }
+}

src/main/java/edu/kit/typicalc/model/step/LetStep.java

@@ -0,0 +1,49 @@
+package edu.kit.typicalc.model.step;
+
+import edu.kit.typicalc.model.Conclusion;
+import edu.kit.typicalc.model.Constraint;
+import edu.kit.typicalc.model.TypeInfererLet;
+
+/**
+ * Models one step of the inference tree where the let rule is applied. A let step contains an
+ * additional instance of a type inferer that is responisble for the „sub-inference“ that takes
+ * place when applying the let rule. This type inferer grants access to all the information
+ * needed to visualize this sub-inference.
+ * If the sub-inference fails due to a contradiction or an infinite type forming in its unification,
+ * the inference step representing the second premise of the let step should not be created
+ * and the „outer“ inference should be interrupted
+ */
+public abstract class LetStep extends InferenceStep {
+    private InferenceStep premise;
+    private TypeInfererLet typeInferer;
+
+    /**
+     * Initializes a new LetStep with the given values.
+     * @param conclusion the conclusion of this step
+     * @param constraint the constraint added in this step
+     * @param premise the right premise of this step
+     * @param typeInferer the typeInferer that performs the Type Inference for the premise
+     *                    that needs its own type Inference.
+     */
+    protected LetStep(Conclusion conclusion, Constraint constraint, InferenceStep premise, TypeInfererLet typeInferer) {
+        super(conclusion, constraint);
+        this.premise = premise;
+        this.typeInferer = typeInferer;
+    }
+    /**
+     * Returns the premise of the let step that doesn’t have its own sub-inference (the
+     * one usually placed right in the proof tree).
+     * @return premise the right premise of this step
+     */
+    public InferenceStep getPremise() {
+        return premise;
+    }
+
+    /**
+     * Returns the TypeInferer for the premise which needs its own type Inference.
+     * @return typeInferer the type inferer of the sub-inference
+     */
+    public TypeInfererLet getTypeInferer() {
+        return typeInferer;
+    }
+}

src/main/java/edu/kit/typicalc/model/step/VarStep.java

@@ -0,0 +1,32 @@
+package edu.kit.typicalc.model.step;
+
+import edu.kit.typicalc.model.Conclusion;
+import edu.kit.typicalc.model.Constraint;
+import edu.kit.typicalc.model.type.TypeAbstraction;
+
+/**
+ * Models one step of the inference tree where the variable rule is applied. It contains a type
+ * abstraction that is identified as the type of the variable in the premise of the step.
+ */
+public abstract class VarStep extends InferenceStep {
+    private TypeAbstraction typeAbstractionInPremise;
+
+    /**
+     * Initializes a new VarStep with the given values.
+     * @param conclusion the conclusion of this step
+     * @param constraint the constraint added in this step
+     * @param typeAbstractionInPremise the type abstraction in the premise of this step
+     */
+    protected VarStep(Conclusion conclusion, Constraint constraint, TypeAbstraction typeAbstractionInPremise) {
+        super(conclusion, constraint);
+        this.typeAbstractionInPremise = typeAbstractionInPremise;
+    }
+    /**
+     * Returns the type abstraction in the premise of the step, that is identified as the
+     * variable’s type.
+     * @return the type abstraction in the premise of this step
+     */
+    public TypeAbstraction getTypeAbsInPremise() {
+        return typeAbstractionInPremise;
+    }
+}