This commit is contained in:
Johanna Stuber 2021-01-31 14:21:23 +01:00
commit b3e6514bb8
13 changed files with 102 additions and 53 deletions

View File

@ -1,10 +1,7 @@
import {MathjaxAdapter} from "./mathjax-adapter"; import {MathjaxAdapter} from "./mathjax-adapter";
import {TemplateResult} from "lit-html"; import {TemplateResult} from "lit-html";
import {html} from "lit-element";
class MathjaxUnification extends MathjaxAdapter { class MathjaxUnification extends MathjaxAdapter {
private content: String = "Loading...";
private latex: String[] = [];
static get properties() { static get properties() {
return { return {
@ -13,21 +10,12 @@ class MathjaxUnification extends MathjaxAdapter {
} }
render(): TemplateResult { render(): TemplateResult {
return html`<mjx-doc id="mjx-document"><mjx-head></mjx-head><mjx-body> return super.render();
<div id="tc-content">${this.content}</div>
</mjx-body></mjx-doc>`;
} }
protected showStep(n: number): void { protected showStep(_n: number): void {
this.content = this.latex[n];
this.requestTypeset(); this.requestTypeset();
} }
public setTex(tex: String): void {
console.log(tex);
this.latex.push(tex);
console.log(this.latex)
}
} }
customElements.define('tc-unification', MathjaxUnification); customElements.define('tc-unification', MathjaxUnification);

View File

@ -0,0 +1,9 @@
#infoHeader {
width: 30vw;
align-items: center;
justify-content: center;
}
#infoContent {
height: 50vh;
}

View File

@ -101,12 +101,12 @@
"@vaadin/vaadin-time-picker": "2.4.0", "@vaadin/vaadin-time-picker": "2.4.0",
"@vaadin/vaadin-context-menu": "4.5.0", "@vaadin/vaadin-context-menu": "4.5.0",
"@vaadin/vaadin-avatar": "1.0.3", "@vaadin/vaadin-avatar": "1.0.3",
"@vaadin-component-factory/vcf-tooltip": "1.3.13",
"@vaadin/vaadin-radio-button": "1.5.1", "@vaadin/vaadin-radio-button": "1.5.1",
"@vaadin/vaadin-tabs": "3.2.0", "@vaadin/vaadin-tabs": "3.2.0",
"@vaadin/vaadin-lumo-styles": "1.6.0", "@vaadin/vaadin-lumo-styles": "1.6.0",
"@vaadin/vaadin-material-styles": "1.3.2", "@vaadin/vaadin-material-styles": "1.3.2",
"open": "^7.2.1" "open": "^7.2.1",
"@vaadin-component-factory/vcf-tooltip": "1.3.13"
}, },
"devDependencies": { "devDependencies": {
"compression-webpack-plugin": "4.0.1", "compression-webpack-plugin": "4.0.1",

View File

@ -147,11 +147,6 @@
<version>5.7.0</version> <version>5.7.0</version>
<scope>test</scope> <scope>test</scope>
</dependency> </dependency>
<dependency>
<groupId>com.vaadin.componentfactory</groupId>
<artifactId>tooltip</artifactId>
<version>1.3.4</version>
</dependency>
</dependencies> </dependencies>
<build> <build>

View File

@ -14,7 +14,7 @@ import java.util.List;
*/ */
public class TypeInferenceResult { public class TypeInferenceResult {
private final List<Substitution> MGU; private final List<Substitution> mgu;
private final Type finalType; private final Type finalType;
/** /**
@ -27,7 +27,7 @@ public class TypeInferenceResult {
* @param typeVar the type variable belonging to the original lambda term * @param typeVar the type variable belonging to the original lambda term
*/ */
protected TypeInferenceResult(List<Substitution> substitutions, TypeVariable typeVar) { protected TypeInferenceResult(List<Substitution> substitutions, TypeVariable typeVar) {
MGU = new ArrayList<>(substitutions); mgu = new ArrayList<>(substitutions);
findMGU(); findMGU();
MGU.sort(Comparator.comparingInt((Substitution o) -> MGU.sort(Comparator.comparingInt((Substitution o) ->
o.getVariable().getIndex()).thenComparing(o -> o.getVariable().getKind())); o.getVariable().getIndex()).thenComparing(o -> o.getVariable().getKind()));
@ -35,10 +35,10 @@ public class TypeInferenceResult {
} }
private void findMGU() { private void findMGU() {
for (int i = 0; i < MGU.size(); i++) { for (int i = 0; i < mgu.size(); i++) {
Substitution applySub = MGU.get(i); Substitution applySub = mgu.get(i);
for (int j = 0; j < MGU.size(); j++) { for (int j = 0; j < mgu.size(); j++) {
Substitution toSub = MGU.get(j); Substitution toSub = mgu.get(j);
if (i == j) { if (i == j) {
continue; continue;
} else if (applySub.getVariable().equals(toSub.getVariable())) { } else if (applySub.getVariable().equals(toSub.getVariable())) {
@ -49,13 +49,13 @@ public class TypeInferenceResult {
} }
Substitution resultSub = new Substitution(toSub.getVariable(), toSub.getType().substitute(applySub)); Substitution resultSub = new Substitution(toSub.getVariable(), toSub.getType().substitute(applySub));
MGU.set(j, resultSub); mgu.set(j, resultSub);
} }
} }
} }
private Type findFinalType(TypeVariable typeVar) { private Type findFinalType(TypeVariable typeVar) {
for (Substitution substitution : MGU) { for (Substitution substitution : mgu) {
if (substitution.getVariable().equals(typeVar)) { if (substitution.getVariable().equals(typeVar)) {
return substitution.getType(); return substitution.getType();
} }
@ -71,7 +71,7 @@ public class TypeInferenceResult {
* @return the most general unifier, null if there is no valid mgu * @return the most general unifier, null if there is no valid mgu
*/ */
protected List<Substitution> getMGU() { protected List<Substitution> getMGU() {
return MGU; return mgu;
} }
/** /**

View File

@ -2,7 +2,9 @@ package edu.kit.typicalc.view.content.typeinferencecontent;
import com.vaadin.flow.component.Tag; import com.vaadin.flow.component.Tag;
import com.vaadin.flow.component.dependency.JsModule; import com.vaadin.flow.component.dependency.JsModule;
import com.vaadin.flow.component.html.Div;
import com.vaadin.flow.component.littemplate.LitTemplate; import com.vaadin.flow.component.littemplate.LitTemplate;
import com.vaadin.flow.component.template.Id;
import edu.kit.typicalc.view.MathjaxAdapter; import edu.kit.typicalc.view.MathjaxAdapter;
/** /**
@ -16,6 +18,9 @@ public class MathjaxUnification extends LitTemplate implements MathjaxAdapter {
private final String[] latex; private final String[] latex;
@Id("tc-content")
private Div content;
/** /**
* Creates a new HTML element that renders the constraints and unification and * Creates a new HTML element that renders the constraints and unification and
* calculates the steps. * calculates the steps.
@ -23,9 +28,6 @@ public class MathjaxUnification extends LitTemplate implements MathjaxAdapter {
*/ */
public MathjaxUnification(String[] latex) { public MathjaxUnification(String[] latex) {
this.latex = latex; this.latex = latex;
for (String s : latex) {
getElement().callJsFunction("setTex", s);
}
showStep(0); showStep(0);
} }
@ -36,6 +38,10 @@ public class MathjaxUnification extends LitTemplate implements MathjaxAdapter {
@Override @Override
public void showStep(int n) { public void showStep(int n) {
if (n < latex.length) {
content.removeAll();
content.add(latex[n]);
}
getElement().callJsFunction("showStep", n); getElement().callJsFunction("showStep", n);
} }

View File

@ -1,11 +1,14 @@
package edu.kit.typicalc.view.content.typeinferencecontent; package edu.kit.typicalc.view.content.typeinferencecontent;
import com.vaadin.flow.component.AttachEvent;
import com.vaadin.flow.component.ComponentEventListener;
import com.vaadin.flow.component.ComponentUtil; import com.vaadin.flow.component.ComponentUtil;
import com.vaadin.flow.component.UI; import com.vaadin.flow.component.UI;
import com.vaadin.flow.component.html.Div; import com.vaadin.flow.component.html.Div;
import com.vaadin.flow.component.orderedlayout.Scroller; import com.vaadin.flow.component.orderedlayout.Scroller;
import com.vaadin.flow.component.orderedlayout.VerticalLayout; import com.vaadin.flow.component.orderedlayout.VerticalLayout;
import com.vaadin.flow.router.PageTitle; import com.vaadin.flow.router.PageTitle;
import com.vaadin.flow.router.PreserveOnRefresh;
import com.vaadin.flow.router.Route; import com.vaadin.flow.router.Route;
import edu.kit.typicalc.model.TypeInfererInterface; import edu.kit.typicalc.model.TypeInfererInterface;
import edu.kit.typicalc.view.content.ControlPanel; import edu.kit.typicalc.view.content.ControlPanel;
@ -14,8 +17,9 @@ import edu.kit.typicalc.view.main.MainViewImpl;
@Route(value = "visualize", layout = MainViewImpl.class) @Route(value = "visualize", layout = MainViewImpl.class)
@PageTitle("TypeInferenceView") @PageTitle("TypeInferenceView")
@PreserveOnRefresh
public class TypeInferenceView extends VerticalLayout public class TypeInferenceView extends VerticalLayout
implements ControlPanelView { implements ControlPanelView, ComponentEventListener<AttachEvent> {
private int currentStep = 0; private int currentStep = 0;
@ -29,6 +33,7 @@ public class TypeInferenceView extends VerticalLayout
typeInferer = ComponentUtil.getData(UI.getCurrent(), TypeInfererInterface.class); typeInferer = ComponentUtil.getData(UI.getCurrent(), TypeInfererInterface.class);
setId("type-inference-view"); setId("type-inference-view");
setSizeFull(); setSizeFull();
addAttachListener(this);
content = new Div(); content = new Div();
controlPanel = new ControlPanel(this); controlPanel = new ControlPanel(this);
Scroller scroller = new Scroller(content); Scroller scroller = new Scroller(content);
@ -80,4 +85,10 @@ public class TypeInferenceView extends VerticalLayout
currentStep = currentStep > 0 ? currentStep - 1 : currentStep; currentStep = currentStep > 0 ? currentStep - 1 : currentStep;
refreshElements(currentStep); refreshElements(currentStep);
} }
@Override
public void onComponentEvent(AttachEvent attachEvent) {
currentStep = 0;
refreshElements(currentStep);
}
} }

View File

@ -15,7 +15,7 @@ public class DrawerContent extends VerticalLayout implements LocaleChangeObserve
private static final long serialVersionUID = -5751275682270653335L; private static final long serialVersionUID = -5751275682270653335L;
/* /*
* IDs for the imported CSS file * IDs for the imported .css-file
*/ */
private static final String RULE_CONTAINER_ID = "ruleContainer"; private static final String RULE_CONTAINER_ID = "ruleContainer";
private static final String DRAWER_CONTENT_ID = "drawerContent"; private static final String DRAWER_CONTENT_ID = "drawerContent";

View File

@ -17,7 +17,7 @@ public class HelpDialog extends Dialog implements LocaleChangeObserver {
private static final long serialVersionUID = 4470277770276296164L; private static final long serialVersionUID = 4470277770276296164L;
/* /*
* IDs for the imported CSS file * IDs for the imported .css-file
*/ */
private static final String HEADING_LAYOUT_ID = "headingLayout"; private static final String HEADING_LAYOUT_ID = "headingLayout";
private static final String CONTENT_LAYOUT_ID = "contentLayout"; private static final String CONTENT_LAYOUT_ID = "contentLayout";
@ -35,6 +35,7 @@ public class HelpDialog extends Dialog implements LocaleChangeObserver {
headingLayout.add(heading); headingLayout.add(heading);
final VerticalLayout contentLayout = new VerticalLayout(); final VerticalLayout contentLayout = new VerticalLayout();
//TODO inputSyntax wird im inputDialog behandelt --> hier anderer Content
inputSyntax = new H5(getTranslation("root.inputSyntax")); inputSyntax = new H5(getTranslation("root.inputSyntax"));
contentLayout.setId(CONTENT_LAYOUT_ID); contentLayout.setId(CONTENT_LAYOUT_ID);
contentLayout.add(inputSyntax); contentLayout.add(inputSyntax);

View File

@ -24,7 +24,7 @@ public class InferenceRuleField extends VerticalLayout implements LocaleChangeOb
private static final long serialVersionUID = -8551851183297707985L; private static final long serialVersionUID = -8551851183297707985L;
/* /*
* Id's for the imported css-file * IDs for the imported .css-file
*/ */
private static final String INFERENCE_RULE_FIELD_ID = "inferenceRuleField"; private static final String INFERENCE_RULE_FIELD_ID = "inferenceRuleField";
private static final String HEADER_ID = "headerField"; private static final String HEADER_ID = "headerField";

View File

@ -0,0 +1,45 @@
package edu.kit.typicalc.view.main;
import com.vaadin.flow.component.dependency.CssImport;
import com.vaadin.flow.component.dialog.Dialog;
import com.vaadin.flow.component.html.H4;
import com.vaadin.flow.component.orderedlayout.HorizontalLayout;
import com.vaadin.flow.component.orderedlayout.VerticalLayout;
import com.vaadin.flow.i18n.LocaleChangeEvent;
import com.vaadin.flow.i18n.LocaleChangeObserver;
/**
* Dialog which contains information on the correct syntax for the users input.
*/
@CssImport("./styles/view/main/info-dialog.css")
public class InfoDialog extends Dialog implements LocaleChangeObserver {
private static final long serialVersionUID = 2914411566361539614L;
/*
* IDs for the imported .css-file
*/
private static final String INFO_HEADER_ID = "infoHeader";
private static final String INFO_CONTENT_ID = "infoContent";
private final H4 heading;
/**
* Creates new InfoDialog.
*/
protected InfoDialog() {
heading = new H4(getTranslation("root.inputSyntax"));
HorizontalLayout infoHeader = new HorizontalLayout(heading);
infoHeader.setId(INFO_HEADER_ID);
//TODO fill with content
VerticalLayout infoContent = new VerticalLayout();
infoContent.setId(INFO_CONTENT_ID);
add(infoHeader, infoContent);
}
@Override
public void localeChange(LocaleChangeEvent event) {
heading.setText(getTranslation("root.inputSyntax"));
}
}

View File

@ -6,13 +6,10 @@ import java.util.function.Consumer;
import com.vaadin.flow.component.textfield.TextField; import com.vaadin.flow.component.textfield.TextField;
import org.apache.commons.lang3.StringUtils; import org.apache.commons.lang3.StringUtils;
import com.vaadin.componentfactory.Tooltip;
import com.vaadin.componentfactory.TooltipAlignment;
import com.vaadin.componentfactory.TooltipPosition;
import com.vaadin.flow.component.button.Button; import com.vaadin.flow.component.button.Button;
import com.vaadin.flow.component.button.ButtonVariant; import com.vaadin.flow.component.button.ButtonVariant;
import com.vaadin.flow.component.dependency.CssImport; import com.vaadin.flow.component.dependency.CssImport;
import com.vaadin.flow.component.html.H5; import com.vaadin.flow.component.dialog.Dialog;
import com.vaadin.flow.component.icon.Icon; import com.vaadin.flow.component.icon.Icon;
import com.vaadin.flow.component.icon.VaadinIcon; import com.vaadin.flow.component.icon.VaadinIcon;
import com.vaadin.flow.component.orderedlayout.HorizontalLayout; import com.vaadin.flow.component.orderedlayout.HorizontalLayout;
@ -27,12 +24,11 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
private static final long serialVersionUID = -6099700300418752958L; private static final long serialVersionUID = -6099700300418752958L;
/* /*
* Id's for the imported css-file * IDs for the imported .css-file
*/ */
private static final String INPUT_FIELD_ID = "inputField"; private static final String INPUT_FIELD_ID = "inputField";
private static final String INPUT_BAR_ID = "inputBar"; private static final String INPUT_BAR_ID = "inputBar";
private final Tooltip infoTooltip;
private final Icon infoIcon; private final Icon infoIcon;
private final Button exampleButton; private final Button exampleButton;
private final Button lambdaButton; private final Button lambdaButton;
@ -47,10 +43,7 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
*/ */
protected InputBar(final Consumer<String> callback) { protected InputBar(final Consumer<String> callback) {
infoIcon = new Icon(VaadinIcon.INFO_CIRCLE); infoIcon = new Icon(VaadinIcon.INFO_CIRCLE);
// TODO: where is this tooltip supposed to show up? next to icon, currently not working infoIcon.addClickListener(event -> onInfoIconClick());
infoTooltip = new Tooltip(infoIcon, TooltipPosition.LEFT, TooltipAlignment.LEFT);
infoTooltip.add(new H5("Hallo"));
initInfoTooltip();
inputField = new TextField(); inputField = new TextField();
inputField.setId(INPUT_FIELD_ID); inputField.setId(INPUT_FIELD_ID);
@ -68,7 +61,7 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
inferTypeButton = new Button(getTranslation("root.typeInfer"), event -> onTypeInferButtonClick(callback)); inferTypeButton = new Button(getTranslation("root.typeInfer"), event -> onTypeInferButtonClick(callback));
inferTypeButton.addThemeVariants(ButtonVariant.LUMO_PRIMARY); inferTypeButton.addThemeVariants(ButtonVariant.LUMO_PRIMARY);
add(infoTooltip, infoIcon, exampleButton, lambdaButton, inputField, inferTypeButton); add(infoIcon, exampleButton, lambdaButton, inputField, inferTypeButton);
setId(INPUT_BAR_ID); setId(INPUT_BAR_ID);
} }
@ -87,12 +80,13 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
} }
private void onExampleButtonClick() { private void onExampleButtonClick() {
ExampleDialog exampleDialog = new ExampleDialog(inputField::setValue); final Dialog exampleDialog = new ExampleDialog(inputField::setValue);
exampleDialog.open(); exampleDialog.open();
} }
private void initInfoTooltip() { private void onInfoIconClick() {
infoTooltip.add(new H5("Hallo")); final Dialog infoDialog = new InfoDialog();
infoDialog.open();
} }
@Override @Override

View File

@ -21,7 +21,7 @@ public class UpperBar extends HorizontalLayout {
private static final long serialVersionUID = -7344967027514015830L; private static final long serialVersionUID = -7344967027514015830L;
/* /*
* Id's for the imported css-file * IDs for the imported .css-file
*/ */
private static final String VIEW_TITLE_ID = "viewTitle"; private static final String VIEW_TITLE_ID = "viewTitle";
private static final String INPUT_BAR_ID = "inputBar"; private static final String INPUT_BAR_ID = "inputBar";