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

Actually fix exception thrown by last example

Browse Source
This commit is contained in:
Moritz Dieing 2021-09-29 17:11:37 +02:00
parent 49adac2a88
commit 8db0436975
2 changed files with 12 additions and 19 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationCreator.java
View File

@ -193,13 +193,16 @@ public class ExplanationCreator implements StepVisitor {
explanationTexts.add(createLatexLetStep(letD, variable, innerTerm, variableDefinition));
letD.getTypeInferer().getFirstInferenceStep().accept(this);
ExplanationCreatorUnification unification =
new ExplanationCreatorUnification(letD.getTypeInferer(), locale, provider, MODE, letCounter, true,
Optional.of(variable));
explanationTexts.addAll(unification.getUnificationsTexts().getLeft());
errorOccurred = unification.getUnificationsTexts().getRight();
letCounter--;
// skip creation of unification texts if nested let produced an error
if (!errorOccurred) {
ExplanationCreatorUnification unification =
new ExplanationCreatorUnification(letD.getTypeInferer(), locale, provider, MODE, letCounter, true,
Optional.of(variable));
explanationTexts.addAll(unification.getUnificationsTexts().getLeft());
errorOccurred = unification.getUnificationsTexts().getRight();
letCounter--;
}
if (!errorOccurred) {
letD.getPremise().accept(this);
}

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

@ -105,8 +105,6 @@ public class ExplanationCreatorUnification {
if (isLetUnification) {
createLetUnficiationFinish();
}
} else if (isLetUnification) {
unificationTexts.remove(unificationTexts.size() - 1);
}
}
@ -159,7 +157,6 @@ public class ExplanationCreatorUnification {
return provider.getTranslation(textKey, locale);
}
// WARNING: call toLatex() before to get proper latex code
private String letCounterToLatex(String setName) {
switch (letCounter) {
case 0:
@ -187,13 +184,8 @@ public class ExplanationCreatorUnification {
}
private void createUnficationTexts() {
List<UnificationStep> unificationSteps;
if (typeInferer.getUnificationSteps().isPresent()) {
unificationSteps = typeInferer.getUnificationSteps().get();
} else {
errorOccurred = true;
return;
}
List<UnificationStep> unificationSteps = typeInferer.getUnificationSteps()
.orElseThrow(IllegalStateException::new);
// skip first step since the substitutions list is still empty (unification introduction is shown)
for (int stepNum = 1; stepNum < unificationSteps.size(); stepNum++) {
@ -258,10 +250,8 @@ public class ExplanationCreatorUnification {
private void createErrorText(UnificationError errorType) {
if (errorType == UnificationError.INFINITE_TYPE) {
unificationTexts.add(getDefaultTextLatex(KEY_PREFIX + "infiniteType"));
unificationTexts.add(getDefaultTextLatex(KEY_PREFIX + "infiniteType"));
} else if (errorType == UnificationError.DIFFERENT_TYPES) {
unificationTexts.add(getDefaultTextLatex(KEY_PREFIX + "differentTypes"));
unificationTexts.add(getDefaultTextLatex(KEY_PREFIX + "differentTypes"));
}
}