From cadc2997911a446b777b85307e739140a44ac881 Mon Sep 17 00:00:00 2001
From: ucrhh <ucrhh@student.kit.edu>
Date: Tue, 9 Feb 2021 22:51:54 +0100
Subject: [PATCH] partly fix issues with failing sub inference

---
 .../java/edu/kit/typicalc/model/Tree.java     |  4 +--
 .../LatexCreatorConstraints.java              | 28 +++++++++++--------
 .../kit/typicalc/view/main/ExampleDialog.java |  3 +-
 3 files changed, 21 insertions(+), 14 deletions(-)

diff --git a/src/main/java/edu/kit/typicalc/model/Tree.java b/src/main/java/edu/kit/typicalc/model/Tree.java
index f70bec8..f303391 100644
--- a/src/main/java/edu/kit/typicalc/model/Tree.java
+++ b/src/main/java/edu/kit/typicalc/model/Tree.java
@@ -63,10 +63,10 @@ public class Tree implements TermVisitorTree {
 
         this.stepFactory = lambdaTerm.hasLet() || partOfLetTerm ? new StepFactoryWithLet() : new StepFactoryDefault();
 
+        this.failedSubInference = false;
+
         this.firstTypeVariable = typeVarFactory.nextTypeVariable();
         this.firstInferenceStep = lambdaTerm.accept(this, typeAssumptions, firstTypeVariable);
-
-        this.failedSubInference = false;
     }
 
     /**
diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreatorConstraints.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreatorConstraints.java
index f5d5095..e589fc8 100644
--- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreatorConstraints.java
+++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreatorConstraints.java
@@ -48,17 +48,19 @@ public class LatexCreatorConstraints implements StepVisitor {
 
     protected List<String> getEverything() {
         List<String> result = new ArrayList<>(constraints);
-        generateUnification().forEach(step -> {
-            result.add(step);
-            numberGenerator.push();
-        });
-        typeInferer.getMGU().ifPresent(mgu -> {
-            result.add(generateMGU());
-            numberGenerator.push();
-            result.add(generateMGU() + LATEX_NEW_LINE + new LatexCreatorType(typeInferer.getType().get()).getLatex());
-            numberGenerator.push();
-        });
-        // todo add some helpful text for the user
+        if (typeInferer.getUnificationSteps().isPresent()) {
+            generateUnification().forEach(step -> {
+                result.add(step);
+                numberGenerator.push();
+            });
+            typeInferer.getMGU().ifPresent(mgu -> {
+                result.add(generateMGU());
+                numberGenerator.push();
+                result.add(generateMGU() + LATEX_NEW_LINE + new LatexCreatorType(typeInferer.getType().get()).getLatex());
+                numberGenerator.push();
+            });
+            // todo add some helpful text for the user
+        }
         if (FIRST_PREFIX.equals(prefix)) {
             result.replaceAll(content -> ALIGN_BEGIN + content + ALIGN_END);
         }
@@ -126,6 +128,10 @@ public class LatexCreatorConstraints implements StepVisitor {
                 constraints.get(constraints.size() - 1) + LATEX_NEW_LINE + NEW_LINE);
         constraints.addAll(subCreator.getEverything());
 
+        // cancels constraint creation if sub inference failed
+        if (letD.getTypeInferer().getMGU().isEmpty()) {
+            return;
+        }
         // adds one step in which all let constraints are added to 'outer' constraint set
         String letConstraints = createLetConstraints(letD.getTypeInferer().getLetConstraints());
         prevStep = prevStep.equals("") ? letConstraints : prevStep + COMMA + letConstraints;
diff --git a/src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java b/src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java
index 779d9be..3c9f796 100644
--- a/src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java
+++ b/src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java
@@ -23,7 +23,8 @@ public class ExampleDialog extends Dialog implements LocaleChangeObserver {
 
     private static final List<String> EXAMPLES =
             List.of("λx.x", "λx.λy.y x", "λx.λy.y (x x)", "let f = λx. g y y in f 3", "(λx.x x) (λx.x x)",
-                    "(λx.λy.y (x y)) (λz. λa. z g a)", "let f = λx. let g = λy. y in g x in f 3");
+                    "(λx.λy.y (x y)) (λz. λa. z g a)", "let f = λx. let g = λy. y in g x in f 3",
+                    "let f = λx. let g = λy.5 5 in g x in f 3");
     private final Paragraph instruction;
 
     /**