fix bug with failing let sub-inference

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

@@ -109,7 +109,16 @@ public class Tree implements TermVisitorTree {
         constraints.add(newConstraint);
 
         InferenceStep leftPremise = appTerm.getFunction().accept(this, typeAssumptions, leftType);
-        InferenceStep rightPremise = appTerm.getParameter().accept(this, typeAssumptions, rightType);
+
+        InferenceStep rightPremise;
+        // if left sub-tree contains a failing let sub-inference,
+        // cancel tree generation with a step only containing a conclusion
+        if (failedSubInference) {
+            Conclusion rightConclusion = new Conclusion(typeAssumptions, appTerm.getParameter(), rightType);
+            rightPremise = new OnlyConclusionStep(rightConclusion);
+        } else {
+            rightPremise = appTerm.getParameter().accept(this, typeAssumptions, rightType);
+        }
 
         Conclusion conclusion = new Conclusion(typeAssumptions, appTerm, conclusionType);
         return stepFactory.createAppStep(leftPremise, rightPremise, conclusion, newConstraint);

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

@@ -20,7 +20,7 @@ public class EmptyStep extends InferenceStep {
         super(
                 new Conclusion(Collections.emptyMap(), new VarTerm(""), new NamedType("")),
                 new Constraint(new NamedType(""), new NamedType(""))
-        ); // TODO: better dummy parameters?
+        );
     }
 
     @Override

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

@@ -0,0 +1,35 @@
+package edu.kit.typicalc.model.step;
+
+import edu.kit.typicalc.model.Conclusion;
+import edu.kit.typicalc.model.Constraint;
+import edu.kit.typicalc.model.type.NamedType;
+
+/**
+ * OnlyConclusionSteps consist only of a conclusion and have no premises.
+ * They are used if a let sub-inference failed and some branches of the tree should end abruptly
+ * due to the termination of the algorithm, but still contain a conclusion.
+ */
+public class OnlyConclusionStep extends InferenceStep {
+
+    /**
+     * Initializes a new step with only a conclusion.
+     *
+     * @param conclusion the conclusion of the step
+     */
+    public OnlyConclusionStep(Conclusion conclusion) {
+        super(
+                conclusion,
+                new Constraint(new NamedType(""), new NamedType(""))
+        );
+    }
+
+    @Override
+    public Constraint getConstraint() {
+        throw new IllegalStateException("getConstraint() should never be called on an OnlyConclusionStep");
+    }
+
+    @Override
+    public void accept(StepVisitor stepVisitor) {
+        stepVisitor.visit(this);
+    }
+}

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

@@ -60,4 +60,11 @@ public interface StepVisitor {
      * @param empty the empty step to visit
      */
     void visit(EmptyStep empty);
+
+    /**
+     * Visits a step containing only a conclusion.
+     *
+     * @param onlyConc the OnlyConclusionStep to visit
+     */
+    void visit(OnlyConclusionStep onlyConc);
 }

src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreator.java

@@ -177,4 +177,10 @@ public class LatexCreator implements StepVisitor {
         String step = AXC + CURLY_LEFT + CURLY_RIGHT + NEW_LINE;
         tree.insert(0, step);
     }
+
+    @Override
+    public void visit(OnlyConclusionStep onlyConc) {
+        String step = AXC + CURLY_LEFT + conclusionToLatex(onlyConc.getConclusion()) + CURLY_RIGHT + NEW_LINE;
+        tree.insert(0, step);
+    }
 }

src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstraints.java

@@ -214,6 +214,11 @@ public class LatexCreatorConstraints implements StepVisitor {
         // empty steps don't have constraints associated with them
     }
 
+    @Override
+    public void visit(OnlyConclusionStep onlyConc) {
+        // steps containing only a conclusion don't have constraints associated with them
+    }
+
     private StringBuilder generateUnificationName() {
         StringBuilder latex = new StringBuilder();
         latex.append(SIGMA);

src/test/java/edu/kit/typicalc/model/step/TestStepVisitor.java

@@ -41,4 +41,9 @@ public class TestStepVisitor implements StepVisitor {
     public void visit(EmptyStep empty) {
         visited = "empty";
     }
+
+    @Override
+    public void visit(OnlyConclusionStep onlyConc) {
+        visited = "onlyConclusion";
+    }
 }