From c6d80d9324e6ea8eff8ac762880d6457c0788274 Mon Sep 17 00:00:00 2001 From: Moritz Dieing <63721811+moritzdieing@users.noreply.github.com> Date: Sat, 24 Jul 2021 11:38:24 +0200 Subject: [PATCH] Implement structure for explanation texts --- .../model/term/TermArgumentVisitor.java | 55 ++++ .../model/type/TypeArgumentVisitor.java | 34 +++ .../latexcreator/ExplanationCreator.java | 254 ++++++++++++++++++ 3 files changed, 343 insertions(+) create mode 100644 src/main/java/edu/kit/typicalc/model/term/TermArgumentVisitor.java create mode 100644 src/main/java/edu/kit/typicalc/model/type/TypeArgumentVisitor.java create mode 100644 src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationCreator.java diff --git a/src/main/java/edu/kit/typicalc/model/term/TermArgumentVisitor.java b/src/main/java/edu/kit/typicalc/model/term/TermArgumentVisitor.java new file mode 100644 index 0000000..fa4941a --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/term/TermArgumentVisitor.java @@ -0,0 +1,55 @@ +package edu.kit.typicalc.model.term; + +import java.util.LinkedList; +import java.util.Queue; + +public class TermArgumentVisitor implements TermVisitor { + + private final Queue argumentList = new LinkedList<>(); + + public Queue getArguments(LambdaTerm term) { + term.accept(this); + return argumentList; + } + + @Override + public void visit(AppTerm appTerm) { + argumentList.clear(); + argumentList.add(appTerm.getFunction()); + argumentList.add(appTerm.getParameter()); + } + + @Override + public void visit(AbsTerm absTerm) { + argumentList.clear(); + argumentList.add(absTerm.getVariable()); + argumentList.add(absTerm.getInner()); + } + + @Override + public void visit(LetTerm letTerm) { + argumentList.clear(); + argumentList.add(letTerm.getVariable()); + argumentList.add(letTerm.getInner()); + argumentList.add(letTerm.getVariableDefinition()); + } + + @Override + public void visit(VarTerm varTerm) { + argumentList.clear(); + // no implementation since the VarTerm is its argument + } + + @Override + public void visit(IntegerTerm intTerm) { + argumentList.clear(); + // no implementation since the IntegerTerm is its argument + } + + @Override + public void visit(BooleanTerm boolTerm) { + argumentList.clear(); + // no implementation since the BooleanTerm is its argument + } + +} diff --git a/src/main/java/edu/kit/typicalc/model/type/TypeArgumentVisitor.java b/src/main/java/edu/kit/typicalc/model/type/TypeArgumentVisitor.java new file mode 100644 index 0000000..0cd40de --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/type/TypeArgumentVisitor.java @@ -0,0 +1,34 @@ +package edu.kit.typicalc.model.type; + +import java.util.LinkedList; +import java.util.Queue; + +public class TypeArgumentVisitor implements TypeVisitor { + + private final Queue argumentList = new LinkedList<>(); + + public Queue getArguments(Type type) { + type.accept(this); + return argumentList; + } + + @Override + public void visit(NamedType named) { + argumentList.clear(); + // no implementation since the NamedType is its argument + } + + @Override + public void visit(TypeVariable variable) { + argumentList.clear(); + // no implementation since the TypeVariable is its argument + } + + @Override + public void visit(FunctionType function) { + argumentList.clear(); + argumentList.add(function.getParameter()); + argumentList.add(function.getOutput()); + } + +} 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 new file mode 100644 index 0000000..e51a206 --- /dev/null +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationCreator.java @@ -0,0 +1,254 @@ +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.Queue; + +import edu.kit.typicalc.model.step.AbsStep; +import edu.kit.typicalc.model.step.AbsStepDefault; +import edu.kit.typicalc.model.step.AbsStepWithLet; +import edu.kit.typicalc.model.step.AppStep; +import edu.kit.typicalc.model.step.AppStepDefault; +import edu.kit.typicalc.model.step.ConstStep; +import edu.kit.typicalc.model.step.ConstStepDefault; +import edu.kit.typicalc.model.step.EmptyStep; +import edu.kit.typicalc.model.step.LetStep; +import edu.kit.typicalc.model.step.LetStepDefault; +import edu.kit.typicalc.model.step.OnlyConclusionStep; +import edu.kit.typicalc.model.step.StepVisitor; +import edu.kit.typicalc.model.step.VarStep; +import edu.kit.typicalc.model.step.VarStepDefault; +import edu.kit.typicalc.model.step.VarStepWithLet; +import edu.kit.typicalc.model.term.TermArgumentVisitor; +import edu.kit.typicalc.model.type.Type; +import edu.kit.typicalc.model.type.TypeArgumentVisitor; +import edu.kit.typicalc.model.term.LambdaTerm; +import edu.kit.typicalc.view.TypicalcI18NProvider; + +public class ExplanationCreator implements StepVisitor { + private final TypicalcI18NProvider provider = new TypicalcI18NProvider(); + private final TermArgumentVisitor termArgumentVisitor = new TermArgumentVisitor(); + private final TypeArgumentVisitor typeArgumentVisitor = new TypeArgumentVisitor(); + + private final Map> explanationTexts = new HashMap<>(); + + private static final LatexCreatorMode MODE = LatexCreatorMode.MATHJAX; + + public ExplanationCreator() { + provider.getProvidedLocales().forEach(l -> explanationTexts.put(l, new ArrayList())); + } + + public Map> getExplanationTexts() { + return explanationTexts; + } + + private String getDefaultTextLatex(String textKey, Locale locale) { + return new StringBuilder(LatexCreatorConstants.TEXT + LatexCreatorConstants.CURLY_LEFT). + append(provider.getTranslation(textKey, locale)). + append(LatexCreatorConstants.CURLY_RIGHT) + .toString(); + } + + private String toLatex(String latex) { + return LatexCreatorConstants.DOLLAR_SIGN + latex + LatexCreatorConstants.DOLLAR_SIGN; + } + + @Override + public void visit(AbsStepDefault absD) { + provider.getProvidedLocales().forEach(l -> { + List texts = explanationTexts.get(l); + texts.add(createLatexAbsStep(absD, l)); + explanationTexts.put(l, texts); + }); + 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); + }); + absL.getPremise().accept(this); + } + + private String createLatexAbsStep(AbsStep abs, Locale locale) { + Queue termArguments = termArgumentVisitor.getArguments(abs.getConclusion().getLambdaTerm()); + Queue typeArguments = typeArgumentVisitor.getArguments(abs.getConstraint().getSecondType()); + + return new StringBuilder(getDefaultTextLatex("key", locale)). + append(toLatex(new LatexCreatorTerm(abs.getConclusion().getLambdaTerm(), MODE).getLatex())). + append(getDefaultTextLatex("key", locale)). + append(toLatex(new LatexCreatorType(abs.getConclusion().getType(), MODE).getLatex())). + append(getDefaultTextLatex("key", locale)). + append(toLatex(new LatexCreatorTerm(termArguments.poll(), MODE).getLatex())). + append(getDefaultTextLatex("key", locale)). + append(toLatex(new LatexCreatorTerm(termArguments.poll(), MODE).getLatex())). + append(getDefaultTextLatex("key", locale)). + append(toLatex(new LatexCreatorType(typeArguments.poll(), MODE).getLatex())). + append(getDefaultTextLatex("key", locale)). + append(toLatex(new LatexCreatorType(typeArguments.poll(), MODE).getLatex())). + append(getDefaultTextLatex("key", locale)). + append(toLatex(new LatexCreatorType(abs.getConstraint().getSecondType(), MODE).getLatex())). + append(getDefaultTextLatex("key", locale)). + append(toLatex(LatexCreatorConstraints.createSingleConstraint(abs.getConstraint(), MODE))). + append(getDefaultTextLatex("key", locale)). + 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); + }); + appD.getPremise1().accept(this); + appD.getPremise2().accept(this); + } + + private String createLatexAppStep(AppStep app, Locale locale) { + Queue termArguments = termArgumentVisitor.getArguments(app.getConclusion().getLambdaTerm()); + Queue typeArguments = typeArgumentVisitor.getArguments(app.getConstraint().getSecondType()); + + return new StringBuilder(getDefaultTextLatex("key", locale)). + append(toLatex(new LatexCreatorTerm(app.getConclusion().getLambdaTerm(), MODE).getLatex())). + append(getDefaultTextLatex("key", locale)). + append(toLatex(new LatexCreatorType(app.getConclusion().getType(), MODE).getLatex())). + append(getDefaultTextLatex("key", locale)). + append(toLatex(new LatexCreatorTerm(termArguments.poll(), MODE).getLatex())). + append(getDefaultTextLatex("key", locale)). + append(toLatex(new LatexCreatorTerm(termArguments.poll(), MODE).getLatex())). + append(getDefaultTextLatex("key", locale)). + append(toLatex(new LatexCreatorType(typeArguments.poll(), MODE).getLatex())). + append(getDefaultTextLatex("key", locale)). + append(toLatex(new LatexCreatorType(typeArguments.poll(), MODE).getLatex())). + append(getDefaultTextLatex("key", locale)). + append(toLatex(new LatexCreatorType(app.getConstraint().getSecondType(), MODE).getLatex())). + append(getDefaultTextLatex("key", locale)). + append(toLatex(LatexCreatorConstraints.createSingleConstraint(app.getConstraint(), MODE))). + append(getDefaultTextLatex("key", locale)). + 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); + }); + } + + private String createLatexConstStep(ConstStep constS, Locale locale) { + + return new StringBuilder(getDefaultTextLatex("key", locale)). + append(toLatex(new LatexCreatorTerm(constS.getConclusion().getLambdaTerm(), MODE).getLatex())). + append(getDefaultTextLatex("key", locale)). + append(toLatex(new LatexCreatorTerm(constS.getConclusion().getLambdaTerm(), MODE).getLatex())). + append(getDefaultTextLatex("key", locale)). + append(toLatex(new LatexCreatorType(constS.getConclusion().getType(), MODE).getLatex())). + append(getDefaultTextLatex("key", locale)). + append(toLatex(new LatexCreatorTerm(constS.getConclusion().getLambdaTerm(), MODE).getLatex())). + append(getDefaultTextLatex("key", locale)). + append("$" + constS.getConclusion().getType() + "$"). + append(getDefaultTextLatex("key", locale)). + append(toLatex(LatexCreatorConstraints.createSingleConstraint(constS.getConstraint(), MODE))). + append(getDefaultTextLatex("key", locale)). + 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); + }); + } + + @Override + public void visit(VarStepWithLet varL) { + provider.getProvidedLocales().forEach(l -> { + List texts = explanationTexts.get(l); + texts.add(createLatexVarStep(varL, l)); + explanationTexts.put(l, texts); + }); + // TODO: maybe create slightly different text + } + + private String createLatexVarStep(VarStep varS, Locale locale) { + + 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)). + 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(toLatex(new LatexCreatorType(varS.getConstraint().getSecondType(), MODE).getLatex())). + append(getDefaultTextLatex("key", locale)). + append(toLatex(LatexCreatorConstraints.createSingleConstraint(varS.getConstraint(), MODE))). + append(getDefaultTextLatex("key", locale)). + 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()); + LambdaTerm variable = termArguments.poll(); + LambdaTerm innerTerm = termArguments.poll(); + + return new StringBuilder(getDefaultTextLatex("key", locale)). + append(toLatex(new LatexCreatorTerm(letS.getConclusion().getLambdaTerm(), MODE).getLatex())). + append(getDefaultTextLatex("key", locale)). + append(toLatex(new LatexCreatorType(letS.getConclusion().getType(), MODE).getLatex())). + append(getDefaultTextLatex("key", locale)). + append(toLatex(new LatexCreatorTerm(variable, MODE).getLatex())). + append(getDefaultTextLatex("key", locale)). + append(toLatex(new LatexCreatorTerm(termArguments.poll(), MODE).getLatex())). + append(getDefaultTextLatex("key", locale)). + append(toLatex(new LatexCreatorTerm(innerTerm, MODE).getLatex())). + append(getDefaultTextLatex("key", locale)). + 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(toLatex(LatexCreatorConstraints.createSingleConstraint(letS.getConstraint(), MODE))). + append(getDefaultTextLatex("key", locale)). + toString(); + } + + + @Override + public void visit(EmptyStep empty) { + // TODO Auto-generated method stub + + } + + @Override + public void visit(OnlyConclusionStep onlyConc) { + // TODO Auto-generated method stub + + } + +}