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

src/main/java/edu/kit/typicalc/model/TypeInferer.java

@@ -45,7 +45,7 @@ public class TypeInferer implements TypeInfererInterface {
         unification = new Unification(tree.getConstraints());
 
         // cancel algorithm if term can't be typified
-        if (!unification.getSubstitutions().isOk()) {
+        if (unification.getSubstitutions().isError()) {
             typeInfResult = Optional.empty();
             return;
         }

src/main/java/edu/kit/typicalc/view/main/DrawerContent.java

@@ -6,6 +6,9 @@ import com.vaadin.flow.component.orderedlayout.VerticalLayout;
 import com.vaadin.flow.i18n.LocaleChangeEvent;
 import com.vaadin.flow.i18n.LocaleChangeObserver;
 
+/**
+ * Container for the components displayed in the drawer area of the web page.
+ */
 @CssImport("./styles/view/main/drawer-content.css")
 public class DrawerContent extends VerticalLayout implements LocaleChangeObserver {
 
@@ -20,7 +23,10 @@ public class DrawerContent extends VerticalLayout implements LocaleChangeObserve
     private final H3 heading;
     private final VerticalLayout ruleContainer;
 
-    public DrawerContent() {
+    /**
+     * Creates a new DrawerContent. 
+     */
+    protected DrawerContent() {
         heading = new H3(getTranslation("root.inferenceRules"));
         ruleContainer = new VerticalLayout();
         ruleContainer.setId(RULE_CONTAINER_ID);

src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java

@@ -10,6 +10,11 @@ import com.vaadin.flow.i18n.LocaleChangeObserver;
 import java.util.List;
 import java.util.function.Consumer;
 
+/**
+ * Contains all predefined examples as buttons. Clicking on a button inserts the example string into
+ * the input bar.
+ *
+ */
 public class ExampleDialog extends Dialog implements LocaleChangeObserver {
     
     private static final long serialVersionUID = 8718432784530464215L;
@@ -18,13 +23,22 @@ public class ExampleDialog extends Dialog implements LocaleChangeObserver {
             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 final Paragraph instruction;
 
-    public ExampleDialog(Consumer<String> callback) {
+    /**
+     * Creates a new ExampleDialog with a callback method to insert the example string into the input
+     * bar.
+     * 
+     * @param callback inserts the string of the chosen example into the input bar
+     */
+    protected ExampleDialog(Consumer<String> callback) {
         VerticalLayout layout = new VerticalLayout();
         instruction = new Paragraph(getTranslation("root.selectExample"));
         layout.add(instruction);
         for (String term : EXAMPLES) {
             Button button = new Button(term);
-            button.addClickListener(click -> callback.accept(term));
+            button.addClickListener(click -> {
+        	callback.accept(term);
+        	this.close();
+            });
             layout.add(button);
         }
         add(layout);

src/main/java/edu/kit/typicalc/view/main/HelpDialog.java

@@ -9,6 +9,9 @@ import com.vaadin.flow.component.orderedlayout.VerticalLayout;
 import com.vaadin.flow.i18n.LocaleChangeEvent;
 import com.vaadin.flow.i18n.LocaleChangeObserver;
 
+/**
+ * Contains information on how to use the application.
+ */
 @CssImport("./styles/view/main/help-dialog.css")
 public class HelpDialog extends Dialog implements LocaleChangeObserver {
     private static final long serialVersionUID = 4470277770276296164L;
@@ -22,7 +25,10 @@ public class HelpDialog extends Dialog implements LocaleChangeObserver {
     private final H3 heading;
     private final H5 inputSyntax;
 
-    public HelpDialog() {
+    /**
+     * Create a new HelpDialog.
+     */
+    protected HelpDialog() {
         final HorizontalLayout headingLayout = new HorizontalLayout();
         heading = new H3(getTranslation("root.operatingHelp"));
         headingLayout.setId(HEADING_LAYOUT_ID);

src/main/java/edu/kit/typicalc/view/main/InferenceRuleField.java

@@ -12,6 +12,11 @@ import com.vaadin.flow.component.orderedlayout.VerticalLayout;
 import com.vaadin.flow.i18n.LocaleChangeEvent;
 import com.vaadin.flow.i18n.LocaleChangeObserver;
 
+/**
+ * Visual representation of an inference rule. The component is composed of the rule itself (displayed
+ * in LaTeX rendered by MathJax), the name of the rule and a button to copy the LaTeX-code to the 
+ * clipboard. Each InferenceRuleField is displayed in drawer area of the web page.
+ */
 @CssImport("./styles/view/main/inference-rule-field.css")
 @JsModule("./src/copy-to-clipboard.js")
 public class InferenceRuleField extends VerticalLayout implements LocaleChangeObserver {
@@ -31,7 +36,14 @@ public class InferenceRuleField extends VerticalLayout implements LocaleChangeOb
     private final H4 ruleName;
     private final MathjaxDisplay rule;
     
-    public InferenceRuleField(final String latex, final String nameKey) {
+    /**
+     * Initializes an InferenceRuleField with a key to get the name of the inference rule and the LaTeX-code
+     * for its visual representation.
+     * 
+     * @param latex the LaTeX-code
+     * @param nameKey the key to get the name of the inference rule
+     */
+    protected InferenceRuleField(final String latex, final String nameKey) {
         this.nameKey = nameKey;
         
         final HorizontalLayout header = new HorizontalLayout();

src/test/java/edu/kit/typicalc/model/TreeTest.java

@@ -0,0 +1,42 @@
+package edu.kit.typicalc.model;
+
+import edu.kit.typicalc.model.term.VarTerm;
+import edu.kit.typicalc.model.type.NamedType;
+import edu.kit.typicalc.model.type.TypeAbstraction;
+import edu.kit.typicalc.model.type.TypeVariableKind;
+import org.junit.jupiter.api.BeforeAll;
+import org.junit.jupiter.api.Test;
+
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.Map;
+
+import static org.junit.jupiter.api.Assertions.assertEquals;
+
+class TreeTest {
+
+    private static final Map<VarTerm, TypeAbstraction> typeAssumptions = new HashMap<>();
+
+    @BeforeAll
+    static void setUp() {
+        typeAssumptions.put(new VarTerm("var"), new TypeAbstraction(new NamedType("type"), new ArrayList<>()));
+    }
+
+    @Test
+    void firstTypeVariableNewFactory() {
+        Tree tree = new Tree(typeAssumptions, new VarTerm("var"));
+        assertEquals(tree.getFirstTypeVariable(), new TypeVariableFactory(TypeVariableKind.TREE).nextTypeVariable());
+    }
+
+    @Test
+    void firstTypeVariableGivenFactory() {
+        TypeVariableFactory factory = new TypeVariableFactory(TypeVariableKind.TREE);
+        TypeVariableFactory factoryRef = new TypeVariableFactory(TypeVariableKind.TREE);
+        for (int i = 0; i < 10; i++) {
+            factory.nextTypeVariable();
+            factoryRef.nextTypeVariable();
+        }
+        Tree tree = new Tree(typeAssumptions, new VarTerm("var"), factory);
+        assertEquals(tree.getFirstTypeVariable(), factoryRef.nextTypeVariable());
+    }
+}