mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-08 18:30:42 +00:00
Bug fixes and text changes
This commit is contained in:
Moritz Dieing
parent
8cc089e543
commit
d721fb1c33
@ -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")).
|
||||
|
||||
@ -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"));
|
||||
}
|
||||
}
|
||||
|
||||
@ -245,10 +245,10 @@ 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, \
|
||||
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 \
|
||||
ausgeführt, um den Typen der let-Variable zu finden und damit die neue Typumgebung 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. \
|
||||
@ -259,20 +259,20 @@ expUnification.function=In diesem Schritt wurde der Constraint %0% ersetzt. Da s
|
||||
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.
|
||||
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% \
|
||||
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%\
|
||||
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.
|
||||
|
||||
Loading…
Reference in New Issue
Block a user