mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-08 18:30:42 +00:00
Add java docs and remove unused methods
This commit is contained in:
parent
2bc908e660
commit
49adac2a88
@ -33,6 +33,10 @@ import edu.kit.typicalc.view.TypicalcI18NProvider;
|
|||||||
import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.DOLLAR_SIGN;
|
import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.DOLLAR_SIGN;
|
||||||
import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.SPACE;
|
import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.SPACE;
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Generates LaTeX code for explanatory texts in a specific language for every step of the type inference algorithm.
|
||||||
|
* To do this, text templates from the resource bundle are filled out with specific content for every input.
|
||||||
|
*/
|
||||||
public class ExplanationCreator implements StepVisitor {
|
public class ExplanationCreator implements StepVisitor {
|
||||||
private static final String KEY_PREFIX = "explanationTree.";
|
private static final String KEY_PREFIX = "explanationTree.";
|
||||||
|
|
||||||
@ -47,7 +51,12 @@ public class ExplanationCreator implements StepVisitor {
|
|||||||
private boolean errorOccurred; // true if one unification was not successful
|
private boolean errorOccurred; // true if one unification was not successful
|
||||||
private int letCounter = 0; // count number of lets for unification indices
|
private int letCounter = 0; // count number of lets for unification indices
|
||||||
|
|
||||||
// creates explanation texts for a specific language
|
/**
|
||||||
|
* Generate the LaTeX code from the type inferer for the language of the provided locale.
|
||||||
|
*
|
||||||
|
* @param typeInferer the TypeInfererInterface to create the LaTeX-code from
|
||||||
|
* @param locale the language of the explanatory texts
|
||||||
|
*/
|
||||||
public ExplanationCreator(TypeInfererInterface typeInferer, Locale locale) {
|
public ExplanationCreator(TypeInfererInterface typeInferer, Locale locale) {
|
||||||
this.locale = locale;
|
this.locale = locale;
|
||||||
errorOccurred = false;
|
errorOccurred = false;
|
||||||
@ -60,6 +69,11 @@ public class ExplanationCreator implements StepVisitor {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Returns a list of strings with an entry for every step of the algorithm.
|
||||||
|
*
|
||||||
|
* @return list of strings containing the explanatory texts
|
||||||
|
*/
|
||||||
public List<String> getExplanationTexts() {
|
public List<String> getExplanationTexts() {
|
||||||
return explanationTexts;
|
return explanationTexts;
|
||||||
}
|
}
|
||||||
@ -156,7 +170,6 @@ public class ExplanationCreator implements StepVisitor {
|
|||||||
@Override
|
@Override
|
||||||
public void visit(VarStepWithLet varL) {
|
public void visit(VarStepWithLet varL) {
|
||||||
explanationTexts.add(createLatexVarStep(varL));
|
explanationTexts.add(createLatexVarStep(varL));
|
||||||
// TODO: maybe create slightly different text
|
|
||||||
}
|
}
|
||||||
|
|
||||||
private String createLatexVarStep(VarStep varS) {
|
private String createLatexVarStep(VarStep varS) {
|
||||||
@ -209,10 +222,12 @@ public class ExplanationCreator implements StepVisitor {
|
|||||||
|
|
||||||
@Override
|
@Override
|
||||||
public void visit(EmptyStep empty) {
|
public void visit(EmptyStep empty) {
|
||||||
|
// no implementation since EmptyStep is not visible for the user
|
||||||
}
|
}
|
||||||
|
|
||||||
@Override
|
@Override
|
||||||
public void visit(OnlyConclusionStep onlyConc) {
|
public void visit(OnlyConclusionStep onlyConc) {
|
||||||
|
// no implementation since OnlyConclusionStep is not visible for the user
|
||||||
}
|
}
|
||||||
|
|
||||||
}
|
}
|
||||||
|
@ -39,6 +39,9 @@ import edu.kit.typicalc.model.type.Type;
|
|||||||
import edu.kit.typicalc.model.type.TypeArgumentVisitor;
|
import edu.kit.typicalc.model.type.TypeArgumentVisitor;
|
||||||
import edu.kit.typicalc.util.Result;
|
import edu.kit.typicalc.util.Result;
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Generates LaTeX code for explanatory texts in a specific language for every step of the unification algorithm.
|
||||||
|
*/
|
||||||
public class ExplanationCreatorUnification {
|
public class ExplanationCreatorUnification {
|
||||||
private static final String KEY_PREFIX = "expUnification.";
|
private static final String KEY_PREFIX = "expUnification.";
|
||||||
private static final String LET_KEY_PREFIX = "expLetUnification.";
|
private static final String LET_KEY_PREFIX = "expLetUnification.";
|
||||||
@ -54,7 +57,18 @@ public class ExplanationCreatorUnification {
|
|||||||
private final List<String> unificationTexts = new ArrayList<>();
|
private final List<String> unificationTexts = new ArrayList<>();
|
||||||
private boolean errorOccurred;
|
private boolean errorOccurred;
|
||||||
|
|
||||||
public ExplanationCreatorUnification(TypeInfererInterface typeInferer, Locale locale, I18NProvider provider,
|
/**
|
||||||
|
* Generates LaTeX code from the provided type inferer for the unification algorithm.
|
||||||
|
*
|
||||||
|
* @param typeInferer the TypeInfererInterface to create the LaTeX-code from
|
||||||
|
* @param locale the language of the explanatory texts
|
||||||
|
* @param provider I18NProvider to get the templates from the resources bundle
|
||||||
|
* @param mode the used LaTeX generation method
|
||||||
|
* @param letCounter counter needed for nested let terms
|
||||||
|
* @param isLetUnification variable to indicate if it is the final unification or a let unification
|
||||||
|
* @param letVariable optional containing the let variable in case of a let unification
|
||||||
|
*/
|
||||||
|
protected ExplanationCreatorUnification(TypeInfererInterface typeInferer, Locale locale, I18NProvider provider,
|
||||||
LatexCreatorMode mode, int letCounter, boolean isLetUnification, Optional<LambdaTerm> letVariable) {
|
LatexCreatorMode mode, int letCounter, boolean isLetUnification, Optional<LambdaTerm> letVariable) {
|
||||||
this.typeInferer = typeInferer;
|
this.typeInferer = typeInferer;
|
||||||
this.locale = locale;
|
this.locale = locale;
|
||||||
@ -66,7 +80,13 @@ public class ExplanationCreatorUnification {
|
|||||||
buildTexts(isLetUnification);
|
buildTexts(isLetUnification);
|
||||||
}
|
}
|
||||||
|
|
||||||
public Pair<List<String>, Boolean> getUnificationsTexts() {
|
/**
|
||||||
|
* Returns a pair of a list of strings containing the explanatory texts and a boolean value.
|
||||||
|
* The boolean value is true if an error occurred during the let unification.
|
||||||
|
*
|
||||||
|
* @return a pair of a list of strings and a boolean value
|
||||||
|
*/
|
||||||
|
protected Pair<List<String>, Boolean> getUnificationsTexts() {
|
||||||
return Pair.of(unificationTexts, errorOccurred);
|
return Pair.of(unificationTexts, errorOccurred);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -29,7 +29,7 @@ public class LatexCreator implements StepVisitor {
|
|||||||
/**
|
/**
|
||||||
* Generate the pieces of LaTeX-code from the type inferer.
|
* Generate the pieces of LaTeX-code from the type inferer.
|
||||||
*
|
*
|
||||||
* @param typeInferer theTypeInfererInterface to create the LaTeX-code from
|
* @param typeInferer the TypeInfererInterface to create the LaTeX-code from
|
||||||
* @param translationProvider translation text provider for {@link UnificationError}
|
* @param translationProvider translation text provider for {@link UnificationError}
|
||||||
* @param mode LaTeX creation mode
|
* @param mode LaTeX creation mode
|
||||||
*/
|
*/
|
||||||
@ -41,7 +41,7 @@ public class LatexCreator implements StepVisitor {
|
|||||||
/**
|
/**
|
||||||
* Generate the pieces of LaTeX-code from the type inferer.
|
* Generate the pieces of LaTeX-code from the type inferer.
|
||||||
*
|
*
|
||||||
* @param typeInferer theTypeInfererInterface to create the LaTeX code from
|
* @param typeInferer the TypeInfererInterface to create the LaTeX code from
|
||||||
* @param stepLabels turns step labels on or off
|
* @param stepLabels turns step labels on or off
|
||||||
* @param translationProvider translation text provider for {@link UnificationError}
|
* @param translationProvider translation text provider for {@link UnificationError}
|
||||||
* @param mode LaTeX creation mode
|
* @param mode LaTeX creation mode
|
||||||
|
@ -1,47 +1,24 @@
|
|||||||
package edu.kit.typicalc.view.main;
|
package edu.kit.typicalc.view.main;
|
||||||
|
|
||||||
import java.util.Arrays;
|
|
||||||
import java.util.List;
|
|
||||||
import java.util.stream.Collectors;
|
|
||||||
|
|
||||||
import org.apache.commons.lang3.StringUtils;
|
|
||||||
|
|
||||||
import com.vaadin.flow.component.UI;
|
import com.vaadin.flow.component.UI;
|
||||||
import com.vaadin.flow.component.dependency.JsModule;
|
import com.vaadin.flow.component.dependency.JsModule;
|
||||||
import com.vaadin.flow.component.textfield.TextField;
|
import com.vaadin.flow.component.textfield.TextField;
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Textfield which allows the user to enter an arbitrary number of type assumptions.
|
||||||
|
*/
|
||||||
@JsModule("./src/type-input-listener.ts")
|
@JsModule("./src/type-input-listener.ts")
|
||||||
public class AssumptionInputField extends TextField {
|
public class AssumptionInputField extends TextField {
|
||||||
private static final long serialVersionUID = -3887662656039679338L;
|
private static final long serialVersionUID = -3887662656039679338L;
|
||||||
|
|
||||||
private static final String ASSUMPTION_INPUT_FIELD_CLASS = "assumption-input-field";
|
private static final String ASSUMPTION_INPUT_FIELD_CLASS = "assumption-input-field";
|
||||||
|
|
||||||
/*
|
|
||||||
* Unicode of subscripted digits in increasing order
|
|
||||||
*/
|
|
||||||
private static final List<Character> SUBSCRIPTED_DIGITS =
|
|
||||||
List.of('\u2080', '\u2081', '\u2082', '\u2083', '\u2084',
|
|
||||||
'\u2085', '\u2086', '\u2087', '\u2088', '\u2089');
|
|
||||||
private static final char TAU = '\u03C4';
|
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Creates an AssumptionInputField.
|
||||||
|
*/
|
||||||
protected AssumptionInputField() {
|
protected AssumptionInputField() {
|
||||||
setClassName(ASSUMPTION_INPUT_FIELD_CLASS);
|
setClassName(ASSUMPTION_INPUT_FIELD_CLASS);
|
||||||
UI.getCurrent().getPage().executeJs("window.addTypeInputListener($0)", ASSUMPTION_INPUT_FIELD_CLASS);
|
UI.getCurrent().getPage().executeJs("window.addTypeInputListener($0)", ASSUMPTION_INPUT_FIELD_CLASS);
|
||||||
}
|
}
|
||||||
|
|
||||||
protected List<String> getTypeAssumptions() {
|
|
||||||
return Arrays.stream(parseBack(getOptionalValue().orElse(StringUtils.EMPTY)).split(";"))
|
|
||||||
.collect(Collectors.toList());
|
|
||||||
}
|
|
||||||
|
|
||||||
private String parseBack(String value) {
|
|
||||||
String rawValue = value.replace(TAU, 't');
|
|
||||||
char[] rawValueArray = rawValue.toCharArray();
|
|
||||||
for (int i = 0; i < rawValueArray.length; i++) {
|
|
||||||
if (SUBSCRIPTED_DIGITS.contains(rawValueArray[i])) {
|
|
||||||
rawValueArray[i] = Character.forDigit(SUBSCRIPTED_DIGITS.indexOf(rawValueArray[i]), 10);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
return new String(rawValueArray);
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
@ -6,7 +6,12 @@ import com.vaadin.flow.component.orderedlayout.VerticalLayout;
|
|||||||
import com.vaadin.flow.i18n.LocaleChangeEvent;
|
import com.vaadin.flow.i18n.LocaleChangeEvent;
|
||||||
import com.vaadin.flow.i18n.LocaleChangeObserver;
|
import com.vaadin.flow.i18n.LocaleChangeObserver;
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Component which contains information on the correct syntax of the term as well as the type assumptions.
|
||||||
|
*/
|
||||||
public class InfoContent extends VerticalLayout implements LocaleChangeObserver {
|
public class InfoContent extends VerticalLayout implements LocaleChangeObserver {
|
||||||
|
private static final long serialVersionUID = 7193916603756938225L;
|
||||||
|
|
||||||
private static final String GRAMMAR_ID = "input-syntax";
|
private static final String GRAMMAR_ID = "input-syntax";
|
||||||
|
|
||||||
private final Span termExplanation;
|
private final Span termExplanation;
|
||||||
@ -15,6 +20,9 @@ public class InfoContent extends VerticalLayout implements LocaleChangeObserver
|
|||||||
private final Span typeExplanation;
|
private final Span typeExplanation;
|
||||||
private final Paragraph typeSyntax;
|
private final Paragraph typeSyntax;
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Creates a new InfoContent.
|
||||||
|
*/
|
||||||
public InfoContent() {
|
public InfoContent() {
|
||||||
termExplanation = new Span();
|
termExplanation = new Span();
|
||||||
termSyntax = new Paragraph();
|
termSyntax = new Paragraph();
|
||||||
|
@ -63,9 +63,6 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
|
|||||||
termInputField.setClearButtonVisible(true);
|
termInputField.setClearButtonVisible(true);
|
||||||
termInputField.setMaxLength(MAX_INPUT_LENGTH);
|
termInputField.setMaxLength(MAX_INPUT_LENGTH);
|
||||||
|
|
||||||
// attach a listener that replaces \ with λ
|
|
||||||
// JavaScript is used because this is a latency-sensitive operation
|
|
||||||
// (and Vaadin does not have APIs for selectionStart/selectionEnd)
|
|
||||||
UI.getCurrent().getPage().executeJs("window.characterListener($0);", TERM_INPUT_FIELD_ID);
|
UI.getCurrent().getPage().executeJs("window.characterListener($0);", TERM_INPUT_FIELD_ID);
|
||||||
Button lambdaButton = new Button(getTranslation("root.lambda"));
|
Button lambdaButton = new Button(getTranslation("root.lambda"));
|
||||||
lambdaButton.setId(LAMBDA_BUTTON_ID);
|
lambdaButton.setId(LAMBDA_BUTTON_ID);
|
||||||
|
Loading…
Reference in New Issue
Block a user