diff --git a/frontend/styles/view/main/assumption-example-content.css b/frontend/styles/view/main/assumption-example-content.css new file mode 100644 index 0000000..eaf0758 --- /dev/null +++ b/frontend/styles/view/main/assumption-example-content.css @@ -0,0 +1,11 @@ +#selected-term-bar { + display: flex; + align-items: center; + padding-top: 0; + margin-top: 0; +} + +#selected-term { + margin-top: 0; + width: 100%; +} \ No newline at end of file diff --git a/frontend/styles/view/main/example-dialog.css b/frontend/styles/view/main/example-dialog.css index 234a86f..e4be10e 100644 --- a/frontend/styles/view/main/example-dialog.css +++ b/frontend/styles/view/main/example-dialog.css @@ -10,4 +10,9 @@ right: 0; position: absolute; bottom: 2.1em; +} + +#exampleContainer { + padding: 0; + margin: 0; } \ No newline at end of file diff --git a/src/main/java/edu/kit/typicalc/view/main/AssumptionExampleContent.java b/src/main/java/edu/kit/typicalc/view/main/AssumptionExampleContent.java new file mode 100644 index 0000000..2aa3f63 --- /dev/null +++ b/src/main/java/edu/kit/typicalc/view/main/AssumptionExampleContent.java @@ -0,0 +1,54 @@ +package edu.kit.typicalc.view.main; + +import java.util.function.Consumer; + +import org.apache.commons.lang3.StringUtils; + +import com.vaadin.flow.component.button.Button; +import com.vaadin.flow.component.dependency.CssImport; +import com.vaadin.flow.component.icon.Icon; +import com.vaadin.flow.component.icon.VaadinIcon; +import com.vaadin.flow.component.orderedlayout.VerticalLayout; +import com.vaadin.flow.component.textfield.TextField; + +/** + * + * + */ +@CssImport("./styles/view/main/assumption-example-content.css") +public class AssumptionExampleContent extends VerticalLayout { + private static final long serialVersionUID = -8157345417001452273L; + + private static final String SELECTED_TERM_BAR_ID = "selected-term-bar"; // exchange with better name + private static final String SELCETED_TERM_ID = "selected-term"; + + /** + * Sets up the type assumptions for the previously selected term. + * + * @param term the term previously selected by the user + * @param forwardCallback callback to start the algorithm with the chosen example + * @param backwardsCallback callback to return to the terms selection stage + */ + protected AssumptionExampleContent(String term, Consumer forwardCallback, Runnable backwardsCallback) { + TextField selectedTerm = new TextField(); + selectedTerm.setLabel(getTranslation("root.selectedTerm")); + selectedTerm.setValue(term); + selectedTerm.setReadOnly(true); + selectedTerm.setId(SELCETED_TERM_ID); + + Icon goBack = VaadinIcon.ANGLE_DOUBLE_LEFT.create(); + goBack.addClickListener(event -> backwardsCallback.run()); + + VerticalLayout selectedTermBar = new VerticalLayout(goBack, selectedTerm); + selectedTermBar.setId(SELECTED_TERM_BAR_ID); + this.add(selectedTermBar); + + String[] exampleAssumptions = getTranslation("root." + term.replaceAll("(\\s+|=)", "")).split(","); + for (String assumptions : exampleAssumptions) { + Button button = new Button(assumptions); + button.addClickListener(click -> forwardCallback.accept(assumptions. + replace(getTranslation("root.emptySet"), StringUtils.EMPTY))); + this.add(button); + } + } +} 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 023213a..8d5f97d 100644 --- a/src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java +++ b/src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java @@ -1,6 +1,9 @@ package edu.kit.typicalc.view.main; -import com.vaadin.flow.component.button.Button; +import java.util.function.Consumer; + +import org.apache.commons.lang3.tuple.Pair; + import com.vaadin.flow.component.dependency.CssImport; import com.vaadin.flow.component.dialog.Dialog; import com.vaadin.flow.component.html.H3; @@ -11,29 +14,35 @@ import com.vaadin.flow.component.orderedlayout.VerticalLayout; import com.vaadin.flow.i18n.LocaleChangeEvent; import com.vaadin.flow.i18n.LocaleChangeObserver; -import java.util.function.Consumer; - /** - * Contains all predefined examples as buttons. - * Clicking on a button inserts the example string into the input field. + * Contains all predefined term examples as buttons. + * Clicking on a button allows the user choose between a number of type assumptions. + * Selecting the type assumptions inserts the selected term as well as the type assumptions into their + * respective input fields. */ @CssImport("./styles/view/main/example-dialog.css") public class ExampleDialog extends Dialog implements LocaleChangeObserver { - - private static final long serialVersionUID = 8718432784530464215L; - + private static final long serialVersionUID = -428675165625776559L; + private static final String HEADING_LAYOUT_ID = "headingLayout"; private static final String EXAMPLE_DIALOG_ID = "exampleDialog"; private static final String CLOSE_ICON_ID = "closeIcon"; - + private static final String EXAMPLE_CONTAINER_ID = "exampleContainer"; + private final H3 instruction; + private final transient Consumer> setExamples; + private final VerticalLayout container; + + private String selectedTerm = null; /** * Creates a new ExampleDialog with a callback method that will receive the selected example. * - * @param callback function to handle the selected lambda term + * @param callback function to handle the selected lambda term and type assumptions */ - protected ExampleDialog(Consumer callback) { + protected ExampleDialog(Consumer> callback) { + setExamples = callback; + instruction = new H3(); HorizontalLayout headingLayout = new HorizontalLayout(); headingLayout.setId(HEADING_LAYOUT_ID); @@ -44,24 +53,37 @@ public class ExampleDialog extends Dialog implements LocaleChangeObserver { headingLayout.add(instruction); headingLayout.add(closeIcon); - - String[] examples = getTranslation("root.exampleTerms").split(","); - VerticalLayout layout = new VerticalLayout(); - for (String term : examples) { - Button button = new Button(term); - button.addClickListener(click -> { - callback.accept(term); - this.close(); - }); - button.setId(term); // needed for integration test - layout.add(button); - } - add(headingLayout, layout); + + container = new VerticalLayout(); + setTermExamples(); + container.setId(EXAMPLE_CONTAINER_ID); + + add(headingLayout, container); setId(EXAMPLE_DIALOG_ID); + setWidth("392px"); + setHeight("661px"); } - + + private void setAssumptionExamples(String term) { + selectedTerm = term; + container.removeAll(); + container.add(new AssumptionExampleContent(term, this::finishExampleSelection, this::setTermExamples)); + instruction.setText(getTranslation("root.selectAssumptions")); + } + + private void setTermExamples() { + container.removeAll(); + container.add(new TermExampleContent(this::setAssumptionExamples)); + instruction.setText(getTranslation("root.selectTerm")); + } + + private void finishExampleSelection(String assumptions) { + setExamples.accept(Pair.of(selectedTerm, assumptions)); + this.close(); + } + @Override public void localeChange(LocaleChangeEvent event) { - instruction.setText(getTranslation("root.selectExample")); + instruction.setText(getTranslation("root.selectTerm")); } } 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 8b1e9bd..8bdfaa2 100644 --- a/src/main/java/edu/kit/typicalc/view/main/InputBar.java +++ b/src/main/java/edu/kit/typicalc/view/main/InputBar.java @@ -107,7 +107,7 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver { } /** - * Sets the provided string as the value of the inputField. + * Sets the provided string as the value of the termInputField. * * @param term the provided string */ @@ -124,8 +124,14 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver { assumptionInputField.setValue(typeAssumptions); } - protected void setTermAndClickTypeInfer(String term) { - setTerm(term); + /** + * Set to provided input as the value of the termInputField and assumptionInputField. + * + * @param input pair of a term (left) and type assumptions (right) + */ + protected void setInputAndClickTypeInfer(Pair input) { + setTerm(input.getLeft()); + assumptionInputField.setValue(input.getRight()); onTypeInferButtonClick(); } @@ -146,7 +152,7 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver { } private void onExampleButtonClick() { - Dialog exampleDialog = new ExampleDialog(this::setTermAndClickTypeInfer); + Dialog exampleDialog = new ExampleDialog(this::setInputAndClickTypeInfer); exampleDialog.open(); } diff --git a/src/main/java/edu/kit/typicalc/view/main/TermExampleContent.java b/src/main/java/edu/kit/typicalc/view/main/TermExampleContent.java new file mode 100644 index 0000000..924c5e2 --- /dev/null +++ b/src/main/java/edu/kit/typicalc/view/main/TermExampleContent.java @@ -0,0 +1,30 @@ +package edu.kit.typicalc.view.main; + + +import java.util.function.Consumer; + +import com.vaadin.flow.component.button.Button; +import com.vaadin.flow.component.orderedlayout.VerticalLayout; + +/** + * Contains all predefined examples as buttons. + * Clicking on a button selects the example and allows the user to chose between various type assumptions. + */ +public class TermExampleContent extends VerticalLayout { + private static final long serialVersionUID = 2882744650931562239L; + + /** + * Sets up the predefined examples with a callback method that will receive the selected example. + * + * @param callback function to handle the selected lambda term + */ + protected TermExampleContent(Consumer callback) { + String[] exampleTerms = getTranslation("root.exampleTerms").split(","); + for (String term : exampleTerms) { + Button button = new Button(term); + button.addClickListener(click -> callback.accept(term)); + button.setId(term); // needed for integration test + this.add(button); + } + } +} diff --git a/src/main/resources/language/general.properties b/src/main/resources/language/general.properties index c829e3c..1196244 100644 --- a/src/main/resources/language/general.properties +++ b/src/main/resources/language/general.properties @@ -3,21 +3,33 @@ root.german=Deutsch root.english=English root.lambda=\u03BB root.allQuantifier=∀ +root.emptySet=∅ root.examplebutton=\uD83D\uDCC2 root.exampleTerms=\ - \u03BBx.x,\ - \u03BBx.\u03BBy.y x,\ - \u03BBx.\u03BBy.y (x x),\ - let f = \u03BBx. g y y in f 3,\ - let k = \u03BBx.\u03BBy. x in k a (k b c),\ - (\u03BBx.x x) (\u03BBx.x x),\ - (\u03BBx.\u03BBy.y (x y)) (\u03BBz. \u03BBa. z g a),\ - let f = \u03BBx. let g = \u03BBy. y in g x in f 3,\ - let f = \u03BBx. let g = \u03BBy.5 5 in g x in f 3 + λx.x,\ + λx.λy.y x,\ + λx.λy.y (x x),\ + let f = λx. g y y in f 3,\ + let k = λx.λy. x in k a (k b c),\ + (λx.x x) (λx.x x),\ + (λx.λy.y (x y)) (λz. λa. z g a),\ + let f = λx. let g = λy. y in g x in f 3,\ + let f = λx. let g = λy.5 5 in g x in f 3 + +root.λx.x=∅, x: int, y: bool +root.λx.λy.yx=∅, x: int, y: bool +root.λx.λy.y(xx)=∅, x: int, y: bool +root.letfλx.gyyinf3=∅, g: a->b->a, g: int->int->bool, g: int->int->bool; y: bool, g: int->int->bool; y: τ₁ +root.letkλx.λy.xinka(kbc)=∅, a: τ₁, a: ∀τ₁.τ₁->int; b: a, a: int; b: bool; c: char +root.(λx.xx)(λx.xx)=∅, x: bool +root.(λx.λy.y(xy))(λz.λa.zga)=∅, g: bool, a: int; g: bool->int, g: ∀τ₂.τ₁->τ₂ +root.letfλx.letgλy.yingxinf3=∅, g: bool->int->bool +root.letfλx.letgλy.55ingxinf3=∅, f: bool->int->bool + root.termGrammar=\u2329Term\u232A ::= (\u2329Term\u232A) | \u2329App\u232A | \u2329Abs\u232A | \ \u2329Let\u232A | \u2329Var\u232A | \u2329Const\u232A
\ \u2329App\u232A ::= \u2329Term\u232A \u2329Term\u232A
\ -\u2329Abs\u232A ::= \u03BB\u2329Var\u232A.\u2329Term\u232A
\ +\u2329Abs\u232A ::= λ\u2329Var\u232A.\u2329Term\u232A
\ \u2329Let\u232A ::= let \u2329Var\u232A = \u2329Term\u232A in \u2329Term\u232A
\ \u2329Var\u232A ::= [a-zA-Z][a-zA-Z0-9]*
\ \u2329Const\u232A ::= [0-9]+ | true | false diff --git a/src/main/resources/language/translation_de.properties b/src/main/resources/language/translation_de.properties index ba5083e..c856e58 100644 --- a/src/main/resources/language/translation_de.properties +++ b/src/main/resources/language/translation_de.properties @@ -2,7 +2,8 @@ root.close=Schließen root.save=Speichern root.copied=LaTeX-Code in Zwischenablage kopiert. root.exampleButton=📂 Beispiele -root.selectExample=Beispiel auswählen: +root.selectTerm=Term auswählen: +root.selectAssumptions=Typannahmen auswählen: root.termLabel=Term root.typeInfer=Typisieren root.operatingHelp=Hilfe @@ -45,8 +46,9 @@ eine Auflistung aller Typinferenzregeln. \ Mit Hilfe des Kopieren-Knopfs kann der Latex-Code der jeweiligen Regel in die Zwischenablage kopiert werden. \ Durch Betätigen des Ableitungsregeln-Knopfs wird das Fenster wieder geschlossen. root.helpExample=Durch Benutzen des Knopfs öffnet sich der Beispiel-Dialog. \ -Nach Anklicken wird der jeweilige Beispielterm in das Eingabefeld eingefügt. \ -Der Term kann nun nach Belieben angepasst oder direkt typisiert werden. +Nach Anklicken eines Beispielterms wird eine Reihe von Typannahmen angezeigt. \ +Mit dem Auswählen einer Menge von Typannahmen werden der Beispielterm und die Typannahmen in ihr jewiliges \ +Eingabefeld eigefügt. Anschließend startet direkt der Typinferenzalgorithmus. root.helpInputField=In das Eingabefeld können Lambda-Terme mit einer Länge von bis zu 1000 Zeichen eingegeben werden. \ Das λ-Zeichen kann dabei entweder durch Klicken des λ-Knopfs oder durch Eingabe eines Backslashs \ eingefügt werden. Durch Klicken des Info-Symbols wird die korrekte Syntax eines Terms \ @@ -164,6 +166,7 @@ root.lastStepTooltip=Letzter Schritt root.firstStepTooltip=Erster Schritt root.previousStepTooltip=Vorheriger Schritt root.nextStepTooltip=Nächster Schritt +root.selectedTerm=Ausgewählter Term root.absLetLatex=\ \\begin{prooftree}\ diff --git a/src/main/resources/language/translation_en.properties b/src/main/resources/language/translation_en.properties index af04a39..94da0c6 100644 --- a/src/main/resources/language/translation_en.properties +++ b/src/main/resources/language/translation_en.properties @@ -2,7 +2,8 @@ root.close=Close root.save=Save root.copied=LaTeX code copied to clipboard. root.exampleButton=📂 Examples -root.selectExample=Select example: +root.selectTerm=Select Term: +root.selectAssumptions=Select Assumptions: root.termLabel=Term root.typeInfer=Type root.operatingHelp=Help @@ -43,9 +44,9 @@ root.inferenceViewFeatures=Inference Tree And Unification root.helpDrawer=Clicking on type inference rules button opens up a collection of all type inference \ rules. By clicking on the copy button the LaTeX code of the corresponding rule is copied to the clipboard. \ The window can be closed by pressing the type inference rules button again. -root.helpExample=Clicking on the button opens up the example dialog. After clicking on an example the corresponding \ -term is inserted into the input field. Now either the type inference algorithm can be started or the term can be \ -modified. +root.helpExample=Clicking on the button opens up the example dialog. After clicking on an example term a number of \ +type assumptions show up. Selecting a set of type assumptions will insert the term and the type assumptions into their \ +respective input fields and automatically start the type inference algorithm. root.helpInputField=The input field allows the user to enter lambda terms with a maximum length of 1000 characters. \ The λ character can be inserted by either clicking the λ button or entering a backslash. \ By clicking on the info icon the grammar defining the valid input syntax is shown. @@ -154,6 +155,7 @@ root.lastStepTooltip=Last step root.firstStepTooltip=First step root.previousStepTooltip=Previous step root.nextStepTooltip=Next step +root.selectedTerm=Selected term root.absLetLatex=\ \\begin{prooftree}\