Merge remote-tracking branch 'origin/master'

README.md

@@ -109,3 +109,11 @@ PORT=80 java -jar target/typicalc-1.0-SNAPSHOT.jar
 ### Deploying using systemd
 
 Copy the `typicalc.service` file into your systemd configuration and enable the service.
+
+## License
+
+Check the third-party libraries in `frontend/src/` for their respective license.
+
+Typicalc itself is licensed under the GPL 3.0 or (at your option) any later version.
+
+© Robin Böhne, Moritz Dieing, Thomas Heinen, Arne Keller, Johanna Stuber

frontend/src/mathjax-proof-tree.ts

@@ -81,7 +81,8 @@ class MathjaxProofTree extends MathjaxAdapter {
                             margin: 0 !important;\
                         }\
                         .typicalc-type, g[semantics='bspr_prooflabel:left'] {\
-                            stroke: transparent; stroke-width: 600px; pointer-events: all;\
+                            /* cross-browser-compatibility: Chrome does not support the stroke trick, but instead bounding-box (which is not supported by Firefox..) */\
+                            stroke: transparent; stroke-width: 600px; pointer-events: all; pointer-events: bounding-box;\
                         }\
                         #typicalc-definition-abs, #typicalc-definition-abs-let, #typicalc-definition-app,\
                         #typicalc-definition-const, #typicalc-definition-var, #typicalc-definition-var-let, #typicalc-definition-let {\
