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:
Moritz Dieing 2021-02-05 18:49:13 +01:00
commit 4d44136528
28 changed files with 213 additions and 137 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
frontend/src/mathjax-adapter.ts
View File

@ -40,14 +40,5 @@ export abstract class MathjaxAdapter extends LitElement {
protected calculateSteps(): void {
}
// connectedCallback() {
// super.connectedCallback();
// if (window.MathJax === undefined || !window.MathJax.isInitialized) {
// window.addEventListener('mathjax-initialized', () => this.execTypeset(this.shadowRoot));
// } else {
// this.execTypeset(this.shadowRoot);
// }
// }
}

30
frontend/src/mathjax-proof-tree.ts
View File

@ -61,8 +61,7 @@ class MathjaxProofTree extends MathjaxAdapter {
let dx = termAbove.getBBox().x;
termAbove = termAbove.parentElement as HTMLElement & SVGGraphicsElement;
while (true) {
// @ts-ignore
if (termAbove.parentNode.getAttribute("semantics") === "bspr_inferenceRule:down") {
if ((termAbove.parentNode! as HTMLElement).getAttribute("semantics") === "bspr_inferenceRule:down") {
break;
}
if (termAbove.transform.baseVal !== null) {
@ -103,7 +102,6 @@ class MathjaxProofTree extends MathjaxAdapter {
parent.removeAttribute("id");
}
const rule = a.querySelector("#" + id + " g[semantics=\"bspr_inferenceRule:down\"]");
console.log(rule);
if (rule !== null) {
let i = 0;
for (const node of rule.childNodes) {
@ -124,39 +122,43 @@ class MathjaxProofTree extends MathjaxAdapter {
steps.push([a, above]);
}
}
// TODO: also fix line length (some are too long AND some are too short)
// this will involve running the algorithm below a second time
const svg = this.shadowRoot.querySelector<SVGElement>("svg")!;
const nodeIterator2 = svg.querySelectorAll<SVGGraphicsElement>("g[data-mml-node='mtr']");
const nodeIterator2 = [...svg.querySelectorAll<SVGGraphicsElement>("g[data-mml-node='mtr']")];
// start layout fixes in the innermost part of the SVG
nodeIterator2.reverse();
const padding = 300;
let counter = 0;
for (const a of nodeIterator2) {
counter++;
let left = null;
let i = 0;
for (const node of a.childNodes) {
for (const rawNode of a.childNodes) {
const node = rawNode as SVGGraphicsElement;
if (i === 1 || i === 3) {
i += 1;
continue;
}
// @ts-ignore
const bbox = node.getBBox();
// @ts-ignore
const mat = node.transform.baseVal[0];
if (mat !== undefined) {
bbox.x += mat.matrix.e;
}
// 500 space between inference steps
// TODO: somehow broken since moving this algorithm to the TS file
// move box, and add padding between inference steps
if (left == null) {
left = bbox.x + bbox.width + 500;
left = bbox.x + bbox.width;
} else {
mat.matrix.e -= bbox.x - left;
left = bbox.x + mat.matrix.e + bbox.width + 500;
mat.matrix.e -= bbox.x - left - padding;
left = bbox.x + mat.matrix.e + bbox.width;
}
i += 1;
}
}
// @ts-ignore
const bbox = svg.childNodes[1].getBBox();
svg.setAttribute("viewBox", bbox.x + " " + bbox.y + " " + bbox.width + " " + bbox.height)
const bbox = (svg.childNodes[1] as SVGGraphicsElement).getBBox();
// TODO: this does not work when using a permalink
svg.setAttribute("viewBox", bbox.x + " " + bbox.y + " " + bbox.width + " " + bbox.height);
if (counter >= 3) {
// should not be used on empty SVGs
// @ts-ignore

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

@ -84,6 +84,10 @@ window.MathJax = {
if (root.getElementById("tc-content") == null) {
return;
}
const mjxContainer = root.querySelector<HTMLElement>("mjx-container");
if (mjxContainer !== null) {
mjxContainer.innerHTML = "";
}
const InputJax = startup.getInputJax();
const OutputJax = startup.getOutputJax();
const html = mathjax.document(root, {InputJax, OutputJax});
@ -106,7 +110,6 @@ mjx-container {\
margin: 0 !important;\
}\
";
console.log(root.host.tagName);
if (hostTag === "tc-proof-tree") {
style.innerHTML += "svg { width: 100%; }";
}

9
pom.xml
View File

@ -233,6 +233,15 @@
<target>11</target>
</configuration>
</plugin>
<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-resources-plugin</artifactId>
<version>3.2.0</version>
<configuration>
<propertiesEncoding>UTF-8</propertiesEncoding>
</configuration>
</plugin>
</plugins>
</build>

2
src/main/java/edu/kit/typicalc/model/Conclusion.java
View File

@ -25,7 +25,7 @@ public class Conclusion {
* @param lambdaTerm the lambda term in the conclusion
* @param type the type assigned to the lambda term in the conclusion
*/
protected Conclusion(Map<VarTerm, TypeAbstraction> typeAssumptions, LambdaTerm lambdaTerm, Type type) {
public Conclusion(Map<VarTerm, TypeAbstraction> typeAssumptions, LambdaTerm lambdaTerm, Type type) {
this.typeAssumptions = typeAssumptions;
this.lambdaTerm = lambdaTerm;
this.type = type;

13
src/main/java/edu/kit/typicalc/model/parser/LambdaLexer.java
View File

@ -111,20 +111,21 @@ public class LambdaLexer {
advance();
return new Result<>(t);
default:
if (Character.isLetter(c)) {
// only allow ascii characters in variable names
if (Character.isLetter(c) && (int) c < 128) {
int startPos = pos;
// identifier
StringBuilder sb = new StringBuilder();
do {
sb.append(term.charAt(pos));
advance();
} while (pos < term.length() && Character.isLetterOrDigit(term.charAt(pos)));
String s = sb.toString();
TokenType type;
// only allow ascii characters in variable names
if (!s.matches("\\A\\p{ASCII}*\\z")) {
} while (pos < term.length() && Character.isLetterOrDigit(term.charAt(pos))
&& (int) term.charAt(pos) < 128);
if (pos < term.length() && (int) term.charAt(pos) >= 128) {
return new Result<>(null, ParseError.UNEXPECTED_CHARACTER);
}
String s = sb.toString();
TokenType type;
switch (s) {
case "let":
type = TokenType.LET;

1
src/main/java/edu/kit/typicalc/model/parser/TypeAssumptionParser.java
View File

@ -40,7 +40,6 @@ public class TypeAssumptionParser {
}
private Result<Pair<Type, Integer>, ParseError> parseType(LambdaLexer lexer, int parenCount) {
// TODO: remove misc. logging
Result<Token, ParseError> token = lexer.nextToken();
if (token.isError()) {
return new Result<>(token);

9
src/main/java/edu/kit/typicalc/model/step/EmptyStep.java
View File

@ -2,6 +2,10 @@ package edu.kit.typicalc.model.step;
import edu.kit.typicalc.model.Conclusion;
import edu.kit.typicalc.model.Constraint;
import edu.kit.typicalc.model.term.VarTerm;
import edu.kit.typicalc.model.type.NamedType;
import java.util.Collections;
/**
* Empty steps are used if the sub-inference that is started when creating a let step failed and the second premise of
@ -13,7 +17,10 @@ public class EmptyStep extends InferenceStep {
* Initializes a new empty step.
*/
public EmptyStep() {
super(null, null); // TODO
super(
new Conclusion(Collections.emptyMap(), new VarTerm(""), new NamedType("")),
new Constraint(new NamedType(""), new NamedType(""))
); // TODO: better dummy parameters?
}
@Override

2
src/main/java/edu/kit/typicalc/model/type/UnificationUtil.java
View File

@ -11,6 +11,8 @@ import java.util.Optional;
/**
* Utility class to avoid unification logic duplication in type methods.
*
* @see Type
*/
final class UnificationUtil {
private UnificationUtil() { }

5
src/main/java/edu/kit/typicalc/view/MathjaxAdapter.java
View File

@ -3,13 +3,12 @@ package edu.kit.typicalc.view;
/**
* 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.
* rendered LaTeX step-by-step.
*/
public interface MathjaxAdapter {
int getStepCount();
void showStep(int n);
void scale(double newScaling);
// TODO: document removal of scaling method
}

1
src/main/java/edu/kit/typicalc/view/content/ControlPanel.java
View File

@ -23,6 +23,7 @@ public class ControlPanel extends HorizontalLayout {
* Sets up buttons with click-listeners that call the corresponding method in the view.
*
* @param view the view that reacts to the button clicks
* @param focusArea the component key shortcuts should work in
*/
public ControlPanel(ControlPanelView view, Component focusArea) {
firstStep = new Button(new Icon(VaadinIcon.ANGLE_DOUBLE_LEFT), evt -> view.firstStepButton());

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

@ -12,7 +12,6 @@ import edu.kit.typicalc.view.content.typeinferencecontent.MathjaxProofTree;
import edu.kit.typicalc.view.content.typeinferencecontent.MathjaxUnification;
import edu.kit.typicalc.view.content.typeinferencecontent.ShareDialog;
import edu.kit.typicalc.view.main.MainViewImpl;
import edu.kit.typicalc.view.main.MathjaxDisplay;
@Route(value = "", layout = MainViewImpl.class)
@PageTitle("Typicalc")
@ -35,24 +34,13 @@ public class StartPageView extends VerticalLayout implements ControlPanelView {
scroller.setScrollDirection(Scroller.ScrollDirection.BOTH);
setAlignItems(Alignment.CENTER);
add(scroller, controlPanel);
// disableControlPanel();
disableControlPanel();
createContent();
}
private void createContent() {
String[] strings = new String[]{"$\\tau_0$", "$\\tau_1$", "$\\tau_2$", "$\\tau_3$", "$\\tau_4$",
"$\\tau_5$", "$\\tau_6$", "$\\tau_7$", "$\\tau_8$", "$\\tau_9$", "$\\tau_{10}$", "$\\tau_{11}$",
"$\\tau_{12}$", "$\\tau_{13}$", "$\\tau_{14}$"};
content.add(new MathjaxDisplay(getTranslation("abs-rule")));
unification = new MathjaxUnification(strings);
tree = new MathjaxProofTree(getTranslation("demo-tree"));
content.add(unification);
content.add(tree);
content.add(new MathjaxProofTree(getTranslation("demo-tree")));
content.add(new MathjaxProofTree(getTranslation("demo-tree")));
content.add(new MathjaxProofTree(getTranslation("demo-tree")));
content.add(new MathjaxProofTree(getTranslation("demo-tree")));
content.add("TODO");
}
private void disableControlPanel() {

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

@ -50,10 +50,5 @@ public class MathjaxProofTree extends LitTemplate implements MathjaxAdapter {
public void showStep(int n) {
getElement().callJsFunction("showStep", n);
}
@Override
public void scale(double newScaling) {
}
}

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

@ -46,10 +46,5 @@ public class MathjaxUnification extends LitTemplate implements MathjaxAdapter {
}
getElement().callJsFunction("showStep", n);
}
@Override
public void scale(double newScaling) {
// todo implement
}
}

33
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/ShareDialog.java
View File

@ -1,6 +1,11 @@
package edu.kit.typicalc.view.content.typeinferencecontent;
import com.vaadin.flow.component.Unit;
import com.vaadin.flow.component.dialog.Dialog;
import com.vaadin.flow.component.orderedlayout.FlexComponent;
import com.vaadin.flow.component.orderedlayout.VerticalLayout;
import com.vaadin.flow.component.textfield.TextArea;
import com.vaadin.flow.component.textfield.TextField;
import com.vaadin.flow.i18n.LocaleChangeEvent;
import com.vaadin.flow.i18n.LocaleChangeObserver;
@ -9,21 +14,45 @@ import com.vaadin.flow.i18n.LocaleChangeObserver;
*/
public class ShareDialog extends Dialog implements LocaleChangeObserver {
private final TextField urlField;
private final TextField packageField;
private final TextArea latexArea;
/**
* Sets up three GUI elements, one for each parameter. The content of each element is equal
* to the String that is passed as corresponding parameter.
* @param url a permalink to share with other users
* @param latexPackages the needed LaTeX-packages to use the displayed mathmatics
* @param latexPackages the needed LaTeX-packages to use the displayed mathematics
* in other LaTeX documents. Should be in the form „\\usepackage<package>“
* @param latexCode LaTeX code for users to copy into their own LaTeX document(s)
*/
public ShareDialog(String url, String latexPackages, String latexCode) {
setWidth(80, Unit.PERCENTAGE);
VerticalLayout layout = new VerticalLayout();
layout.setAlignItems(FlexComponent.Alignment.START);
layout.setSizeFull();
add(layout);
urlField = new TextField(getTranslation("share.url.label"));
packageField = new TextField(getTranslation("share.packages.label"));
latexArea = new TextArea(getTranslation("share.latex.label"));
urlField.setValue(url);
packageField.setValue(latexPackages);
latexArea.setValue(latexCode);
urlField.setWidthFull();
packageField.setWidthFull();
latexArea.setWidthFull();
layout.add(urlField, packageField, latexArea);
}
@Override
public void localeChange(LocaleChangeEvent localeChangeEvent) {
urlField.setLabel(getTranslation("share.url.label"));
packageField.setLabel(getTranslation("share.packages.label"));
latexArea.setLabel(getTranslation("share.latex.label"));
}
}

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

@ -18,37 +18,45 @@ import edu.kit.typicalc.view.main.MainViewImpl;
@CssImport("./styles/view/type-inference.css")
public class TypeInferenceView extends VerticalLayout
implements ControlPanelView, ComponentEventListener<AttachEvent> {
/**
* Route of this view.
*/
public static final String ROUTE = "infer";
private static final String SCROLLER_ID = "scroller";
private static final String CONTENT_ID = "content";
private static final String ID = "type-inference-view";
private int currentStep = 0;
private MathjaxUnification unification;
private MathjaxProofTree tree;
private final transient TypeInfererInterface typeInferer;
private final transient LatexCreator lc;
private final Div content;
private final ControlPanel controlPanel;
private final ShareDialog shareDialog;
public TypeInferenceView(TypeInfererInterface typeInferer) {
this.typeInferer = typeInferer;
setId(ID);
setSizeFull();
addAttachListener(this);
lc = new LatexCreator(typeInferer);
content = new Div();
content.setId(CONTENT_ID);
controlPanel = new ControlPanel(this, this);
ControlPanel controlPanel = new ControlPanel(this, this);
Scroller scroller = new Scroller(content);
scroller.setId(SCROLLER_ID);
scroller.setScrollDirection(Scroller.ScrollDirection.BOTH);
setAlignItems(Alignment.CENTER);
add(scroller, controlPanel);
setContent();
shareDialog = new ShareDialog(getTranslation("root.domain")
+ ROUTE + "/"
+ typeInferer.getFirstInferenceStep().getConclusion().getLambdaTerm(),
lc.getLatexPackages(), lc.getTree());
}
private void setContent() {
// todo implement correctly
LatexCreator lc = new LatexCreator(typeInferer);
unification = new MathjaxUnification(lc.getUnification());
tree = new MathjaxProofTree(lc.getTree());
content.add(unification, tree);
@ -56,7 +64,7 @@ public class TypeInferenceView extends VerticalLayout
@Override
public void shareButton() {
// todo implement
shareDialog.open();
}
private void refreshElements(int currentStep) {

6
src/main/java/edu/kit/typicalc/view/main/ErrorNotification.java
View File

@ -9,15 +9,15 @@ import com.vaadin.flow.component.orderedlayout.VerticalLayout;
public class ErrorNotification extends Notification {
private static final long serialVersionUID = 1L;
private static final long serialVersionUID = 239587L;
private static final String NOTIFICATION_ID = "errorNotification";
protected ErrorNotification(final String errorMessage) {
final VerticalLayout container = new VerticalLayout();
final Span errorSpan = new Span(errorMessage);
final Button closeButton = new Button(getTranslation("root.close"), event -> this.close());
container.add(errorSpan, closeButton);
container.setAlignItems(FlexComponent.Alignment.CENTER);
addThemeVariants(NotificationVariant.LUMO_ERROR);

20
src/main/java/edu/kit/typicalc/view/main/InferenceRuleField.java
View File

@ -14,15 +14,15 @@ 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
* 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 {
private static final long serialVersionUID = -8551851183297707985L;
/*
* IDs for the imported .css-file
*/
@ -30,32 +30,32 @@ public class InferenceRuleField extends VerticalLayout implements LocaleChangeOb
private static final String HEADER_ID = "headerField";
private static final String MAIN_ID = "main";
private static final String RULE_NAME_ID = "ruleName";
private final String nameKey;
private final Button copyButton;
private final H4 ruleName;
private final MathjaxDisplay rule;
/**
* 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();
header.setId(HEADER_ID);
this.ruleName = new H4(getTranslation(nameKey));
ruleName.setId(RULE_NAME_ID);
header.add(ruleName);
final VerticalLayout main = new VerticalLayout();
main.setId(MAIN_ID);
this.copyButton = new Button(getTranslation("root.copyLatex"), new Icon(VaadinIcon.CLIPBOARD));
this.rule = new MathjaxDisplay(latex); //TODO scale, when method implemented
MathjaxDisplay rule = new MathjaxDisplay(latex); //TODO scale, when method implemented
// TODO: scale to what exactly?
copyButton.addClickListener(event -> UI.getCurrent().getPage().executeJs("window.copyToClipboard($0)", latex));
main.add(rule, copyButton);
add(header, main);

7
src/main/java/edu/kit/typicalc/view/main/InfoDialog.java
View File

@ -13,13 +13,12 @@ import com.vaadin.flow.i18n.LocaleChangeEvent;
import com.vaadin.flow.i18n.LocaleChangeObserver;
/**
* Dialog which contains information on the correct syntax for the users input.
* Dialog which contains information on the correct syntax for the users input.
*/
@CssImport("./styles/view/main/info-dialog.css")
public class InfoDialog extends Dialog implements LocaleChangeObserver {
private static final long serialVersionUID = 2914411566361539614L;
/*
* IDs for the imported .css-file
*/
@ -29,7 +28,7 @@ public class InfoDialog extends Dialog implements LocaleChangeObserver {
private static final String CLOSE_ICON_ID = "closeIcon";
private final H4 heading;
/**
* Creates new InfoDialog.
* @throws Exception

47
src/main/java/edu/kit/typicalc/view/main/InputBar.java
View File

@ -14,7 +14,9 @@ import com.vaadin.flow.data.value.ValueChangeMode;
import com.vaadin.flow.i18n.LocaleChangeEvent;
import com.vaadin.flow.i18n.LocaleChangeObserver;
import org.apache.commons.lang3.StringUtils;
import org.apache.commons.lang3.tuple.Pair;
import java.util.Map;
import java.util.Optional;
import java.util.function.Consumer;
@ -35,10 +37,8 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
private static final short MAX_INPUT_LENGTH = 1000;
private final Icon infoIcon;
private final Button exampleButton;
private final Button lambdaButton;
private final TextField inputField;
private final TypeAssumptionsArea typeAssumptionsArea;
private final Button inferTypeButton;
/**
@ -47,8 +47,8 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
*
* @param callback Consumer to call the inferType()-method in UpperBar
*/
protected InputBar(final Consumer<String> callback) {
infoIcon = new Icon(VaadinIcon.INFO_CIRCLE);
protected InputBar(Consumer<Pair<String, Map<String, String>>> callback) {
Icon infoIcon = new Icon(VaadinIcon.INFO_CIRCLE);
infoIcon.addClickListener(event -> onInfoIconClick());
inputField = new TextField();
@ -56,24 +56,29 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
inputField.setClearButtonVisible(true);
inputField.setValueChangeMode(ValueChangeMode.EAGER);
inputField.addValueChangeListener(event -> onInputFieldValueChange());
lambdaButton = new Button(getTranslation("root.lambda"), event -> onLambdaButtonClick());
exampleButton = new Button(getTranslation("root.examplebutton"), event -> onExampleButtonClick());
Button lambdaButton = new Button(getTranslation("root.lambda"), event -> onLambdaButtonClick());
Button typeAssumptions = new Button(
getTranslation("root.typeAssumptions"),
event -> onTypeAssumptionsButton()
); // TODO
typeAssumptionsArea = new TypeAssumptionsArea();
Button exampleButton = new Button(getTranslation("root.examplebutton"), event -> onExampleButtonClick());
exampleButton.setId(EXAMPLE_BUTTON_ID);
inferTypeButton = new Button(getTranslation("root.typeInfer"), event -> onTypeInferButtonClick(callback));
inferTypeButton.addClickShortcut(Key.ENTER).listenOn(this);
inferTypeButton.addThemeVariants(ButtonVariant.LUMO_PRIMARY);
inferTypeButton.setId(INFER_BUTTON_ID);
add(infoIcon, exampleButton, lambdaButton, inputField, inferTypeButton);
add(infoIcon, exampleButton, lambdaButton, typeAssumptions, inputField, inferTypeButton);
setId(INPUT_BAR_ID);
}
/**
* Sets the provided string as the value of the inputField and starts the type inference algorithm.
*
*
* @param term the provided string
*/
protected void inferTerm(final String term) {
protected void inferTerm(String term) {
inputField.setValue(term);
inferTypeButton.click();
}
@ -83,11 +88,11 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
.setValue(value.replace("\\", getTranslation("root.lambda"))));
}
private void onTypeInferButtonClick(final Consumer<String> callback) {
final String currentInput = inputField.getOptionalValue().orElse(StringUtils.EMPTY);
private void onTypeInferButtonClick(Consumer<Pair<String, Map<String, String>>> callback) {
String currentInput = inputField.getOptionalValue().orElse(StringUtils.EMPTY);
if (currentInput.length() < MAX_INPUT_LENGTH) {
callback.accept(currentInput);
callback.accept(Pair.of(currentInput, typeAssumptionsArea.getTypeAssumptions()));
} else {
final Notification errorNotification = new ErrorNotification(getTranslation("root.overlongInput"));
errorNotification.open();
@ -95,25 +100,29 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
}
private void onLambdaButtonClick() {
final StringBuilder inputBuilder = new StringBuilder();
final Optional<String> currentInput = inputField.getOptionalValue();
StringBuilder inputBuilder = new StringBuilder();
Optional<String> currentInput = inputField.getOptionalValue();
currentInput.ifPresent(inputBuilder::append);
inputBuilder.append(getTranslation("root.lambda"));
inputField.setValue(inputBuilder.toString());
inputField.focus();
}
private void onTypeAssumptionsButton() {
typeAssumptionsArea.open();
}
private void onExampleButtonClick() {
final Consumer<String> setValue = value -> {
Consumer<String> setValue = value -> {
inputField.setValue(value);
inputField.focus();
};
final Dialog exampleDialog = new ExampleDialog(setValue);
Dialog exampleDialog = new ExampleDialog(setValue);
exampleDialog.open();
}
private void onInfoIconClick() {
final Dialog infoDialog = new InfoDialog();
Dialog infoDialog = new InfoDialog();
infoDialog.open();
}

17
src/main/java/edu/kit/typicalc/view/main/MainViewImpl.java
View File

@ -31,8 +31,6 @@ import java.util.List;
@JavaScript("./src/tex-svg-full.js")
public class MainViewImpl extends AppLayout implements MainView, HasErrorParameter<NotFoundException> {
private static final long serialVersionUID = -2411433187835906976L;
private static final String ROUTE = "infer";
private static final String SLASH = "/";
private final UpperBar upperBar;
@ -65,11 +63,11 @@ public class MainViewImpl extends AppLayout implements MainView, HasErrorParamet
BeforeEnterEvent event,
ErrorParameter<NotFoundException> parameter) {
if (event.getLocation().getPath().matches(ROUTE + SLASH + ".*")) {
if (event.getLocation().getPath().matches(TypeInferenceView.ROUTE + "/.*")) {
List<String> segments = event.getLocation().getSegments();
String term = segments.get(segments.size() - 1);
upperBar.inferTerm(decodeURL(term));
} else if (event.getLocation().getPath().equals(ROUTE)) {
} else if (event.getLocation().getPath().equals(TypeInferenceView.ROUTE)) {
setContent(new StartPageView());
upperBar.inferTerm(StringUtils.EMPTY);
} else if (event.getLocation().getPath().equals(StringUtils.EMPTY)) {
@ -81,16 +79,13 @@ public class MainViewImpl extends AppLayout implements MainView, HasErrorParamet
return HttpServletResponse.SC_OK;
}
private void setTermInURL(String lambdaTerm) {
UI.getCurrent().getPage().getHistory().replaceState(null, new Location(ROUTE + SLASH + lambdaTerm));
UI.getCurrent().getPage().getHistory().replaceState(null,
new Location(TypeInferenceView.ROUTE + "/" + lambdaTerm));
}
private String decodeURL(String encodedUrl) {
try {
return java.net.URLDecoder.decode(encodedUrl, StandardCharsets.UTF_8);
} catch (IllegalArgumentException e) {
return "";
}
return java.net.URLDecoder.decode(encodedUrl, StandardCharsets.UTF_8);
}
}

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

@ -36,10 +36,5 @@ public class MathjaxDisplay extends LitTemplate implements MathjaxAdapter {
public void showStep(int n) {
// do nothing
}
@Override
public void scale(double newScaling) {
// todo implement
}
}

9
src/main/java/edu/kit/typicalc/view/main/TypeAssumptionField.java Normal file
View File

@ -0,0 +1,9 @@
package edu.kit.typicalc.view.main;
import com.vaadin.flow.component.Component;
import com.vaadin.flow.component.Tag;
@Tag("tc-type-assumption")
public class TypeAssumptionField extends Component {
// TODO
}

39
src/main/java/edu/kit/typicalc/view/main/TypeAssumptionsArea.java Normal file
View File

@ -0,0 +1,39 @@
package edu.kit.typicalc.view.main;
import com.vaadin.flow.component.Component;
import com.vaadin.flow.component.Tag;
import com.vaadin.flow.component.dialog.Dialog;
import com.vaadin.flow.component.html.H3;
import com.vaadin.flow.component.orderedlayout.VerticalLayout;
import com.vaadin.flow.i18n.LocaleChangeEvent;
import com.vaadin.flow.i18n.LocaleChangeObserver;
import java.util.ArrayList;
import java.util.Collections;
import java.util.List;
import java.util.Map;
@Tag("tc-type-assumptions")
public class TypeAssumptionsArea extends Dialog implements LocaleChangeObserver {
private final List<TypeAssumptionField> fields = new ArrayList<>();
protected TypeAssumptionsArea() {
VerticalLayout layout = new VerticalLayout();
layout.add(new H3(getTranslation("root.typeAssumptions")));
fields.add(new TypeAssumptionField());
for (Component c : fields) {
layout.add(c);
}
// TODO
}
protected Map<String, String> getTypeAssumptions() {
// TODO
return Collections.emptyMap();
}
@Override
public void localeChange(LocaleChangeEvent event) {
// TODO
}
}

31
src/main/java/edu/kit/typicalc/view/main/UpperBar.java
View File

@ -16,13 +16,14 @@ import com.vaadin.flow.router.Location;
import edu.kit.typicalc.view.content.infocontent.StartPageView;
import edu.kit.typicalc.view.main.MainView.MainViewListener;
import org.apache.commons.lang3.StringUtils;
import org.apache.commons.lang3.tuple.Pair;
import java.util.HashMap;
import java.util.Map;
import java.util.function.Consumer;
/**
* Contains all the components constantly shown in the upper part of the webage.
* Contains all the components constantly shown in the upper part of the webpage.
*/
@CssImport("./styles/view/main/upper-bar.css")
public class UpperBar extends HorizontalLayout implements LocaleChangeObserver {
@ -36,9 +37,7 @@ public class UpperBar extends HorizontalLayout implements LocaleChangeObserver {
private static final String HELP_ICON_ID = "helpIcon";
private static final String UPPER_BAR_ID = "header";
private final H1 viewTitle;
private final InputBar inputBar;
private final Icon helpIcon;
private final Button rules;
private final transient MainViewListener presenter;
@ -51,18 +50,18 @@ public class UpperBar extends HorizontalLayout implements LocaleChangeObserver {
* @param setContent function to set the content of the application
* @param setTermInURL function to set the term into the URL
*/
protected UpperBar(final MainViewListener presenter, final Consumer<Component> setContent,
final Consumer<String> setTermInURL) {
protected UpperBar(MainViewListener presenter, Consumer<Component> setContent,
Consumer<String> setTermInURL) {
this.presenter = presenter;
this.setTermInURL = setTermInURL;
this.viewTitle = new H1(getTranslation("root.typicalc"));
H1 viewTitle = new H1(getTranslation("root.typicalc"));
viewTitle.addClickListener(event -> routeToStartPage(setContent));
viewTitle.setId(VIEW_TITLE_ID);
this.inputBar = new InputBar(this::typeInfer);
inputBar.setId(INPUT_BAR_ID);
this.helpIcon = new Icon(VaadinIcon.QUESTION_CIRCLE);
Icon helpIcon = new Icon(VaadinIcon.QUESTION_CIRCLE);
helpIcon.addClickListener(event -> onHelpIconClick());
helpIcon.setId(HELP_ICON_ID);
this.rules = new DrawerToggle();
@ -77,20 +76,20 @@ public class UpperBar extends HorizontalLayout implements LocaleChangeObserver {
/**
* Starts the type inference algorithm by passing the required arguments to the MainViewListener.
*
* @param lambdaString the lambda term to be type-inferred
* @param termAndAssumptions the lambda term to be type-inferred and the type assumptions to use
*/
protected void typeInfer(final String lambdaString) {
setTermInURL.accept(lambdaString);
presenter.typeInferLambdaString(lambdaString, new HashMap<>());
protected void typeInfer(Pair<String, Map<String, String>> termAndAssumptions) {
setTermInURL.accept(termAndAssumptions.getLeft()); // TODO: include types?
presenter.typeInferLambdaString(termAndAssumptions.getLeft(), termAndAssumptions.getRight());
}
/**
* Calls the inferTerm method in {@link edu.kit.typicalc.view.main.InputBar} with the provided
* string as the argument.
*
*
* @param term the provided string
*/
protected void inferTerm(final String term) {
protected void inferTerm(String term) {
inputBar.inferTerm(term);
}
@ -106,6 +105,6 @@ public class UpperBar extends HorizontalLayout implements LocaleChangeObserver {
@Override
public void localeChange(LocaleChangeEvent event) {
rules.setText(getTranslation("root.inferenceRules"));
rules.setText(getTranslation("root.inferenceRules"));
}
}

1
src/main/resources/application.properties
View File

@ -1,5 +1,6 @@
server.port=${PORT:8080}
logging.level.org.atmosphere = warn
spring.mustache.check-template-location = false
spring.devtools.add-properties = false
# vaadin.whitelisted-packages= org/vaadin/example

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

@ -1,3 +1,4 @@
root.domain=http://localhost:8080/
root.lambda=\u03BB
root.home=home
root.typicalc=Typicalc

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

@ -3,7 +3,7 @@ root.copyLatex=Kopiere Latex-Code
root.selectExample=Beispiel auswählen:
root.typeInfer=Typisieren
root.operatingHelp=Bedienhilfen
root.inputSyntax=Eingabe Syntax
root.inputSyntax=Eingabe-Syntax
root.inferenceRules=Ableitungsregeln
root.overlongInput=Die maximale Länge der Eingabe beträgt 1000 Zeichen!
root.absRule=Abs-Regel