arnekeller/Typicalc
1
0
Fork 0
mirror of https://gitlab.kit.edu/uskyk/typicalc.git synced 2024-11-08 18:30:42 +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:
Johanna Stuber 2021-02-15 16:10:44 +01:00
commit 13c746a0b1
29 changed files with 411 additions and 127 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
.gitlab-ci.yml
View File

@ -1,5 +1,6 @@
build:
script:
- file src/main/resources/language/translation_de.properties | rg UTF-8
- mvn -Dmaven.repo.local=/tmp/m2/repository -Duser.home=/tmp checkstyle:check jacoco:prepare-agent test jacoco:report
- python3 /opt/cover2cover.py target/site/jacoco/jacoco.xml src/main/java > target/site/cobertura.xml
- python3 /opt/source2filename.py target/site/cobertura.xml

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

@ -4,7 +4,7 @@ SVGElement.prototype.getTransformToElement = SVGElement.prototype.getTransformTo
return elem.getScreenCTM().inverse().multiply(this.getScreenCTM());
};
window.MathJax = {
loader: {load: ['output/svg', '[tex]/ams', '[tex]/bussproofs', '[tex]/colorv2', '[tex]/textmacros', '[tex]/unicode']},
loader: {load: ['output/svg', '[tex]/ams', '[tex]/bussproofs', '[tex]/color', '[tex]/textmacros', '[tex]/unicode']},
tex: {
packages: {'[+]': ['ams', 'bussproofs', 'color', 'textmacros', 'unicode']},
inlineMath: [['$', '$'], ['\\(', '\\)']]
@ -145,6 +145,6 @@ mjx-container {\
}
};
// disable MathJax context menu
// window.addEventListener("contextmenu", function (event) {
// event.stopPropagation();
// }, true);
window.addEventListener("contextmenu", function (event) {
event.stopPropagation();
}, true);

3
frontend/styles/view/error-notification.css Normal file
View File

@ -0,0 +1,3 @@
#errorNotificationContent {
align-items: center;
}

16
frontend/styles/view/main/help-dialog.css
View File

@ -1,9 +1,12 @@
#contentLayout {
height: 80vh;
width: 1000px !important;
padding-left: 0;
padding-right: 0;
height: 500px;
}
#headingLayout {
width: 80vw;
width: 100%;
display: flex;
position: relative;
align-items: center;
@ -13,4 +16,13 @@
#languageSelect {
position: absolute;
right: 0;
}
#accordion {
width: 100%;
}
.help-field {
justify-content: center;
align-items: center;
}

3
frontend/styles/view/main/input-bar.css
View File

@ -11,6 +11,3 @@
padding: 1em;
}
vaadin-drawer-toggle {
width: 10em;
}

15
frontend/styles/view/main/main-view.css
View File

@ -1,7 +1,16 @@
#header {
height: var(--lumo-size-xl);
height: var(--lumo-size-xl);
}
#header h1 {
font-size: var(--lumo-font-size-l);
margin: 0;
font-size: var(--lumo-font-size-l);
margin: 0;
}
#start-page {
width: 100%;
height: 100%;
align-items: center;
}
#start-page-scroller {
width: 100%;
height: 100%;
}

3
frontend/styles/view/not-found.css Normal file
View File

@ -0,0 +1,3 @@
#not-found {
align-items: center;
}

11
frontend/styles/view/share-dialog.css Normal file
View File

@ -0,0 +1,11 @@
#share-dialog {
width: 80%;
}
#share-dialog-layout {
align-items: start;
width: 100%;
height: 100%;
}
.share-dialog-field {
width: 100%;
}

13
frontend/styles/view/type-inference.css
View File

