mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-08 18:30:42 +00:00
parent
70ce558cd0
commit
41479483f2
@ -25,7 +25,7 @@ public final class AssumptionGeneratorUtil {
|
|||||||
} else {
|
} else {
|
||||||
StringBuilder assumptions = new StringBuilder();
|
StringBuilder assumptions = new StringBuilder();
|
||||||
typeAssumptions.forEach(((varTerm, typeAbstraction) -> {
|
typeAssumptions.forEach(((varTerm, typeAbstraction) -> {
|
||||||
String termLatex = new LatexCreatorTerm(varTerm).getLatex();
|
String termLatex = new LatexCreatorTerm(varTerm, mode).getLatex();
|
||||||
String abstraction = generateTypeAbstraction(typeAbstraction, mode);
|
String abstraction = generateTypeAbstraction(typeAbstraction, mode);
|
||||||
assumptions.append(termLatex)
|
assumptions.append(termLatex)
|
||||||
.append(COLON)
|
.append(COLON)
|
||||||
|
@ -85,7 +85,7 @@ public class LatexCreator implements StepVisitor {
|
|||||||
|
|
||||||
private String conclusionToLatex(Conclusion conclusion) {
|
private String conclusionToLatex(Conclusion conclusion) {
|
||||||
String typeAssumptions = typeAssumptionsToLatex(conclusion.getTypeAssumptions(), mode);
|
String typeAssumptions = typeAssumptionsToLatex(conclusion.getTypeAssumptions(), mode);
|
||||||
String term = new LatexCreatorTerm(conclusion.getLambdaTerm()).getLatex();
|
String term = new LatexCreatorTerm(conclusion.getLambdaTerm(), mode).getLatex();
|
||||||
String type = new LatexCreatorType(conclusion.getType()).getLatex(mode);
|
String type = new LatexCreatorType(conclusion.getType()).getLatex(mode);
|
||||||
return DOLLAR_SIGN + typeAssumptions + VDASH + term + COLON + type + DOLLAR_SIGN;
|
return DOLLAR_SIGN + typeAssumptions + VDASH + term + COLON + type + DOLLAR_SIGN;
|
||||||
}
|
}
|
||||||
@ -105,7 +105,7 @@ public class LatexCreator implements StepVisitor {
|
|||||||
|
|
||||||
private String generateVarStepPremise(VarStep var) {
|
private String generateVarStepPremise(VarStep var) {
|
||||||
String assumptions = typeAssumptionsToLatex(var.getConclusion().getTypeAssumptions(), mode);
|
String assumptions = typeAssumptionsToLatex(var.getConclusion().getTypeAssumptions(), mode);
|
||||||
String term = new LatexCreatorTerm(var.getConclusion().getLambdaTerm()).getLatex();
|
String term = new LatexCreatorTerm(var.getConclusion().getLambdaTerm(), mode).getLatex();
|
||||||
String type = generateTypeAbstraction(var.getTypeAbsInPremise(), mode);
|
String type = generateTypeAbstraction(var.getTypeAbsInPremise(), mode);
|
||||||
return PAREN_LEFT + assumptions + PAREN_RIGHT + PAREN_LEFT + term
|
return PAREN_LEFT + assumptions + PAREN_RIGHT + PAREN_LEFT + term
|
||||||
+ PAREN_RIGHT + EQUALS + type;
|
+ PAREN_RIGHT + EQUALS + type;
|
||||||
@ -134,7 +134,7 @@ public class LatexCreator implements StepVisitor {
|
|||||||
@Override
|
@Override
|
||||||
public void visit(ConstStepDefault constD) {
|
public void visit(ConstStepDefault constD) {
|
||||||
tree.insert(0, generateConclusion(constD, LABEL_CONST, UIC));
|
tree.insert(0, generateConclusion(constD, LABEL_CONST, UIC));
|
||||||
String visitorBuffer = new LatexCreatorTerm(constD.getConclusion().getLambdaTerm()).getLatex();
|
String visitorBuffer = new LatexCreatorTerm(constD.getConclusion().getLambdaTerm(), mode).getLatex();
|
||||||
String step = AXC + CURLY_LEFT + DOLLAR_SIGN + visitorBuffer + SPACE + LATEX_IN + SPACE + CONST
|
String step = AXC + CURLY_LEFT + DOLLAR_SIGN + visitorBuffer + SPACE + LATEX_IN + SPACE + CONST
|
||||||
+ DOLLAR_SIGN + CURLY_RIGHT + NEW_LINE;
|
+ DOLLAR_SIGN + CURLY_RIGHT + NEW_LINE;
|
||||||
tree.insert(0, step);
|
tree.insert(0, step);
|
||||||
|
@ -409,7 +409,7 @@ public class LatexCreatorConstraints implements StepVisitor {
|
|||||||
latex.append(PAREN_LEFT);
|
latex.append(PAREN_LEFT);
|
||||||
latex.append(typeAssumptions);
|
latex.append(typeAssumptions);
|
||||||
latex.append("" + PAREN_RIGHT + COMMA + LATEX_SPACE);
|
latex.append("" + PAREN_RIGHT + COMMA + LATEX_SPACE);
|
||||||
latex.append(new LatexCreatorTerm(letVariable.orElseThrow(IllegalStateException::new)).getLatex());
|
latex.append(new LatexCreatorTerm(letVariable.orElseThrow(IllegalStateException::new), mode).getLatex());
|
||||||
latex.append("" + COLON + TYPE_ABSTRACTION + PAREN_LEFT + SIGMA);
|
latex.append("" + COLON + TYPE_ABSTRACTION + PAREN_LEFT + SIGMA);
|
||||||
latex.append(constraintSetIndex);
|
latex.append(constraintSetIndex);
|
||||||
latex.append(PAREN_LEFT);
|
latex.append(PAREN_LEFT);
|
||||||
|
@ -11,8 +11,8 @@ import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.La
|
|||||||
* @see LambdaTerm
|
* @see LambdaTerm
|
||||||
*/
|
*/
|
||||||
public class LatexCreatorTerm implements TermVisitor {
|
public class LatexCreatorTerm implements TermVisitor {
|
||||||
|
|
||||||
private final StringBuilder latex = new StringBuilder();
|
private final StringBuilder latex = new StringBuilder();
|
||||||
|
private final LatexCreatorMode mode;
|
||||||
|
|
||||||
private enum ParenthesesNeeded {
|
private enum ParenthesesNeeded {
|
||||||
NEVER,
|
NEVER,
|
||||||
@ -27,7 +27,8 @@ public class LatexCreatorTerm implements TermVisitor {
|
|||||||
*
|
*
|
||||||
* @param lambdaTerm the term to convert into LaTeX
|
* @param lambdaTerm the term to convert into LaTeX
|
||||||
*/
|
*/
|
||||||
protected LatexCreatorTerm(LambdaTerm lambdaTerm) {
|
protected LatexCreatorTerm(LambdaTerm lambdaTerm, LatexCreatorMode mode) {
|
||||||
|
this.mode = mode;
|
||||||
lambdaTerm.accept(this);
|
lambdaTerm.accept(this);
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -78,10 +79,18 @@ public class LatexCreatorTerm implements TermVisitor {
|
|||||||
|
|
||||||
@Override
|
@Override
|
||||||
public void visit(VarTerm varTerm) {
|
public void visit(VarTerm varTerm) {
|
||||||
|
if (mode == LatexCreatorMode.MATHJAX) {
|
||||||
|
latex.append("\\class{typicalc-type typicalc-type-v-");
|
||||||
|
latex.append(varTerm.hashCode());
|
||||||
|
latex.append("}{");
|
||||||
|
}
|
||||||
latex.append(MONO_TEXT);
|
latex.append(MONO_TEXT);
|
||||||
latex.append(CURLY_LEFT);
|
latex.append(CURLY_LEFT);
|
||||||
latex.append(varTerm.getName());
|
latex.append(varTerm.getName());
|
||||||
latex.append(CURLY_RIGHT);
|
latex.append(CURLY_RIGHT);
|
||||||
|
if (mode == LatexCreatorMode.MATHJAX) {
|
||||||
|
latex.append("}");
|
||||||
|
}
|
||||||
needsParentheses = ParenthesesNeeded.NEVER;
|
needsParentheses = ParenthesesNeeded.NEVER;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -20,35 +20,40 @@ class LatexCreatorTermTest {
|
|||||||
typeInferer = model.getTypeInferer("λx.y", new HashMap<>()).unwrap();
|
typeInferer = model.getTypeInferer("λx.y", new HashMap<>()).unwrap();
|
||||||
assertEquals(LAMBDA + SPACE + MONO_TEXT + "{x}" + DOT_SIGN
|
assertEquals(LAMBDA + SPACE + MONO_TEXT + "{x}" + DOT_SIGN
|
||||||
+ LATEX_SPACE + MONO_TEXT + "{y}",
|
+ LATEX_SPACE + MONO_TEXT + "{y}",
|
||||||
new LatexCreatorTerm(typeInferer.getFirstInferenceStep().getConclusion().getLambdaTerm()).getLatex());
|
new LatexCreatorTerm(typeInferer.getFirstInferenceStep().getConclusion().getLambdaTerm(),
|
||||||
|
LatexCreatorMode.NORMAL).getLatex());
|
||||||
}
|
}
|
||||||
|
|
||||||
@Test
|
@Test
|
||||||
void appTest() {
|
void appTest() {
|
||||||
typeInferer = model.getTypeInferer("x y", new HashMap<>()).unwrap();
|
typeInferer = model.getTypeInferer("x y", new HashMap<>()).unwrap();
|
||||||
assertEquals(MONO_TEXT + "{x}" + LATEX_SPACE + MONO_TEXT + "{y}",
|
assertEquals(MONO_TEXT + "{x}" + LATEX_SPACE + MONO_TEXT + "{y}",
|
||||||
new LatexCreatorTerm(typeInferer.getFirstInferenceStep().getConclusion().getLambdaTerm()).getLatex());
|
new LatexCreatorTerm(typeInferer.getFirstInferenceStep().getConclusion().getLambdaTerm(),
|
||||||
|
LatexCreatorMode.NORMAL).getLatex());
|
||||||
}
|
}
|
||||||
|
|
||||||
@Test
|
@Test
|
||||||
void varTest() {
|
void varTest() {
|
||||||
typeInferer = model.getTypeInferer("x", new HashMap<>()).unwrap();
|
typeInferer = model.getTypeInferer("x", new HashMap<>()).unwrap();
|
||||||
assertEquals(MONO_TEXT + "{x}",
|
assertEquals(MONO_TEXT + "{x}",
|
||||||
new LatexCreatorTerm(typeInferer.getFirstInferenceStep().getConclusion().getLambdaTerm()).getLatex());
|
new LatexCreatorTerm(typeInferer.getFirstInferenceStep().getConclusion().getLambdaTerm(),
|
||||||
|
LatexCreatorMode.NORMAL).getLatex());
|
||||||
}
|
}
|
||||||
|
|
||||||
@Test
|
@Test
|
||||||
void integerTest() {
|
void integerTest() {
|
||||||
typeInferer = model.getTypeInferer("5", new HashMap<>()).unwrap();
|
typeInferer = model.getTypeInferer("5", new HashMap<>()).unwrap();
|
||||||
assertEquals(MONO_TEXT + "{5}",
|
assertEquals(MONO_TEXT + "{5}",
|
||||||
new LatexCreatorTerm(typeInferer.getFirstInferenceStep().getConclusion().getLambdaTerm()).getLatex());
|
new LatexCreatorTerm(typeInferer.getFirstInferenceStep().getConclusion().getLambdaTerm(),
|
||||||
|
LatexCreatorMode.NORMAL).getLatex());
|
||||||
}
|
}
|
||||||
|
|
||||||
@Test
|
@Test
|
||||||
void booleanTest() {
|
void booleanTest() {
|
||||||
typeInferer = model.getTypeInferer("true", new HashMap<>()).unwrap();
|
typeInferer = model.getTypeInferer("true", new HashMap<>()).unwrap();
|
||||||
assertEquals(MONO_TEXT + "{true}",
|
assertEquals(MONO_TEXT + "{true}",
|
||||||
new LatexCreatorTerm(typeInferer.getFirstInferenceStep().getConclusion().getLambdaTerm()).getLatex());
|
new LatexCreatorTerm(typeInferer.getFirstInferenceStep().getConclusion().getLambdaTerm(),
|
||||||
|
LatexCreatorMode.NORMAL).getLatex());
|
||||||
}
|
}
|
||||||
|
|
||||||
@Test
|
@Test
|
||||||
@ -57,7 +62,8 @@ class LatexCreatorTermTest {
|
|||||||
assertEquals(MONO_TEXT + CURLY_LEFT + BOLD_TEXT + "{let}" + CURLY_RIGHT + LATEX_SPACE + MONO_TEXT + "{f}"
|
assertEquals(MONO_TEXT + CURLY_LEFT + BOLD_TEXT + "{let}" + CURLY_RIGHT + LATEX_SPACE + MONO_TEXT + "{f}"
|
||||||
+ EQUALS + MONO_TEXT + "{x}" + LATEX_SPACE + MONO_TEXT + CURLY_LEFT + BOLD_TEXT + "{in}"
|
+ EQUALS + MONO_TEXT + "{x}" + LATEX_SPACE + MONO_TEXT + CURLY_LEFT + BOLD_TEXT + "{in}"
|
||||||
+ CURLY_RIGHT + LATEX_SPACE + MONO_TEXT + "{f}",
|
+ CURLY_RIGHT + LATEX_SPACE + MONO_TEXT + "{f}",
|
||||||
new LatexCreatorTerm(typeInferer.getFirstInferenceStep().getConclusion().getLambdaTerm()).getLatex());
|
new LatexCreatorTerm(typeInferer.getFirstInferenceStep().getConclusion().getLambdaTerm(),
|
||||||
|
LatexCreatorMode.NORMAL).getLatex());
|
||||||
}
|
}
|
||||||
|
|
||||||
@Test
|
@Test
|
||||||
@ -65,7 +71,8 @@ class LatexCreatorTermTest {
|
|||||||
typeInferer = model.getTypeInferer("x (y z)", new HashMap<>()).unwrap();
|
typeInferer = model.getTypeInferer("x (y z)", new HashMap<>()).unwrap();
|
||||||
assertEquals(MONO_TEXT + "{x}" + LATEX_SPACE + PAREN_LEFT + MONO_TEXT + "{y}"
|
assertEquals(MONO_TEXT + "{x}" + LATEX_SPACE + PAREN_LEFT + MONO_TEXT + "{y}"
|
||||||
+ LATEX_SPACE + MONO_TEXT + "{z}" + PAREN_RIGHT,
|
+ LATEX_SPACE + MONO_TEXT + "{z}" + PAREN_RIGHT,
|
||||||
new LatexCreatorTerm(typeInferer.getFirstInferenceStep().getConclusion().getLambdaTerm()).getLatex());
|
new LatexCreatorTerm(typeInferer.getFirstInferenceStep().getConclusion().getLambdaTerm(),
|
||||||
|
LatexCreatorMode.NORMAL).getLatex());
|
||||||
}
|
}
|
||||||
|
|
||||||
}
|
}
|
||||||
|
Loading…
Reference in New Issue
Block a user