Add type assumption examples

This commit is contained in:
Moritz Dieing 2021-07-05 18:01:38 +02:00
parent 116aea51c3
commit 1581985400
9 changed files with 192 additions and 47 deletions

View File

@ -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%;
}

View File

@ -10,4 +10,9 @@
right: 0;
position: absolute;
bottom: 2.1em;
}
#exampleContainer {
padding: 0;
margin: 0;
}

View File

@ -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<String> 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);
}
}
}

View File

@ -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<Pair<String, String>> 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<String> callback) {
protected ExampleDialog(Consumer<Pair<String, String>> 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"));
}
}

View File

@ -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
*/
@ -127,8 +127,14 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
.collect(Collectors.joining("; ")));
}
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<String, String> input) {
setTerm(input.getLeft());
assumptionInputField.setValue(input.getRight());
onTypeInferButtonClick();
}
@ -149,7 +155,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();
}

View File

@ -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<String> 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);
}
}
}

View File

@ -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 <br> \
\u2329App\u232A ::= \u2329Term\u232A \u2329Term\u232A <br> \
\u2329Abs\u232A ::= \u03BB\u2329Var\u232A.\u2329Term\u232A <br> \
\u2329Abs\u232A ::= λ\u2329Var\u232A.\u2329Term\u232A <br> \
\u2329Let\u232A ::= <b>let</b> \u2329Var\u232A = \u2329Term\u232A <b>in</b> \u2329Term\u232A <br> \
\u2329Var\u232A ::= [a-zA-Z][a-zA-Z0-9]* <br> \
\u2329Const\u232A ::= [0-9]+ | true | false

View File

@ -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 \
@ -162,6 +164,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}\

View File

@ -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.
@ -152,6 +153,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}\