From 158760ed5f51fbfed93fe1ffd47d2de3ba60566c Mon Sep 17 00:00:00 2001 From: Moritz Dieing <63721811+moritzdieing@users.noreply.github.com> Date: Fri, 29 Jan 2021 17:15:59 +0100 Subject: [PATCH 01/15] =?UTF-8?q?HelpDialog=20und=20kleinere=20=C3=84nderu?= =?UTF-8?q?ngen?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- frontend/styles/view/main/help-dialog.css | 7 +++ frontend/styles/view/main/upper-bar.css | 4 +- .../kit/typicalc/view/main/ExampleDialog.java | 6 ++- .../kit/typicalc/view/main/HelpDialog.java | 45 +++++++++++++++++++ .../edu/kit/typicalc/view/main/InputBar.java | 27 ++++++----- .../kit/typicalc/view/main/MainViewImpl.java | 10 ++++- .../edu/kit/typicalc/view/main/UpperBar.java | 45 ++++++++++--------- .../language/translation_de.properties | 2 + 8 files changed, 108 insertions(+), 38 deletions(-) create mode 100644 frontend/styles/view/main/help-dialog.css create mode 100644 src/main/java/edu/kit/typicalc/view/main/HelpDialog.java diff --git a/frontend/styles/view/main/help-dialog.css b/frontend/styles/view/main/help-dialog.css new file mode 100644 index 0000000..962f36e --- /dev/null +++ b/frontend/styles/view/main/help-dialog.css @@ -0,0 +1,7 @@ +#contentLayout { + height: 80vh; +} + +#headingLayout { + width: 80vw; +} \ No newline at end of file diff --git a/frontend/styles/view/main/upper-bar.css b/frontend/styles/view/main/upper-bar.css index 17ccd6f..2fc61b3 100644 --- a/frontend/styles/view/main/upper-bar.css +++ b/frontend/styles/view/main/upper-bar.css @@ -16,7 +16,7 @@ cursor: pointer; } -#icon { +#helpIcon { margin-left: auto; margin-right: 1em; } @@ -33,7 +33,7 @@ @media (min-width: 1000px) { #inputBar { - margin-left: 30em; + margin-left: 26em; } #viewTitle { diff --git a/src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java b/src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java index b2e92e5..0b24408 100644 --- a/src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java +++ b/src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java @@ -13,10 +13,12 @@ import java.util.function.Consumer; public class ExampleDialog extends Dialog implements LocaleChangeObserver { private static final List 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)"); + private Paragraph instruction; public ExampleDialog(Consumer callback) { VerticalLayout layout = new VerticalLayout(); - layout.add(new Paragraph(getTranslation("root.selectExample"))); + instruction = new Paragraph(getTranslation("root.selectExample")); + layout.add(instruction); for (String term : EXAMPLES) { Button button = new Button(term); button.addClickListener(click -> callback.accept(term)); @@ -27,6 +29,6 @@ public class ExampleDialog extends Dialog implements LocaleChangeObserver { @Override public void localeChange(LocaleChangeEvent event) { - // TODO + instruction.setText(getTranslation("root.selectExample")); } } diff --git a/src/main/java/edu/kit/typicalc/view/main/HelpDialog.java b/src/main/java/edu/kit/typicalc/view/main/HelpDialog.java new file mode 100644 index 0000000..42f9b64 --- /dev/null +++ b/src/main/java/edu/kit/typicalc/view/main/HelpDialog.java @@ -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.H3; +import com.vaadin.flow.component.html.H5; +import com.vaadin.flow.component.orderedlayout.FlexComponent; +import com.vaadin.flow.component.orderedlayout.FlexComponent.JustifyContentMode; +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; + +@CssImport("./styles/view/main/help-dialog.css") +public class HelpDialog extends Dialog implements LocaleChangeObserver { + + private static final long serialVersionUID = 4470277770276296164L; + + private static final String HEADING_LAYOUT_ID = "headingLayout"; + private static final String CONTENT_LAYOUT_ID = "contentLayout"; + + private final H3 heading; + private final H5 inputSyntax; + + public HelpDialog() { + final HorizontalLayout headingLayout = new HorizontalLayout(); + heading = new H3(getTranslation("root.operatingHelp")); + headingLayout.setId(HEADING_LAYOUT_ID); + headingLayout.add(heading); + headingLayout.setAlignItems(FlexComponent.Alignment.CENTER); + headingLayout.setJustifyContentMode(JustifyContentMode.CENTER); + + final VerticalLayout contentLayout = new VerticalLayout(); + inputSyntax = new H5(getTranslation("root.inputSyntax")); + contentLayout.setId(CONTENT_LAYOUT_ID); + contentLayout.add(inputSyntax); + add(headingLayout, contentLayout); + } + + @Override + public void localeChange(LocaleChangeEvent event) { + heading.setText(getTranslation("root.operatingHelp")); + inputSyntax.setText(getTranslation("root.inputSyntax")); + } +} diff --git a/src/main/java/edu/kit/typicalc/view/main/InputBar.java b/src/main/java/edu/kit/typicalc/view/main/InputBar.java index fb894f2..2c04f3b 100644 --- a/src/main/java/edu/kit/typicalc/view/main/InputBar.java +++ b/src/main/java/edu/kit/typicalc/view/main/InputBar.java @@ -3,7 +3,8 @@ package edu.kit.typicalc.view.main; import java.util.Optional; import java.util.function.Consumer; -import com.vaadin.flow.component.textfield.TextArea; +import com.vaadin.flow.component.textfield.TextField; + import org.apache.commons.lang3.StringUtils; import com.vaadin.componentfactory.Tooltip; import com.vaadin.componentfactory.TooltipAlignment; @@ -25,11 +26,15 @@ import com.vaadin.flow.i18n.LocaleChangeObserver; @CssImport("./styles/view/main/input-bar.css") public class InputBar extends HorizontalLayout implements LocaleChangeObserver { + private static final long serialVersionUID = -6099700300418752958L; + + private static final String INPUT_FIELD_ID = "inputField"; + private final Tooltip infoTooltip; private final Icon infoIcon; private final Button exampleButton; private final Button lambdaButton; - private final TextArea inputField; + private final TextField inputField; private final Button inferTypeButton; /** @@ -40,21 +45,19 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver { */ protected InputBar(final Consumer callback) { infoIcon = new Icon(VaadinIcon.INFO_CIRCLE); - // TODO: where is this tooltip supposed to show up? - infoTooltip = new Tooltip(); + // TODO: where is this tooltip supposed to show up? next to icon, currently not working + infoTooltip = new Tooltip(infoIcon, TooltipPosition.LEFT, TooltipAlignment.LEFT); + infoTooltip.add(new H5("Hallo")); initInfoTooltip(); - infoTooltip.attachToComponent(infoIcon); - infoTooltip.setPosition(TooltipPosition.BOTTOM); - infoTooltip.setAlignment(TooltipAlignment.TOP); - - inputField = new TextArea(); - inputField.setId("inputField"); + + inputField = new TextField(); + inputField.setId(INPUT_FIELD_ID); inputField.setClearButtonVisible(true); //TODO seems to be the only solution to "immediately" parse backslash inputField.addValueChangeListener(event -> { if (inputField.getOptionalValue().isPresent()) { String value = inputField.getValue(); - value = value.replace("\\", "λ"); + value = value.replace("\\", "λ"); //TODO exchange magic strings inputField.setValue(value); } }); @@ -63,7 +66,7 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver { inferTypeButton = new Button(getTranslation("root.typeInfer"), event -> onTypeInferButtonClick(callback)); inferTypeButton.addThemeVariants(ButtonVariant.LUMO_PRIMARY); - add(infoIcon, infoTooltip, exampleButton, lambdaButton, inputField, inferTypeButton); + add(infoTooltip, infoIcon, exampleButton, lambdaButton, inputField, inferTypeButton); setAlignItems(FlexComponent.Alignment.CENTER); } diff --git a/src/main/java/edu/kit/typicalc/view/main/MainViewImpl.java b/src/main/java/edu/kit/typicalc/view/main/MainViewImpl.java index 4a17d4e..8d08958 100644 --- a/src/main/java/edu/kit/typicalc/view/main/MainViewImpl.java +++ b/src/main/java/edu/kit/typicalc/view/main/MainViewImpl.java @@ -9,6 +9,9 @@ import com.vaadin.flow.component.html.Span; import com.vaadin.flow.component.notification.Notification; import com.vaadin.flow.component.notification.Notification.Position; import com.vaadin.flow.component.notification.NotificationVariant; +import com.vaadin.flow.component.orderedlayout.FlexComponent; +import com.vaadin.flow.component.orderedlayout.VerticalLayout; + import edu.kit.typicalc.model.ModelImpl; import edu.kit.typicalc.model.TypeInfererInterface; import edu.kit.typicalc.model.parser.ParseError; @@ -26,6 +29,8 @@ import edu.kit.typicalc.view.content.typeinferencecontent.TypeInferenceView; @JavaScript("./src/tex-svg-full.js") public class MainViewImpl extends AppLayout implements MainView { + private static final long serialVersionUID = -2411433187835906976L; + /** * Creates a new MainViewImpl. */ @@ -44,12 +49,15 @@ public class MainViewImpl extends AppLayout implements MainView { @Override public void displayError(final ParseError error) { //TODO add error keys to bundle + final VerticalLayout container = new VerticalLayout(); final Span errorText = new Span(getTranslation("root." + error.toString())); final Notification errorNotification = new Notification(); final Button closeButton = new Button(getTranslation("root.close"), event -> errorNotification.close()); errorNotification.addThemeVariants(NotificationVariant.LUMO_ERROR); - errorNotification.add(errorText, closeButton); + container.add(errorText, closeButton); + container.setAlignItems(FlexComponent.Alignment.CENTER); + errorNotification.add(container); errorNotification.setPosition(Position.MIDDLE); errorNotification.open(); } diff --git a/src/main/java/edu/kit/typicalc/view/main/UpperBar.java b/src/main/java/edu/kit/typicalc/view/main/UpperBar.java index 3740a8a..bba88c5 100644 --- a/src/main/java/edu/kit/typicalc/view/main/UpperBar.java +++ b/src/main/java/edu/kit/typicalc/view/main/UpperBar.java @@ -4,27 +4,33 @@ import java.util.HashMap; import com.vaadin.flow.component.applayout.DrawerToggle; import com.vaadin.flow.component.dependency.CssImport; +import com.vaadin.flow.component.dialog.Dialog; import com.vaadin.flow.component.html.H1; import com.vaadin.flow.component.icon.Icon; import com.vaadin.flow.component.icon.VaadinIcon; import com.vaadin.flow.component.orderedlayout.FlexComponent; import com.vaadin.flow.component.orderedlayout.HorizontalLayout; -import com.vaadin.flow.i18n.LocaleChangeEvent; -import com.vaadin.flow.i18n.LocaleChangeObserver; import edu.kit.typicalc.view.content.infocontent.StartPageView; import edu.kit.typicalc.view.main.MainView.MainViewListener; -@CssImport("./styles/view/main/upper-bar.css") /** * Contains all the components constantly shown in the upper part of the webage. */ -public class UpperBar extends HorizontalLayout implements LocaleChangeObserver { +@CssImport("./styles/view/main/upper-bar.css") +public class UpperBar extends HorizontalLayout { + + private static final long serialVersionUID = -7344967027514015830L; + + private static final String VIEW_TITLE_ID = "viewTitle"; + private static final String INPUT_BAR_ID = "inputBar"; + private static final String HELP_ICON_ID = "helpIcon"; + private static final String UPPER_BAR_ID = "header"; private final H1 viewTitle; private final InputBar inputBar; - private final Icon helpDialogIcon; + private final Icon helpIcon; - private final MainViewListener presenter; + private final transient MainViewListener presenter; /** * Initializes a new UpperBar with the provided mainViewListener. @@ -35,17 +41,18 @@ public class UpperBar extends HorizontalLayout implements LocaleChangeObserver { this.presenter = presenter; this.viewTitle = new H1(getTranslation("root.typicalc")); - viewTitle.setId("viewTitle"); + viewTitle.setId(VIEW_TITLE_ID); this.inputBar = new InputBar(this::typeInfer); - inputBar.setId("inputBar"); - this.helpDialogIcon = new Icon(VaadinIcon.QUESTION_CIRCLE); - helpDialogIcon.setId("icon"); + inputBar.setId(INPUT_BAR_ID); + this.helpIcon = new Icon(VaadinIcon.QUESTION_CIRCLE); + helpIcon.addClickListener(event -> onHelpIconClick()); + helpIcon.setId(HELP_ICON_ID); viewTitle.addClickListener(event -> this.getUI().get().navigate(StartPageView.class)); - add(new DrawerToggle(), viewTitle, inputBar, helpDialogIcon); - setId("header"); - getThemeList().set("dark", true); // remove magic string + add(new DrawerToggle(), viewTitle, inputBar, helpIcon); + setId(UPPER_BAR_ID); + getThemeList().set("dark", true); //TODO remove magic string setWidthFull(); setSpacing(false); setAlignItems(FlexComponent.Alignment.CENTER); @@ -60,12 +67,8 @@ public class UpperBar extends HorizontalLayout implements LocaleChangeObserver { presenter.typeInferLambdaString(lambdaString, new HashMap<>()); } - private void createHelpDialog() { - //TODO create help dialog here --> maybe move to separate class if too big - } - - @Override - public void localeChange(LocaleChangeEvent event) { - // TODO Auto-generated method stub - } + private void onHelpIconClick() { + Dialog helpDialog = new HelpDialog(); + helpDialog.open(); + } } diff --git a/src/main/resources/language/translation_de.properties b/src/main/resources/language/translation_de.properties index a7fd73b..f681038 100644 --- a/src/main/resources/language/translation_de.properties +++ b/src/main/resources/language/translation_de.properties @@ -5,6 +5,8 @@ root.lambda=\u03BB root.examplebutton=📂 root.selectExample=Beispiel auswählen: root.typeInfer=Typisieren +root.operatingHelp=Bedienhilfen +root.inputSyntax=Eingabe Syntax abs-rule=\ \\begin{prooftree}\ From d294ed54714a74894cc3f165d5f0050cf585e03f Mon Sep 17 00:00:00 2001 From: ucrhh Date: Fri, 29 Jan 2021 17:29:38 +0100 Subject: [PATCH 02/15] change mathjax unifiaction to use String[] --- frontend/src/mathjax-adapter.ts | 13 +++++------ frontend/src/mathjax-display.ts | 4 ---- frontend/src/mathjax-unification.ts | 22 +++++++++++++++--- .../content/infocontent/StartPageView.java | 15 +++++++----- .../typeinferencecontent/LatexCreator.java | 4 ++-- .../MathjaxUnification.java | 23 +++++++++++-------- .../TypeInferenceView.java | 13 ++++------- 7 files changed, 54 insertions(+), 40 deletions(-) diff --git a/frontend/src/mathjax-adapter.ts b/frontend/src/mathjax-adapter.ts index bde069c..39fb896 100644 --- a/frontend/src/mathjax-adapter.ts +++ b/frontend/src/mathjax-adapter.ts @@ -9,13 +9,11 @@ declare let window: { }; export abstract class MathjaxAdapter extends LitElement { - protected execTypeset() { + protected execTypeset(shadowRoot: ShadowRoot | null) { if (window.MathJax !== undefined) { - window.MathJax.typesetShadow(this.shadowRoot, () => this.calculateSteps()); + window.MathJax.typesetShadow(shadowRoot, () => this.calculateSteps()); } } - // @ts-ignore - render(): TemplateResult { return html` @@ -25,14 +23,15 @@ export abstract class MathjaxAdapter extends LitElement { protected abstract showStep(n: number): void; - protected abstract calculateSteps(): void; + protected calculateSteps(): void { + } connectedCallback() { super.connectedCallback(); if (window.MathJax === undefined || !window.MathJax.isInitialized) { - window.addEventListener('mathjax-initialized', () => this.execTypeset()); + window.addEventListener('mathjax-initialized', () => this.execTypeset(this.shadowRoot)); } else { - this.execTypeset(); + this.execTypeset(this.shadowRoot); } } } diff --git a/frontend/src/mathjax-display.ts b/frontend/src/mathjax-display.ts index 1330af9..2bd3c60 100644 --- a/frontend/src/mathjax-display.ts +++ b/frontend/src/mathjax-display.ts @@ -7,12 +7,8 @@ class MathjaxDisplay extends MathjaxAdapter { return super.render(); } - protected showStep(_n: number): void { } - - protected calculateSteps(): void { - } } customElements.define('tc-display', MathjaxDisplay); \ No newline at end of file diff --git a/frontend/src/mathjax-unification.ts b/frontend/src/mathjax-unification.ts index 25baa2b..0ab1c25 100644 --- a/frontend/src/mathjax-unification.ts +++ b/frontend/src/mathjax-unification.ts @@ -1,17 +1,33 @@ import {MathjaxAdapter} from "./mathjax-adapter"; import {TemplateResult} from "lit-html"; +import {html} from "lit-element"; class MathjaxUnification extends MathjaxAdapter { + private content: String = "Loading..."; + private latex: String[] = []; + + static get properties() { + return { + content: {type: String} + } + } render(): TemplateResult { - return super.render(); + return html` +
${this.content}
+ `; } + protected showStep(n: number): void { + this.content = this.latex[n]; + this.updateComplete.then(() => this.execTypeset(this.shadowRoot)); - protected showStep(_n: number): void { } - protected calculateSteps(): void { + public setTex(tex: String): void { + console.log(tex); + this.latex.push(tex); + console.log(this.latex) } } diff --git a/src/main/java/edu/kit/typicalc/view/content/infocontent/StartPageView.java b/src/main/java/edu/kit/typicalc/view/content/infocontent/StartPageView.java index 96c68f7..257efbc 100644 --- a/src/main/java/edu/kit/typicalc/view/content/infocontent/StartPageView.java +++ b/src/main/java/edu/kit/typicalc/view/content/infocontent/StartPageView.java @@ -23,6 +23,7 @@ public class StartPageView extends VerticalLayout implements ControlPanelView { private final Div content; private final ControlPanel controlPanel; MathjaxProofTree mjxPT; + MathjaxUnification mjxU; public StartPageView() { // todo implement correctly @@ -35,17 +36,17 @@ public class StartPageView extends VerticalLayout implements ControlPanelView { scroller.setScrollDirection(Scroller.ScrollDirection.BOTH); setAlignItems(Alignment.CENTER); add(scroller, controlPanel); - disableControlPanel(); +// disableControlPanel(); createContent(); } private void createContent() { + String[] strings = new String[]{"$\\vdash$", "$\\Gamma$"}; content.add(new MathjaxDisplay(getTranslation("abs-rule"))); - content.add(new MathjaxUnification("\\(conswwwwwwWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWW" - + "WWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWW" - + "WWWWWWWWWWWWWWWWWWWWWtraint test \\vdash \\)")); + mjxU = new MathjaxUnification(strings); mjxPT = new MathjaxProofTree(getTranslation("demo-tree")); + content.add(mjxU); content.add(mjxPT); content.add(new MathjaxProofTree(getTranslation("demo-tree"))); content.add(new MathjaxProofTree(getTranslation("demo-tree"))); @@ -55,8 +56,8 @@ public class StartPageView extends VerticalLayout implements ControlPanelView { private void disableControlPanel() { // todo disable everything -// controlPanel.setEnabledFirstStep(false); -// controlPanel.setEnabledLastStep(false); + controlPanel.setEnabledFirstStep(false); + controlPanel.setEnabledLastStep(false); controlPanel.setEnabledNextStep(false); controlPanel.setEnabledPreviousStep(false); controlPanel.setEnabledShareButton(false); @@ -78,9 +79,11 @@ public class StartPageView extends VerticalLayout implements ControlPanelView { @Override public void nextStepButton() { + mjxU.showStep(1); } @Override public void previousStepButton() { + mjxU.showStep(0); } } diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreator.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreator.java index 232ff3e..535be81 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreator.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreator.java @@ -76,7 +76,7 @@ public class LatexCreator implements StepVisitor, TermVisitor, TypeVisitor { /** * @return the LaTeX-code for constraints nad unification */ - protected String getUnification() { + protected String[] getUnification() { return null; } // todo implement @@ -88,7 +88,7 @@ public class LatexCreator implements StepVisitor, TermVisitor, TypeVisitor { } // todo implement private String conclusionToLatex(Conclusion conclusion) { - // todo implement + return "{some text}"; } diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxUnification.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxUnification.java index 3995ea2..b41e216 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxUnification.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxUnification.java @@ -3,11 +3,12 @@ package edu.kit.typicalc.view.content.typeinferencecontent; import com.vaadin.flow.component.ClientCallable; import com.vaadin.flow.component.Tag; 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.template.Id; +import com.vaadin.flow.component.notification.Notification; import edu.kit.typicalc.view.MathjaxAdapter; +import java.util.Arrays; + /** * Renders the constraints and unification from LaTeX using MathJax and allows step-by- * step-revealing capabilities. Relies on MathjaxUnificationJS to interact with MathJax. @@ -18,17 +19,21 @@ import edu.kit.typicalc.view.MathjaxAdapter; public class MathjaxUnification extends LitTemplate implements MathjaxAdapter { private int stepCount = -1; - - @Id("tc-content") - private Div content; +// +// @Id("tc-content") +// private Div content; /** * Creates a new HTML element that renders the constraints and unification and * calculates the steps. - * @param latex the LaTeX-String to render with MathJax + * @param latex the LaTeX-String[] to render with MathJax */ - public MathjaxUnification(String latex) { - content.add(latex); + public MathjaxUnification(String[] latex) { + Notification.show(Arrays.toString(latex)); + for (String s : latex) { + getElement().callJsFunction("setTex", s); + } + showStep(1); } @ClientCallable @@ -43,7 +48,7 @@ public class MathjaxUnification extends LitTemplate implements MathjaxAdapter { @Override public void showStep(int n) { - // todo implement + getElement().callJsFunction("showStep", n); } @Override diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java index 3eb43ef..0dda169 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java @@ -32,15 +32,10 @@ public class TypeInferenceView extends HorizontalLayout } private void buildView(TypeInfererInterface typeInferer) { - if (typeInferer == null) { - // todo throw exception - unification = new MathjaxUnification("\\vdash test"); - tree = new MathjaxProofTree(getTranslation("demo-tree")); - } else { - LatexCreator lc = new LatexCreator(typeInferer); - unification = new MathjaxUnification(lc.getUnification()); - tree = new MathjaxProofTree(lc.getTree()); - } + // todo implement correctly + LatexCreator lc = new LatexCreator(typeInferer); + unification = new MathjaxUnification(lc.getUnification()); + tree = new MathjaxProofTree(lc.getTree()); add(unification); add(new Scroller(tree)); } From 370acda75c0af66a15a75078962350b419ce1c6d Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Fri, 29 Jan 2021 18:23:33 +0100 Subject: [PATCH 03/15] First integration test --- pom.xml | 26 ++++++ .../edu/kit/typicalc/view/AbstractIT.java | 27 ++++++ .../edu/kit/typicalc/view/ScreenshotIT.java | 93 +++++++++++++++++++ .../resources/checkstyle-suppressions.xml | 1 + 4 files changed, 147 insertions(+) create mode 100644 src/test/java/edu/kit/typicalc/view/AbstractIT.java create mode 100644 src/test/java/edu/kit/typicalc/view/ScreenshotIT.java diff --git a/pom.xml b/pom.xml index 1b207e9..14b464f 100644 --- a/pom.xml +++ b/pom.xml @@ -103,6 +103,17 @@ 3.8.1 test + + org.springframework.boot + spring-boot-starter-test + test + + + org.junit.vintage + junit-vintage-engine + + + org.junit.jupiter @@ -172,6 +183,21 @@ maven-surefire-plugin 2.22.2 + + org.apache.maven.plugins + maven-failsafe-plugin + 2.22.2 + + + + integration-test + + + + + false + + org.jacoco jacoco-maven-plugin diff --git a/src/test/java/edu/kit/typicalc/view/AbstractIT.java b/src/test/java/edu/kit/typicalc/view/AbstractIT.java new file mode 100644 index 0000000..117377f --- /dev/null +++ b/src/test/java/edu/kit/typicalc/view/AbstractIT.java @@ -0,0 +1,27 @@ +package edu.kit.typicalc.view; + +import org.junit.Before; +import org.junit.Rule; + +import com.vaadin.testbench.IPAddress; +import com.vaadin.testbench.ScreenshotOnFailureRule; +import com.vaadin.testbench.TestBenchTestCase; +import org.openqa.selenium.firefox.FirefoxDriver; + +/** + * Base class for all our integration tests, allowing us to change the applicable driver, + * test URL or other configurations in one place. + */ +public abstract class AbstractIT extends TestBenchTestCase { + + @Rule + public ScreenshotOnFailureRule rule = new ScreenshotOnFailureRule(this, + true); + + @Before + public void setUp() { + setDriver(new FirefoxDriver()); + getDriver().get("http://127.0.0.1:8080"); + } + +} diff --git a/src/test/java/edu/kit/typicalc/view/ScreenshotIT.java b/src/test/java/edu/kit/typicalc/view/ScreenshotIT.java new file mode 100644 index 0000000..a3528d2 --- /dev/null +++ b/src/test/java/edu/kit/typicalc/view/ScreenshotIT.java @@ -0,0 +1,93 @@ +package edu.kit.typicalc.view; + +import static org.junit.Assert.assertTrue; + +import java.io.File; +import java.io.IOException; + +import edu.kit.typicalc.view.main.MainViewImpl; +import org.junit.Test; +import org.openqa.selenium.HasCapabilities; + +import com.vaadin.testbench.Parameters; +import com.vaadin.testbench.commands.TestBenchCommandExecutor; + +/** + * This example contains usage examples of screenshot comparison feature. + *

+ */ +public class ScreenshotIT extends AbstractIT { + + /** + * We'll want to perform some additional setup functions, so we override the + * setUp() method. + */ + @Override + public void setUp() { + super.setUp(); + + // Set a fixed viewport size so the screenshot is always the same + // resolution + testBench().resizeViewPortTo(1000, 500); + + // Define the directory for reference screenshots and for error files + Parameters.setScreenshotReferenceDirectory("src/test/resources/screenshots"); + Parameters.setScreenshotErrorDirectory("target/screenshot_errors"); + } + + @Test + public void initialView() throws Exception { + // Change this calculation after running the test once to see how errors + // in screenshots are verified. + // The output is placed in target/screenshot_errors + + generateReferenceIfNotFound("initialView"); + + // Compare screen with reference image with id "oneplustwo" from the + // reference image directory. Reference image filenames also contain + // browser, version and platform. + assertTrue( + "Screenshot comparison for 'initialView' failed, see " + + Parameters.getScreenshotErrorDirectory() + + " for error images", + testBench().compareScreen("initialView")); + } + + /** + * Generates a reference screenshot if no reference exists. + *

+ * This method only exists for demonstration purposes. Normally you should + * perform this task manually after verifying that the screenshots look + * correct. + * + * @param referenceId + * the id of the reference image + * @throws IOException + */ + private void generateReferenceIfNotFound(String referenceId) + throws IOException { + String refName = ((TestBenchCommandExecutor) testBench()) + .getReferenceNameGenerator().generateName(referenceId, + ((HasCapabilities) getDriver()).getCapabilities()); + File referenceFile = new File( + Parameters.getScreenshotReferenceDirectory(), refName + ".png"); + if (referenceFile.exists()) { + return; + } + + if (!referenceFile.getParentFile().exists()) { + referenceFile.getParentFile().mkdirs(); + } + + File errorFile = new File(Parameters.getScreenshotErrorDirectory(), + referenceFile.getName()); + + // Take a screenshot and move it to the reference location + testBench().compareScreen(referenceId); + errorFile.renameTo(referenceFile); + + System.out.println("Created new reference file in " + referenceFile); + + } + +} diff --git a/src/test/resources/checkstyle-suppressions.xml b/src/test/resources/checkstyle-suppressions.xml index 0ffc556..0aff2fd 100644 --- a/src/test/resources/checkstyle-suppressions.xml +++ b/src/test/resources/checkstyle-suppressions.xml @@ -5,5 +5,6 @@ + From 19549357bdd4ea72a995c30c5070abebcf70e203 Mon Sep 17 00:00:00 2001 From: Moritz Dieing <63721811+moritzdieing@users.noreply.github.com> Date: Fri, 29 Jan 2021 19:03:15 +0100 Subject: [PATCH 04/15] DrawerContent und RuleField erweitert --- frontend/styles/view/main/drawer-content.css | 11 ++++++ .../kit/typicalc/view/main/DrawerContent.java | 35 +++++++++++++++++-- .../kit/typicalc/view/main/ExampleDialog.java | 5 ++- .../view/main/InferenceRuleField.java | 22 +++++++++--- .../language/translation_de.properties | 2 ++ 5 files changed, 67 insertions(+), 8 deletions(-) create mode 100644 frontend/styles/view/main/drawer-content.css diff --git a/frontend/styles/view/main/drawer-content.css b/frontend/styles/view/main/drawer-content.css new file mode 100644 index 0000000..ffb7a26 --- /dev/null +++ b/frontend/styles/view/main/drawer-content.css @@ -0,0 +1,11 @@ +#ruleContainer { + overflow: auto; + margin: 0; + height: 100%; + max-width: 256px; + padding: 0.5em 0.5em; +} + +#drawerContent { + padding: 0.5em 0; +} \ No newline at end of file diff --git a/src/main/java/edu/kit/typicalc/view/main/DrawerContent.java b/src/main/java/edu/kit/typicalc/view/main/DrawerContent.java index 12ab87a..5327df1 100644 --- a/src/main/java/edu/kit/typicalc/view/main/DrawerContent.java +++ b/src/main/java/edu/kit/typicalc/view/main/DrawerContent.java @@ -1,10 +1,41 @@ package edu.kit.typicalc.view.main; +import com.vaadin.flow.component.dependency.CssImport; +import com.vaadin.flow.component.html.H3; +import com.vaadin.flow.component.orderedlayout.FlexComponent; import com.vaadin.flow.component.orderedlayout.VerticalLayout; +import com.vaadin.flow.i18n.LocaleChangeEvent; +import com.vaadin.flow.i18n.LocaleChangeObserver; -public class DrawerContent extends VerticalLayout { +@CssImport("./styles/view/main/drawer-content.css") +public class DrawerContent extends VerticalLayout implements LocaleChangeObserver { + private static final long serialVersionUID = -5751275682270653335L; + + private static final String RULE_CONTAINER_ID = "ruleContainer"; + private static final String DRAWER_CONTENT_ID = "drawerContent"; + + private final H3 heading; + private final VerticalLayout ruleContainer; + public DrawerContent() { - //TODO implement + heading = new H3(getTranslation("root.inferenceRules")); + ruleContainer = new VerticalLayout(); + ruleContainer.setId(RULE_CONTAINER_ID); + initRuleContainer(); + add(heading, ruleContainer); + setWidthFull(); + setHeightFull(); + setAlignItems(FlexComponent.Alignment.CENTER); + setId(DRAWER_CONTENT_ID); + } + + private void initRuleContainer() { + ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule")); + } + + @Override + public void localeChange(LocaleChangeEvent event) { + heading.setText(getTranslation("root.inferenceRules")); } } diff --git a/src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java b/src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java index 0b24408..6fc8c83 100644 --- a/src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java +++ b/src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java @@ -11,9 +11,12 @@ import java.util.List; import java.util.function.Consumer; public class ExampleDialog extends Dialog implements LocaleChangeObserver { + + private static final long serialVersionUID = 8718432784530464215L; + private static final List 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)"); - private Paragraph instruction; + private final Paragraph instruction; public ExampleDialog(Consumer callback) { VerticalLayout layout = new VerticalLayout(); diff --git a/src/main/java/edu/kit/typicalc/view/main/InferenceRuleField.java b/src/main/java/edu/kit/typicalc/view/main/InferenceRuleField.java index c7908bf..a13e8ce 100644 --- a/src/main/java/edu/kit/typicalc/view/main/InferenceRuleField.java +++ b/src/main/java/edu/kit/typicalc/view/main/InferenceRuleField.java @@ -4,27 +4,39 @@ import com.vaadin.flow.component.UI; import com.vaadin.flow.component.button.Button; import com.vaadin.flow.component.dependency.JsModule; import com.vaadin.flow.component.html.Div; +import com.vaadin.flow.component.html.H5; +import com.vaadin.flow.component.icon.Icon; +import com.vaadin.flow.component.icon.VaadinIcon; import com.vaadin.flow.i18n.LocaleChangeEvent; import com.vaadin.flow.i18n.LocaleChangeObserver; @JsModule("./src/copy-to-clipboard.js") public class InferenceRuleField extends Div implements LocaleChangeObserver { + //TODO add css! + + private static final long serialVersionUID = -8551851183297707985L; + + private static final String INFERENCE_RULE_FIELD_ID = "inferenceRuleField"; - private final String latex; private final String nameKey; private final Button copyButton; + private final H5 ruleName; + private final MathjaxDisplay rule; public InferenceRuleField(final String latex, final String nameKey) { - this.latex = latex; this.nameKey = nameKey; - this.copyButton = new Button(getTranslation("root.copyLatex"), - event -> UI.getCurrent().getPage().executeJs("window.copyToClipboard($0)", latex)); + this.ruleName = new H5(getTranslation(nameKey)); + this.copyButton = new Button(getTranslation("root.copyLatex"), new Icon(VaadinIcon.CLIPBOARD)); + this.rule = new MathjaxDisplay(latex); //TODO scale, when method implemented + copyButton.addClickListener(event -> UI.getCurrent().getPage().executeJs("window.copyToClipboard($0)", latex)); + add(ruleName, rule, copyButton); + setId(INFERENCE_RULE_FIELD_ID); } @Override public void localeChange(LocaleChangeEvent event) { copyButton.setText(getTranslation("root.copyLatex")); - //TODO use nameKey to change name of rule, when attribute is created + ruleName.setText(getTranslation(nameKey)); } } diff --git a/src/main/resources/language/translation_de.properties b/src/main/resources/language/translation_de.properties index f681038..d954056 100644 --- a/src/main/resources/language/translation_de.properties +++ b/src/main/resources/language/translation_de.properties @@ -7,6 +7,8 @@ root.selectExample=Beispiel auswählen: root.typeInfer=Typisieren root.operatingHelp=Bedienhilfen root.inputSyntax=Eingabe Syntax +root.inferenceRules=Ableitungsregeln +root.absRule=Abs-Regel abs-rule=\ \\begin{prooftree}\ From 90c83613d8ee3857503430de96f5427c64ca6af7 Mon Sep 17 00:00:00 2001 From: ucrhh Date: Fri, 29 Jan 2021 19:15:19 +0100 Subject: [PATCH 05/15] make MathjaxUnification consistent to itself --- .../MathjaxUnification.java | 20 ++++--------------- 1 file changed, 4 insertions(+), 16 deletions(-) diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxUnification.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxUnification.java index b41e216..3cd49c0 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxUnification.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxUnification.java @@ -1,14 +1,10 @@ package edu.kit.typicalc.view.content.typeinferencecontent; -import com.vaadin.flow.component.ClientCallable; import com.vaadin.flow.component.Tag; import com.vaadin.flow.component.dependency.JsModule; import com.vaadin.flow.component.littemplate.LitTemplate; -import com.vaadin.flow.component.notification.Notification; import edu.kit.typicalc.view.MathjaxAdapter; -import java.util.Arrays; - /** * Renders the constraints and unification from LaTeX using MathJax and allows step-by- * step-revealing capabilities. Relies on MathjaxUnificationJS to interact with MathJax. @@ -18,10 +14,7 @@ import java.util.Arrays; @JsModule("./src/mathjax-unification.ts") public class MathjaxUnification extends LitTemplate implements MathjaxAdapter { - private int stepCount = -1; -// -// @Id("tc-content") -// private Div content; + private final String[] latex; /** * Creates a new HTML element that renders the constraints and unification and @@ -29,21 +22,16 @@ public class MathjaxUnification extends LitTemplate implements MathjaxAdapter { * @param latex the LaTeX-String[] to render with MathJax */ public MathjaxUnification(String[] latex) { - Notification.show(Arrays.toString(latex)); + this.latex = latex; for (String s : latex) { getElement().callJsFunction("setTex", s); } - showStep(1); - } - - @ClientCallable - private void setStepCount(int stepCount) { - this.stepCount = stepCount; + showStep(0); } @Override public int getStepCount() { - return this.stepCount; + return this.latex.length; } @Override From 31cc4cb235c6fa2f252748f53a3815a4d68d1162 Mon Sep 17 00:00:00 2001 From: ucrhh Date: Fri, 29 Jan 2021 19:31:14 +0100 Subject: [PATCH 06/15] implement button functionality in TypeInferenceView --- .../TypeInferenceView.java | 26 +++++++++---------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java index 0dda169..36c5de6 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java @@ -45,32 +45,32 @@ public class TypeInferenceView extends HorizontalLayout // todo implement } - //todo implement correctly + private void refreshElements(int currentStep) { + unification.showStep(currentStep); + tree.showStep(currentStep < tree.getStepCount() ? currentStep : tree.getStepCount() - 1); + } + @Override public void firstStepButton() { - currentStep = 0; - unification.showStep(currentStep); - tree.showStep(currentStep); + currentStep = currentStep > tree.getStepCount() ? tree.getStepCount() : 0; + refreshElements(currentStep); } @Override public void lastStepButton() { - currentStep = unification.getStepCount() - 1; - unification.showStep(currentStep); - tree.showStep(tree.getStepCount() - 1); + currentStep = currentStep < tree.getStepCount() - 1 ? tree.getStepCount() - 1 : unification.getStepCount() - 1; + refreshElements(currentStep); } @Override public void nextStepButton() { - currentStep++; - unification.showStep(currentStep); - tree.showStep(currentStep); + currentStep = currentStep < unification.getStepCount() - 1 ? currentStep + 1 : currentStep; + refreshElements(currentStep); } @Override public void previousStepButton() { - currentStep--; - unification.showStep(currentStep); - tree.showStep(currentStep); + currentStep = currentStep > 0 ? currentStep - 1 : currentStep; + refreshElements(currentStep); } } From 38399222e5b2d44a0b12c420a89e765d01b41207 Mon Sep 17 00:00:00 2001 From: ucrhh Date: Fri, 29 Jan 2021 19:55:31 +0100 Subject: [PATCH 07/15] test unification and tree reveal --- .../content/infocontent/StartPageView.java | 34 +++++++++++++------ .../TypeInferenceView.java | 2 +- 2 files changed, 24 insertions(+), 12 deletions(-) diff --git a/src/main/java/edu/kit/typicalc/view/content/infocontent/StartPageView.java b/src/main/java/edu/kit/typicalc/view/content/infocontent/StartPageView.java index 257efbc..0fd9bc1 100644 --- a/src/main/java/edu/kit/typicalc/view/content/infocontent/StartPageView.java +++ b/src/main/java/edu/kit/typicalc/view/content/infocontent/StartPageView.java @@ -22,8 +22,8 @@ public class StartPageView extends VerticalLayout implements ControlPanelView { private final Div content; private final ControlPanel controlPanel; - MathjaxProofTree mjxPT; - MathjaxUnification mjxU; + MathjaxProofTree tree; + MathjaxUnification unification; public StartPageView() { // todo implement correctly @@ -42,12 +42,14 @@ public class StartPageView extends VerticalLayout implements ControlPanelView { } private void createContent() { - String[] strings = new String[]{"$\\vdash$", "$\\Gamma$"}; + String[] strings = new String[]{"$\\tau_0$", "$\\tau_1$", "$\\tau_2$", "$\\tau_3$", "$\\tau_4$", + "$\\tau_5$", "$\\tau_6$", "$\\tau_7$", "$\\tau_8$", "$\\tau_9$", "$\\tau_{10}$", "$\\tau_{11}$", + "$\\tau_{12}$", "$\\tau_{13}$", "$\\tau_{14}$"}; content.add(new MathjaxDisplay(getTranslation("abs-rule"))); - mjxU = new MathjaxUnification(strings); - mjxPT = new MathjaxProofTree(getTranslation("demo-tree")); - content.add(mjxU); - content.add(mjxPT); + unification = new MathjaxUnification(strings); + tree = new MathjaxProofTree(getTranslation("demo-tree")); + content.add(unification); + content.add(tree); content.add(new MathjaxProofTree(getTranslation("demo-tree"))); content.add(new MathjaxProofTree(getTranslation("demo-tree"))); content.add(new MathjaxProofTree(getTranslation("demo-tree"))); @@ -67,23 +69,33 @@ public class StartPageView extends VerticalLayout implements ControlPanelView { public void shareButton() { } + private int currentStep = 0; + private void refreshElements(int currentStep) { + unification.showStep(currentStep); + tree.showStep(currentStep < tree.getStepCount() ? currentStep : tree.getStepCount() - 1); + } + @Override public void firstStepButton() { - mjxPT.showStep(0); + currentStep = currentStep > tree.getStepCount() ? tree.getStepCount() - 1 : 0; + refreshElements(currentStep); } @Override public void lastStepButton() { - mjxPT.showStep(5); + currentStep = currentStep < tree.getStepCount() - 1 ? tree.getStepCount() - 1 : unification.getStepCount() - 1; + refreshElements(currentStep); } @Override public void nextStepButton() { - mjxU.showStep(1); + currentStep = currentStep < unification.getStepCount() - 1 ? currentStep + 1 : currentStep; + refreshElements(currentStep); } @Override public void previousStepButton() { - mjxU.showStep(0); + currentStep = currentStep > 0 ? currentStep - 1 : currentStep; + refreshElements(currentStep); } } diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java index 36c5de6..b843e49 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java @@ -52,7 +52,7 @@ public class TypeInferenceView extends HorizontalLayout @Override public void firstStepButton() { - currentStep = currentStep > tree.getStepCount() ? tree.getStepCount() : 0; + currentStep = currentStep > tree.getStepCount() ? tree.getStepCount() - 1 : 0; refreshElements(currentStep); } From 69b9ef47739ea456a3ab43b6dd34598023ce3392 Mon Sep 17 00:00:00 2001 From: Moritz Dieing <63721811+moritzdieing@users.noreply.github.com> Date: Sat, 30 Jan 2021 01:28:53 +0100 Subject: [PATCH 08/15] DrawerContent erweitert + styling und logik besser getrennt --- frontend/styles/view/main/drawer-content.css | 7 +++-- frontend/styles/view/main/help-dialog.css | 2 ++ .../styles/view/main/inference-rule-field.css | 30 ++++++++++++++++++ frontend/styles/view/main/input-bar.css | 4 +++ frontend/styles/view/main/upper-bar.css | 2 ++ .../kit/typicalc/view/main/DrawerContent.java | 12 ++++--- .../kit/typicalc/view/main/HelpDialog.java | 7 ++--- .../view/main/InferenceRuleField.java | 31 ++++++++++++++----- .../edu/kit/typicalc/view/main/InputBar.java | 7 +++-- .../edu/kit/typicalc/view/main/UpperBar.java | 11 +++---- 10 files changed, 88 insertions(+), 25 deletions(-) create mode 100644 frontend/styles/view/main/inference-rule-field.css diff --git a/frontend/styles/view/main/drawer-content.css b/frontend/styles/view/main/drawer-content.css index ffb7a26..587ccc1 100644 --- a/frontend/styles/view/main/drawer-content.css +++ b/frontend/styles/view/main/drawer-content.css @@ -1,11 +1,14 @@ #ruleContainer { overflow: auto; - margin: 0; + margin: 1px; height: 100%; max-width: 256px; - padding: 0.5em 0.5em; + padding: 1.1em 0.5em 0.5em 0.5em; } #drawerContent { padding: 0.5em 0; + width: 100%; + height: 100%; + align-items: center; } \ No newline at end of file diff --git a/frontend/styles/view/main/help-dialog.css b/frontend/styles/view/main/help-dialog.css index 962f36e..19a4375 100644 --- a/frontend/styles/view/main/help-dialog.css +++ b/frontend/styles/view/main/help-dialog.css @@ -4,4 +4,6 @@ #headingLayout { width: 80vw; + align-items: center; + justify-content: center; } \ No newline at end of file diff --git a/frontend/styles/view/main/inference-rule-field.css b/frontend/styles/view/main/inference-rule-field.css new file mode 100644 index 0000000..5b0fd5b --- /dev/null +++ b/frontend/styles/view/main/inference-rule-field.css @@ -0,0 +1,30 @@ +#inferenceRuleField { + display: flex; + align-items: center; + border: 2px solid #e8e8e8; + border-radius: 5px; + box-shadow: 0 4px 8px 0 rgba(0, 0, 0, 0.2), 0 6px 20px 0 rgba(0, 0, 0, 0.19); + margin-top: 0.25em; + margin-bottom: 0.25em; + padding: 0px; +} + +#headerField { + border-bottom: 2px solid #e8e8e8; + background-color: #f8f8f8; + align-items: center; + justify-content: center; + width: 100%; + padding: 0.5em 0em; +} + +#ruleName { + margin: 1px; +} + +#main { + align-items: center; + width: 100%; + margin: 0px; + padding-top: 0.2em; +} \ No newline at end of file diff --git a/frontend/styles/view/main/input-bar.css b/frontend/styles/view/main/input-bar.css index b11cf5b..aae4461 100644 --- a/frontend/styles/view/main/input-bar.css +++ b/frontend/styles/view/main/input-bar.css @@ -13,3 +13,7 @@ #inputField { height: 2.3em; } + +#inputBar { + align-items: center; +} diff --git a/frontend/styles/view/main/upper-bar.css b/frontend/styles/view/main/upper-bar.css index 2fc61b3..67564c1 100644 --- a/frontend/styles/view/main/upper-bar.css +++ b/frontend/styles/view/main/upper-bar.css @@ -1,5 +1,7 @@ #header { height: var(--lumo-size-xl); + width: 100%; + align-items: center; } #header img { diff --git a/src/main/java/edu/kit/typicalc/view/main/DrawerContent.java b/src/main/java/edu/kit/typicalc/view/main/DrawerContent.java index 5327df1..9912688 100644 --- a/src/main/java/edu/kit/typicalc/view/main/DrawerContent.java +++ b/src/main/java/edu/kit/typicalc/view/main/DrawerContent.java @@ -2,7 +2,6 @@ package edu.kit.typicalc.view.main; import com.vaadin.flow.component.dependency.CssImport; import com.vaadin.flow.component.html.H3; -import com.vaadin.flow.component.orderedlayout.FlexComponent; import com.vaadin.flow.component.orderedlayout.VerticalLayout; import com.vaadin.flow.i18n.LocaleChangeEvent; import com.vaadin.flow.i18n.LocaleChangeObserver; @@ -12,6 +11,9 @@ public class DrawerContent extends VerticalLayout implements LocaleChangeObserve private static final long serialVersionUID = -5751275682270653335L; + /* + * Id's for the imported css-file + */ private static final String RULE_CONTAINER_ID = "ruleContainer"; private static final String DRAWER_CONTENT_ID = "drawerContent"; @@ -24,13 +26,15 @@ public class DrawerContent extends VerticalLayout implements LocaleChangeObserve ruleContainer.setId(RULE_CONTAINER_ID); initRuleContainer(); add(heading, ruleContainer); - setWidthFull(); - setHeightFull(); - setAlignItems(FlexComponent.Alignment.CENTER); setId(DRAWER_CONTENT_ID); } private void initRuleContainer() { + //TODO just demo content, exchange with correct rules + ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule")); + ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule")); + ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule")); + ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule")); ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule")); } diff --git a/src/main/java/edu/kit/typicalc/view/main/HelpDialog.java b/src/main/java/edu/kit/typicalc/view/main/HelpDialog.java index 42f9b64..9f96002 100644 --- a/src/main/java/edu/kit/typicalc/view/main/HelpDialog.java +++ b/src/main/java/edu/kit/typicalc/view/main/HelpDialog.java @@ -4,8 +4,6 @@ import com.vaadin.flow.component.dependency.CssImport; import com.vaadin.flow.component.dialog.Dialog; import com.vaadin.flow.component.html.H3; import com.vaadin.flow.component.html.H5; -import com.vaadin.flow.component.orderedlayout.FlexComponent; -import com.vaadin.flow.component.orderedlayout.FlexComponent.JustifyContentMode; import com.vaadin.flow.component.orderedlayout.HorizontalLayout; import com.vaadin.flow.component.orderedlayout.VerticalLayout; import com.vaadin.flow.i18n.LocaleChangeEvent; @@ -16,6 +14,9 @@ public class HelpDialog extends Dialog implements LocaleChangeObserver { private static final long serialVersionUID = 4470277770276296164L; + /* + * Id's for the imported css-file + */ private static final String HEADING_LAYOUT_ID = "headingLayout"; private static final String CONTENT_LAYOUT_ID = "contentLayout"; @@ -27,8 +28,6 @@ public class HelpDialog extends Dialog implements LocaleChangeObserver { heading = new H3(getTranslation("root.operatingHelp")); headingLayout.setId(HEADING_LAYOUT_ID); headingLayout.add(heading); - headingLayout.setAlignItems(FlexComponent.Alignment.CENTER); - headingLayout.setJustifyContentMode(JustifyContentMode.CENTER); final VerticalLayout contentLayout = new VerticalLayout(); inputSyntax = new H5(getTranslation("root.inputSyntax")); diff --git a/src/main/java/edu/kit/typicalc/view/main/InferenceRuleField.java b/src/main/java/edu/kit/typicalc/view/main/InferenceRuleField.java index a13e8ce..d3e6c29 100644 --- a/src/main/java/edu/kit/typicalc/view/main/InferenceRuleField.java +++ b/src/main/java/edu/kit/typicalc/view/main/InferenceRuleField.java @@ -2,34 +2,51 @@ package edu.kit.typicalc.view.main; import com.vaadin.flow.component.UI; import com.vaadin.flow.component.button.Button; +import com.vaadin.flow.component.dependency.CssImport; import com.vaadin.flow.component.dependency.JsModule; -import com.vaadin.flow.component.html.Div; -import com.vaadin.flow.component.html.H5; +import com.vaadin.flow.component.html.H4; import com.vaadin.flow.component.icon.Icon; import com.vaadin.flow.component.icon.VaadinIcon; +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; +@CssImport("./styles/view/main/inference-rule-field.css") @JsModule("./src/copy-to-clipboard.js") -public class InferenceRuleField extends Div implements LocaleChangeObserver { - //TODO add css! +public class InferenceRuleField extends VerticalLayout implements LocaleChangeObserver { private static final long serialVersionUID = -8551851183297707985L; + /* + * Id's for the imported css-file + */ private static final String INFERENCE_RULE_FIELD_ID = "inferenceRuleField"; + private static final String HEADER_ID = "headerField"; + private static final String MAIN_ID = "main"; + private static final String RULE_NAME_ID = "ruleName"; private final String nameKey; private final Button copyButton; - private final H5 ruleName; + private final H4 ruleName; private final MathjaxDisplay rule; public InferenceRuleField(final String latex, final String nameKey) { this.nameKey = nameKey; - this.ruleName = new H5(getTranslation(nameKey)); + + final HorizontalLayout header = new HorizontalLayout(); + header.setId(HEADER_ID); + this.ruleName = new H4(getTranslation(nameKey)); + ruleName.setId(RULE_NAME_ID); + header.add(ruleName); + + final VerticalLayout main = new VerticalLayout(); + main.setId(MAIN_ID); this.copyButton = new Button(getTranslation("root.copyLatex"), new Icon(VaadinIcon.CLIPBOARD)); this.rule = new MathjaxDisplay(latex); //TODO scale, when method implemented copyButton.addClickListener(event -> UI.getCurrent().getPage().executeJs("window.copyToClipboard($0)", latex)); - add(ruleName, rule, copyButton); + main.add(rule, copyButton); + add(header, main); setId(INFERENCE_RULE_FIELD_ID); } diff --git a/src/main/java/edu/kit/typicalc/view/main/InputBar.java b/src/main/java/edu/kit/typicalc/view/main/InputBar.java index 2c04f3b..db9e266 100644 --- a/src/main/java/edu/kit/typicalc/view/main/InputBar.java +++ b/src/main/java/edu/kit/typicalc/view/main/InputBar.java @@ -15,7 +15,6 @@ import com.vaadin.flow.component.dependency.CssImport; import com.vaadin.flow.component.html.H5; import com.vaadin.flow.component.icon.Icon; import com.vaadin.flow.component.icon.VaadinIcon; -import com.vaadin.flow.component.orderedlayout.FlexComponent; import com.vaadin.flow.component.orderedlayout.HorizontalLayout; import com.vaadin.flow.i18n.LocaleChangeEvent; import com.vaadin.flow.i18n.LocaleChangeObserver; @@ -28,7 +27,11 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver { private static final long serialVersionUID = -6099700300418752958L; + /* + * Id's for the imported css-file + */ private static final String INPUT_FIELD_ID = "inputField"; + private static final String INPUT_BAR_ID = "inputBar"; private final Tooltip infoTooltip; private final Icon infoIcon; @@ -67,7 +70,7 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver { inferTypeButton.addThemeVariants(ButtonVariant.LUMO_PRIMARY); add(infoTooltip, infoIcon, exampleButton, lambdaButton, inputField, inferTypeButton); - setAlignItems(FlexComponent.Alignment.CENTER); + setId(INPUT_BAR_ID); } private void onTypeInferButtonClick(final Consumer callback) { diff --git a/src/main/java/edu/kit/typicalc/view/main/UpperBar.java b/src/main/java/edu/kit/typicalc/view/main/UpperBar.java index bba88c5..a6579f1 100644 --- a/src/main/java/edu/kit/typicalc/view/main/UpperBar.java +++ b/src/main/java/edu/kit/typicalc/view/main/UpperBar.java @@ -8,7 +8,6 @@ import com.vaadin.flow.component.dialog.Dialog; import com.vaadin.flow.component.html.H1; import com.vaadin.flow.component.icon.Icon; import com.vaadin.flow.component.icon.VaadinIcon; -import com.vaadin.flow.component.orderedlayout.FlexComponent; import com.vaadin.flow.component.orderedlayout.HorizontalLayout; import edu.kit.typicalc.view.content.infocontent.StartPageView; import edu.kit.typicalc.view.main.MainView.MainViewListener; @@ -21,6 +20,9 @@ public class UpperBar extends HorizontalLayout { private static final long serialVersionUID = -7344967027514015830L; + /* + * Id's for the imported css-file + */ private static final String VIEW_TITLE_ID = "viewTitle"; private static final String INPUT_BAR_ID = "inputBar"; private static final String HELP_ICON_ID = "helpIcon"; @@ -41,21 +43,18 @@ public class UpperBar extends HorizontalLayout { this.presenter = presenter; this.viewTitle = new H1(getTranslation("root.typicalc")); + viewTitle.addClickListener(event -> this.getUI().get().navigate(StartPageView.class)); viewTitle.setId(VIEW_TITLE_ID); this.inputBar = new InputBar(this::typeInfer); inputBar.setId(INPUT_BAR_ID); this.helpIcon = new Icon(VaadinIcon.QUESTION_CIRCLE); helpIcon.addClickListener(event -> onHelpIconClick()); helpIcon.setId(HELP_ICON_ID); - - viewTitle.addClickListener(event -> this.getUI().get().navigate(StartPageView.class)); - + add(new DrawerToggle(), viewTitle, inputBar, helpIcon); setId(UPPER_BAR_ID); getThemeList().set("dark", true); //TODO remove magic string - setWidthFull(); setSpacing(false); - setAlignItems(FlexComponent.Alignment.CENTER); } /** From 0f5531ef47fca1be50f2e52687fea37ab9bcde78 Mon Sep 17 00:00:00 2001 From: uogau Date: Sat, 30 Jan 2021 09:28:48 +0100 Subject: [PATCH 09/15] NamedType angepasst --- src/main/java/edu/kit/typicalc/model/type/NamedType.java | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/main/java/edu/kit/typicalc/model/type/NamedType.java b/src/main/java/edu/kit/typicalc/model/type/NamedType.java index 33f798a..4d89221 100644 --- a/src/main/java/edu/kit/typicalc/model/type/NamedType.java +++ b/src/main/java/edu/kit/typicalc/model/type/NamedType.java @@ -53,8 +53,7 @@ public class NamedType extends Type { */ @Override public Type substitute(TypeVariable a, Type b) { - //TODO: Methode überhaupt sinnvoll? - return null; + return this; } /** From 2adc72cf74049e30251fc13d193249bff6dbfe50 Mon Sep 17 00:00:00 2001 From: uogau Date: Sat, 30 Jan 2021 09:37:01 +0100 Subject: [PATCH 10/15] =?UTF-8?q?Kleine=20=C3=84nderungen?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../edu/kit/typicalc/model/type/TypeVariable.java | 4 ++++ .../kit/typicalc/model/type/UnificationActions.java | 5 ++++- .../edu/kit/typicalc/model/type/FunctionTypeTest.java | 11 ----------- 3 files changed, 8 insertions(+), 12 deletions(-) diff --git a/src/main/java/edu/kit/typicalc/model/type/TypeVariable.java b/src/main/java/edu/kit/typicalc/model/type/TypeVariable.java index c136e91..1cc8706 100644 --- a/src/main/java/edu/kit/typicalc/model/type/TypeVariable.java +++ b/src/main/java/edu/kit/typicalc/model/type/TypeVariable.java @@ -64,6 +64,10 @@ public class TypeVariable extends Type { } } + /** + * Accepts a visitor. + * @param typeVisitor the visitor that wants to visit this + */ public void accept(TypeVisitor typeVisitor) { typeVisitor.visit(this); } diff --git a/src/main/java/edu/kit/typicalc/model/type/UnificationActions.java b/src/main/java/edu/kit/typicalc/model/type/UnificationActions.java index 5409b70..25aa799 100644 --- a/src/main/java/edu/kit/typicalc/model/type/UnificationActions.java +++ b/src/main/java/edu/kit/typicalc/model/type/UnificationActions.java @@ -30,7 +30,10 @@ public class UnificationActions { public Collection getConstraints() { return constraints; } - + /** + * Getter for substitution + * @return the substitution stored in this object + */ public Optional getSubstitution() { return substitution; } diff --git a/src/test/java/edu/kit/typicalc/model/type/FunctionTypeTest.java b/src/test/java/edu/kit/typicalc/model/type/FunctionTypeTest.java index 74b31c3..c76964b 100644 --- a/src/test/java/edu/kit/typicalc/model/type/FunctionTypeTest.java +++ b/src/test/java/edu/kit/typicalc/model/type/FunctionTypeTest.java @@ -1,22 +1,11 @@ package edu.kit.typicalc.model.type; -import org.junit.jupiter.api.AfterEach; -import org.junit.jupiter.api.BeforeEach; import org.junit.jupiter.api.Test; import static org.junit.jupiter.api.Assertions.*; class FunctionTypeTest { - @BeforeEach - void setUp() { - - } - - @AfterEach - void tearDown() { - } - @Test void substitute() { TypeVariable typeVariable1 = new TypeVariable(TypeVaribaleKind.USER_INPUT, 1); From aafb8ead44f9e257cbab18bf3b2bbe40703f781a Mon Sep 17 00:00:00 2001 From: uogau Date: Sat, 30 Jan 2021 09:41:56 +0100 Subject: [PATCH 11/15] FunctionType: substitute angepasst --- .../kit/typicalc/model/type/FunctionType.java | 18 +----------------- 1 file changed, 1 insertion(+), 17 deletions(-) diff --git a/src/main/java/edu/kit/typicalc/model/type/FunctionType.java b/src/main/java/edu/kit/typicalc/model/type/FunctionType.java index 1948b95..b34fa84 100644 --- a/src/main/java/edu/kit/typicalc/model/type/FunctionType.java +++ b/src/main/java/edu/kit/typicalc/model/type/FunctionType.java @@ -41,23 +41,7 @@ public class FunctionType extends Type { */ @Override public FunctionType substitute(TypeVariable a, Type b) { - boolean first = false; - boolean second = false; - if (this.parameter.contains(a)) { - first = true; - } - if (this.output.contains(a)) { - second = true; - } - if (first && second) { - return new FunctionType(parameter.substitute(a, b), output.substitute(a, b)); - } else if (first) { - return new FunctionType(parameter.substitute(a, b), output); - } else if (second) { - return new FunctionType(parameter, output.substitute(a, b)); - } else { - return this; - } + return new FunctionType(parameter.substitute(a, b), output.substitute(a, b)); } /** From dee5e2b3f032381a98140140c921ea47e24e6c5f Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Sat, 30 Jan 2021 09:49:13 +0100 Subject: [PATCH 12/15] Type: constrainEqualTo* implementation --- .../kit/typicalc/model/UnificationError.java | 3 +- .../kit/typicalc/model/type/FunctionType.java | 22 ++++---- .../kit/typicalc/model/type/NamedType.java | 20 +++---- .../edu/kit/typicalc/model/type/Type.java | 2 +- .../kit/typicalc/model/type/TypeVariable.java | 19 ++++--- .../model/type/UnificationActions.java | 13 ++++- .../typicalc/model/type/UnificationUtil.java | 55 +++++++++++++++++++ 7 files changed, 100 insertions(+), 34 deletions(-) create mode 100644 src/main/java/edu/kit/typicalc/model/type/UnificationUtil.java diff --git a/src/main/java/edu/kit/typicalc/model/UnificationError.java b/src/main/java/edu/kit/typicalc/model/UnificationError.java index b0cc58b..ec69459 100644 --- a/src/main/java/edu/kit/typicalc/model/UnificationError.java +++ b/src/main/java/edu/kit/typicalc/model/UnificationError.java @@ -1,5 +1,6 @@ package edu.kit.typicalc.model; public enum UnificationError { - INFINITE_TYPE + INFINITE_TYPE, + DIFFERENT_TYPES } diff --git a/src/main/java/edu/kit/typicalc/model/type/FunctionType.java b/src/main/java/edu/kit/typicalc/model/type/FunctionType.java index b34fa84..b905c6c 100644 --- a/src/main/java/edu/kit/typicalc/model/type/FunctionType.java +++ b/src/main/java/edu/kit/typicalc/model/type/FunctionType.java @@ -10,8 +10,8 @@ import java.util.Objects; */ public class FunctionType extends Type { - private Type parameter; - private Type output; + private final Type parameter; + private final Type output; /** * Initializes a new FunctionType with the given parameter and output types. * @param parameter the type of this function’s parameter @@ -60,9 +60,9 @@ public class FunctionType extends Type { * @param type the other type * @return unification steps necessary, or an error if that is impossible */ + @Override public Result constrainEqualTo(Type type) { - //TODO - return null; + return type.constrainEqualToFunction(this); } /** @@ -71,9 +71,9 @@ public class FunctionType extends Type { * @param type the function type * @return unification steps necessary, or an error if that is impossible */ - public Result constrainEqualToFunction(Type type) { - //TODO - return null; + @Override + public Result constrainEqualToFunction(FunctionType type) { + return UnificationUtil.functionFunction(this, type); } /** @@ -82,9 +82,9 @@ public class FunctionType extends Type { * @param type the named type * @return unification steps necessary, or an error if that is impossible */ + @Override public Result constrainEqualToNamedType(NamedType type) { - //TODO - return null; + return UnificationUtil.functionNamed(this, type); } /** @@ -93,9 +93,9 @@ public class FunctionType extends Type { * @param type the type variable * @return the unification steps necessary, or an error if that is impossible */ + @Override public Result constrainEqualToVariable(TypeVariable type) { - //TODO - return null; + return UnificationUtil.functionVariable(this, type); } /** diff --git a/src/main/java/edu/kit/typicalc/model/type/NamedType.java b/src/main/java/edu/kit/typicalc/model/type/NamedType.java index 4d89221..d8f5712 100644 --- a/src/main/java/edu/kit/typicalc/model/type/NamedType.java +++ b/src/main/java/edu/kit/typicalc/model/type/NamedType.java @@ -18,7 +18,7 @@ public class NamedType extends Type { */ public static final NamedType INT = new NamedType("int"); - private String name; + private final String name; /** * Initializes a new NamedType with the given name. @@ -72,9 +72,9 @@ public class NamedType extends Type { * @param type the other type * @return unification steps necessary, or an error if that is impossible */ + @Override public Result constrainEqualTo(Type type) { - //TODO - return null; + return type.constrainEqualToNamedType(this); } /** @@ -83,9 +83,9 @@ public class NamedType extends Type { * @param type the function type * @return unification steps necessary, or an error if that is impossible */ - public Result constrainEqualToFunction(Type type) { - //TODO - return null; + @Override + public Result constrainEqualToFunction(FunctionType type) { + return UnificationUtil.functionNamed(type, this); } /** @@ -94,9 +94,9 @@ public class NamedType extends Type { * @param type the named type * @return unification steps necessary, or an error if that is impossible */ + @Override public Result constrainEqualToNamedType(NamedType type) { - //TODO - return null; + return UnificationUtil.namedNamed(this, type); } /** @@ -105,9 +105,9 @@ public class NamedType extends Type { * @param type the type variable * @return the unification steps necessary, or an error if that is impossible */ + @Override public Result constrainEqualToVariable(TypeVariable type) { - //TODO - return null; + return UnificationUtil.variableNamed(type, this); } @Override diff --git a/src/main/java/edu/kit/typicalc/model/type/Type.java b/src/main/java/edu/kit/typicalc/model/type/Type.java index e96b43e..63c3199 100644 --- a/src/main/java/edu/kit/typicalc/model/type/Type.java +++ b/src/main/java/edu/kit/typicalc/model/type/Type.java @@ -42,7 +42,7 @@ public abstract class Type { * @param type the function type * @return unification steps necessary, or an error if that is impossible */ - public abstract Result constrainEqualToFunction(Type type); + public abstract Result constrainEqualToFunction(FunctionType type); /** * Computes the necessary constraints (and substitution) to unify this type with a diff --git a/src/main/java/edu/kit/typicalc/model/type/TypeVariable.java b/src/main/java/edu/kit/typicalc/model/type/TypeVariable.java index 1cc8706..0233585 100644 --- a/src/main/java/edu/kit/typicalc/model/type/TypeVariable.java +++ b/src/main/java/edu/kit/typicalc/model/type/TypeVariable.java @@ -56,6 +56,7 @@ public class TypeVariable extends Type { * @param b the type to insert * @return itself, or b if a is equal to this object */ + @Override public Type substitute(TypeVariable a, Type b) { if (this.equals(a)) { return b; @@ -79,9 +80,9 @@ public class TypeVariable extends Type { * @param type the other type * @return unification steps necessary, or an error if that is impossible */ + @Override public Result constrainEqualTo(Type type) { - //TODO - return null; + return type.constrainEqualToVariable(this); } /** @@ -90,9 +91,9 @@ public class TypeVariable extends Type { * @param type the function type * @return unification steps necessary, or an error if that is impossible */ - public Result constrainEqualToFunction(Type type) { - //TODO - return null; + @Override + public Result constrainEqualToFunction(FunctionType type) { + return UnificationUtil.functionVariable(type, this); } /** @@ -101,9 +102,9 @@ public class TypeVariable extends Type { * @param type the named type * @return unification steps necessary, or an error if that is impossible */ + @Override public Result constrainEqualToNamedType(NamedType type) { - //TODO - return null; + return UnificationUtil.variableNamed(this, type); } /** @@ -112,9 +113,9 @@ public class TypeVariable extends Type { * @param type the type variable * @return the unification steps necessary, or an error if that is impossible */ + @Override public Result constrainEqualToVariable(TypeVariable type) { - //TODO - return null; + return UnificationUtil.variableVariable(this, type); } @Override diff --git a/src/main/java/edu/kit/typicalc/model/type/UnificationActions.java b/src/main/java/edu/kit/typicalc/model/type/UnificationActions.java index 25aa799..9d947a4 100644 --- a/src/main/java/edu/kit/typicalc/model/type/UnificationActions.java +++ b/src/main/java/edu/kit/typicalc/model/type/UnificationActions.java @@ -4,14 +4,15 @@ import edu.kit.typicalc.model.Constraint; import edu.kit.typicalc.model.Substitution; import java.util.Collection; +import java.util.Collections; import java.util.Optional; /** * Models the necessary actions to process a constraint. */ public class UnificationActions { - private Collection constraints; - private Optional substitution; + private final Collection constraints; + private final Optional substitution; /** * Initializes this object using the provided constraints and substitution. @@ -23,6 +24,14 @@ public class UnificationActions { this.substitution = substitution; } + /** + * Initializes an empty object. + */ + protected UnificationActions() { + this.constraints = Collections.emptyList(); + this.substitution = Optional.empty(); + } + /** * Getter for constraints * @return the constraints stored in this object diff --git a/src/main/java/edu/kit/typicalc/model/type/UnificationUtil.java b/src/main/java/edu/kit/typicalc/model/type/UnificationUtil.java new file mode 100644 index 0000000..064489c --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/type/UnificationUtil.java @@ -0,0 +1,55 @@ +package edu.kit.typicalc.model.type; + +import edu.kit.typicalc.model.Constraint; +import edu.kit.typicalc.model.Substitution; +import edu.kit.typicalc.model.UnificationError; +import edu.kit.typicalc.util.Result; + +import java.util.Collections; +import java.util.List; +import java.util.Optional; + +/** + * Utility class to avoid unification logic duplication in type methods. + */ +final class UnificationUtil { + // TODO: document class? implementation detail? + private UnificationUtil() { + + } + + // TODO: check for infinite types + + static Result functionFunction(FunctionType a, FunctionType b) { + return new Result<>(new UnificationActions(List.of( + new Constraint(a.getParameter(), b.getParameter()), + new Constraint(a.getOutput(), b.getOutput())), Optional.empty())); + } + + static Result functionNamed(FunctionType a, NamedType b) { + return new Result<>(null, UnificationError.DIFFERENT_TYPES); + } + + static Result functionVariable(FunctionType a, TypeVariable b) { + return new Result<>(new UnificationActions(Collections.emptyList(), + Optional.of(new Substitution(b, a)))); + } + + static Result variableNamed(TypeVariable a, NamedType b) { + return new Result<>(new UnificationActions(Collections.emptyList(), + Optional.of(new Substitution(a, b)))); + } + + static Result variableVariable(TypeVariable a, TypeVariable b) { + return new Result<>(new UnificationActions(Collections.emptyList(), + Optional.of(new Substitution(a, b)))); + } + + static Result namedNamed(NamedType a, NamedType b) { + if (a != b) { + return new Result<>(null, UnificationError.DIFFERENT_TYPES); + } else { + return new Result<>(new UnificationActions()); + } + } +} From b716b204b3e183e6b3ae7bc0ae1b1290fa1a535a Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Sat, 30 Jan 2021 10:32:15 +0100 Subject: [PATCH 13/15] Unification tests, miscellaneous code style fixes --- .../edu/kit/typicalc/model/Constraint.java | 19 +++++ .../edu/kit/typicalc/model/Substitution.java | 24 ++++++ .../kit/typicalc/model/UnificationError.java | 12 +++ .../typicalc/model/parser/LambdaLexer.java | 7 +- .../typicalc/model/parser/LambdaParser.java | 3 +- .../edu/kit/typicalc/model/parser/Token.java | 21 ++++- .../typicalc/model/type/TypeAbstraction.java | 7 +- .../kit/typicalc/model/type/TypeVariable.java | 7 +- .../typicalc/model/type/UnificationUtil.java | 13 +++- .../model/parser/LambdaParserTest.java | 9 ++- .../typicalc/model/type/UnificationTest.java | 77 +++++++++++++++++++ 11 files changed, 184 insertions(+), 15 deletions(-) create mode 100644 src/test/java/edu/kit/typicalc/model/type/UnificationTest.java diff --git a/src/main/java/edu/kit/typicalc/model/Constraint.java b/src/main/java/edu/kit/typicalc/model/Constraint.java index e26d32b..761bf6f 100644 --- a/src/main/java/edu/kit/typicalc/model/Constraint.java +++ b/src/main/java/edu/kit/typicalc/model/Constraint.java @@ -2,6 +2,8 @@ package edu.kit.typicalc.model; import edu.kit.typicalc.model.type.Type; +import java.util.Objects; + /** * Constrains two types to be equal. */ @@ -35,4 +37,21 @@ public class Constraint { return b; } + @Override + public boolean equals(Object o) { + if (this == o) { + return true; + } + if (o == null || getClass() != o.getClass()) { + return false; + } + Constraint that = (Constraint) o; + return (a.equals(that.a) && b.equals(that.b)) + || (a.equals(that.b) && b.equals(that.a)); + } + + @Override + public int hashCode() { + return Objects.hash(a, b); + } } diff --git a/src/main/java/edu/kit/typicalc/model/Substitution.java b/src/main/java/edu/kit/typicalc/model/Substitution.java index e1782b7..0063819 100644 --- a/src/main/java/edu/kit/typicalc/model/Substitution.java +++ b/src/main/java/edu/kit/typicalc/model/Substitution.java @@ -3,6 +3,8 @@ package edu.kit.typicalc.model; import edu.kit.typicalc.model.type.Type; import edu.kit.typicalc.model.type.TypeVariable; +import java.util.Objects; + /** * A substitution specifies that some type should be replaced by a different type. */ @@ -36,4 +38,26 @@ public class Substitution { Type getType() { return b; } + + @Override + public String toString() { + return "Substitution[" + a + " => " + b + "]"; + } + + @Override + public boolean equals(Object o) { + if (this == o) { + return true; + } + if (o == null || getClass() != o.getClass()) { + return false; + } + Substitution that = (Substitution) o; + return a.equals(that.a) && b.equals(that.b); + } + + @Override + public int hashCode() { + return Objects.hash(a, b); + } } diff --git a/src/main/java/edu/kit/typicalc/model/UnificationError.java b/src/main/java/edu/kit/typicalc/model/UnificationError.java index ec69459..070dec4 100644 --- a/src/main/java/edu/kit/typicalc/model/UnificationError.java +++ b/src/main/java/edu/kit/typicalc/model/UnificationError.java @@ -1,6 +1,18 @@ package edu.kit.typicalc.model; +/** + * Errors that can occur during unification. + * + * @see Unification + * @see UnificationStep + */ public enum UnificationError { + /** + * Unification would lead to an infinite type. + */ INFINITE_TYPE, + /** + * Some {@link edu.kit.typicalc.model.type.NamedType} is not equal to another type. + */ DIFFERENT_TYPES } diff --git a/src/main/java/edu/kit/typicalc/model/parser/LambdaLexer.java b/src/main/java/edu/kit/typicalc/model/parser/LambdaLexer.java index 09847f1..61989e9 100644 --- a/src/main/java/edu/kit/typicalc/model/parser/LambdaLexer.java +++ b/src/main/java/edu/kit/typicalc/model/parser/LambdaLexer.java @@ -108,6 +108,7 @@ public class LambdaLexer { return new Result<>(t); default: if (Character.isLetter(c)) { + int startPos = pos; // identifier StringBuilder sb = new StringBuilder(); do { @@ -133,17 +134,17 @@ public class LambdaLexer { type = TokenType.VARIABLE; break; } - return new Result<>(new Token(type, sb.toString(), pos)); + return new Result<>(new Token(type, sb.toString(), startPos)); } else if (Character.isDigit(c)) { + int startPos = pos; // number literal StringBuilder sb = new StringBuilder(); do { sb.append(term.charAt(pos)); advance(); } while (pos < term.length() && Character.isDigit(term.charAt(pos))); - return new Result<>(new Token(TokenType.NUMBER, sb.toString(), pos)); + return new Result<>(new Token(TokenType.NUMBER, sb.toString(), startPos)); } else { - //throw new ParseException("Illegal character '" + term.charAt(pos) + "'"); return new Result<>(null, ParseError.UNEXPECTED_CHARACTER); } } diff --git a/src/main/java/edu/kit/typicalc/model/parser/LambdaParser.java b/src/main/java/edu/kit/typicalc/model/parser/LambdaParser.java index 64d693c..7249298 100644 --- a/src/main/java/edu/kit/typicalc/model/parser/LambdaParser.java +++ b/src/main/java/edu/kit/typicalc/model/parser/LambdaParser.java @@ -58,10 +58,11 @@ public class LambdaParser { * @param type the token type to compare the current token type to */ private Optional expect(TokenType type) { + Token lastToken = token; TokenType current = token.getType(); Optional error = nextToken(); if (current != type) { - return Optional.of(ParseError.UNEXPECTED_TOKEN.withToken(token)); + return Optional.of(ParseError.UNEXPECTED_TOKEN.withToken(lastToken)); } return error; } diff --git a/src/main/java/edu/kit/typicalc/model/parser/Token.java b/src/main/java/edu/kit/typicalc/model/parser/Token.java index 3394e28..5b6c20e 100644 --- a/src/main/java/edu/kit/typicalc/model/parser/Token.java +++ b/src/main/java/edu/kit/typicalc/model/parser/Token.java @@ -1,5 +1,7 @@ package edu.kit.typicalc.model.parser; +import java.util.Objects; + /** * A token of the Prolog language. */ @@ -73,6 +75,23 @@ public class Token { @Override public String toString() { - return type + "(\"" + text + "\")"; + return type + "(\"" + text + "\")[" + pos + "]"; + } + + @Override + public boolean equals(Object o) { + if (this == o) { + return true; + } + if (o == null || getClass() != o.getClass()) { + return false; + } + Token token = (Token) o; + return pos == token.pos && type == token.type && Objects.equals(text, token.text); + } + + @Override + public int hashCode() { + return Objects.hash(type, text, pos); } } diff --git a/src/main/java/edu/kit/typicalc/model/type/TypeAbstraction.java b/src/main/java/edu/kit/typicalc/model/type/TypeAbstraction.java index 805773b..ed96d32 100644 --- a/src/main/java/edu/kit/typicalc/model/type/TypeAbstraction.java +++ b/src/main/java/edu/kit/typicalc/model/type/TypeAbstraction.java @@ -2,6 +2,7 @@ package edu.kit.typicalc.model.type; import edu.kit.typicalc.model.TypeVariableFactory; +import java.util.Collections; import java.util.List; import java.util.Objects; @@ -11,8 +12,8 @@ import java.util.Objects; */ public class TypeAbstraction { - private Type type; - private List quantifiedVariables; + private final Type type; + private final List quantifiedVariables; /** * Initializes a new type abstraction with its type and the type variables bound by * the for-all quantifier. @@ -31,7 +32,7 @@ public class TypeAbstraction { */ public TypeAbstraction(Type type) { this.type = type; - this.quantifiedVariables = null; + this.quantifiedVariables = Collections.emptyList(); } /** diff --git a/src/main/java/edu/kit/typicalc/model/type/TypeVariable.java b/src/main/java/edu/kit/typicalc/model/type/TypeVariable.java index 0233585..536f4bd 100644 --- a/src/main/java/edu/kit/typicalc/model/type/TypeVariable.java +++ b/src/main/java/edu/kit/typicalc/model/type/TypeVariable.java @@ -115,7 +115,12 @@ public class TypeVariable extends Type { */ @Override public Result constrainEqualToVariable(TypeVariable type) { - return UnificationUtil.variableVariable(this, type); + return UnificationUtil.variableVariable(type, this); + } + + @Override + public String toString() { + return "TypeVariable[" + kind + "_" + index + "]"; } @Override diff --git a/src/main/java/edu/kit/typicalc/model/type/UnificationUtil.java b/src/main/java/edu/kit/typicalc/model/type/UnificationUtil.java index 064489c..fca61d6 100644 --- a/src/main/java/edu/kit/typicalc/model/type/UnificationUtil.java +++ b/src/main/java/edu/kit/typicalc/model/type/UnificationUtil.java @@ -18,8 +18,6 @@ final class UnificationUtil { } - // TODO: check for infinite types - static Result functionFunction(FunctionType a, FunctionType b) { return new Result<>(new UnificationActions(List.of( new Constraint(a.getParameter(), b.getParameter()), @@ -31,6 +29,9 @@ final class UnificationUtil { } static Result functionVariable(FunctionType a, TypeVariable b) { + if (a.contains(b)) { + return new Result<>(null, UnificationError.INFINITE_TYPE); + } return new Result<>(new UnificationActions(Collections.emptyList(), Optional.of(new Substitution(b, a)))); } @@ -41,8 +42,12 @@ final class UnificationUtil { } static Result variableVariable(TypeVariable a, TypeVariable b) { - return new Result<>(new UnificationActions(Collections.emptyList(), - Optional.of(new Substitution(a, b)))); + if (!a.equals(b)) { + return new Result<>(new UnificationActions(Collections.emptyList(), + Optional.of(new Substitution(a, b)))); + } else { + return new Result<>(new UnificationActions()); + } } static Result namedNamed(NamedType a, NamedType b) { diff --git a/src/test/java/edu/kit/typicalc/model/parser/LambdaParserTest.java b/src/test/java/edu/kit/typicalc/model/parser/LambdaParserTest.java index 60fe4f7..7a0f433 100644 --- a/src/test/java/edu/kit/typicalc/model/parser/LambdaParserTest.java +++ b/src/test/java/edu/kit/typicalc/model/parser/LambdaParserTest.java @@ -9,6 +9,7 @@ import edu.kit.typicalc.model.term.IntegerTerm; import edu.kit.typicalc.model.term.LambdaTerm; import edu.kit.typicalc.model.term.LetTerm; import edu.kit.typicalc.model.term.VarTerm; +import edu.kit.typicalc.model.parser.Token.TokenType; import edu.kit.typicalc.util.Result; import org.junit.jupiter.api.Test; @@ -85,12 +86,16 @@ class LambdaParserTest { LambdaParser parser = new LambdaParser(""); assertEquals(ParseError.TOO_FEW_TOKENS, parser.parse().unwrapError()); parser = new LambdaParser("x)"); - assertEquals(ParseError.UNEXPECTED_TOKEN, parser.parse().unwrapError()); + ParseError error = parser.parse().unwrapError(); + assertEquals(ParseError.UNEXPECTED_TOKEN, error); + assertEquals(new Token(TokenType.RP, ")", 1), error.getCause()); parser = new LambdaParser("??"); assertEquals(ParseError.UNEXPECTED_CHARACTER, parser.parse().unwrapError()); parser = new LambdaParser("123333333333333"); assertEquals(ParseError.UNEXPECTED_CHARACTER, parser.parse().unwrapError()); parser = new LambdaParser("x 123333333333333"); - assertEquals(ParseError.UNEXPECTED_CHARACTER, parser.parse().unwrapError()); + error = parser.parse().unwrapError(); + assertEquals(ParseError.UNEXPECTED_CHARACTER, error); + assertEquals(new Token(TokenType.NUMBER, "123333333333333", 2), error.getCause()); } } diff --git a/src/test/java/edu/kit/typicalc/model/type/UnificationTest.java b/src/test/java/edu/kit/typicalc/model/type/UnificationTest.java new file mode 100644 index 0000000..f6ff460 --- /dev/null +++ b/src/test/java/edu/kit/typicalc/model/type/UnificationTest.java @@ -0,0 +1,77 @@ +package edu.kit.typicalc.model.type; + +import edu.kit.typicalc.model.Constraint; +import edu.kit.typicalc.model.Substitution; +import edu.kit.typicalc.model.UnificationError; +import org.junit.jupiter.api.Test; + +import java.util.Collection; + +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertTrue; + +class UnificationTest { + @Test + void all() { + TypeVariable a1 = new TypeVariable(TypeVaribaleKind.TREE, 1); + TypeVariable a2 = new TypeVariable(TypeVaribaleKind.TREE, 2); + TypeVariable a3 = new TypeVariable(TypeVaribaleKind.TREE, 3); + FunctionType id = new FunctionType(a1, a1); + FunctionType fun = new FunctionType(a2, a3); + NamedType string = new NamedType("string"); + NamedType object = new NamedType("object"); + + // Function constraints + UnificationError error = id.constrainEqualTo(a1).unwrapError(); + assertEquals(UnificationError.INFINITE_TYPE, error); + + UnificationActions actions = id.constrainEqualTo(a2).unwrap(); + assertEquals(new Substitution(a2, id), actions.getSubstitution().get()); + assertTrue(actions.getConstraints().isEmpty()); + + error = id.constrainEqualTo(string).unwrapError(); + assertEquals(UnificationError.DIFFERENT_TYPES, error); + + actions = id.constrainEqualTo(fun).unwrap(); + assertTrue(actions.getSubstitution().isEmpty()); + Collection constraints = actions.getConstraints(); + assertEquals(2, constraints.size()); + assertTrue(constraints.contains(new Constraint(a1, a2))); + assertTrue(constraints.contains(new Constraint(a1, a3))); + + // Variable constraints + actions = a1.constrainEqualTo(a1).unwrap(); + assertTrue(actions.getConstraints().isEmpty()); + assertTrue(actions.getSubstitution().isEmpty()); + + actions = a1.constrainEqualTo(a2).unwrap(); + assertTrue(actions.getConstraints().isEmpty()); + assertEquals(new Substitution(a1, a2), actions.getSubstitution().get()); + + error = a1.constrainEqualTo(id).unwrapError(); + assertEquals(UnificationError.INFINITE_TYPE, error); + + actions = a2.constrainEqualTo(id).unwrap(); + assertEquals(new Substitution(a2, id), actions.getSubstitution().get()); + assertTrue(actions.getConstraints().isEmpty()); + + actions = a1.constrainEqualTo(string).unwrap(); + assertTrue(actions.getConstraints().isEmpty()); + assertEquals(new Substitution(a1, string), actions.getSubstitution().get()); + + // Named type constraints + actions = string.constrainEqualTo(string).unwrap(); + assertTrue(actions.getConstraints().isEmpty()); + assertTrue(actions.getSubstitution().isEmpty()); + + error = string.constrainEqualTo(object).unwrapError(); + assertEquals(UnificationError.DIFFERENT_TYPES, error); + + error = string.constrainEqualTo(id).unwrapError(); + assertEquals(UnificationError.DIFFERENT_TYPES, error); + + actions = string.constrainEqualTo(a1).unwrap(); + assertTrue(actions.getConstraints().isEmpty()); + assertEquals(new Substitution(a1, string), actions.getSubstitution().get()); + } +} From e25a9476217d422c303714229cd5e25701b9e3dc Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Sat, 30 Jan 2021 10:37:27 +0100 Subject: [PATCH 14/15] Formatting: tabs -> spaces --- .../typicalc/model/term/TermVisitorTree.java | 35 +-- .../kit/typicalc/model/type/NamedType.java | 210 +++++++++--------- .../kit/typicalc/model/type/TypeVisitor.java | 30 +-- .../kit/typicalc/view/main/DrawerContent.java | 22 +- .../kit/typicalc/view/main/HelpDialog.java | 33 ++- .../edu/kit/typicalc/view/main/InputBar.java | 13 +- .../kit/typicalc/view/main/MainViewImpl.java | 7 +- 7 files changed, 176 insertions(+), 174 deletions(-) diff --git a/src/main/java/edu/kit/typicalc/model/term/TermVisitorTree.java b/src/main/java/edu/kit/typicalc/model/term/TermVisitorTree.java index 2166daa..41b11f9 100644 --- a/src/main/java/edu/kit/typicalc/model/term/TermVisitorTree.java +++ b/src/main/java/edu/kit/typicalc/model/term/TermVisitorTree.java @@ -11,12 +11,13 @@ public interface TermVisitorTree { * Returns an {@link edu.kit.typicalc.model.step.AppStep} suiting the given application (lambda term) * to type-infer and the type assumptions to consider. * Simultaneously assembles the tree's constraint list. + * * @param appTerm the application (lambda term) to build the inference step structure for, - * i.e. the lambda term in the conclusion of the returned inference step + * i.e. the lambda term in the conclusion of the returned inference step * @param typeAssumptions the type assumptions to consider, - * i.e. the type assumptions in the conclusion of the returned inference step + * i.e. the type assumptions in the conclusion of the returned inference step * @param conclusionType the type that the lambda term in the conclusion - * of the returned inference step will be assigned + * of the returned inference step will be assigned * @return an {@link edu.kit.typicalc.model.step.AppStep} */ InferenceStep visit(AppTerm appTerm, Map typeAssumptions, Type conclusionType); @@ -25,12 +26,13 @@ public interface TermVisitorTree { * Returns an {@link edu.kit.typicalc.model.step.AbsStep} suiting the given abstraction (lambda term) * to type-infer and the type assumptions to consider. * Simultaneously assembles the tree's constraint list. + * * @param absTerm the abstraction (lambda term) to build the inference step structure for, - * i.e. the lambda term in the conclusion of the returned inference step + * i.e. the lambda term in the conclusion of the returned inference step * @param typeAssumptions the type assumptions to consider, - * i.e. the type assumptions in the conclusion of the returned inference step + * i.e. the type assumptions in the conclusion of the returned inference step * @param conclusionType the type that the lambda term in the conclusion - * of the returned inference step will be assigned + * of the returned inference step will be assigned * @return an {@link edu.kit.typicalc.model.step.AbsStep} */ InferenceStep visit(AbsTerm absTerm, Map typeAssumptions, Type conclusionType); @@ -39,12 +41,13 @@ public interface TermVisitorTree { * Returns an {@link edu.kit.typicalc.model.step.LetStep} suiting the given let expression (lambda term) * to type-infer and the type assumptions to consider. * Simultaneously assembles the tree's constraint list. + * * @param letTerm the let expression (lambda term) to build the inference step structure for, - * i.e. the lambda term in the conclusion of the returned inference step + * i.e. the lambda term in the conclusion of the returned inference step * @param typeAssumptions the type assumptions to consider, - * i.e. the type assumptions in the conclusion of the returned inference step + * i.e. the type assumptions in the conclusion of the returned inference step * @param conclusionType the type that the lambda term in the conclusion - * of the returned inference step will be assigned + * of the returned inference step will be assigned * @return an {@link edu.kit.typicalc.model.step.LetStep} */ InferenceStep visit(LetTerm letTerm, Map typeAssumptions, Type conclusionType); @@ -53,12 +56,13 @@ public interface TermVisitorTree { * Returns an {@link edu.kit.typicalc.model.step.ConstStep} suiting the given constant * to type-infer and the type assumptions to consider. * Simultaneously assembles the tree's constraint list. + * * @param constTerm the constant to build the inference step structure for, - * i.e. the lambda term in the conclusion of the returned inference step + * i.e. the lambda term in the conclusion of the returned inference step * @param typeAssumptions the type assumptions to consider, - * i.e. the type assumptions in the conclusion of the returned inference step + * i.e. the type assumptions in the conclusion of the returned inference step * @param conclusionType the type that the lambda term in the conclusion - * of the returned inference step will be assigned + * of the returned inference step will be assigned * @return an {@link edu.kit.typicalc.model.step.ConstStep} */ InferenceStep visit(ConstTerm constTerm, Map typeAssumptions, Type conclusionType); @@ -67,12 +71,13 @@ public interface TermVisitorTree { * Returns an {@link edu.kit.typicalc.model.step.VarStep} suiting the given variable (lambda term) * to type-infer and the type assumptions to consider. * Simultaneously assembles the tree's constraint list. + * * @param varTerm the variable (lambda term) to build the inference step structure for, - * i.e. the lambda term in the conclusion of the returned inference step + * i.e. the lambda term in the conclusion of the returned inference step * @param typeAssumptions the type assumptions to consider, - * i.e. the type assumptions in the conclusion of the returned inference step + * i.e. the type assumptions in the conclusion of the returned inference step * @param conclusionType the type that the lambda term in the conclusion - * of the returned inference step will be assigned + * of the returned inference step will be assigned * @return an {@link edu.kit.typicalc.model.step.VarStep} */ InferenceStep visit(VarTerm varTerm, Map typeAssumptions, Type conclusionType) diff --git a/src/main/java/edu/kit/typicalc/model/type/NamedType.java b/src/main/java/edu/kit/typicalc/model/type/NamedType.java index d8f5712..9f2f31d 100644 --- a/src/main/java/edu/kit/typicalc/model/type/NamedType.java +++ b/src/main/java/edu/kit/typicalc/model/type/NamedType.java @@ -9,121 +9,121 @@ import java.util.Objects; * Models a simple named type. */ public class NamedType extends Type { - /** - * boolean type - */ - public static final NamedType BOOLEAN = new NamedType("boolean"); - /** - * int type - */ - public static final NamedType INT = new NamedType("int"); + /** + * boolean type + */ + public static final NamedType BOOLEAN = new NamedType("boolean"); + /** + * int type + */ + public static final NamedType INT = new NamedType("int"); - private final String name; + private final String name; - /** - * Initializes a new NamedType with the given name. - * @param name the name of this type - */ - public NamedType(String name) { - this.name = name; - } + /** + * Initializes a new NamedType with the given name. + * @param name the name of this type + */ + public NamedType(String name) { + this.name = name; + } - /** - * Returns the name of the named type. - * @return the name of this type - */ - public String getName() { - return name; - } + /** + * Returns the name of the named type. + * @return the name of this type + */ + public String getName() { + return name; + } - /** - * Checks whether some type occurs in this type. - * @param x the type to look for - * @return whether the specified type is equal to this type - */ - public boolean contains(Type x) { - return this.equals(x); - } + /** + * Checks whether some type occurs in this type. + * @param x the type to look for + * @return whether the specified type is equal to this type + */ + public boolean contains(Type x) { + return this.equals(x); + } - /** - * Substitutes a type variable for a different type. - * @param a the type to replace - * @param b the type to insert - * @return itself, or b if a is equal to this object - */ - @Override - public Type substitute(TypeVariable a, Type b) { - return this; - } + /** + * Substitutes a type variable for a different type. + * @param a the type to replace + * @param b the type to insert + * @return itself, or b if a is equal to this object + */ + @Override + public Type substitute(TypeVariable a, Type b) { + return this; + } - /** - * Accepts a visitor. - * @param typeVisitor the visitor that wants to visit this - */ - @Override - public void accept(TypeVisitor typeVisitor) { - typeVisitor.visit(this); - } + /** + * Accepts a visitor. + * @param typeVisitor the visitor that wants to visit this + */ + @Override + public void accept(TypeVisitor typeVisitor) { + typeVisitor.visit(this); + } - /** - * Computes the necessary constraints (and substitution) to unify this type with - * another. This method uses the constrainEqualToNamedType method on the other - * type. - * @param type the other type - * @return unification steps necessary, or an error if that is impossible - */ - @Override - public Result constrainEqualTo(Type type) { - return type.constrainEqualToNamedType(this); - } + /** + * Computes the necessary constraints (and substitution) to unify this type with + * another. This method uses the constrainEqualToNamedType method on the other + * type. + * @param type the other type + * @return unification steps necessary, or an error if that is impossible + */ + @Override + public Result constrainEqualTo(Type type) { + return type.constrainEqualToNamedType(this); + } - /** - * Computes the necessary constraints (and substitution) to unify this type with a - * function type. - * @param type the function type - * @return unification steps necessary, or an error if that is impossible - */ - @Override - public Result constrainEqualToFunction(FunctionType type) { - return UnificationUtil.functionNamed(type, this); - } + /** + * Computes the necessary constraints (and substitution) to unify this type with a + * function type. + * @param type the function type + * @return unification steps necessary, or an error if that is impossible + */ + @Override + public Result constrainEqualToFunction(FunctionType type) { + return UnificationUtil.functionNamed(type, this); + } - /** - * Computes the necessary constraints (and substitution) to unify this type with a - * named type. - * @param type the named type - * @return unification steps necessary, or an error if that is impossible - */ - @Override - public Result constrainEqualToNamedType(NamedType type) { - return UnificationUtil.namedNamed(this, type); - } + /** + * Computes the necessary constraints (and substitution) to unify this type with a + * named type. + * @param type the named type + * @return unification steps necessary, or an error if that is impossible + */ + @Override + public Result constrainEqualToNamedType(NamedType type) { + return UnificationUtil.namedNamed(this, type); + } - /** - * Computes the necessary constraints (and substitution) to unify this type with a - * type variable. - * @param type the type variable - * @return the unification steps necessary, or an error if that is impossible - */ - @Override - public Result constrainEqualToVariable(TypeVariable type) { - return UnificationUtil.variableNamed(type, this); - } + /** + * Computes the necessary constraints (and substitution) to unify this type with a + * type variable. + * @param type the type variable + * @return the unification steps necessary, or an error if that is impossible + */ + @Override + public Result constrainEqualToVariable(TypeVariable type) { + return UnificationUtil.variableNamed(type, this); + } - @Override - public boolean equals(Object o) { - if (this == o) { - return true; - } - if (o == null || getClass() != o.getClass()) { - return false; - } - NamedType namedType = (NamedType) o; - return Objects.equals(name, namedType.name); - } + @Override + public boolean equals(Object o) { + if (this == o) { + return true; + } + if (o == null || getClass() != o.getClass()) { + return false; + } + NamedType namedType = (NamedType) o; + return Objects.equals(name, namedType.name); + } - @Override - public int hashCode() { - return Objects.hash(name); - } + @Override + public int hashCode() { + return Objects.hash(name); + } } diff --git a/src/main/java/edu/kit/typicalc/model/type/TypeVisitor.java b/src/main/java/edu/kit/typicalc/model/type/TypeVisitor.java index d5baaef..f09d7dc 100644 --- a/src/main/java/edu/kit/typicalc/model/type/TypeVisitor.java +++ b/src/main/java/edu/kit/typicalc/model/type/TypeVisitor.java @@ -4,21 +4,21 @@ package edu.kit.typicalc.model.type; * Can be implemented to process Type objects. */ public interface TypeVisitor { - /** - * Visit a named type. - * @param named the type to be visited - */ - void visit(NamedType named); + /** + * Visit a named type. + * @param named the type to be visited + */ + void visit(NamedType named); - /** - * Visit a type variable - * @param variable the variable to be visited - */ - void visit(TypeVariable variable); + /** + * Visit a type variable + * @param variable the variable to be visited + */ + void visit(TypeVariable variable); - /** - * Visit a function. - * @param function the function to be visited - */ - void visit(FunctionType function); + /** + * Visit a function. + * @param function the function to be visited + */ + void visit(FunctionType function); } diff --git a/src/main/java/edu/kit/typicalc/view/main/DrawerContent.java b/src/main/java/edu/kit/typicalc/view/main/DrawerContent.java index 9912688..71871a9 100644 --- a/src/main/java/edu/kit/typicalc/view/main/DrawerContent.java +++ b/src/main/java/edu/kit/typicalc/view/main/DrawerContent.java @@ -10,16 +10,16 @@ import com.vaadin.flow.i18n.LocaleChangeObserver; public class DrawerContent extends VerticalLayout implements LocaleChangeObserver { private static final long serialVersionUID = -5751275682270653335L; - + /* - * Id's for the imported css-file + * IDs for the imported CSS file */ private static final String RULE_CONTAINER_ID = "ruleContainer"; private static final String DRAWER_CONTENT_ID = "drawerContent"; private final H3 heading; private final VerticalLayout ruleContainer; - + public DrawerContent() { heading = new H3(getTranslation("root.inferenceRules")); ruleContainer = new VerticalLayout(); @@ -28,18 +28,18 @@ public class DrawerContent extends VerticalLayout implements LocaleChangeObserve add(heading, ruleContainer); setId(DRAWER_CONTENT_ID); } - + private void initRuleContainer() { - //TODO just demo content, exchange with correct rules - ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule")); - ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule")); - ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule")); - ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule")); - ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule")); + //TODO just demo content, exchange with correct rules + ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule")); + ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule")); + ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule")); + ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule")); + ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule")); } @Override public void localeChange(LocaleChangeEvent event) { - heading.setText(getTranslation("root.inferenceRules")); + heading.setText(getTranslation("root.inferenceRules")); } } diff --git a/src/main/java/edu/kit/typicalc/view/main/HelpDialog.java b/src/main/java/edu/kit/typicalc/view/main/HelpDialog.java index 9f96002..890cd74 100644 --- a/src/main/java/edu/kit/typicalc/view/main/HelpDialog.java +++ b/src/main/java/edu/kit/typicalc/view/main/HelpDialog.java @@ -11,34 +11,33 @@ import com.vaadin.flow.i18n.LocaleChangeObserver; @CssImport("./styles/view/main/help-dialog.css") public class HelpDialog extends Dialog implements LocaleChangeObserver { - private static final long serialVersionUID = 4470277770276296164L; - + /* - * Id's for the imported css-file + * IDs for the imported CSS file */ private static final String HEADING_LAYOUT_ID = "headingLayout"; private static final String CONTENT_LAYOUT_ID = "contentLayout"; - + private final H3 heading; private final H5 inputSyntax; - + public HelpDialog() { - final HorizontalLayout headingLayout = new HorizontalLayout(); - heading = new H3(getTranslation("root.operatingHelp")); - headingLayout.setId(HEADING_LAYOUT_ID); - headingLayout.add(heading); - - final VerticalLayout contentLayout = new VerticalLayout(); - inputSyntax = new H5(getTranslation("root.inputSyntax")); - contentLayout.setId(CONTENT_LAYOUT_ID); - contentLayout.add(inputSyntax); - add(headingLayout, contentLayout); + final HorizontalLayout headingLayout = new HorizontalLayout(); + heading = new H3(getTranslation("root.operatingHelp")); + headingLayout.setId(HEADING_LAYOUT_ID); + headingLayout.add(heading); + + final VerticalLayout contentLayout = new VerticalLayout(); + inputSyntax = new H5(getTranslation("root.inputSyntax")); + contentLayout.setId(CONTENT_LAYOUT_ID); + contentLayout.add(inputSyntax); + add(headingLayout, contentLayout); } @Override public void localeChange(LocaleChangeEvent event) { - heading.setText(getTranslation("root.operatingHelp")); - inputSyntax.setText(getTranslation("root.inputSyntax")); + heading.setText(getTranslation("root.operatingHelp")); + inputSyntax.setText(getTranslation("root.inputSyntax")); } } diff --git a/src/main/java/edu/kit/typicalc/view/main/InputBar.java b/src/main/java/edu/kit/typicalc/view/main/InputBar.java index db9e266..a1e2296 100644 --- a/src/main/java/edu/kit/typicalc/view/main/InputBar.java +++ b/src/main/java/edu/kit/typicalc/view/main/InputBar.java @@ -24,15 +24,14 @@ import com.vaadin.flow.i18n.LocaleChangeObserver; */ @CssImport("./styles/view/main/input-bar.css") public class InputBar extends HorizontalLayout implements LocaleChangeObserver { - private static final long serialVersionUID = -6099700300418752958L; - + /* * Id's for the imported css-file */ private static final String INPUT_FIELD_ID = "inputField"; private static final String INPUT_BAR_ID = "inputBar"; - + private final Tooltip infoTooltip; private final Icon infoIcon; private final Button exampleButton; @@ -42,17 +41,17 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver { /** * Creates an InputBar with a Consumer-object to call the inferType()-method in UpperBar. - * The current user input is passed as the methods argument. + * The current user input is passed as the methods argument. * * @param callback Consumer to call the inferType()-method in UpperBar */ protected InputBar(final Consumer 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 infoTooltip = new Tooltip(infoIcon, TooltipPosition.LEFT, TooltipAlignment.LEFT); infoTooltip.add(new H5("Hallo")); initInfoTooltip(); - + inputField = new TextField(); inputField.setId(INPUT_FIELD_ID); inputField.setClearButtonVisible(true); @@ -93,7 +92,7 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver { } private void initInfoTooltip() { - infoTooltip.add(new H5("Hallo")); + infoTooltip.add(new H5("Hallo")); } @Override diff --git a/src/main/java/edu/kit/typicalc/view/main/MainViewImpl.java b/src/main/java/edu/kit/typicalc/view/main/MainViewImpl.java index 8d08958..76fb069 100644 --- a/src/main/java/edu/kit/typicalc/view/main/MainViewImpl.java +++ b/src/main/java/edu/kit/typicalc/view/main/MainViewImpl.java @@ -20,7 +20,7 @@ import edu.kit.typicalc.view.content.typeinferencecontent.TypeInferenceView; /** * Contains all the displayed components and builds the applications user interface (UI). - * Vaadins app layout provides the rough structure of the UI. Using this structure the UI always + * Vaadin's app layout provides the rough structure of the UI. Using this structure the UI always * consists of an upper bar at the top of the screen and a drawer on the left side of * the screen. */ @@ -28,7 +28,6 @@ import edu.kit.typicalc.view.content.typeinferencecontent.TypeInferenceView; @JsModule("./styles/shared-styles.js") @JavaScript("./src/tex-svg-full.js") public class MainViewImpl extends AppLayout implements MainView { - private static final long serialVersionUID = -2411433187835906976L; /** @@ -48,8 +47,8 @@ public class MainViewImpl extends AppLayout implements MainView { @Override public void displayError(final ParseError error) { - //TODO add error keys to bundle - final VerticalLayout container = new VerticalLayout(); + //TODO add error keys to bundle + final VerticalLayout container = new VerticalLayout(); final Span errorText = new Span(getTranslation("root." + error.toString())); final Notification errorNotification = new Notification(); final Button closeButton = new Button(getTranslation("root.close"), event -> errorNotification.close()); From 614a7398e2699eb0f74efb5f63f3e88a0e548414 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Sat, 30 Jan 2021 10:40:34 +0100 Subject: [PATCH 15/15] Checkstyle: enforce spaces --- src/test/resources/checkstyle.xml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/test/resources/checkstyle.xml b/src/test/resources/checkstyle.xml index 3a97f7e..dcec557 100644 --- a/src/test/resources/checkstyle.xml +++ b/src/test/resources/checkstyle.xml @@ -8,6 +8,11 @@ + + + + +