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

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

Browse Source
This commit is contained in:
ucrhh 2021-02-03 15:27:30 +01:00
commit 3fba4ae1be
11 changed files with 120 additions and 59 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
frontend/src/mathjax-setup.js
View File

@ -85,6 +85,24 @@ window.MathJax = {
const OutputJax = startup.getOutputJax();
const html = mathjax.document(root, {InputJax, OutputJax});
html.render();
if (root.querySelector("#style-fixes") == null) {
const style = document.createElement('style');
style.type = "text/css";
style.innerHTML = "\
mjx-doc, mjx-body, mjx-container, #tc-content, svg {\
height: 100%;\
}\
mjx-container {\
margin: 0 !important;\
}\
";
console.log(root.host.tagName);
if (root.host.tagName === "TC-PROOF-TREE") {
style.innerHTML += "svg { width: 100%; }";
}
style.id = "style-fixes";
root.querySelector("mjx-head").appendChild(style);
}
const svg = root.querySelector("svg");
const nodeIterator = svg.querySelectorAll("g[data-mml-node='mtr']");
let counter = 0;

3
frontend/styles/view/proof-tree.css Normal file
View File

@ -0,0 +1,3 @@
tc-proof-tree {
flex: auto;
}

9
frontend/styles/view/type-inference.css Normal file
View File

@ -0,0 +1,9 @@
#scroller {
width: 100%;
height: 100%;
}
#content {
display: flex;
flex-direction: column;
height: 100%;
}

3
frontend/styles/view/unification.css Normal file
View File

@ -0,0 +1,3 @@
tc-unification {
flex: initial;
}

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

