From 8dd5753ee05b33382dae49cc44a67245d910d39e Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Mon, 5 Jul 2021 09:17:37 +0200 Subject: [PATCH] Highlight each type variable separately --- .../latexcreator/AssumptionGeneratorUtil.java | 4 +-- .../latexcreator/LatexCreator.java | 4 +-- .../latexcreator/LatexCreatorConstraints.java | 26 ++++++++-------- .../latexcreator/LatexCreatorType.java | 31 ++++++++++++++----- .../edu/kit/typicalc/model/ModelImplTest.java | 1 - .../latexcreator/LatexCreatorTypeTest.java | 8 ++--- 6 files changed, 44 insertions(+), 30 deletions(-) diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/AssumptionGeneratorUtil.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/AssumptionGeneratorUtil.java index 7fc45d4..ad0a6dd 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/AssumptionGeneratorUtil.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/AssumptionGeneratorUtil.java @@ -42,13 +42,13 @@ public final class AssumptionGeneratorUtil { if (abs.hasQuantifiedVariables()) { abstraction.append(FOR_ALL); abs.getQuantifiedVariables().forEach(typeVariable -> { - String variableTex = new LatexCreatorType(typeVariable).getLatex(mode); + String variableTex = new LatexCreatorType(typeVariable, mode).getLatex(); abstraction.append(variableTex).append(COMMA); }); abstraction.deleteCharAt(abstraction.length() - 1); abstraction.append(DOT_SIGN); } - abstraction.append(new LatexCreatorType(abs.getInnerType()).getLatex(mode)); + abstraction.append(new LatexCreatorType(abs.getInnerType(), mode).getLatex()); return abstraction.toString(); } } diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreator.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreator.java index a07c6e5..397fc11 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreator.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreator.java @@ -86,7 +86,7 @@ public class LatexCreator implements StepVisitor { private String conclusionToLatex(Conclusion conclusion) { String typeAssumptions = typeAssumptionsToLatex(conclusion.getTypeAssumptions(), mode); String term = new LatexCreatorTerm(conclusion.getLambdaTerm(), mode).getLatex(); - String type = new LatexCreatorType(conclusion.getType()).getLatex(mode); + String type = new LatexCreatorType(conclusion.getType(), mode).getLatex(); return DOLLAR_SIGN + typeAssumptions + VDASH + term + COLON + type + DOLLAR_SIGN; } @@ -163,7 +163,7 @@ public class LatexCreator implements StepVisitor { mode == LatexCreatorMode.MATHJAX ? LABEL_VAR_WITH_CLASS : LABEL_VAR, // TODO: differentiate with let UIC)); String typeAbstraction = generateTypeAbstraction(varL.getTypeAbsInPremise(), mode); - String instantiatedType = new LatexCreatorType(varL.getInstantiatedTypeAbs()).getLatex(mode); + String instantiatedType = new LatexCreatorType(varL.getInstantiatedTypeAbs(), mode).getLatex(); String premiseRight = typeAbstraction + INSTANTIATE_SIGN + instantiatedType; String premiseLeft = AXC + CURLY_LEFT + DOLLAR_SIGN + ALIGN_BEGIN + generateVarStepPremise(varL) diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstraints.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstraints.java index d3e3b55..5c98b0e 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstraints.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstraints.java @@ -133,8 +133,8 @@ public class LatexCreatorConstraints implements StepVisitor { } private String createSingleConstraint(Constraint constraint) { - String firstType = new LatexCreatorType(constraint.getFirstType()).getLatex(mode); - String secondType = new LatexCreatorType(constraint.getSecondType()).getLatex(mode); + String firstType = new LatexCreatorType(constraint.getFirstType(), mode).getLatex(); + String secondType = new LatexCreatorType(constraint.getSecondType(), mode).getLatex(); return firstType + EQUALS + secondType; } @@ -297,9 +297,9 @@ public class LatexCreatorConstraints implements StepVisitor { sb.append(CURLY_LEFT); sb.append(COLOR_HIGHLIGHTED); } - sb.append(new LatexCreatorType(unificationConstraints.get(i).getFirstType()).getLatex(mode)); + sb.append(new LatexCreatorType(unificationConstraints.get(i).getFirstType(), mode).getLatex()); sb.append(EQUALS); - sb.append(new LatexCreatorType(unificationConstraints.get(i).getSecondType()).getLatex(mode)); + sb.append(new LatexCreatorType(unificationConstraints.get(i).getSecondType(), mode).getLatex()); if ((markError && i == 0) || markLastTwoConstraints && (i < 2)) { sb.append(CURLY_RIGHT); } @@ -310,12 +310,12 @@ public class LatexCreatorConstraints implements StepVisitor { // perform the substitution "manually" and color the new type Substitution s = substitutions.get(substitutions.size() - 1); String original = previousConstraints[invIdx]; - String originalType = new LatexCreatorType(s.getVariable()).getLatex(mode); + String originalType = new LatexCreatorType(s.getVariable(), mode).getLatex(); if (original.contains(originalType)) { StringBuilder highlightedChange2 = new StringBuilder(); highlightedChange2.append(CURLY_LEFT); highlightedChange2.append(COLOR_HIGHLIGHTED); - highlightedChange2.append(new LatexCreatorType(s.getType()).getLatex(mode)); + highlightedChange2.append(new LatexCreatorType(s.getType(), mode).getLatex()); highlightedChange2.append(CURLY_RIGHT); latex.append(original.replace(originalType, highlightedChange2.toString())); } else { @@ -341,9 +341,9 @@ public class LatexCreatorConstraints implements StepVisitor { } latex.append(BRACKET_LEFT); latex.append(AMPERSAND); - latex.append(new LatexCreatorType(substitutions.get(i).getVariable()).getLatex(mode)); + latex.append(new LatexCreatorType(substitutions.get(i).getVariable(), mode).getLatex()); latex.append(SUBSTITUTION_SIGN); - latex.append(new LatexCreatorType(substitutions.get(i).getType()).getLatex(mode)); + latex.append(new LatexCreatorType(substitutions.get(i).getType(), mode).getLatex()); latex.append(BRACKET_RIGHT); latex.append(LATEX_NEW_LINE); } @@ -368,9 +368,9 @@ public class LatexCreatorConstraints implements StepVisitor { latex.append(BRACKET_LEFT); typeInferer.getMGU().ifPresent(mgu -> mgu.forEach(substitution -> { latex.append(AMPERSAND); - latex.append(new LatexCreatorType(substitution.getVariable()).getLatex(mode)); + latex.append(new LatexCreatorType(substitution.getVariable(), mode).getLatex()); latex.append(SUBSTITUTION_SIGN); - latex.append(new LatexCreatorType(substitution.getType()).getLatex(mode)); + latex.append(new LatexCreatorType(substitution.getType(), mode).getLatex()); latex.append(COMMA); latex.append(LATEX_NEW_LINE); })); @@ -387,10 +387,10 @@ public class LatexCreatorConstraints implements StepVisitor { latex.append(constraintSetIndex); latex.append(PAREN_LEFT); latex.append( - new LatexCreatorType(typeInferer.getFirstInferenceStep().getConclusion().getType()).getLatex(mode)); + new LatexCreatorType(typeInferer.getFirstInferenceStep().getConclusion().getType(), mode).getLatex()); latex.append("" + PAREN_RIGHT + EQUALS); latex.append( - new LatexCreatorType(typeInferer.getType().orElseThrow(IllegalStateException::new)).getLatex(mode)); + new LatexCreatorType(typeInferer.getType().orElseThrow(IllegalStateException::new), mode).getLatex()); return latex.toString(); } @@ -414,7 +414,7 @@ public class LatexCreatorConstraints implements StepVisitor { latex.append(constraintSetIndex); latex.append(PAREN_LEFT); latex.append( - new LatexCreatorType(typeInferer.getFirstInferenceStep().getConclusion().getType()).getLatex(mode) + new LatexCreatorType(typeInferer.getFirstInferenceStep().getConclusion().getType(), mode).getLatex() ); latex.append("" + PAREN_RIGHT + COMMA + SIGMA); latex.append(constraintSetIndex); diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorType.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorType.java index 26883af..03c180a 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorType.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorType.java @@ -17,6 +17,7 @@ import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.La public class LatexCreatorType implements TypeVisitor { private final Type type; private static final int MAX_LENGTH = 100000; // 100 KB + private final LatexCreatorMode mode; private final StringBuilder latex = new StringBuilder(); private boolean needsParentheses = false; @@ -26,28 +27,33 @@ public class LatexCreatorType implements TypeVisitor { * * @param type the type */ - protected LatexCreatorType(Type type) { + protected LatexCreatorType(Type type, LatexCreatorMode mode) { this.type = type; + this.mode = mode; type.accept(this); } /** * @return the generated LaTeX code */ - protected String getLatex(LatexCreatorMode mode) { - if (mode == LatexCreatorMode.MATHJAX) { - // this class is used in frontend/src/mathjax-setup.js - return "\\class{typicalc-type typicalc-type-" + type.hashCode() + "}{" + latex + "}"; - } else { - return latex.toString(); - } + protected String getLatex() { + return latex.toString(); } @Override public void visit(NamedType named) { latex.append(MONO_TEXT); latex.append(CURLY_LEFT); + if (mode == LatexCreatorMode.MATHJAX) { + // this class is used in frontend/src/mathjax-setup.js + latex.append("\\class{typicalc-type typicalc-type-") + .append(named.hashCode()) + .append("}{"); + } latex.append(named.getName()); + if (mode == LatexCreatorMode.MATHJAX) { + latex.append(CURLY_RIGHT); + } latex.append(CURLY_RIGHT); needsParentheses = false; } @@ -68,10 +74,19 @@ public class LatexCreatorType implements TypeVisitor { default: throw new IllegalStateException("unreachable code"); } + if (mode == LatexCreatorMode.MATHJAX) { + // this class is used in frontend/src/mathjax-setup.js + latex.append("\\class{typicalc-type typicalc-type-") + .append(variable.hashCode()) + .append("}{"); + } latex.append(name); latex.append(UNDERSCORE); latex.append(CURLY_LEFT); latex.append(variable.getIndex()); + if (mode == LatexCreatorMode.MATHJAX) { + latex.append(CURLY_RIGHT); + } latex.append(CURLY_RIGHT); needsParentheses = false; } diff --git a/src/test/java/edu/kit/typicalc/model/ModelImplTest.java b/src/test/java/edu/kit/typicalc/model/ModelImplTest.java index 75a1f3e..90b7e5b 100644 --- a/src/test/java/edu/kit/typicalc/model/ModelImplTest.java +++ b/src/test/java/edu/kit/typicalc/model/ModelImplTest.java @@ -1,7 +1,6 @@ package edu.kit.typicalc.model; import edu.kit.typicalc.model.parser.ParseError; -import edu.kit.typicalc.model.parser.TypeAssumptionParser; import edu.kit.typicalc.model.step.AbsStepDefault; import edu.kit.typicalc.model.step.VarStepDefault; import edu.kit.typicalc.model.term.AbsTerm; diff --git a/src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorTypeTest.java b/src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorTypeTest.java index a5acbc9..70badf1 100644 --- a/src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorTypeTest.java +++ b/src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorTypeTest.java @@ -19,21 +19,21 @@ class LatexCreatorTypeTest { void identityTest() { typeInferer = model.getTypeInferer("λx.x", new HashMap<>()).unwrap(); assertEquals(TREE_VARIABLE + "_{2} " + RIGHT_ARROW + SPACE + TREE_VARIABLE + "_{2}", - new LatexCreatorType(typeInferer.getType().get()).getLatex(LatexCreatorMode.NORMAL)); + new LatexCreatorType(typeInferer.getType().get(), LatexCreatorMode.NORMAL).getLatex()); } @Test void generatedTypeTest() { typeInferer = model.getTypeInferer("x", new HashMap<>()).unwrap(); assertEquals(GENERATED_ASSUMPTION_VARIABLE + "_{1}", - new LatexCreatorType(typeInferer.getType().get()).getLatex(LatexCreatorMode.NORMAL)); + new LatexCreatorType(typeInferer.getType().get(), LatexCreatorMode.NORMAL).getLatex()); } @Test void namedTypeTest() { typeInferer = model.getTypeInferer("5", new HashMap<>()).unwrap(); assertEquals(MONO_TEXT + "{int}", - new LatexCreatorType(typeInferer.getType().get()).getLatex(LatexCreatorMode.NORMAL)); + new LatexCreatorType(typeInferer.getType().get(), LatexCreatorMode.NORMAL).getLatex()); } @Test @@ -42,6 +42,6 @@ class LatexCreatorTypeTest { map.put("x", "t1"); typeInferer = model.getTypeInferer("x", map).unwrap(); assertEquals(USER_VARIABLE + "_{1}", - new LatexCreatorType(typeInferer.getType().get()).getLatex(LatexCreatorMode.NORMAL)); + new LatexCreatorType(typeInferer.getType().get(), LatexCreatorMode.NORMAL).getLatex()); } }