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 0640d95..a96829d 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 @@ -61,7 +61,7 @@ public class LatexCreator implements StepVisitor { protected String[] getUnification() { List 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) { 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 index ddeab0d..b9d8b20 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreatorConstants.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreatorConstants.java @@ -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}}";