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

.gitlab-ci.yml

@@ -2,3 +2,8 @@ build:
   script:
     - mvn -Dmaven.repo.local=/tmp/m2/repository -Duser.home=/tmp checkstyle:check
     - mvn -Dmaven.repo.local=/tmp/m2/repository -Duser.home=/tmp test
+    - mvn -Dmaven.repo.local=/tmp/m2/repository -Duser.home=/tmp cobertura:cobertura
+    - "head target/site/cobertura/coverage.xml | rg --only-matching -r '$1' 'line-rate=\"([0-9.]+)\"' | awk '{ print \"Test Coverage: \" $1 * 100 \"%\" }'"
+  artifacts:
+    reports:
+      cobertura: target/site/cobertura/coverage.xml

frontend/src/mathjax-adapter.ts

@@ -0,0 +1,39 @@
+import {LitElement, html} from 'lit-element';
+import {TemplateResult} from "lit-html";
+
+declare let window: {
+    MathJax: {
+        typesetShadow: (arg0: ShadowRoot | null, arg1: () => void) => void,
+        isInitialized: boolean,
+    } | undefined;
+    addEventListener: (arg0: string, arg1: () => void) => void;
+};
+
+export abstract class MathjaxAdapter extends LitElement {
+    protected execTypeset() {
+        if (window.MathJax !== undefined) {
+            window.MathJax.typesetShadow(this.shadowRoot, () => this.calculateSteps());
+        }
+    }
+
+
+    render(): TemplateResult {
+        return html`<mjx-doc><mjx-head></mjx-head><mjx-body>
+            <div id="tc-content"></div>
+        </mjx-body></mjx-doc>`;
+    }
+
+    connectedCallback() {
+        super.connectedCallback();
+        if (window.MathJax === undefined || !window.MathJax.isInitialized) {
+            window.addEventListener('mathjax-initialized', () => this.execTypeset());
+        } else {
+            this.execTypeset();
+        }
+    }
+
+    protected abstract showStep(n: number): void;
+
+    protected abstract calculateSteps(): void;
+}
+

frontend/src/mathjax-display.ts

@@ -0,0 +1,18 @@
+import {MathjaxAdapter} from "./mathjax-adapter";
+import {TemplateResult} from "lit-html";
+
+class MathjaxDisplay extends MathjaxAdapter {
+
+    render(): TemplateResult {
+        return super.render();
+    }
+
+
+    protected showStep(_n: number): void {
+    }
+
+    protected calculateSteps(): void {
+    }
+}
+
+customElements.define('tc-display', MathjaxDisplay);

package.json

@@ -29,34 +29,51 @@
     "@vaadin/vaadin-select": "2.4.0",
     "@vaadin/vaadin-split-layout": "4.3.0",
     "@vaadin/vaadin-text-field": "2.8.2",
-    "lit-element": "2.3.1",
     "@vaadin/form": "./target/flow-frontend/form",
     "@vaadin/vaadin-avatar": "1.0.3",
