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

Highlight each type variable separately

Browse Source
This commit is contained in:
Arne Keller 2021-07-05 09:17:37 +02:00
parent a0ae4f08b6
commit 8dd5753ee0
6 changed files with 44 additions and 30 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/AssumptionGeneratorUtil.java
View File

@ -42,13 +42,13 @@ public final class AssumptionGeneratorUtil {
if (abs.hasQuantifiedVariables()) { if (abs.hasQuantifiedVariables()) {
abstraction.append(FOR_ALL); abstraction.append(FOR_ALL);
abs.getQuantifiedVariables().forEach(typeVariable -> { abs.getQuantifiedVariables().forEach(typeVariable -> {
String variableTex = new LatexCreatorType(typeVariable).getLatex(mode); String variableTex = new LatexCreatorType(typeVariable, mode).getLatex();
abstraction.append(variableTex).append(COMMA); abstraction.append(variableTex).append(COMMA);
}); });
abstraction.deleteCharAt(abstraction.length() - 1); abstraction.deleteCharAt(abstraction.length() - 1);
abstraction.append(DOT_SIGN); abstraction.append(DOT_SIGN);
} }
abstraction.append(new LatexCreatorType(abs.getInnerType()).getLatex(mode)); abstraction.append(new LatexCreatorType(abs.getInnerType(), mode).getLatex());
return abstraction.toString(); return abstraction.toString();
} }
} }

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

@ -86,7 +86,7 @@ public class LatexCreator implements StepVisitor {
private String conclusionToLatex(Conclusion conclusion) { private String conclusionToLatex(Conclusion conclusion) {
String typeAssumptions = typeAssumptionsToLatex(conclusion.getTypeAssumptions(), mode); String typeAssumptions = typeAssumptionsToLatex(conclusion.getTypeAssumptions(), mode);
String term = new LatexCreatorTerm(conclusion.getLambdaTerm(), mode).getLatex(); String term = new LatexCreatorTerm(conclusion.getLambdaTerm(), mode).getLatex();
String type = new LatexCreatorType(conclusion.getType()).getLatex(mode); String type = new LatexCreatorType(conclusion.getType(), mode).getLatex();
return DOLLAR_SIGN + typeAssumptions + VDASH + term + COLON + type + DOLLAR_SIGN; return DOLLAR_SIGN + typeAssumptions + VDASH + term + COLON + type + DOLLAR_SIGN;
} }
@ -163,7 +163,7 @@ public class LatexCreator implements StepVisitor {
mode == LatexCreatorMode.MATHJAX ? LABEL_VAR_WITH_CLASS : LABEL_VAR, // TODO: differentiate with let mode == LatexCreatorMode.MATHJAX ? LABEL_VAR_WITH_CLASS : LABEL_VAR, // TODO: differentiate with let
UIC)); UIC));
String typeAbstraction = generateTypeAbstraction(varL.getTypeAbsInPremise(), mode); String typeAbstraction = generateTypeAbstraction(varL.getTypeAbsInPremise(), mode);
String instantiatedType = new LatexCreatorType(varL.getInstantiatedTypeAbs()).getLatex(mode); String instantiatedType = new LatexCreatorType(varL.getInstantiatedTypeAbs(), mode).getLatex();
String premiseRight = typeAbstraction + INSTANTIATE_SIGN + instantiatedType; String premiseRight = typeAbstraction + INSTANTIATE_SIGN + instantiatedType;
String premiseLeft = AXC + CURLY_LEFT + DOLLAR_SIGN + ALIGN_BEGIN String premiseLeft = AXC + CURLY_LEFT + DOLLAR_SIGN + ALIGN_BEGIN
+ generateVarStepPremise(varL) + generateVarStepPremise(varL)

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

