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

partly implement let constraint generation

Browse Source
This commit is contained in:
ucrhh 2021-02-07 12:07:26 +01:00
parent 4c48c1dca5
commit 03af53b20a
3 changed files with 39 additions and 29 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/ConstraintSetIndexFactory.java
View File

@ -1,5 +1,10 @@
package edu.kit.typicalc.view.content.typeinferencecontent;
import static edu.kit.typicalc.view.content.typeinferencecontent.LatexCreatorConstants.CURLY_LEFT;
import static edu.kit.typicalc.view.content.typeinferencecontent.LatexCreatorConstants.CURLY_RIGHT;
import static edu.kit.typicalc.view.content.typeinferencecontent.LatexCreatorConstants.LET;
import static edu.kit.typicalc.view.content.typeinferencecontent.LatexCreatorConstants.UNDERSCORE;
/**
* A constraint set index factory is used to create consecutive indices for multiple (let-) constraint sets
* that might be created during the inference of one lambda term.
@ -21,7 +26,15 @@ public class ConstraintSetIndexFactory {
*
* @return the next constraint set index
*/
public int nextConstraintSetIndex() {
return nextConstraintSetIndex++;
public String nextConstraintSetIndex() {
String index = nextConstraintSetIndex == FIRST_CONSTRAINT_SET_INDEX
? ""
: nextConstraintSetIndex == FIRST_CONSTRAINT_SET_INDEX + 1
? UNDERSCORE + CURLY_LEFT + LET + CURLY_RIGHT
: UNDERSCORE + CURLY_LEFT + LET + UNDERSCORE
+ CURLY_LEFT + nextConstraintSetIndex + CURLY_RIGHT + CURLY_RIGHT;
nextConstraintSetIndex++;
return index;
}
}

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

@ -9,7 +9,7 @@ public final class LatexCreatorConstants {
protected static final String IN = "in";
protected static final String CONSTRAINT_SET = "C";
protected static final String NEW_LINE = "\n";
protected static final String NEW_LINE = System.lineSeparator();
protected static final String SPACE = " ";
protected static final String DOLLAR_SIGN = "$";
protected static final String EQUALS = "=";

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

@ -12,58 +12,53 @@ import java.util.Optional;
import static edu.kit.typicalc.view.content.typeinferencecontent.LatexCreatorConstants.*;
public class LatexCreatorConstraints implements StepVisitor {
private static final String FIRST_PREFIX = "";
private final List<String> constraints;
private final TypeInfererInterface typeInferer;
private final ConstraintSetIndexFactory constraintSetIndexFactory;
private final int constraintSetIndex;
private final String constraintSetIndex;
private final String prefix;
private String prevStep;
protected LatexCreatorConstraints(TypeInfererInterface typeInferer) {
this(typeInferer, new ConstraintSetIndexFactory());
this(typeInferer, new ConstraintSetIndexFactory(), FIRST_PREFIX);
}
protected LatexCreatorConstraints(TypeInfererInterface typeInferer,
ConstraintSetIndexFactory constraintSetIndexFactory) {
ConstraintSetIndexFactory constraintSetIndexFactory,
String prefix) {
this.prefix = prefix;
this.prevStep = "";
this.constraintSetIndexFactory = constraintSetIndexFactory;
this.constraintSetIndex = constraintSetIndexFactory.nextConstraintSetIndex();
this.typeInferer = typeInferer;
constraints = new ArrayList<>();
constraints.add(PHANTOM_X);
if (FIRST_PREFIX.equals(prefix)) {
constraints.add(DOLLAR_SIGN + CONSTRAINT_SET + EQUALS + LATEX_CURLY_LEFT + LATEX_CURLY_RIGHT + DOLLAR_SIGN);
}
typeInferer.getFirstInferenceStep().accept(this);
}
protected List<String> getEverything() {
List<String> result = new ArrayList<>(this.getConstraints());
List<String> result = new ArrayList<>(constraints);
result.addAll(generateUnification());
typeInferer.getMGU().ifPresent(mgu -> result.add(generateMGU()));
// todo return final type
return result;
}
protected List<String> getConstraints() {
List<String> temp = new ArrayList<>(constraints);
temp.replaceAll(current -> {
String index = constraintSetIndex == 0 ? ""
: UNDERSCORE + CURLY_LEFT + LET + UNDERSCORE + CURLY_LEFT + constraintSetIndex
+ CURLY_RIGHT + CURLY_RIGHT;
return DOLLAR_SIGN + CONSTRAINT_SET + index + EQUALS + LATEX_CURLY_LEFT + current
+ LATEX_CURLY_RIGHT + DOLLAR_SIGN;
});
return temp;
}
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;
String previousConstraints = constraints.get(constraints.size() - 1);
if (constraints.size() > 1) {
constraints.add(previousConstraints + COMMA + currentConstraint);
} else {
prevStep = prevStep.equals("") ? currentConstraint : prevStep + COMMA + currentConstraint;
currentConstraint = prefix + DOLLAR_SIGN + CONSTRAINT_SET + constraintSetIndex + EQUALS + LATEX_CURLY_LEFT
+ prevStep + LATEX_CURLY_RIGHT + DOLLAR_SIGN;
constraints.add(currentConstraint);
}
}
@Override
public void visit(AbsStepDefault absD) {
@ -101,8 +96,10 @@ public class LatexCreatorConstraints implements StepVisitor {
@Override
public void visit(LetStepDefault letD) {
new LatexCreatorConstraints(letD.getTypeInferer(), constraintSetIndexFactory).getEverything();
addConstraint(letD);
LatexCreatorConstraints subCreator = new LatexCreatorConstraints(letD.getTypeInferer(),
constraintSetIndexFactory, constraints.get(constraints.size() - 1));
constraints.addAll(subCreator.getEverything());
letD.getPremise().accept(this);
}