arnekeller/Typicalc
1
0
Fork 0
mirror of https://gitlab.kit.edu/uskyk/typicalc.git synced 2024-11-09 10:50:42 +00:00
Code Issues Packages Projects Releases Wiki Activity

add mathjax proof tree

Browse Source
This commit is contained in:
ucrhh 2021-01-28 14:50:25 +01:00
parent e114e7e3f5
commit 2c62690428
6 changed files with 107 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
frontend/src/mathjax-proof-tree.ts Normal file
View File

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

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

@ -6,6 +6,7 @@ import com.vaadin.flow.component.orderedlayout.VerticalLayout;
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.main.MainViewImpl;
import edu.kit.typicalc.view.main.MathjaxDisplay;
@ -21,6 +22,7 @@ public class StartPageView extends VerticalLayout {
// todo implement correctly
setId("start-page");
add(new MathjaxDisplay());
add(new MathjaxProofTree());
sayHello = new Button("Say hello");
add(sayHello);
}

22
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxProofTree.java Normal file
View File

@ -0,0 +1,22 @@
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;
@Tag("tc-proof-tree")
@JsModule("./src/mathjax-proof-tree.ts")
public class MathjaxProofTree extends LitTemplate {
@Id("tc-content")
private Div content;
/**
* todo Creates the hello world template.
*/
public MathjaxProofTree() {
content.add(getTranslation("demo-tree"));
}
}

2
src/main/java/edu/kit/typicalc/view/main/MathjaxDisplay.java
View File

