mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-08 10:20:41 +00:00
Refactor explanation texts
This commit is contained in:
Arne Keller
parent
c190289f6f
commit
0b5016da4f
@ -43,7 +43,7 @@ public class ExplanationCreator implements StepVisitor {
|
||||
|
||||
private final List<String> 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<LambdaTerm> termArguments = termArgumentVisitor.getArguments(abs.getConclusion().getLambdaTerm());
|
||||
Queue<Type> 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<LambdaTerm> termArguments = termArgumentVisitor.getArguments(app.getConclusion().getLambdaTerm());
|
||||
Queue<Type> 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);
|
||||
}
|
||||
|
||||
|
||||
|
||||
@ -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<Locale> 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 "";
|
||||
}
|
||||
}
|
||||
@ -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% \
|
||||
|
||||
Loading…
Reference in New Issue
Block a user