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

Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc

Browse Source
This commit is contained in:
Moritz Dieing 2021-02-06 12:09:40 +01:00
commit c42fd73361
11 changed files with 113 additions and 80 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
frontend/src/mathjax-proof-tree.ts
View File

@ -26,9 +26,10 @@ class MathjaxProofTree extends MathjaxAdapter {
protected calculateSteps(): void {
if (this.shadowRoot !== null) {
const root = this.shadowRoot;
let semanticsMatch = (semantics: string) => semantics.indexOf("bspr_inference:") >= 0;
// first, enumerate all of the steps
let nodeIterator = document.createNodeIterator(this.shadowRoot, NodeFilter.SHOW_ELEMENT);
let nodeIterator = document.createNodeIterator(root, NodeFilter.SHOW_ELEMENT);
let steps = [];
let a = null;
let stepIdx = 0;
@ -44,7 +45,7 @@ class MathjaxProofTree extends MathjaxAdapter {
}
}
// then fix some more mathjax layout issues
for (const step of this.shadowRoot.querySelectorAll<HTMLElement>('g[typicalc="step"]')) {
for (const step of root.querySelectorAll<HTMLElement>('g[typicalc="step"]')) {
const infRule = step.querySelector<HTMLElement>('g[semantics="bspr_inferenceRule:down"]');
if (infRule === null) {
continue;
@ -78,7 +79,7 @@ class MathjaxProofTree extends MathjaxAdapter {
stepAbove.transform.baseVal[0].matrix.e -= dx;
}
// then create the steps
nodeIterator = document.createNodeIterator(this.shadowRoot, NodeFilter.SHOW_ELEMENT);
nodeIterator = document.createNodeIterator(root, NodeFilter.SHOW_ELEMENT);
steps = [];
stepIdx = 0;
while (a = nodeIterator.nextNode() as HTMLElement) {
@ -122,7 +123,7 @@ class MathjaxProofTree extends MathjaxAdapter {
steps.push([a, above]);
}
}
const svg = this.shadowRoot.querySelector<SVGElement>("svg")!;
const svg = root.querySelector<SVGElement>("svg")!;
const nodeIterator2 = [...svg.querySelectorAll<SVGGraphicsElement>("g[data-mml-node='mtr']")];
// start layout fixes in the innermost part of the SVG
nodeIterator2.reverse();
@ -170,9 +171,9 @@ class MathjaxProofTree extends MathjaxAdapter {
i += 1;
}
}
const bbox = (svg.childNodes[1] as SVGGraphicsElement).getBBox();
// TODO: this does not work when using a permalink
svg.setAttribute("viewBox", bbox.x + " " + bbox.y + " " + bbox.width + " " + bbox.height);
// TODO: this does not scale the SVG correctly
//const bbox = (svg.childNodes[1] as SVGGraphicsElement).getBBox();
//svg.setAttribute("viewBox", bbox.x + " " + bbox.y + " " + bbox.width + " " + bbox.height);
if (counter >= 3) {
// should not be used on empty SVGs
// @ts-ignore

13
frontend/styles/view/main/input-bar.css
View File

@ -1,13 +1,5 @@
@media (max-width: 500px) {
#inputField {
width: 20em;
}
}
@media (min-width: 1000px) {
#inputField {
width: 30em;
}
#inputField {
flex-grow: 1;
}
#inputField {
@ -16,6 +8,7 @@
#inputBar {
align-items: center;
padding: 1em;
}
vaadin-drawer-toggle {

26
frontend/styles/view/main/upper-bar.css
View File

@ -20,31 +20,13 @@
}
#helpIcon {
margin-left: auto;
margin-left: 1em;
margin-right: 1em;
}
@media (max-width: 500px) {
#inputBar {
margin: auto;
}
#viewTitle {
margin-right: 5em;
}
}
@media (min-width: 1000px) {
#inputBar {
margin-left: 22em;
}
#viewTitle {
margin-right: auto;
}
#inputBar {
flex-grow: 1;
justify-content: end;
}

3
src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java
View File

