Add unification texts to bundle

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

@@ -30,9 +30,6 @@ import edu.kit.typicalc.model.type.TypeArgumentVisitor;
 import edu.kit.typicalc.model.term.LambdaTerm;
 import edu.kit.typicalc.view.TypicalcI18NProvider;
 
-import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.TEXT;
-import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.CURLY_LEFT;
-import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.CURLY_RIGHT;
 import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.DOLLAR_SIGN;
 import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.SPACE;
 

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

@@ -1,7 +1,6 @@
 package edu.kit.typicalc.view.content.typeinferencecontent.latexcreator;
 
 import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.AssumptionGeneratorUtil.typeAssumptionsToLatex;
-import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.AMPERSAND;
 import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.BRACKET_LEFT;
 import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.BRACKET_RIGHT;
 import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.COMMA;
@@ -17,12 +16,13 @@ import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.La
 import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.CONSTRAINT_SET;
 import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.GAMMA;
 import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.SIGMA;
+import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.DOLLAR_SIGN;
+import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.SPACE;
 
 import java.util.ArrayList;
 import java.util.List;
 import java.util.Locale;
 import java.util.Optional;
-import java.util.Queue;
 
 import org.apache.commons.lang3.tuple.Pair;
 
@@ -39,6 +39,8 @@ import edu.kit.typicalc.model.type.TypeArgumentVisitor;
 import edu.kit.typicalc.util.Result;
 
 public class ExplanationCreatorUnification {
+    private static final String KEY_PREFIX = "expUnification.";
+    private static final String LET_KEY_PREFIX = "expLetUnification.";    
     
     private final TypeArgumentVisitor typeDeterminer = new TypeArgumentVisitor();
     private final TypeInfererInterface typeInferer;
@@ -68,8 +70,8 @@ public class ExplanationCreatorUnification {
    }
 
    private void buildTexts(boolean isLetUnification) {
-       String initialStepKey = isLetUnification ? "key1" : "key2";
+       String initialPrefix = isLetUnification ? LET_KEY_PREFIX : KEY_PREFIX;
-       unificationTexts.add(getDefaultTextLatex(initialStepKey));
+       unificationTexts.add(getDefaultTextLatex(initialPrefix + "initial1"));
        createUnficationTexts();
 
        if (!errorOccurred) {
@@ -86,30 +88,31 @@ public class ExplanationCreatorUnification {
                typeAssumptionsToLatex(typeInferer.getFirstInferenceStep().getConclusion().getTypeAssumptions(), mode);
        String letVariableLatex = new LatexCreatorTerm(this.letVariable.get(), mode).getLatex();
 
-       StringBuilder latex = new StringBuilder(getDefaultTextLatex("key")).
+       StringBuilder latex = new StringBuilder(getDefaultTextLatex(LET_KEY_PREFIX + "typeAss1")).
                append(toLatex(GAMMA)).
-               append(getDefaultTextLatex("key")).
+               append(getDefaultTextLatex(LET_KEY_PREFIX + "typeAss2")).
                append(toLatex(letCounterToLatex(SIGMA))).
+               append(getDefaultTextLatex(LET_KEY_PREFIX + "typeAss3")).
                append(toLatex(GAMMA)).
-               append(getDefaultTextLatex("key")).
+               append(getDefaultTextLatex(LET_KEY_PREFIX + "typeAss4")).
                append(toLatex(letVariableLatex)).
-               append(getDefaultTextLatex("key")).
+               append(getDefaultTextLatex(LET_KEY_PREFIX + "typeAss5")).
                append(toLatex(createTypeAbstraction(typeAssumptions))).
-               append(getDefaultTextLatex("key")).
+               append(getDefaultTextLatex(LET_KEY_PREFIX + "typeAss6")).
                append(toLatex(letVariableLatex)).
-               append(getDefaultTextLatex("key")).
+               append(getDefaultTextLatex(LET_KEY_PREFIX + "typeAss7")).
                append(toLatex(GAMMA)).
-               append(getDefaultTextLatex("key")).
+               append(getDefaultTextLatex(LET_KEY_PREFIX + "typeAss8")).
                append(new LatexCreatorType(typeInferer.getType().get(), mode).getLatex()).
-               append(getDefaultTextLatex("key")).
+               append(getDefaultTextLatex(LET_KEY_PREFIX + "typeAss9")).
                append(toLatex(letCounterToLatex(SIGMA) + PAREN_LEFT + typeAssumptions + "" + PAREN_RIGHT)).
-               append(getDefaultTextLatex("key"));
+               append(getDefaultTextLatex(LET_KEY_PREFIX + "typeAss10"));
        unificationTexts.add(latex.toString());
 
        // add "second part" of let step here, so that the letCounterToLatex method can still be used
-       latex = new StringBuilder(getDefaultTextLatex("key")).
+       latex = new StringBuilder(getDefaultTextLatex(LET_KEY_PREFIX + "letStep1")).
                append(toLatex(letCounterToLatex(CONSTRAINT_SET))).
-               append(getDefaultTextLatex("key"));
+               append(getDefaultTextLatex(LET_KEY_PREFIX + "letStep2"));
        unificationTexts.add(latex.toString());
    }
 
@@ -123,33 +126,30 @@ public class ExplanationCreatorUnification {
    }
 
    private void createFinalType(boolean isLetUnification) {
-       String keyPrefix = isLetUnification ? "let" : "";
+       String keyPrefix = isLetUnification ? LET_KEY_PREFIX : KEY_PREFIX;
 
-       StringBuilder latex = new StringBuilder(getDefaultTextLatex(keyPrefix + "key")).
+       StringBuilder latex = new StringBuilder(getDefaultTextLatex(keyPrefix + "finalType1")).
                append(toLatex(letCounterToLatex(SIGMA))).
-               append(getDefaultTextLatex(keyPrefix + "key")).
+               append(getDefaultTextLatex(keyPrefix + "finalType2")).
                append(toLatex(new LatexCreatorType(typeInferer.getFirstInferenceStep().getConclusion().getType(), mode)
                        .getLatex())).
-               append(getDefaultTextLatex(keyPrefix + "key")).
+               append(getDefaultTextLatex(keyPrefix + "finalType3")).
                append(toLatex(new LatexCreatorType(typeInferer.getType().get(), mode).getLatex())).
-               append(getDefaultTextLatex(keyPrefix + "key"));
+               append(getDefaultTextLatex(keyPrefix + "finalType4"));
        unificationTexts.add(latex.toString());
    }
 
    private void createMGU() {
-       StringBuilder latex =  new StringBuilder(getDefaultTextLatex("key")).
+       StringBuilder latex =  new StringBuilder(getDefaultTextLatex(KEY_PREFIX + "mgu1")).
                append(toLatex(letCounterToLatex(SIGMA))).
-               append(getDefaultTextLatex("key")).
+               append(getDefaultTextLatex(KEY_PREFIX + "mgu2")).
                append(toLatex(letCounterToLatex(CONSTRAINT_SET))).
-               append(getDefaultTextLatex("key"));
+               append(getDefaultTextLatex(KEY_PREFIX + "mgu3"));
        unificationTexts.add(latex.toString());
    }
 
    private String getDefaultTextLatex(String textKey) {
-       return new StringBuilder(LatexCreatorConstants.TEXT + LatexCreatorConstants.CURLY_LEFT).
+       return provider.getTranslation(textKey, locale);
-               append(provider.getTranslation(textKey, locale)).
-               append(LatexCreatorConstants.CURLY_RIGHT)
-               .toString();
    }
 
    // WARNING: call toLatex() before to get proper latex code
@@ -166,7 +166,7 @@ public class ExplanationCreatorUnification {
    }
 
    private String toLatex(String latex) {
-       return LatexCreatorConstants.DOLLAR_SIGN + latex + LatexCreatorConstants.DOLLAR_SIGN;
+       return SPACE + DOLLAR_SIGN + latex + DOLLAR_SIGN + SPACE;
    }
 
    private String getSubstitutionLatex(Substitution sub) {
@@ -197,19 +197,20 @@ public class ExplanationCreatorUnification {
            }
 
            List<Constraint> constraints = step.getConstraints();
-           Queue<Type> leftTypeArgs = typeDeterminer.getArguments(currentConstraint.getFirstType());
+           if (currentConstraint.getFirstType().equals(currentConstraint.getSecondType())) {
-           Queue<Type> rightTypeArgs = typeDeterminer.getArguments(currentConstraint.getSecondType());
+               // trivial constraint
-           if (leftTypeArgs.isEmpty()) {
+               createTrivialConstraintText(currentConstraint);
+           } else if (typeDeterminer.getArguments(currentConstraint.getFirstType()).isEmpty()) {
                // left side is a variable
                createVariableText(currentConstraint.getFirstType(), currentConstraint.getSecondType(),
                        currentConstraint, subs.unwrap().get(0));
-           } else if (rightTypeArgs.isEmpty()) {
+           } else if (typeDeterminer.getArguments(currentConstraint.getSecondType()).isEmpty()) {
                // right side is a variable
                createVariableText(currentConstraint.getSecondType(), currentConstraint.getFirstType(),
                        currentConstraint, subs.unwrap().get(0));
            } else {
                // both sides are functions
-               createFunctionText(leftTypeArgs, rightTypeArgs, currentConstraint,
+               createFunctionText(currentConstraint,
                        constraints.get(constraints.size() - 1), constraints.get(constraints.size() - 2));
            }
 
@@ -217,55 +218,54 @@ public class ExplanationCreatorUnification {
        }
    }
    
-   private void createFunctionText(Queue<Type> leftTypeArgs, Queue<Type> rightTypeArgs, Constraint currentConstraint,
+   private void createTrivialConstraintText(Constraint currentConstraint) {
-           Constraint newConstraint1, Constraint newConstraint2) {
        StringBuilder latex = new StringBuilder();
-       latex.append(getDefaultTextLatex("key")).
+       latex.append(getDefaultTextLatex(KEY_PREFIX + "trivial1")).
        append(toLatex(LatexCreatorConstraints.createSingleConstraint(currentConstraint, mode))).
-       append(getDefaultTextLatex("key")).
+       append(getDefaultTextLatex(KEY_PREFIX + "trivial2"));
+       unificationTexts.add(latex.toString());
+   }
+
+   private void createFunctionText(Constraint currentConstraint, Constraint newConstraint1, Constraint newConstraint2) {
+       StringBuilder latex = new StringBuilder();
+       latex.append(getDefaultTextLatex(KEY_PREFIX + "function1")).
+       append(toLatex(LatexCreatorConstraints.createSingleConstraint(currentConstraint, mode))).
+       append(getDefaultTextLatex(KEY_PREFIX + "function2")).
        append(toLatex(new LatexCreatorType(currentConstraint.getFirstType(), mode).getLatex())).
-       append(getDefaultTextLatex("key")).
+       append(getDefaultTextLatex(KEY_PREFIX + "function3")).
        append(toLatex(new LatexCreatorType(currentConstraint.getSecondType(), mode).getLatex())).
-       append(getDefaultTextLatex("key")).
+       append(getDefaultTextLatex(KEY_PREFIX + "function4")).
-       append(toLatex(new LatexCreatorType(leftTypeArgs.poll(), mode).getLatex())).
-       append(getDefaultTextLatex("key")).
-       append(toLatex(new LatexCreatorType(rightTypeArgs.poll(), mode).getLatex())).
-       append(getDefaultTextLatex("key")).
-       append(toLatex(new LatexCreatorType(leftTypeArgs.poll(), mode).getLatex())).
-       append(getDefaultTextLatex("key")).
-       append(toLatex(new LatexCreatorType(rightTypeArgs.poll(), mode).getLatex())).
-       append(getDefaultTextLatex("key")).
-       append(toLatex(LatexCreatorConstraints.createSingleConstraint(currentConstraint, mode))).
-       append(getDefaultTextLatex("key")).
        append(toLatex(LatexCreatorConstraints.createSingleConstraint(newConstraint1, mode))).
-       append(getDefaultTextLatex("key")).
+       append(getDefaultTextLatex(KEY_PREFIX + "function5")).
        append(toLatex(LatexCreatorConstraints.createSingleConstraint(newConstraint2, mode))).
-       append(getDefaultTextLatex("key")).toString();
+       append(getDefaultTextLatex(KEY_PREFIX + "function6")).
+       append(toLatex(LatexCreatorConstraints.createSingleConstraint(currentConstraint, mode))).
+       append(getDefaultTextLatex(KEY_PREFIX + "function7"));
        unificationTexts.add(latex.toString());
    }
 
    private void createVariableText(Type variable, Type anyType, Constraint currentConstraint,
            Substitution newSubstitution) {
        StringBuilder latex = new StringBuilder();
-       latex.append(getDefaultTextLatex("key")).
+       latex.append(getDefaultTextLatex(KEY_PREFIX + "variable1")).
        append(toLatex(LatexCreatorConstraints.createSingleConstraint(currentConstraint, mode))).
-       append(getDefaultTextLatex("key")).
+       append(getDefaultTextLatex(KEY_PREFIX + "variable2")).
        append(toLatex(new LatexCreatorType(variable, mode).getLatex())).
-       append(getDefaultTextLatex("key")).
+       append(getDefaultTextLatex(KEY_PREFIX + "variable3")).
        append(toLatex(new LatexCreatorType(variable, mode).getLatex())).
-       append(getDefaultTextLatex("key")).
+       append(getDefaultTextLatex(KEY_PREFIX + "variable4")).
        append(toLatex(new LatexCreatorType(anyType, mode).getLatex())).
-       append(getDefaultTextLatex("key")).
+       append(getDefaultTextLatex(KEY_PREFIX + "variable5")).
        append(toLatex(getSubstitutionLatex(newSubstitution))).
-       append(getDefaultTextLatex("key"));
+       append(getDefaultTextLatex(KEY_PREFIX + "variable6"));
        unificationTexts.add(latex.toString());
    }
 
    private void createErrorText(UnificationError errorType) {
        if (errorType == UnificationError.DIFFERENT_TYPES) {
-           unificationTexts.add(getDefaultTextLatex("key"));
+           unificationTexts.add(getDefaultTextLatex(KEY_PREFIX + "infiniteType"));
        } else if (errorType == UnificationError.INFINITE_TYPE) {
-           unificationTexts.add(getDefaultTextLatex("key"));
+           unificationTexts.add(getDefaultTextLatex(KEY_PREFIX + "differentTypes"));
        }
    }
 

src/main/resources/language/translation_de.properties

@@ -244,3 +244,54 @@ explanationTree.letStep7=gestartet. Mit dem Ergebnis der Let-Teilinferenz lässt
 explanationTree.letStep8=bestimmen. Da der Let-Ausdruck und der innere Term vom gleichen Typ sind, muss außerdem die \
 Bedingung
 explanationTree.letStep9=der Constraintmenge hinzugefügt werden.
+
+expUnification.initial1=In den folgenden Schritten wird der Unifikationsalgorithmus auf der Constraintmenge ausgeführt, \
+um den Typen des eingegebenen Terms zu bestimmen.
+expLetUnification.initial1=In den folgenden Schritten wird der Unifikationsalgorithmus auf der Constraintmenge \
+ausgeführt, um den Typen der let-Variable zu finden und damit die neue Typumgebung zu bestimmen.
+expUnification.trivial1=In diesem Schritt wurde der Constraint
+expUnification.trivial2=entfernt. Da linke und rechte Seite identisch sind, ist der Constraint immer erfüllt und \
+wird somit nicht benötigt.
+expUnification.variable1=In diesem Schritt wurde der Constraint
+expUnification.variable2=ersetzt. Da t ein Variablentyp ist und nicht in
+expUnification.variable3=vorkommt, können alle Vorkommen von
+expUnification.variable4=durch
+expUnification.variable5=ersetzt werden. In der Folge wird die Substitution
+expUnification.variable6=erstellt und auf die übrige Constraintmenge angewandt. Die daraus resultierenden Veräderungen \
+sind blau markiert.
+expUnification.function1=In diesem Schritt wurde der Constraint
+expUnification.function2=ersetzt. Da sowohl
+expUnification.function3=als auch
+expUnification.function4=Funktionstypen sind, müssen die beiden Constraints
+expUnification.function5=und
+expUnification.function6=der Constraintmenge hinzugefügt werden. Der ursprüngliche Constraint
+expUnification.function7=wurde aus der Menge entfernt.
+expUnification.mgu1=In diesem Schritt wird der allgemeinste Unifikator
+expUnification.mgu2=der Constraintmenge
+expUnification.mgu3=berechnet. Dafür wird die gesamte Menge an Substitutionen auf jede einzelne der Substitutionen \
+aus der Menge angewandt.
+expUnification.finalType1=In diesem Schritt wird der zuvor berechnete allgemeinste Unifikator
+expUnification.finalType2=auf den Typen
+expUnification.finalType3=des eingegebenen Terms angewandt. Das Ergebnis
+expUnification.finalType4=ist der finale Type des eingegebenen Terms.
+expUnification.infiniteType=Eine Typvariable taucht auf beiden Seiten des hervorgehobenen Constraints auf. \
+Da sich hier ein unendlicher Typ ergeben würde, bricht die Unifikation ab.
+expUnification.diffrentTypes=Da die Typen auf den beiden Seiten des hervorgehobenen Constraints nicht übereinstimmen, \
+bricht die Unifikation hier ab.
+expLetUnification.finalType1=In diesem Schritt wird der zuvor berechnete allgemeinste Unifikator
+expLetUnification.finalType2=auf den Typen
+expLetUnification.finalType3=der Let-Definition angewandt. Das Ergebnis
+expLetUnification.finalType4=ist der finale Typ der Let-Definition.
+expLetUnification.typeAss1=In diesem Schritt werden die Typannahmen
+expLetUnification.typeAss2=für die weitere Durchführung des Algorithmus berechnet. Im ersten Schritt wird dafür der MGU
+expLetUnification.typeAss3=der Let-Teilinferenz auf die aktuelle Menge von Typannahmen angewandt. Die dadurch entstandenen \
+Typannahmen werden anschließend der Menge
+expLetUnification.typeAss4=hinzugefügt. Im zweiten Schritt wird der Typ der let-Variable
+expLetUnification.typeAss5=berechnet. Dafür wird Typabstraktion
+expLetUnification.typeAss6=zuerst instanziiert und dann gemeinsam mit der Variable
+expLetUnification.typeAss7=als Typannahme der Menge
+expLetUnification.typeAss8=hinzugefügt. Bei der Instanziierung werden alle Typvariablen, die frei in
+expLetUnification.typeAss9=aber nicht frei in
+expLetUnification.typeAss10=vorkommen allquantifiziert.
+expLetUnification.letStep1=Die Let-Teilinferenz ist jetzt abgeschlossen. Der Typinferenz-Algorithmus wird mit der um
+expLetUnification.letStep2=erweiterten Constraintmenge und den neu berechneten Typannahmen fortgeführt.