@ -13,7 +13,7 @@ public class MathjaxDisplay extends LitTemplate {
@Id("tc-content")
private Div content;
/**
* Creates the hello world template.
* todo Creates the hello world template.
*/
public MathjaxDisplay() {
content.add(getTranslation("abs-rule"));

36
src/main/resources/language/translation_de.properties
View File

@ -1,8 +1,11 @@
root.close=Schließen
root.copyLatex=Kopiere Latex-Code
root.typicalc=Typicalc
root.lambda=\u03BB
root.typeInfer=Typisieren
abs-rule=\\begin{prooftree}\
abs-rule=\
\\begin{prooftree}\
\\AxiomC{$\\Gamma=\\vdash t_1 : \\tau_1 \\rightarrow \\tau_2$}\
\
\\AxiomC{$\\Gamma \\vdash t_2 : \\tau_1$}\
@ -11,7 +14,34 @@ abs-rule=\\begin{prooftree}\
\\BinaryInfC{$\\Gamma \\vdash t_1 \\ t_2 : \\tau_2$}\
\\end{prooftree}
root.lambda=\u03BB
root.typeInfer=Typisieren
demo-tree=\
\\begin{prooftree}\n\
\\AxiomC{$\\lapp{\\left( \\assmapping{\\lv{f}}{\\alpha_2}, \\assmapping{\\lv{x}}{\\alpha_4} \\right)}{\\left( \\lv{f} \\right) = \\alpha_6}$}\n\
\\LeftLabel{\\textsc{Var}}\n\
\\UnaryInfC{$\\ltype{\\assmapping{\\lv{f}}{\\alpha_2}, \\assmapping{\\lv{x}}{\\alpha_2}}{\\lv{f}}{\\alpha_6}$}\n\
\n\
\\AxiomC{$\\lapp{\\left( \\assmapping{\\lv{f}}{\\alpha_2}, \\assmapping{\\lv{x}}{\\alpha_4} \\right)}{\\left( \\lv{f} \\right) = \\alpha_8}$}\n\
\n\
\\LeftLabel{\\textsc{Var}}\n\
\\UnaryInfC{$\\ltype{\\assmapping{\\lv{f}}{\\alpha_2}, \\assmapping{\\lv{x}}{\\alpha_2}}{\\lv{f}}{\\alpha_8}$}\n\
\n\
\n\
\\AxiomC{$\\lapp{\\left( \\assmapping{\\lv{f}}{\\alpha_2}, \\assmapping{\\lv{x}}{\\alpha_4} \\right)}{\\left( \\lv{x} \\right) = \\alpha_9}$}\n\
\n\
\\LeftLabel{\\textsc{Var}}\n\
\\UnaryInfC{$\\ltype{\\assmapping{\\lv{f}}{\\alpha_2}, \\assmapping{\\lv{x}}{\\alpha_2}}{\\lv{x}}{\\alpha_9}$}\n\
\n\
\\LeftLabel{\\textsc{App}}\n\
\\BinaryInfC{$\\ltype{\\assmapping{\\lv{f}}{\\alpha_2}, \\assmapping{\\lv{x}}{\\alpha_2}}{\\lapp{\\lv{f}}{\\lv{x}}}{\\alpha_7}$}\n\
\n\
\\LeftLabel{\\textsc{App}}\n\
\\BinaryInfC{$\\ltype{\\assmapping{\\lv{f}}{\\alpha_2}, \\assmapping{\\lv{x}}{\\alpha_2}}{\\lapp{\\lv{f}}{\\left( \\lapp{\\lv{f}}{\\lv{x}} \\right)}}{\\alpha_5}$}\n\
\n\
\\LeftLabel{\\textsc{Abs}}\n\
\\UnaryInfC{$\\ltype{\\assmapping{\\lv{f}}{\\alpha_2}}{\\la{x}{\\lapp{\\lv{f}}{\\left( \\lapp{\\lv{f}}{\\lv{x}} \\right) }}}{\\alpha_3}$}\n\
\n\
\\LeftLabel{\\textsc{Abs}}\n\
\\UnaryInfC{$\\ltype{}{\\la{f}{\\la{x}{\\lapp{\\lv{f}}{\\left( \\lapp{\\lv{f}}{\\lv{x}} \\right) }}}}{\\alpha_1}$}\n\
\\end{prooftree}

33
src/main/resources/language/translation_en.properties
View File

@ -1,6 +1,8 @@
root.close=Close
root.copyLatex=Copy latex code
root.typicalc=Typicalc
root.lambda=\u03BB
root.typeInfer=Typisieren
abs-rule=\
\\begin{prooftree}\n\
@ -11,5 +13,32 @@ abs-rule=\
\\BinaryInfC{$\\Gamma \\vdash t_1 \\ t_2 : \\tau_2$}\n\
\\end{prooftree}
root.lambda=\u03BB
root.typeInfer=Typisieren
demo-tree=\
\\begin{prooftree}\n\
\\AxiomC{$\\lapp{\\left( \\assmapping{\\lv{f}}{\\alpha_2}, \\assmapping{\\lv{x}}{\\alpha_4} \\right)}{\\left( \\lv{f} \\right) = \\alpha_6}$}\n\
\\LeftLabel{\\textsc{Var}}\n\
\\UnaryInfC{$\\ltype{\\assmapping{\\lv{f}}{\\alpha_2}, \\assmapping{\\lv{x}}{\\alpha_2}}{\\lv{f}}{\\alpha_6}$}\n\
\n\
\\AxiomC{$\\lapp{\\left( \\assmapping{\\lv{f}}{\\alpha_2}, \\assmapping{\\lv{x}}{\\alpha_4} \\right)}{\\left( \\lv{f} \\right) = \\alpha_8}$}\n\
\n\
\\LeftLabel{\\textsc{Var}}\n\
\\UnaryInfC{$\\ltype{\\assmapping{\\lv{f}}{\\alpha_2}, \\assmapping{\\lv{x}}{\\alpha_2}}{\\lv{f}}{\\alpha_8}$}\n\
\n\
\n\
\\AxiomC{$\\lapp{\\left( \\assmapping{\\lv{f}}{\\alpha_2}, \\assmapping{\\lv{x}}{\\alpha_4} \\right)}{\\left( \\lv{x} \\right) = \\alpha_9}$}\n\
\n\
\\LeftLabel{\\textsc{Var}}\n\
\\UnaryInfC{$\\ltype{\\assmapping{\\lv{f}}{\\alpha_2}, \\assmapping{\\lv{x}}{\\alpha_2}}{\\lv{x}}{\\alpha_9}$}\n\
\n\
\\LeftLabel{\\textsc{App}}\n\
\\BinaryInfC{$\\ltype{\\assmapping{\\lv{f}}{\\alpha_2}, \\assmapping{\\lv{x}}{\\alpha_2}}{\\lapp{\\lv{f}}{\\lv{x}}}{\\alpha_7}$}\n\
\n\
\\LeftLabel{\\textsc{App}}\n\
\\BinaryInfC{$\\ltype{\\assmapping{\\lv{f}}{\\alpha_2}, \\assmapping{\\lv{x}}{\\alpha_2}}{\\lapp{\\lv{f}}{\\left( \\lapp{\\lv{f}}{\\lv{x}} \\right)}}{\\alpha_5}$}\n\
\n\
\\LeftLabel{\\textsc{Abs}}\n\
\\UnaryInfC{$\\ltype{\\assmapping{\\lv{f}}{\\alpha_2}}{\\la{x}{\\lapp{\\lv{f}}{\\left( \\lapp{\\lv{f}}{\\lv{x}} \\right) }}}{\\alpha_3}$}\n\
\n\
\\LeftLabel{\\textsc{Abs}}\n\
\\UnaryInfC{$\\ltype{}{\\la{f}{\\la{x}{\\lapp{\\lv{f}}{\\left( \\lapp{\\lv{f}}{\\lv{x}} \\right) }}}}{\\alpha_1}$}\n\
\\end{prooftree}