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

make final type look consistent to Übungsblatt

Browse Source
This commit is contained in:
ucrhh 2021-02-12 12:31:45 +01:00
parent 0fa40e7837
commit dabde5e455
2 changed files with 31 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java
View File

@ -78,7 +78,7 @@ public class TypeInferenceResult {
/**
* Returns the type that is the result of the type inference. It is obtained by applying
* the mgu to the type variable the type inference result was given in its construstor.
* the mgu to the type variable the type inference result was given in its constructor.
* If no valid type can be found for the lambda term to type-infer, null is returned.
*
* @return the final type of the lambda term, null if there is no valid type

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

@ -59,8 +59,7 @@ public class LatexCreatorConstraints implements StepVisitor {
typeInferer.getMGU().ifPresent(mgu -> {
result.add(generateMGU(constraintSets));
numberGenerator.push();
result.add(generateMGU(constraintSets) + LATEX_NEW_LINE
+ new LatexCreatorType(typeInferer.getType().get()).getLatex());
result.add(generateMGU(constraintSets) + LATEX_NEW_LINE + generateFinalType());
numberGenerator.push();
});
// todo add some helpful text for the user
@ -161,6 +160,16 @@ public class LatexCreatorConstraints implements StepVisitor {
// empty steps dont have constraints associated with them
}
private StringBuilder generateUnificationName() {
StringBuilder latex = new StringBuilder();
latex.append(SIGMA);
latex.append(constraintSetIndex);
latex.append("" + COLON + EQUALS + MGU + PAREN_LEFT + CONSTRAINT_SET);
latex.append(constraintSetIndex);
latex.append("" + PAREN_RIGHT + EQUALS);
return latex;
}
private List<String> generateUnification(String constraintSets) {
List<String> steps = new ArrayList<>();
@ -176,12 +185,8 @@ public class LatexCreatorConstraints implements StepVisitor {
}
StringBuilder latex = new StringBuilder();
latex.append(constraintSets);
latex.append(AMPERSAND + SPLIT_BEGIN + SIGMA);
latex.append(constraintSetIndex);
latex.append("" + COLON + EQUALS + MGU + PAREN_LEFT + CONSTRAINT_SET);
latex.append(constraintSetIndex);
latex.append("" + PAREN_RIGHT + EQUALS);
latex.append(AMPERSAND + SPLIT_BEGIN);
latex.append(generateUnificationName());
boolean markError = error.isPresent();
error.ifPresent(latex::append); // TODO: translation
@ -244,18 +249,33 @@ public class LatexCreatorConstraints implements StepVisitor {
private String generateMGU(String constraintSets) {
StringBuilder latex = new StringBuilder();
latex.append(constraintSets);
latex.append(AMPERSAND + SPLIT_BEGIN);
latex.append(generateUnificationName());
latex.append(SPACE);
latex.append(BRACKET_LEFT);
typeInferer.getMGU().ifPresent(mgu -> mgu.forEach(substitution -> {
latex.append(AMPERSAND);
latex.append(new LatexCreatorType(substitution.getVariable()).getLatex());
latex.append(SUBSTITUTION_SIGN);
latex.append(new LatexCreatorType(substitution.getType()).getLatex());
latex.append(COMMA);
latex.append(LATEX_NEW_LINE);
latex.append(NEW_LINE);
}));
latex.delete(latex.length() - (COMMA + LATEX_NEW_LINE + NEW_LINE).length(), latex.length());
latex.delete(latex.length() - (COMMA + LATEX_NEW_LINE).length(), latex.length());
latex.append(BRACKET_RIGHT);
latex.append(SPLIT_END);
return latex.toString();
}
private String generateFinalType() {
StringBuilder latex = new StringBuilder();
latex.append(AMPERSAND);
latex.append(SIGMA);
latex.append(constraintSetIndex);
latex.append(PAREN_LEFT);
latex.append(new LatexCreatorType(typeInferer.getFirstInferenceStep().getConclusion().getType()).getLatex());
latex.append("" + PAREN_RIGHT + EQUALS);
latex.append(new LatexCreatorType(typeInferer.getType().get()).getLatex());
return latex.toString();
}
}