mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-08 18:30:42 +00:00
Fix code style issues
This commit is contained in:
parent
a7f1556fe6
commit
c78d6b9e0a
@ -25,7 +25,7 @@ public class Conclusion {
|
|||||||
* @param lambdaTerm the lambda term in the conclusion
|
* @param lambdaTerm the lambda term in the conclusion
|
||||||
* @param type the type assigned to 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.typeAssumptions = typeAssumptions;
|
||||||
this.lambdaTerm = lambdaTerm;
|
this.lambdaTerm = lambdaTerm;
|
||||||
this.type = type;
|
this.type = type;
|
||||||
|
@ -111,20 +111,21 @@ public class LambdaLexer {
|
|||||||
advance();
|
advance();
|
||||||
return new Result<>(t);
|
return new Result<>(t);
|
||||||
default:
|
default:
|
||||||
if (Character.isLetter(c)) {
|
// only allow ascii characters in variable names
|
||||||
|
if (Character.isLetter(c) && (int) c < 128) {
|
||||||
int startPos = pos;
|
int startPos = pos;
|
||||||
// identifier
|
// identifier
|
||||||
StringBuilder sb = new StringBuilder();
|
StringBuilder sb = new StringBuilder();
|
||||||
do {
|
do {
|
||||||
sb.append(term.charAt(pos));
|
sb.append(term.charAt(pos));
|
||||||
advance();
|
advance();
|
||||||
} while (pos < term.length() && Character.isLetterOrDigit(term.charAt(pos)));
|
} while (pos < term.length() && Character.isLetterOrDigit(term.charAt(pos))
|
||||||
String s = sb.toString();
|
&& (int) term.charAt(pos) < 128);
|
||||||
TokenType type;
|
if (pos < term.length() && (int) term.charAt(pos) >= 128) {
|
||||||
// only allow ascii characters in variable names
|
|
||||||
if (!s.matches("\\A\\p{ASCII}*\\z")) {
|
|
||||||
return new Result<>(null, ParseError.UNEXPECTED_CHARACTER);
|
return new Result<>(null, ParseError.UNEXPECTED_CHARACTER);
|
||||||
}
|
}
|
||||||
|
String s = sb.toString();
|
||||||
|
TokenType type;
|
||||||
switch (s) {
|
switch (s) {
|
||||||
case "let":
|
case "let":
|
||||||
type = TokenType.LET;
|
type = TokenType.LET;
|
||||||
|
@ -40,7 +40,6 @@ public class TypeAssumptionParser {
|
|||||||
}
|
}
|
||||||
|
|
||||||
private Result<Pair<Type, Integer>, ParseError> parseType(LambdaLexer lexer, int parenCount) {
|
private Result<Pair<Type, Integer>, ParseError> parseType(LambdaLexer lexer, int parenCount) {
|
||||||
// TODO: remove misc. logging
|
|
||||||
Result<Token, ParseError> token = lexer.nextToken();
|
Result<Token, ParseError> token = lexer.nextToken();
|
||||||
if (token.isError()) {
|
if (token.isError()) {
|
||||||
return new Result<>(token);
|
return new Result<>(token);
|
||||||
|
@ -2,6 +2,10 @@ package edu.kit.typicalc.model.step;
|
|||||||
|
|
||||||
import edu.kit.typicalc.model.Conclusion;
|
import edu.kit.typicalc.model.Conclusion;
|
||||||
import edu.kit.typicalc.model.Constraint;
|
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
|
* 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.
|
* Initializes a new empty step.
|
||||||
*/
|
*/
|
||||||
public EmptyStep() {
|
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
|
@Override
|
||||||
|
@ -11,6 +11,8 @@ import java.util.Optional;
|
|||||||
|
|
||||||
/**
|
/**
|
||||||
* Utility class to avoid unification logic duplication in type methods.
|
* Utility class to avoid unification logic duplication in type methods.
|
||||||
|
*
|
||||||
|
* @see Type
|
||||||
*/
|
*/
|
||||||
final class UnificationUtil {
|
final class UnificationUtil {
|
||||||
private UnificationUtil() { }
|
private UnificationUtil() { }
|
||||||
|
@ -3,13 +3,12 @@ package edu.kit.typicalc.view;
|
|||||||
/**
|
/**
|
||||||
* Represents an HTML element that uses MathJax and custom JavaScript classes to render its contents.
|
* 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
|
* 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 {
|
public interface MathjaxAdapter {
|
||||||
|
|
||||||
int getStepCount();
|
int getStepCount();
|
||||||
|
|
||||||
void showStep(int n);
|
void showStep(int n);
|
||||||
|
// TODO: document removal of scaling method
|
||||||
void scale(double newScaling);
|
|
||||||
}
|
}
|
||||||
|
@ -23,6 +23,7 @@ public class ControlPanel extends HorizontalLayout {
|
|||||||
* Sets up buttons with click-listeners that call the corresponding method in the view.
|
* 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 view the view that reacts to the button clicks
|
||||||
|
* @param focusArea the component key shortcuts should work in
|
||||||
*/
|
*/
|
||||||
public ControlPanel(ControlPanelView view, Component focusArea) {
|
public ControlPanel(ControlPanelView view, Component focusArea) {
|
||||||
firstStep = new Button(new Icon(VaadinIcon.ANGLE_DOUBLE_LEFT), evt -> view.firstStepButton());
|
firstStep = new Button(new Icon(VaadinIcon.ANGLE_DOUBLE_LEFT), evt -> view.firstStepButton());
|
||||||
|
@ -50,10 +50,5 @@ public class MathjaxProofTree extends LitTemplate implements MathjaxAdapter {
|
|||||||
public void showStep(int n) {
|
public void showStep(int n) {
|
||||||
getElement().callJsFunction("showStep", n);
|
getElement().callJsFunction("showStep", n);
|
||||||
}
|
}
|
||||||
|
|
||||||
@Override
|
|
||||||
public void scale(double newScaling) {
|
|
||||||
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -46,10 +46,5 @@ public class MathjaxUnification extends LitTemplate implements MathjaxAdapter {
|
|||||||
}
|
}
|
||||||
getElement().callJsFunction("showStep", n);
|
getElement().callJsFunction("showStep", n);
|
||||||
}
|
}
|
||||||
|
|
||||||
@Override
|
|
||||||
public void scale(double newScaling) {
|
|
||||||
// todo implement
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -14,7 +14,6 @@ import com.vaadin.flow.i18n.LocaleChangeObserver;
|
|||||||
*/
|
*/
|
||||||
public class ShareDialog extends Dialog implements LocaleChangeObserver {
|
public class ShareDialog extends Dialog implements LocaleChangeObserver {
|
||||||
|
|
||||||
private final VerticalLayout layout;
|
|
||||||
private final TextField urlField;
|
private final TextField urlField;
|
||||||
private final TextField packageField;
|
private final TextField packageField;
|
||||||
private final TextArea latexArea;
|
private final TextArea latexArea;
|
||||||
@ -29,7 +28,7 @@ public class ShareDialog extends Dialog implements LocaleChangeObserver {
|
|||||||
*/
|
*/
|
||||||
public ShareDialog(String url, String latexPackages, String latexCode) {
|
public ShareDialog(String url, String latexPackages, String latexCode) {
|
||||||
setWidth(80, Unit.PERCENTAGE);
|
setWidth(80, Unit.PERCENTAGE);
|
||||||
layout = new VerticalLayout();
|
VerticalLayout layout = new VerticalLayout();
|
||||||
layout.setAlignItems(FlexComponent.Alignment.START);
|
layout.setAlignItems(FlexComponent.Alignment.START);
|
||||||
layout.setSizeFull();
|
layout.setSizeFull();
|
||||||
add(layout);
|
add(layout);
|
||||||
|
@ -31,21 +31,18 @@ public class TypeInferenceView extends VerticalLayout
|
|||||||
|
|
||||||
private MathjaxUnification unification;
|
private MathjaxUnification unification;
|
||||||
private MathjaxProofTree tree;
|
private MathjaxProofTree tree;
|
||||||
private final LatexCreator lc;
|
private final transient LatexCreator lc;
|
||||||
private final transient TypeInfererInterface typeInferer;
|
|
||||||
private final Div content;
|
private final Div content;
|
||||||
private final ControlPanel controlPanel;
|
private final ShareDialog shareDialog;
|
||||||
private ShareDialog shareDialog;
|
|
||||||
|
|
||||||
public TypeInferenceView(TypeInfererInterface typeInferer) {
|
public TypeInferenceView(TypeInfererInterface typeInferer) {
|
||||||
this.typeInferer = typeInferer;
|
|
||||||
setId(ID);
|
setId(ID);
|
||||||
setSizeFull();
|
setSizeFull();
|
||||||
addAttachListener(this);
|
addAttachListener(this);
|
||||||
lc = new LatexCreator(typeInferer);
|
lc = new LatexCreator(typeInferer);
|
||||||
content = new Div();
|
content = new Div();
|
||||||
content.setId(CONTENT_ID);
|
content.setId(CONTENT_ID);
|
||||||
controlPanel = new ControlPanel(this, this);
|
ControlPanel controlPanel = new ControlPanel(this, this);
|
||||||
Scroller scroller = new Scroller(content);
|
Scroller scroller = new Scroller(content);
|
||||||
scroller.setId(SCROLLER_ID);
|
scroller.setId(SCROLLER_ID);
|
||||||
scroller.setScrollDirection(Scroller.ScrollDirection.BOTH);
|
scroller.setScrollDirection(Scroller.ScrollDirection.BOTH);
|
||||||
|
@ -9,15 +9,15 @@ import com.vaadin.flow.component.orderedlayout.VerticalLayout;
|
|||||||
|
|
||||||
public class ErrorNotification extends Notification {
|
public class ErrorNotification extends Notification {
|
||||||
|
|
||||||
private static final long serialVersionUID = 1L;
|
private static final long serialVersionUID = 239587L;
|
||||||
|
|
||||||
private static final String NOTIFICATION_ID = "errorNotification";
|
private static final String NOTIFICATION_ID = "errorNotification";
|
||||||
|
|
||||||
protected ErrorNotification(final String errorMessage) {
|
protected ErrorNotification(final String errorMessage) {
|
||||||
final VerticalLayout container = new VerticalLayout();
|
final VerticalLayout container = new VerticalLayout();
|
||||||
final Span errorSpan = new Span(errorMessage);
|
final Span errorSpan = new Span(errorMessage);
|
||||||
final Button closeButton = new Button(getTranslation("root.close"), event -> this.close());
|
final Button closeButton = new Button(getTranslation("root.close"), event -> this.close());
|
||||||
|
|
||||||
container.add(errorSpan, closeButton);
|
container.add(errorSpan, closeButton);
|
||||||
container.setAlignItems(FlexComponent.Alignment.CENTER);
|
container.setAlignItems(FlexComponent.Alignment.CENTER);
|
||||||
addThemeVariants(NotificationVariant.LUMO_ERROR);
|
addThemeVariants(NotificationVariant.LUMO_ERROR);
|
||||||
|
@ -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
|
* 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.
|
* clipboard. Each InferenceRuleField is displayed in drawer area of the web page.
|
||||||
*/
|
*/
|
||||||
@CssImport("./styles/view/main/inference-rule-field.css")
|
@CssImport("./styles/view/main/inference-rule-field.css")
|
||||||
@JsModule("./src/copy-to-clipboard.js")
|
@JsModule("./src/copy-to-clipboard.js")
|
||||||
public class InferenceRuleField extends VerticalLayout implements LocaleChangeObserver {
|
public class InferenceRuleField extends VerticalLayout implements LocaleChangeObserver {
|
||||||
|
|
||||||
private static final long serialVersionUID = -8551851183297707985L;
|
private static final long serialVersionUID = -8551851183297707985L;
|
||||||
|
|
||||||
/*
|
/*
|
||||||
* IDs for the imported .css-file
|
* 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 HEADER_ID = "headerField";
|
||||||
private static final String MAIN_ID = "main";
|
private static final String MAIN_ID = "main";
|
||||||
private static final String RULE_NAME_ID = "ruleName";
|
private static final String RULE_NAME_ID = "ruleName";
|
||||||
|
|
||||||
private final String nameKey;
|
private final String nameKey;
|
||||||
private final Button copyButton;
|
private final Button copyButton;
|
||||||
private final H4 ruleName;
|
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
|
* Initializes an InferenceRuleField with a key to get the name of the inference rule and the LaTeX-code
|
||||||
* for its visual representation.
|
* for its visual representation.
|
||||||
*
|
*
|
||||||
* @param latex the LaTeX-code
|
* @param latex the LaTeX-code
|
||||||
* @param nameKey the key to get the name of the inference rule
|
* @param nameKey the key to get the name of the inference rule
|
||||||
*/
|
*/
|
||||||
protected InferenceRuleField(final String latex, final String nameKey) {
|
protected InferenceRuleField(final String latex, final String nameKey) {
|
||||||
this.nameKey = nameKey;
|
this.nameKey = nameKey;
|
||||||
|
|
||||||
final HorizontalLayout header = new HorizontalLayout();
|
final HorizontalLayout header = new HorizontalLayout();
|
||||||
header.setId(HEADER_ID);
|
header.setId(HEADER_ID);
|
||||||
this.ruleName = new H4(getTranslation(nameKey));
|
this.ruleName = new H4(getTranslation(nameKey));
|
||||||
ruleName.setId(RULE_NAME_ID);
|
ruleName.setId(RULE_NAME_ID);
|
||||||
header.add(ruleName);
|
header.add(ruleName);
|
||||||
|
|
||||||
final VerticalLayout main = new VerticalLayout();
|
final VerticalLayout main = new VerticalLayout();
|
||||||
main.setId(MAIN_ID);
|
main.setId(MAIN_ID);
|
||||||
this.copyButton = new Button(getTranslation("root.copyLatex"), new Icon(VaadinIcon.CLIPBOARD));
|
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));
|
copyButton.addClickListener(event -> UI.getCurrent().getPage().executeJs("window.copyToClipboard($0)", latex));
|
||||||
main.add(rule, copyButton);
|
main.add(rule, copyButton);
|
||||||
add(header, main);
|
add(header, main);
|
||||||
|
@ -9,13 +9,12 @@ import com.vaadin.flow.i18n.LocaleChangeEvent;
|
|||||||
import com.vaadin.flow.i18n.LocaleChangeObserver;
|
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")
|
@CssImport("./styles/view/main/info-dialog.css")
|
||||||
public class InfoDialog extends Dialog implements LocaleChangeObserver {
|
public class InfoDialog extends Dialog implements LocaleChangeObserver {
|
||||||
|
|
||||||
private static final long serialVersionUID = 2914411566361539614L;
|
private static final long serialVersionUID = 2914411566361539614L;
|
||||||
|
|
||||||
/*
|
/*
|
||||||
* IDs for the imported .css-file
|
* IDs for the imported .css-file
|
||||||
*/
|
*/
|
||||||
@ -23,7 +22,7 @@ public class InfoDialog extends Dialog implements LocaleChangeObserver {
|
|||||||
private static final String INFO_CONTENT_ID = "infoContent";
|
private static final String INFO_CONTENT_ID = "infoContent";
|
||||||
|
|
||||||
private final H4 heading;
|
private final H4 heading;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Creates new InfoDialog.
|
* Creates new InfoDialog.
|
||||||
*/
|
*/
|
||||||
@ -31,7 +30,7 @@ public class InfoDialog extends Dialog implements LocaleChangeObserver {
|
|||||||
heading = new H4(getTranslation("root.inputSyntax"));
|
heading = new H4(getTranslation("root.inputSyntax"));
|
||||||
HorizontalLayout infoHeader = new HorizontalLayout(heading);
|
HorizontalLayout infoHeader = new HorizontalLayout(heading);
|
||||||
infoHeader.setId(INFO_HEADER_ID);
|
infoHeader.setId(INFO_HEADER_ID);
|
||||||
|
|
||||||
//TODO fill with content
|
//TODO fill with content
|
||||||
VerticalLayout infoContent = new VerticalLayout();
|
VerticalLayout infoContent = new VerticalLayout();
|
||||||
infoContent.setId(INFO_CONTENT_ID);
|
infoContent.setId(INFO_CONTENT_ID);
|
||||||
|
@ -35,9 +35,6 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
|
|||||||
|
|
||||||
private static final short MAX_INPUT_LENGTH = 1000;
|
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 TextField inputField;
|
||||||
private final Button inferTypeButton;
|
private final Button inferTypeButton;
|
||||||
|
|
||||||
@ -48,7 +45,7 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
|
|||||||
* @param callback Consumer to call the inferType()-method in UpperBar
|
* @param callback Consumer to call the inferType()-method in UpperBar
|
||||||
*/
|
*/
|
||||||
protected InputBar(final Consumer<String> callback) {
|
protected InputBar(final Consumer<String> callback) {
|
||||||
infoIcon = new Icon(VaadinIcon.INFO_CIRCLE);
|
Icon infoIcon = new Icon(VaadinIcon.INFO_CIRCLE);
|
||||||
infoIcon.addClickListener(event -> onInfoIconClick());
|
infoIcon.addClickListener(event -> onInfoIconClick());
|
||||||
|
|
||||||
inputField = new TextField();
|
inputField = new TextField();
|
||||||
@ -56,8 +53,8 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
|
|||||||
inputField.setClearButtonVisible(true);
|
inputField.setClearButtonVisible(true);
|
||||||
inputField.setValueChangeMode(ValueChangeMode.EAGER);
|
inputField.setValueChangeMode(ValueChangeMode.EAGER);
|
||||||
inputField.addValueChangeListener(event -> onInputFieldValueChange());
|
inputField.addValueChangeListener(event -> onInputFieldValueChange());
|
||||||
lambdaButton = new Button(getTranslation("root.lambda"), event -> onLambdaButtonClick());
|
Button lambdaButton = new Button(getTranslation("root.lambda"), event -> onLambdaButtonClick());
|
||||||
exampleButton = new Button(getTranslation("root.examplebutton"), event -> onExampleButtonClick());
|
Button exampleButton = new Button(getTranslation("root.examplebutton"), event -> onExampleButtonClick());
|
||||||
exampleButton.setId(EXAMPLE_BUTTON_ID);
|
exampleButton.setId(EXAMPLE_BUTTON_ID);
|
||||||
inferTypeButton = new Button(getTranslation("root.typeInfer"), event -> onTypeInferButtonClick(callback));
|
inferTypeButton = new Button(getTranslation("root.typeInfer"), event -> onTypeInferButtonClick(callback));
|
||||||
inferTypeButton.addClickShortcut(Key.ENTER).listenOn(this);
|
inferTypeButton.addClickShortcut(Key.ENTER).listenOn(this);
|
||||||
@ -67,10 +64,10 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
|
|||||||
add(infoIcon, exampleButton, lambdaButton, inputField, inferTypeButton);
|
add(infoIcon, exampleButton, lambdaButton, inputField, inferTypeButton);
|
||||||
setId(INPUT_BAR_ID);
|
setId(INPUT_BAR_ID);
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Sets the provided string as the value of the inputField and starts the type inference algorithm.
|
* Sets the provided string as the value of the inputField and starts the type inference algorithm.
|
||||||
*
|
*
|
||||||
* @param term the provided string
|
* @param term the provided string
|
||||||
*/
|
*/
|
||||||
protected void inferTerm(final String term) {
|
protected void inferTerm(final String term) {
|
||||||
|
@ -36,10 +36,5 @@ public class MathjaxDisplay extends LitTemplate implements MathjaxAdapter {
|
|||||||
public void showStep(int n) {
|
public void showStep(int n) {
|
||||||
// do nothing
|
// do nothing
|
||||||
}
|
}
|
||||||
|
|
||||||
@Override
|
|
||||||
public void scale(double newScaling) {
|
|
||||||
// todo implement
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user