-    "open": "^7.2.1"
+    "open": "^7.2.1",
+    "@vaadin/vaadin-crud": "1.3.0",
+    "@vaadin/vaadin-cookie-consent": "1.2.0",
+    "@vaadin/vaadin-upload": "4.4.1",
+    "@vaadin/vaadin-board": "2.2.0",
+    "@vaadin/vaadin-date-time-picker": "1.4.0",
+    "@vaadin/vaadin-login": "1.2.0",
+    "@vaadin/vaadin-accordion": "1.2.0",
+    "@vaadin/vaadin-checkbox": "2.5.0",
+    "@vaadin/vaadin-time-picker": "2.4.0",
+    "@vaadin/vaadin-context-menu": "4.5.0",
+    "@vaadin/vaadin-tabs": "3.2.0",
+    "@vaadin/vaadin-radio-button": "1.5.1",
+    "@vaadin/vaadin-rich-text-editor": "1.3.0",
+    "lit-element": "2.3.1",
+    "@vaadin/vaadin-core-shrinkwrap": "18.0.5",
+    "@vaadin/vaadin-grid-pro": "2.2.2",
+    "@vaadin/vaadin-shrinkwrap": "18.0.5",
+    "@vaadin/vaadin-date-picker": "4.4.1"
   },
   "devDependencies": {
+    "@types/validator": "13.1.0",
+    "awesome-typescript-loader": "5.2.1",
+    "chokidar": "^3.4.0",
+    "compression-webpack-plugin": "4.0.1",
+    "copy-webpack-plugin": "5.1.2",
+    "css-loader": "4.2.1",
+    "extract-loader": "5.1.0",
+    "html-webpack-plugin": "3.2.0",
+    "lit-css-loader": "0.0.4",
+    "lit-element": "^2.3.1",
+    "lit-html": "1.2.1",
+    "progress-webpack-plugin": "0.0.24",
+    "raw-loader": "4.0.0",
+    "script-ext-html-webpack-plugin": "2.1.4",
+    "terser": "4.6.7",
+    "typescript": "4.0.3",
+    "validator": "13.1.17",
     "webpack": "4.42.0",
+    "webpack-babel-multi-target-plugin": "2.3.3",
     "webpack-cli": "3.3.11",
     "webpack-dev-server": "3.11.0",
-    "webpack-babel-multi-target-plugin": "2.3.3",
-    "copy-webpack-plugin": "5.1.2",
-    "webpack-merge": "4.2.2",
-    "raw-loader": "4.0.0",
-    "compression-webpack-plugin": "4.0.1",
-    "html-webpack-plugin": "3.2.0",
-    "script-ext-html-webpack-plugin": "2.1.4",
-    "awesome-typescript-loader": "5.2.1",
-    "typescript": "4.0.3",
-    "terser": "4.6.7",
-    "progress-webpack-plugin": "0.0.24",
-    "lit-element": "2.3.1",
-    "chokidar": "^3.4.0",
-    "validator": "13.1.17",
-    "lit-html": "1.2.1",
-    "@types/validator": "13.1.0",
-    "css-loader": "4.2.1",
-    "lit-css-loader": "0.0.4",
-    "extract-loader": "5.1.0"
+    "webpack-merge": "4.2.2"
   },
   "vaadin": {
     "dependencies": {
@@ -89,7 +106,24 @@
       "@vaadin/vaadin-custom-field": "1.3.0",
       "lit-element": "2.3.1",
       "@vaadin/vaadin-avatar": "1.0.3",
-      "open": "^7.2.1"
+      "open": "^7.2.1",
+      "@vaadin/vaadin-crud": "1.3.0",
+      "@vaadin/vaadin-cookie-consent": "1.2.0",
+      "@vaadin/vaadin-core-shrinkwrap": "18.0.5",
+      "@vaadin/vaadin-upload": "4.4.1",
+      "@vaadin/vaadin-board": "2.2.0",
+      "@vaadin/vaadin-charts": "7.0.0",
+      "@vaadin/vaadin-grid-pro": "2.2.2",
+      "@vaadin/vaadin-shrinkwrap": "18.0.5",
+      "@vaadin/vaadin-date-time-picker": "1.4.0",
+      "@vaadin/vaadin-login": "1.2.0",
+      "@vaadin/vaadin-date-picker": "4.4.1",
+      "@vaadin/vaadin-accordion": "1.2.0",
+      "@vaadin/vaadin-checkbox": "2.5.0",
+      "@vaadin/vaadin-time-picker": "2.4.0",
+      "@vaadin/vaadin-tabs": "3.2.0",
+      "@vaadin/vaadin-radio-button": "1.5.1",
+      "@vaadin/vaadin-rich-text-editor": "1.3.0"
     },
     "devDependencies": {
       "webpack-babel-multi-target-plugin": "2.3.3",
@@ -115,6 +149,6 @@
       "lit-css-loader": "0.0.4",
       "extract-loader": "5.1.0"
     },
-    "hash": "176a855b9845a8bd6e1b6138940c86e0431291e79479361d27a18a7b50bd4678"
+    "hash": "04462da9d778f9542e7732e145ac4b9dbdea38fe120e57367afe34d62fd3024a"
   }
 }

pom.xml

@@ -154,6 +154,17 @@
                 <artifactId>maven-surefire-plugin</artifactId>
                 <version>2.22.2</version>
             </plugin>
+            <plugin>
+                <groupId>org.codehaus.mojo</groupId>
+                <artifactId>cobertura-maven-plugin</artifactId>
+                <version>2.7</version>
+                <configuration>
+                    <check/>
+                    <formats>
+                        <format>xml</format>
+                    </formats>
+                </configuration>
+            </plugin>
 
             <plugin>
                 <artifactId>maven-checkstyle-plugin</artifactId>
@@ -255,4 +266,20 @@
         </profile>
 
     </profiles>
