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

add more explanation to unification

Browse Source
This commit is contained in:
ucrhh 2021-02-11 21:27:08 +01:00
parent e85b39c93e
commit 9851ac61da
2 changed files with 11 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstants.java
View File

@ -7,6 +7,7 @@ public final class LatexCreatorConstants {
protected static final String CONST = "Const"; protected static final String CONST = "Const";
protected static final String LET = "let"; protected static final String LET = "let";
protected static final String IN = "in"; protected static final String IN = "in";
protected static final String MGU = "mgu";
protected static final String CONSTRAINT_SET = "C"; protected static final String CONSTRAINT_SET = "C";
protected static final String DOLLAR_SIGN = "$"; protected static final String DOLLAR_SIGN = "$";
@ -38,6 +39,7 @@ public final class LatexCreatorConstants {
protected static final String TREE_VARIABLE = "\\alpha"; protected static final String TREE_VARIABLE = "\\alpha";
protected static final String GENERATED_ASSUMPTION_VARIABLE = "\\beta"; protected static final String GENERATED_ASSUMPTION_VARIABLE = "\\beta";
protected static final String USER_VARIABLE = "\\tau"; protected static final String USER_VARIABLE = "\\tau";
protected static final String SIGMA = "\\sigma";
protected static final String GAMMA = "\\Gamma"; protected static final String GAMMA = "\\Gamma";
protected static final String LATEX_NEW_LINE = "\\\\"; protected static final String LATEX_NEW_LINE = "\\\\";

11
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstraints.java
View File

@ -8,9 +8,10 @@ import java.util.ArrayList;
import java.util.List; import java.util.List;
import java.util.Optional; import java.util.Optional;
// todo javadoc
import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.*; import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.*;
// todo javadoc
public class LatexCreatorConstraints implements StepVisitor { public class LatexCreatorConstraints implements StepVisitor {
private static final String FIRST_PREFIX = ""; private static final String FIRST_PREFIX = "";
@ -162,7 +163,7 @@ public class LatexCreatorConstraints implements StepVisitor {
private List<String> generateUnification(String constraintSets) { private List<String> generateUnification(String constraintSets) {
List<String> steps = new ArrayList<>(); List<String> steps = new ArrayList<>();
// TODO: check if unification is present
List<UnificationStep> unificationSteps = typeInferer.getUnificationSteps() List<UnificationStep> unificationSteps = typeInferer.getUnificationSteps()
.orElseThrow(IllegalStateException::new); .orElseThrow(IllegalStateException::new);
for (UnificationStep step : unificationSteps) { for (UnificationStep step : unificationSteps) {
@ -175,6 +176,12 @@ public class LatexCreatorConstraints implements StepVisitor {
} }
StringBuilder latex = new StringBuilder(); StringBuilder latex = new StringBuilder();
latex.append(constraintSets); latex.append(constraintSets);
latex.append(SIGMA);
latex.append(constraintSetIndex);
latex.append("" + COLON + EQUALS + MGU + PAREN_LEFT + CONSTRAINT_SET);
latex.append(constraintSetIndex);
latex.append("" + PAREN_RIGHT + EQUALS);
List<Substitution> substitutions = subs.unwrap(); List<Substitution> substitutions = subs.unwrap();
for (Substitution s : substitutions) { for (Substitution s : substitutions) {
latex.append(new LatexCreatorType(s.getVariable()).getLatex()); latex.append(new LatexCreatorType(s.getVariable()).getLatex());