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

frontend/src/mathjax-unification.ts

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

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

@@ -1,20 +1,15 @@
 package edu.kit.typicalc.view;
 
-import com.vaadin.flow.component.littemplate.LitTemplate;
-
 /**
  * Represents an HTML element that uses MathJax and custom JavaScript classes to render its contents.
  * Provides an interface between Java code and said JavaScript classes. Allows to reveal parts of the
  * rendered LaTeX step-by-step. Allows for scaling of the rendered LaTeX.
  */
-public abstract class MathjaxAdapter extends LitTemplate {
+public interface MathjaxAdapter {
 
-    /**
-     * Creates a new HTML element that renders the LaTeX string passed as parameter using MathJax. Because
-     * MathJax is used to render the String, all LaTeX commands used must be MathJax compatible.
-     * @param latex the LaTex string to render with MathJax
-     */
-    protected MathjaxAdapter(String latex) {
+    int getStepCount();
 
-    }
+    void showStep(int n);
+
+    void scale(double newScaling);
 }

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

@@ -7,6 +7,7 @@ import com.vaadin.flow.router.PageTitle;
 import com.vaadin.flow.router.Route;
 import com.vaadin.flow.router.RouteAlias;
 import edu.kit.typicalc.view.content.typeinferencecontent.MathjaxProofTree;
+import edu.kit.typicalc.view.content.typeinferencecontent.MathjaxUnification;
 import edu.kit.typicalc.view.main.MainViewImpl;
 import edu.kit.typicalc.view.main.MathjaxDisplay;
 
@@ -21,8 +22,9 @@ public class StartPageView extends VerticalLayout {
     public StartPageView() {
         // todo implement correctly
         setId("start-page");
-        add(new MathjaxDisplay());
-        add(new MathjaxProofTree());
+        add(new MathjaxDisplay(getTranslation("abs-rule")));
+        add(new MathjaxUnification("\\(constraint test \\vdash \\)"));
+        add(new MathjaxProofTree(getTranslation("demo-tree")));
         sayHello = new Button("Say hello");
         add(sayHello);
     }

src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreator.java

@@ -24,6 +24,8 @@ import edu.kit.typicalc.model.type.TypeVisitor;
  */
 public class LatexCreator implements StepVisitor, TermVisitor, TypeVisitor {
 
+    private static final String EQUAL_SIGN = "=";
+
     private static final String LABEL_ABS = "\\LeftLabel{ABS}";
     private static final String LABEL_APP = "\\LeftLabel{APP}";
     private static final String LABEL_CONST = "\\LeftLabel{CONST}";
@@ -43,6 +45,11 @@ public class LatexCreator implements StepVisitor, TermVisitor, TypeVisitor {
     private final StringBuilder tree;
     private final boolean stepLabels;
 
+    /**
+     * Needed for typeVisitor methods
+     */
+    private String typeBuffer;
+
     /**
      * Generate the pieces of LaTeX-code from the type inferer.
      *
@@ -64,28 +71,28 @@ public class LatexCreator implements StepVisitor, TermVisitor, TypeVisitor {
      */
     protected String getTree() {
         return null;
-    }
+    } // todo implement
 
     /**
      * @return the LaTeX-code for constraints nad unification
      */
     protected String getUnification() {
         return null;
-    }
+    } // todo implement
 
     /**
      * @return the packages needed for the LaTeX-code from getTree() and getUnification()to work
      */
     protected String getLatexPackages() {
         return null;
-    }
+    } // todo implement
 
     private String conclusionToLatex(Conclusion conclusion) {
         // todo implement
-        return "";
+        return "{some text}";
     }
 
-    private void generateConclusion(InferenceStep step, String label, String command) {
+    private StringBuilder generateConclusion(InferenceStep step, String label, String command) {
         StringBuilder conclusion = new StringBuilder();
         if (stepLabels) {
             conclusion.append(label);
@@ -94,52 +101,79 @@ public class LatexCreator implements StepVisitor, TermVisitor, TypeVisitor {
         conclusion.append(command);
         conclusion.append(conclusionToLatex(step.getConclusion()));
         conclusion.append(System.lineSeparator());
-        tree.insert(0, conclusion);
+        return conclusion;
     }
 
+    private StringBuilder generateConstraint(InferenceStep step) {
+        // todo implement maybe rename to addConstraint
+        StringBuilder constraint = new StringBuilder();
+        step.getConstraint().getFirstType().accept(this);
+        String firstType = typeBuffer;
+        step.getConstraint().getSecondType().accept(this);
+        String secondType = typeBuffer;
+        constraint.append(firstType)
+                .append(EQUAL_SIGN)
+                .append(secondType)
+                .append(System.lineSeparator());
+        return constraint;
+    }
+
+    // todo use generateConstraint
     @Override
     public void visit(AbsStepDefault absD) {
-        generateConclusion(absD, LABEL_ABS, UIC);
-
-
+        tree.insert(0, generateConclusion(absD, LABEL_ABS, UIC));
+        absD.getPremise().accept(this);
     }
 
     @Override
     public void visit(AbsStepWithLet absL) {
-        generateConclusion(absL, LABEL_ABS, UIC);
-
+        tree.insert(0, generateConclusion(absL, LABEL_ABS, UIC));
+        absL.getPremise().accept(this);
     }
 
     @Override
     public void visit(AppStepDefault appD) {
-        generateConclusion(appD, LABEL_APP, UIC);
-
+        tree.insert(0, generateConclusion(appD, LABEL_APP, BIC));
+        appD.getPremise2().accept(this);
+        appD.getPremise1().accept(this);
     }
 
     @Override
     public void visit(ConstStepDefault constD) {
-        generateConclusion(constD, LABEL_CONST, UIC);
-
+        tree.insert(0, generateConclusion(constD, LABEL_CONST, UIC));
+        // todo implement
+        StringBuilder temp = new StringBuilder();
+        temp.append(AXC).append("{const default}");
+        tree.insert(0, temp);
     }
 
     @Override
     public void visit(VarStepDefault varD) {
-        generateConclusion(varD, LABEL_VAR, UIC);
-
+        tree.insert(0, generateConclusion(varD, LABEL_VAR, UIC));
+        // todo implement
+        StringBuilder temp = new StringBuilder();
+        temp.append(AXC).append("{var default}");
+        tree.insert(0, temp);
     }
 
     @Override
     public void visit(VarStepWithLet varL) {
-        generateConclusion(varL, LABEL_VAR, UIC);
-
+        tree.insert(0, generateConclusion(varL, LABEL_VAR, UIC));
+        // todo implement
+        StringBuilder temp = new StringBuilder();
+        temp.append(AXC).append("{var with let}");
+        tree.insert(0, temp);
     }
 
     @Override
     public void visit(LetStepDefault letD) {
-        generateConclusion(letD, LABEL_LET, UIC);
-
+        tree.insert(0, generateConclusion(letD, LABEL_LET, BIC));
+        letD.getPremise().accept(this);
+        // todo implement
     }
 
+
+
     @Override
     public void visit(AppTerm appTerm) {
 
@@ -165,6 +199,8 @@ public class LatexCreator implements StepVisitor, TermVisitor, TypeVisitor {
 
     }
 
+
+
     @Override
     public void visit(NamedType named) {
 

src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxProofTree.java

@@ -5,18 +5,43 @@ 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;
+import edu.kit.typicalc.view.MathjaxAdapter;
 
+/**
+ * Renders a tree from LaTeX using MathJax and allows for step-by-step-revealing for
+ * proof trees that use the bussproofs package. Relies on MathjaxProofTreeJS to interact
+ * with MathJax.
+ */
 @Tag("tc-proof-tree")
 @JsModule("./src/mathjax-proof-tree.ts")
-public class MathjaxProofTree extends LitTemplate {
+public class MathjaxProofTree extends LitTemplate implements MathjaxAdapter {
 
     @Id("tc-content")
     private Div content;
+
     /**
-     * todo Creates the hello world template.
+     * Creates a new HTML element that renders the proof tree and cuts it into steps.
+     * The latex String must consist of exactly one proof tree environment in order for
+     * this element to work. In other cases the expected behaviour is undefined.
+     * @param latex the LaTeX-String to render with MathJax
      */
-    public MathjaxProofTree() {
-        content.add(getTranslation("demo-tree"));
+    public MathjaxProofTree(String latex) {
+        content.add(latex);
+    }
+
+    @Override
+    public int getStepCount() {
+        return 0;
+    }
+
+    @Override
+    public void showStep(int n) {
+
+    }
+
+    @Override
+    public void scale(double newScaling) {
+
     }
 }
 

src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxUnification.java

@@ -0,0 +1,46 @@
+package edu.kit.typicalc.view.content.typeinferencecontent;
+
+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;
+import edu.kit.typicalc.view.MathjaxAdapter;
+
+/**
+ * Renders the constraints and unification from LaTeX using MathJax and allows step-by-
+ * step-revealing capabilities. Relies on MathjaxUnificationJS to interact with MathJax.
+ */
+@Tag("tc-unification")
+@JsModule("./src/mathjax-unification.ts")
+public class MathjaxUnification extends LitTemplate implements MathjaxAdapter {
+
+    @Id("tc-content")
+    private Div content;
+
+    /**
+     * Creates a new HTML element that renders the constraints and unification and
+     * calculates the steps.
+     * @param latex the LaTeX-String to render with MathJax
+     */
+    public MathjaxUnification(String latex) {
+        content.add(latex);
+    }
+
+    @Override
+    public int getStepCount() {
+        // todo implement
+        return 0;
+    }
+
+    @Override
+    public void showStep(int n) {
+        // todo implement
+    }
+
+    @Override
+    public void scale(double newScaling) {
+        // todo implement
+    }
+}
+

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

@@ -6,6 +6,7 @@ import com.vaadin.flow.component.applayout.DrawerToggle;
 import com.vaadin.flow.component.avatar.Avatar;
 import com.vaadin.flow.component.button.Button;
 import com.vaadin.flow.component.dependency.CssImport;
+import com.vaadin.flow.component.dependency.JavaScript;
 import com.vaadin.flow.component.dependency.JsModule;
 import com.vaadin.flow.component.html.H1;
 import com.vaadin.flow.component.html.Image;
@@ -20,14 +21,15 @@ import com.vaadin.flow.component.tabs.Tabs;
 import edu.kit.typicalc.model.ModelImpl;
 import edu.kit.typicalc.model.TypeInfererInterface;
 import edu.kit.typicalc.model.parser.ParseError;
-import edu.kit.typicalc.view.content.typeinferencecontent.TypeInferenceView;
 import edu.kit.typicalc.presenter.Presenter;
+import edu.kit.typicalc.view.content.typeinferencecontent.TypeInferenceView;
 
 /**
  * The main view is a top-level placeholder for other views.
  */
 @CssImport("./styles/view/main/main-view.css")
 @JsModule("./styles/shared-styles.js")
+@JavaScript("./src/tex-svg-full.js")
 public class MainViewImpl extends AppLayout implements MainView {
 
     private H1 viewTitle;

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

@@ -1,24 +1,44 @@
 package edu.kit.typicalc.view.main;
 
 import com.vaadin.flow.component.Tag;
-import com.vaadin.flow.component.dependency.JavaScript;
 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;
+import edu.kit.typicalc.view.MathjaxAdapter;
 
+/**
+ * Renders static LaTeX content using MathJax. Relies on MathjaxDisplayJS to interact
+ * with MathJax.
+ */
 @Tag("tc-display")
 @JsModule("./src/mathjax-display.ts")
-@JavaScript("./src/tex-svg-full.js")
-public class MathjaxDisplay extends LitTemplate {
+public class MathjaxDisplay extends LitTemplate implements MathjaxAdapter {
 
     @Id("tc-content")
     private Div content;
     /**
-     * todo Creates the hello world template.
+     * Creates a new HTML element that renders the LaTeX code.
+     *
+     * @param latex the LaTeX string to render with MathJax
      */
-    public MathjaxDisplay() {
-        content.add(getTranslation("abs-rule"));
+    public MathjaxDisplay(String latex) {
+        content.add(latex);
+    }
+
+    @Override
+    public int getStepCount() {
+        return 0;
+    }
+
+    @Override
+    public void showStep(int n) {
+        // do nothing
+    }
+
+    @Override
+    public void scale(double newScaling) {
+        // todo implement
     }
 }