@ -18,22 +18,11 @@ import static edu.kit.typicalc.view.content.typeinferencecontent.LatexCreatorCon
* only use packages and commands that MathJax supports. The LaTeX code is also usable
* outside of MathJax, in a normal .tex document.
*/
public class LatexCreator implements StepVisitor, TypeVisitor {
public class LatexCreator implements StepVisitor {
private final TypeInfererInterface typeInferer;
private final StringBuilder tree;
private final boolean stepLabels;
/**
* Needed for visitor methods
*/
private String visitorBuffer = "";
/**
* Needed for visitor methods
*/
private boolean needsParentheses = false;
/**
* Generate the pieces of LaTeX-code from the type inferer.
*
@ -84,8 +73,7 @@ public class LatexCreator implements StepVisitor, TypeVisitor {
private String conclusionToLatex(Conclusion conclusion) {
String typeAssumptions = typeAssumptionsToLatex(conclusion.getTypeAssumptions());
String term = new LatexCreatorTerm(conclusion.getLambdaTerm()).getLatex();
conclusion.getType().accept(this);
String type = visitorBuffer;
String type = new LatexCreatorType(conclusion.getType()).getLatex();
return DOLLAR_SIGN + GAMMA + VDASH + term + COLON + type + DOLLAR_SIGN;
}
@ -103,10 +91,8 @@ public class LatexCreator implements StepVisitor, TypeVisitor {
}
private String generateConstraint(InferenceStep step) {
step.getConstraint().getFirstType().accept(this);
String firstType = visitorBuffer;
step.getConstraint().getSecondType().accept(this);
String secondType = visitorBuffer;
String firstType = new LatexCreatorType(step.getConstraint().getFirstType()).getLatex();
String secondType = new LatexCreatorType(step.getConstraint().getSecondType()).getLatex();
return firstType + SPACE + EQUAL_SIGN + SPACE + secondType;
}
@ -147,7 +133,7 @@ public class LatexCreator implements StepVisitor, TypeVisitor {
@Override
public void visit(ConstStepDefault constD) {
tree.insert(0, generateConclusion(constD, LABEL_CONST, UIC));
visitorBuffer = new LatexCreatorTerm(constD.getConclusion().getLambdaTerm()).getLatex();
String visitorBuffer = new LatexCreatorTerm(constD.getConclusion().getLambdaTerm()).getLatex();
String step = AXC + CURLY_LEFT + DOLLAR_SIGN + visitorBuffer + SPACE + LATEX_IN + SPACE + CONST
+ DOLLAR_SIGN + CURLY_RIGHT + NEW_LINE;
tree.insert(0, step);
@ -163,8 +149,7 @@ public class LatexCreator implements StepVisitor, TypeVisitor {
public void visit(VarStepWithLet varL) {
tree.insert(0, generateConclusion(varL, LABEL_VAR, BIC));
String typeAbstraction = generateTypeAbstraction(varL.getTypeAbsInPremise());
varL.getInstantiatedTypeAbs().accept(this);
String instantiatedType = visitorBuffer;
String instantiatedType = new LatexCreatorType(varL.getInstantiatedTypeAbs()).getLatex();
String premiseRight = AXC + CURLY_LEFT + DOLLAR_SIGN + typeAbstraction + INSTANTIATE_SIGN + instantiatedType
+ DOLLAR_SIGN + CURLY_RIGHT + NEW_LINE;
tree.insert(0, premiseRight);
@ -183,40 +168,4 @@ public class LatexCreator implements StepVisitor, TypeVisitor {
public void visit(EmptyStep empty) {
// TODO
}
@Override
public void visit(NamedType named) {
visitorBuffer = TEXTTT + CURLY_LEFT + named.getName() + CURLY_RIGHT;
needsParentheses = false;
}
@Override
public void visit(TypeVariable variable) {
String name;
switch (variable.getKind()) {
case TREE:
name = TREE_VARIABLE;
break;
case GENERATED_TYPE_ASSUMPTION:
name = GENERATED_ASSUMPTION_VARIABLE;
break;
case USER_INPUT:
name = USER_VARIABLE;
break;
default:
throw new IllegalStateException("unreachable code");
}
visitorBuffer = name + UNDERSCORE + CURLY_LEFT + variable.getIndex() + CURLY_RIGHT;
needsParentheses = false;
}
@Override
public void visit(FunctionType function) {
function.getParameter().accept(this);
String parameter = needsParentheses ? PAREN_LEFT + visitorBuffer + PAREN_RIGHT : visitorBuffer;
function.getOutput().accept(this);
String output = visitorBuffer;
visitorBuffer = parameter + SPACE + RIGHT_ARROW + SPACE + output;
needsParentheses = true;
}
}

69
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreatorType.java Normal file
View File

@ -0,0 +1,69 @@
package edu.kit.typicalc.view.content.typeinferencecontent;
import edu.kit.typicalc.model.type.FunctionType;
import edu.kit.typicalc.model.type.NamedType;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeVariable;
import edu.kit.typicalc.model.type.TypeVisitor;
import static edu.kit.typicalc.view.content.typeinferencecontent.LatexCreatorConstants.*;
public class LatexCreatorType implements TypeVisitor {
private final StringBuilder latex = new StringBuilder();
private boolean needsParentheses = false;
protected LatexCreatorType(Type type) {
type.accept(this);
}
protected String getLatex() {
return latex.toString();
}
@Override
public void visit(NamedType named) {
latex.append(TEXTTT);
latex.append(CURLY_LEFT);
latex.append(named.getName());
latex.append(CURLY_RIGHT);
needsParentheses = false;
}
@Override
public void visit(TypeVariable variable) {
String name;
switch (variable.getKind()) {
case TREE:
name = TREE_VARIABLE;
break;
case GENERATED_TYPE_ASSUMPTION:
name = GENERATED_ASSUMPTION_VARIABLE;
break;
case USER_INPUT:
name = USER_VARIABLE;
break;
default:
throw new IllegalStateException("unreachable code");
}
latex.append(name);
latex.append(UNDERSCORE);
latex.append(CURLY_LEFT);
latex.append(variable.getIndex());
latex.append(CURLY_RIGHT);
needsParentheses = false;
}
@Override
public void visit(FunctionType function) {
latex.append(PAREN_LEFT);
function.getParameter().accept(this);
latex.append(PAREN_RIGHT); // TODO: reduce parentheses
latex.append(SPACE);
latex.append(RIGHT_ARROW);
latex.append(SPACE);
latex.append(PAREN_LEFT);
function.getOutput().accept(this);
latex.append(PAREN_RIGHT); // TODO: reduce parentheses
needsParentheses = true;
}
}

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

@ -2,6 +2,7 @@ package edu.kit.typicalc.view.content.typeinferencecontent;
import com.vaadin.flow.component.ClientCallable;
import com.vaadin.flow.component.Tag;
import com.vaadin.flow.component.dependency.CssImport;
import com.vaadin.flow.component.dependency.JsModule;
import com.vaadin.flow.component.html.Div;
import com.vaadin.flow.component.littemplate.LitTemplate;
@ -16,6 +17,7 @@ import edu.kit.typicalc.view.MathjaxAdapter;
@Tag("tc-proof-tree")
@JsModule("./src/mathjax-adapter.ts")
@JsModule("./src/mathjax-proof-tree.ts")
@CssImport("./styles/view/proof-tree.css")
public class MathjaxProofTree extends LitTemplate implements MathjaxAdapter {
private int stepCount = -1;

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

@ -1,6 +1,7 @@
package edu.kit.typicalc.view.content.typeinferencecontent;
import com.vaadin.flow.component.Tag;
import com.vaadin.flow.component.dependency.CssImport;
import com.vaadin.flow.component.dependency.JsModule;
import com.vaadin.flow.component.html.Div;
import com.vaadin.flow.component.littemplate.LitTemplate;
@ -14,6 +15,7 @@ import edu.kit.typicalc.view.MathjaxAdapter;
@Tag("tc-unification")
@JsModule("./src/mathjax-adapter.ts")
@JsModule("./src/mathjax-unification.ts")
@CssImport("./styles/view/unification.css")
public class MathjaxUnification extends LitTemplate implements MathjaxAdapter {
private final String[] latex;

7
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java
View File

@ -2,6 +2,7 @@ package edu.kit.typicalc.view.content.typeinferencecontent;
import com.vaadin.flow.component.AttachEvent;
import com.vaadin.flow.component.ComponentEventListener;
import com.vaadin.flow.component.dependency.CssImport;
import com.vaadin.flow.component.html.Div;
import com.vaadin.flow.component.orderedlayout.Scroller;
import com.vaadin.flow.component.orderedlayout.VerticalLayout;
@ -14,8 +15,11 @@ import edu.kit.typicalc.view.main.MainViewImpl;
@Route(value = "visualize", layout = MainViewImpl.class)
@PageTitle("TypeInferenceView")
@CssImport("./styles/view/type-inference.css")
public class TypeInferenceView extends VerticalLayout
implements ControlPanelView, ComponentEventListener<AttachEvent> {
private static final String SCROLLER_ID = "scroller";
private static final String CONTENT_ID = "content";
private int currentStep = 0;
@ -31,9 +35,10 @@ public class TypeInferenceView extends VerticalLayout
setSizeFull();
addAttachListener(this);
content = new Div();
content.setId(CONTENT_ID);
controlPanel = new ControlPanel(this, this);
Scroller scroller = new Scroller(content);
scroller.setSizeFull();
scroller.setId(SCROLLER_ID);
scroller.setScrollDirection(Scroller.ScrollDirection.BOTH);
setAlignItems(Alignment.CENTER);
add(scroller, controlPanel);

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

@ -8,7 +8,7 @@ root.operatingHelp=Bedienhilfen
root.inputSyntax=Eingabe Syntax
root.inferenceRules=Ableitungsregeln
root.absRule=Abs-Regel
root.overlongInput=Die maximale Länge der Eingabe beträgt 1000 Zeichen!
root.overlongInput=Die maximale Länge der Eingabe beträgt 1000 Zeichen!
abs-rule=\
\\begin{prooftree}\

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

@ -3,6 +3,7 @@ root.copyLatex=Copy latex code
root.typicalc=Typicalc
root.examplebutton=📂
root.selectExample=Select example:
root.inferenceRules=Inference Rules
root.typeInfer=Type
abs-rule=\