mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-08 18:30:42 +00:00
Add structure for unification texts
This commit is contained in:
Moritz Dieing
parent
69479a6368
commit
6968a4b5f2
@ -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<Locale, List<String>> explanationTexts = new HashMap<>();
|
||||
private final List<String> 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<String>()));
|
||||
// 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<Locale, List<String>> getExplanationTexts() {
|
||||
public List<String> 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<String> 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<String> 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<LambdaTerm> termArguments = termArgumentVisitor.getArguments(abs.getConclusion().getLambdaTerm());
|
||||
Queue<Type> 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<String> 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<LambdaTerm> termArguments = termArgumentVisitor.getArguments(app.getConclusion().getLambdaTerm());
|
||||
Queue<Type> 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<String> 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<String> 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<String> 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<String> 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<LambdaTerm> termArguments = termArgumentVisitor.getArguments(letS.getConclusion().getLambdaTerm());
|
||||
Queue<LambdaTerm> 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) {
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
@ -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<LambdaTerm> letVariable;
|
||||
|
||||
private final List<String> unificationTexts = new ArrayList<>();
|
||||
private boolean errorOccurred;
|
||||
|
||||
public ExplanationCreatorUnification(TypeInfererInterface typeInferer, Locale locale, I18NProvider provider,
|
||||
LatexCreatorMode mode, int letCounter, boolean isLetUnification, Optional<LambdaTerm> letVariable) {
|
||||
this.typeInferer = typeInferer;
|
||||
this.locale = locale;
|
||||
this.provider = provider;
|
||||
this.mode = mode;
|
||||
this.letCounter = letCounter;
|
||||
this.letVariable = letVariable;
|
||||
|
||||
buildTexts(isLetUnification);
|
||||
}
|
||||
|
||||
public Pair<List<String>, 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<UnificationStep> unificationSteps = typeInferer.getUnificationSteps()
|
||||
.orElseThrow(IllegalStateException::new);
|
||||
|
||||
List<Constraint> 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<List<Substitution>, UnificationError> subs = step.getSubstitutions();
|
||||
|
||||
if (subs.isError()) {
|
||||
createErrorText(subs.unwrapError());
|
||||
errorOccurred = true;
|
||||
break;
|
||||
}
|
||||
|
||||
List<Constraint> constraints = step.getConstraints();
|
||||
Queue<Type> leftTypeArgs = typeDeterminer.getArguments(currentConstraint.getFirstType());
|
||||
Queue<Type> 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<Type> leftTypeArgs, Queue<Type> 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"));
|
||||
}
|
||||
}
|
||||
|
||||
}
|
||||
Loading…
Reference in New Issue
Block a user