From 6968a4b5f2c81fe5e402f657fd63bece4cbab544 Mon Sep 17 00:00:00 2001 From: Moritz Dieing <63721811+moritzdieing@users.noreply.github.com> Date: Mon, 9 Aug 2021 13:02:01 +0200 Subject: [PATCH] Add structure for unification texts --- .../latexcreator/ExplanationCreator.java | 241 ++++++++-------- .../ExplanationCreatorUnification.java | 272 ++++++++++++++++++ 2 files changed, 401 insertions(+), 112 deletions(-) create mode 100644 src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationCreatorUnification.java 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 e51a206..709ef05 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 @@ -1,12 +1,14 @@ package edu.kit.typicalc.view.content.typeinferencecontent.latexcreator; import java.util.ArrayList; -import java.util.HashMap; import java.util.List; import java.util.Locale; -import java.util.Map; +import java.util.Optional; import java.util.Queue; +import com.vaadin.flow.i18n.I18NProvider; + +import edu.kit.typicalc.model.TypeInfererInterface; import edu.kit.typicalc.model.step.AbsStep; import edu.kit.typicalc.model.step.AbsStepDefault; import edu.kit.typicalc.model.step.AbsStepWithLet; @@ -28,227 +30,242 @@ import edu.kit.typicalc.model.type.TypeArgumentVisitor; import edu.kit.typicalc.model.term.LambdaTerm; import edu.kit.typicalc.view.TypicalcI18NProvider; +import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.TEXT; +import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.CURLY_LEFT; +import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.CURLY_RIGHT; +import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.DOLLAR_SIGN; +import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.SPACE; + public class ExplanationCreator implements StepVisitor { - private final TypicalcI18NProvider provider = new TypicalcI18NProvider(); + private static final String KEY_PREFIX = "explanationTree."; + + private final I18NProvider provider = new TypicalcI18NProvider(); private final TermArgumentVisitor termArgumentVisitor = new TermArgumentVisitor(); private final TypeArgumentVisitor typeArgumentVisitor = new TypeArgumentVisitor(); + private final Locale locale; - private final Map> explanationTexts = new HashMap<>(); + private final List explanationTexts = new ArrayList<>(); private static final LatexCreatorMode MODE = LatexCreatorMode.MATHJAX; + private boolean errorOccurred; // true if one unification was not successful + private int letCounter = 0; // count number of lets for unification indices - public ExplanationCreator() { - provider.getProvidedLocales().forEach(l -> explanationTexts.put(l, new ArrayList())); + // creates explanation texts for a specific language + public ExplanationCreator(TypeInfererInterface typeInferer, Locale locale) { + this.locale = locale; + errorOccurred = false; + + explanationTexts.add(createInitialText(typeInferer)); + typeInferer.getFirstInferenceStep().accept(this); + if (!errorOccurred) { + explanationTexts.addAll(new ExplanationCreatorUnification(typeInferer, locale, provider, MODE, + letCounter, false, Optional.empty()).getUnificationsTexts().getLeft()); + } } - public Map> getExplanationTexts() { + public List getExplanationTexts() { return explanationTexts; } - - private String getDefaultTextLatex(String textKey, Locale locale) { - return new StringBuilder(LatexCreatorConstants.TEXT + LatexCreatorConstants.CURLY_LEFT). + + private String getDefaultTextLatex(String textKey) { + return new StringBuilder(TEXT + CURLY_LEFT). append(provider.getTranslation(textKey, locale)). - append(LatexCreatorConstants.CURLY_RIGHT) + append(CURLY_RIGHT) .toString(); } private String toLatex(String latex) { - return LatexCreatorConstants.DOLLAR_SIGN + latex + LatexCreatorConstants.DOLLAR_SIGN; + return SPACE + DOLLAR_SIGN + latex + DOLLAR_SIGN + SPACE; + } + + private String createInitialText(TypeInfererInterface typeInferer) { + 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(); } @Override public void visit(AbsStepDefault absD) { - provider.getProvidedLocales().forEach(l -> { - List texts = explanationTexts.get(l); - texts.add(createLatexAbsStep(absD, l)); - explanationTexts.put(l, texts); - }); + explanationTexts.add(createLatexAbsStep(absD)); absD.getPremise().accept(this); } @Override public void visit(AbsStepWithLet absL) { - provider.getProvidedLocales().forEach(l -> { - List texts = explanationTexts.get(l); - texts.add(createLatexAbsStep(absL, l)); - explanationTexts.put(l, texts); - }); + explanationTexts.add(createLatexAbsStep(absL)); absL.getPremise().accept(this); } - private String createLatexAbsStep(AbsStep abs, Locale locale) { + private String createLatexAbsStep(AbsStep abs) { Queue termArguments = termArgumentVisitor.getArguments(abs.getConclusion().getLambdaTerm()); Queue typeArguments = typeArgumentVisitor.getArguments(abs.getConstraint().getSecondType()); - return new StringBuilder(getDefaultTextLatex("key", locale)). + return new StringBuilder(getDefaultTextLatex(KEY_PREFIX + "absStep1")). append(toLatex(new LatexCreatorTerm(abs.getConclusion().getLambdaTerm(), MODE).getLatex())). - append(getDefaultTextLatex("key", locale)). + append(getDefaultTextLatex(KEY_PREFIX + "absStep2")). append(toLatex(new LatexCreatorType(abs.getConclusion().getType(), MODE).getLatex())). - append(getDefaultTextLatex("key", locale)). + append(getDefaultTextLatex(KEY_PREFIX + "absStep3")). append(toLatex(new LatexCreatorTerm(termArguments.poll(), MODE).getLatex())). - append(getDefaultTextLatex("key", locale)). + append(getDefaultTextLatex(KEY_PREFIX + "absStep4")). append(toLatex(new LatexCreatorTerm(termArguments.poll(), MODE).getLatex())). - append(getDefaultTextLatex("key", locale)). + append(getDefaultTextLatex(KEY_PREFIX + "absStep5")). append(toLatex(new LatexCreatorType(typeArguments.poll(), MODE).getLatex())). - append(getDefaultTextLatex("key", locale)). + append(getDefaultTextLatex(KEY_PREFIX + "absStep6")). append(toLatex(new LatexCreatorType(typeArguments.poll(), MODE).getLatex())). - append(getDefaultTextLatex("key", locale)). + append(getDefaultTextLatex(KEY_PREFIX + "absStep7")). append(toLatex(new LatexCreatorType(abs.getConstraint().getSecondType(), MODE).getLatex())). - append(getDefaultTextLatex("key", locale)). + append(getDefaultTextLatex(KEY_PREFIX + "absStep8")). append(toLatex(LatexCreatorConstraints.createSingleConstraint(abs.getConstraint(), MODE))). - append(getDefaultTextLatex("key", locale)). + append(getDefaultTextLatex(KEY_PREFIX + "absStep9")). toString(); } @Override public void visit(AppStepDefault appD) { - provider.getProvidedLocales().forEach(l -> { - List texts = explanationTexts.get(l); - texts.add(createLatexAppStep(appD, l)); - explanationTexts.put(l, texts); - }); + explanationTexts.add(createLatexAppStep(appD)); appD.getPremise1().accept(this); appD.getPremise2().accept(this); } - private String createLatexAppStep(AppStep app, Locale locale) { + private String createLatexAppStep(AppStep app) { Queue termArguments = termArgumentVisitor.getArguments(app.getConclusion().getLambdaTerm()); Queue typeArguments = typeArgumentVisitor.getArguments(app.getConstraint().getSecondType()); - return new StringBuilder(getDefaultTextLatex("key", locale)). + return new StringBuilder(getDefaultTextLatex(KEY_PREFIX + "appStep1")). append(toLatex(new LatexCreatorTerm(app.getConclusion().getLambdaTerm(), MODE).getLatex())). - append(getDefaultTextLatex("key", locale)). + append(getDefaultTextLatex(KEY_PREFIX + "appStep2")). append(toLatex(new LatexCreatorType(app.getConclusion().getType(), MODE).getLatex())). - append(getDefaultTextLatex("key", locale)). + append(getDefaultTextLatex(KEY_PREFIX + "appStep3")). append(toLatex(new LatexCreatorTerm(termArguments.poll(), MODE).getLatex())). - append(getDefaultTextLatex("key", locale)). + append(getDefaultTextLatex(KEY_PREFIX + "appStep4")). append(toLatex(new LatexCreatorTerm(termArguments.poll(), MODE).getLatex())). - append(getDefaultTextLatex("key", locale)). + append(getDefaultTextLatex(KEY_PREFIX + "appStep5")). append(toLatex(new LatexCreatorType(typeArguments.poll(), MODE).getLatex())). - append(getDefaultTextLatex("key", locale)). + append(getDefaultTextLatex(KEY_PREFIX + "appStep6")). append(toLatex(new LatexCreatorType(typeArguments.poll(), MODE).getLatex())). - append(getDefaultTextLatex("key", locale)). + append(getDefaultTextLatex(KEY_PREFIX + "appStep7")). append(toLatex(new LatexCreatorType(app.getConstraint().getSecondType(), MODE).getLatex())). - append(getDefaultTextLatex("key", locale)). + append(getDefaultTextLatex(KEY_PREFIX + "appStep8")). append(toLatex(LatexCreatorConstraints.createSingleConstraint(app.getConstraint(), MODE))). - append(getDefaultTextLatex("key", locale)). + append(getDefaultTextLatex(KEY_PREFIX + "appStep9")). toString(); } @Override public void visit(ConstStepDefault constD) { - provider.getProvidedLocales().forEach(l -> { - List texts = explanationTexts.get(l); - texts.add(createLatexConstStep(constD, l)); - explanationTexts.put(l, texts); - }); + explanationTexts.add(createLatexConstStep(constD)); } - private String createLatexConstStep(ConstStep constS, Locale locale) { + private String createLatexConstStep(ConstStep constS) { - return new StringBuilder(getDefaultTextLatex("key", locale)). + return new StringBuilder(getDefaultTextLatex(KEY_PREFIX + "constStep1")). append(toLatex(new LatexCreatorTerm(constS.getConclusion().getLambdaTerm(), MODE).getLatex())). - append(getDefaultTextLatex("key", locale)). + append(getDefaultTextLatex(KEY_PREFIX + "constStep2")). append(toLatex(new LatexCreatorTerm(constS.getConclusion().getLambdaTerm(), MODE).getLatex())). - append(getDefaultTextLatex("key", locale)). + append(getDefaultTextLatex(KEY_PREFIX + "constStep3")). append(toLatex(new LatexCreatorType(constS.getConclusion().getType(), MODE).getLatex())). - append(getDefaultTextLatex("key", locale)). + append(getDefaultTextLatex(KEY_PREFIX + "constStep4")). append(toLatex(new LatexCreatorTerm(constS.getConclusion().getLambdaTerm(), MODE).getLatex())). - append(getDefaultTextLatex("key", locale)). - append("$" + constS.getConclusion().getType() + "$"). - append(getDefaultTextLatex("key", locale)). + append(getDefaultTextLatex(KEY_PREFIX + "constStep5")). + append(toLatex(new LatexCreatorType(constS.getConclusion().getType(), MODE).getLatex())). + append(getDefaultTextLatex(KEY_PREFIX + "constStep6")). append(toLatex(LatexCreatorConstraints.createSingleConstraint(constS.getConstraint(), MODE))). - append(getDefaultTextLatex("key", locale)). + append(getDefaultTextLatex(KEY_PREFIX + "constStep7")). toString(); } @Override public void visit(VarStepDefault varD) { - provider.getProvidedLocales().forEach(l -> { - List texts = explanationTexts.get(l); - texts.add(createLatexVarStep(varD, l)); - explanationTexts.put(l, texts); - }); + explanationTexts.add(createLatexVarStep(varD)); } @Override public void visit(VarStepWithLet varL) { - provider.getProvidedLocales().forEach(l -> { - List texts = explanationTexts.get(l); - texts.add(createLatexVarStep(varL, l)); - explanationTexts.put(l, texts); - }); + explanationTexts.add(createLatexVarStep(varL)); // TODO: maybe create slightly different text } - private String createLatexVarStep(VarStep varS, Locale locale) { + private String createLatexVarStep(VarStep varS) { + String termLatex = new LatexCreatorTerm(varS.getConclusion().getLambdaTerm(), MODE).getLatex(); - return new StringBuilder(getDefaultTextLatex("key", locale)). - append(toLatex(new LatexCreatorTerm(varS.getConclusion().getLambdaTerm(), MODE).getLatex())). - append(getDefaultTextLatex("key", locale)). - append(toLatex(new LatexCreatorTerm(varS.getConclusion().getLambdaTerm(), MODE).getLatex())). - append(getDefaultTextLatex("key", locale)). + 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", locale)). - append(toLatex(new LatexCreatorTerm(varS.getConclusion().getLambdaTerm(), MODE).getLatex())). - append(getDefaultTextLatex("key", locale)). + 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", locale)). + append(getDefaultTextLatex(KEY_PREFIX + "varStep6")). append(toLatex(LatexCreatorConstraints.createSingleConstraint(varS.getConstraint(), MODE))). - append(getDefaultTextLatex("key", locale)). + append(getDefaultTextLatex(KEY_PREFIX + "varStep7")). toString(); } @Override public void visit(LetStepDefault letD) { - provider.getProvidedLocales().forEach(l -> { - List texts = explanationTexts.get(l); - texts.add(createLatexLetStep(letD, l)); - explanationTexts.put(l, texts); - }); - - letD.getPremise().accept(this); - } - - private String createLatexLetStep(LetStep letS, Locale locale) { - Queue termArguments = termArgumentVisitor.getArguments(letS.getConclusion().getLambdaTerm()); + Queue termArguments = termArgumentVisitor.getArguments(letD.getConclusion().getLambdaTerm()); LambdaTerm variable = termArguments.poll(); LambdaTerm innerTerm = termArguments.poll(); + LambdaTerm variableDefinition = termArguments.poll(); + letCounter++; + explanationTexts.add(createLatexLetStep(letD, variable, innerTerm, variableDefinition)); - return new StringBuilder(getDefaultTextLatex("key", locale)). + 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--; + + if (!errorOccurred) { + letD.getPremise().accept(this); + } + } + + private String createLatexLetStep(LetStep letS, LambdaTerm variable, LambdaTerm innerTerm, + LambdaTerm variableDefinition) { + + return new StringBuilder(getDefaultTextLatex(KEY_PREFIX + "letStep1")). append(toLatex(new LatexCreatorTerm(letS.getConclusion().getLambdaTerm(), MODE).getLatex())). - append(getDefaultTextLatex("key", locale)). + append(getDefaultTextLatex(KEY_PREFIX + "letStep2")). append(toLatex(new LatexCreatorType(letS.getConclusion().getType(), MODE).getLatex())). - append(getDefaultTextLatex("key", locale)). + append(getDefaultTextLatex(KEY_PREFIX + "letStep3")). append(toLatex(new LatexCreatorTerm(variable, MODE).getLatex())). - append(getDefaultTextLatex("key", locale)). - append(toLatex(new LatexCreatorTerm(termArguments.poll(), MODE).getLatex())). - append(getDefaultTextLatex("key", locale)). + 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", locale)). + 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", locale)). - append(toLatex(new LatexCreatorTerm(innerTerm, MODE).getLatex())). - append(getDefaultTextLatex("key", locale)). - append(toLatex(new LatexCreatorType(letS.getConstraint().getSecondType(), MODE).getLatex())). - append(getDefaultTextLatex("key", locale)). + append(getDefaultTextLatex(KEY_PREFIX + "letStep8")). append(toLatex(LatexCreatorConstraints.createSingleConstraint(letS.getConstraint(), MODE))). - append(getDefaultTextLatex("key", locale)). + append(getDefaultTextLatex(KEY_PREFIX + "letStep9")). toString(); } @Override - public void visit(EmptyStep empty) { - // TODO Auto-generated method stub - + public void visit(EmptyStep empty) { } @Override - public void visit(OnlyConclusionStep onlyConc) { - // TODO Auto-generated method stub - + public void visit(OnlyConclusionStep onlyConc) { } } 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 new file mode 100644 index 0000000..a1b59f9 --- /dev/null +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationCreatorUnification.java @@ -0,0 +1,272 @@ +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.AMPERSAND; +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; +import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.LATEX_NEW_LINE; +import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.SUBSTITUTION_SIGN; +import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.TYPE_ABSTRACTION; +import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.CURLY_LEFT; +import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.CURLY_RIGHT; +import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.LET; +import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.PAREN_LEFT; +import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.PAREN_RIGHT; +import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.UNDERSCORE; +import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.CONSTRAINT_SET; +import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.GAMMA; +import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.SIGMA; + +import java.util.ArrayList; +import java.util.List; +import java.util.Locale; +import java.util.Optional; +import java.util.Queue; + +import org.apache.commons.lang3.tuple.Pair; + +import com.vaadin.flow.i18n.I18NProvider; + +import edu.kit.typicalc.model.Constraint; +import edu.kit.typicalc.model.Substitution; +import edu.kit.typicalc.model.TypeInfererInterface; +import edu.kit.typicalc.model.UnificationError; +import edu.kit.typicalc.model.UnificationStep; +import edu.kit.typicalc.model.term.LambdaTerm; +import edu.kit.typicalc.model.type.Type; +import edu.kit.typicalc.model.type.TypeArgumentVisitor; +import edu.kit.typicalc.util.Result; + +public class ExplanationCreatorUnification { + + private final TypeArgumentVisitor typeDeterminer = new TypeArgumentVisitor(); + private final TypeInfererInterface typeInferer; + private final Locale locale; + private final I18NProvider provider; + private final LatexCreatorMode mode; + private final int letCounter; + private final Optional letVariable; + + private final List unificationTexts = new ArrayList<>(); + private boolean errorOccurred; + + public ExplanationCreatorUnification(TypeInfererInterface typeInferer, Locale locale, I18NProvider provider, + LatexCreatorMode mode, int letCounter, boolean isLetUnification, Optional letVariable) { + this.typeInferer = typeInferer; + this.locale = locale; + this.provider = provider; + this.mode = mode; + this.letCounter = letCounter; + this.letVariable = letVariable; + + buildTexts(isLetUnification); + } + + public Pair, Boolean> getUnificationsTexts() { + return Pair.of(unificationTexts, errorOccurred); + } + + private void buildTexts(boolean isLetUnification) { + String initialStepKey = isLetUnification ? "key1" : "key2"; + unificationTexts.add(getDefaultTextLatex(initialStepKey)); + createUnficationTexts(); + + if (!errorOccurred) { + createMGU(); + createFinalType(isLetUnification); + if (isLetUnification) { + createLetUnficiationFinish(); + } + } + } + + private void createLetUnficiationFinish() { + String typeAssumptions = + typeAssumptionsToLatex(typeInferer.getFirstInferenceStep().getConclusion().getTypeAssumptions(), mode); + String letVariableLatex = new LatexCreatorTerm(this.letVariable.get(), mode).getLatex(); + + StringBuilder latex = new StringBuilder(getDefaultTextLatex("key")). + append(toLatex(GAMMA)). + append(getDefaultTextLatex("key")). + append(toLatex(letCounterToLatex(SIGMA))). + append(toLatex(GAMMA)). + append(getDefaultTextLatex("key")). + append(toLatex(letVariableLatex)). + append(getDefaultTextLatex("key")). + append(toLatex(createTypeAbstraction(typeAssumptions))). + append(getDefaultTextLatex("key")). + append(toLatex(letVariableLatex)). + append(getDefaultTextLatex("key")). + append(toLatex(GAMMA)). + append(getDefaultTextLatex("key")). + append(new LatexCreatorType(typeInferer.getType().get(), mode).getLatex()). + append(getDefaultTextLatex("key")). + append(toLatex(letCounterToLatex(SIGMA) + PAREN_LEFT + typeAssumptions + "" + PAREN_RIGHT)). + append(getDefaultTextLatex("key")); + unificationTexts.add(latex.toString()); + + // add "second part" of let step here, so that the letCounterToLatex method can still be used + latex = new StringBuilder(getDefaultTextLatex("key")). + append(toLatex(letCounterToLatex(CONSTRAINT_SET))). + append(getDefaultTextLatex("key")); + unificationTexts.add(latex.toString()); + } + + private String createTypeAbstraction(String typeAssumptions) { + return new StringBuilder(TYPE_ABSTRACTION + PAREN_LEFT + letCounterToLatex(SIGMA)). + append(new LatexCreatorType(typeInferer.getFirstInferenceStep().getConclusion().getType(), mode) + .getLatex()). + append("" + PAREN_RIGHT + COMMA + letCounterToLatex(SIGMA) + PAREN_LEFT). + append(typeAssumptions). + append("" + PAREN_RIGHT + PAREN_RIGHT).toString(); + } + + private void createFinalType(boolean isLetUnification) { + String keyPrefix = isLetUnification ? "let" : ""; + + StringBuilder latex = new StringBuilder(getDefaultTextLatex(keyPrefix + "key")). + append(toLatex(letCounterToLatex(SIGMA))). + append(getDefaultTextLatex(keyPrefix + "key")). + append(toLatex(new LatexCreatorType(typeInferer.getFirstInferenceStep().getConclusion().getType(), mode) + .getLatex())). + append(getDefaultTextLatex(keyPrefix + "key")). + append(toLatex(new LatexCreatorType(typeInferer.getType().get(), mode).getLatex())). + append(getDefaultTextLatex(keyPrefix + "key")); + unificationTexts.add(latex.toString()); + } + + private void createMGU() { + StringBuilder latex = new StringBuilder(getDefaultTextLatex("key")). + append(toLatex(letCounterToLatex(SIGMA))). + append(getDefaultTextLatex("key")). + append(toLatex(letCounterToLatex(CONSTRAINT_SET))). + append(getDefaultTextLatex("key")); + unificationTexts.add(latex.toString()); + } + + private String getDefaultTextLatex(String textKey) { + return new StringBuilder(LatexCreatorConstants.TEXT + LatexCreatorConstants.CURLY_LEFT). + append(provider.getTranslation(textKey, locale)). + append(LatexCreatorConstants.CURLY_RIGHT) + .toString(); + } + + // WARNING: call toLatex() before to get proper latex code + private String letCounterToLatex(String setName) { + switch (letCounter) { + case 0: + return setName; + case 1: + return setName + UNDERSCORE + CURLY_LEFT + LET + CURLY_RIGHT; + default: + return setName + UNDERSCORE + CURLY_LEFT + LET + CURLY_LEFT + letCounter + + CURLY_RIGHT + CURLY_RIGHT; + } + } + + private String toLatex(String latex) { + return LatexCreatorConstants.DOLLAR_SIGN + latex + LatexCreatorConstants.DOLLAR_SIGN; + } + + private String getSubstitutionLatex(Substitution sub) { + return new StringBuilder(BRACKET_LEFT) + .append(AMPERSAND) + .append(new LatexCreatorType(sub.getVariable(), mode).getLatex()) + .append(SUBSTITUTION_SIGN) + .append(new LatexCreatorType(sub.getType(), mode).getLatex()) + .append(BRACKET_RIGHT) + .append(LATEX_NEW_LINE).toString(); + } + + private void createUnficationTexts() { + List unificationSteps = typeInferer.getUnificationSteps() + .orElseThrow(IllegalStateException::new); + + List initialConstraints = unificationSteps.get(0).getConstraints(); + // skip first step since the substitutions list is still empty (unification introduction is shown) + Constraint currentConstraint = initialConstraints.get(initialConstraints.size() - 1); + for (int stepNum = 1; stepNum < unificationSteps.size() - 1; stepNum++) { + UnificationStep step = unificationSteps.get(stepNum); + Result, UnificationError> subs = step.getSubstitutions(); + + if (subs.isError()) { + createErrorText(subs.unwrapError()); + errorOccurred = true; + break; + } + + List constraints = step.getConstraints(); + Queue leftTypeArgs = typeDeterminer.getArguments(currentConstraint.getFirstType()); + Queue rightTypeArgs = typeDeterminer.getArguments(currentConstraint.getSecondType()); + if (leftTypeArgs.isEmpty()) { + // left side is a variable + createVariableText(currentConstraint.getFirstType(), currentConstraint.getSecondType(), + currentConstraint, subs.unwrap().get(0)); + } else if (rightTypeArgs.isEmpty()) { + // right side is a variable + createVariableText(currentConstraint.getSecondType(), currentConstraint.getFirstType(), + currentConstraint, subs.unwrap().get(0)); + } else { + // both sides are functions + createFunctionText(leftTypeArgs, rightTypeArgs, currentConstraint, + constraints.get(constraints.size() - 1), constraints.get(constraints.size() - 2)); + } + + currentConstraint = constraints.get(constraints.size() - 1); + } + } + + private void createFunctionText(Queue leftTypeArgs, Queue rightTypeArgs, Constraint currentConstraint, + Constraint newConstraint1, Constraint newConstraint2) { + StringBuilder latex = new StringBuilder(); + latex.append(getDefaultTextLatex("key")). + append(toLatex(LatexCreatorConstraints.createSingleConstraint(currentConstraint, mode))). + append(getDefaultTextLatex("key")). + append(toLatex(new LatexCreatorType(currentConstraint.getFirstType(), mode).getLatex())). + append(getDefaultTextLatex("key")). + append(toLatex(new LatexCreatorType(currentConstraint.getSecondType(), mode).getLatex())). + append(getDefaultTextLatex("key")). + append(toLatex(new LatexCreatorType(leftTypeArgs.poll(), mode).getLatex())). + append(getDefaultTextLatex("key")). + append(toLatex(new LatexCreatorType(rightTypeArgs.poll(), mode).getLatex())). + append(getDefaultTextLatex("key")). + append(toLatex(new LatexCreatorType(leftTypeArgs.poll(), mode).getLatex())). + append(getDefaultTextLatex("key")). + append(toLatex(new LatexCreatorType(rightTypeArgs.poll(), mode).getLatex())). + append(getDefaultTextLatex("key")). + append(toLatex(LatexCreatorConstraints.createSingleConstraint(currentConstraint, mode))). + append(getDefaultTextLatex("key")). + append(toLatex(LatexCreatorConstraints.createSingleConstraint(newConstraint1, mode))). + append(getDefaultTextLatex("key")). + append(toLatex(LatexCreatorConstraints.createSingleConstraint(newConstraint2, mode))). + append(getDefaultTextLatex("key")).toString(); + unificationTexts.add(latex.toString()); + } + + private void createVariableText(Type variable, Type anyType, Constraint currentConstraint, + Substitution newSubstitution) { + StringBuilder latex = new StringBuilder(); + latex.append(getDefaultTextLatex("key")). + append(toLatex(LatexCreatorConstraints.createSingleConstraint(currentConstraint, mode))). + append(getDefaultTextLatex("key")). + append(toLatex(new LatexCreatorType(variable, mode).getLatex())). + append(getDefaultTextLatex("key")). + append(toLatex(new LatexCreatorType(variable, mode).getLatex())). + append(getDefaultTextLatex("key")). + append(toLatex(new LatexCreatorType(anyType, mode).getLatex())). + append(getDefaultTextLatex("key")). + append(toLatex(getSubstitutionLatex(newSubstitution))). + append(getDefaultTextLatex("key")); + unificationTexts.add(latex.toString()); + } + + private void createErrorText(UnificationError errorType) { + if (errorType == UnificationError.DIFFERENT_TYPES) { + unificationTexts.add(getDefaultTextLatex("key")); + } else if (errorType == UnificationError.INFINITE_TYPE) { + unificationTexts.add(getDefaultTextLatex("key")); + } + } + +}