arnekeller/Typicalc
1
0
Fork 0
mirror of https://gitlab.kit.edu/uskyk/typicalc.git synced 2024-11-08 18:30:42 +00:00
Code Issues Packages Projects Releases Wiki Activity

Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc

Browse Source
This commit is contained in:
Johanna Stuber 2021-01-31 21:16:57 +01:00
commit 784d04992e
3 changed files with 66 additions and 54 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

48
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreator.java
View File

@ -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;
}

45
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreatorConstants.java Normal file
View File

@ -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}";
}

27
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreatorTerm.java
View File

@ -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