diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationCreatorUnification.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationCreatorUnification.java index c6c469b..0671dfc 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationCreatorUnification.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationCreatorUnification.java @@ -71,7 +71,7 @@ public class ExplanationCreatorUnification { private void buildTexts(boolean isLetUnification) { String initialPrefix = isLetUnification ? LET_KEY_PREFIX : KEY_PREFIX; - unificationTexts.add(getDefaultTextLatex(initialPrefix + "initial1")); + unificationTexts.add(getDefaultTextLatex(initialPrefix + "initial")); createUnficationTexts(); if (!errorOccurred) { @@ -84,37 +84,22 @@ public class ExplanationCreatorUnification { } private void createLetUnficiationFinish() { - String typeAssumptions = + String typeAssumptions = typeAssumptionsToLatex(typeInferer.getFirstInferenceStep().getConclusion().getTypeAssumptions(), mode); - String letVariableLatex = new LatexCreatorTerm(this.letVariable.get(), mode).getLatex(); - - // TODO: replace with parametrized translation text (see createVariableText) - StringBuilder latex = new StringBuilder(getDefaultTextLatex(LET_KEY_PREFIX + "typeAss1")). - append(toLatex(GAMMA)). - append(getDefaultTextLatex(LET_KEY_PREFIX + "typeAss2")). - append(toLatex(letCounterToLatex(SIGMA))). - append(getDefaultTextLatex(LET_KEY_PREFIX + "typeAss3")). - append(toLatex(GAMMA)). - append(getDefaultTextLatex(LET_KEY_PREFIX + "typeAss4")). - append(toLatex(letVariableLatex)). - append(getDefaultTextLatex(LET_KEY_PREFIX + "typeAss5")). - append(toLatex(createTypeAbstraction(typeAssumptions))). - append(getDefaultTextLatex(LET_KEY_PREFIX + "typeAss6")). - append(toLatex(letVariableLatex)). - append(getDefaultTextLatex(LET_KEY_PREFIX + "typeAss7")). - append(toLatex(GAMMA)). - append(getDefaultTextLatex(LET_KEY_PREFIX + "typeAss8")). - append(new LatexCreatorType(typeInferer.getType().get(), mode).getLatex()). - append(getDefaultTextLatex(LET_KEY_PREFIX + "typeAss9")). - append(toLatex(letCounterToLatex(SIGMA) + PAREN_LEFT + typeAssumptions + "" + PAREN_RIGHT)). - append(getDefaultTextLatex(LET_KEY_PREFIX + "typeAss10")); - unificationTexts.add(latex.toString()); + String letVariableLatex = toLatex(new LatexCreatorTerm(this.letVariable.get(), mode).getLatex()); + String gamma = toLatex(GAMMA); + String sigma = toLatex(letCounterToLatex(SIGMA)); + String finalType = toLatex(new LatexCreatorType(typeInferer.getType().get(), mode).getLatex()); + String newAssumptions = toLatex(letCounterToLatex(SIGMA) + PAREN_LEFT + typeAssumptions + "" + PAREN_RIGHT); + String typeAbstraction = toLatex(createTypeAbstraction(typeAssumptions)); + String finalText1 = provider.getTranslation(LET_KEY_PREFIX + "typeAss", locale, gamma, sigma, letVariableLatex, + typeAbstraction, finalType, newAssumptions); + unificationTexts.add(finalText1); // add "second part" of let step here, so that the letCounterToLatex method can still be used - latex = new StringBuilder(getDefaultTextLatex(LET_KEY_PREFIX + "letStep1")). - append(toLatex(letCounterToLatex(CONSTRAINT_SET))). - append(getDefaultTextLatex(LET_KEY_PREFIX + "letStep2")); - unificationTexts.add(latex.toString()); + String constraintSet = toLatex(letCounterToLatex(CONSTRAINT_SET)); + String finalText2 = provider.getTranslation(LET_KEY_PREFIX + "letStep", locale, constraintSet); + unificationTexts.add(finalText2); } private String createTypeAbstraction(String typeAssumptions) { @@ -128,26 +113,19 @@ public class ExplanationCreatorUnification { private void createFinalType(boolean isLetUnification) { String keyPrefix = isLetUnification ? LET_KEY_PREFIX : KEY_PREFIX; - - // TODO: replace with parametrized translation text (see createVariableText) - StringBuilder latex = new StringBuilder(getDefaultTextLatex(keyPrefix + "finalType1")). - append(toLatex(letCounterToLatex(SIGMA))). - append(getDefaultTextLatex(keyPrefix + "finalType2")). - append(toLatex(new LatexCreatorType(typeInferer.getFirstInferenceStep().getConclusion().getType(), mode) - .getLatex())). - append(getDefaultTextLatex(keyPrefix + "finalType3")). - append(toLatex(new LatexCreatorType(typeInferer.getType().get(), mode).getLatex())). - append(getDefaultTextLatex(keyPrefix + "finalType4")); - unificationTexts.add(latex.toString()); + String sigma = toLatex(letCounterToLatex(SIGMA)); + String initialType = toLatex( + new LatexCreatorType(typeInferer.getFirstInferenceStep().getConclusion().getType(), mode).getLatex()); + String finalType = toLatex(new LatexCreatorType(typeInferer.getType().get(), mode).getLatex()); + String finalText = provider.getTranslation(keyPrefix + "finalType", locale, sigma, initialType, finalType); + unificationTexts.add(finalText); } private void createMGU() { - StringBuilder latex = new StringBuilder(getDefaultTextLatex(KEY_PREFIX + "mgu1")). - append(toLatex(letCounterToLatex(SIGMA))). - append(getDefaultTextLatex(KEY_PREFIX + "mgu2")). - append(toLatex(letCounterToLatex(CONSTRAINT_SET))). - append(getDefaultTextLatex(KEY_PREFIX + "mgu3")); - unificationTexts.add(latex.toString()); + String sigma = toLatex(letCounterToLatex(SIGMA)); + String constraintSet = toLatex(letCounterToLatex(CONSTRAINT_SET)); + String finalText = provider.getTranslation(KEY_PREFIX + "mgu", locale, sigma, constraintSet); + unificationTexts.add(finalText); } private String getDefaultTextLatex(String textKey) { @@ -188,7 +166,8 @@ public class ExplanationCreatorUnification { // skip first step since the substitutions list is still empty (unification introduction is shown) for (int stepNum = 1; stepNum < unificationSteps.size(); stepNum++) { UnificationStep step = unificationSteps.get(stepNum); - Constraint currentConstraint = step.getProcessedConstraint().get(); // works because only step 0 has no constraint + // works because only step 0 has no constraint + Constraint currentConstraint = step.getProcessedConstraint().get(); Result, UnificationError> subs = step.getSubstitutions(); if (subs.isError()) { @@ -219,31 +198,20 @@ public class ExplanationCreatorUnification { } private void createTrivialConstraintText(Constraint currentConstraint) { - StringBuilder latex = new StringBuilder(); - // TODO: replace with parametrized translation text (see createVariableText) - latex.append(getDefaultTextLatex(KEY_PREFIX + "trivial1")). - append(toLatex(LatexCreatorConstraints.createSingleConstraint(currentConstraint, mode))). - append(getDefaultTextLatex(KEY_PREFIX + "trivial2")); - unificationTexts.add(latex.toString()); + String constraintLatex = toLatex(LatexCreatorConstraints.createSingleConstraint(currentConstraint, mode)); + String finalText = provider.getTranslation(KEY_PREFIX + "trivial", locale, constraintLatex); + unificationTexts.add(finalText); } private void createFunctionText(Constraint currentConstraint, Constraint newConstraint1, Constraint newConstraint2) { - StringBuilder latex = new StringBuilder(); - // TODO: replace with parametrized translation text (see createVariableText) - 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_PREFIX + "function3")). - append(toLatex(new LatexCreatorType(currentConstraint.getSecondType(), mode).getLatex())). - append(getDefaultTextLatex(KEY_PREFIX + "function4")). - append(toLatex(LatexCreatorConstraints.createSingleConstraint(newConstraint1, mode))). - append(getDefaultTextLatex(KEY_PREFIX + "function5")). - append(toLatex(LatexCreatorConstraints.createSingleConstraint(newConstraint2, mode))). - append(getDefaultTextLatex(KEY_PREFIX + "function6")). - append(toLatex(LatexCreatorConstraints.createSingleConstraint(currentConstraint, mode))). - append(getDefaultTextLatex(KEY_PREFIX + "function7")); - unificationTexts.add(latex.toString()); + String constraintLatex = toLatex(LatexCreatorConstraints.createSingleConstraint(currentConstraint, mode)); + String firstType = toLatex(new LatexCreatorType(currentConstraint.getFirstType(), mode).getLatex()); + String secondType = toLatex(new LatexCreatorType(currentConstraint.getSecondType(), mode).getLatex()); + String firstNewConstraint = toLatex(LatexCreatorConstraints.createSingleConstraint(newConstraint1, mode)); + String secondNewConstraint = toLatex(LatexCreatorConstraints.createSingleConstraint(newConstraint2, mode)); + String finalText = provider.getTranslation(KEY_PREFIX + "function", locale, constraintLatex, firstType, + secondType, firstNewConstraint, secondNewConstraint); + unificationTexts.add(finalText); } private void createVariableText(Type variable, Type anyType, Constraint currentConstraint, diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationTranslationProvider.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationTranslationProvider.java index 48aa5ba..d1c965e 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationTranslationProvider.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationTranslationProvider.java @@ -6,6 +6,8 @@ import java.util.List; import java.util.Locale; public class ExplanationTranslationProvider implements I18NProvider { + private static final long serialVersionUID = 5240864819723940755L; + private final I18NProvider innerProvider; public ExplanationTranslationProvider(I18NProvider provider) { diff --git a/src/main/resources/language/translation_de.properties b/src/main/resources/language/translation_de.properties index eb34b66..1a649fd 100644 --- a/src/main/resources/language/translation_de.properties +++ b/src/main/resources/language/translation_de.properties @@ -245,50 +245,34 @@ explanationTree.letStep8=bestimmen. Da der Let-Ausdruck und der innere Term vom Bedingung explanationTree.letStep9=der Constraintmenge hinzugefügt werden. -expUnification.initial1=In den folgenden Schritten wird der Unifikationsalgorithmus auf der Constraintmenge ausgeführt, \ +expUnification.initial=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 \ +expLetUnification.initial=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.trivial=In diesem Schritt wurde der Constraint %0% entfernt. Da linke und rechte Seite identisch sind,\ + ist der Constraint immer erfüllt und wird somit nicht benötigt. expUnification.variable=In diesem Schritt wurde der Constraint %0% ersetzt.\ - Da %1% ein Variablentyp ist und nicht in %2% vorkommt, können alle Vorkommen von %1% durch %2% ersetzt werden.\ - In der Folge wird die Substitution %3% erstellt und auf die übrige Constraintmenge angewandt.\ - Die daraus resultierenden Veränderungen 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. + Da %1% ein Variablentyp ist und nicht in %2% vorkommt, können alle Vorkommen von %1% durch %2% ersetzt werden.\ + In der Folge wird die Substitution %3% erstellt und auf die übrige Constraintmenge angewandt.\ + Die daraus resultierenden Veränderungen sind blau markiert. +expUnification.function=In diesem Schritt wurde der Constraint %0% ersetzt. Da sowohl %1% als auch %2% Funktionstypen\ + sind, müssen die beiden Constraints %3% und %4% der Constraintmenge hinzugefügt werden. Der ursprüngliche Constraint\ + %0% wurde aus der Menge entfernt. +expUnification.mgu=In diesem Schritt wird der allgemeinste Unifikator %0% der Constraintmenge %1% berechnet. Dafür wird\ + die gesamte Menge an Substitutionen auf jede einzelne der Substitutionen aus der Menge angewandt. +expUnification.finalType=In diesem Schritt wird der zuvor berechnete allgemeinste Unifikator %0% auf den Typen %1%\ + des eingegebenen Terms angewandt. Das Ergebnis %2% 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. +expLetUnification.finalType=In diesem Schritt wird der zuvor berechnete allgemeinste Unifikator %0% auf den Typen %1%\ + der Let-Definition angewandt. Das Ergebnis %2% ist der finale Typ der Let-Definition. +expLetUnification.typeAss=In diesem Schritt werden die Typannahmen %0% für die weitere Durchführung des Algorithmus\ + berechnet. Im ersten Schritt wird dafür der MGU %1% der Let-Teilinferenz auf die aktuelle Menge von Typannahmen\ + angewandt. Die dadurch entstandenen Typannahmen werden anschließend der Menge %0% hinzugefügt. Im zweiten Schritt\ + wird der Typ der let-Variable %2% berechnet. Dafür wird die Typabstraktion %3% zuerst instanziiert und dann gemeinsam\ + mit der Variable %2% als Typannahme der Menge %0% hinzugefügt. Bei der Instanziierung werden alle Typvariablen, die frei\ + in %4% aber nicht frei in %5% vorkommen allquantifiziert. +expLetUnification.letStep1=Die Let-Teilinferenz ist jetzt abgeschlossen. Der Typinferenz-Algorithmus wird mit der um %0%\ + erweiterten Constraintmenge und den neu berechneten Typannahmen fortgeführt.