mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-08 18:30:42 +00:00
stop tree animation during unification
This commit is contained in:
parent
28025a25c2
commit
7db36724ea
@ -6,6 +6,7 @@ import edu.kit.typicalc.model.step.*;
|
|||||||
import edu.kit.typicalc.model.term.VarTerm;
|
import edu.kit.typicalc.model.term.VarTerm;
|
||||||
import edu.kit.typicalc.model.type.TypeAbstraction;
|
import edu.kit.typicalc.model.type.TypeAbstraction;
|
||||||
|
|
||||||
|
import java.util.List;
|
||||||
import java.util.Map;
|
import java.util.Map;
|
||||||
|
|
||||||
import static edu.kit.typicalc.view.content.typeinferencecontent.LatexCreatorConstants.*;
|
import static edu.kit.typicalc.view.content.typeinferencecontent.LatexCreatorConstants.*;
|
||||||
@ -21,6 +22,7 @@ public class LatexCreator implements StepVisitor {
|
|||||||
private final TypeInfererInterface typeInferer;
|
private final TypeInfererInterface typeInferer;
|
||||||
private final StringBuilder tree;
|
private final StringBuilder tree;
|
||||||
private final boolean stepLabels;
|
private final boolean stepLabels;
|
||||||
|
private final LatexCreatorConstraints constraintsCreator;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Generate the pieces of LaTeX-code from the type inferer.
|
* Generate the pieces of LaTeX-code from the type inferer.
|
||||||
@ -42,6 +44,7 @@ public class LatexCreator implements StepVisitor {
|
|||||||
this.tree = new StringBuilder();
|
this.tree = new StringBuilder();
|
||||||
this.stepLabels = stepLabels;
|
this.stepLabels = stepLabels;
|
||||||
typeInferer.getFirstInferenceStep().accept(this);
|
typeInferer.getFirstInferenceStep().accept(this);
|
||||||
|
this.constraintsCreator = new LatexCreatorConstraints(typeInferer);
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
@ -54,12 +57,16 @@ public class LatexCreator implements StepVisitor {
|
|||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Returns the LaTeX-code for constraints, unification, MGU and MGU
|
* Returns the LaTeX-code for constraints, unification, MGU and final type
|
||||||
*
|
*
|
||||||
* @return the LaTeX-code for constraints and unification
|
* @return the LaTeX-code for constraints and unification
|
||||||
*/
|
*/
|
||||||
protected String[] getUnification() {
|
protected String[] getUnification() {
|
||||||
return new LatexCreatorConstraints(typeInferer).getEverything().toArray(new String[0]);
|
return constraintsCreator.getEverything().toArray(new String[0]);
|
||||||
|
}
|
||||||
|
|
||||||
|
protected List<Integer> getTreeNumbers() {
|
||||||
|
return constraintsCreator.getTreeNumbers();
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
|
@ -18,25 +18,29 @@ public class LatexCreatorConstraints implements StepVisitor {
|
|||||||
private final List<String> constraints;
|
private final List<String> constraints;
|
||||||
private final TypeInfererInterface typeInferer;
|
private final TypeInfererInterface typeInferer;
|
||||||
private final ConstraintSetIndexFactory constraintSetIndexFactory;
|
private final ConstraintSetIndexFactory constraintSetIndexFactory;
|
||||||
|
private final TreeNumberGenerator numberGenerator;
|
||||||
private final String constraintSetIndex;
|
private final String constraintSetIndex;
|
||||||
private final String prefix;
|
private final String prefix;
|
||||||
private String prevStep;
|
private String prevStep;
|
||||||
|
|
||||||
protected LatexCreatorConstraints(TypeInfererInterface typeInferer) {
|
protected LatexCreatorConstraints(TypeInfererInterface typeInferer) {
|
||||||
this(typeInferer, new ConstraintSetIndexFactory(), FIRST_PREFIX);
|
this(typeInferer, new ConstraintSetIndexFactory(), new TreeNumberGenerator(), FIRST_PREFIX);
|
||||||
}
|
}
|
||||||
|
|
||||||
private LatexCreatorConstraints(TypeInfererInterface typeInferer,
|
private LatexCreatorConstraints(TypeInfererInterface typeInferer,
|
||||||
ConstraintSetIndexFactory constraintSetIndexFactory,
|
ConstraintSetIndexFactory constraintSetIndexFactory,
|
||||||
|
TreeNumberGenerator numberGenerator,
|
||||||
String prefix) {
|
String prefix) {
|
||||||
this.prefix = prefix;
|
this.prefix = prefix;
|
||||||
this.prevStep = "";
|
this.prevStep = "";
|
||||||
this.constraintSetIndexFactory = constraintSetIndexFactory;
|
this.constraintSetIndexFactory = constraintSetIndexFactory;
|
||||||
|
this.numberGenerator = numberGenerator;
|
||||||
this.constraintSetIndex = constraintSetIndexFactory.nextConstraintSetIndex();
|
this.constraintSetIndex = constraintSetIndexFactory.nextConstraintSetIndex();
|
||||||
this.typeInferer = typeInferer;
|
this.typeInferer = typeInferer;
|
||||||
constraints = new ArrayList<>();
|
constraints = new ArrayList<>();
|
||||||
if (FIRST_PREFIX.equals(prefix)) {
|
if (FIRST_PREFIX.equals(prefix)) {
|
||||||
constraints.add(CONSTRAINT_SET + EQUALS + LATEX_CURLY_LEFT + LATEX_CURLY_RIGHT);
|
constraints.add(CONSTRAINT_SET + EQUALS + LATEX_CURLY_LEFT + LATEX_CURLY_RIGHT);
|
||||||
|
numberGenerator.incrementPush();
|
||||||
}
|
}
|
||||||
|
|
||||||
typeInferer.getFirstInferenceStep().accept(this);
|
typeInferer.getFirstInferenceStep().accept(this);
|
||||||
@ -44,15 +48,25 @@ public class LatexCreatorConstraints implements StepVisitor {
|
|||||||
|
|
||||||
protected List<String> getEverything() {
|
protected List<String> getEverything() {
|
||||||
List<String> result = new ArrayList<>(constraints);
|
List<String> result = new ArrayList<>(constraints);
|
||||||
result.addAll(generateUnification());
|
generateUnification().forEach(step -> {
|
||||||
typeInferer.getMGU().ifPresent(mgu -> result.add(generateMGU()));
|
result.add(step);
|
||||||
// todo return final type
|
numberGenerator.push();
|
||||||
|
});
|
||||||
|
typeInferer.getMGU().ifPresent(mgu -> {
|
||||||
|
result.add(generateMGU());
|
||||||
|
numberGenerator.push();
|
||||||
|
});
|
||||||
|
// todo return final type, dont forget numberGenerator.push();
|
||||||
if (FIRST_PREFIX.equals(prefix)) {
|
if (FIRST_PREFIX.equals(prefix)) {
|
||||||
result.replaceAll(content -> ALIGN_BEGIN + content + ALIGN_END);
|
result.replaceAll(content -> ALIGN_BEGIN + content + ALIGN_END);
|
||||||
}
|
}
|
||||||
return result;
|
return result;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
protected List<Integer> getTreeNumbers() {
|
||||||
|
return numberGenerator.getNumbers();
|
||||||
|
}
|
||||||
|
|
||||||
private String createSingleConstraint(Constraint constraint) {
|
private String createSingleConstraint(Constraint constraint) {
|
||||||
String firstType = new LatexCreatorType(constraint.getFirstType()).getLatex();
|
String firstType = new LatexCreatorType(constraint.getFirstType()).getLatex();
|
||||||
String secondType = new LatexCreatorType(constraint.getSecondType()).getLatex();
|
String secondType = new LatexCreatorType(constraint.getSecondType()).getLatex();
|
||||||
@ -65,6 +79,7 @@ public class LatexCreatorConstraints implements StepVisitor {
|
|||||||
currentConstraint = prefix + CONSTRAINT_SET + constraintSetIndex + EQUALS + LATEX_CURLY_LEFT
|
currentConstraint = prefix + CONSTRAINT_SET + constraintSetIndex + EQUALS + LATEX_CURLY_LEFT
|
||||||
+ prevStep + LATEX_CURLY_RIGHT;
|
+ prevStep + LATEX_CURLY_RIGHT;
|
||||||
constraints.add(currentConstraint);
|
constraints.add(currentConstraint);
|
||||||
|
numberGenerator.incrementPush();
|
||||||
}
|
}
|
||||||
|
|
||||||
@Override
|
@Override
|
||||||
@ -105,7 +120,8 @@ public class LatexCreatorConstraints implements StepVisitor {
|
|||||||
public void visit(LetStepDefault letD) {
|
public void visit(LetStepDefault letD) {
|
||||||
addConstraint(letD);
|
addConstraint(letD);
|
||||||
LatexCreatorConstraints subCreator = new LatexCreatorConstraints(letD.getTypeInferer(),
|
LatexCreatorConstraints subCreator = new LatexCreatorConstraints(letD.getTypeInferer(),
|
||||||
constraintSetIndexFactory, constraints.get(constraints.size() - 1) + LATEX_NEW_LINE + NEW_LINE);
|
constraintSetIndexFactory, numberGenerator,
|
||||||
|
constraints.get(constraints.size() - 1) + LATEX_NEW_LINE + NEW_LINE);
|
||||||
constraints.addAll(subCreator.getEverything());
|
constraints.addAll(subCreator.getEverything());
|
||||||
|
|
||||||
// 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
|
||||||
@ -114,6 +130,7 @@ public class LatexCreatorConstraints implements StepVisitor {
|
|||||||
letConstraints = prefix + CONSTRAINT_SET + constraintSetIndex + EQUALS + LATEX_CURLY_LEFT
|
letConstraints = prefix + CONSTRAINT_SET + constraintSetIndex + EQUALS + LATEX_CURLY_LEFT
|
||||||
+ prevStep + LATEX_CURLY_RIGHT;
|
+ prevStep + LATEX_CURLY_RIGHT;
|
||||||
constraints.add(letConstraints);
|
constraints.add(letConstraints);
|
||||||
|
numberGenerator.push();
|
||||||
|
|
||||||
letD.getPremise().accept(this);
|
letD.getPremise().accept(this);
|
||||||
}
|
}
|
||||||
|
@ -0,0 +1,27 @@
|
|||||||
|
package edu.kit.typicalc.view.content.typeinferencecontent;
|
||||||
|
|
||||||
|
import java.util.ArrayList;
|
||||||
|
import java.util.List;
|
||||||
|
|
||||||
|
public class TreeNumberGenerator {
|
||||||
|
private final List<Integer> numbers;
|
||||||
|
private int current;
|
||||||
|
|
||||||
|
protected TreeNumberGenerator() {
|
||||||
|
numbers = new ArrayList<>();
|
||||||
|
current = -1;
|
||||||
|
}
|
||||||
|
|
||||||
|
protected void push() {
|
||||||
|
numbers.add(current);
|
||||||
|
}
|
||||||
|
|
||||||
|
protected void incrementPush() {
|
||||||
|
current++;
|
||||||
|
numbers.add(current);
|
||||||
|
}
|
||||||
|
|
||||||
|
protected List<Integer> getNumbers() {
|
||||||
|
return numbers;
|
||||||
|
}
|
||||||
|
}
|
@ -12,6 +12,8 @@ import edu.kit.typicalc.model.TypeInfererInterface;
|
|||||||
import edu.kit.typicalc.view.content.ControlPanel;
|
import edu.kit.typicalc.view.content.ControlPanel;
|
||||||
import edu.kit.typicalc.view.content.ControlPanelView;
|
import edu.kit.typicalc.view.content.ControlPanelView;
|
||||||
|
|
||||||
|
import java.util.List;
|
||||||
|
|
||||||
@PageTitle("TypeInferenceView")
|
@PageTitle("TypeInferenceView")
|
||||||
@CssImport("./styles/view/type-inference.css")
|
@CssImport("./styles/view/type-inference.css")
|
||||||
public class TypeInferenceView extends VerticalLayout
|
public class TypeInferenceView extends VerticalLayout
|
||||||
@ -24,6 +26,8 @@ public class TypeInferenceView extends VerticalLayout
|
|||||||
private static final String CONTENT_ID = "content";
|
private static final String CONTENT_ID = "content";
|
||||||
private static final String ID = "type-inference-view";
|
private static final String ID = "type-inference-view";
|
||||||
|
|
||||||
|
private final List<Integer> treeNumbers;
|
||||||
|
|
||||||
private int currentStep = 0;
|
private int currentStep = 0;
|
||||||
|
|
||||||
|
|
||||||
@ -45,6 +49,7 @@ public class TypeInferenceView extends VerticalLayout
|
|||||||
scroller.setScrollDirection(Scroller.ScrollDirection.BOTH);
|
scroller.setScrollDirection(Scroller.ScrollDirection.BOTH);
|
||||||
setAlignItems(Alignment.CENTER);
|
setAlignItems(Alignment.CENTER);
|
||||||
add(scroller, controlPanel);
|
add(scroller, controlPanel);
|
||||||
|
treeNumbers = lc.getTreeNumbers();
|
||||||
setContent();
|
setContent();
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -62,38 +67,38 @@ public class TypeInferenceView extends VerticalLayout
|
|||||||
);
|
);
|
||||||
}
|
}
|
||||||
|
|
||||||
private void refreshElements(int currentStep) {
|
private void refreshElements() {
|
||||||
unification.showStep(currentStep);
|
unification.showStep(currentStep);
|
||||||
tree.showStep(currentStep < tree.getStepCount() ? currentStep : tree.getStepCount() - 1);
|
tree.showStep(treeNumbers.get(currentStep));
|
||||||
}
|
}
|
||||||
|
|
||||||
@Override
|
@Override
|
||||||
public void firstStepButton() {
|
public void firstStepButton() {
|
||||||
currentStep = currentStep > tree.getStepCount() && tree.getStepCount() > 0 ? tree.getStepCount() - 1 : 0;
|
currentStep = currentStep > tree.getStepCount() && tree.getStepCount() > 0 ? tree.getStepCount() - 1 : 0;
|
||||||
refreshElements(currentStep);
|
refreshElements();
|
||||||
}
|
}
|
||||||
|
|
||||||
@Override
|
@Override
|
||||||
public void lastStepButton() {
|
public void lastStepButton() {
|
||||||
currentStep = currentStep < tree.getStepCount() - 1 ? tree.getStepCount() - 1 : unification.getStepCount() - 1;
|
currentStep = currentStep < tree.getStepCount() - 1 ? tree.getStepCount() - 1 : unification.getStepCount() - 1;
|
||||||
refreshElements(currentStep);
|
refreshElements();
|
||||||
}
|
}
|
||||||
|
|
||||||
@Override
|
@Override
|
||||||
public void nextStepButton() {
|
public void nextStepButton() {
|
||||||
currentStep = currentStep < unification.getStepCount() - 1 ? currentStep + 1 : currentStep;
|
currentStep = currentStep < unification.getStepCount() - 1 ? currentStep + 1 : currentStep;
|
||||||
refreshElements(currentStep);
|
refreshElements();
|
||||||
}
|
}
|
||||||
|
|
||||||
@Override
|
@Override
|
||||||
public void previousStepButton() {
|
public void previousStepButton() {
|
||||||
currentStep = currentStep > 0 ? currentStep - 1 : currentStep;
|
currentStep = currentStep > 0 ? currentStep - 1 : currentStep;
|
||||||
refreshElements(currentStep);
|
refreshElements();
|
||||||
}
|
}
|
||||||
|
|
||||||
@Override
|
@Override
|
||||||
public void onComponentEvent(AttachEvent attachEvent) {
|
public void onComponentEvent(AttachEvent attachEvent) {
|
||||||
currentStep = 0;
|
currentStep = 0;
|
||||||
refreshElements(currentStep);
|
refreshElements();
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
Loading…
Reference in New Issue
Block a user