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

new line after each 10 constraints

Browse Source
This commit is contained in:
Johanna Stuber 2021-03-07 22:20:18 +01:00
parent 7a28facd83
commit 5b86874e0c
2 changed files with 38 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -24,6 +24,7 @@ import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.La
public class LatexCreatorConstraints implements StepVisitor { public class LatexCreatorConstraints implements StepVisitor {
private static final String FIRST_PREFIX = ""; private static final String FIRST_PREFIX = "";
private static final int BREAK_AFTER = 10;
private final List<String> constraints; private final List<String> constraints;
private final TypeInfererInterface typeInferer; private final TypeInfererInterface typeInferer;
@ -35,6 +36,7 @@ public class LatexCreatorConstraints implements StepVisitor {
private final Optional<Map<VarTerm, TypeAbstraction>> newTypeAssumption; private final Optional<Map<VarTerm, TypeAbstraction>> newTypeAssumption;
private String prevStep; private String prevStep;
private final Function<UnificationError, String> translationProvider; private final Function<UnificationError, String> translationProvider;
private int constraintsInCurrLine;
/** /**
* Initializes the LatexCreatorConstraints with the right values calculates the strings * Initializes the LatexCreatorConstraints with the right values calculates the strings
@ -66,6 +68,7 @@ public class LatexCreatorConstraints implements StepVisitor {
this.constraintSetIndex = constraintSetIndexFactory.nextConstraintSetIndex(); this.constraintSetIndex = constraintSetIndexFactory.nextConstraintSetIndex();
this.typeInferer = typeInferer; this.typeInferer = typeInferer;
this.translationProvider = translationProvider; this.translationProvider = translationProvider;
this.constraintsInCurrLine = 0;
constraints = new ArrayList<>(); constraints = new ArrayList<>();
if (FIRST_PREFIX.equals(prefix)) { if (FIRST_PREFIX.equals(prefix)) {
constraints.add(AMPERSAND + CONSTRAINT_SET + EQUALS + LATEX_CURLY_LEFT + LATEX_CURLY_RIGHT); constraints.add(AMPERSAND + CONSTRAINT_SET + EQUALS + LATEX_CURLY_LEFT + LATEX_CURLY_RIGHT);
@ -132,12 +135,21 @@ public class LatexCreatorConstraints implements StepVisitor {
} }
private void addConstraint(InferenceStep step) { private void addConstraint(InferenceStep step) {
String currentConstraint = createSingleConstraint(step.getConstraint()); String currentSingleConstraint = createSingleConstraint(step.getConstraint());
prevStep = prevStep.equals("") ? currentConstraint : prevStep + COMMA + currentConstraint; if (!prevStep.equals("")) {
currentConstraint = prefix + AMPERSAND + CONSTRAINT_SET + constraintSetIndex + EQUALS + LATEX_CURLY_LEFT prevStep += COMMA;
+ prevStep + LATEX_CURLY_RIGHT; }
constraints.add(currentConstraint); if (constraintsInCurrLine >= BREAK_AFTER) {
prevStep += LATEX_NEW_LINE + AMPERSAND;
constraintsInCurrLine = 0;
}
prevStep += currentSingleConstraint;
String currentConstraints = prefix + AMPERSAND + SPLIT_BEGIN + CONSTRAINT_SET + constraintSetIndex
+ EQUALS + LATEX_CURLY_LEFT + AMPERSAND + prevStep + LATEX_CURLY_RIGHT + SPLIT_END;
constraints.add(currentConstraints);
numberGenerator.incrementPush(); numberGenerator.incrementPush();
constraintsInCurrLine++;
} }
@Override @Override
@ -195,8 +207,8 @@ public class LatexCreatorConstraints implements StepVisitor {
// adds one step in which all let constraints are added to 'outer' constraint set // adds one step in which all let constraints are added to 'outer' constraint set
String letConstraints = createLetConstraints(letD.getTypeInferer().getLetConstraints()); String letConstraints = createLetConstraints(letD.getTypeInferer().getLetConstraints());
prevStep = prevStep.equals("") ? letConstraints : prevStep + COMMA + letConstraints; prevStep = prevStep.equals("") ? letConstraints : prevStep + COMMA + letConstraints;
letConstraints = prefix + AMPERSAND + CONSTRAINT_SET + constraintSetIndex + EQUALS + LATEX_CURLY_LEFT letConstraints = prefix + AMPERSAND + SPLIT_BEGIN + CONSTRAINT_SET + constraintSetIndex + EQUALS
+ prevStep + LATEX_CURLY_RIGHT; + LATEX_CURLY_LEFT + AMPERSAND + prevStep + LATEX_CURLY_RIGHT + SPLIT_END;
constraints.add(letConstraints); constraints.add(letConstraints);
numberGenerator.push(); numberGenerator.push();
@ -205,7 +217,15 @@ public class LatexCreatorConstraints implements StepVisitor {
private String createLetConstraints(List<Constraint> letConstraints) { private String createLetConstraints(List<Constraint> letConstraints) {
StringBuilder result = new StringBuilder(); StringBuilder result = new StringBuilder();
letConstraints.forEach(constraint -> result.append(createSingleConstraint(constraint)).append(COMMA)); letConstraints.forEach(constraint -> {
if (constraintsInCurrLine >= BREAK_AFTER) {
result.append(LATEX_NEW_LINE)
.append(AMPERSAND);
constraintsInCurrLine = 0;
}
result.append(createSingleConstraint(constraint)).append(COMMA);
constraintsInCurrLine++;
});
if (!letConstraints.isEmpty()) { if (!letConstraints.isEmpty()) {
result.deleteCharAt(result.length() - 1); result.deleteCharAt(result.length() - 1);
} }

17
src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstraintsTest.java
View File

@ -26,8 +26,9 @@ class LatexCreatorConstraintsTest {
typeInferer = model.getTypeInferer("x", new HashMap<>()).unwrap(); typeInferer = model.getTypeInferer("x", new HashMap<>()).unwrap();
List<String> actual = new LatexCreatorConstraints(typeInferer, Enum::toString).getEverything(); List<String> actual = new LatexCreatorConstraints(typeInferer, Enum::toString).getEverything();
String constraintSet = AMPERSAND + CONSTRAINT_SET + EQUALS + LATEX_CURLY_LEFT + TREE_VARIABLE + "_{1}" + EQUALS String constraintSet = AMPERSAND + SPLIT_BEGIN + CONSTRAINT_SET + EQUALS + LATEX_CURLY_LEFT + AMPERSAND
+ GENERATED_ASSUMPTION_VARIABLE + "_{1}" + LATEX_CURLY_RIGHT; + TREE_VARIABLE + "_{1}" + EQUALS + GENERATED_ASSUMPTION_VARIABLE + "_{1}" + LATEX_CURLY_RIGHT
+ SPLIT_END;
String mgu = "" + EQUALS + BRACKET_LEFT + AMPERSAND + TREE_VARIABLE + "_{1}" String mgu = "" + EQUALS + BRACKET_LEFT + AMPERSAND + TREE_VARIABLE + "_{1}"
@ -55,12 +56,14 @@ class LatexCreatorConstraintsTest {
typeInferer = model.getTypeInferer("λx.y", new HashMap<>()).unwrap(); typeInferer = model.getTypeInferer("λx.y", new HashMap<>()).unwrap();
List<String> actual = new LatexCreatorConstraints(typeInferer, Enum::toString).getEverything(); List<String> actual = new LatexCreatorConstraints(typeInferer, Enum::toString).getEverything();
String constraintSet1 = AMPERSAND + CONSTRAINT_SET + EQUALS + LATEX_CURLY_LEFT + TREE_VARIABLE + "_{1}" + EQUALS String constraintSet1 = AMPERSAND + SPLIT_BEGIN + CONSTRAINT_SET + EQUALS + LATEX_CURLY_LEFT + AMPERSAND
+ TREE_VARIABLE + "_{2}" + SPACE + RIGHT_ARROW + SPACE + TREE_VARIABLE + "_{3}" + LATEX_CURLY_RIGHT; + TREE_VARIABLE + "_{1}" + EQUALS + TREE_VARIABLE + "_{2}" + SPACE + RIGHT_ARROW + SPACE
+ TREE_VARIABLE + "_{3}" + LATEX_CURLY_RIGHT + SPLIT_END;
String constraintSet2 = AMPERSAND + CONSTRAINT_SET + EQUALS + LATEX_CURLY_LEFT + TREE_VARIABLE + "_{1}" + EQUALS String constraintSet2 = AMPERSAND + SPLIT_BEGIN + CONSTRAINT_SET + EQUALS + LATEX_CURLY_LEFT + AMPERSAND
+ TREE_VARIABLE + "_{2}" + SPACE + RIGHT_ARROW + SPACE + TREE_VARIABLE + "_{3}" + COMMA + TREE_VARIABLE + TREE_VARIABLE + "_{1}" + EQUALS + TREE_VARIABLE + "_{2}" + SPACE + RIGHT_ARROW + SPACE
+ "_{3}" + EQUALS + GENERATED_ASSUMPTION_VARIABLE + "_{1}" + LATEX_CURLY_RIGHT; + TREE_VARIABLE + "_{3}" + COMMA + TREE_VARIABLE + "_{3}" + EQUALS + GENERATED_ASSUMPTION_VARIABLE
+ "_{1}" + LATEX_CURLY_RIGHT + SPLIT_END;
String unify1 = MGU_START + EQUALS + UNIFY + PAREN_LEFT + LATEX_CURLY_LEFT + AMPERSAND String unify1 = MGU_START + EQUALS + UNIFY + PAREN_LEFT + LATEX_CURLY_LEFT + AMPERSAND
+ TREE_VARIABLE + "_{3}" + EQUALS + GENERATED_ASSUMPTION_VARIABLE + "_{1}"; + TREE_VARIABLE + "_{3}" + EQUALS + GENERATED_ASSUMPTION_VARIABLE + "_{1}";