+
+    <reporting>
+        <plugins>
+            <plugin>
+                <groupId>org.codehaus.mojo</groupId>
+                <artifactId>cobertura-maven-plugin</artifactId>
+                <version>2.7</version>
+                <configuration>
+                    <check/>
+                    <formats>
+                        <format>xml</format>
+                    </formats>
+                </configuration>
+            </plugin>
+        </plugins>
+    </reporting>
 </project>

src/main/java/edu/kit/typicalc/model/parser/ParseError.java

@@ -6,11 +6,14 @@ public enum ParseError {
      *  the lambda term didn't meet the specified syntax
      */
     UNEXPECTED_TOKEN,
-    
+
+    /**
+     * some tokens were remaining after parsing a full lambda term
+     */
     TOO_MANY_TOKENS,
 
     /**
-     * the String contained a character not allowed in that place
+     * the string contained a character not allowed in that context
      */
     UNEXPECTED_CHARACTER
 }

src/main/java/edu/kit/typicalc/model/term/BooleanTerm.java

@@ -2,6 +2,8 @@ package edu.kit.typicalc.model.term;
 
 import edu.kit.typicalc.model.type.NamedType;
 
+import java.util.Objects;
+
 /**
  * Representation of a constant boolean lambda term: either false or true.
  */
@@ -30,4 +32,21 @@ public class BooleanTerm extends ConstTerm {
 	public String toString() {
 		return Boolean.toString(value);
 	}
+
+	@Override
+	public boolean equals(Object o) {
+		if (this == o) {
+			return true;
+		}
+		if (o == null || getClass() != o.getClass()) {
+			return false;
+		}
+		BooleanTerm that = (BooleanTerm) o;
+		return value == that.value;
+	}
+
+	@Override
+	public int hashCode() {
+		return Objects.hash(value);
+	}
 }

src/main/java/edu/kit/typicalc/view/content/infocontent/StartPageView.java

@@ -8,6 +8,7 @@ import com.vaadin.flow.router.PageTitle;
 import com.vaadin.flow.router.Route;
 import com.vaadin.flow.router.RouteAlias;
 import edu.kit.typicalc.view.main.MainViewImpl;
+import edu.kit.typicalc.view.main.MathjaxDisplay;
 
 @Route(value = "home", layout = MainViewImpl.class)
 @PageTitle("Typicalc")
@@ -18,10 +19,12 @@ public class StartPageView extends VerticalLayout {
     private Button sayHello;
 
     public StartPageView() {
+        // todo implement correctly
         setId("start-page");
         name = new TextArea("translation test");
         name.setValue(getTranslation("abs-rule"));
         name.setWidthFull();
+        add(new MathjaxDisplay());
         sayHello = new Button("Say hello");
         add(name, sayHello);
         sayHello.addClickListener(e -> {

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

@@ -0,0 +1,22 @@
+package edu.kit.typicalc.view.main;
+
+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;
+
+@Tag("tc-display")
+@JsModule("./src/mathjax-display.ts")
+public class MathjaxDisplay extends LitTemplate {
+
+    @Id("tc-content")
+    private Div content;
+    /**
+     * Creates the hello world template.
+     */
+    public MathjaxDisplay() {
+        content.add("testtestetstest");
+    }
+}
+

src/test/java/edu/kit/typicalc/model/parser/LambdaParserTest.java

@@ -4,6 +4,7 @@ import static org.junit.jupiter.api.Assertions.assertEquals;
 
 import edu.kit.typicalc.model.term.AbsTerm;
 import edu.kit.typicalc.model.term.AppTerm;
+import edu.kit.typicalc.model.term.BooleanTerm;
 import edu.kit.typicalc.model.term.ConstTerm;
 import edu.kit.typicalc.model.term.IntegerTerm;
 import edu.kit.typicalc.model.term.LambdaTerm;
@@ -49,4 +50,31 @@ class LambdaParserTest {
 						)
 				));
 	}
+	@Test
+	void complicatedTerm() {
+		LambdaParser parser = new LambdaParser("(λx.λy.x y 5)(λz.z)(true)");
+		assertEquals(parser.parse().unwrap(),
+				new AppTerm(
+						new AppTerm(
+								new AbsTerm(
+										new VarTerm("x"),
+										new AbsTerm(
+												new VarTerm("y"),
+												new AppTerm(
+														new AppTerm(
+																new VarTerm("x"),
+																new VarTerm("y")
+														),
+														new IntegerTerm(5)
+												)
+										)
+								),
+								new AbsTerm(
+										new VarTerm("z"),
+										new VarTerm("z")
+								)
+						),
+						new BooleanTerm(true)
+				));
+	}
 }