From d721fb1c33dd4b47c57180d8c65d03246cbfd8c1 Mon Sep 17 00:00:00 2001 From: Moritz Dieing <63721811+moritzdieing@users.noreply.github.com> Date: Wed, 18 Aug 2021 14:28:19 +0200 Subject: [PATCH] Bug fixes and text changes --- .../latexcreator/ExplanationCreator.java | 2 +- .../ExplanationCreatorUnification.java | 19 +++++--- .../language/translation_de.properties | 44 +++++++++---------- 3 files changed, 35 insertions(+), 30 deletions(-) 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 0a2ce34..273bc41 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 @@ -171,7 +171,7 @@ public class ExplanationCreator implements StepVisitor { append(getDefaultTextLatex(KEY_PREFIX + "constStep4")). append(toLatex(new LatexCreatorTerm(constS.getConclusion().getLambdaTerm(), MODE).getLatex())). append(getDefaultTextLatex(KEY_PREFIX + "constStep5")). - append(toLatex(new LatexCreatorType(constS.getConclusion().getType(), MODE).getLatex())). + 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")). 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 0671dfc..d125cf7 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 @@ -1,6 +1,7 @@ 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.APOSTROPHE; 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; @@ -71,7 +72,11 @@ public class ExplanationCreatorUnification { private void buildTexts(boolean isLetUnification) { String initialPrefix = isLetUnification ? LET_KEY_PREFIX : KEY_PREFIX; - unificationTexts.add(getDefaultTextLatex(initialPrefix + "initial")); + String letVariable = isLetUnification + ? toLatex(new LatexCreatorTerm(this.letVariable.get(), mode).getLatex()) : ""; + String constraintSet = toLatex(letCounterToLatex(CONSTRAINT_SET)); + String finalText = provider.getTranslation(initialPrefix + "initial", locale, constraintSet, letVariable); + unificationTexts.add(finalText); createUnficationTexts(); if (!errorOccurred) { @@ -87,7 +92,7 @@ public class ExplanationCreatorUnification { String typeAssumptions = typeAssumptionsToLatex(typeInferer.getFirstInferenceStep().getConclusion().getTypeAssumptions(), mode); String letVariableLatex = toLatex(new LatexCreatorTerm(this.letVariable.get(), mode).getLatex()); - String gamma = toLatex(GAMMA); + String gamma = toLatex(GAMMA + APOSTROPHE); 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); @@ -103,7 +108,7 @@ public class ExplanationCreatorUnification { } private String createTypeAbstraction(String typeAssumptions) { - return new StringBuilder(TYPE_ABSTRACTION + PAREN_LEFT + letCounterToLatex(SIGMA)). + return new StringBuilder(TYPE_ABSTRACTION + PAREN_LEFT + letCounterToLatex(SIGMA) + PAREN_LEFT). append(new LatexCreatorType(typeInferer.getFirstInferenceStep().getConclusion().getType(), mode) .getLatex()). append("" + PAREN_RIGHT + COMMA + letCounterToLatex(SIGMA) + PAREN_LEFT). @@ -150,8 +155,8 @@ public class ExplanationCreatorUnification { } private String getSubstitutionLatex(Substitution sub) { - return new StringBuilder(BRACKET_LEFT) - //.append(AMPERSAND) + return new StringBuilder() + .append(BRACKET_LEFT) .append(new LatexCreatorType(sub.getVariable(), mode).getLatex()) .append(SUBSTITUTION_SIGN) .append(new LatexCreatorType(sub.getType(), mode).getLatex()) @@ -226,9 +231,9 @@ public class ExplanationCreatorUnification { } private void createErrorText(UnificationError errorType) { - if (errorType == UnificationError.DIFFERENT_TYPES) { + if (errorType == UnificationError.INFINITE_TYPE) { unificationTexts.add(getDefaultTextLatex(KEY_PREFIX + "infiniteType")); - } else if (errorType == UnificationError.INFINITE_TYPE) { + } else if (errorType == UnificationError.DIFFERENT_TYPES) { unificationTexts.add(getDefaultTextLatex(KEY_PREFIX + "differentTypes")); } } diff --git a/src/main/resources/language/translation_de.properties b/src/main/resources/language/translation_de.properties index 1a649fd..a9f2994 100644 --- a/src/main/resources/language/translation_de.properties +++ b/src/main/resources/language/translation_de.properties @@ -245,34 +245,34 @@ explanationTree.letStep8=bestimmen. Da der Let-Ausdruck und der innere Term vom Bedingung explanationTree.letStep9=der Constraintmenge hinzugefügt werden. -expUnification.initial=In den folgenden Schritten wird der Unifikationsalgorithmus auf der Constraintmenge ausgeführt, \ -um den Typen des eingegebenen Terms zu bestimmen. -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.trivial=In diesem Schritt wurde der Constraint %0% entfernt. Da linke und rechte Seite identisch sind,\ +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% \ + ausgeführt, um den Typen der let-Variable %1% zu bestimmen. +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.\ +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.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\ +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%\ +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 Substitution 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, \ +expUnification.differentTypes=Da die Typen auf den beiden Seiten des hervorgehobenen Constraints nicht übereinstimmen, \ bricht die Unifikation hier ab. -expLetUnification.finalType=In diesem Schritt wird der zuvor berechnete allgemeinste Unifikator %0% auf den Typen %1%\ +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%\ +expLetUnification.typeAss=In diesem Schritt werden die Typannahmen %0% für die weitere Durchführung des Algorithmus \ + berechnet. Im ersten Schritt wird dafür %1% 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.letStep=Die Let-Teilinferenz ist jetzt abgeschlossen. Der Typinferenz-Algorithmus wird mit der um %0% \ erweiterten Constraintmenge und den neu berechneten Typannahmen fortgeführt.