@@ -276,6 +277,10 @@ class MathjaxProofTree extends MathjaxAdapter {
             (svg.children[1] as SVGGraphicsElement).transform.baseVal[0].matrix.e += offset.e + svgWidth / 2 - conclusionWidth / 2;
             console.timeEnd('stepCalculation');
 
+            const thisShadowRoot = this.shadowRoot;
+            const hoverTextElID = "typicalc-hover-explainer";
+            let defElBackground: SVGRectElement | null;
+
             if (nodeIterator.length >= 3) {
                 // should not be used on empty SVGs
                 window.svgPanZoomFun(svg, {
@@ -316,6 +321,20 @@ class MathjaxProofTree extends MathjaxAdapter {
                                 instance.panBy({x: ev.deltaX - pannedX, y: ev.deltaY - pannedY})
                                 pannedX = ev.deltaX
                                 pannedY = ev.deltaY
+                                // also move the tooltip
+                                let explainer = thisShadowRoot.getElementById(hoverTextElID);
+                                if (explainer) {
+                                    const ctm1 = svg.getBoundingClientRect();
+                                    const ctm2 = defElBackground!.getBoundingClientRect();
+                                    explainer.style.left = (ctm2.left - ctm1.left) + "px";
+                                    explainer.style.top = (ctm2.bottom - ctm1.top) + "px";
+                                    // TODO(performance): this should be more efficient, but somehow flickers
+                                    /*
+                                    const dx = (ctm2.left - ctm1.left) - explainer.offsetLeft;
+                                    const dy = (ctm2.bottom - ctm1.top) - explainer.offsetTop;
+                                    explainer.style.transform = "translate(" + dx + "px," + dy + "px)";
+                                     */
+                                }
                             });
 
                             let initialScale = 1;
@@ -360,12 +379,6 @@ class MathjaxProofTree extends MathjaxAdapter {
 
             const viewport = svg.querySelector("#step0")!.parentNode as SVGGraphicsElement;
             const handleMouseEvent = (e: MouseEvent, mouseIn: boolean) => {
-                // remove previous tooltip, if possible
-                const hoverTextElID = "typicalc-hover-explainer";
-                let explainer = this.shadowRoot!.getElementById(hoverTextElID);
-                if (explainer) {
-                    explainer.parentNode!.removeChild(explainer);
-                }
                 let typeTarget = e.target! as SVGGraphicsElement;
                 let counter = 0;
                 while (!typeTarget.classList.contains("typicalc-type")
@@ -400,7 +413,7 @@ class MathjaxProofTree extends MathjaxAdapter {
                         const svgRect = defEl.getBBox();
                         defEl.transform.baseVal[0].matrix.e = -transform.e - svgRect.width + offsetX + 1000;
                         defEl.transform.baseVal[0].matrix.f = -transform.f - 5500 + offsetY;
-                        let defElBackground = this.shadowRoot!.getElementById(defId + "-background") as SVGRectElement | null;
+                        defElBackground = this.shadowRoot!.getElementById(defId + "-background") as SVGRectElement | null;
                         if (!defElBackground) {
                             defElBackground = document.createElementNS("http://www.w3.org/2000/svg", "rect");
                             defElBackground.id = defId + "-background";
@@ -422,9 +435,45 @@ class MathjaxProofTree extends MathjaxAdapter {
                         p.style.position = "absolute";
                         p.style.left = (ctm2.left - ctm1.left) + "px";
                         p.style.top = (ctm2.bottom - ctm1.top) + "px";
+                        p.style.backgroundColor = "white";
+                        p.style.padding = "5px";
                         p.innerText = data[stepIndex];
                         // @ts-ignore
-                        window.MathJax.typesetPromise([p]);
+                        window.MathJax.typesetPromise([p])
+                            .then(() => {
+                                const svgP = p.getElementsByTagName("svg")[0];
+                                const relevantElement = svgP.childNodes[1]! as SVGGraphicsElement;
+                                const relevantDefs = svgP.childNodes[0]!;
+                                const ourDefs = svg.getElementsByTagName("defs")[0];
+                                while (relevantDefs.childNodes.length > 0) {
+                                    ourDefs.appendChild(relevantDefs.childNodes[0]);
+                                }
+                                const insertionTarget = svg.getElementsByClassName("svg-pan-zoom_viewport")[0];
+                                // remove previous tooltip, if possible
+                                let explainers = svg.getElementsByClassName(hoverTextElID);
+                                for (const explainer of explainers) {
+                                    explainer.parentNode!.removeChild(explainer);
+                                }
+                                relevantElement.classList.add(hoverTextElID);
+                                const x = String(-transform.e - svgRect.width + 30500);
+                                const y = -transform.f - 4000;
+                                const prevTransform = relevantElement.getAttribute("transform");
+                                const newTranslate = "translate(" + x + ", " + y + ")";
+                                const newTransform = prevTransform + " " + newTranslate;
+                                relevantElement.setAttribute("transform", newTransform);
+                                let ttBackground = document.createElementNS("http://www.w3.org/2000/svg", "rect");
+                                ttBackground.classList.add(hoverTextElID);
+                                const bbox = relevantElement.getBBox();
+                                const newTranslate2 = "translate(" + x + ", " + (y - bbox.height / 2) + ")";
+                                const newTransform2 = prevTransform + " " + newTranslate2;
+                                ttBackground.setAttribute("transform", newTransform2);
+                                ttBackground.setAttribute("width", String(bbox.width + 2000));
+                                ttBackground.setAttribute("height", String(bbox.height + 1000));
+                                ttBackground.setAttribute("fill", "yellow");
+                                insertionTarget.appendChild(ttBackground);
+                                insertionTarget.appendChild(relevantElement);
+                                thisShadowRoot.removeChild(p);
+                            });
                         this.shadowRoot!.appendChild(p);
 
                         if (typeTarget.classList.length >= 3) {
@@ -437,6 +486,13 @@ class MathjaxProofTree extends MathjaxAdapter {
                         hoverStyles!.innerHTML = "";
                         hoverStylesUnification!.innerHTML = "";
                     } else if (isLabel) {
+                        // remove previous tooltip, if possible
+                        let explainers = svg.getElementsByClassName(hoverTextElID);
+                        // do not use a for..of loop, it won't work
+                        while (explainers.length > 0) {
+                            const exp = explainers[0];
+                            exp.parentNode!.removeChild(exp);
+                        }
                         const defId = typeTarget.classList[1].replace("-label-", "-definition-");
                         this.shadowRoot!.getElementById(defId)!.style.display = "none";
                         let defElBackground = this.shadowRoot!.getElementById(defId + "-background");

frontend/src/mathjax-setup.js

@@ -99,7 +99,6 @@ window.MathJax = {
                 const OutputJax = startup.getOutputJax();
                 const html = mathjax.document(root, {InputJax, OutputJax});
                 html.render();
-                const hostTag = root.host.tagName.toLowerCase();
                 if (callback) {
                     callback(html);
                 }

pom.xml

@@ -20,7 +20,7 @@
     <parent>
         <groupId>org.springframework.boot</groupId>
         <artifactId>spring-boot-starter-parent</artifactId>
-        <version>2.4.0</version>
+        <version>2.5.3</version>
     </parent>
 
     <repositories>

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

@@ -181,8 +181,14 @@ public class Tree implements TermVisitorTree {
                 return new TypeAbstraction(newType, value.getQuantifiedVariables());
             });
 
-            TypeAbstraction newTypeAbstraction = new TypeAbstraction(
+            Type letType = typeInfererLet.getType().orElseThrow(IllegalStateException::new);
-                    typeInfererLet.getType().orElseThrow(IllegalStateException::new), extendedTypeAssumptions);
+            // increase ID of type variables to highlight them separately
+            for (TypeVariable t : letType.getFreeTypeVariables()) {
+                TypeVariable t2 = new TypeVariable(t.getKind(), t.getIndex());
+                t2.setUniqueIndex(t.getUniqueIndex() + 1);
+                letType = letType.substitute(t, t2);
+            }
+            TypeAbstraction newTypeAbstraction = new TypeAbstraction(letType, extendedTypeAssumptions);
             extendedTypeAssumptions.remove(letTerm.getVariable());
             extendedTypeAssumptions.put(letTerm.getVariable(), newTypeAbstraction);
 

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

@@ -1,13 +1,14 @@
 package edu.kit.typicalc.model.step;
 
+import edu.kit.typicalc.model.Constraint;
 import edu.kit.typicalc.model.type.FunctionType;
-import edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants;
+import edu.kit.typicalc.model.type.Type;
-import edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstraints;
+import edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.*;
-import edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorMode;
+import org.apache.commons.lang3.tuple.Pair;
-import edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorType;
 
 import java.util.ArrayList;
 import java.util.List;
+import java.util.stream.Collectors;
 
 public class StepAnnotator implements StepVisitor {
     private final List<String> annotations = new ArrayList<>();
@@ -18,58 +19,90 @@ public class StepAnnotator implements StepVisitor {
 
     @Override
     public void visit(AbsStepDefault absD) {
-        var t1 = ((FunctionType) absD.getConstraint().getSecondType()).getParameter();
+        visitAbs(absD);
-        var t2 = ((FunctionType) absD.getConstraint().getSecondType()).getOutput();
-        annotations.add("$$\\begin{align}"
-                + "&" + LatexCreatorConstants.RULE_VARIABLE + "_1 := "
-                + new LatexCreatorType(t1, LatexCreatorMode.NORMAL).getLatex() + LatexCreatorConstants.LATEX_NEW_LINE
-                + "\n"
-                + "&" + LatexCreatorConstants.RULE_VARIABLE + "_2 := "
-                + new LatexCreatorType(t2, LatexCreatorMode.NORMAL).getLatex() + LatexCreatorConstants.LATEX_NEW_LINE
-                + "\n"
-                + "&" + LatexCreatorConstraints.createSingleConstraint(absD.getConstraint(), LatexCreatorMode.NORMAL)
-                + "\\end{align}$$");
         absD.getPremise().accept(this);
     }
 
     @Override
     public void visit(AbsStepWithLet absL) {
-        annotations.add("$"
+        visitAbs(absL);
-                + LatexCreatorConstraints.createSingleConstraint(absL.getConstraint(), LatexCreatorMode.NORMAL) + "$");
         absL.getPremise().accept(this);
     }
 
+    private void visitAbs(AbsStep absStep) {
+        var t1 = ((FunctionType) absStep.getConstraint().getSecondType()).getParameter();
+        var t2 = ((FunctionType) absStep.getConstraint().getSecondType()).getOutput();
+        visitGeneric(t1, t2, absStep.getConstraint());
+    }
+
+    private void visitGeneric(Type t1, Type t2, Constraint c) {
+        visitGeneric2(List.of(Pair.of("_1", t1), Pair.of("_2", t2)), c);
+    }
+
+    private void visitGeneric2(List<Pair<String, Type>> types, Constraint c) {
+        visitGeneric3(
+                types.stream()
+                        .map(pair -> Pair.of(pair.getLeft(),
+                                new LatexCreatorType(pair.getRight(), LatexCreatorMode.NORMAL).getLatex()))
+                        .collect(Collectors.toList()),
+                c
+        );
+    }
+
+    private void visitGeneric3(List<Pair<String, String>> types, Constraint c) {
+        var sb = new StringBuilder("$$\\begin{align}");
+        for (var pair : types) {
+            sb.append("&" + LatexCreatorConstants.RULE_VARIABLE)
+                    .append(pair.getLeft())
+                    .append(" := ")
+                    .append(pair.getRight())
+                    .append(LatexCreatorConstants.LATEX_NEW_LINE)
+                    .append("\n");
+        }
+        sb.append("&").append(LatexCreatorConstraints.createSingleConstraint(c, LatexCreatorMode.NORMAL));
+        annotations.add(sb + "\\end{align}$$");
+    }
+
     @Override
     public void visit(AppStepDefault appD) {
-        annotations.add("$"
+        visitGeneric(
-                + LatexCreatorConstraints.createSingleConstraint(appD.getConstraint(), LatexCreatorMode.NORMAL) + "$");
+                appD.getPremise2().getConclusion().getType(),
+                appD.getConclusion().getType(),
+                appD.getConstraint());
         appD.getPremise1().accept(this);
         appD.getPremise2().accept(this);
     }
 
     @Override
     public void visit(ConstStepDefault constD) {
-        annotations.add("$"
+        visitGeneric2(List.of(Pair.of("_c", constD.getConclusion().getType())), constD.getConstraint());
-                + LatexCreatorConstraints.createSingleConstraint(constD.getConstraint(), LatexCreatorMode.NORMAL)
-                + "$");
     }
 
     @Override
     public void visit(VarStepDefault varD) {
-        annotations.add("$"
+        visitGeneric2(List.of(
-                + LatexCreatorConstraints.createSingleConstraint(varD.getConstraint(), LatexCreatorMode.NORMAL) + "$");
+                Pair.of("", varD.getInstantiatedTypeAbs()),
+                Pair.of("'", varD.getConclusion().getType())),
+                varD.getConstraint());
     }
 
     @Override
     public void visit(VarStepWithLet varL) {
-        annotations.add("$"
+        visitGeneric3(List.of(
-                + LatexCreatorConstraints.createSingleConstraint(varL.getConstraint(), LatexCreatorMode.NORMAL) + "$");
+                Pair.of("'",
+                        AssumptionGeneratorUtil.generateTypeAbstraction(varL.getTypeAbsInPremise(),
+                                LatexCreatorMode.NORMAL)),
+                Pair.of("",
+                        new LatexCreatorType(varL.getInstantiatedTypeAbs(), LatexCreatorMode.NORMAL).getLatex())),
+                varL.getConstraint());
     }
 
     @Override
     public void visit(LetStepDefault letD) {
-        annotations.add("$"
+        visitGeneric2(List.of(
-                + LatexCreatorConstraints.createSingleConstraint(letD.getConstraint(), LatexCreatorMode.NORMAL) + "$");
+                Pair.of("_1", letD.getTypeInferer().getFirstInferenceStep().getConclusion().getType()),
+                Pair.of("_2", letD.getPremise().getConclusion().getType())),
+                letD.getConstraint());
         letD.getTypeInferer().getFirstInferenceStep().accept(this);
         letD.getPremise().accept(this);
     }

src/main/java/edu/kit/typicalc/model/term/TermArgumentVisitor.java

@@ -0,0 +1,55 @@
+package edu.kit.typicalc.model.term;
+
+import java.util.LinkedList;
+import java.util.Queue;
+
+public class TermArgumentVisitor implements TermVisitor {
+    
+    private final Queue<LambdaTerm> argumentList = new LinkedList<>();
+
+    public Queue<LambdaTerm> getArguments(LambdaTerm term) {
+        term.accept(this);
+        return argumentList;
+    }
+    
+    @Override
+    public void visit(AppTerm appTerm) {
+        argumentList.clear();
+        argumentList.add(appTerm.getFunction());
+        argumentList.add(appTerm.getParameter());
+    }
+
+    @Override
+    public void visit(AbsTerm absTerm) {
+        argumentList.clear();
+        argumentList.add(absTerm.getVariable());
+        argumentList.add(absTerm.getInner());
+    }
+
+    @Override
+    public void visit(LetTerm letTerm) {
+        argumentList.clear();
+        argumentList.add(letTerm.getVariable());
+        argumentList.add(letTerm.getInner());
+        argumentList.add(letTerm.getVariableDefinition());
+    }
+
+    @Override
+    public void visit(VarTerm varTerm) {
+        argumentList.clear();
+        // no implementation since the VarTerm is its argument
+    }
+
+    @Override
+    public void visit(IntegerTerm intTerm) {
+        argumentList.clear();
+        // no implementation since the IntegerTerm is its argument
+    }
+
+    @Override
+    public void visit(BooleanTerm boolTerm) {
+        argumentList.clear();
+        // no implementation since the BooleanTerm is its argument
+    }
+
+}

src/main/java/edu/kit/typicalc/model/type/TypeArgumentVisitor.java

@@ -0,0 +1,34 @@
+package edu.kit.typicalc.model.type;
+
+import java.util.LinkedList;
+import java.util.Queue;
+
+public class TypeArgumentVisitor implements TypeVisitor {
+    
+    private final Queue<Type> argumentList = new LinkedList<>();
+    
+    public Queue<Type> getArguments(Type type) {
+        type.accept(this);
+        return argumentList;
+    }
+
+    @Override
+    public void visit(NamedType named) {
+        argumentList.clear();
+        // no implementation since the NamedType is its argument
+    }
+
+    @Override
+    public void visit(TypeVariable variable) {
+        argumentList.clear();
+        // no implementation since the TypeVariable is its argument
+    }
+
+    @Override
+    public void visit(FunctionType function) {
+        argumentList.clear();
+        argumentList.add(function.getParameter());
+        argumentList.add(function.getOutput());
+    }
+
+}

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

@@ -37,7 +37,7 @@ public final class AssumptionGeneratorUtil {
         }
     }
 
-    protected static String generateTypeAbstraction(TypeAbstraction abs, LatexCreatorMode mode) {
+    public static String generateTypeAbstraction(TypeAbstraction abs, LatexCreatorMode mode) {
         StringBuilder abstraction = new StringBuilder();
         if (abs.hasQuantifiedVariables()) {
             abstraction.append(FOR_ALL);

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

@@ -0,0 +1,254 @@
+package edu.kit.typicalc.view.content.typeinferencecontent.latexcreator;
+
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.List;
+import java.util.Locale;
+import java.util.Map;
+import java.util.Queue;
+
+import edu.kit.typicalc.model.step.AbsStep;
+import edu.kit.typicalc.model.step.AbsStepDefault;
+import edu.kit.typicalc.model.step.AbsStepWithLet;
+import edu.kit.typicalc.model.step.AppStep;
+import edu.kit.typicalc.model.step.AppStepDefault;
+import edu.kit.typicalc.model.step.ConstStep;
+import edu.kit.typicalc.model.step.ConstStepDefault;
+import edu.kit.typicalc.model.step.EmptyStep;
+import edu.kit.typicalc.model.step.LetStep;
+import edu.kit.typicalc.model.step.LetStepDefault;
+import edu.kit.typicalc.model.step.OnlyConclusionStep;
+import edu.kit.typicalc.model.step.StepVisitor;
+import edu.kit.typicalc.model.step.VarStep;
+import edu.kit.typicalc.model.step.VarStepDefault;
+import edu.kit.typicalc.model.step.VarStepWithLet;
+import edu.kit.typicalc.model.term.TermArgumentVisitor;
+import edu.kit.typicalc.model.type.Type;
+import edu.kit.typicalc.model.type.TypeArgumentVisitor;
+import edu.kit.typicalc.model.term.LambdaTerm;
+import edu.kit.typicalc.view.TypicalcI18NProvider;
+
+public class ExplanationCreator implements StepVisitor {
+    private final TypicalcI18NProvider provider = new TypicalcI18NProvider();
+    private final TermArgumentVisitor termArgumentVisitor = new TermArgumentVisitor();
+    private final TypeArgumentVisitor typeArgumentVisitor = new TypeArgumentVisitor();
+    
+    private final Map<Locale, List<String>> explanationTexts = new HashMap<>();
+    
+    private static final LatexCreatorMode MODE = LatexCreatorMode.MATHJAX;
+
+    public ExplanationCreator() {
+        provider.getProvidedLocales().forEach(l -> explanationTexts.put(l, new ArrayList<String>()));
+    }
+    
+    public Map<Locale, List<String>> getExplanationTexts() {
+        return explanationTexts;
+    }
+    
+    private String getDefaultTextLatex(String textKey, Locale locale) {
+        return new StringBuilder(LatexCreatorConstants.TEXT + LatexCreatorConstants.CURLY_LEFT).
+                append(provider.getTranslation(textKey, locale)).
+                append(LatexCreatorConstants.CURLY_RIGHT)
+                .toString();
+    }
+    
+    private String toLatex(String latex) {
+        return LatexCreatorConstants.DOLLAR_SIGN + latex + LatexCreatorConstants.DOLLAR_SIGN;
+    }
+    
+    @Override
+    public void visit(AbsStepDefault absD) {
+        provider.getProvidedLocales().forEach(l -> {
+            List<String> texts = explanationTexts.get(l);
+            texts.add(createLatexAbsStep(absD, l));
+            explanationTexts.put(l, texts);
+        });
+        absD.getPremise().accept(this);
+    }
+    
+    @Override
+    public void visit(AbsStepWithLet absL) {
+        provider.getProvidedLocales().forEach(l -> {
+            List<String> texts = explanationTexts.get(l);
+            texts.add(createLatexAbsStep(absL, l));
+            explanationTexts.put(l, texts);
+        });
+        absL.getPremise().accept(this);
+    }
+    
+    private String createLatexAbsStep(AbsStep abs, Locale locale) {
+        Queue<LambdaTerm> termArguments = termArgumentVisitor.getArguments(abs.getConclusion().getLambdaTerm());
+        Queue<Type> typeArguments = typeArgumentVisitor.getArguments(abs.getConstraint().getSecondType());
+        
+        return new StringBuilder(getDefaultTextLatex("key", locale)).
+                append(toLatex(new LatexCreatorTerm(abs.getConclusion().getLambdaTerm(), MODE).getLatex())).
+                append(getDefaultTextLatex("key", locale)).
+                append(toLatex(new LatexCreatorType(abs.getConclusion().getType(), MODE).getLatex())).
+                append(getDefaultTextLatex("key", locale)).
+                append(toLatex(new LatexCreatorTerm(termArguments.poll(), MODE).getLatex())).
+                append(getDefaultTextLatex("key", locale)).
+                append(toLatex(new LatexCreatorTerm(termArguments.poll(), MODE).getLatex())).
+                append(getDefaultTextLatex("key", locale)).
+                append(toLatex(new LatexCreatorType(typeArguments.poll(), MODE).getLatex())).
+                append(getDefaultTextLatex("key", locale)).
+                append(toLatex(new LatexCreatorType(typeArguments.poll(), MODE).getLatex())).
+                append(getDefaultTextLatex("key", locale)).
+                append(toLatex(new LatexCreatorType(abs.getConstraint().getSecondType(), MODE).getLatex())).
+                append(getDefaultTextLatex("key", locale)).
+                append(toLatex(LatexCreatorConstraints.createSingleConstraint(abs.getConstraint(), MODE))).
+                append(getDefaultTextLatex("key", locale)).
+                toString();
+    }
+
+    @Override
+    public void visit(AppStepDefault appD) {
+        provider.getProvidedLocales().forEach(l -> {
+            List<String> texts = explanationTexts.get(l);
+            texts.add(createLatexAppStep(appD, l));
+            explanationTexts.put(l, texts);
+        });
+        appD.getPremise1().accept(this);
+        appD.getPremise2().accept(this);
+    }
+    
+    private String createLatexAppStep(AppStep app, Locale locale) {
+        Queue<LambdaTerm> termArguments = termArgumentVisitor.getArguments(app.getConclusion().getLambdaTerm());
+        Queue<Type> typeArguments = typeArgumentVisitor.getArguments(app.getConstraint().getSecondType());
+        
+        return new StringBuilder(getDefaultTextLatex("key", locale)).
+                append(toLatex(new LatexCreatorTerm(app.getConclusion().getLambdaTerm(), MODE).getLatex())).
+                append(getDefaultTextLatex("key", locale)).
+                append(toLatex(new LatexCreatorType(app.getConclusion().getType(), MODE).getLatex())).
+                append(getDefaultTextLatex("key", locale)).
+                append(toLatex(new LatexCreatorTerm(termArguments.poll(), MODE).getLatex())).
+                append(getDefaultTextLatex("key", locale)).
+                append(toLatex(new LatexCreatorTerm(termArguments.poll(), MODE).getLatex())).
+                append(getDefaultTextLatex("key", locale)).
+                append(toLatex(new LatexCreatorType(typeArguments.poll(), MODE).getLatex())).
+                append(getDefaultTextLatex("key", locale)).
+                append(toLatex(new LatexCreatorType(typeArguments.poll(), MODE).getLatex())).
+                append(getDefaultTextLatex("key", locale)).
+                append(toLatex(new LatexCreatorType(app.getConstraint().getSecondType(), MODE).getLatex())).
+                append(getDefaultTextLatex("key", locale)).
+                append(toLatex(LatexCreatorConstraints.createSingleConstraint(app.getConstraint(), MODE))).
+                append(getDefaultTextLatex("key", locale)).
+                toString();
+    }
+    
+
+    @Override
+    public void visit(ConstStepDefault constD) {
+        provider.getProvidedLocales().forEach(l -> {
+            List<String> texts = explanationTexts.get(l);
+            texts.add(createLatexConstStep(constD, l));
+            explanationTexts.put(l, texts);
+        });
+    }
+    
+    private String createLatexConstStep(ConstStep constS, Locale locale) {
+        
+        return new StringBuilder(getDefaultTextLatex("key", locale)).
+                append(toLatex(new LatexCreatorTerm(constS.getConclusion().getLambdaTerm(), MODE).getLatex())).
+                append(getDefaultTextLatex("key", locale)).
+                append(toLatex(new LatexCreatorTerm(constS.getConclusion().getLambdaTerm(), MODE).getLatex())).
+                append(getDefaultTextLatex("key", locale)).
+                append(toLatex(new LatexCreatorType(constS.getConclusion().getType(), MODE).getLatex())).
+                append(getDefaultTextLatex("key", locale)).
+                append(toLatex(new LatexCreatorTerm(constS.getConclusion().getLambdaTerm(), MODE).getLatex())).
+                append(getDefaultTextLatex("key", locale)).
+                append("$" + constS.getConclusion().getType() + "$").
+                append(getDefaultTextLatex("key", locale)).
+                append(toLatex(LatexCreatorConstraints.createSingleConstraint(constS.getConstraint(), MODE))).
+                append(getDefaultTextLatex("key", locale)).
+                toString();
+    }
+
+    @Override
+    public void visit(VarStepDefault varD) {
+        provider.getProvidedLocales().forEach(l -> {
+            List<String> texts = explanationTexts.get(l);
+            texts.add(createLatexVarStep(varD, l));
+            explanationTexts.put(l, texts);
+        });
+    }
+
+    @Override
+    public void visit(VarStepWithLet varL) {
+        provider.getProvidedLocales().forEach(l -> {
+            List<String> texts = explanationTexts.get(l);
+            texts.add(createLatexVarStep(varL, l));
+            explanationTexts.put(l, texts);
+        });
+        // TODO: maybe create slightly different text
+    }
+    
+    private String createLatexVarStep(VarStep varS, Locale locale) {
+        
+        return new StringBuilder(getDefaultTextLatex("key", locale)).
+                append(toLatex(new LatexCreatorTerm(varS.getConclusion().getLambdaTerm(), MODE).getLatex())).
+                append(getDefaultTextLatex("key", locale)).
+                append(toLatex(new LatexCreatorTerm(varS.getConclusion().getLambdaTerm(), MODE).getLatex())).
+                append(getDefaultTextLatex("key", locale)).
+                append(toLatex(new LatexCreatorType(varS.getConclusion().getType(), MODE).getLatex())).
+                append(getDefaultTextLatex("key", locale)).
+                append(toLatex(new LatexCreatorTerm(varS.getConclusion().getLambdaTerm(), MODE).getLatex())).
+                append(getDefaultTextLatex("key", locale)).
+                append(toLatex(new LatexCreatorType(varS.getConstraint().getSecondType(), MODE).getLatex())).
+                append(getDefaultTextLatex("key", locale)).
+                append(toLatex(LatexCreatorConstraints.createSingleConstraint(varS.getConstraint(), MODE))).
+                append(getDefaultTextLatex("key", locale)).
+                toString();
+    }
+
+    @Override
+    public void visit(LetStepDefault letD) {
+        provider.getProvidedLocales().forEach(l -> {
+            List<String> texts = explanationTexts.get(l);
+            texts.add(createLatexLetStep(letD, l));
+            explanationTexts.put(l, texts);
+        });
+        
+        letD.getPremise().accept(this);
+    }
+    
+    private String createLatexLetStep(LetStep letS, Locale locale) {
+        Queue<LambdaTerm> termArguments = termArgumentVisitor.getArguments(letS.getConclusion().getLambdaTerm());
+        LambdaTerm variable = termArguments.poll();
+        LambdaTerm innerTerm = termArguments.poll();
+        
+        return new StringBuilder(getDefaultTextLatex("key", locale)).
+                append(toLatex(new LatexCreatorTerm(letS.getConclusion().getLambdaTerm(), MODE).getLatex())).
+                append(getDefaultTextLatex("key", locale)).
+                append(toLatex(new LatexCreatorType(letS.getConclusion().getType(), MODE).getLatex())).
+                append(getDefaultTextLatex("key", locale)).
+                append(toLatex(new LatexCreatorTerm(variable, MODE).getLatex())).
+                append(getDefaultTextLatex("key", locale)).
+                append(toLatex(new LatexCreatorTerm(termArguments.poll(), MODE).getLatex())).
+                append(getDefaultTextLatex("key", locale)).
+                append(toLatex(new LatexCreatorTerm(innerTerm, MODE).getLatex())).
+                append(getDefaultTextLatex("key", locale)).
+                append(toLatex(new LatexCreatorTerm(variable, MODE).getLatex())).
+                append(getDefaultTextLatex("key", locale)).
+                append(toLatex(new LatexCreatorTerm(innerTerm, MODE).getLatex())).
+                append(getDefaultTextLatex("key", locale)).
+                append(toLatex(new LatexCreatorType(letS.getConstraint().getSecondType(), MODE).getLatex())).
+                append(getDefaultTextLatex("key", locale)).
+                append(toLatex(LatexCreatorConstraints.createSingleConstraint(letS.getConstraint(), MODE))).
+                append(getDefaultTextLatex("key", locale)).
+                toString();
+    }
+    
+
+    @Override
+    public void visit(EmptyStep empty) {
+        // TODO Auto-generated method stub
+        
+    }
+
+    @Override
+    public void visit(OnlyConclusionStep onlyConc) {
+        // TODO Auto-generated method stub
+        
+    }
+
+}

src/test/java/edu/kit/typicalc/model/TreeTest.java

@@ -1,5 +1,6 @@
 package edu.kit.typicalc.model;
 
+import edu.kit.typicalc.model.parser.LambdaParser;
 import edu.kit.typicalc.model.step.*;
 import edu.kit.typicalc.model.term.*;
 import edu.kit.typicalc.model.type.*;
@@ -10,8 +11,7 @@ import org.junit.jupiter.api.Test;
 
 import java.util.*;
 
-import static org.junit.jupiter.api.Assertions.assertEquals;
+import static org.junit.jupiter.api.Assertions.*;
-import static org.junit.jupiter.api.Assertions.assertThrows;
 
 class TreeTest {
 
@@ -171,6 +171,20 @@ class TreeTest {
         assertEquals(constraints, tree.getConstraints());
     }
 
+    @Test
+    void derivedLetTypeHasNewUniqueIndex() {
+        var term = "let id = λx.x in id 5";
+        var tree = new Tree(new HashMap<>(), new LambdaParser(term).parse().unwrap());
+        var ls = (LetStep) tree.getFirstInferenceStep();
+        var as = (AbsStepWithLet) ls.getTypeInferer().getFirstInferenceStep();
+        var vs = (VarStep) as.getPremise();
+        var tv = (TypeVariable) vs.getInstantiatedTypeAbs();
+        var as2 = (AppStep) ls.getPremise();
+        var types = as2.getConclusion().getTypeAssumptions().get(new VarTerm("id")).getQuantifiedVariables().toArray(new TypeVariable[0]);
+        assertEquals(1, types.length);
+        assertNotEquals(tv.getUniqueIndex(), types[0].getUniqueIndex());
+    }
+
     @Test
     void equalsTest() {
         EqualsVerifier.forClass(Tree.class).usingGetClass()