From 0b5016da4f61853bee9615b52e68aa70cd937bfd Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Sat, 21 Aug 2021 17:44:49 +0200 Subject: [PATCH] Refactor explanation texts --- .../latexcreator/ExplanationCreator.java | 147 ++++++------------ .../ExplanationTranslationProvider.java | 30 ---- .../language/translation_de.properties | 68 +++----- 3 files changed, 70 insertions(+), 175 deletions(-) delete mode 100644 src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationTranslationProvider.java diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationCreator.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationCreator.java index 273bc41..8700361 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationCreator.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationCreator.java @@ -43,7 +43,7 @@ public class ExplanationCreator implements StepVisitor { private final List explanationTexts = new ArrayList<>(); - private static final LatexCreatorMode MODE = LatexCreatorMode.MATHJAX; + private static final LatexCreatorMode MODE = LatexCreatorMode.NORMAL; // no highlighting here private boolean errorOccurred; // true if one unification was not successful private int letCounter = 0; // count number of lets for unification indices @@ -64,10 +64,6 @@ public class ExplanationCreator implements StepVisitor { return explanationTexts; } - private String getDefaultTextLatex(String textKey) { - return provider.getTranslation(textKey, locale); - } - private String toLatex(String latex) { return SPACE + DOLLAR_SIGN + latex + DOLLAR_SIGN + SPACE; } @@ -76,15 +72,11 @@ public class ExplanationCreator implements StepVisitor { String typeLatex = new LatexCreatorType(typeInferer.getFirstInferenceStep().getConclusion().getType(), MODE). getLatex(); - return new StringBuilder(getDefaultTextLatex(KEY_PREFIX + "initial1")). - append(toLatex(new LatexCreatorTerm( - typeInferer.getFirstInferenceStep().getConclusion().getLambdaTerm(), MODE).getLatex())). - append(getDefaultTextLatex(KEY_PREFIX + "initial2")). - append(toLatex(typeLatex)). - append(getDefaultTextLatex(KEY_PREFIX + "initial3")). - append(toLatex(typeLatex)). - append(getDefaultTextLatex(KEY_PREFIX + "initial4")). - toString(); + var arg1 = toLatex(new LatexCreatorTerm( + typeInferer.getFirstInferenceStep().getConclusion().getLambdaTerm(), MODE).getLatex()); + var arg2 = toLatex(typeLatex); + + return provider.getTranslation(KEY_PREFIX + "initial", locale, arg1, arg2); } @Override @@ -103,24 +95,17 @@ public class ExplanationCreator implements StepVisitor { Queue termArguments = termArgumentVisitor.getArguments(abs.getConclusion().getLambdaTerm()); Queue typeArguments = typeArgumentVisitor.getArguments(abs.getConstraint().getSecondType()); - return new StringBuilder(getDefaultTextLatex(KEY_PREFIX + "absStep1")). - append(toLatex(new LatexCreatorTerm(abs.getConclusion().getLambdaTerm(), MODE).getLatex())). - append(getDefaultTextLatex(KEY_PREFIX + "absStep2")). - append(toLatex(new LatexCreatorType(abs.getConclusion().getType(), MODE).getLatex())). - append(getDefaultTextLatex(KEY_PREFIX + "absStep3")). - append(toLatex(new LatexCreatorTerm(termArguments.poll(), MODE).getLatex())). - append(getDefaultTextLatex(KEY_PREFIX + "absStep4")). - append(toLatex(new LatexCreatorTerm(termArguments.poll(), MODE).getLatex())). - append(getDefaultTextLatex(KEY_PREFIX + "absStep5")). - append(toLatex(new LatexCreatorType(typeArguments.poll(), MODE).getLatex())). - append(getDefaultTextLatex(KEY_PREFIX + "absStep6")). - append(toLatex(new LatexCreatorType(typeArguments.poll(), MODE).getLatex())). - append(getDefaultTextLatex(KEY_PREFIX + "absStep7")). - append(toLatex(new LatexCreatorType(abs.getConstraint().getSecondType(), MODE).getLatex())). - append(getDefaultTextLatex(KEY_PREFIX + "absStep8")). - append(toLatex(LatexCreatorConstraints.createSingleConstraint(abs.getConstraint(), MODE))). - append(getDefaultTextLatex(KEY_PREFIX + "absStep9")). - toString(); + var arg1 = toLatex(new LatexCreatorTerm(abs.getConclusion().getLambdaTerm(), MODE).getLatex()); + var arg2 = toLatex(new LatexCreatorType(abs.getConclusion().getType(), MODE).getLatex()); + var arg3 = toLatex(new LatexCreatorTerm(termArguments.poll(), MODE).getLatex()); + var arg4 = toLatex(new LatexCreatorTerm(termArguments.poll(), MODE).getLatex()); + var arg5 = toLatex(new LatexCreatorType(typeArguments.poll(), MODE).getLatex()); + var arg6 = toLatex(new LatexCreatorType(typeArguments.poll(), MODE).getLatex()); + var arg7 = toLatex(new LatexCreatorType(abs.getConstraint().getSecondType(), MODE).getLatex()); + var arg8 = toLatex(LatexCreatorConstraints.createSingleConstraint(abs.getConstraint(), MODE)); + + return provider.getTranslation(KEY_PREFIX + "absStep", locale, + arg1, arg2, arg3, arg4, arg5, arg6, arg7, arg8); } @Override @@ -134,24 +119,17 @@ public class ExplanationCreator implements StepVisitor { Queue termArguments = termArgumentVisitor.getArguments(app.getConclusion().getLambdaTerm()); Queue typeArguments = typeArgumentVisitor.getArguments(app.getConstraint().getSecondType()); - return new StringBuilder(getDefaultTextLatex(KEY_PREFIX + "appStep1")). - append(toLatex(new LatexCreatorTerm(app.getConclusion().getLambdaTerm(), MODE).getLatex())). - append(getDefaultTextLatex(KEY_PREFIX + "appStep2")). - append(toLatex(new LatexCreatorType(app.getConclusion().getType(), MODE).getLatex())). - append(getDefaultTextLatex(KEY_PREFIX + "appStep3")). - append(toLatex(new LatexCreatorTerm(termArguments.poll(), MODE).getLatex())). - append(getDefaultTextLatex(KEY_PREFIX + "appStep4")). - append(toLatex(new LatexCreatorTerm(termArguments.poll(), MODE).getLatex())). - append(getDefaultTextLatex(KEY_PREFIX + "appStep5")). - append(toLatex(new LatexCreatorType(typeArguments.poll(), MODE).getLatex())). - append(getDefaultTextLatex(KEY_PREFIX + "appStep6")). - append(toLatex(new LatexCreatorType(typeArguments.poll(), MODE).getLatex())). - append(getDefaultTextLatex(KEY_PREFIX + "appStep7")). - append(toLatex(new LatexCreatorType(app.getConstraint().getSecondType(), MODE).getLatex())). - append(getDefaultTextLatex(KEY_PREFIX + "appStep8")). - append(toLatex(LatexCreatorConstraints.createSingleConstraint(app.getConstraint(), MODE))). - append(getDefaultTextLatex(KEY_PREFIX + "appStep9")). - toString(); + var arg1 = toLatex(new LatexCreatorTerm(app.getConclusion().getLambdaTerm(), MODE).getLatex()); + var arg2 = toLatex(new LatexCreatorType(app.getConclusion().getType(), MODE).getLatex()); + var arg3 = toLatex(new LatexCreatorTerm(termArguments.poll(), MODE).getLatex()); + var arg4 = toLatex(new LatexCreatorTerm(termArguments.poll(), MODE).getLatex()); + var arg5 = toLatex(new LatexCreatorType(typeArguments.poll(), MODE).getLatex()); + var arg6 = toLatex(new LatexCreatorType(typeArguments.poll(), MODE).getLatex()); + var arg7 = toLatex(new LatexCreatorType(app.getConstraint().getSecondType(), MODE).getLatex()); + var arg8 = toLatex(LatexCreatorConstraints.createSingleConstraint(app.getConstraint(), MODE)); + + return provider.getTranslation(KEY_PREFIX + "appStep", locale, + arg1, arg2, arg3, arg4, arg5, arg6, arg7, arg8); } @@ -162,20 +140,12 @@ public class ExplanationCreator implements StepVisitor { private String createLatexConstStep(ConstStep constS) { - return new StringBuilder(getDefaultTextLatex(KEY_PREFIX + "constStep1")). - append(toLatex(new LatexCreatorTerm(constS.getConclusion().getLambdaTerm(), MODE).getLatex())). - append(getDefaultTextLatex(KEY_PREFIX + "constStep2")). - append(toLatex(new LatexCreatorTerm(constS.getConclusion().getLambdaTerm(), MODE).getLatex())). - append(getDefaultTextLatex(KEY_PREFIX + "constStep3")). - append(toLatex(new LatexCreatorType(constS.getConclusion().getType(), MODE).getLatex())). - append(getDefaultTextLatex(KEY_PREFIX + "constStep4")). - append(toLatex(new LatexCreatorTerm(constS.getConclusion().getLambdaTerm(), MODE).getLatex())). - append(getDefaultTextLatex(KEY_PREFIX + "constStep5")). - append(toLatex(new LatexCreatorType(constS.getConstraint().getSecondType(), MODE).getLatex())). - append(getDefaultTextLatex(KEY_PREFIX + "constStep6")). - append(toLatex(LatexCreatorConstraints.createSingleConstraint(constS.getConstraint(), MODE))). - append(getDefaultTextLatex(KEY_PREFIX + "constStep7")). - toString(); + var arg1 = toLatex(new LatexCreatorTerm(constS.getConclusion().getLambdaTerm(), MODE).getLatex()); + var arg2 = toLatex(new LatexCreatorType(constS.getConclusion().getType(), MODE).getLatex()); + var arg3 = toLatex(new LatexCreatorType(constS.getConstraint().getSecondType(), MODE).getLatex()); + var arg4 = toLatex(LatexCreatorConstraints.createSingleConstraint(constS.getConstraint(), MODE)); + + return provider.getTranslation(KEY_PREFIX + "constStep", locale, arg1, arg2, arg3, arg4); } @Override @@ -192,20 +162,12 @@ public class ExplanationCreator implements StepVisitor { private String createLatexVarStep(VarStep varS) { String termLatex = new LatexCreatorTerm(varS.getConclusion().getLambdaTerm(), MODE).getLatex(); - return new StringBuilder(getDefaultTextLatex(KEY_PREFIX + "varStep1")). - append(toLatex(termLatex)). - append(getDefaultTextLatex(KEY_PREFIX + "varStep2")). - append(toLatex(termLatex)). - append(getDefaultTextLatex(KEY_PREFIX + "varStep3")). - append(toLatex(new LatexCreatorType(varS.getConclusion().getType(), MODE).getLatex())). - append(getDefaultTextLatex(KEY_PREFIX + "varStep4")). - append(toLatex(termLatex)). - append(getDefaultTextLatex(KEY_PREFIX + "varStep5")). - append(toLatex(new LatexCreatorType(varS.getConstraint().getSecondType(), MODE).getLatex())). - append(getDefaultTextLatex(KEY_PREFIX + "varStep6")). - append(toLatex(LatexCreatorConstraints.createSingleConstraint(varS.getConstraint(), MODE))). - append(getDefaultTextLatex(KEY_PREFIX + "varStep7")). - toString(); + var arg1 = toLatex(termLatex); + var arg2 = toLatex(new LatexCreatorType(varS.getConclusion().getType(), MODE).getLatex()); + var arg3 = toLatex(new LatexCreatorType(varS.getConstraint().getSecondType(), MODE).getLatex()); + var arg4 = toLatex(LatexCreatorConstraints.createSingleConstraint(varS.getConstraint(), MODE)); + + return provider.getTranslation(KEY_PREFIX + "varStep", locale, arg1, arg2, arg3, arg4); } @Override @@ -231,26 +193,17 @@ public class ExplanationCreator implements StepVisitor { } private String createLatexLetStep(LetStep letS, LambdaTerm variable, LambdaTerm innerTerm, - LambdaTerm variableDefinition) { + LambdaTerm variableDefinition) { - return new StringBuilder(getDefaultTextLatex(KEY_PREFIX + "letStep1")). - append(toLatex(new LatexCreatorTerm(letS.getConclusion().getLambdaTerm(), MODE).getLatex())). - append(getDefaultTextLatex(KEY_PREFIX + "letStep2")). - append(toLatex(new LatexCreatorType(letS.getConclusion().getType(), MODE).getLatex())). - append(getDefaultTextLatex(KEY_PREFIX + "letStep3")). - append(toLatex(new LatexCreatorTerm(variable, MODE).getLatex())). - append(getDefaultTextLatex(KEY_PREFIX + "letStep4")). - append(toLatex(new LatexCreatorTerm(variableDefinition, MODE).getLatex())). - append(getDefaultTextLatex(KEY_PREFIX + "letStep5")). - append(toLatex(new LatexCreatorTerm(innerTerm, MODE).getLatex())). - append(getDefaultTextLatex(KEY_PREFIX + "letStep6")). - append(toLatex(new LatexCreatorTerm(variableDefinition, MODE).getLatex())). - append(getDefaultTextLatex(KEY_PREFIX + "letStep7")). - append(toLatex(new LatexCreatorTerm(variable, MODE).getLatex())). - append(getDefaultTextLatex(KEY_PREFIX + "letStep8")). - append(toLatex(LatexCreatorConstraints.createSingleConstraint(letS.getConstraint(), MODE))). - append(getDefaultTextLatex(KEY_PREFIX + "letStep9")). - toString(); + var arg1 = toLatex(new LatexCreatorTerm(letS.getConclusion().getLambdaTerm(), MODE).getLatex()); + var arg2 = toLatex(new LatexCreatorType(letS.getConclusion().getType(), MODE).getLatex()); + var arg3 = toLatex(new LatexCreatorTerm(variable, MODE).getLatex()); + var arg4 = toLatex(new LatexCreatorTerm(variableDefinition, MODE).getLatex()); + var arg5 = toLatex(new LatexCreatorTerm(innerTerm, MODE).getLatex()); + var arg6 = toLatex(LatexCreatorConstraints.createSingleConstraint(letS.getConstraint(), MODE)); + + return provider.getTranslation(KEY_PREFIX + "letStep", locale, + arg1, arg2, arg3, arg4, arg5, arg6); } 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 deleted file mode 100644 index d1c965e..0000000 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationTranslationProvider.java +++ /dev/null @@ -1,30 +0,0 @@ -package edu.kit.typicalc.view.content.typeinferencecontent.latexcreator; - -import com.vaadin.flow.i18n.I18NProvider; - -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) { - this.innerProvider = provider; - } - - @Override - public List getProvidedLocales() { - return innerProvider.getProvidedLocales(); - } - - @Override - public String getTranslation(String key, Locale locale, Object... params) { - return innerProvider.getTranslation(key, locale, params); - } - - public String getTranslationInstantiated(String key, Locale locale, Object... params) { - return ""; - } -} diff --git a/src/main/resources/language/translation_de.properties b/src/main/resources/language/translation_de.properties index a9f2994..89797e9 100644 --- a/src/main/resources/language/translation_de.properties +++ b/src/main/resources/language/translation_de.properties @@ -197,54 +197,26 @@ share.latexTree.label=LaTeX-Code (vollständiger Typherleitungsbaum) share.packagesUnification.label=Pakete (Unifikation/MGU) share.latexUnification.label=LaTeX-Code (aktueller Schritt in Unifikation/MGU) -explanationTree.initial1=Zu Beginn der Typinferenz wird dem eingegebenen Term -explanationTree.initial2=die Typvariable -explanationTree.initial3=zugewiesen. In den folgenden Schritten wird der Typ von -explanationTree.initial4=sukzessive bestimmt. -explanationTree.varStep1=Der aktuelle Term -explanationTree.varStep2=ist eine Variable. Daher wird in diesem Schritt die Var-Regel auf die Variable -explanationTree.varStep3=vom Typ -explanationTree.varStep4=angewendet. Da -explanationTree.varStep5=unter der Typumgebung den Typen -explanationTree.varStep6=besitzt, wird die Bedingung -explanationTree.varStep7=der Constraintmenge hinzugefügt. -explanationTree.absStep1=Da der aktuelle Term -explanationTree.absStep2=eine Abstraktion vom Typ -explanationTree.absStep3=mit Parameter -explanationTree.absStep4=und Ergebnis -explanationTree.absStep5=ist, wird in diesem Schritt die Abs-Regel angewendet. Dafür wird dem Parameter der Typ -explanationTree.absStep6=und dem Ergebnis der Typ -explanationTree.absStep7=zugewiesen. Da die Abstraktion unter dieser zusätzlichen Annahme den Typ -explanationTree.absStep8=besitzt, muss die Bedingung -explanationTree.absStep9=der Constraintmenge hinzugefügt werden. -explanationTree.appStep1=Da der aktuelle Term -explanationTree.appStep2=eine Applikation vom Typ -explanationTree.appStep3=mit Funktion -explanationTree.appStep4=und Argument -explanationTree.appStep5=ist, wird in diesem Schritt die App-Regel angewendet. Dafür wird der Funktion der Typ -explanationTree.appStep6=und dem Argument der Typ -explanationTree.appStep7=zugewiesen. Da die Funktion unter dieser zusätzlichen Annahme den Typ -explanationTree.appStep8=besitzt, muss die Bedingung -explanationTree.appStep9=der Constraintmenge hinzugefügt werden. -explanationTree.constStep1=Der aktuelle Term -explanationTree.constStep2=ist eine Konstante. Daher wird in diesem Schritt die Const-Regel auf die Konstante -explanationTree.constStep3=vom Typ -explanationTree.constStep4=angewendet. Da -explanationTree.constStep5=ein -explanationTree.constStep6=Wert ist, wird die Bedingung -explanationTree.constStep7=der Constraintmenge hinzugefügt. -explanationTree.letStep1=Da der aktuelle Term -explanationTree.letStep2=ein Let-Ausdruck vom Typ -explanationTree.letStep3=mit Variable -explanationTree.letStep4=, Definition -explanationTree.letStep5=und innerem Term -explanationTree.letStep6=ist, wird in diesem Schritt die Let-Regel angewendet. Dafür wird im linken Teilbaum eine neue \ -Typinferenz mit dem Term -explanationTree.letStep7=gestartet. Mit dem Ergebnis der Let-Teilinferenz lässt sich anschließend der Typ der Variable -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. - +explanationTree.initial=Zu Beginn der Typinferenz wird dem eingegebenen Term %0% die Typvariable %1% zugewiesen. \ +In den folgenden Schritten wird der Typ von %1% sukzessive bestimmt. +explanationTree.varStep=Der aktuelle Term %0% ist eine Variable. Daher wird in diesem Schritt die Var-Regel auf die \ +Variable %0% vom Typ %1% angewendet. Da %0% unter der Typumgebung den Typen %2% besitzt, wird die Bedingung %3% \ +der Constraintmenge hinzugefügt. +explanationTree.absStep=Da der aktuelle Term %0% eine Abstraktion vom Typ %1% mit Parameter %2% und Ergebnis %3% ist, \ +wird in diesem Schritt die Abs-Regel angewendet. Dafür wird dem Parameter der Typ %4% und dem Ergebnis der Typ %5% \ +zugewiesen. Da die Abstraktion unter dieser zusätzlichen Annahme den Typ %6% besitzt, muss die Bedingung %7% der \ +Constraintmenge hinzugefügt werden. +explanationTree.appStep=Da der aktuelle Term %0% eine Applikation vom Typ %1% mit Funktion %2% und Argument %3% ist, \ +wird in diesem Schritt die App-Regel angewendet. Dafür wird der Funktion der Typ %4% und dem Argument der Typ %5% \ +zugewiesen. Da die Funktion unter dieser zusätzlichen Annahme den Typ %6% besitzt, muss die Bedingung %7% der \ +Constraintmenge hinzugefügt werden. +explanationTree.constStep=Der aktuelle Term %0% ist eine Konstante. Daher wird in diesem Schritt die Const-Regel auf \ +die Konstante %0% vom Typ %1% angewendet. Da %0% ein %2%-Wert ist, wird die Bedingung %3% der Constraintmenge hinzugefügt. +explanationTree.letStep=Da der aktuelle Term %0% ein Let-Ausdruck vom Typ %1% mit Variable %2%, Definition %3% \ +und innerem Term %4% ist, wird in diesem Schritt die Let-Regel angewendet. Dafür wird im linken Teilbaum eine neue \ +Typinferenz mit dem Term %3% gestartet. Mit dem Ergebnis der Let-Teilinferenz lässt sich anschließend der Typ der Variable \ +%2% bestimmen. Da der Let-Ausdruck und der innere Term vom gleichen Typ sind, muss außerdem die \ +Bedingung %5% der Constraintmenge hinzugefügt werden. expUnification.initial=In den folgenden Schritten wird der Unifikationsalgorithmus auf der Constraintmenge %0% ausgeführt, \ um den Typen des eingegebenen Terms zu bestimmen. expLetUnification.initial=In den folgenden Schritten wird der Unifikationsalgorithmus auf der Constraintmenge %0% \