From f1554d602ac5fd186fe697703d78a8e85dcc09ff Mon Sep 17 00:00:00 2001 From: ucrhh Date: Sun, 31 Jan 2021 18:10:07 +0100 Subject: [PATCH] move LatexCreator constants into seperate class --- .../typicalc/model/TypeInferenceResult.java | 2 +- .../typeinferencecontent/LatexCreator.java | 48 ++----------------- .../LatexCreatorConstants.java | 45 +++++++++++++++++ .../LatexCreatorTerm.java | 27 ++++++----- 4 files changed, 67 insertions(+), 55 deletions(-) create mode 100644 src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreatorConstants.java diff --git a/src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java b/src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java index b8e878b..9c08fcc 100644 --- a/src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java +++ b/src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java @@ -29,7 +29,7 @@ public class TypeInferenceResult { protected TypeInferenceResult(List substitutions, TypeVariable typeVar) { mgu = new ArrayList<>(substitutions); findMGU(); - MGU.sort(Comparator.comparingInt((Substitution o) -> + mgu.sort(Comparator.comparingInt((Substitution o) -> o.getVariable().getIndex()).thenComparing(o -> o.getVariable().getKind())); finalType = findFinalType(typeVar); } diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreator.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreator.java index a35d5a4..0df9c96 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreator.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreator.java @@ -9,6 +9,8 @@ import edu.kit.typicalc.model.type.*; import java.util.Map; +import static edu.kit.typicalc.view.content.typeinferencecontent.LatexCreatorConstants.*; + /** * Generates LaTeX-code from a TypeInfererInterface object. Two mostly independent pie- * ces of code are generated, one for the constraints/unification and one for the proof tree. @@ -18,47 +20,6 @@ import java.util.Map; */ public class LatexCreator implements StepVisitor, TypeVisitor { - private static final String CONST = "Const"; - - private static final String NEW_LINE = System.lineSeparator(); - private static final String SPACE = " "; - private static final String EQUAL_SIGN = "="; - private static final String DOLLAR_SIGN = "$"; - private static final String DOT_SIGN = "."; - private static final String COLON = ":"; - private static final String CURLY_LEFT = "{"; - private static final String CURLY_RIGHT = "}"; - private static final String UNDERSCORE = "_"; - private static final String PAREN_LEFT = "("; - private static final String PAREN_RIGHT = ")"; - - private static final String LABEL_ABS = "\\LeftLabel{ABS}"; - private static final String LABEL_APP = "\\LeftLabel{APP}"; - private static final String LABEL_CONST = "\\LeftLabel{CONST}"; - private static final String LABEL_VAR = "\\LeftLabel{VAR}"; - private static final String LABEL_LET = "\\LeftLabel{LET}"; - - private static final String UIC = "\\UnaryInfC"; - private static final String BIC = "\\BinaryInfC"; - private static final String AXC = "\\AxiomC"; - - private static final String TREE_VARIABLE = "\\alpha"; - private static final String GENERATED_ASSUMPTION_VARIABLE = "\\beta"; - private static final String USER_VARIABLE = "\\tau"; - private static final String GAMMA = "\\Gamma"; - - private static final String LAMBDA = "\\lambda"; - private static final String LATEX_SPACE = "\\ "; - private static final String TEXTTT = "\\texttt"; - private static final String RIGHT_ARROW = "\\rightarrow"; - private static final String INSTANTIATE_SIGN = "\\succeq"; - private static final String LATEX_IN = "\\in"; - private static final String VDASH = "\\vdash"; - private static final String TREE_BEGIN = "\\begin{prooftree}"; - private static final String TREE_END = "\\end{prooftree}"; - - - private final TypeInfererInterface typeInferer; private final StringBuilder tree; private final boolean stepLabels; @@ -93,7 +54,7 @@ public class LatexCreator implements StepVisitor, TypeVisitor { */ protected String getTree() { typeInferer.getFirstInferenceStep().accept(this); - return TREE_BEGIN + tree.toString() + TREE_END; + return TREE_BEGIN + NEW_LINE + tree.toString() + TREE_END; } /** @@ -123,7 +84,8 @@ public class LatexCreator implements StepVisitor, TypeVisitor { private String conclusionToLatex(Conclusion conclusion) { String typeAssumptions = typeAssumptionsToLatex(conclusion.getTypeAssumptions()); String term = new LatexCreatorTerm(conclusion.getLambdaTerm()).getLatex(); - String type = " \\tau_{42}"; + conclusion.getType().accept(this); + String type = visitorBuffer; return DOLLAR_SIGN + GAMMA + VDASH + term + COLON + type + DOLLAR_SIGN; } diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreatorConstants.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreatorConstants.java new file mode 100644 index 0000000..be86ded --- /dev/null +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreatorConstants.java @@ -0,0 +1,45 @@ +package edu.kit.typicalc.view.content.typeinferencecontent; + +public final class LatexCreatorConstants { + private LatexCreatorConstants() { + } + + protected static final String CONST = "Const"; + + protected static final String NEW_LINE = System.lineSeparator(); + protected static final String SPACE = " "; + protected static final String DOLLAR_SIGN = "$"; + protected static final String EQUAL_SIGN = "="; + protected static final String DOT_SIGN = "."; + protected static final String COLON = ":"; + protected static final String UNDERSCORE = "_"; + protected static final String CURLY_LEFT = "{"; + protected static final String CURLY_RIGHT = "}"; + protected static final String PAREN_LEFT = "("; + protected static final String PAREN_RIGHT = ")"; + + protected static final String LABEL_ABS = "\\LeftLabel{ABS}"; + protected static final String LABEL_APP = "\\LeftLabel{APP}"; + protected static final String LABEL_CONST = "\\LeftLabel{CONST}"; + protected static final String LABEL_VAR = "\\LeftLabel{VAR}"; + protected static final String LABEL_LET = "\\LeftLabel{LET}"; + + protected static final String UIC = "\\UnaryInfC"; + protected static final String BIC = "\\BinaryInfC"; + protected static final String AXC = "\\AxiomC"; + + protected static final String TREE_VARIABLE = "\\alpha"; + protected static final String GENERATED_ASSUMPTION_VARIABLE = "\\beta"; + protected static final String USER_VARIABLE = "\\tau"; + protected static final String GAMMA = "\\Gamma"; + + protected static final String LAMBDA = "\\lambda"; + protected static final String LATEX_SPACE = "\\ "; + protected static final String TEXTTT = "\\texttt"; + protected static final String RIGHT_ARROW = "\\rightarrow"; + protected static final String INSTANTIATE_SIGN = "\\succeq"; + protected static final String LATEX_IN = "\\in"; + protected static final String VDASH = "\\vdash"; + protected static final String TREE_BEGIN = "\\begin{prooftree}"; + protected static final String TREE_END = "\\end{prooftree}"; +} diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreatorTerm.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreatorTerm.java index 3fe9f1e..a9ffadd 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreatorTerm.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreatorTerm.java @@ -8,15 +8,10 @@ import edu.kit.typicalc.model.term.LetTerm; import edu.kit.typicalc.model.term.TermVisitor; import edu.kit.typicalc.model.term.VarTerm; +import static edu.kit.typicalc.view.content.typeinferencecontent.LatexCreatorConstants.*; + public class LatexCreatorTerm implements TermVisitor { // TODO: document - private static final String PAREN_LEFT = "("; - private static final String PAREN_RIGHT = ")"; - private static final String LATEX_SPACE = "\\ "; - private static final String LAMBDA = "\\lambda"; - private static final String CURLY_LEFT = "{"; - private static final String CURLY_RIGHT = "}"; - private static final String TEXTTT = "\\texttt"; private final StringBuilder latex; private boolean needsParentheses = false; @@ -27,6 +22,11 @@ public class LatexCreatorTerm implements TermVisitor { } public String getLatex() { + // remove most outer parentheses if they exist +// if (latex.indexOf(PAREN_LEFT) == 0 && latex.indexOf(PAREN_RIGHT) == latex.length() - 1) { +// latex.deleteCharAt(latex.length() - 1); +// latex.deleteCharAt(0); +// } return latex.toString(); } @@ -34,32 +34,37 @@ public class LatexCreatorTerm implements TermVisitor { public void visit(AppTerm appTerm) { appTerm.getFunction().accept(this); latex.append(LATEX_SPACE); + latex.append(PAREN_LEFT); + int index = latex.length() - 1; appTerm.getParameter().accept(this); if (needsParentheses) { - latex.insert(0, PAREN_LEFT); latex.append(PAREN_RIGHT); + } else { + latex.deleteCharAt(index); } needsParentheses = true; } @Override public void visit(AbsTerm absTerm) { + latex.append(PAREN_LEFT); latex.append(LAMBDA); - latex.append(' '); + latex.append(SPACE); absTerm.getVariable().accept(this); - latex.append('.'); + latex.append(DOT_SIGN); latex.append(LATEX_SPACE); absTerm.getInner().accept(this); + latex.append(PAREN_RIGHT); needsParentheses = false; } @Override public void visit(VarTerm varTerm) { - needsParentheses = false; latex.append(TEXTTT); latex.append(CURLY_LEFT); latex.append(varTerm.getName()); latex.append(CURLY_RIGHT); + needsParentheses = false; } @Override