arnekeller/Typicalc
1
0
Fork 0
mirror of https://gitlab.kit.edu/uskyk/typicalc.git synced 2024-11-10 03:10:44 +00:00
Code Issues Packages Projects Releases Wiki Activity

add let constraint to outer constraint set

Browse Source
This commit is contained in:
ucrhh 2021-02-09 17:17:11 +01:00
parent f49fb3f984
commit 28025a25c2
1 changed files with 26 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -26,7 +26,7 @@ public class LatexCreatorConstraints implements StepVisitor {
this(typeInferer, new ConstraintSetIndexFactory(), FIRST_PREFIX);
}
protected LatexCreatorConstraints(TypeInfererInterface typeInferer,
private LatexCreatorConstraints(TypeInfererInterface typeInferer,
ConstraintSetIndexFactory constraintSetIndexFactory,
String prefix) {
this.prefix = prefix;
@ -53,10 +53,14 @@ public class LatexCreatorConstraints implements StepVisitor {
return result;
}
protected void addConstraint(InferenceStep step) {
String firstType = new LatexCreatorType(step.getConstraint().getFirstType()).getLatex();
String secondType = new LatexCreatorType(step.getConstraint().getSecondType()).getLatex();
String currentConstraint = firstType + SPACE + EQUALS + SPACE + secondType;
private String createSingleConstraint(Constraint constraint) {
String firstType = new LatexCreatorType(constraint.getFirstType()).getLatex();
String secondType = new LatexCreatorType(constraint.getSecondType()).getLatex();
return firstType + SPACE + EQUALS + SPACE + secondType;
}
private void addConstraint(InferenceStep step) {
String currentConstraint = createSingleConstraint(step.getConstraint());
prevStep = prevStep.equals("") ? currentConstraint : prevStep + COMMA + currentConstraint;
currentConstraint = prefix + CONSTRAINT_SET + constraintSetIndex + EQUALS + LATEX_CURLY_LEFT
+ prevStep + LATEX_CURLY_RIGHT;
@ -103,9 +107,26 @@ public class LatexCreatorConstraints implements StepVisitor {
LatexCreatorConstraints subCreator = new LatexCreatorConstraints(letD.getTypeInferer(),
constraintSetIndexFactory, constraints.get(constraints.size() - 1) + LATEX_NEW_LINE + NEW_LINE);
constraints.addAll(subCreator.getEverything());
// adds one step in which all let constraints are added to 'outer' constraint set
String letConstraints = createLetConstraints(letD.getTypeInferer().getLetConstraints());
prevStep = prevStep.equals("") ? letConstraints : prevStep + COMMA + letConstraints;
letConstraints = prefix + CONSTRAINT_SET + constraintSetIndex + EQUALS + LATEX_CURLY_LEFT
+ prevStep + LATEX_CURLY_RIGHT;
constraints.add(letConstraints);
letD.getPremise().accept(this);
}
private String createLetConstraints(List<Constraint> letConstraints) {
StringBuilder result = new StringBuilder();
letConstraints.forEach(constraint -> result.append(createSingleConstraint(constraint)).append(COMMA));
if (!letConstraints.isEmpty()) {
result.deleteCharAt(result.length() - 1);
}
return result.toString();
}
@Override
public void visit(EmptyStep empty) {
// empty steps dont have constraints associated with them