From dabde5e455d16ee114c6237d2466cbc4a02a2eb8 Mon Sep 17 00:00:00 2001
From: ucrhh <ucrhh@student.kit.edu>
Date: Fri, 12 Feb 2021 12:31:45 +0100
Subject: [PATCH] =?UTF-8?q?make=20final=20type=20look=20consistent=20to=20?=
 =?UTF-8?q?=C3=9Cbungsblatt?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .../typicalc/model/TypeInferenceResult.java   |  2 +-
 .../latexcreator/LatexCreatorConstraints.java | 40 ++++++++++++++-----
 2 files changed, 31 insertions(+), 11 deletions(-)

diff --git a/src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java b/src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java
index cdaecac..68da474 100644
--- a/src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java
+++ b/src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java
@@ -78,7 +78,7 @@ public class TypeInferenceResult {
 
     /**
      * 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.
+     * the mgu to the type variable the type inference result was given in its constructor.
      * 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
diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstraints.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstraints.java
index 3dfb75c..de6a056 100644
--- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstraints.java
+++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstraints.java
@@ -59,8 +59,7 @@ public class LatexCreatorConstraints implements StepVisitor {
             typeInferer.getMGU().ifPresent(mgu -> {
                 result.add(generateMGU(constraintSets));
                 numberGenerator.push();
-                result.add(generateMGU(constraintSets) + LATEX_NEW_LINE
-                            + new LatexCreatorType(typeInferer.getType().get()).getLatex());
+                result.add(generateMGU(constraintSets) + LATEX_NEW_LINE + generateFinalType());
                 numberGenerator.push();
             });
             // todo add some helpful text for the user
@@ -161,6 +160,16 @@ public class LatexCreatorConstraints implements StepVisitor {
         // empty steps dont have constraints associated with them
     }
 
+    private StringBuilder generateUnificationName() {
+        StringBuilder latex = new StringBuilder();
+        latex.append(SIGMA);
+        latex.append(constraintSetIndex);
+        latex.append("" + COLON + EQUALS + MGU + PAREN_LEFT + CONSTRAINT_SET);
+        latex.append(constraintSetIndex);
+        latex.append("" + PAREN_RIGHT + EQUALS);
+        return latex;
+    }
+
     private List<String> generateUnification(String constraintSets) {
         List<String> steps = new ArrayList<>();
 
@@ -176,12 +185,8 @@ public class LatexCreatorConstraints implements StepVisitor {
             }
             StringBuilder latex = new StringBuilder();
             latex.append(constraintSets);
-            latex.append(AMPERSAND + SPLIT_BEGIN + SIGMA);
-            latex.append(constraintSetIndex);
-            latex.append("" + COLON + EQUALS + MGU + PAREN_LEFT + CONSTRAINT_SET);
-            latex.append(constraintSetIndex);
-            latex.append("" + PAREN_RIGHT + EQUALS);
-
+            latex.append(AMPERSAND + SPLIT_BEGIN);
+            latex.append(generateUnificationName());
 
             boolean markError = error.isPresent();
             error.ifPresent(latex::append); // TODO: translation
@@ -244,18 +249,33 @@ public class LatexCreatorConstraints implements StepVisitor {
     private String generateMGU(String constraintSets) {
         StringBuilder latex = new StringBuilder();
         latex.append(constraintSets);
+        latex.append(AMPERSAND + SPLIT_BEGIN);
+        latex.append(generateUnificationName());
         latex.append(SPACE);
         latex.append(BRACKET_LEFT);
         typeInferer.getMGU().ifPresent(mgu -> mgu.forEach(substitution -> {
+            latex.append(AMPERSAND);
             latex.append(new LatexCreatorType(substitution.getVariable()).getLatex());
             latex.append(SUBSTITUTION_SIGN);
             latex.append(new LatexCreatorType(substitution.getType()).getLatex());
             latex.append(COMMA);
             latex.append(LATEX_NEW_LINE);
-            latex.append(NEW_LINE);
         }));
-        latex.delete(latex.length() - (COMMA + LATEX_NEW_LINE + NEW_LINE).length(), latex.length());
+        latex.delete(latex.length() - (COMMA + LATEX_NEW_LINE).length(), latex.length());
         latex.append(BRACKET_RIGHT);
+        latex.append(SPLIT_END);
+        return latex.toString();
+    }
+
+    private String generateFinalType() {
+        StringBuilder latex = new StringBuilder();
+        latex.append(AMPERSAND);
+        latex.append(SIGMA);
+        latex.append(constraintSetIndex);
+        latex.append(PAREN_LEFT);
+        latex.append(new LatexCreatorType(typeInferer.getFirstInferenceStep().getConclusion().getType()).getLatex());
+        latex.append("" + PAREN_RIGHT + EQUALS);
+        latex.append(new LatexCreatorType(typeInferer.getType().get()).getLatex());
         return latex.toString();
     }
 }