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

refactor LatexCreatorConstraints

Browse Source
This commit is contained in:
ucrhh 2021-02-06 13:30:13 +01:00
parent b5f114303f
commit e34464f641
5 changed files with 131 additions and 83 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

27
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/ConstraintSetIndexFactory.java Normal file
View File

@ -0,0 +1,27 @@
package edu.kit.typicalc.view.content.typeinferencecontent;
/**
* 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.
*/
public class ConstraintSetIndexFactory {
private static final int FIRST_CONSTRAINT_SET_INDEX = 0;
private int nextConstraintSetIndex;
/**
* Creates a new factory.
*/
protected ConstraintSetIndexFactory() {
nextConstraintSetIndex = FIRST_CONSTRAINT_SET_INDEX;
}
/**
* Returns the next constraint set index.
*
* @return the next constraint set index
*/
public int nextConstraintSetIndex() {
return nextConstraintSetIndex++;
}
}

82
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreator.java
View File

@ -2,20 +2,12 @@ package edu.kit.typicalc.view.content.typeinferencecontent;
import edu.kit.typicalc.model.Conclusion;
import edu.kit.typicalc.model.Constraint;
import edu.kit.typicalc.model.Substitution;
import edu.kit.typicalc.model.TypeInfererInterface;
import edu.kit.typicalc.model.UnificationError;
import edu.kit.typicalc.model.UnificationStep;
import edu.kit.typicalc.model.step.*;
import edu.kit.typicalc.model.term.*;
import edu.kit.typicalc.model.type.*;
import edu.kit.typicalc.util.Result;
import edu.kit.typicalc.model.term.VarTerm;
import edu.kit.typicalc.model.type.TypeAbstraction;
import java.util.ArrayList;
import java.util.List;
import java.util.Map;
import java.util.Optional;
import static edu.kit.typicalc.view.content.typeinferencecontent.LatexCreatorConstants.*;
@ -29,7 +21,6 @@ import static edu.kit.typicalc.view.content.typeinferencecontent.LatexCreatorCon
public class LatexCreator implements StepVisitor {
private final TypeInfererInterface typeInferer;
private final StringBuilder tree;
private final LatexCreatorConstraints constraintsGenerator;
private final boolean stepLabels;
/**
@ -51,7 +42,6 @@ public class LatexCreator implements StepVisitor {
this.typeInferer = typeInferer;
this.tree = new StringBuilder();
this.stepLabels = stepLabels;
constraintsGenerator = new LatexCreatorConstraints(typeInferer);
typeInferer.getFirstInferenceStep().accept(this);
}
@ -70,12 +60,8 @@ public class LatexCreator implements StepVisitor {
* @return the LaTeX-code for constraints and unification
*/
protected String[] getUnification() {
List<String> result = new ArrayList<>(constraintsGenerator.getConstraints());
result.addAll(generateUnification());
typeInferer.getMGU().ifPresent(mgu -> result.add(generateMGU()));
// todo return final type
return result.toArray(new String[0]);
} // todo implement
return new LatexCreatorConstraints(typeInferer).getEverything().toArray(new String[0]);
}
/**
* Returns needed LaTeX packages
@ -107,66 +93,6 @@ public class LatexCreator implements StepVisitor {
}
}
private List<String> generateUnification() {
List<String> steps = new ArrayList<>();
// TODO: check if unification is present
List<UnificationStep> unificationSteps = typeInferer.getUnificationSteps()
.orElseThrow(IllegalStateException::new);
for (UnificationStep step : unificationSteps) {
Result<List<Substitution>, UnificationError> subs = step.getSubstitutions();
Optional<UnificationError> error = Optional.empty();
if (subs.isError()) {
error = Optional.of(subs.unwrapError());
step = unificationSteps.get(unificationSteps.size() - 2);
subs = step.getSubstitutions(); // TODO: what if first step fails?
}
StringBuilder latex = new StringBuilder();
latex.append(DOLLAR_SIGN);
latex.append(ALIGN_BEGIN);
List<Substitution> substitutions = subs.unwrap();
for (Substitution s : substitutions) {
latex.append(new LatexCreatorType(s.getVariable()).getLatex());
latex.append(SUBSTITUTION_SIGN);
latex.append(new LatexCreatorType(s.getType()).getLatex());
latex.append(LATEX_NEW_LINE);
}
error.ifPresent(latex::append); // TODO: translation
if (error.isPresent()) {
latex.append(LATEX_NEW_LINE);
}
List<Constraint> constraints = step.getConstraints();
for (Constraint c : constraints) {
latex.append(new LatexCreatorType(c.getFirstType()).getLatex());
latex.append(EQUALS);
latex.append(new LatexCreatorType(c.getSecondType()).getLatex());
latex.append(LATEX_NEW_LINE);
}
latex.append(ALIGN_END);
latex.append(DOLLAR_SIGN);
steps.add(latex.toString());
}
return steps;
}
private String generateMGU() {
StringBuilder mguLatex = new StringBuilder();
mguLatex.append(DOLLAR_SIGN);
mguLatex.append(ALIGN_BEGIN);
mguLatex.append(BRACKET_LEFT);
typeInferer.getMGU().ifPresent(mgu -> mgu.forEach(substitution -> {
mguLatex.append(new LatexCreatorType(substitution.getVariable()).getLatex());
mguLatex.append(SUBSTITUTION_SIGN);
mguLatex.append(new LatexCreatorType(substitution.getType()).getLatex());
mguLatex.append(COMMA);
mguLatex.append(LATEX_NEW_LINE);
mguLatex.append(NEW_LINE);
}));
mguLatex.delete(mguLatex.length() - 3, mguLatex.length());
mguLatex.append(BRACKET_RIGHT);
mguLatex.append(ALIGN_END);
mguLatex.append(DOLLAR_SIGN);
return mguLatex.toString();
}
private String conclusionToLatex(Conclusion conclusion) {
String typeAssumptions = typeAssumptionsToLatex(conclusion.getTypeAssumptions());

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

@ -7,6 +7,7 @@ public final class LatexCreatorConstants {
protected static final String CONST = "Const";
protected static final String LET = "let";
protected static final String IN = "in";
protected static final String CONSTRAINT_SET = "C";
protected static final String NEW_LINE = "\n";
protected static final String SPACE = " ";
@ -43,6 +44,8 @@ public final class LatexCreatorConstants {
protected static final String SUBSTITUTION_SIGN = "\\mathrel{\\unicode{x21E8}}";
protected static final String LAMBDA = "\\lambda";
protected static final String LATEX_SPACE = "\\ ";
protected static final String LATEX_CURLY_LEFT = "\\{";
protected static final String LATEX_CURLY_RIGHT = "\\}";
protected static final String FOR_ALL = "\\forall";
protected static final String TEXTTT = "\\texttt";
protected static final String TEXTBF = "\\textbf";

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

@ -1,26 +1,55 @@
package edu.kit.typicalc.view.content.typeinferencecontent;
import edu.kit.typicalc.model.TypeInfererInterface;
import edu.kit.typicalc.model.*;
import edu.kit.typicalc.model.step.*;
import edu.kit.typicalc.util.Result;
import java.util.ArrayList;
import java.util.List;
import java.util.Optional;
// todo javadoc
import static edu.kit.typicalc.view.content.typeinferencecontent.LatexCreatorConstants.*;
public class LatexCreatorConstraints implements StepVisitor {
private final List<String> constraints;
private final TypeInfererInterface typeInferer;
private final ConstraintSetIndexFactory constraintSetIndexFactory;
private final int constraintSetIndex;
public LatexCreatorConstraints(TypeInfererInterface typeInferer) {
protected LatexCreatorConstraints(TypeInfererInterface typeInferer) {
this(typeInferer, new ConstraintSetIndexFactory());
}
protected LatexCreatorConstraints(TypeInfererInterface typeInferer,
ConstraintSetIndexFactory constraintSetIndexFactory) {
this.constraintSetIndexFactory = constraintSetIndexFactory;
this.constraintSetIndex = constraintSetIndexFactory.nextConstraintSetIndex();
this.typeInferer = typeInferer;
constraints = new ArrayList<>();
constraints.add(PHANTOM_X);
typeInferer.getFirstInferenceStep().accept(this);
}
protected List<String> getEverything() {
List<String> result = new ArrayList<>(this.getConstraints());
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 -> DOLLAR_SIGN + current + DOLLAR_SIGN);
//todo vllt. noch was anderes drumrum schreiben
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;
}
@ -72,6 +101,7 @@ public class LatexCreatorConstraints implements StepVisitor {
@Override
public void visit(LetStepDefault letD) {
new LatexCreatorConstraints(letD.getTypeInferer(), constraintSetIndexFactory).getEverything();
addConstraint(letD);
letD.getPremise().accept(this);
}
@ -80,4 +110,66 @@ public class LatexCreatorConstraints implements StepVisitor {
public void visit(EmptyStep empty) {
// empty steps dont have constraints associated with them
}
private List<String> generateUnification() {
List<String> steps = new ArrayList<>();
// TODO: check if unification is present
List<UnificationStep> unificationSteps = typeInferer.getUnificationSteps()
.orElseThrow(IllegalStateException::new);
for (UnificationStep step : unificationSteps) {
Result<List<Substitution>, UnificationError> subs = step.getSubstitutions();
Optional<UnificationError> error = Optional.empty();
if (subs.isError()) {
error = Optional.of(subs.unwrapError());
step = unificationSteps.get(unificationSteps.size() - 2);
subs = step.getSubstitutions(); // TODO: what if first step fails?
}
StringBuilder latex = new StringBuilder();
latex.append(DOLLAR_SIGN);
latex.append(ALIGN_BEGIN);
List<Substitution> substitutions = subs.unwrap();
for (Substitution s : substitutions) {
latex.append(new LatexCreatorType(s.getVariable()).getLatex());
latex.append(SUBSTITUTION_SIGN);
latex.append(new LatexCreatorType(s.getType()).getLatex());
latex.append(LATEX_NEW_LINE);
}
error.ifPresent(latex::append); // TODO: translation
if (error.isPresent()) {
latex.append(LATEX_NEW_LINE);
}
List<Constraint> unificationConstraints = step.getConstraints();
for (Constraint c : unificationConstraints) {
latex.append(new LatexCreatorType(c.getFirstType()).getLatex());
latex.append(EQUALS);
latex.append(new LatexCreatorType(c.getSecondType()).getLatex());
latex.append(LATEX_NEW_LINE);
}
latex.append(ALIGN_END);
latex.append(DOLLAR_SIGN);
steps.add(latex.toString());
}
return steps;
}
private String generateMGU() {
StringBuilder mguLatex = new StringBuilder();
mguLatex.append(DOLLAR_SIGN);
mguLatex.append(ALIGN_BEGIN);
mguLatex.append(BRACKET_LEFT);
typeInferer.getMGU().ifPresent(mgu -> mgu.forEach(substitution -> {
mguLatex.append(new LatexCreatorType(substitution.getVariable()).getLatex());
mguLatex.append(SUBSTITUTION_SIGN);
mguLatex.append(new LatexCreatorType(substitution.getType()).getLatex());
mguLatex.append(COMMA);
mguLatex.append(LATEX_NEW_LINE);
mguLatex.append(NEW_LINE);
}));
mguLatex.delete(mguLatex.length() - 3, mguLatex.length());
mguLatex.append(BRACKET_RIGHT);
mguLatex.append(ALIGN_END);
mguLatex.append(DOLLAR_SIGN);
return mguLatex.toString();
}
}

2
src/main/resources/language/general.properties
View File

@ -57,7 +57,7 @@ root.letLatex=\
\\AxiomC{$\\Gamma , \\texttt{x} : ta(\\tau_1 , \\Gamma ) \\vdash t_2 : \\tau_2$}\
\
\\LeftLabel{\\rm L{\\small ET}}\
\\BinaryInfC{$\\Gamma \\vdash\ \\textbf{let} \\ \\texttt{x} = t_1 \\ \\textbf{in} \\ t_2 : \\tau_2$}\
\\BinaryInfC{$\\Gamma \\vdash \\textbf{let} \\ \\texttt{x} = t_1 \\ \\textbf{in} \\ t_2 : \\tau_2$}\
\\end{prooftree}
root.varLetLatex=\