@ -133,8 +133,8 @@ public class LatexCreatorConstraints implements StepVisitor {
} }
private String createSingleConstraint(Constraint constraint) { private String createSingleConstraint(Constraint constraint) {
String firstType = new LatexCreatorType(constraint.getFirstType()).getLatex(mode); String firstType = new LatexCreatorType(constraint.getFirstType(), mode).getLatex();
String secondType = new LatexCreatorType(constraint.getSecondType()).getLatex(mode); String secondType = new LatexCreatorType(constraint.getSecondType(), mode).getLatex();
return firstType + EQUALS + secondType; return firstType + EQUALS + secondType;
} }
@ -297,9 +297,9 @@ public class LatexCreatorConstraints implements StepVisitor {
sb.append(CURLY_LEFT); sb.append(CURLY_LEFT);
sb.append(COLOR_HIGHLIGHTED); sb.append(COLOR_HIGHLIGHTED);
} }
sb.append(new LatexCreatorType(unificationConstraints.get(i).getFirstType()).getLatex(mode)); sb.append(new LatexCreatorType(unificationConstraints.get(i).getFirstType(), mode).getLatex());
sb.append(EQUALS); sb.append(EQUALS);
sb.append(new LatexCreatorType(unificationConstraints.get(i).getSecondType()).getLatex(mode)); sb.append(new LatexCreatorType(unificationConstraints.get(i).getSecondType(), mode).getLatex());
if ((markError && i == 0) || markLastTwoConstraints && (i < 2)) { if ((markError && i == 0) || markLastTwoConstraints && (i < 2)) {
sb.append(CURLY_RIGHT); sb.append(CURLY_RIGHT);
} }
@ -310,12 +310,12 @@ public class LatexCreatorConstraints implements StepVisitor {
// perform the substitution "manually" and color the new type // perform the substitution "manually" and color the new type
Substitution s = substitutions.get(substitutions.size() - 1); Substitution s = substitutions.get(substitutions.size() - 1);
String original = previousConstraints[invIdx]; String original = previousConstraints[invIdx];
String originalType = new LatexCreatorType(s.getVariable()).getLatex(mode); String originalType = new LatexCreatorType(s.getVariable(), mode).getLatex();
if (original.contains(originalType)) { if (original.contains(originalType)) {
StringBuilder highlightedChange2 = new StringBuilder(); StringBuilder highlightedChange2 = new StringBuilder();
highlightedChange2.append(CURLY_LEFT); highlightedChange2.append(CURLY_LEFT);
highlightedChange2.append(COLOR_HIGHLIGHTED); highlightedChange2.append(COLOR_HIGHLIGHTED);
highlightedChange2.append(new LatexCreatorType(s.getType()).getLatex(mode)); highlightedChange2.append(new LatexCreatorType(s.getType(), mode).getLatex());
highlightedChange2.append(CURLY_RIGHT); highlightedChange2.append(CURLY_RIGHT);
latex.append(original.replace(originalType, highlightedChange2.toString())); latex.append(original.replace(originalType, highlightedChange2.toString()));
} else { } else {
@ -341,9 +341,9 @@ public class LatexCreatorConstraints implements StepVisitor {
} }
latex.append(BRACKET_LEFT); latex.append(BRACKET_LEFT);
latex.append(AMPERSAND); latex.append(AMPERSAND);
latex.append(new LatexCreatorType(substitutions.get(i).getVariable()).getLatex(mode)); latex.append(new LatexCreatorType(substitutions.get(i).getVariable(), mode).getLatex());
latex.append(SUBSTITUTION_SIGN); latex.append(SUBSTITUTION_SIGN);
latex.append(new LatexCreatorType(substitutions.get(i).getType()).getLatex(mode)); latex.append(new LatexCreatorType(substitutions.get(i).getType(), mode).getLatex());
latex.append(BRACKET_RIGHT); latex.append(BRACKET_RIGHT);
latex.append(LATEX_NEW_LINE); latex.append(LATEX_NEW_LINE);
} }
@ -368,9 +368,9 @@ public class LatexCreatorConstraints implements StepVisitor {
latex.append(BRACKET_LEFT); latex.append(BRACKET_LEFT);
typeInferer.getMGU().ifPresent(mgu -> mgu.forEach(substitution -> { typeInferer.getMGU().ifPresent(mgu -> mgu.forEach(substitution -> {
latex.append(AMPERSAND); latex.append(AMPERSAND);
latex.append(new LatexCreatorType(substitution.getVariable()).getLatex(mode)); latex.append(new LatexCreatorType(substitution.getVariable(), mode).getLatex());
latex.append(SUBSTITUTION_SIGN); latex.append(SUBSTITUTION_SIGN);
latex.append(new LatexCreatorType(substitution.getType()).getLatex(mode)); latex.append(new LatexCreatorType(substitution.getType(), mode).getLatex());
latex.append(COMMA); latex.append(COMMA);
latex.append(LATEX_NEW_LINE); latex.append(LATEX_NEW_LINE);
})); }));
@ -387,10 +387,10 @@ public class LatexCreatorConstraints implements StepVisitor {
latex.append(constraintSetIndex); latex.append(constraintSetIndex);
latex.append(PAREN_LEFT); latex.append(PAREN_LEFT);
latex.append( latex.append(
new LatexCreatorType(typeInferer.getFirstInferenceStep().getConclusion().getType()).getLatex(mode)); new LatexCreatorType(typeInferer.getFirstInferenceStep().getConclusion().getType(), mode).getLatex());
latex.append("" + PAREN_RIGHT + EQUALS); latex.append("" + PAREN_RIGHT + EQUALS);
latex.append( latex.append(
new LatexCreatorType(typeInferer.getType().orElseThrow(IllegalStateException::new)).getLatex(mode)); new LatexCreatorType(typeInferer.getType().orElseThrow(IllegalStateException::new), mode).getLatex());
return latex.toString(); return latex.toString();
} }
@ -414,7 +414,7 @@ public class LatexCreatorConstraints implements StepVisitor {
latex.append(constraintSetIndex); latex.append(constraintSetIndex);
latex.append(PAREN_LEFT); latex.append(PAREN_LEFT);
latex.append( latex.append(
new LatexCreatorType(typeInferer.getFirstInferenceStep().getConclusion().getType()).getLatex(mode) new LatexCreatorType(typeInferer.getFirstInferenceStep().getConclusion().getType(), mode).getLatex()
); );
latex.append("" + PAREN_RIGHT + COMMA + SIGMA); latex.append("" + PAREN_RIGHT + COMMA + SIGMA);
latex.append(constraintSetIndex); latex.append(constraintSetIndex);

31
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorType.java
View File

@ -17,6 +17,7 @@ import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.La
public class LatexCreatorType implements TypeVisitor { public class LatexCreatorType implements TypeVisitor {
private final Type type; private final Type type;
private static final int MAX_LENGTH = 100000; // 100 KB private static final int MAX_LENGTH = 100000; // 100 KB
private final LatexCreatorMode mode;
private final StringBuilder latex = new StringBuilder(); private final StringBuilder latex = new StringBuilder();
private boolean needsParentheses = false; private boolean needsParentheses = false;
@ -26,28 +27,33 @@ public class LatexCreatorType implements TypeVisitor {
* *
* @param type the type * @param type the type
*/ */
protected LatexCreatorType(Type type) { protected LatexCreatorType(Type type, LatexCreatorMode mode) {
this.type = type; this.type = type;
this.mode = mode;
type.accept(this); type.accept(this);
} }
/** /**
* @return the generated LaTeX code * @return the generated LaTeX code
*/ */
protected String getLatex(LatexCreatorMode mode) { protected String getLatex() {
if (mode == LatexCreatorMode.MATHJAX) { return latex.toString();
// this class is used in frontend/src/mathjax-setup.js
return "\\class{typicalc-type typicalc-type-" + type.hashCode() + "}{" + latex + "}";
} else {
return latex.toString();
}
} }
@Override @Override
public void visit(NamedType named) { public void visit(NamedType named) {
latex.append(MONO_TEXT); latex.append(MONO_TEXT);
latex.append(CURLY_LEFT); latex.append(CURLY_LEFT);
if (mode == LatexCreatorMode.MATHJAX) {
// this class is used in frontend/src/mathjax-setup.js
latex.append("\\class{typicalc-type typicalc-type-")
.append(named.hashCode())
.append("}{");
}
latex.append(named.getName()); latex.append(named.getName());
if (mode == LatexCreatorMode.MATHJAX) {
latex.append(CURLY_RIGHT);
}
latex.append(CURLY_RIGHT); latex.append(CURLY_RIGHT);
needsParentheses = false; needsParentheses = false;
} }
@ -68,10 +74,19 @@ public class LatexCreatorType implements TypeVisitor {
default: default:
throw new IllegalStateException("unreachable code"); throw new IllegalStateException("unreachable code");
} }
if (mode == LatexCreatorMode.MATHJAX) {
// this class is used in frontend/src/mathjax-setup.js
latex.append("\\class{typicalc-type typicalc-type-")
.append(variable.hashCode())
.append("}{");
}
latex.append(name); latex.append(name);
latex.append(UNDERSCORE); latex.append(UNDERSCORE);
latex.append(CURLY_LEFT); latex.append(CURLY_LEFT);
latex.append(variable.getIndex()); latex.append(variable.getIndex());
if (mode == LatexCreatorMode.MATHJAX) {
latex.append(CURLY_RIGHT);
}
latex.append(CURLY_RIGHT); latex.append(CURLY_RIGHT);
needsParentheses = false; needsParentheses = false;
} }

1
src/test/java/edu/kit/typicalc/model/ModelImplTest.java
View File

@ -1,7 +1,6 @@
package edu.kit.typicalc.model; package edu.kit.typicalc.model;
import edu.kit.typicalc.model.parser.ParseError; import edu.kit.typicalc.model.parser.ParseError;
import edu.kit.typicalc.model.parser.TypeAssumptionParser;
import edu.kit.typicalc.model.step.AbsStepDefault; import edu.kit.typicalc.model.step.AbsStepDefault;
import edu.kit.typicalc.model.step.VarStepDefault; import edu.kit.typicalc.model.step.VarStepDefault;
import edu.kit.typicalc.model.term.AbsTerm; import edu.kit.typicalc.model.term.AbsTerm;

8
src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorTypeTest.java
View File

@ -19,21 +19,21 @@ class LatexCreatorTypeTest {
void identityTest() { void identityTest() {
typeInferer = model.getTypeInferer("λx.x", new HashMap<>()).unwrap(); typeInferer = model.getTypeInferer("λx.x", new HashMap<>()).unwrap();
assertEquals(TREE_VARIABLE + "_{2} " + RIGHT_ARROW + SPACE + TREE_VARIABLE + "_{2}", assertEquals(TREE_VARIABLE + "_{2} " + RIGHT_ARROW + SPACE + TREE_VARIABLE + "_{2}",
new LatexCreatorType(typeInferer.getType().get()).getLatex(LatexCreatorMode.NORMAL)); new LatexCreatorType(typeInferer.getType().get(), LatexCreatorMode.NORMAL).getLatex());
} }
@Test @Test
void generatedTypeTest() { void generatedTypeTest() {
typeInferer = model.getTypeInferer("x", new HashMap<>()).unwrap(); typeInferer = model.getTypeInferer("x", new HashMap<>()).unwrap();
assertEquals(GENERATED_ASSUMPTION_VARIABLE + "_{1}", assertEquals(GENERATED_ASSUMPTION_VARIABLE + "_{1}",
new LatexCreatorType(typeInferer.getType().get()).getLatex(LatexCreatorMode.NORMAL)); new LatexCreatorType(typeInferer.getType().get(), LatexCreatorMode.NORMAL).getLatex());
} }
@Test @Test
void namedTypeTest() { void namedTypeTest() {
typeInferer = model.getTypeInferer("5", new HashMap<>()).unwrap(); typeInferer = model.getTypeInferer("5", new HashMap<>()).unwrap();
assertEquals(MONO_TEXT + "{int}", assertEquals(MONO_TEXT + "{int}",
new LatexCreatorType(typeInferer.getType().get()).getLatex(LatexCreatorMode.NORMAL)); new LatexCreatorType(typeInferer.getType().get(), LatexCreatorMode.NORMAL).getLatex());
} }
@Test @Test
@ -42,6 +42,6 @@ class LatexCreatorTypeTest {
map.put("x", "t1"); map.put("x", "t1");
typeInferer = model.getTypeInferer("x", map).unwrap(); typeInferer = model.getTypeInferer("x", map).unwrap();
assertEquals(USER_VARIABLE + "_{1}", assertEquals(USER_VARIABLE + "_{1}",
new LatexCreatorType(typeInferer.getType().get()).getLatex(LatexCreatorMode.NORMAL)); new LatexCreatorType(typeInferer.getType().get(), LatexCreatorMode.NORMAL).getLatex());
} }
} }