arnekeller/Typicalc
1
0
Fork 0
mirror of https://gitlab.kit.edu/uskyk/typicalc.git synced 2024-11-08 10:20:41 +00:00
Code Issues Packages Projects Releases Wiki Activity

Refractor unification explanation

Browse Source
This commit is contained in:
Moritz Dieing 2021-08-18 10:16:26 +02:00
parent 8ec10126b5
commit 8cc089e543
3 changed files with 63 additions and 109 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -71,7 +71,7 @@ public class ExplanationCreatorUnification {
private void buildTexts(boolean isLetUnification) { private void buildTexts(boolean isLetUnification) {
String initialPrefix = isLetUnification ? LET_KEY_PREFIX : KEY_PREFIX; String initialPrefix = isLetUnification ? LET_KEY_PREFIX : KEY_PREFIX;
unificationTexts.add(getDefaultTextLatex(initialPrefix + "initial1")); unificationTexts.add(getDefaultTextLatex(initialPrefix + "initial"));
createUnficationTexts(); createUnficationTexts();
if (!errorOccurred) { if (!errorOccurred) {
@ -86,35 +86,20 @@ public class ExplanationCreatorUnification {
private void createLetUnficiationFinish() { private void createLetUnficiationFinish() {
String typeAssumptions = String typeAssumptions =
typeAssumptionsToLatex(typeInferer.getFirstInferenceStep().getConclusion().getTypeAssumptions(), mode); typeAssumptionsToLatex(typeInferer.getFirstInferenceStep().getConclusion().getTypeAssumptions(), mode);
String letVariableLatex = new LatexCreatorTerm(this.letVariable.get(), mode).getLatex(); String letVariableLatex = toLatex(new LatexCreatorTerm(this.letVariable.get(), mode).getLatex());
String gamma = toLatex(GAMMA);
// TODO: replace with parametrized translation text (see createVariableText) String sigma = toLatex(letCounterToLatex(SIGMA));
StringBuilder latex = new StringBuilder(getDefaultTextLatex(LET_KEY_PREFIX + "typeAss1")). String finalType = toLatex(new LatexCreatorType(typeInferer.getType().get(), mode).getLatex());
append(toLatex(GAMMA)). String newAssumptions = toLatex(letCounterToLatex(SIGMA) + PAREN_LEFT + typeAssumptions + "" + PAREN_RIGHT);
append(getDefaultTextLatex(LET_KEY_PREFIX + "typeAss2")). String typeAbstraction = toLatex(createTypeAbstraction(typeAssumptions));
append(toLatex(letCounterToLatex(SIGMA))). String finalText1 = provider.getTranslation(LET_KEY_PREFIX + "typeAss", locale, gamma, sigma, letVariableLatex,
append(getDefaultTextLatex(LET_KEY_PREFIX + "typeAss3")). typeAbstraction, finalType, newAssumptions);
append(toLatex(GAMMA)). unificationTexts.add(finalText1);
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());
// add "second part" of let step here, so that the letCounterToLatex method can still be used // add "second part" of let step here, so that the letCounterToLatex method can still be used
latex = new StringBuilder(getDefaultTextLatex(LET_KEY_PREFIX + "letStep1")). String constraintSet = toLatex(letCounterToLatex(CONSTRAINT_SET));
append(toLatex(letCounterToLatex(CONSTRAINT_SET))). String finalText2 = provider.getTranslation(LET_KEY_PREFIX + "letStep", locale, constraintSet);
append(getDefaultTextLatex(LET_KEY_PREFIX + "letStep2")); unificationTexts.add(finalText2);
unificationTexts.add(latex.toString());
} }
private String createTypeAbstraction(String typeAssumptions) { private String createTypeAbstraction(String typeAssumptions) {
@ -128,26 +113,19 @@ public class ExplanationCreatorUnification {
private void createFinalType(boolean isLetUnification) { private void createFinalType(boolean isLetUnification) {
String keyPrefix = isLetUnification ? LET_KEY_PREFIX : KEY_PREFIX; String keyPrefix = isLetUnification ? LET_KEY_PREFIX : KEY_PREFIX;
String sigma = toLatex(letCounterToLatex(SIGMA));
// TODO: replace with parametrized translation text (see createVariableText) String initialType = toLatex(
StringBuilder latex = new StringBuilder(getDefaultTextLatex(keyPrefix + "finalType1")). new LatexCreatorType(typeInferer.getFirstInferenceStep().getConclusion().getType(), mode).getLatex());
append(toLatex(letCounterToLatex(SIGMA))). String finalType = toLatex(new LatexCreatorType(typeInferer.getType().get(), mode).getLatex());
append(getDefaultTextLatex(keyPrefix + "finalType2")). String finalText = provider.getTranslation(keyPrefix + "finalType", locale, sigma, initialType, finalType);
append(toLatex(new LatexCreatorType(typeInferer.getFirstInferenceStep().getConclusion().getType(), mode) unificationTexts.add(finalText);
.getLatex())).
append(getDefaultTextLatex(keyPrefix + "finalType3")).
append(toLatex(new LatexCreatorType(typeInferer.getType().get(), mode).getLatex())).
append(getDefaultTextLatex(keyPrefix + "finalType4"));
unificationTexts.add(latex.toString());
} }
private void createMGU() { private void createMGU() {
StringBuilder latex = new StringBuilder(getDefaultTextLatex(KEY_PREFIX + "mgu1")). String sigma = toLatex(letCounterToLatex(SIGMA));
append(toLatex(letCounterToLatex(SIGMA))). String constraintSet = toLatex(letCounterToLatex(CONSTRAINT_SET));
append(getDefaultTextLatex(KEY_PREFIX + "mgu2")). String finalText = provider.getTranslation(KEY_PREFIX + "mgu", locale, sigma, constraintSet);
append(toLatex(letCounterToLatex(CONSTRAINT_SET))). unificationTexts.add(finalText);
append(getDefaultTextLatex(KEY_PREFIX + "mgu3"));
unificationTexts.add(latex.toString());
} }
private String getDefaultTextLatex(String textKey) { 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) // skip first step since the substitutions list is still empty (unification introduction is shown)
for (int stepNum = 1; stepNum < unificationSteps.size(); stepNum++) { for (int stepNum = 1; stepNum < unificationSteps.size(); stepNum++) {
UnificationStep step = unificationSteps.get(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<List<Substitution>, UnificationError> subs = step.getSubstitutions(); Result<List<Substitution>, UnificationError> subs = step.getSubstitutions();
if (subs.isError()) { if (subs.isError()) {
@ -219,31 +198,20 @@ public class ExplanationCreatorUnification {
} }
private void createTrivialConstraintText(Constraint currentConstraint) { private void createTrivialConstraintText(Constraint currentConstraint) {
StringBuilder latex = new StringBuilder(); String constraintLatex = toLatex(LatexCreatorConstraints.createSingleConstraint(currentConstraint, mode));
// TODO: replace with parametrized translation text (see createVariableText) String finalText = provider.getTranslation(KEY_PREFIX + "trivial", locale, constraintLatex);
latex.append(getDefaultTextLatex(KEY_PREFIX + "trivial1")). unificationTexts.add(finalText);
append(toLatex(LatexCreatorConstraints.createSingleConstraint(currentConstraint, mode))).
append(getDefaultTextLatex(KEY_PREFIX + "trivial2"));
unificationTexts.add(latex.toString());
} }
private void createFunctionText(Constraint currentConstraint, Constraint newConstraint1, Constraint newConstraint2) { private void createFunctionText(Constraint currentConstraint, Constraint newConstraint1, Constraint newConstraint2) {
StringBuilder latex = new StringBuilder(); String constraintLatex = toLatex(LatexCreatorConstraints.createSingleConstraint(currentConstraint, mode));
// TODO: replace with parametrized translation text (see createVariableText) String firstType = toLatex(new LatexCreatorType(currentConstraint.getFirstType(), mode).getLatex());
latex.append(getDefaultTextLatex(KEY_PREFIX + "function1")). String secondType = toLatex(new LatexCreatorType(currentConstraint.getSecondType(), mode).getLatex());
append(toLatex(LatexCreatorConstraints.createSingleConstraint(currentConstraint, mode))). String firstNewConstraint = toLatex(LatexCreatorConstraints.createSingleConstraint(newConstraint1, mode));
append(getDefaultTextLatex(KEY_PREFIX + "function2")). String secondNewConstraint = toLatex(LatexCreatorConstraints.createSingleConstraint(newConstraint2, mode));
append(toLatex(new LatexCreatorType(currentConstraint.getFirstType(), mode).getLatex())). String finalText = provider.getTranslation(KEY_PREFIX + "function", locale, constraintLatex, firstType,
append(getDefaultTextLatex(KEY_PREFIX + "function3")). secondType, firstNewConstraint, secondNewConstraint);
append(toLatex(new LatexCreatorType(currentConstraint.getSecondType(), mode).getLatex())). unificationTexts.add(finalText);
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());
} }
private void createVariableText(Type variable, Type anyType, Constraint currentConstraint, private void createVariableText(Type variable, Type anyType, Constraint currentConstraint,

2
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationTranslationProvider.java
View File

@ -6,6 +6,8 @@ import java.util.List;
import java.util.Locale; import java.util.Locale;
public class ExplanationTranslationProvider implements I18NProvider { public class ExplanationTranslationProvider implements I18NProvider {
private static final long serialVersionUID = 5240864819723940755L;
private final I18NProvider innerProvider; private final I18NProvider innerProvider;
public ExplanationTranslationProvider(I18NProvider provider) { public ExplanationTranslationProvider(I18NProvider provider) {

64
src/main/resources/language/translation_de.properties
View File

@ -245,50 +245,34 @@ explanationTree.letStep8=bestimmen. Da der Let-Ausdruck und der innere Term vom
Bedingung Bedingung
explanationTree.letStep9=der Constraintmenge hinzugefügt werden. 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. 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. 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.trivial=In diesem Schritt wurde der Constraint %0% entfernt. Da linke und rechte Seite identisch sind,\
expUnification.trivial2=entfernt. Da linke und rechte Seite identisch sind, ist der Constraint immer erfüllt und \ ist der Constraint immer erfüllt und wird somit nicht benötigt.
wird somit nicht benötigt.
expUnification.variable=In diesem Schritt wurde der Constraint %0% ersetzt.\ 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.\ 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.\ In der Folge wird die Substitution %3% erstellt und auf die übrige Constraintmenge angewandt.\
Die daraus resultierenden Veränderungen sind blau markiert. Die daraus resultierenden Veränderungen sind blau markiert.
expUnification.function1=In diesem Schritt wurde der Constraint expUnification.function=In diesem Schritt wurde der Constraint %0% ersetzt. Da sowohl %1% als auch %2% Funktionstypen\
expUnification.function2=ersetzt. Da sowohl sind, müssen die beiden Constraints %3% und %4% der Constraintmenge hinzugefügt werden. Der ursprüngliche Constraint\
expUnification.function3=als auch %0% wurde aus der Menge entfernt.
expUnification.function4=Funktionstypen sind, müssen die beiden Constraints expUnification.mgu=In diesem Schritt wird der allgemeinste Unifikator %0% der Constraintmenge %1% berechnet. Dafür wird\
expUnification.function5=und die gesamte Menge an Substitutionen auf jede einzelne der Substitutionen aus der Menge angewandt.
expUnification.function6=der Constraintmenge hinzugefügt werden. Der ursprüngliche Constraint expUnification.finalType=In diesem Schritt wird der zuvor berechnete allgemeinste Unifikator %0% auf den Typen %1%\
expUnification.function7=wurde aus der Menge entfernt. des eingegebenen Terms angewandt. Das Ergebnis %2% ist der finale Type des eingegebenen Terms.
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. \ 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. 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, \ expUnification.diffrentTypes=Da die Typen auf den beiden Seiten des hervorgehobenen Constraints nicht übereinstimmen, \
bricht die Unifikation hier ab. bricht die Unifikation hier ab.
expLetUnification.finalType1=In diesem Schritt wird der zuvor berechnete allgemeinste Unifikator expLetUnification.finalType=In diesem Schritt wird der zuvor berechnete allgemeinste Unifikator %0% auf den Typen %1%\
expLetUnification.finalType2=auf den Typen der Let-Definition angewandt. Das Ergebnis %2% ist der finale Typ der Let-Definition.
expLetUnification.finalType3=der Let-Definition angewandt. Das Ergebnis expLetUnification.typeAss=In diesem Schritt werden die Typannahmen %0% für die weitere Durchführung des Algorithmus\
expLetUnification.finalType4=ist der finale Typ der Let-Definition. berechnet. Im ersten Schritt wird dafür der MGU %1% der Let-Teilinferenz auf die aktuelle Menge von Typannahmen\
expLetUnification.typeAss1=In diesem Schritt werden die Typannahmen angewandt. Die dadurch entstandenen Typannahmen werden anschließend der Menge %0% hinzugefügt. Im zweiten Schritt\
expLetUnification.typeAss2=für die weitere Durchführung des Algorithmus berechnet. Im ersten Schritt wird dafür der MGU wird der Typ der let-Variable %2% berechnet. Dafür wird die Typabstraktion %3% zuerst instanziiert und dann gemeinsam\
expLetUnification.typeAss3=der Let-Teilinferenz auf die aktuelle Menge von Typannahmen angewandt. Die dadurch entstandenen \ mit der Variable %2% als Typannahme der Menge %0% hinzugefügt. Bei der Instanziierung werden alle Typvariablen, die frei\
Typannahmen werden anschließend der Menge in %4% aber nicht frei in %5% vorkommen allquantifiziert.
expLetUnification.typeAss4=hinzugefügt. Im zweiten Schritt wird der Typ der let-Variable expLetUnification.letStep1=Die Let-Teilinferenz ist jetzt abgeschlossen. Der Typinferenz-Algorithmus wird mit der um %0%\
expLetUnification.typeAss5=berechnet. Dafür wird Typabstraktion erweiterten Constraintmenge und den neu berechneten Typannahmen fortgeführt.
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.