mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-08 10:20:41 +00:00
Only use hover classes when using Mathjax
This commit is contained in:
Arne Keller
parent
916f73927d
commit
74c21773d4
@ -20,6 +20,7 @@ import edu.kit.typicalc.model.TypeInfererInterface;
|
||||
import edu.kit.typicalc.view.content.ControlPanel;
|
||||
import edu.kit.typicalc.view.content.ControlPanelView;
|
||||
import edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreator;
|
||||
import edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorMode;
|
||||
import edu.kit.typicalc.view.main.TypeInferenceRules;
|
||||
import edu.kit.typicalc.view.main.MainViewImpl;
|
||||
|
||||
@ -62,6 +63,7 @@ public class TypeInferenceView extends VerticalLayout
|
||||
private MathjaxUnification unification;
|
||||
private MathjaxProofTree tree = null;
|
||||
private transient LatexCreator lc;
|
||||
private transient LatexCreator lcUser;
|
||||
private final transient TypeInfererInterface typeInferer;
|
||||
private final Div content;
|
||||
private final ControlPanel controlPanel;
|
||||
@ -136,8 +138,8 @@ public class TypeInferenceView extends VerticalLayout
|
||||
UI.getCurrent().getPage().executeJs("return decodeURI(window.location.href)").then(url ->
|
||||
new ShareDialog(
|
||||
url.asString().replace(" ", "%20"),
|
||||
lc.getTree(),
|
||||
lc.getUnification()[currentStep]).open()
|
||||
lcUser.getTree(),
|
||||
lcUser.getUnification()[currentStep]).open()
|
||||
);
|
||||
}
|
||||
|
||||
@ -197,7 +199,11 @@ public class TypeInferenceView extends VerticalLayout
|
||||
if (typeInferer != null) {
|
||||
content.removeAll();
|
||||
lc = new LatexCreator(typeInferer,
|
||||
error -> getTranslation("root." + error.toString().toLowerCase(Locale.ENGLISH)));
|
||||
error -> getTranslation("root." + error.toString().toLowerCase(Locale.ENGLISH)),
|
||||
LatexCreatorMode.MATHJAX);
|
||||
lcUser = new LatexCreator(typeInferer,
|
||||
error -> getTranslation("root." + error.toString().toLowerCase(Locale.ENGLISH)),
|
||||
LatexCreatorMode.NORMAL);
|
||||
treeNumbers = lc.getTreeNumbers();
|
||||
setContent();
|
||||
refreshElements();
|
||||
|
||||
@ -18,14 +18,15 @@ public final class AssumptionGeneratorUtil {
|
||||
private AssumptionGeneratorUtil() {
|
||||
}
|
||||
|
||||
protected static String typeAssumptionsToLatex(Map<VarTerm, TypeAbstraction> typeAssumptions) {
|
||||
protected static String typeAssumptionsToLatex(Map<VarTerm, TypeAbstraction> typeAssumptions,
|
||||
LatexCreatorMode mode) {
|
||||
if (typeAssumptions.isEmpty()) {
|
||||
return "";
|
||||
} else {
|
||||
StringBuilder assumptions = new StringBuilder();
|
||||
typeAssumptions.forEach(((varTerm, typeAbstraction) -> {
|
||||
String termLatex = new LatexCreatorTerm(varTerm).getLatex();
|
||||
String abstraction = generateTypeAbstraction(typeAbstraction);
|
||||
String abstraction = generateTypeAbstraction(typeAbstraction, mode);
|
||||
assumptions.append(termLatex)
|
||||
.append(COLON)
|
||||
.append(abstraction)
|
||||
@ -36,18 +37,18 @@ public final class AssumptionGeneratorUtil {
|
||||
}
|
||||
}
|
||||
|
||||
protected static String generateTypeAbstraction(TypeAbstraction abs) {
|
||||
protected static String generateTypeAbstraction(TypeAbstraction abs, LatexCreatorMode mode) {
|
||||
StringBuilder abstraction = new StringBuilder();
|
||||
if (abs.hasQuantifiedVariables()) {
|
||||
abstraction.append(FOR_ALL);
|
||||
abs.getQuantifiedVariables().forEach(typeVariable -> {
|
||||
String variableTex = new LatexCreatorType(typeVariable).getLatex();
|
||||
String variableTex = new LatexCreatorType(typeVariable).getLatex(mode);
|
||||
abstraction.append(variableTex).append(COMMA);
|
||||
});
|
||||
abstraction.deleteCharAt(abstraction.length() - 1);
|
||||
abstraction.append(DOT_SIGN);
|
||||
}
|
||||
abstraction.append(new LatexCreatorType(abs.getInnerType()).getLatex());
|
||||
abstraction.append(new LatexCreatorType(abs.getInnerType()).getLatex(mode));
|
||||
return abstraction.toString();
|
||||
}
|
||||
}
|
||||
|
||||
@ -22,6 +22,7 @@ import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.La
|
||||
*/
|
||||
public class LatexCreator implements StepVisitor {
|
||||
private final StringBuilder tree;
|
||||
private final LatexCreatorMode mode;
|
||||
private final boolean stepLabels;
|
||||
private final LatexCreatorConstraints constraintsCreator;
|
||||
|
||||
@ -30,9 +31,11 @@ public class LatexCreator implements StepVisitor {
|
||||
*
|
||||
* @param typeInferer theTypeInfererInterface to create the LaTeX-code from
|
||||
* @param translationProvider translation text provider for {@link UnificationError}
|
||||
* @param mode LaTeX creation mode
|
||||
*/
|
||||
public LatexCreator(TypeInfererInterface typeInferer, Function<UnificationError, String> translationProvider) {
|
||||
this(typeInferer, true, translationProvider);
|
||||
public LatexCreator(TypeInfererInterface typeInferer, Function<UnificationError, String> translationProvider,
|
||||
LatexCreatorMode mode) {
|
||||
this(typeInferer, true, translationProvider, mode);
|
||||
}
|
||||
|
||||
/**
|
||||
@ -41,13 +44,16 @@ public class LatexCreator implements StepVisitor {
|
||||
* @param typeInferer theTypeInfererInterface to create the LaTeX code from
|
||||
* @param stepLabels turns step labels on or off
|
||||
* @param translationProvider translation text provider for {@link UnificationError}
|
||||
* @param mode LaTeX creation mode
|
||||
*/
|
||||
public LatexCreator(TypeInfererInterface typeInferer, boolean stepLabels,
|
||||
Function<UnificationError, String> translationProvider) {
|
||||
Function<UnificationError, String> translationProvider,
|
||||
LatexCreatorMode mode) {
|
||||
this.tree = new StringBuilder();
|
||||
this.mode = mode;
|
||||
this.stepLabels = stepLabels;
|
||||
typeInferer.getFirstInferenceStep().accept(this);
|
||||
this.constraintsCreator = new LatexCreatorConstraints(typeInferer, translationProvider);
|
||||
this.constraintsCreator = new LatexCreatorConstraints(typeInferer, translationProvider, mode);
|
||||
}
|
||||
|
||||
/**
|
||||
@ -78,9 +84,9 @@ public class LatexCreator implements StepVisitor {
|
||||
}
|
||||
|
||||
private String conclusionToLatex(Conclusion conclusion) {
|
||||
String typeAssumptions = typeAssumptionsToLatex(conclusion.getTypeAssumptions());
|
||||
String typeAssumptions = typeAssumptionsToLatex(conclusion.getTypeAssumptions(), mode);
|
||||
String term = new LatexCreatorTerm(conclusion.getLambdaTerm()).getLatex();
|
||||
String type = new LatexCreatorType(conclusion.getType()).getLatex();
|
||||
String type = new LatexCreatorType(conclusion.getType()).getLatex(mode);
|
||||
return DOLLAR_SIGN + typeAssumptions + VDASH + term + COLON + type + DOLLAR_SIGN;
|
||||
}
|
||||
|
||||
@ -98,9 +104,9 @@ public class LatexCreator implements StepVisitor {
|
||||
}
|
||||
|
||||
private String generateVarStepPremise(VarStep var) {
|
||||
String assumptions = typeAssumptionsToLatex(var.getConclusion().getTypeAssumptions());
|
||||
String assumptions = typeAssumptionsToLatex(var.getConclusion().getTypeAssumptions(), mode);
|
||||
String term = new LatexCreatorTerm(var.getConclusion().getLambdaTerm()).getLatex();
|
||||
String type = generateTypeAbstraction(var.getTypeAbsInPremise());
|
||||
String type = generateTypeAbstraction(var.getTypeAbsInPremise(), mode);
|
||||
return PAREN_LEFT + assumptions + PAREN_RIGHT + PAREN_LEFT + term
|
||||
+ PAREN_RIGHT + EQUALS + type;
|
||||
}
|
||||
@ -144,8 +150,8 @@ public class LatexCreator implements StepVisitor {
|
||||
@Override
|
||||
public void visit(VarStepWithLet varL) {
|
||||
tree.insert(0, generateConclusion(varL, LABEL_VAR, UIC));
|
||||
String typeAbstraction = generateTypeAbstraction(varL.getTypeAbsInPremise());
|
||||
String instantiatedType = new LatexCreatorType(varL.getInstantiatedTypeAbs()).getLatex();
|
||||
String typeAbstraction = generateTypeAbstraction(varL.getTypeAbsInPremise(), mode);
|
||||
String instantiatedType = new LatexCreatorType(varL.getInstantiatedTypeAbs()).getLatex(mode);
|
||||
String premiseRight = typeAbstraction + INSTANTIATE_SIGN + instantiatedType;
|
||||
String premiseLeft = AXC + CURLY_LEFT + DOLLAR_SIGN + ALIGN_BEGIN
|
||||
+ generateVarStepPremise(varL)
|
||||
|
||||
@ -37,6 +37,7 @@ public class LatexCreatorConstraints implements StepVisitor {
|
||||
private String prevStep;
|
||||
private final Function<UnificationError, String> translationProvider;
|
||||
private int constraintsInCurrLine;
|
||||
private final LatexCreatorMode mode;
|
||||
|
||||
/**
|
||||
* Initializes the LatexCreatorConstraints with the right values calculates the strings
|
||||
@ -46,10 +47,11 @@ public class LatexCreatorConstraints implements StepVisitor {
|
||||
* @param translationProvider translation text provider for {@link UnificationError}
|
||||
*/
|
||||
protected LatexCreatorConstraints(TypeInfererInterface typeInferer,
|
||||
Function<UnificationError, String> translationProvider) {
|
||||
Function<UnificationError, String> translationProvider,
|
||||
LatexCreatorMode mode) {
|
||||
this(typeInferer,
|
||||
new ConstraintSetIndexFactory(), new TreeNumberGenerator(),
|
||||
FIRST_PREFIX, Optional.empty(), Optional.empty(), translationProvider);
|
||||
FIRST_PREFIX, Optional.empty(), Optional.empty(), translationProvider, mode);
|
||||
}
|
||||
|
||||
private LatexCreatorConstraints(TypeInfererInterface typeInferer,
|
||||
@ -58,7 +60,8 @@ public class LatexCreatorConstraints implements StepVisitor {
|
||||
String prefix,
|
||||
Optional<VarTerm> letVariable,
|
||||
Optional<Map<VarTerm, TypeAbstraction>> newTypeAssumption,
|
||||
Function<UnificationError, String> translationProvider) {
|
||||
Function<UnificationError, String> translationProvider,
|
||||
LatexCreatorMode mode) {
|
||||
this.prefix = prefix;
|
||||
this.letVariable = letVariable;
|
||||
this.newTypeAssumption = newTypeAssumption;
|
||||
@ -74,6 +77,7 @@ public class LatexCreatorConstraints implements StepVisitor {
|
||||
constraints.add(AMPERSAND + CONSTRAINT_SET + EQUALS + LATEX_CURLY_LEFT + LATEX_CURLY_RIGHT);
|
||||
numberGenerator.incrementPush();
|
||||
}
|
||||
this.mode = mode;
|
||||
|
||||
typeInferer.getFirstInferenceStep().accept(this);
|
||||
}
|
||||
@ -129,8 +133,8 @@ public class LatexCreatorConstraints implements StepVisitor {
|
||||
}
|
||||
|
||||
private String createSingleConstraint(Constraint constraint) {
|
||||
String firstType = new LatexCreatorType(constraint.getFirstType()).getLatex();
|
||||
String secondType = new LatexCreatorType(constraint.getSecondType()).getLatex();
|
||||
String firstType = new LatexCreatorType(constraint.getFirstType()).getLatex(mode);
|
||||
String secondType = new LatexCreatorType(constraint.getSecondType()).getLatex(mode);
|
||||
return firstType + EQUALS + secondType;
|
||||
}
|
||||
|
||||
@ -197,7 +201,7 @@ public class LatexCreatorConstraints implements StepVisitor {
|
||||
LatexCreatorConstraints subCreator = new LatexCreatorConstraints(letD.getTypeInferer(),
|
||||
constraintSetIndexFactory, numberGenerator,
|
||||
constraints.get(constraints.size() - 1) + LATEX_NEW_LINE + NEW_LINE, Optional.of(term.getVariable()),
|
||||
newTypeAss, translationProvider);
|
||||
newTypeAss, translationProvider, mode);
|
||||
constraints.addAll(subCreator.getEverything());
|
||||
|
||||
// cancels constraint creation if sub inference failed
|
||||
@ -293,9 +297,9 @@ public class LatexCreatorConstraints implements StepVisitor {
|
||||
sb.append(CURLY_LEFT);
|
||||
sb.append(COLOR_HIGHLIGHTED);
|
||||
}
|
||||
sb.append(new LatexCreatorType(unificationConstraints.get(i).getFirstType()).getLatex());
|
||||
sb.append(new LatexCreatorType(unificationConstraints.get(i).getFirstType()).getLatex(mode));
|
||||
sb.append(EQUALS);
|
||||
sb.append(new LatexCreatorType(unificationConstraints.get(i).getSecondType()).getLatex());
|
||||
sb.append(new LatexCreatorType(unificationConstraints.get(i).getSecondType()).getLatex(mode));
|
||||
if ((markError && i == 0) || markLastTwoConstraints && (i < 2)) {
|
||||
sb.append(CURLY_RIGHT);
|
||||
}
|
||||
@ -306,19 +310,19 @@ public class LatexCreatorConstraints implements StepVisitor {
|
||||
// perform the substitution "manually" and color the new type
|
||||
Substitution s = substitutions.get(substitutions.size() - 1);
|
||||
String original = previousConstraints[invIdx];
|
||||
String originalType = new LatexCreatorType(s.getVariable()).getLatex();
|
||||
String originalType = new LatexCreatorType(s.getVariable()).getLatex(mode);
|
||||
if (original.contains(originalType)) {
|
||||
StringBuilder highlightedChange2 = new StringBuilder();
|
||||
highlightedChange2.append(CURLY_LEFT);
|
||||
highlightedChange2.append(COLOR_HIGHLIGHTED);
|
||||
highlightedChange2.append(new LatexCreatorType(s.getType()).getLatex());
|
||||
highlightedChange2.append(new LatexCreatorType(s.getType()).getLatex(mode));
|
||||
highlightedChange2.append(CURLY_RIGHT);
|
||||
latex.append(original.replace(originalType, highlightedChange2.toString()));
|
||||
} else {
|
||||
latex.append(sb.toString());
|
||||
latex.append(sb);
|
||||
}
|
||||
} else {
|
||||
latex.append(sb.toString());
|
||||
latex.append(sb);
|
||||
}
|
||||
if (i > 0) {
|
||||
latex.append(COMMA);
|
||||
@ -337,9 +341,9 @@ public class LatexCreatorConstraints implements StepVisitor {
|
||||
}
|
||||
latex.append(BRACKET_LEFT);
|
||||
latex.append(AMPERSAND);
|
||||
latex.append(new LatexCreatorType(substitutions.get(i).getVariable()).getLatex());
|
||||
latex.append(new LatexCreatorType(substitutions.get(i).getVariable()).getLatex(mode));
|
||||
latex.append(SUBSTITUTION_SIGN);
|
||||
latex.append(new LatexCreatorType(substitutions.get(i).getType()).getLatex());
|
||||
latex.append(new LatexCreatorType(substitutions.get(i).getType()).getLatex(mode));
|
||||
latex.append(BRACKET_RIGHT);
|
||||
latex.append(LATEX_NEW_LINE);
|
||||
}
|
||||
@ -364,9 +368,9 @@ public class LatexCreatorConstraints implements StepVisitor {
|
||||
latex.append(BRACKET_LEFT);
|
||||
typeInferer.getMGU().ifPresent(mgu -> mgu.forEach(substitution -> {
|
||||
latex.append(AMPERSAND);
|
||||
latex.append(new LatexCreatorType(substitution.getVariable()).getLatex());
|
||||
latex.append(new LatexCreatorType(substitution.getVariable()).getLatex(mode));
|
||||
latex.append(SUBSTITUTION_SIGN);
|
||||
latex.append(new LatexCreatorType(substitution.getType()).getLatex());
|
||||
latex.append(new LatexCreatorType(substitution.getType()).getLatex(mode));
|
||||
latex.append(COMMA);
|
||||
latex.append(LATEX_NEW_LINE);
|
||||
}));
|
||||
@ -382,16 +386,18 @@ public class LatexCreatorConstraints implements StepVisitor {
|
||||
latex.append(SIGMA);
|
||||
latex.append(constraintSetIndex);
|
||||
latex.append(PAREN_LEFT);
|
||||
latex.append(new LatexCreatorType(typeInferer.getFirstInferenceStep().getConclusion().getType()).getLatex());
|
||||
latex.append(
|
||||
new LatexCreatorType(typeInferer.getFirstInferenceStep().getConclusion().getType()).getLatex(mode));
|
||||
latex.append("" + PAREN_RIGHT + EQUALS);
|
||||
latex.append(new LatexCreatorType(typeInferer.getType().orElseThrow(IllegalStateException::new)).getLatex());
|
||||
latex.append(
|
||||
new LatexCreatorType(typeInferer.getType().orElseThrow(IllegalStateException::new)).getLatex(mode));
|
||||
return latex.toString();
|
||||
}
|
||||
|
||||
// generates the TypeAssumptions for the right sub tree of a let step
|
||||
private String generateNewTypeAssumptions(String subPrefix) {
|
||||
InferenceStep step = typeInferer.getFirstInferenceStep();
|
||||
String typeAssumptions = typeAssumptionsToLatex(step.getConclusion().getTypeAssumptions());
|
||||
String typeAssumptions = typeAssumptionsToLatex(step.getConclusion().getTypeAssumptions(), mode);
|
||||
if ("".equals(typeAssumptions)) {
|
||||
typeAssumptions = EMPTY_SET;
|
||||
}
|
||||
@ -407,13 +413,15 @@ public class LatexCreatorConstraints implements StepVisitor {
|
||||
latex.append("" + COLON + TYPE_ABSTRACTION + PAREN_LEFT + SIGMA);
|
||||
latex.append(constraintSetIndex);
|
||||
latex.append(PAREN_LEFT);
|
||||
latex.append(new LatexCreatorType(typeInferer.getFirstInferenceStep().getConclusion().getType()).getLatex());
|
||||
latex.append(
|
||||
new LatexCreatorType(typeInferer.getFirstInferenceStep().getConclusion().getType()).getLatex(mode)
|
||||
);
|
||||
latex.append("" + PAREN_RIGHT + COMMA + SIGMA);
|
||||
latex.append(constraintSetIndex);
|
||||
latex.append(PAREN_LEFT);
|
||||
latex.append(typeAssumptions);
|
||||
latex.append("" + PAREN_RIGHT + PAREN_RIGHT + EQUALS);
|
||||
latex.append(typeAssumptionsToLatex(newTypeAssumption.orElseThrow(IllegalSelectorException::new)));
|
||||
latex.append(typeAssumptionsToLatex(newTypeAssumption.orElseThrow(IllegalSelectorException::new), mode));
|
||||
return latex.toString();
|
||||
}
|
||||
}
|
||||
|
||||
@ -0,0 +1,9 @@
|
||||
package edu.kit.typicalc.view.content.typeinferencecontent.latexcreator;
|
||||
|
||||
/**
|
||||
* Used to switch between different LaTeX generation methods.
|
||||
*/
|
||||
public enum LatexCreatorMode {
|
||||
MATHJAX,
|
||||
NORMAL
|
||||
}
|
||||
@ -34,9 +34,13 @@ public class LatexCreatorType implements TypeVisitor {
|
||||
/**
|
||||
* @return the generated LaTeX code
|
||||
*/
|
||||
protected String getLatex() {
|
||||
protected String getLatex(LatexCreatorMode mode) {
|
||||
if (mode == LatexCreatorMode.MATHJAX) {
|
||||
// this class is used in frontend/src/mathjax-setup.js
|
||||
return "\\class{typicalc-type typicalc-type-" + type.hashCode() + "}{" + latex + "}";
|
||||
} else {
|
||||
return latex.toString();
|
||||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
|
||||
@ -26,7 +26,7 @@ class LatexCreatorConstraintsTest {
|
||||
@Test
|
||||
void singleVarDefaultConstraintTest() {
|
||||
typeInferer = model.getTypeInferer("x", new HashMap<>()).unwrap();
|
||||
List<String> actual = new LatexCreatorConstraints(typeInferer, Enum::toString).getEverything();
|
||||
List<String> actual = new LatexCreatorConstraints(typeInferer, Enum::toString, LatexCreatorMode.NORMAL).getEverything();
|
||||
|
||||
String constraintSet = AMPERSAND + SPLIT_BEGIN + CONSTRAINT_SET + EQUALS + LATEX_CURLY_LEFT + AMPERSAND
|
||||
+ TREE_VARIABLE + "_{1}" + EQUALS + GENERATED_ASSUMPTION_VARIABLE + "_{1}" + LATEX_CURLY_RIGHT
|
||||
@ -56,7 +56,7 @@ class LatexCreatorConstraintsTest {
|
||||
@Test
|
||||
void singleAbsDefaultConstraintTest() {
|
||||
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, LatexCreatorMode.NORMAL).getEverything();
|
||||
|
||||
String constraintSet1 = AMPERSAND + SPLIT_BEGIN + CONSTRAINT_SET + EQUALS + LATEX_CURLY_LEFT + AMPERSAND
|
||||
+ TREE_VARIABLE + "_{1}" + EQUALS + TREE_VARIABLE + "_{2}" + SPACE + RIGHT_ARROW + SPACE
|
||||
@ -104,12 +104,12 @@ class LatexCreatorConstraintsTest {
|
||||
@Test
|
||||
void lineBreak() {
|
||||
typeInferer = model.getTypeInferer("a b c d e f", new HashMap<>()).unwrap();
|
||||
List<String> actual = new LatexCreatorConstraints(typeInferer, Enum::toString).getEverything();
|
||||
List<String> actual = new LatexCreatorConstraints(typeInferer, Enum::toString, LatexCreatorMode.NORMAL).getEverything();
|
||||
|
||||
assertEquals("\\begin{aligned}&\\begin{split}C=\\{&\\alpha_{2}=\\alpha_{3} \\rightarrow \\alpha_{1},\\alpha_{4}=\\alpha_{5} \\rightarrow \\alpha_{2},\\alpha_{6}=\\alpha_{7} \\rightarrow \\alpha_{4},\\alpha_{8}=\\alpha_{9} \\rightarrow \\alpha_{6},\\alpha_{10}=\\alpha_{11} \\rightarrow \\alpha_{8},\\alpha_{10}=\\beta_{1},\\alpha_{11}=\\beta_{2},\\alpha_{9}=\\beta_{3},\\alpha_{7}=\\beta_{4},\\alpha_{5}=\\beta_{5},\\\\&\\alpha_{3}=\\beta_{6}\\}\\end{split}\\end{aligned}", actual.get(11));
|
||||
|
||||
typeInferer = model.getTypeInferer("let g = a b c d e f in g", new HashMap<>()).unwrap();
|
||||
actual = new LatexCreatorConstraints(typeInferer, Enum::toString).getEverything();
|
||||
actual = new LatexCreatorConstraints(typeInferer, Enum::toString, LatexCreatorMode.NORMAL).getEverything();
|
||||
|
||||
assertEquals("\\begin{aligned}&\\begin{split}C=\\{&\\alpha_{1}=\\alpha_{13}\\}\\end{split}\\\\\n" +
|
||||
"&\\begin{split}C_{let}=\\{&\\alpha_{3}=\\alpha_{4} \\rightarrow \\alpha_{2},\\alpha_{5}=\\alpha_{6} \\rightarrow \\alpha_{3},\\alpha_{7}=\\alpha_{8} \\rightarrow \\alpha_{5},\\alpha_{9}=\\alpha_{10} \\rightarrow \\alpha_{7},\\alpha_{11}=\\alpha_{12} \\rightarrow \\alpha_{9},\\alpha_{11}=\\beta_{1},\\alpha_{12}=\\beta_{2},\\alpha_{10}=\\beta_{3},\\alpha_{8}=\\beta_{4},\\alpha_{6}=\\beta_{5},\\\\&\\alpha_{4}=\\beta_{6}\\}\\end{split}\\end{aligned}", actual.get(12));
|
||||
@ -118,7 +118,7 @@ class LatexCreatorConstraintsTest {
|
||||
@Test
|
||||
void emptyLetTypeAssumptions() {
|
||||
typeInferer = model.getTypeInferer("let g = 5 in g", new HashMap<>()).unwrap();
|
||||
List<String> actual = new LatexCreatorConstraints(typeInferer, Enum::toString).getEverything();
|
||||
List<String> actual = new LatexCreatorConstraints(typeInferer, Enum::toString, LatexCreatorMode.NORMAL).getEverything();
|
||||
assertEquals("\\begin{aligned}&\\begin{split}C=\\{&\\alpha_{1}=\\alpha_{3}\\}\\end{split}\\\\\n" +
|
||||
"&\\begin{split}C_{let}=\\{&\\alpha_{2}=\\texttt{int}\\}\\end{split}\\\\&\\begin{split}\\sigma_{let}:=\\textit{mgu}(C_{let})=[&\\alpha_{2}\\mathrel{\\unicode{x21E8}}\\texttt{int}]\\end{split}\\\\&\\sigma_{let}(\\alpha_{2})=\\texttt{int}\\\\&\\Gamma'=\\sigma_{let}(\\emptyset),\\ \\texttt{g}:ta(\\sigma_{let}(\\alpha_{2}),\\sigma_{let}(\\emptyset))=\\texttt{g}:\\texttt{int}\\end{aligned}", actual.get(6));
|
||||
}
|
||||
@ -127,7 +127,7 @@ class LatexCreatorConstraintsTest {
|
||||
void excessiveMemoryUsageAvoided() {
|
||||
try {
|
||||
typeInferer = model.getTypeInferer("(λx.x)(λx.x)(λx.x)(λx.x)(λx.x)(λx.x)(λx.x)(λx.x)(λx.x)(λx.x)(λx.x)(λx.x)", new HashMap<>()).unwrap();
|
||||
List<String> actual = new LatexCreatorConstraints(typeInferer, Enum::toString).getEverything();
|
||||
List<String> actual = new LatexCreatorConstraints(typeInferer, Enum::toString, LatexCreatorMode.NORMAL).getEverything();
|
||||
// should have thrown IllegalStateException by now
|
||||
fail("did not throw exception");
|
||||
} catch (IllegalStateException e) {
|
||||
|
||||
@ -15,7 +15,7 @@ class LatexCreatorTest {
|
||||
@Test
|
||||
void testFailedLet() {
|
||||
TypeInfererInterface typeInferer = model.getTypeInferer("let fun = 5 5 in fun 42", new HashMap<>()).unwrap();
|
||||
String latex = new LatexCreator(typeInferer, Enum::toString).getTree();
|
||||
String latex = new LatexCreator(typeInferer, Enum::toString, LatexCreatorMode.NORMAL).getTree();
|
||||
assertEquals("\\begin{prooftree}\n" +
|
||||
"\\AxiomC{$\\texttt{5} \\in Const$}\n" +
|
||||
"\\LeftLabel{\\textrm C{\\small ONST}}\n" +
|
||||
@ -30,7 +30,7 @@ class LatexCreatorTest {
|
||||
"\\BinaryInfC{$\\vdash\\texttt{\\textbf{let}}\\ \\texttt{fun}=\\texttt{5}\\ \\texttt{5}\\ \\texttt{\\textbf{in}}\\ \\texttt{fun}\\ \\texttt{42}:\\alpha_{1}$}\n" +
|
||||
"\\end{prooftree}", latex);
|
||||
typeInferer = model.getTypeInferer("(let fun = 5 5 in fun) 42", new HashMap<>()).unwrap();
|
||||
latex = new LatexCreator(typeInferer, Enum::toString).getTree();
|
||||
latex = new LatexCreator(typeInferer, Enum::toString, LatexCreatorMode.NORMAL).getTree();
|
||||
assertEquals("\\begin{prooftree}\n" +
|
||||
"\\AxiomC{$\\texttt{5} \\in Const$}\n" +
|
||||
"\\LeftLabel{\\textrm C{\\small ONST}}\n" +
|
||||
|
||||
@ -19,20 +19,21 @@ class LatexCreatorTypeTest {
|
||||
void identityTest() {
|
||||
typeInferer = model.getTypeInferer("λx.x", new HashMap<>()).unwrap();
|
||||
assertEquals(TREE_VARIABLE + "_{2} " + RIGHT_ARROW + SPACE + TREE_VARIABLE + "_{2}",
|
||||
new LatexCreatorType(typeInferer.getType().get()).getLatex());
|
||||
new LatexCreatorType(typeInferer.getType().get()).getLatex(LatexCreatorMode.NORMAL));
|
||||
}
|
||||
|
||||
@Test
|
||||
void generatedTypeTest() {
|
||||
typeInferer = model.getTypeInferer("x", new HashMap<>()).unwrap();
|
||||
assertEquals(GENERATED_ASSUMPTION_VARIABLE + "_{1}",
|
||||
new LatexCreatorType(typeInferer.getType().get()).getLatex());
|
||||
new LatexCreatorType(typeInferer.getType().get()).getLatex(LatexCreatorMode.NORMAL));
|
||||
}
|
||||
|
||||
@Test
|
||||
void namedTypeTest() {
|
||||
typeInferer = model.getTypeInferer("5", new HashMap<>()).unwrap();
|
||||
assertEquals(MONO_TEXT + "{int}", new LatexCreatorType(typeInferer.getType().get()).getLatex());
|
||||
assertEquals(MONO_TEXT + "{int}",
|
||||
new LatexCreatorType(typeInferer.getType().get()).getLatex(LatexCreatorMode.NORMAL));
|
||||
}
|
||||
|
||||
@Test
|
||||
@ -40,6 +41,7 @@ class LatexCreatorTypeTest {
|
||||
HashMap<String, String> map = new HashMap<>();
|
||||
map.put("x", "t1");
|
||||
typeInferer = model.getTypeInferer("x", map).unwrap();
|
||||
assertEquals(USER_VARIABLE + "_{1}", new LatexCreatorType(typeInferer.getType().get()).getLatex());
|
||||
assertEquals(USER_VARIABLE + "_{1}",
|
||||
new LatexCreatorType(typeInferer.getType().get()).getLatex(LatexCreatorMode.NORMAL));
|
||||
}
|
||||
}
|
||||
|
||||
@ -6,5 +6,8 @@
|
||||
<suppressions>
|
||||
<suppress files="src/main/resources/*" checks=".*" />
|
||||
<suppress files="src/test/resources/*" checks=".*" />
|
||||
<suppress
|
||||
files="src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstraints.java"
|
||||
checks="ParameterNumber" />
|
||||
</suppressions>
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user