mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-08 18:30:42 +00:00
implement mgu generation in LatexCreator
This commit is contained in:
parent
886ea78869
commit
bb300e292c
@ -61,7 +61,7 @@ public class LatexCreator implements StepVisitor {
|
||||
protected String[] getUnification() {
|
||||
List<String> result = new ArrayList<>(constraintsGenerator.getConstraints());
|
||||
result.addAll(generateUnification());
|
||||
//todo MGU and final type
|
||||
typeInferer.getMGU().ifPresent(mgu -> result.add(generateMGU()));
|
||||
return result.toArray(new String[0]);
|
||||
} // todo implement
|
||||
|
||||
@ -121,7 +121,22 @@ public class LatexCreator implements StepVisitor {
|
||||
steps.add(latex.toString());
|
||||
}
|
||||
return steps;
|
||||
}
|
||||
|
||||
private String generateMGU() {
|
||||
StringBuilder mguLatex = new StringBuilder();
|
||||
mguLatex.append(DOLLAR_SIGN);
|
||||
mguLatex.append(BRACKET_LEFT);
|
||||
typeInferer.getMGU().ifPresent(mgu -> mgu.forEach(substitution -> {
|
||||
mguLatex.append(new LatexCreatorType(substitution.getVariable()).getLatex());
|
||||
mguLatex.append(SUBSTITUTION_SIGN);
|
||||
mguLatex.append(new LatexCreatorType(substitution.getType()).getLatex());
|
||||
mguLatex.append(COMMA);
|
||||
}));
|
||||
mguLatex.deleteCharAt(mguLatex.length() - 1);
|
||||
mguLatex.append(BRACKET_RIGHT);
|
||||
mguLatex.append(DOLLAR_SIGN);
|
||||
return mguLatex.toString();
|
||||
}
|
||||
|
||||
private String conclusionToLatex(Conclusion conclusion) {
|
||||
|
@ -20,6 +20,8 @@ public final class LatexCreatorConstants {
|
||||
protected static final String CURLY_RIGHT = "}";
|
||||
protected static final String PAREN_LEFT = "(";
|
||||
protected static final String PAREN_RIGHT = ")";
|
||||
protected static final String BRACKET_LEFT = "[";
|
||||
protected static final String BRACKET_RIGHT = "]";
|
||||
|
||||
protected static final String LABEL_ABS = "\\LeftLabel{\\rm A{\\small BS}}";
|
||||
protected static final String LABEL_APP = "\\LeftLabel{\\rm A{\\small PP}}";
|
||||
|
Loading…
Reference in New Issue
Block a user