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

frontend/styles/view/main/help-dialog.css

@@ -0,0 +1,7 @@
+#contentLayout {
+	height: 80vh;
+}
+
+#headingLayout {
+	width: 80vw;
+}

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 {

src/main/java/edu/kit/typicalc/model/type/FunctionType.java

@@ -29,7 +29,7 @@ public class FunctionType extends Type {
      */
     @Override
     public boolean contains(Type x) {
-        return (contains(parameter) || contains(output));
+        return (parameter.contains(x) || output.contains(x));
     }
 
     /**
@@ -43,18 +43,18 @@ public class FunctionType extends Type {
     public FunctionType substitute(TypeVariable a, Type b) {
         boolean first = false;
         boolean second = false;
-        if (this.parameter.equals(a)) {
+        if (this.parameter.contains(a)) {
             first = true;
         }
-        if (this.output.equals(a)) {
+        if (this.output.contains(a)) {
              second = true;
         }
         if (first && second) {
-            return new FunctionType(b, b);
+            return new FunctionType(parameter.substitute(a, b), output.substitute(a, b));
         } else if (first) {
-            return new FunctionType(b, output);
+            return new FunctionType(parameter.substitute(a, b), output);
         } else if (second) {
-            return new FunctionType(parameter, b);
+            return new FunctionType(parameter, output.substitute(a, b));
         } else {
             return this;
         }

src/main/java/edu/kit/typicalc/presenter/Presenter.java

@@ -2,6 +2,9 @@ package edu.kit.typicalc.presenter;
 
 import java.util.Map;
 import edu.kit.typicalc.model.Model;
+import edu.kit.typicalc.model.TypeInfererInterface;
+import edu.kit.typicalc.model.parser.ParseError;
+import edu.kit.typicalc.util.Result;
 import edu.kit.typicalc.view.main.MainView;
 import edu.kit.typicalc.view.main.MainView.MainViewListener;
 
@@ -25,7 +28,11 @@ public class Presenter implements MainViewListener {
 
     @Override
     public void typeInferLambdaString(String lambdaTerm, Map<String, String> typeAssumptions) {
-        //TODO: Wo den Error verarbeiten? Wahrscheinlich Parameter von setTypeInferenceView ändern
-        view.setTypeInferenceView(model.getTypeInferer(lambdaTerm, typeAssumptions).unwrap());
+        Result<TypeInfererInterface, ParseError> result = model.getTypeInferer(lambdaTerm, typeAssumptions);
+        if (result.isError()) {
+            view.displayError(result.unwrapError());
+        } else {
+            view.setTypeInferenceView(result.unwrap());
+        }
     }
 }

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<String> EXAMPLES =
             List.of("λx.x", "λx.λy.y x", "λx.λy.y (x x)", "let f = λx. g y y in f 3", "(λx.x x) (λx.x x)");
+    private Paragraph instruction;
 
     public ExampleDialog(Consumer<String> 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"));
     }
 }

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"));
+    }
+}

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

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();
     }

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();
+    }    
 }

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}\

src/test/java/edu/kit/typicalc/model/type/FunctionTypeTest.java

@@ -0,0 +1,47 @@
+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);
+        TypeVariable typeVariable2 = new TypeVariable(TypeVaribaleKind.USER_INPUT, 2);
+        TypeVariable typeVariable3 = new TypeVariable(TypeVaribaleKind.USER_INPUT, 3);
+
+        FunctionType functionType1 = new FunctionType(typeVariable1, typeVariable2);
+
+        FunctionType newType = functionType1.substitute(typeVariable1, typeVariable3);
+
+        assertEquals(newType, new FunctionType(typeVariable3, typeVariable2));
+    }
+
+    @Test
+    void substitute2() {
+        TypeVariable typeVariable1 = new TypeVariable(TypeVaribaleKind.USER_INPUT, 1);
+        TypeVariable typeVariable2 = new TypeVariable(TypeVaribaleKind.USER_INPUT, 2);
+        TypeVariable typeVariable3 = new TypeVariable(TypeVaribaleKind.USER_INPUT, 3);
+        TypeVariable typeVariable4 = new TypeVariable(TypeVaribaleKind.USER_INPUT, 4);
+
+        FunctionType functionType1 = new FunctionType(typeVariable1, typeVariable2);
+        FunctionType functionType2 = new FunctionType(functionType1, typeVariable3);
+
+        FunctionType newType = functionType2.substitute(typeVariable1, typeVariable4);
+
+        assertEquals(newType, new FunctionType(new FunctionType(typeVariable4, typeVariable2), typeVariable3));
+    }
+}