mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-08 18:30:42 +00:00
fix some todos
This commit is contained in:
parent
a8652642fc
commit
6128871223
@ -69,11 +69,11 @@ public class LatexCreator implements StepVisitor {
|
||||
/**
|
||||
* Returns needed LaTeX packages
|
||||
*
|
||||
* @return the packages needed for the LaTeX-code from getTree() and getUnification() to work
|
||||
* @return the packages needed for the LaTeX-code from getTree() to work
|
||||
*/
|
||||
public String getLatexPackages() {
|
||||
return BUSSPROOFS;
|
||||
} // todo implement
|
||||
}
|
||||
|
||||
|
||||
|
||||
@ -120,8 +120,8 @@ public class LatexCreator implements StepVisitor {
|
||||
String assumptions = typeAssumptionsToLatex(var.getConclusion().getTypeAssumptions());
|
||||
String term = new LatexCreatorTerm(var.getConclusion().getLambdaTerm()).getLatex();
|
||||
String type = generateTypeAbstraction(var.getTypeAbsInPremise());
|
||||
return DOLLAR_SIGN + PAREN_LEFT + assumptions + PAREN_RIGHT + PAREN_LEFT + term
|
||||
+ PAREN_RIGHT + EQUALS + type + DOLLAR_SIGN;
|
||||
return PAREN_LEFT + assumptions + PAREN_RIGHT + PAREN_LEFT + term
|
||||
+ PAREN_RIGHT + EQUALS + type;
|
||||
}
|
||||
|
||||
private String generateTypeAbstraction(TypeAbstraction abs) {
|
||||
@ -171,7 +171,8 @@ public class LatexCreator implements StepVisitor {
|
||||
@Override
|
||||
public void visit(VarStepDefault varD) {
|
||||
tree.insert(0, generateConclusion(varD, LABEL_VAR, UIC));
|
||||
tree.insert(0, AXC + CURLY_LEFT + generateVarStepPremise(varD) + CURLY_RIGHT + NEW_LINE);
|
||||
tree.insert(0, AXC + CURLY_LEFT + DOLLAR_SIGN + generateVarStepPremise(varD)
|
||||
+ DOLLAR_SIGN + CURLY_RIGHT + NEW_LINE);
|
||||
}
|
||||
|
||||
@Override
|
||||
@ -182,9 +183,9 @@ public class LatexCreator implements StepVisitor {
|
||||
String premiseRight = DOLLAR_SIGN + typeAbstraction + INSTANTIATE_SIGN + instantiatedType
|
||||
+ DOLLAR_SIGN + NEW_LINE;
|
||||
String premiseLeft = AXC + CURLY_LEFT + DOLLAR_SIGN + ALIGN_BEGIN
|
||||
+ generateVarStepPremise(varL).replace(DOLLAR_SIGN, "")
|
||||
+ SPACE + LATEX_NEW_LINE + SPACE // TODO: less replacement fixups
|
||||
+ premiseRight.replace(DOLLAR_SIGN, "")
|
||||
+ generateVarStepPremise(varL)
|
||||
+ SPACE + LATEX_NEW_LINE + SPACE
|
||||
+ premiseRight
|
||||
+ ALIGN_END + DOLLAR_SIGN + CURLY_RIGHT + NEW_LINE;
|
||||
tree.insert(0, premiseLeft);
|
||||
}
|
||||
@ -194,7 +195,6 @@ public class LatexCreator implements StepVisitor {
|
||||
tree.insert(0, generateConclusion(letD, LABEL_LET, BIC));
|
||||
letD.getPremise().accept(this);
|
||||
letD.getTypeInferer().getFirstInferenceStep().accept(this);
|
||||
// todo correct?
|
||||
}
|
||||
|
||||
@Override
|
||||
|
@ -200,14 +200,7 @@ public class LatexCreatorConstraints implements StepVisitor {
|
||||
latex.append(CURLY_LEFT);
|
||||
}
|
||||
latex.append(new LatexCreatorType(unificationConstraints.get(i).getFirstType()).getLatex());
|
||||
if (markError && i == 0) {
|
||||
latex.append(CURLY_RIGHT);
|
||||
}
|
||||
latex.append(EQUALS);
|
||||
if (markError && i == 0) {
|
||||
latex.append(COLOR_RED);
|
||||
latex.append(CURLY_LEFT);
|
||||
}
|
||||
latex.append(new LatexCreatorType(unificationConstraints.get(i).getSecondType()).getLatex());
|
||||
if (markError && i == 0) {
|
||||
latex.append(CURLY_RIGHT);
|
||||
|
Loading…
Reference in New Issue
Block a user