Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc

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

@@ -6,6 +6,7 @@ import edu.kit.typicalc.model.step.*;
 import edu.kit.typicalc.model.term.VarTerm;
 import edu.kit.typicalc.model.type.TypeAbstraction;
 
+import java.util.List;
 import java.util.Map;
 
 import static edu.kit.typicalc.view.content.typeinferencecontent.LatexCreatorConstants.*;
@@ -21,6 +22,7 @@ public class LatexCreator implements StepVisitor {
     private final TypeInfererInterface typeInferer;
     private final StringBuilder tree;
     private final boolean stepLabels;
+    private final LatexCreatorConstraints constraintsCreator;
 
     /**
      * Generate the pieces of LaTeX-code from the type inferer.
@@ -42,6 +44,7 @@ public class LatexCreator implements StepVisitor {
         this.tree = new StringBuilder();
         this.stepLabels = stepLabels;
         typeInferer.getFirstInferenceStep().accept(this);
+        this.constraintsCreator = new LatexCreatorConstraints(typeInferer);
     }
 
     /**
@@ -54,12 +57,16 @@ public class LatexCreator implements StepVisitor {
     }
 
     /**
-     * Returns the LaTeX-code for constraints, unification, MGU and MGU
+     * Returns the LaTeX-code for constraints, unification, MGU and final type
      *
      * @return the LaTeX-code for constraints and unification
      */
     protected String[] getUnification() {
-        return new LatexCreatorConstraints(typeInferer).getEverything().toArray(new String[0]);
+        return constraintsCreator.getEverything().toArray(new String[0]);
+    }
+
+    protected List<Integer> getTreeNumbers() {
+        return constraintsCreator.getTreeNumbers();
     }
 
     /**

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

@@ -18,25 +18,29 @@ public class LatexCreatorConstraints implements StepVisitor {
     private final List<String> constraints;
     private final TypeInfererInterface typeInferer;
     private final ConstraintSetIndexFactory constraintSetIndexFactory;
+    private final TreeNumberGenerator numberGenerator;
     private final String constraintSetIndex;
     private final String prefix;
     private String prevStep;
 
     protected LatexCreatorConstraints(TypeInfererInterface typeInferer) {
-        this(typeInferer, new ConstraintSetIndexFactory(), FIRST_PREFIX);
+        this(typeInferer, new ConstraintSetIndexFactory(), new TreeNumberGenerator(), FIRST_PREFIX);
     }
 
     private LatexCreatorConstraints(TypeInfererInterface typeInferer,
                                       ConstraintSetIndexFactory constraintSetIndexFactory,
+                                      TreeNumberGenerator numberGenerator,
                                       String prefix) {
         this.prefix = prefix;
         this.prevStep = "";
         this.constraintSetIndexFactory = constraintSetIndexFactory;
+        this.numberGenerator = numberGenerator;
         this.constraintSetIndex = constraintSetIndexFactory.nextConstraintSetIndex();
         this.typeInferer = typeInferer;
         constraints = new ArrayList<>();
         if (FIRST_PREFIX.equals(prefix)) {
             constraints.add(CONSTRAINT_SET + EQUALS + LATEX_CURLY_LEFT + LATEX_CURLY_RIGHT);
+            numberGenerator.incrementPush();
         }
 
         typeInferer.getFirstInferenceStep().accept(this);
@@ -44,15 +48,25 @@ public class LatexCreatorConstraints implements StepVisitor {
 
     protected List<String> getEverything() {
         List<String> result = new ArrayList<>(constraints);
-        result.addAll(generateUnification());
+        generateUnification().forEach(step -> {
-        typeInferer.getMGU().ifPresent(mgu -> result.add(generateMGU()));
+            result.add(step);
-        // todo return final type
+            numberGenerator.push();
+        });
+        typeInferer.getMGU().ifPresent(mgu -> {
+            result.add(generateMGU());
+            numberGenerator.push();
+        });
+        // todo return final type, dont forget numberGenerator.push();
         if (FIRST_PREFIX.equals(prefix)) {
             result.replaceAll(content -> ALIGN_BEGIN + content + ALIGN_END);
         }
         return result;
     }
 
+    protected List<Integer> getTreeNumbers() {
+        return numberGenerator.getNumbers();
+    }
+
     private String createSingleConstraint(Constraint constraint) {
         String firstType = new LatexCreatorType(constraint.getFirstType()).getLatex();
         String secondType = new LatexCreatorType(constraint.getSecondType()).getLatex();
@@ -65,6 +79,7 @@ public class LatexCreatorConstraints implements StepVisitor {
         currentConstraint = prefix + CONSTRAINT_SET + constraintSetIndex + EQUALS + LATEX_CURLY_LEFT
                 + prevStep + LATEX_CURLY_RIGHT;
         constraints.add(currentConstraint);
+        numberGenerator.incrementPush();
     }
 
     @Override
@@ -105,7 +120,8 @@ public class LatexCreatorConstraints implements StepVisitor {
     public void visit(LetStepDefault letD) {
         addConstraint(letD);
         LatexCreatorConstraints subCreator = new LatexCreatorConstraints(letD.getTypeInferer(),
-                constraintSetIndexFactory, constraints.get(constraints.size() - 1) + LATEX_NEW_LINE + NEW_LINE);
+                constraintSetIndexFactory, numberGenerator,
+                constraints.get(constraints.size() - 1) + LATEX_NEW_LINE + NEW_LINE);
         constraints.addAll(subCreator.getEverything());
 
         // adds one step in which all let constraints are added to 'outer' constraint set
@@ -114,6 +130,7 @@ public class LatexCreatorConstraints implements StepVisitor {
         letConstraints = prefix + CONSTRAINT_SET + constraintSetIndex + EQUALS + LATEX_CURLY_LEFT
                 + prevStep + LATEX_CURLY_RIGHT;
         constraints.add(letConstraints);
+        numberGenerator.push();
 
         letD.getPremise().accept(this);
     }

src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TreeNumberGenerator.java

@@ -0,0 +1,27 @@
+package edu.kit.typicalc.view.content.typeinferencecontent;
+
+import java.util.ArrayList;
+import java.util.List;
+
+public class TreeNumberGenerator {
+    private final List<Integer> numbers;
+    private int current;
+
+    protected TreeNumberGenerator() {
+        numbers = new ArrayList<>();
+        current = -1;
+    }
+
+    protected void push() {
+        numbers.add(current);
+    }
+
+    protected void incrementPush() {
+        current++;
+        numbers.add(current);
+    }
+
+    protected List<Integer> getNumbers() {
+        return numbers;
+    }
+}

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

@@ -12,6 +12,8 @@ import edu.kit.typicalc.model.TypeInfererInterface;
 import edu.kit.typicalc.view.content.ControlPanel;
 import edu.kit.typicalc.view.content.ControlPanelView;
 
+import java.util.List;
+
 @PageTitle("TypeInferenceView")
 @CssImport("./styles/view/type-inference.css")
 public class TypeInferenceView extends VerticalLayout
@@ -24,6 +26,8 @@ public class TypeInferenceView extends VerticalLayout
     private static final String CONTENT_ID = "content";
     private static final String ID = "type-inference-view";
 
+    private final List<Integer> treeNumbers;
+
     private int currentStep = 0;
 
 
@@ -45,6 +49,7 @@ public class TypeInferenceView extends VerticalLayout
         scroller.setScrollDirection(Scroller.ScrollDirection.BOTH);
         setAlignItems(Alignment.CENTER);
         add(scroller, controlPanel);
+        treeNumbers = lc.getTreeNumbers();
         setContent();
     }
 
@@ -62,38 +67,38 @@ public class TypeInferenceView extends VerticalLayout
         );
     }
 
-    private void refreshElements(int currentStep) {
+    private void refreshElements() {
         unification.showStep(currentStep);
-        tree.showStep(currentStep < tree.getStepCount() ? currentStep : tree.getStepCount() - 1);
+        tree.showStep(treeNumbers.get(currentStep));
     }
 
     @Override
     public void firstStepButton() {
         currentStep = currentStep > tree.getStepCount()  && tree.getStepCount() > 0 ? tree.getStepCount() - 1 : 0;
-        refreshElements(currentStep);
+        refreshElements();
     }
 
     @Override
     public void lastStepButton() {
         currentStep = currentStep < tree.getStepCount() - 1 ? tree.getStepCount() - 1 : unification.getStepCount() - 1;
-        refreshElements(currentStep);
+        refreshElements();
     }
 
     @Override
     public void nextStepButton() {
         currentStep = currentStep < unification.getStepCount() - 1 ? currentStep + 1 : currentStep;
-        refreshElements(currentStep);
+        refreshElements();
     }
 
     @Override
     public void previousStepButton() {
         currentStep = currentStep > 0 ? currentStep - 1 : currentStep;
-        refreshElements(currentStep);
+        refreshElements();
     }
 
     @Override
     public void onComponentEvent(AttachEvent attachEvent) {
         currentStep = 0;
-        refreshElements(currentStep);
+        refreshElements();
     }
 }