This commit is contained in:
ucrhh 2021-02-12 14:08:21 +01:00
parent 6128871223
commit af16a6bd87
6 changed files with 59 additions and 7 deletions

View File

@ -16,6 +16,8 @@ import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.La
* of code are generated: one for the constraints/unification and one for the proof tree.
* The LaTeX code can be rendered by MathJax, so it must only use packages and commands that MathJax supports.
* The LaTeX code is also usable outside of MathJax, in a normal LaTeX document.
*
* @see InferenceStep
*/
public class LatexCreator implements StepVisitor {
private final StringBuilder tree;
@ -62,6 +64,11 @@ public class LatexCreator implements StepVisitor {
return constraintsCreator.getEverything().toArray(new String[0]);
}
/**
* Returns a list of numbers which correlate to the steps should be in during certain steps of the unification.
*
* @return a list of step indices
*/
public List<Integer> getTreeNumbers() {
return constraintsCreator.getTreeNumbers();
}

View File

@ -1,5 +1,8 @@
package edu.kit.typicalc.view.content.typeinferencecontent.latexcreator;
/**
* Provides a list of constants needed for the creation of the LaTeX code.
*/
public final class LatexCreatorConstants {
private LatexCreatorConstants() {
}

View File

@ -10,8 +10,10 @@ import java.util.Optional;
import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.*;
// todo javadoc
/**
* Generates the LaTeX code needed for the MathjaxUnification element, namely the constraints, the unification,
* the MGU and the final type.
*/
public class LatexCreatorConstraints implements StepVisitor {
private static final String FIRST_PREFIX = "";
@ -24,6 +26,12 @@ public class LatexCreatorConstraints implements StepVisitor {
private final String prefix;
private String prevStep;
/**
* Initializes the LatexCreatorConstraints with the right values calculates the strings
* that will be returned in getEverything().
*
* @param typeInferer the source for the generation of the LaTeX code
*/
protected LatexCreatorConstraints(TypeInfererInterface typeInferer) {
this(typeInferer, new ConstraintSetIndexFactory(), new TreeNumberGenerator(), FIRST_PREFIX);
}
@ -47,6 +55,12 @@ public class LatexCreatorConstraints implements StepVisitor {
typeInferer.getFirstInferenceStep().accept(this);
}
/**
* Returns a list of strings, each of the strings represents one step in the collecting of constraints,
* the unification, the mgu and the final type.
*
* @return steps for the MathjaxUnification element to display
*/
protected List<String> getEverything() {
List<String> result = new ArrayList<>(constraints);
@ -70,6 +84,14 @@ public class LatexCreatorConstraints implements StepVisitor {
return result;
}
/**
* Returns a list of numbers that describe in which step the tree should be, fitting to the current step of
* the unification. The list is always the same length as the list provided by getEverything().
* The index stands for the step the unification is in, the Integer at that index stands for the step that the
* tree should be in (at that point).
*
* @return a list describing in which step the tree should be
*/
protected List<Integer> getTreeNumbers() {
return numberGenerator.getNumbers();
}
@ -157,7 +179,7 @@ public class LatexCreatorConstraints implements StepVisitor {
@Override
public void visit(EmptyStep empty) {
// empty steps dont have constraints associated with them
// empty steps don't have constraints associated with them
}
private StringBuilder generateUnificationName() {

View File

@ -29,7 +29,7 @@ public class LatexCreatorTerm implements TermVisitor {
* @return the generated LaTeX code
*/
public String getLatex() {
// remove most outer parentheses if they exist, untested
// todo remove most outer parentheses if they exist, untested
// long count = latex.chars().filter(ch -> ch == PAREN_LEFT).count();
// if (latex.indexOf(String.valueOf(PAREN_LEFT)) == 0
// && latex.indexOf(String.valueOf(PAREN_RIGHT)) == latex.length() - 1

View File

@ -4,15 +4,24 @@ import java.util.ArrayList;
import java.util.Collections;
import java.util.List;
/**
* Generates the steps in which the tree should be during a certain step in unification.
*/
public class TreeNumberGenerator {
private final List<Integer> numbers;
private int current;
/**
* Initializes the TreeNumberGenerator().
*/
protected TreeNumberGenerator() {
numbers = new ArrayList<>();
current = -1;
}
/**
* Push the current index. Translates into the tree not doing anything in this step.
*/
protected void push() {
if (current < 0) {
throw new IllegalStateException("The first step must add a step to the tree");
@ -20,11 +29,19 @@ public class TreeNumberGenerator {
numbers.add(current);
}
/**
* Push an incremented index. Translates into the tree going to the next step.
*/
protected void incrementPush() {
current++;
numbers.add(current);
}
/**
* Returns the resulting list.
*
* @return the list of step indices
*/
protected List<Integer> getNumbers() {
return Collections.unmodifiableList(numbers);
}

View File

@ -31,7 +31,8 @@ class UnificationTest {
Unification u = new Unification(constraints);
List<UnificationStep> steps = u.getUnificationSteps();
assertEquals(2, steps.size());
assertEquals(new UnificationStep(new Result<>(new ArrayList<>()), new ArrayList<>(initialConstraints)), steps.get(0));
assertEquals(new UnificationStep(new Result<>(new ArrayList<>()),
new ArrayList<>(initialConstraints)), steps.get(0));
List<Substitution> substitutions = new ArrayList<>(List.of(new Substitution(a, new FunctionType(b, c))));
assertEquals(new UnificationStep(new Result<>(
substitutions
@ -52,7 +53,8 @@ class UnificationTest {
Unification u = new Unification(constraints);
List<UnificationStep> steps = u.getUnificationSteps();
assertEquals(6, steps.size());
assertEquals(new UnificationStep(new Result<>(new ArrayList<>()), new ArrayList<>(initialConstraints)), steps.get(0));
assertEquals(new UnificationStep(new Result<>(new ArrayList<>()),
new ArrayList<>(initialConstraints)), steps.get(0));
initialConstraints.removeFirst();
List<Substitution> substitutions = new ArrayList<>(List.of(new Substitution(a, new FunctionType(b, c))));
@ -97,7 +99,8 @@ class UnificationTest {
Unification u = new Unification(constraints);
List<UnificationStep> steps = u.getUnificationSteps();
assertEquals(2, steps.size());
assertEquals(new UnificationStep(new Result<>(new ArrayList<>()), new ArrayList<>(initialConstraints)), steps.get(0));
assertEquals(new UnificationStep(new Result<>(new ArrayList<>()),
new ArrayList<>(initialConstraints)), steps.get(0));
assertEquals(new UnificationStep(new Result<>(null,
UnificationError.INFINITE_TYPE
), new ArrayList<>()), steps.get(1));