@ -63,9 +63,6 @@ public class TypeInferenceResult {
}
}
return typeVar;
// TODO: correct?
// throw new IllegalStateException("MGU has to contain substitution for original type variable: "
// + typeVar.toString());
}
/**

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

@ -41,15 +41,23 @@ public class LatexCreator implements StepVisitor {
this(typeInferer, true);
}
/**
* Generate the pieces of LaTeX-code from the type inferer.
*
* @param typeInferer theTypeInfererInterface to create the LaTeX-code from
* @param stepLabels turns step labels on (true) or off (false)
*/
protected LatexCreator(TypeInfererInterface typeInferer, boolean stepLabels) {
this.typeInferer = typeInferer;
this.tree = new StringBuilder();
this.stepLabels = stepLabels;
constraintsGenerator = new LatexCreatorConstraints();
constraintsGenerator = new LatexCreatorConstraints(typeInferer);
typeInferer.getFirstInferenceStep().accept(this);
}
/**
* Returns the proof tree
*
* @return the LaTeX-code for the proof tree
*/
protected String getTree() {
@ -57,22 +65,29 @@ public class LatexCreator implements StepVisitor {
}
/**
* Returns the LaTeX-code for constraints, unification, MGU and MGU
*
* @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 the packages needed for the LaTeX-code from getTree() and getUnification()to work
* Returns needed LaTeX packages
*
* @return the packages needed for the LaTeX-code from getTree() and getUnification() to work
*/
protected String getLatexPackages() {
return BUSSPROOFS;
} // todo implement
private String typeAssumptionsToLatex(Map<VarTerm, TypeAbstraction> typeAssumptions) {
//todo sort entries?
if (typeAssumptions.isEmpty()) {
@ -107,26 +122,26 @@ public class LatexCreator implements StepVisitor {
}
StringBuilder latex = new StringBuilder();
latex.append(DOLLAR_SIGN);
latex.append("\\begin{align}");
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.append(LATEX_NEW_LINE);
}
error.ifPresent(latex::append); // TODO: translation
if (error.isPresent()) {
latex.append("\\\\");
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.append(LATEX_NEW_LINE);
}
latex.append("\\end{align}");
latex.append(ALIGN_END);
latex.append(DOLLAR_SIGN);
steps.add(latex.toString());
}
@ -136,15 +151,19 @@ public class LatexCreator implements StepVisitor {
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.deleteCharAt(mguLatex.length() - 1);
mguLatex.delete(mguLatex.length() - 3, mguLatex.length());
mguLatex.append(BRACKET_RIGHT);
mguLatex.append(ALIGN_END);
mguLatex.append(DOLLAR_SIGN);
return mguLatex.toString();
}
@ -193,24 +212,20 @@ public class LatexCreator implements StepVisitor {
}
// todo use generateConstraint
@Override
public void visit(AbsStepDefault absD) {
constraintsGenerator.addConstraint(absD);
tree.insert(0, generateConclusion(absD, LABEL_ABS, UIC));
absD.getPremise().accept(this);
}
@Override
public void visit(AbsStepWithLet absL) {
constraintsGenerator.addConstraint(absL);
tree.insert(0, generateConclusion(absL, LABEL_ABS, UIC));
absL.getPremise().accept(this);
}
@Override
public void visit(AppStepDefault appD) {
constraintsGenerator.addConstraint(appD);
tree.insert(0, generateConclusion(appD, LABEL_APP, BIC));
appD.getPremise2().accept(this);
appD.getPremise1().accept(this);
@ -218,7 +233,6 @@ public class LatexCreator implements StepVisitor {
@Override
public void visit(ConstStepDefault constD) {
constraintsGenerator.addConstraint(constD);
tree.insert(0, generateConclusion(constD, LABEL_CONST, UIC));
String visitorBuffer = new LatexCreatorTerm(constD.getConclusion().getLambdaTerm()).getLatex();
String step = AXC + CURLY_LEFT + DOLLAR_SIGN + visitorBuffer + SPACE + LATEX_IN + SPACE + CONST
@ -228,30 +242,27 @@ public class LatexCreator implements StepVisitor {
@Override
public void visit(VarStepDefault varD) {
constraintsGenerator.addConstraint(varD);
tree.insert(0, generateConclusion(varD, LABEL_VAR, UIC));
tree.insert(0, AXC + CURLY_LEFT + generateVarStepPremise(varD) + CURLY_RIGHT + NEW_LINE);
}
@Override
public void visit(VarStepWithLet varL) {
constraintsGenerator.addConstraint(varL);
tree.insert(0, generateConclusion(varL, LABEL_VAR, UIC));
String typeAbstraction = generateTypeAbstraction(varL.getTypeAbsInPremise());
String instantiatedType = new LatexCreatorType(varL.getInstantiatedTypeAbs()).getLatex();
String premiseRight = DOLLAR_SIGN + typeAbstraction + INSTANTIATE_SIGN + instantiatedType
+ DOLLAR_SIGN + NEW_LINE;
String premiseLeft = AXC + CURLY_LEFT + DOLLAR_SIGN + "\\begin{align}"
String premiseLeft = AXC + CURLY_LEFT + DOLLAR_SIGN + ALIGN_BEGIN
+ generateVarStepPremise(varL).replace(DOLLAR_SIGN, "")
+ " \\\\ " // TODO: less magic strings, less replacement fixups
+ SPACE + LATEX_NEW_LINE + SPACE // TODO: less replacement fixups
+ premiseRight.replace(DOLLAR_SIGN, "")
+ "\\end{align}" + DOLLAR_SIGN + CURLY_RIGHT + NEW_LINE;
+ ALIGN_END + DOLLAR_SIGN + CURLY_RIGHT + NEW_LINE;
tree.insert(0, premiseLeft);
}
@Override
public void visit(LetStepDefault letD) {
constraintsGenerator.addConstraint(letD);
tree.insert(0, generateConclusion(letD, LABEL_LET, BIC));
letD.getPremise().accept(this);
letD.getTypeInferer().getFirstInferenceStep().accept(this);

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

@ -38,6 +38,8 @@ public final class LatexCreatorConstants {
protected static final String USER_VARIABLE = "\\tau";
protected static final String GAMMA = "\\Gamma";
protected static final String LATEX_NEW_LINE = "\\\\";
protected static final String PHANTOM_X = "\\phantom{x}";
protected static final String SUBSTITUTION_SIGN = "\\mathrel{\\unicode{x21E8}}";
protected static final String LAMBDA = "\\lambda";
protected static final String LATEX_SPACE = "\\ ";
@ -50,6 +52,8 @@ public final class LatexCreatorConstants {
protected static final String VDASH = "\\vdash";
protected static final String TREE_BEGIN = "\\begin{prooftree}";
protected static final String TREE_END = "\\end{prooftree}";
protected static final String ALIGN_BEGIN = "\\begin{align*}";
protected static final String ALIGN_END = "\\end{align*}";
protected static final String BUSSPROOFS = "\\usepackage{bussproofs}";
}

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

@ -1,25 +1,25 @@
package edu.kit.typicalc.view.content.typeinferencecontent;
import edu.kit.typicalc.model.step.InferenceStep;
import edu.kit.typicalc.model.TypeInfererInterface;
import edu.kit.typicalc.model.step.*;
import java.util.ArrayList;
import java.util.List;
import static edu.kit.typicalc.view.content.typeinferencecontent.LatexCreatorConstants.*;
public class LatexCreatorConstraints {
public class LatexCreatorConstraints implements StepVisitor {
private final List<String> constraints;
public LatexCreatorConstraints() {
public LatexCreatorConstraints(TypeInfererInterface typeInferer) {
constraints = new ArrayList<>();
constraints.add("");
constraints.add(PHANTOM_X);
typeInferer.getFirstInferenceStep().accept(this);
}
protected List<String> getConstraints() {
List<String> temp = new ArrayList<>(constraints);
temp.replaceAll(current -> current.equals("")
? current
: DOLLAR_SIGN + current + DOLLAR_SIGN);
temp.replaceAll(current -> DOLLAR_SIGN + current + DOLLAR_SIGN);
//todo vllt. noch was anderes drumrum schreiben
return temp;
}
@ -35,4 +35,49 @@ public class LatexCreatorConstraints {
constraints.add(currentConstraint);
}
}
@Override
public void visit(AbsStepDefault absD) {
addConstraint(absD);
absD.getPremise().accept(this);
}
@Override
public void visit(AbsStepWithLet absL) {
addConstraint(absL);
absL.getPremise().accept(this);
}
@Override
public void visit(AppStepDefault appD) {
addConstraint(appD);
appD.getPremise1().accept(this);
appD.getPremise2().accept(this);
}
@Override
public void visit(ConstStepDefault constD) {
addConstraint(constD);
}
@Override
public void visit(VarStepDefault varD) {
addConstraint(varD);
}
@Override
public void visit(VarStepWithLet varL) {
addConstraint(varL);
}
@Override
public void visit(LetStepDefault letD) {
addConstraint(letD);
letD.getPremise().accept(this);
}
@Override
public void visit(EmptyStep empty) {
// empty steps dont have constraints associated with them
}
}

14
src/main/java/edu/kit/typicalc/view/main/DrawerContent.java
View File

@ -30,12 +30,14 @@ public class DrawerContent extends VerticalLayout implements LocaleChangeObserve
heading = new H3(getTranslation("root.inferenceRules"));
ruleContainer = new VerticalLayout();
ruleContainer.setId(RULE_CONTAINER_ID);
initRuleContainer();
add(heading, ruleContainer);
setId(DRAWER_CONTENT_ID);
}
private void initRuleContainer() {
@Override
public void localeChange(LocaleChangeEvent event) {
heading.setText(getTranslation("root.inferenceRules"));
ruleContainer.removeAll();
ruleContainer.add(new InferenceRuleField(getTranslation("root.absLatex"), "root.absRule"));
ruleContainer.add(new InferenceRuleField(getTranslation("root.appLatex"), "root.appRule"));
ruleContainer.add(new InferenceRuleField(getTranslation("root.varLatex"), "root.varRule"));
@ -43,13 +45,5 @@ public class DrawerContent extends VerticalLayout implements LocaleChangeObserve
ruleContainer.add(new InferenceRuleField(getTranslation("root.letLatex"), "root.letRule"));
ruleContainer.add(new InferenceRuleField(getTranslation("root.absLetLatex"), "root.absRuleLet"));
ruleContainer.add(new InferenceRuleField(getTranslation("root.varLetLatex"), "root.varRuleLet"));
}
@Override
public void localeChange(LocaleChangeEvent event) {
heading.setText(getTranslation("root.inferenceRules"));
ruleContainer.removeAll();
initRuleContainer();
}
}

2
src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java
View File

@ -23,7 +23,7 @@ public class ExampleDialog extends Dialog implements LocaleChangeObserver {
private static final List<String> EXAMPLES =
List.of("λx.x", "λx.λy.y x", "λx.λy.y (x x)", "let f = λx. g y y in f 3", "(λx.x x) (λx.x x)",
"(λx.λy.y (x x)) (λz. λa. z g a)");
"(λx.λy.y (x y)) (λz. λa. z g a)");
private final Paragraph instruction;
/**

7
src/main/java/edu/kit/typicalc/view/main/InputBar.java
View File

@ -1,6 +1,7 @@
package edu.kit.typicalc.view.main;
import com.vaadin.flow.component.Key;
import com.vaadin.flow.component.UI;
import com.vaadin.flow.component.button.Button;
import com.vaadin.flow.component.button.ButtonVariant;
import com.vaadin.flow.component.dependency.CssImport;
@ -81,7 +82,10 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
*/
protected void inferTerm(String term) {
inputField.setValue(term);
inferTypeButton.click();
// for some reason the Vaadin "click" does not work
//inferTypeButton.click();
UI.getCurrent().getPage().executeJs(
String.format("document.getElementById('%s').click()", INFER_BUTTON_ID));
}
private void onInputFieldValueChange() {
@ -93,6 +97,7 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
String currentInput = inputField.getOptionalValue().orElse(StringUtils.EMPTY);
if (currentInput.length() < MAX_INPUT_LENGTH) {
UI.getCurrent().getPage().setTitle(getTranslation("root.typicalc") + " - " + currentInput);
callback.accept(Pair.of(currentInput, typeAssumptionsArea.getTypeAssumptions()));
} else {
final Notification errorNotification = new ErrorNotification(getTranslation("root.overlongInput"));

1
src/main/java/edu/kit/typicalc/view/main/MainViewImpl.java
View File

@ -30,6 +30,7 @@ import java.util.List;
@JsModule("./styles/shared-styles.js")
@JavaScript("./src/svg-pan-zoom.min.js")
@JavaScript("./src/tex-svg-full.js")
@PageTitle("Typicalc")
public class MainViewImpl extends AppLayout implements MainView, HasErrorParameter<NotFoundException> {
private static final long serialVersionUID = -2411433187835906976L;