@ -1,3 +1,14 @@
#type-inference-view {
width: 100%;
height: 100%;
padding: 0 0 1em;
align-items: center;
}
#type-inference-view::before {
margin: 0 !important;
}
#scroller {
width: 100%;
height: 100%;
@ -7,6 +18,8 @@
display: flex;
flex-direction: column;
height: 100%;
padding: 10px;
box-sizing: border-box;
}
tc-proof-tree {

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

@ -56,9 +56,8 @@ public class TypeAssumptionParser { // TODO: document type syntax? or refer to o
return type2;
}
type = type2.unwrap().getLeft();
parenCount -= type2.unwrap().getRight() - 1;
removedParens += type2.unwrap().getRight() - 1;
if (parenCount < 0) {
if (parenCount - removedParens < 0) {
return new Result<>(new ImmutablePair<>(type, removedParens));
}
break;
@ -81,9 +80,8 @@ public class TypeAssumptionParser { // TODO: document type syntax? or refer to o
}
t = token.unwrap();
if (t.getType() == TokenType.RIGHT_PARENTHESIS) {
parenCount -= 1;
removedParens += 1;
if (parenCount <= 0) {
if (parenCount - removedParens <= 0) {
return new Result<>(new ImmutablePair<>(type, removedParens));
}
continue;
@ -100,8 +98,7 @@ public class TypeAssumptionParser { // TODO: document type syntax? or refer to o
}
type = new FunctionType(type, nextType.unwrap().getLeft());
removedParens += nextType.unwrap().getRight();
parenCount -= nextType.unwrap().getRight();
if (parenCount <= 0) {
if (parenCount - removedParens <= 0) {
return new Result<>(new ImmutablePair<>(type, removedParens));
}
}

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

@ -10,5 +10,4 @@ public interface MathjaxAdapter {
int getStepCount();
void showStep(int n);
// TODO: document removal of scaling method
}

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

@ -17,6 +17,9 @@ import edu.kit.typicalc.view.main.MainViewImpl;
@JsModule("./src/mathjax-setup.js")
public class StartPageView extends VerticalLayout implements ControlPanelView {
private static final String ID = "start-page";
private static final String SCROLLER_ID = "start-page-scroller";
private final Div content;
private final ControlPanel controlPanel;
MathjaxProofTree tree;
@ -24,14 +27,12 @@ public class StartPageView extends VerticalLayout implements ControlPanelView {
public StartPageView() {
// todo implement correctly
setId("start-page");
setSizeFull();
setId(ID);
content = new Div();
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);
disableControlPanel();
createContent();

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

@ -1,8 +1,7 @@
package edu.kit.typicalc.view.content.typeinferencecontent;
import com.vaadin.flow.component.Unit;
import com.vaadin.flow.component.dependency.CssImport;
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;
@ -12,8 +11,13 @@ import com.vaadin.flow.i18n.LocaleChangeObserver;
/**
* Contains GUI elements to extract the URL and LaTeX code of the currently shown proof tree.
*/
@CssImport("./styles/view/share-dialog.css")
public class ShareDialog extends Dialog implements LocaleChangeObserver {
private static final String ID = "share-dialog";
private static final String LAYOUT_ID = "share-dialog-layout";
private static final String FIELD_CLASS = "share-dialog-field";
private final TextField urlField;
private final TextField packageField;
private final TextArea latexArea;
@ -27,10 +31,9 @@ public class ShareDialog extends Dialog implements LocaleChangeObserver {
* @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);
setId(ID);
VerticalLayout layout = new VerticalLayout();
layout.setAlignItems(FlexComponent.Alignment.START);
layout.setSizeFull();
layout.setId(LAYOUT_ID);
add(layout);
urlField = new TextField(getTranslation("share.url.label"));
@ -38,12 +41,11 @@ public class ShareDialog extends Dialog implements LocaleChangeObserver {
latexArea = new TextArea(getTranslation("share.latex.label"));
urlField.setValue(url);
urlField.setClassName(FIELD_CLASS);
packageField.setValue(latexPackages);
packageField.setClassName(FIELD_CLASS);
latexArea.setValue(latexCode);
urlField.setWidthFull();
packageField.setWidthFull();
latexArea.setWidthFull();
latexArea.setClassName(FIELD_CLASS);
layout.add(urlField, packageField, latexArea);
}

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

@ -14,6 +14,7 @@ import edu.kit.typicalc.view.content.ControlPanelView;
import edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreator;
import java.util.List;
import java.util.Locale;
@PageTitle("TypeInferenceView")
@CssImport("./styles/view/type-inference.css")
@ -39,16 +40,17 @@ public class TypeInferenceView extends VerticalLayout
public TypeInferenceView(TypeInfererInterface typeInferer) {
setId(ID);
setSizeFull();
addAttachListener(this);
lc = new LatexCreator(typeInferer);
// TODO: document new translation function
// TODO: is Function<UnificationError, String> too limiting?
lc = new LatexCreator(typeInferer,
error -> getTranslation("root." + error.toString().toLowerCase(Locale.ENGLISH)));
content = new Div();
content.setId(CONTENT_ID);
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);
treeNumbers = lc.getTreeNumbers();
setContent();

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

@ -2,12 +2,14 @@ package edu.kit.typicalc.view.content.typeinferencecontent.latexcreator;
import edu.kit.typicalc.model.Conclusion;
import edu.kit.typicalc.model.TypeInfererInterface;
import edu.kit.typicalc.model.UnificationError;
import edu.kit.typicalc.model.step.*;
import edu.kit.typicalc.model.term.VarTerm;
import edu.kit.typicalc.model.type.TypeAbstraction;
import java.util.List;
import java.util.Map;
import java.util.function.Function;
import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.*;
@ -28,22 +30,25 @@ public class LatexCreator implements StepVisitor {
* Generate the pieces of LaTeX-code from the type inferer.
*
* @param typeInferer theTypeInfererInterface to create the LaTeX-code from
* @param translationProvider translation text provider for {@link UnificationError}
*/
public LatexCreator(TypeInfererInterface typeInferer) {
this(typeInferer, true);
public LatexCreator(TypeInfererInterface typeInferer, Function<UnificationError, String> translationProvider) {
this(typeInferer, true, translationProvider);
}
/**
* Generate the pieces of LaTeX-code from the type inferer.
*
* @param typeInferer theTypeInfererInterface to create the LaTeX-code from
* @param stepLabels turns step labels on (true) or off (false)
* @param typeInferer theTypeInfererInterface to create the LaTeX code from
* @param stepLabels turns step labels on or off
* @param translationProvider translation text provider for {@link UnificationError}
*/
public LatexCreator(TypeInfererInterface typeInferer, boolean stepLabels) {
public LatexCreator(TypeInfererInterface typeInferer, boolean stepLabels,
Function<UnificationError, String> translationProvider) {
this.tree = new StringBuilder();
this.stepLabels = stepLabels;
typeInferer.getFirstInferenceStep().accept(this);
this.constraintsCreator = new LatexCreatorConstraints(typeInferer);
this.constraintsCreator = new LatexCreatorConstraints(typeInferer, translationProvider);
}
/**

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

@ -1,7 +1,9 @@
package edu.kit.typicalc.view.content.typeinferencecontent.latexcreator;
/**
* Provides a list of constants needed for the creation of the LaTeX code.
* Provides a number of constants needed for the creation of LaTeX code in
* {@link LatexCreator}, {@link LatexCreatorConstraints}, {@link LatexCreatorTerm} and
* {@link LatexCreatorType}.
*/
public final class LatexCreatorConstants {
private LatexCreatorConstants() {
@ -47,7 +49,6 @@ public final class LatexCreatorConstants {
protected static final String LATEX_NEW_LINE = "\\\\";
protected static final String CIRC = "\\circ";
protected static final String PHANTOM_X = "\\phantom{x}";
protected static final String SUBSTITUTION_SIGN = "\\mathrel{\\unicode{x21E8}}";
protected static final String COLOR_RED = "\\color{#f00}";
protected static final String LAMBDA = "\\lambda";

24
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstraints.java
View File

@ -7,6 +7,7 @@ import edu.kit.typicalc.util.Result;
import java.util.ArrayList;
import java.util.List;
import java.util.Optional;
import java.util.function.Function;
import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.*;
@ -25,27 +26,34 @@ public class LatexCreatorConstraints implements StepVisitor {
private final String constraintSetIndex;
private final String prefix;
private String prevStep;
private final Function<UnificationError, String> translationProvider;
/**
* Initializes the LatexCreatorConstraints with the right values calculates the strings
* that will be returned in getEverything().
*
* @param typeInferer the source for the generation of the LaTeX code
* @param translationProvider translation text provider for {@link UnificationError}
*/
protected LatexCreatorConstraints(TypeInfererInterface typeInferer) {
this(typeInferer, new ConstraintSetIndexFactory(), new TreeNumberGenerator(), FIRST_PREFIX);
protected LatexCreatorConstraints(TypeInfererInterface typeInferer,
Function<UnificationError, String> translationProvider) {
this(typeInferer,
new ConstraintSetIndexFactory(), new TreeNumberGenerator(),
FIRST_PREFIX, translationProvider);
}
private LatexCreatorConstraints(TypeInfererInterface typeInferer,
ConstraintSetIndexFactory constraintSetIndexFactory,
TreeNumberGenerator numberGenerator,
String prefix) {
String prefix,
Function<UnificationError, String> translationProvider) {
this.prefix = prefix;
this.prevStep = "";
this.constraintSetIndexFactory = constraintSetIndexFactory;
this.numberGenerator = numberGenerator;
this.constraintSetIndex = constraintSetIndexFactory.nextConstraintSetIndex();
this.typeInferer = typeInferer;
this.translationProvider = translationProvider;
constraints = new ArrayList<>();
if (FIRST_PREFIX.equals(prefix)) {
constraints.add(AMPERSAND + CONSTRAINT_SET + EQUALS + LATEX_CURLY_LEFT + LATEX_CURLY_RIGHT);
@ -150,7 +158,8 @@ public class LatexCreatorConstraints implements StepVisitor {
addConstraint(letD);
LatexCreatorConstraints subCreator = new LatexCreatorConstraints(letD.getTypeInferer(),
constraintSetIndexFactory, numberGenerator,
constraints.get(constraints.size() - 1) + LATEX_NEW_LINE + NEW_LINE);
constraints.get(constraints.size() - 1) + LATEX_NEW_LINE + NEW_LINE,
translationProvider);
constraints.addAll(subCreator.getEverything());
// cancels constraint creation if sub inference failed
@ -218,8 +227,8 @@ public class LatexCreatorConstraints implements StepVisitor {
for (int i = unificationConstraints.size() - 1; i >= 0; i--) {
latex.append(AMPERSAND);
if (markError && i == 0) {
latex.append(COLOR_RED);
latex.append(CURLY_LEFT);
latex.append(COLOR_RED);
}
latex.append(new LatexCreatorType(unificationConstraints.get(i).getFirstType()).getLatex());
latex.append(EQUALS);
@ -233,8 +242,7 @@ public class LatexCreatorConstraints implements StepVisitor {
}
}
if (!unificationConstraints.isEmpty()) {
// todo somehow this gets colored red too when an error occurs
latex.append(PAREN_RIGHT + LATEX_CURLY_RIGHT + LATEX_NEW_LINE);
latex.append(LATEX_CURLY_RIGHT + PAREN_RIGHT + LATEX_NEW_LINE);
}
List<Substitution> substitutions = subs.unwrap();
@ -254,8 +262,8 @@ public class LatexCreatorConstraints implements StepVisitor {
latex.append(SPLIT_END);
if (error.isPresent()) {
latex.append(LATEX_NEW_LINE + AMPERSAND);
latex.append(translationProvider.apply(error.get()));
}
error.ifPresent(latex::append); // TODO: translation
steps.add(latex.toString());
}
return steps;

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

@ -1,33 +1,35 @@
package edu.kit.typicalc.view.main;
import com.vaadin.flow.component.button.Button;
import com.vaadin.flow.component.dependency.CssImport;
import com.vaadin.flow.component.html.Span;
import com.vaadin.flow.component.notification.Notification;
import com.vaadin.flow.component.notification.NotificationVariant;
import com.vaadin.flow.component.orderedlayout.FlexComponent;
import com.vaadin.flow.component.orderedlayout.VerticalLayout;
/**
* The notification being displayed on invalid input.
*/
@CssImport("./styles/view/error-notification.css")
public class ErrorNotification extends Notification {
private static final long serialVersionUID = 239587L;
private static final String NOTIFICATION_ID = "errorNotification";
private static final String NOTIFICATION_CONTENT_ID = "errorNotificationContent";
/**
* Creates a new ErrorNotification with a specific error message.
*
*
* @param errorMessage the error message
*/
protected ErrorNotification(String errorMessage) {
VerticalLayout container = new VerticalLayout();
container.setId(NOTIFICATION_CONTENT_ID);
Span errorSpan = new Span(errorMessage);
Button closeButton = new Button(getTranslation("root.close"), event -> this.close());
container.add(errorSpan, closeButton);
container.setAlignItems(FlexComponent.Alignment.CENTER);
addThemeVariants(NotificationVariant.LUMO_ERROR);
add(container);
setPosition(Position.MIDDLE);

42
src/main/java/edu/kit/typicalc/view/main/HelpContentField.java Normal file
View File

@ -0,0 +1,42 @@
package edu.kit.typicalc.view.main;
import com.vaadin.flow.component.accordion.AccordionPanel;
import com.vaadin.flow.component.button.Button;
import com.vaadin.flow.component.details.DetailsVariant;
import com.vaadin.flow.component.html.Paragraph;
import com.vaadin.flow.component.orderedlayout.HorizontalLayout;
import com.vaadin.flow.i18n.LocaleChangeEvent;
import com.vaadin.flow.i18n.LocaleChangeObserver;
public class HelpContentField extends AccordionPanel implements LocaleChangeObserver {
private static final String CLASSNAME = "help-field";
private static final long serialVersionUID = -2793005857762897734L;
private final String summaryKey;
private final String contentKey;
private final Paragraph content;
protected HelpContentField(String summaryKey, String contentKey) {
this.summaryKey = summaryKey;
this.contentKey = contentKey;
this.content = new Paragraph(getTranslation(contentKey));
setSummaryText(getTranslation(summaryKey));
setContent(content);
addThemeVariants(DetailsVariant.FILLED);
}
protected HelpContentField(String summaryKey, Button button, String contentKey) {
this(summaryKey, contentKey);
HorizontalLayout layout = new HorizontalLayout(button, content);
layout.setClassName(CLASSNAME);
setContent(layout);
}
@Override
public void localeChange(LocaleChangeEvent event) {
setSummaryText(getTranslation(summaryKey));
content.setText(getTranslation(contentKey));
}
}

35
src/main/java/edu/kit/typicalc/view/main/HelpDialog.java
View File

@ -2,10 +2,14 @@ package edu.kit.typicalc.view.main;
import com.vaadin.flow.component.ItemLabelGenerator;
import com.vaadin.flow.component.UI;
import com.vaadin.flow.component.accordion.Accordion;
import com.vaadin.flow.component.applayout.DrawerToggle;
import com.vaadin.flow.component.button.Button;
import com.vaadin.flow.component.dependency.CssImport;
import com.vaadin.flow.component.dialog.Dialog;
import com.vaadin.flow.component.html.H3;
import com.vaadin.flow.component.html.H5;
import com.vaadin.flow.component.icon.Icon;
import com.vaadin.flow.component.icon.VaadinIcon;
import com.vaadin.flow.component.orderedlayout.HorizontalLayout;
import com.vaadin.flow.component.orderedlayout.VerticalLayout;
import com.vaadin.flow.component.select.Select;
@ -27,9 +31,9 @@ public class HelpDialog extends Dialog implements LocaleChangeObserver {
private static final String HEADING_LAYOUT_ID = "headingLayout";
private static final String CONTENT_LAYOUT_ID = "contentLayout";
private static final String LANGUAGE_SELECT_ID = "languageSelect";
private static final String ACCORDION_ID = "accordion";
private final H3 heading;
private final H5 inputSyntax;
private final Select<Locale> languageSelect;
private final ItemLabelGenerator<Locale> renderer;
@ -49,17 +53,36 @@ public class HelpDialog extends Dialog implements LocaleChangeObserver {
headingLayout.add(heading, languageSelect);
VerticalLayout contentLayout = new VerticalLayout();
//TODO inputSyntax wird im inputDialog behandelt --> hier anderer Content
inputSyntax = new H5();
Accordion content = createHelpContent();
content.setId(ACCORDION_ID);
contentLayout.add(content);
contentLayout.setId(CONTENT_LAYOUT_ID);
contentLayout.add(inputSyntax);
add(headingLayout, contentLayout);
}
private Accordion createHelpContent() {
Accordion acc = new Accordion();
acc.add(new HelpContentField("root.drawer", new DrawerToggle(), "root.helpDrawer"));
acc.add(new HelpContentField("root.example",
new Button(getTranslation("root.examplebutton")), "root.helpExample"));
acc.add(new HelpContentField("root.inputField", "root.helpInputField"));
acc.add(new HelpContentField("root.typeAssumptions", "root.helpTypeAssumptions"));
acc.add(new HelpContentField("root.firstStepButton",
new Button(new Icon(VaadinIcon.ANGLE_DOUBLE_LEFT)), "root.helpFirstStepButton"));
acc.add(new HelpContentField("root.previousStepButton",
new Button(new Icon(VaadinIcon.ANGLE_LEFT)), "root.helpPreviousStepButton"));
acc.add(new HelpContentField("root.nextStepButton",
new Button(new Icon(VaadinIcon.ANGLE_RIGHT)), "root.helpNextStepButton"));
acc.add(new HelpContentField("root.lastStepButton",
new Button(new Icon(VaadinIcon.ANGLE_DOUBLE_RIGHT)), "root.helpLastStepButton"));
acc.add(new HelpContentField("root.shareButton",
new Button(new Icon(VaadinIcon.CONNECT)), "root.helpShareButton"));
return acc;
}
@Override
public void localeChange(LocaleChangeEvent event) {
heading.setText(getTranslation("root.operatingHelp"));
inputSyntax.setText(getTranslation("root.inputSyntax"));
languageSelect.setLabel(getTranslation("root.selectLanguage"));
languageSelect.setTextRenderer(renderer);
}

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

@ -1,5 +1,6 @@
package edu.kit.typicalc.view.main;
import com.vaadin.flow.component.dependency.CssImport;
import com.vaadin.flow.component.html.H1;
import com.vaadin.flow.component.html.H2;
import com.vaadin.flow.component.orderedlayout.VerticalLayout;
@ -11,7 +12,10 @@ import com.vaadin.flow.router.ParentLayout;
* This is the view used when an unknown URL is requested by the user.
*/
@ParentLayout(MainViewImpl.class)
@CssImport("./styles/view/not-found.css")
public class NotFoundView extends VerticalLayout implements LocaleChangeObserver {
private static final String ID = "not-found";
private final H1 error404;
private final H2 suggestion;
@ -19,10 +23,10 @@ public class NotFoundView extends VerticalLayout implements LocaleChangeObserver
* Initializes a new NotFoundView with an error message.
*/
public NotFoundView() {
setId(ID);
error404 = new H1();
suggestion = new H2();
add(error404, suggestion); // todo make beautiful
setAlignItems(Alignment.CENTER);
}
@Override

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

@ -62,6 +62,13 @@ public class TypeAssumptionField extends HorizontalLayout implements LocaleChang
setId(ASSUMPTIONS_FIELD_ID);
}
/**
* Focus the variable field of this element.
*/
protected void focus() {
variableInputField.focus();
}
/**
* Gets the variable of the type assumption.
*

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

@ -94,6 +94,7 @@ public class TypeAssumptionsArea extends Dialog implements LocaleChangeObserver
});
assumptionContainer.add(assumption);
fields.add(assumption);
assumption.focus();
}
private void onDeleteAllClick() {

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

@ -3,15 +3,12 @@ package edu.kit.typicalc.view.main;
import com.vaadin.flow.component.Component;
import com.vaadin.flow.component.UI;
import com.vaadin.flow.component.applayout.DrawerToggle;
import com.vaadin.flow.component.button.Button;
import com.vaadin.flow.component.dependency.CssImport;
import com.vaadin.flow.component.dialog.Dialog;
import com.vaadin.flow.component.html.H1;
import com.vaadin.flow.component.icon.Icon;
import com.vaadin.flow.component.icon.VaadinIcon;
import com.vaadin.flow.component.orderedlayout.HorizontalLayout;
import com.vaadin.flow.i18n.LocaleChangeEvent;
import com.vaadin.flow.i18n.LocaleChangeObserver;
import com.vaadin.flow.router.Location;
import edu.kit.typicalc.view.content.infocontent.StartPageView;
import edu.kit.typicalc.view.main.MainView.MainViewListener;
@ -26,7 +23,7 @@ import java.util.function.Consumer;
* 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 {
public class UpperBar extends HorizontalLayout {
private static final long serialVersionUID = -7344967027514015830L;
/*
@ -38,7 +35,6 @@ public class UpperBar extends HorizontalLayout implements LocaleChangeObserver {
private static final String UPPER_BAR_ID = "header";
private final InputBar inputBar;
private final Button rules;
private final transient MainViewListener presenter;
private final transient Consumer<Pair<String, Map<String, String>>> setTermInURL;
@ -64,9 +60,8 @@ public class UpperBar extends HorizontalLayout implements LocaleChangeObserver {
Icon helpIcon = new Icon(VaadinIcon.QUESTION_CIRCLE);
helpIcon.addClickListener(event -> onHelpIconClick());
helpIcon.setId(HELP_ICON_ID);
this.rules = new DrawerToggle();
add(rules, viewTitle, inputBar, helpIcon);
add(new DrawerToggle(), viewTitle, inputBar, helpIcon);
setId(UPPER_BAR_ID);
getThemeList().set("dark", true); //TODO remove magic string
setSpacing(false);
@ -103,9 +98,4 @@ public class UpperBar extends HorizontalLayout implements LocaleChangeObserver {
Dialog helpDialog = new HelpDialog();
helpDialog.open();
}
@Override
public void localeChange(LocaleChangeEvent event) {
rules.setText(getTranslation("root.inferenceRules"));
}
}

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

@ -23,6 +23,46 @@ root.addAssumption=Typannahme hinzufügen
root.deleteAll=Alle löschen
root.variable=Variable
root.type=Typ
root.drawer=Drawer
root.example=Beispiele
root.inputField=Eingabefeld
root.firstStepButton=Erster-Schritt Knopf
root.previousStepButton=Vorheriger-Schritt Knopf
root.nextStepButton=Nächster-Schritt Knopf
root.lastStepButton=Letzter-Schritt Knopf
root.shareButton=Teilen Knopf
root.helpDrawer=Durch Klicken des Knopfs öffnet sich der Drawer. \
Im Drawer ist eine Auflistung aller Typregeln zu finden. \
Außerdem kann durch Klicken des Kopieren-Knopfs der Latex-Code der Regel in die Zwischenablage kopiert werden.
root.helpExample=Durch Klicken des Knopfs öffnet sich der Beispiel-Dialog. \
Nach Anklicken wird der jeweilige Beispielterm in das Eingabefeld eingefügt. \
Der Term kann nun nach belieben angepasst oder direkt typisiert werden.
root.helpInputField=In das Eingabefeld können Lambda-Terme mit einer Länge von bis zu 1000 Zeichen eingegeben werden. \
Das \u03BB-Zeichen kann dabei entweder durch Klicken des \u03BB-Knopfs oder durch Eingabe eines Backslashs an der \
aktuellen Cursorposition eingefügt werden. Durch Klicken des Info-Symbols wird die korrekte Syntax eines Terms \
angezeigt.
root.helpTypeAssumptions=Durch Klicken des Typannahmen-Knopfs öffnet sich ein Dialog zur Eingabe von Typannahmen. \
Durch Klicken des Info-Symbols wird die korrekte Syntax des Typs einer Typannahme angezeigt. Sofern eine Variable in \
mehreren Typannahmen vorkommt, wird ausschließlich die oberste Typannahme, die diese Variable enthält, \
berücksichtigt.
root.helpFirstStepButton=Je nach Stand der Algorithmusausführung ändert sich die Funtion des Knopfs. \
Wenn aktuell der Baum aufgebaut wird, springt die Anzeige nach Klicken des Knopfs zurück zum ersten Schritt des \
Typherleitungsbaums. Wenn bereits die Unifikation druchgeführt wird, sprigt die Anzeige nach Klicken des Knopfs \
in den letzten Schritt des Baums. Der Knopf lässt sich außerdem durch die Tastenkombination "STRG + Linke Pfeiltaste" \
ansprechen.
root.helpPreviousStepButton=Durch Klicken des Vorheriger-Schritt Knopfs wird der vorherige Schritt des Algorithmus \
angezeigt. Der Knopf lässt sich außerdem auf der Tastatur durch die Taste "Linke Pfeiltaste" ansprechen.
root.helpNextStepButton=Durch Klicken des Nächster-Schritt Knopfs wird der nächste Schritt des Algorithmus angezeigt. \
Der Knopf lässt sich außerdem durch auf der Tastatur durch die Taste "Rechte Pfeiltaste" ansprechen.
root.helpLastStepButton=Je nach Stand der Algorithmusausführung ändert sich die Funtion des Knopfs. \
Wenn aktuell der Baum aufgebaut wird, springt die Anzeige nach Klicken des Knopfs vor zum letzten Schritt des \
Typherleitungsbaums. Wenn bereits die Unifikation druchgeführt wird, sprigt die Anzeige nach Klicken des Knopfs \
vor zur Anzeige des finalen Typs. Der Knopf lässt sich außerdem durch die Tastenkombination \
"STRG + Rechte Pfeiltaste" ansprechen.
root.helpShareButton=Durch Klicken des Teilen Knopfs öffnet sich ein Dialog, in dem der LaTeX-Code des finalen \
Typherleitungsbaums des eingegebenen Terms und die benötigen Pakete zum Einbinden des Latex-Codes angezeigt werden. \
Zusätzlich dazu enthält der Dialog einen Permalink zur aktuellen Seite, der sowohl den Term als auch die Typannahmen \
kodiert.
root.absLetLatex=\
\\begin{prooftree}\

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

@ -25,6 +25,41 @@ root.variable=Variable
root.type=Type
root.title404=404 - Not Found
root.message404="Try /infer/<term> or type your favourite term into the input field
root.drawer=Drawer
root.example=Examples
root.inputField=Input Field
root.firstStepButton=First Step Button
root.previousStepButton=Previous Step Button
root.nextStepButton=Next Step Button
root.lastStepButton=Last Step Button
root.shareButton=Share Button
root.helpDrawer=Clicking on the button opens up the drawer. The drawer contains a collection of all type inference \
rules. By clicking on the copy-button the LaTeX-code of the corresponding rule is copied to the clipboard.
root.helpExample=Clicking on the button opens up the example dialog. After clicking on an example the corresponding \
term is inserted into the input field. Now either the type inference algorithm can be started or the term can be \
modified.
root.helpInputField=The input field allows the user to enter lambda terms with a maximum length of 1000 characters. \
The \u03BB-sign can be inserted at the current cursor position by either clicking the \u03BB-button or entering a \
backslash. By clicking on the info-symbol the grammar defining the valid input synatx is shown.
root.helpTypeAssumptions=Clicking on the type-assumptions-button opens up a dialog to enter type assumptions. \
By clicking the info-symbol the grammar defining a valid type of a type assmuption is shown. If the same variable \
is contained in multiple type assumptions, only the uppermost type assumption containing the variable is used for \
the algorithm.
root.helpFirstStepButton=The function of the button depends on the current state of the algorithm execution. \
If the tree is currently built up, clicking on the button shows the first step of the inference tree. \
If the unification algorithm is already in progress, clicking on the button shows the last step of the inference \
tree. The key combination "CTRL + left arrow key" also executes a click on the button.
root.helpPreviousStepButton=By clicking the previous-step button the previous step of the algorithm is shown. \
The key combination "left arrow key" also executes a click on the button.
root.helpNextStepButton=By clicking the next-step button the next step of the algorithm is shown. \
The key combination "right arrow key" also executes a click on the button.
root.helpLastStepButton=The function of the button depends on the current state of the algorithm execution. \
If the tree is currently built up, clicking on the button shows the last step of the inference tree. \
If the unification algorithm is already in progress, clicking on the button shows the final type of the \
entered term. The key combination "CTRL + right arrow key" also executes a click on the button.
root.helpShareButton=Clicking the share button opens up a dialog containing the LaTeX-code of the final inference \
tree and the packages needed to execute the LaTeX-code. In addition a permalink to the current page is provided. \
This link encodes the current term as well as the current type assumptions.
root.absLetLatex=\
\\begin{prooftree}\

48
src/test/java/edu/kit/typicalc/model/ModelImplTest.java
View File

@ -1,10 +1,25 @@
package edu.kit.typicalc.model;
import edu.kit.typicalc.model.parser.ParseError;
import edu.kit.typicalc.model.step.AbsStepDefault;
import edu.kit.typicalc.model.step.VarStepDefault;
import edu.kit.typicalc.model.term.AbsTerm;
import edu.kit.typicalc.model.term.LambdaTerm;
import edu.kit.typicalc.model.term.VarTerm;
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.TypeAbstraction;
import edu.kit.typicalc.model.type.TypeVariable;
import edu.kit.typicalc.model.type.TypeVariableKind;
import edu.kit.typicalc.util.Result;
import org.junit.jupiter.api.Test;
import java.util.LinkedHashMap;
import java.util.List;
import java.util.Map;
import static org.junit.jupiter.api.Assertions.assertEquals;
import static org.junit.jupiter.api.Assertions.assertTrue;
class ModelImplTest {
@ -18,6 +33,37 @@ class ModelImplTest {
map2.put("a.x", "3.int");
assertTrue(model.getTypeInferer("test.x.x.test", map2).isError());
assertTrue(model.getTypeInferer("x", map2).isError());
assertTrue(model.getTypeInferer("x", map).isOk());
Result<TypeInfererInterface, ParseError> result = model.getTypeInferer("λy.x", map);
VarTerm y = new VarTerm("y");
VarTerm x = new VarTerm("x");
LambdaTerm term = new AbsTerm(y, x);
assertTrue(result.isOk());
TypeInfererInterface typeInference = result.unwrap();
assertTrue(typeInference.getType().isPresent());
TypeVariable a1 = new TypeVariable(TypeVariableKind.TREE, 1);
TypeVariable a2 = new TypeVariable(TypeVariableKind.TREE, 2);
TypeVariable a3 = new TypeVariable(TypeVariableKind.TREE, 3);
Type resultFunction = new FunctionType(a2, NamedType.INT);
assertEquals(
resultFunction,
typeInference.getType().get());
assertEquals(
List.of(new Substitution(a1, resultFunction), new Substitution(a3, NamedType.INT)),
typeInference.getMGU().get());
assertEquals(
new AbsStepDefault(
new VarStepDefault(
new TypeAbstraction(NamedType.INT), NamedType.INT,
new Conclusion(Map.of(
x, new TypeAbstraction(NamedType.INT),
y, new TypeAbstraction(a2)),
x, a3),
new Constraint(a3, NamedType.INT)
),
new Conclusion(Map.of(x, new TypeAbstraction(NamedType.INT)), term, a1),
new Constraint(a1, new FunctionType(a2, a3))
), typeInference.getFirstInferenceStep()
);
}
}

42
src/test/java/edu/kit/typicalc/model/parser/TypeAssumptionParserTest.java
View File

@ -5,6 +5,7 @@ import edu.kit.typicalc.model.type.*;
import edu.kit.typicalc.util.Result;
import org.junit.jupiter.api.Test;
import java.util.HashMap;
import java.util.LinkedHashMap;
import java.util.Map;
@ -164,10 +165,10 @@ class TypeAssumptionParserTest {
assertEquals(new VarTerm("id"), assumption.getKey());
assertEquals(new TypeAbstraction(
new FunctionType(
new FunctionType(
new FunctionType(INT, INT),
new FunctionType(BOOLEAN, BOOLEAN)
),
new FunctionType(
new FunctionType(INT, INT),
new FunctionType(BOOLEAN, BOOLEAN)
),
new FunctionType(
new FunctionType(int2, boolean2),
new FunctionType(boolean2, int2)
@ -188,8 +189,37 @@ class TypeAssumptionParserTest {
assertEquals(new VarTerm("fun"), assumption.getKey());
assertEquals(new TypeAbstraction(
new FunctionType(
new FunctionType(new NamedType("a"), new FunctionType(new NamedType("b"), new NamedType("c"))),
new NamedType("d")
new FunctionType(new NamedType("a"), new FunctionType(new NamedType("b"), new NamedType("c"))),
new NamedType("d")
)), assumption.getValue());
}
@Test
void variousTypes() {
Type x = new NamedType("x");
Type xx = new FunctionType(x, x);
Type xxx = new FunctionType(x, xx);
Type xxxx = new FunctionType(x, xxx);
Type xxxxx = new FunctionType(xx, xxx);
Type xxxxxx = new FunctionType(xxx, xxx);
Map<String, TypeAbstraction> tests = new HashMap<>();
tests.put("x", new TypeAbstraction(x));
tests.put("x -> x", new TypeAbstraction(xx));
tests.put("x -> (x)", new TypeAbstraction(xx));
tests.put("x -> ((x))", new TypeAbstraction(xx));
tests.put("x -> x -> x", new TypeAbstraction(xxx));
tests.put("x -> (x -> x)", new TypeAbstraction(xxx));
tests.put("x -> x -> x -> x", new TypeAbstraction(xxxx));
tests.put("x -> (x -> x -> x)", new TypeAbstraction(xxxx));
tests.put("x -> (x -> (x -> x))", new TypeAbstraction(xxxx));
tests.put("x -> (x -> (x -> (x)))", new TypeAbstraction(xxxx));
tests.put("(x -> x) -> (x -> (x -> (x)))", new TypeAbstraction(xxxxx));
tests.put("((x) -> ((x)) -> (x)) -> (x -> (x -> (x)))", new TypeAbstraction(xxxxxx));
for (Map.Entry<String, TypeAbstraction> entry : tests.entrySet()) {
TypeAssumptionParser parser = new TypeAssumptionParser();
Result<Map<VarTerm, TypeAbstraction>, ParseError> type = parser.parse(Map.of("type1", entry.getKey()));
assertTrue(type.isOk());
assertEquals(entry.getValue(), type.unwrap().get(new VarTerm("type1")));
}
}
}

94
src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstraintsTest.java
View File

@ -15,38 +15,38 @@ class LatexCreatorConstraintsTest {
private static final String EMPTY_CONSTRAINT_SET =
ALIGN_BEGIN + AMPERSAND + CONSTRAINT_SET + EQUALS + LATEX_CURLY_LEFT + LATEX_CURLY_RIGHT + ALIGN_END;
private static final String MGU_START = LATEX_NEW_LINE + AMPERSAND + SPLIT_BEGIN + SIGMA + COLON + EQUALS + MGU + PAREN_LEFT
+ CONSTRAINT_SET + PAREN_RIGHT;
private final Model model = new ModelImpl();
private TypeInfererInterface typeInferer;
// todo tests should test all of getEverything, not only the first 2 parts
@Test
void singleVarDefaultConstraintTest() {
typeInferer = model.getTypeInferer("x", new HashMap<>()).unwrap();
List<String> expected = new LatexCreatorConstraints(typeInferer).getEverything();
List<String> actual = new LatexCreatorConstraints(typeInferer, Enum::toString).getEverything();
String constraintSet = AMPERSAND + CONSTRAINT_SET + EQUALS + LATEX_CURLY_LEFT + TREE_VARIABLE + "_{1}" + EQUALS
+ GENERATED_ASSUMPTION_VARIABLE + "_{1}" + LATEX_CURLY_RIGHT;
String mguStart = LATEX_NEW_LINE + AMPERSAND + SPLIT_BEGIN + SIGMA + COLON + EQUALS + MGU + PAREN_LEFT
+ CONSTRAINT_SET + PAREN_RIGHT;
String mgu = "" + EQUALS + BRACKET_LEFT + AMPERSAND + TREE_VARIABLE + "_{1}"
+ SUBSTITUTION_SIGN + GENERATED_ASSUMPTION_VARIABLE + "_{1}" + BRACKET_RIGHT + SPLIT_END;
List<String> actual = List.of(EMPTY_CONSTRAINT_SET,
List<String> expected = List.of(EMPTY_CONSTRAINT_SET,
ALIGN_BEGIN + constraintSet + ALIGN_END,
ALIGN_BEGIN + constraintSet + mguStart + EQUALS + UNIFY + PAREN_LEFT + LATEX_CURLY_LEFT + AMPERSAND
+ TREE_VARIABLE + "_{1}" + EQUALS + GENERATED_ASSUMPTION_VARIABLE + "_{1}" + PAREN_RIGHT
+ LATEX_CURLY_RIGHT + SPLIT_END + ALIGN_END,
ALIGN_BEGIN + constraintSet + mguStart + mgu + ALIGN_END,
ALIGN_BEGIN + constraintSet + mguStart + mgu + ALIGN_END,
ALIGN_BEGIN + constraintSet + mguStart + mgu + LATEX_NEW_LINE + AMPERSAND + SIGMA + PAREN_LEFT
ALIGN_BEGIN + constraintSet + MGU_START + EQUALS + UNIFY + PAREN_LEFT + LATEX_CURLY_LEFT + AMPERSAND
+ TREE_VARIABLE + "_{1}" + EQUALS + GENERATED_ASSUMPTION_VARIABLE + "_{1}" + LATEX_CURLY_RIGHT
+ PAREN_RIGHT + SPLIT_END + ALIGN_END,
ALIGN_BEGIN + constraintSet + MGU_START + mgu + ALIGN_END,
ALIGN_BEGIN + constraintSet + MGU_START + mgu + ALIGN_END,
ALIGN_BEGIN + constraintSet + MGU_START + mgu + LATEX_NEW_LINE + AMPERSAND + SIGMA + PAREN_LEFT
+ TREE_VARIABLE + "_{1}" + PAREN_RIGHT + EQUALS + GENERATED_ASSUMPTION_VARIABLE
+ "_{1}" + ALIGN_END);
assertEquals(actual.size(), expected.size());
for (int i = 0; i < actual.size(); i++) {
assertEquals(actual.get(i), expected.get(i));
assertEquals(expected.size(), actual.size());
for (int i = 0; i < expected.size(); i++) {
assertEquals(expected.get(i), actual.get(i));
}
}
@ -54,46 +54,46 @@ class LatexCreatorConstraintsTest {
@Test
void singleAbsDefaultConstraintTest() {
typeInferer = model.getTypeInferer("λx.y", new HashMap<>()).unwrap();
List<String> expected = new LatexCreatorConstraints(typeInferer).getEverything();
List<String> actual = new LatexCreatorConstraints(typeInferer, Enum::toString).getEverything();
List<String> actual = List.of(EMPTY_CONSTRAINT_SET,
ALIGN_BEGIN + AMPERSAND + CONSTRAINT_SET + EQUALS + LATEX_CURLY_LEFT + TREE_VARIABLE + "_{1}" + EQUALS
+ TREE_VARIABLE + "_{2}" + SPACE + RIGHT_ARROW + SPACE + TREE_VARIABLE + "_{3}"
+ LATEX_CURLY_RIGHT + ALIGN_END);
String constraintSet1 = AMPERSAND + CONSTRAINT_SET + EQUALS + LATEX_CURLY_LEFT + TREE_VARIABLE + "_{1}" + EQUALS
+ TREE_VARIABLE + "_{2}" + SPACE + RIGHT_ARROW + SPACE + TREE_VARIABLE + "_{3}" + LATEX_CURLY_RIGHT;
for (int i = 0; i < actual.size(); i++) {
assertEquals(actual.get(i), expected.get(i));
}
}
String constraintSet2 = AMPERSAND + CONSTRAINT_SET + EQUALS + LATEX_CURLY_LEFT + TREE_VARIABLE + "_{1}" + EQUALS
+ TREE_VARIABLE + "_{2}" + SPACE + RIGHT_ARROW + SPACE + TREE_VARIABLE + "_{3}" + COMMA + TREE_VARIABLE
+ "_{3}" + EQUALS + GENERATED_ASSUMPTION_VARIABLE + "_{1}" + LATEX_CURLY_RIGHT;
String unify1 = MGU_START + EQUALS + UNIFY + PAREN_LEFT + LATEX_CURLY_LEFT + AMPERSAND
+ TREE_VARIABLE + "_{3}" + EQUALS + GENERATED_ASSUMPTION_VARIABLE + "_{1}";
@Test
void singleAppConstraintTest() {
typeInferer = model.getTypeInferer("x y", new HashMap<>()).unwrap();
List<String> expected = new LatexCreatorConstraints(typeInferer).getEverything();
String subs2 = LATEX_NEW_LINE + CIRC
+ BRACKET_LEFT + AMPERSAND + TREE_VARIABLE + "_{1}" + SUBSTITUTION_SIGN + TREE_VARIABLE
+ "_{2}" + SPACE + RIGHT_ARROW + SPACE + TREE_VARIABLE + "_{3}" + BRACKET_RIGHT;
List<String> actual = List.of(EMPTY_CONSTRAINT_SET,
ALIGN_BEGIN + AMPERSAND + CONSTRAINT_SET + EQUALS + LATEX_CURLY_LEFT + TREE_VARIABLE + "_{2}" + EQUALS
+ TREE_VARIABLE + "_{3}" + SPACE + RIGHT_ARROW + SPACE + TREE_VARIABLE + "_{1}"
+ LATEX_CURLY_RIGHT + ALIGN_END);
String mgu = constraintSet2 + MGU_START + EQUALS + BRACKET_LEFT + AMPERSAND + TREE_VARIABLE + "_{1}"
+ SUBSTITUTION_SIGN + TREE_VARIABLE + "_{2}" + SPACE + RIGHT_ARROW + SPACE
+ GENERATED_ASSUMPTION_VARIABLE + "_{1}" + COMMA + LATEX_NEW_LINE + AMPERSAND + TREE_VARIABLE
+ "_{3}" + SUBSTITUTION_SIGN + GENERATED_ASSUMPTION_VARIABLE + "_{1}" + BRACKET_RIGHT
+ SPLIT_END;
for (int i = 0; i < actual.size(); i++) {
assertEquals(actual.get(i), expected.get(i));
}
}
List<String> expected = List.of(EMPTY_CONSTRAINT_SET,
ALIGN_BEGIN + constraintSet1 + ALIGN_END,
ALIGN_BEGIN + constraintSet2 + ALIGN_END,
ALIGN_BEGIN + constraintSet2 + unify1 + COMMA + LATEX_NEW_LINE + AMPERSAND + TREE_VARIABLE + "_{1}"
+ EQUALS + TREE_VARIABLE + "_{2}" + SPACE + RIGHT_ARROW + SPACE + TREE_VARIABLE + "_{3}"
+ LATEX_CURLY_RIGHT + PAREN_RIGHT + SPLIT_END + ALIGN_END,
ALIGN_BEGIN + constraintSet2 + unify1 + LATEX_CURLY_RIGHT + PAREN_RIGHT + subs2 + SPLIT_END + ALIGN_END,
ALIGN_BEGIN + constraintSet2 + MGU_START + EQUALS + BRACKET_LEFT + AMPERSAND + TREE_VARIABLE + "_{3}"
+ SUBSTITUTION_SIGN + GENERATED_ASSUMPTION_VARIABLE + "_{1}" + BRACKET_RIGHT + subs2 + SPLIT_END
+ ALIGN_END,
ALIGN_BEGIN + mgu + ALIGN_END,
ALIGN_BEGIN + mgu + LATEX_NEW_LINE + AMPERSAND + SIGMA + PAREN_LEFT + TREE_VARIABLE + "_{1}"
+ PAREN_RIGHT + EQUALS + TREE_VARIABLE + "_{2}" + SPACE + RIGHT_ARROW + SPACE
+ GENERATED_ASSUMPTION_VARIABLE + "_{1}" + ALIGN_END);
@Test
void singleConstConstraintTest() {
typeInferer = model.getTypeInferer("5", new HashMap<>()).unwrap();
List<String> expected = new LatexCreatorConstraints(typeInferer).getEverything();
List<String> actual = List.of(EMPTY_CONSTRAINT_SET,
ALIGN_BEGIN + AMPERSAND + CONSTRAINT_SET + EQUALS + LATEX_CURLY_LEFT + TREE_VARIABLE + "_{1}" + EQUALS
+ MONO_TEXT + "{int}" + LATEX_CURLY_RIGHT + ALIGN_END);
for (int i = 0; i < actual.size(); i++) {
assertEquals(actual.get(i), expected.get(i));
assertEquals(expected.size(), actual.size());
for (int i = 0; i < expected.size(); i++) {
assertEquals(expected.get(i), actual.get(i));
}
}
}