mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-09-16 16:55:08 +00:00
Small code style fixes + documentation
This commit is contained in:
parent
b26f71e8b2
commit
376933a4f5
@ -30,8 +30,7 @@ You can now also attach break points in code for debugging purposes, by clicking
|
|||||||
### Running tests
|
### Running tests
|
||||||
To run the unit tests and checkstyle: `mvn test`.
|
To run the unit tests and checkstyle: `mvn test`.
|
||||||
|
|
||||||
To run the integration tests: `mvn integration-test` (note that due to OS platform differences, it is unlikely that
|
To run the integration tests: `mvn integration-test` (note that the screenshots are outdated, so the tests will fail..).
|
||||||
you will get a 100% match on the first attempt.)
|
|
||||||
|
|
||||||
## Technical documentation
|
## Technical documentation
|
||||||
Documentation on the application is contained in this file and the Javadocs in each source file.
|
Documentation on the application is contained in this file and the Javadocs in each source file.
|
||||||
|
@ -1,3 +0,0 @@
|
|||||||
#tc-content {
|
|
||||||
overflow-y: auto;
|
|
||||||
}
|
|
@ -1,3 +0,0 @@
|
|||||||
[part="toggle"] {
|
|
||||||
color: white;
|
|
||||||
}
|
|
@ -1,4 +0,0 @@
|
|||||||
#inputSyntax {
|
|
||||||
font-family: "Courier", serif;
|
|
||||||
margin-top: 1.5em;
|
|
||||||
}
|
|
@ -9,7 +9,7 @@
|
|||||||
align-items: flex-start;
|
align-items: flex-start;
|
||||||
}
|
}
|
||||||
|
|
||||||
#input-syntax {
|
.input-syntax {
|
||||||
font-family: "Courier";
|
font-family: "Courier";
|
||||||
margin-top: 1.5em;
|
margin-top: 1.5em;
|
||||||
}
|
}
|
@ -32,18 +32,18 @@ public class ModelImpl implements Model {
|
|||||||
LambdaParser parser = new LambdaParser(lambdaTerm);
|
LambdaParser parser = new LambdaParser(lambdaTerm);
|
||||||
Result<LambdaTerm, ParseError> result = parser.parse();
|
Result<LambdaTerm, ParseError> result = parser.parse();
|
||||||
if (result.isError()) {
|
if (result.isError()) {
|
||||||
return new Result<>(null, result.unwrapError());
|
return result.castError();
|
||||||
}
|
}
|
||||||
//Parse Type Assumptions
|
//Parse Type Assumptions
|
||||||
TypeAssumptionParser assumptionParser = new TypeAssumptionParser();
|
TypeAssumptionParser assumptionParser = new TypeAssumptionParser();
|
||||||
Result<Map<VarTerm, TypeAbstraction>, ParseError> assumptionMap = assumptionParser.parse(typeAssumptions);
|
Result<Map<VarTerm, TypeAbstraction>, ParseError> assumptionMap = assumptionParser.parse(typeAssumptions);
|
||||||
if (assumptionMap.isError()) {
|
if (assumptionMap.isError()) {
|
||||||
return new Result<>(null, assumptionMap.unwrapError());
|
return assumptionMap.castError();
|
||||||
}
|
}
|
||||||
// scope variables
|
// scope variables
|
||||||
LambdaTerm term = result.unwrap();
|
LambdaTerm term = result.unwrap();
|
||||||
term.accept(new ScopingVisitor());
|
term.accept(new ScopingVisitor());
|
||||||
TypeInferer typeInferer = new TypeInferer(term, assumptionMap.unwrap());
|
TypeInferer typeInferer = new TypeInferer(term, assumptionMap.unwrap());
|
||||||
return new Result<>(typeInferer, null);
|
return new Result<>(typeInferer);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -33,8 +33,8 @@ public class Unification {
|
|||||||
Type b = c.getSecondType();
|
Type b = c.getSecondType();
|
||||||
Result<UnificationActions, UnificationError> actions = a.constrainEqualTo(b);
|
Result<UnificationActions, UnificationError> actions = a.constrainEqualTo(b);
|
||||||
if (actions.isError()) {
|
if (actions.isError()) {
|
||||||
steps.add(new UnificationStep(new Result<>(actions), new ArrayList<>(constraints), Optional.of(c)));
|
steps.add(new UnificationStep(actions.castError(), new ArrayList<>(constraints), Optional.of(c)));
|
||||||
substitutionsResult = new Result<>(actions);
|
substitutionsResult = actions.castError();
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
UnificationActions thisStep = actions.unwrap();
|
UnificationActions thisStep = actions.unwrap();
|
||||||
|
@ -35,7 +35,7 @@ public class LambdaLexer {
|
|||||||
while (true) {
|
while (true) {
|
||||||
Result<Token, ParseError> token = parseNextToken();
|
Result<Token, ParseError> token = parseNextToken();
|
||||||
if (token.isError()) {
|
if (token.isError()) {
|
||||||
result = new Result<>(null, token.unwrapError());
|
result = token.castError();
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
Token value = token.unwrap();
|
Token value = token.unwrap();
|
||||||
|
@ -158,7 +158,7 @@ public class LambdaParser {
|
|||||||
}
|
}
|
||||||
Result<VarTerm, ParseError> varTerm = parseVar();
|
Result<VarTerm, ParseError> varTerm = parseVar();
|
||||||
if (varTerm.isError()) {
|
if (varTerm.isError()) {
|
||||||
return new Result<>(varTerm);
|
return varTerm.castError();
|
||||||
}
|
}
|
||||||
error = expect(TokenType.EQUALS);
|
error = expect(TokenType.EQUALS);
|
||||||
if (error.isPresent()) {
|
if (error.isPresent()) {
|
||||||
@ -166,7 +166,7 @@ public class LambdaParser {
|
|||||||
}
|
}
|
||||||
Result<LambdaTerm, ParseError> def = parseTerm(false);
|
Result<LambdaTerm, ParseError> def = parseTerm(false);
|
||||||
if (def.isError()) {
|
if (def.isError()) {
|
||||||
return new Result<>(def);
|
return def.castError();
|
||||||
}
|
}
|
||||||
error = expect(TokenType.IN);
|
error = expect(TokenType.IN);
|
||||||
if (error.isPresent()) {
|
if (error.isPresent()) {
|
||||||
@ -174,7 +174,7 @@ public class LambdaParser {
|
|||||||
}
|
}
|
||||||
Result<LambdaTerm, ParseError> body = parseTerm(false);
|
Result<LambdaTerm, ParseError> body = parseTerm(false);
|
||||||
if (body.isError()) {
|
if (body.isError()) {
|
||||||
return new Result<>(body);
|
return body.castError();
|
||||||
}
|
}
|
||||||
return new Result<>(new LetTerm(varTerm.unwrap(), def.unwrap(), body.unwrap()));
|
return new Result<>(new LetTerm(varTerm.unwrap(), def.unwrap(), body.unwrap()));
|
||||||
}
|
}
|
||||||
@ -190,9 +190,9 @@ public class LambdaParser {
|
|||||||
Result<VarTerm, ParseError> varTerm = parseVar();
|
Result<VarTerm, ParseError> varTerm = parseVar();
|
||||||
return new Result<>(varTerm.unwrap()); // variable token can always be parsed
|
return new Result<>(varTerm.unwrap()); // variable token can always be parsed
|
||||||
case LAMBDA:
|
case LAMBDA:
|
||||||
return new Result<>(parseAbstraction());
|
return parseAbstraction().castError();
|
||||||
case LET:
|
case LET:
|
||||||
return new Result<>(parseLet());
|
return parseLet().castError();
|
||||||
case TRUE:
|
case TRUE:
|
||||||
case FALSE:
|
case FALSE:
|
||||||
String boolText = token.getText();
|
String boolText = token.getText();
|
||||||
|
@ -23,17 +23,6 @@ public class Result<T, E> {
|
|||||||
this.error = null;
|
this.error = null;
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
|
||||||
* Creates a new result by copying another one.
|
|
||||||
*
|
|
||||||
* @param other the result
|
|
||||||
*/
|
|
||||||
@SuppressWarnings("unchecked")
|
|
||||||
public Result(Result<?, ?> other) {
|
|
||||||
this.value = (T) other.value;
|
|
||||||
this.error = (E) other.error;
|
|
||||||
}
|
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Creates a new result containing the given value or error.
|
* Creates a new result containing the given value or error.
|
||||||
* Only one of the parameters may be non-null.
|
* Only one of the parameters may be non-null.
|
||||||
@ -78,19 +67,6 @@ public class Result<T, E> {
|
|||||||
return value;
|
return value;
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
|
||||||
* If the result contains a regular value, returns that value.
|
|
||||||
* Otherwise return the supplied alternative value.
|
|
||||||
*
|
|
||||||
* @return the value or the alternative
|
|
||||||
*/
|
|
||||||
public T unwrapOr(T alternative) {
|
|
||||||
if (value == null) {
|
|
||||||
return alternative;
|
|
||||||
}
|
|
||||||
return value;
|
|
||||||
}
|
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* If the result contains an error, returns that error.
|
* If the result contains an error, returns that error.
|
||||||
* Otherwise an IllegalStateException is thrown.
|
* Otherwise an IllegalStateException is thrown.
|
||||||
@ -123,8 +99,9 @@ public class Result<T, E> {
|
|||||||
* @param <U> the desired type
|
* @param <U> the desired type
|
||||||
* @return a copy of this object
|
* @return a copy of this object
|
||||||
*/
|
*/
|
||||||
|
@SuppressWarnings("unchecked")
|
||||||
public <U> Result<U, E> castError() {
|
public <U> Result<U, E> castError() {
|
||||||
return new Result<>(null, this.error);
|
return new Result<>((U) this.value, this.error);
|
||||||
}
|
}
|
||||||
|
|
||||||
@Override
|
@Override
|
||||||
|
@ -39,4 +39,14 @@ If a step label is targeted, a tooltip is rendered next to it (was very annoying
|
|||||||
The last paragraph requires that some elements of the proof tree / unification steps are marked using HTML classes
|
The last paragraph requires that some elements of the proof tree / unification steps are marked using HTML classes
|
||||||
and CSS IDs. It would be useless to expose this implementation detail to end users (especially since the relevant
|
and CSS IDs. It would be useless to expose this implementation detail to end users (especially since the relevant
|
||||||
LaTeX macros are unlikely to be defined in the user's environment).
|
LaTeX macros are unlikely to be defined in the user's environment).
|
||||||
Note that the actual content is the same for both "modes".
|
Note that the actual content is the same for both "modes".
|
||||||
|
|
||||||
|
### Special character (∀, λ) input
|
||||||
|
|
||||||
|
This is handled by a script (`input-bar-enhancements.ts`) in the user's browser, to reduce latency.
|
||||||
|
The buttons next to the input fields are also handled the same way.
|
||||||
|
|
||||||
|
### Browser history
|
||||||
|
|
||||||
|
Each click on the 'type' button results in a new history entry. Care has been taken that using the back/next buttons
|
||||||
|
in the browser actually works (see `UI.navigate` in `MainViewImpl.processInput`).
|
@ -14,7 +14,7 @@ import edu.kit.typicalc.model.parser.AdditionalInformation;
|
|||||||
import edu.kit.typicalc.model.parser.ExpectedInput;
|
import edu.kit.typicalc.model.parser.ExpectedInput;
|
||||||
import edu.kit.typicalc.model.parser.ParseError;
|
import edu.kit.typicalc.model.parser.ParseError;
|
||||||
import edu.kit.typicalc.model.parser.Token;
|
import edu.kit.typicalc.model.parser.Token;
|
||||||
import edu.kit.typicalc.view.main.InfoContent;
|
import edu.kit.typicalc.view.main.SyntaxContent;
|
||||||
|
|
||||||
import java.util.Collection;
|
import java.util.Collection;
|
||||||
import java.util.Optional;
|
import java.util.Optional;
|
||||||
@ -41,11 +41,11 @@ public class ErrorView extends VerticalLayout implements LocaleChangeObserver {
|
|||||||
errorMessage = new Div();
|
errorMessage = new Div();
|
||||||
container.add(heading, errorMessage);
|
container.add(heading, errorMessage);
|
||||||
|
|
||||||
InfoContent infoContent = new InfoContent();
|
SyntaxContent syntaxContent = new SyntaxContent();
|
||||||
hint = new Paragraph();
|
hint = new Paragraph();
|
||||||
infoContent.addComponentAsFirst(hint);
|
syntaxContent.addComponentAsFirst(hint);
|
||||||
|
|
||||||
add(container, infoContent);
|
add(container, syntaxContent);
|
||||||
}
|
}
|
||||||
|
|
||||||
private String errorMessageForToken(Token token) {
|
private String errorMessageForToken(Token token) {
|
||||||
|
@ -3,7 +3,6 @@ package edu.kit.typicalc.view.content.typeinferencecontent;
|
|||||||
import com.vaadin.flow.component.ClientCallable;
|
import com.vaadin.flow.component.ClientCallable;
|
||||||
import com.vaadin.flow.component.Html;
|
import com.vaadin.flow.component.Html;
|
||||||
import com.vaadin.flow.component.Tag;
|
import com.vaadin.flow.component.Tag;
|
||||||
import com.vaadin.flow.component.dependency.CssImport;
|
|
||||||
import com.vaadin.flow.component.dependency.JsModule;
|
import com.vaadin.flow.component.dependency.JsModule;
|
||||||
import com.vaadin.flow.component.html.Div;
|
import com.vaadin.flow.component.html.Div;
|
||||||
import com.vaadin.flow.component.littemplate.LitTemplate;
|
import com.vaadin.flow.component.littemplate.LitTemplate;
|
||||||
@ -11,17 +10,17 @@ import com.vaadin.flow.component.template.Id;
|
|||||||
import edu.kit.typicalc.view.MathjaxAdapter;
|
import edu.kit.typicalc.view.MathjaxAdapter;
|
||||||
|
|
||||||
import java.util.List;
|
import java.util.List;
|
||||||
|
import java.util.function.Consumer;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Renders the constraints and unification (LaTeX, using MathJax) and allows step-by-
|
* Renders the constraints and unification (LaTeX, using MathJax) and allows step-by-
|
||||||
* step revealing. Relies on MathjaxUnificationTS to interact with MathJax.
|
* step revealing.
|
||||||
*/
|
*/
|
||||||
@Tag("tc-explanation")
|
@Tag("tc-explanation")
|
||||||
@JsModule("./src/mathjax-explanation.ts")
|
@JsModule("./src/mathjax-explanation.ts")
|
||||||
@CssImport("./styles/view/explanation.css")
|
|
||||||
public class MathjaxExplanation extends LitTemplate implements MathjaxAdapter {
|
public class MathjaxExplanation extends LitTemplate implements MathjaxAdapter {
|
||||||
|
|
||||||
private final TypeInferenceView typeInferenceView;
|
private final transient Consumer<Integer> stepSwitchCallback;
|
||||||
private final List<String> latex;
|
private final List<String> latex;
|
||||||
|
|
||||||
// initialized by Vaadin
|
// initialized by Vaadin
|
||||||
@ -31,15 +30,16 @@ public class MathjaxExplanation extends LitTemplate implements MathjaxAdapter {
|
|||||||
/**
|
/**
|
||||||
* Creates a new HTML element that renders the provided texts.
|
* Creates a new HTML element that renders the provided texts.
|
||||||
*
|
*
|
||||||
* @param view the type inference view this explanation text is attached to
|
* @param stepSwitchCallback the callback used when the user clicks on one of the texts
|
||||||
* @param latex the latex texts for all steps
|
* @param latex the latex texts for all steps
|
||||||
* @param initialStep the step to show initially
|
* @param initialStep the step to show initially
|
||||||
*/
|
*/
|
||||||
public MathjaxExplanation(TypeInferenceView view, List<String> latex, int initialStep) {
|
public MathjaxExplanation(Consumer<Integer> stepSwitchCallback, List<String> latex, int initialStep) {
|
||||||
this.typeInferenceView = view;
|
this.stepSwitchCallback = stepSwitchCallback;
|
||||||
this.latex = latex;
|
this.latex = latex;
|
||||||
StringBuilder finalTex = new StringBuilder("<div>");
|
StringBuilder finalTex = new StringBuilder("<div>");
|
||||||
for (int i = 0; i < latex.size(); i++) {
|
for (int i = 0; i < latex.size(); i++) {
|
||||||
|
// this class/id is used by the frontend script to locate texts
|
||||||
finalTex.append(String.format("<p class='tc-text' id='tc-text-%d'>", i));
|
finalTex.append(String.format("<p class='tc-text' id='tc-text-%d'>", i));
|
||||||
finalTex.append(latex.get(i));
|
finalTex.append(latex.get(i));
|
||||||
finalTex.append("</p>");
|
finalTex.append("</p>");
|
||||||
@ -59,9 +59,12 @@ public class MathjaxExplanation extends LitTemplate implements MathjaxAdapter {
|
|||||||
getElement().callJsFunction("showStep", n);
|
getElement().callJsFunction("showStep", n);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Called when the user clicks on the explanation text of a specific step.
|
||||||
|
*/
|
||||||
@ClientCallable
|
@ClientCallable
|
||||||
private void switchToStep(int unificationStepIdx) {
|
private void switchToStep(int unificationStepIdx) {
|
||||||
typeInferenceView.setCurrentStep(unificationStepIdx);
|
stepSwitchCallback.accept(unificationStepIdx);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -130,7 +130,8 @@ public class TypeInferenceView extends VerticalLayout
|
|||||||
container.setId(CONTENT_ID2);
|
container.setId(CONTENT_ID2);
|
||||||
unification = new MathjaxUnification(lc.getUnification());
|
unification = new MathjaxUnification(lc.getUnification());
|
||||||
var explainer = new ExplanationCreator(typeInferer, getLocale());
|
var explainer = new ExplanationCreator(typeInferer, getLocale());
|
||||||
this.explanation = new MathjaxExplanation(this, explainer.getExplanationTexts(), this.currentStep);
|
this.explanation = new MathjaxExplanation(
|
||||||
|
this::setCurrentStep, explainer.getExplanationTexts(), this.currentStep);
|
||||||
|
|
||||||
if (tree == null) {
|
if (tree == null) {
|
||||||
tree = new MathjaxProofTree(lc.getTree(), stepAnnotations);
|
tree = new MathjaxProofTree(lc.getTree(), stepAnnotations);
|
||||||
|
@ -18,7 +18,15 @@ public final class AssumptionGeneratorUtil {
|
|||||||
private AssumptionGeneratorUtil() {
|
private AssumptionGeneratorUtil() {
|
||||||
}
|
}
|
||||||
|
|
||||||
protected static String typeAssumptionsToLatex(Map<VarTerm, TypeAbstraction> typeAssumptions,
|
/**
|
||||||
|
* Converts some type assumptions into LaTeX code to display them.
|
||||||
|
* Basic structure: name: Type, otherName: OtherType
|
||||||
|
*
|
||||||
|
* @param typeAssumptions the type assumptions
|
||||||
|
* @param mode latex creator mode
|
||||||
|
* @return the latex code
|
||||||
|
*/
|
||||||
|
static String typeAssumptionsToLatex(Map<VarTerm, TypeAbstraction> typeAssumptions,
|
||||||
LatexCreatorMode mode) {
|
LatexCreatorMode mode) {
|
||||||
if (typeAssumptions.isEmpty()) {
|
if (typeAssumptions.isEmpty()) {
|
||||||
return "";
|
return "";
|
||||||
@ -37,6 +45,14 @@ public final class AssumptionGeneratorUtil {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Return the latex code for a given type abstraction, e.g.:
|
||||||
|
* ∀t1. t1 -> t1
|
||||||
|
*
|
||||||
|
* @param abs the type abstraction
|
||||||
|
* @param mode latex creator mode
|
||||||
|
* @return the latex code
|
||||||
|
*/
|
||||||
public static String generateTypeAbstraction(TypeAbstraction abs, LatexCreatorMode mode) {
|
public static String generateTypeAbstraction(TypeAbstraction abs, LatexCreatorMode mode) {
|
||||||
StringBuilder abstraction = new StringBuilder();
|
StringBuilder abstraction = new StringBuilder();
|
||||||
if (abs.hasQuantifiedVariables()) {
|
if (abs.hasQuantifiedVariables()) {
|
||||||
|
@ -43,8 +43,6 @@ public final class LatexCreatorConstants {
|
|||||||
protected static final char BRACKET_RIGHT = ']';
|
protected static final char BRACKET_RIGHT = ']';
|
||||||
|
|
||||||
protected static final String LABEL_ABS = "\\LeftLabel{\\textrm A{\\small BS}}";
|
protected static final String LABEL_ABS = "\\LeftLabel{\\textrm A{\\small BS}}";
|
||||||
protected static final String LABEL_ABS_WITH_CLASS =
|
|
||||||
"\\LeftLabel{\\class{typicalc-label typicalc-label-abs}{\\textrm A{\\small BS}}}";
|
|
||||||
protected static final String LABEL_APP = "\\LeftLabel{\\textrm A{\\small PP}}";
|
protected static final String LABEL_APP = "\\LeftLabel{\\textrm A{\\small PP}}";
|
||||||
protected static final String LABEL_CONST = "\\LeftLabel{\\textrm C{\\small ONST}}";
|
protected static final String LABEL_CONST = "\\LeftLabel{\\textrm C{\\small ONST}}";
|
||||||
protected static final String LABEL_VAR = "\\LeftLabel{\\textrm V{\\small AR}}";
|
protected static final String LABEL_VAR = "\\LeftLabel{\\textrm V{\\small AR}}";
|
||||||
@ -73,7 +71,6 @@ public final class LatexCreatorConstants {
|
|||||||
protected static final String FOR_ALL = "\\forall";
|
protected static final String FOR_ALL = "\\forall";
|
||||||
protected static final String MONO_TEXT = "\\texttt";
|
protected static final String MONO_TEXT = "\\texttt";
|
||||||
protected static final String BOLD_TEXT = "\\textbf";
|
protected static final String BOLD_TEXT = "\\textbf";
|
||||||
protected static final String TEXT = "\\text";
|
|
||||||
protected static final String RIGHT_ARROW = "\\rightarrow";
|
protected static final String RIGHT_ARROW = "\\rightarrow";
|
||||||
protected static final String INSTANTIATE_SIGN = "\\succeq";
|
protected static final String INSTANTIATE_SIGN = "\\succeq";
|
||||||
protected static final String LATEX_IN = "\\in";
|
protected static final String LATEX_IN = "\\in";
|
||||||
@ -86,7 +83,7 @@ public final class LatexCreatorConstants {
|
|||||||
protected static final String SPLIT_END = "\\end{split}";
|
protected static final String SPLIT_END = "\\end{split}";
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Not actually a LaTeX command, but understood by MathJax.
|
* Not actually a LaTeX command, but understood by MathJax / the browser.
|
||||||
*/
|
*/
|
||||||
protected static final String BREAK_ROW = "<br>";
|
protected static final String BREAK_ROW = "<br>";
|
||||||
}
|
}
|
||||||
|
@ -127,6 +127,14 @@ public class LatexCreatorConstraints implements StepVisitor {
|
|||||||
return numberGenerator.getNumbers();
|
return numberGenerator.getNumbers();
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Returns the latex code to display a single constraint:
|
||||||
|
* type1 = type2
|
||||||
|
*
|
||||||
|
* @param constraint the constraint
|
||||||
|
* @param mode latex creator mode (if MathJax, adds the step index to the constraint)
|
||||||
|
* @return the latex code
|
||||||
|
*/
|
||||||
public static String createSingleConstraint(Constraint constraint, LatexCreatorMode mode) {
|
public static String createSingleConstraint(Constraint constraint, LatexCreatorMode mode) {
|
||||||
String firstType = new LatexCreatorType(constraint.getFirstType(), mode).getLatex();
|
String firstType = new LatexCreatorType(constraint.getFirstType(), mode).getLatex();
|
||||||
String secondType = new LatexCreatorType(constraint.getSecondType(), mode).getLatex();
|
String secondType = new LatexCreatorType(constraint.getSecondType(), mode).getLatex();
|
||||||
@ -248,19 +256,28 @@ public class LatexCreatorConstraints implements StepVisitor {
|
|||||||
return latex;
|
return latex;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Main method of this class, creates the latex code for each step of the unification.
|
||||||
|
*
|
||||||
|
* @param constraintSets current constraint set (added to the latex)
|
||||||
|
* @return latex code for each step
|
||||||
|
*/
|
||||||
private List<String> generateUnification(String constraintSets) {
|
private List<String> generateUnification(String constraintSets) {
|
||||||
List<String> steps = new ArrayList<>();
|
List<String> steps = new ArrayList<>();
|
||||||
|
|
||||||
List<UnificationStep> unificationSteps = typeInferer.getUnificationSteps()
|
List<UnificationStep> unificationSteps = typeInferer.getUnificationSteps()
|
||||||
.orElseThrow(IllegalStateException::new);
|
.orElseThrow(IllegalStateException::new);
|
||||||
// store constraints of previous step to highlight changes
|
// store constraints of previous step to highlight changes
|
||||||
String[] previousConstraints = new String[0];
|
List<String> previousConstraints = new ArrayList<>();
|
||||||
|
|
||||||
for (int stepNum = 0; stepNum < unificationSteps.size(); stepNum++) {
|
for (int stepNum = 0; stepNum < unificationSteps.size(); stepNum++) {
|
||||||
UnificationStep step = unificationSteps.get(stepNum);
|
UnificationStep step = unificationSteps.get(stepNum);
|
||||||
List<String> constraints2 = new ArrayList<>();
|
List<String> constraints2 = new ArrayList<>();
|
||||||
Result<List<Substitution>, UnificationError> subs = step.getSubstitutions();
|
Result<List<Substitution>, UnificationError> subs = step.getSubstitutions();
|
||||||
Optional<UnificationError> error = Optional.empty();
|
Optional<UnificationError> error = Optional.empty();
|
||||||
if (subs.isError()) {
|
if (subs.isError()) {
|
||||||
|
// display previous step again
|
||||||
|
// and show the error message
|
||||||
error = Optional.of(subs.unwrapError());
|
error = Optional.of(subs.unwrapError());
|
||||||
step = unificationSteps.get(unificationSteps.size() - 2);
|
step = unificationSteps.get(unificationSteps.size() - 2);
|
||||||
subs = step.getSubstitutions();
|
subs = step.getSubstitutions();
|
||||||
@ -277,32 +294,37 @@ public class LatexCreatorConstraints implements StepVisitor {
|
|||||||
// if new constraints were created in this step, mark them
|
// if new constraints were created in this step, mark them
|
||||||
boolean markLastTwoConstraints = (stepNum != 0)
|
boolean markLastTwoConstraints = (stepNum != 0)
|
||||||
&& unificationSteps.get(stepNum - 1).getConstraints().size() < unificationConstraints.size();
|
&& unificationSteps.get(stepNum - 1).getConstraints().size() < unificationConstraints.size();
|
||||||
|
|
||||||
|
// render each constraint present in this step
|
||||||
if (!unificationConstraints.isEmpty()) {
|
if (!unificationConstraints.isEmpty()) {
|
||||||
latex.append(UNIFY + PAREN_LEFT + LATEX_CURLY_LEFT);
|
latex.append(UNIFY + PAREN_LEFT + LATEX_CURLY_LEFT);
|
||||||
}
|
}
|
||||||
for (int i = unificationConstraints.size() - 1; i >= 0; i--) {
|
for (int i = unificationConstraints.size() - 1; i >= 0; i--) {
|
||||||
latex.append(AMPERSAND);
|
latex.append(AMPERSAND);
|
||||||
StringBuilder sb = new StringBuilder();
|
StringBuilder sb = new StringBuilder();
|
||||||
|
boolean highligthingConstraint = false;
|
||||||
if (markError && i == 0) {
|
if (markError && i == 0) {
|
||||||
sb.append(CURLY_LEFT);
|
sb.append(CURLY_LEFT);
|
||||||
sb.append(COLOR_RED);
|
sb.append(COLOR_RED);
|
||||||
|
highligthingConstraint = true;
|
||||||
} else if (markLastTwoConstraints && (i < 2)) {
|
} else if (markLastTwoConstraints && (i < 2)) {
|
||||||
sb.append(CURLY_LEFT);
|
sb.append(CURLY_LEFT);
|
||||||
sb.append(COLOR_HIGHLIGHTED);
|
sb.append(COLOR_HIGHLIGHTED);
|
||||||
|
highligthingConstraint = true;
|
||||||
}
|
}
|
||||||
sb.append(new LatexCreatorType(unificationConstraints.get(i).getFirstType(), mode).getLatex());
|
sb.append(new LatexCreatorType(unificationConstraints.get(i).getFirstType(), mode).getLatex());
|
||||||
sb.append(EQUALS);
|
sb.append(EQUALS);
|
||||||
sb.append(new LatexCreatorType(unificationConstraints.get(i).getSecondType(), mode).getLatex());
|
sb.append(new LatexCreatorType(unificationConstraints.get(i).getSecondType(), mode).getLatex());
|
||||||
if ((markError && i == 0) || markLastTwoConstraints && (i < 2)) {
|
if (highligthingConstraint) {
|
||||||
sb.append(CURLY_RIGHT);
|
sb.append(CURLY_RIGHT);
|
||||||
}
|
}
|
||||||
constraints2.add(sb.toString());
|
constraints2.add(sb.toString());
|
||||||
int invIdx = unificationConstraints.size() - 1 - i;
|
int invIdx = unificationConstraints.size() - 1 - i;
|
||||||
// if this constraint was modified by the substitution
|
// if this constraint was modified by the substitution
|
||||||
if (invIdx < previousConstraints.length) {
|
if (invIdx < previousConstraints.size()) {
|
||||||
// perform the substitution "manually" and color the new type
|
// perform the substitution "manually" and color the new type
|
||||||
Substitution s = substitutions.get(substitutions.size() - 1);
|
Substitution s = substitutions.get(substitutions.size() - 1);
|
||||||
String original = previousConstraints[invIdx];
|
String original = previousConstraints.get(invIdx);
|
||||||
String originalType = new LatexCreatorType(s.getVariable(), mode).getLatex();
|
String originalType = new LatexCreatorType(s.getVariable(), mode).getLatex();
|
||||||
if (original.contains(originalType)) {
|
if (original.contains(originalType)) {
|
||||||
StringBuilder highlightedChange2 = new StringBuilder();
|
StringBuilder highlightedChange2 = new StringBuilder();
|
||||||
@ -326,8 +348,9 @@ public class LatexCreatorConstraints implements StepVisitor {
|
|||||||
constraints2.remove(constraints2.size() - 1);
|
constraints2.remove(constraints2.size() - 1);
|
||||||
latex.append(LATEX_CURLY_RIGHT + PAREN_RIGHT + LATEX_NEW_LINE);
|
latex.append(LATEX_CURLY_RIGHT + PAREN_RIGHT + LATEX_NEW_LINE);
|
||||||
}
|
}
|
||||||
previousConstraints = constraints2.toArray(new String[0]);
|
previousConstraints = constraints2;
|
||||||
|
|
||||||
|
// also render the substitutions
|
||||||
for (int i = substitutions.size() - 1; i >= 0; i--) {
|
for (int i = substitutions.size() - 1; i >= 0; i--) {
|
||||||
if (!unificationConstraints.isEmpty() || i != substitutions.size() - 1) {
|
if (!unificationConstraints.isEmpty() || i != substitutions.size() - 1) {
|
||||||
latex.append(CIRC);
|
latex.append(CIRC);
|
||||||
@ -343,6 +366,7 @@ public class LatexCreatorConstraints implements StepVisitor {
|
|||||||
latex.delete(latex.length() - LATEX_NEW_LINE.length(), latex.length());
|
latex.delete(latex.length() - LATEX_NEW_LINE.length(), latex.length());
|
||||||
latex.append(SPLIT_END);
|
latex.append(SPLIT_END);
|
||||||
latex.append(ALIGN_END + MATH_END);
|
latex.append(ALIGN_END + MATH_END);
|
||||||
|
// finally, display the error if there is one
|
||||||
error.ifPresent(unificationError -> latex.append(translationProvider.apply(unificationError)));
|
error.ifPresent(unificationError -> latex.append(translationProvider.apply(unificationError)));
|
||||||
steps.add(latex.toString());
|
steps.add(latex.toString());
|
||||||
}
|
}
|
||||||
|
@ -4,6 +4,13 @@ package edu.kit.typicalc.view.content.typeinferencecontent.latexcreator;
|
|||||||
* Used to switch between different LaTeX generation methods.
|
* Used to switch between different LaTeX generation methods.
|
||||||
*/
|
*/
|
||||||
public enum LatexCreatorMode {
|
public enum LatexCreatorMode {
|
||||||
|
/**
|
||||||
|
* This mode adds a few HTML classes and ids to the generated LaTeX to facilitate highlighting etc.
|
||||||
|
* See OVERVIEW.md in the view package for more details.
|
||||||
|
*/
|
||||||
MATHJAX,
|
MATHJAX,
|
||||||
|
/**
|
||||||
|
* Regular LaTeX mode. Doesn't use any MathJax extensions.
|
||||||
|
*/
|
||||||
NORMAL
|
NORMAL
|
||||||
}
|
}
|
||||||
|
@ -15,7 +15,6 @@ import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.La
|
|||||||
* @see Type
|
* @see Type
|
||||||
*/
|
*/
|
||||||
public class LatexCreatorType implements TypeVisitor {
|
public class LatexCreatorType implements TypeVisitor {
|
||||||
private final Type type;
|
|
||||||
private static final int MAX_LENGTH = 100000; // 100 KB
|
private static final int MAX_LENGTH = 100000; // 100 KB
|
||||||
private final LatexCreatorMode mode;
|
private final LatexCreatorMode mode;
|
||||||
|
|
||||||
@ -28,7 +27,6 @@ public class LatexCreatorType implements TypeVisitor {
|
|||||||
* @param type the type
|
* @param type the type
|
||||||
*/
|
*/
|
||||||
public LatexCreatorType(Type type, LatexCreatorMode mode) {
|
public LatexCreatorType(Type type, LatexCreatorMode mode) {
|
||||||
this.type = type;
|
|
||||||
this.mode = mode;
|
this.mode = mode;
|
||||||
type.accept(this);
|
type.accept(this);
|
||||||
}
|
}
|
||||||
|
@ -20,7 +20,7 @@ public class TreeNumberGenerator {
|
|||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Push the current index. Translates into the tree not doing anything in this step.
|
* Push the current index. This means that the tree will not change in this step.
|
||||||
*/
|
*/
|
||||||
protected void push() {
|
protected void push() {
|
||||||
if (current < 0) {
|
if (current < 0) {
|
||||||
@ -30,7 +30,7 @@ public class TreeNumberGenerator {
|
|||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Push an incremented index. Translates into the tree going to the next step.
|
* Push an incremented index. This advances the proof tree.
|
||||||
*/
|
*/
|
||||||
protected void incrementPush() {
|
protected void incrementPush() {
|
||||||
current++;
|
current++;
|
||||||
|
@ -139,7 +139,7 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
|
|||||||
}
|
}
|
||||||
|
|
||||||
private void onInfoIconClick() {
|
private void onInfoIconClick() {
|
||||||
Dialog infoDialog = new InfoDialog();
|
Dialog infoDialog = new SyntaxDialog();
|
||||||
infoDialog.open();
|
infoDialog.open();
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -9,10 +9,10 @@ import com.vaadin.flow.i18n.LocaleChangeObserver;
|
|||||||
/**
|
/**
|
||||||
* Component which contains information on the correct syntax of the term as well as the type assumptions.
|
* 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 SyntaxContent extends VerticalLayout implements LocaleChangeObserver {
|
||||||
private static final long serialVersionUID = 7193916603756938225L;
|
private static final long serialVersionUID = 7193916603756938225L;
|
||||||
|
|
||||||
private static final String GRAMMAR_ID = "input-syntax";
|
private static final String GRAMMAR_CLASS = "input-syntax";
|
||||||
|
|
||||||
private final Span termExplanation;
|
private final Span termExplanation;
|
||||||
private final Paragraph termSyntax;
|
private final Paragraph termSyntax;
|
||||||
@ -21,16 +21,16 @@ public class InfoContent extends VerticalLayout implements LocaleChangeObserver
|
|||||||
private final Paragraph typeSyntax;
|
private final Paragraph typeSyntax;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Creates a new InfoContent.
|
* Creates a new SyntaxContent.
|
||||||
*/
|
*/
|
||||||
public InfoContent() {
|
public SyntaxContent() {
|
||||||
termExplanation = new Span();
|
termExplanation = new Span();
|
||||||
termSyntax = new Paragraph();
|
termSyntax = new Paragraph();
|
||||||
assExplanation = new Span();
|
assExplanation = new Span();
|
||||||
typeExplanation = new Span();
|
typeExplanation = new Span();
|
||||||
typeSyntax = new Paragraph();
|
typeSyntax = new Paragraph();
|
||||||
termSyntax.setId(GRAMMAR_ID);
|
termSyntax.setClassName(GRAMMAR_CLASS);
|
||||||
typeSyntax.setId(GRAMMAR_ID);
|
typeSyntax.setClassName(GRAMMAR_CLASS);
|
||||||
add(termExplanation, termSyntax, assExplanation, typeExplanation, typeSyntax);
|
add(termExplanation, termSyntax, assExplanation, typeExplanation, typeSyntax);
|
||||||
}
|
}
|
||||||
|
|
@ -11,8 +11,8 @@ import com.vaadin.flow.component.orderedlayout.VerticalLayout;
|
|||||||
/**
|
/**
|
||||||
* 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/syntax-dialog.css")
|
||||||
public class InfoDialog extends Dialog {
|
public class SyntaxDialog extends Dialog {
|
||||||
private static final long serialVersionUID = 2914411566361539614L;
|
private static final long serialVersionUID = 2914411566361539614L;
|
||||||
|
|
||||||
/*
|
/*
|
||||||
@ -23,9 +23,9 @@ public class InfoDialog extends Dialog {
|
|||||||
private static final String CLOSE_ICON_CLASS = "close-icon";
|
private static final String CLOSE_ICON_CLASS = "close-icon";
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Creates new InfoDialog.
|
* Creates new SyntaxDialog.
|
||||||
*/
|
*/
|
||||||
protected InfoDialog() {
|
protected SyntaxDialog() {
|
||||||
H4 heading = new H4(getTranslation("root.inputSyntax"));
|
H4 heading = new H4(getTranslation("root.inputSyntax"));
|
||||||
HorizontalLayout infoHeader = new HorizontalLayout(heading);
|
HorizontalLayout infoHeader = new HorizontalLayout(heading);
|
||||||
Icon closeIcon = new Icon(VaadinIcon.CLOSE_SMALL);
|
Icon closeIcon = new Icon(VaadinIcon.CLOSE_SMALL);
|
||||||
@ -34,7 +34,7 @@ public class InfoDialog extends Dialog {
|
|||||||
infoHeader.setId(INFO_HEADER_ID);
|
infoHeader.setId(INFO_HEADER_ID);
|
||||||
infoHeader.add(closeIcon);
|
infoHeader.add(closeIcon);
|
||||||
|
|
||||||
VerticalLayout infoContent = new InfoContent();
|
VerticalLayout infoContent = new SyntaxContent();
|
||||||
infoContent.setId(INFO_CONTENT_ID);
|
infoContent.setId(INFO_CONTENT_ID);
|
||||||
|
|
||||||
add(infoHeader, infoContent);
|
add(infoHeader, infoContent);
|
@ -8,7 +8,7 @@ import com.vaadin.flow.component.orderedlayout.VerticalLayout;
|
|||||||
|
|
||||||
/**
|
/**
|
||||||
* Contains all predefined examples as buttons.
|
* Contains all predefined examples as buttons.
|
||||||
* Clicking on a button selects the example and allows the user to chose between various type assumptions.
|
* Clicking on a button selects the example and allows the user to choose between various type assumptions.
|
||||||
*/
|
*/
|
||||||
public class TermExampleContent extends VerticalLayout {
|
public class TermExampleContent extends VerticalLayout {
|
||||||
private static final long serialVersionUID = 2882744650931562239L;
|
private static final long serialVersionUID = 2882744650931562239L;
|
||||||
|
@ -75,7 +75,8 @@ root.helpShortcuts=<kbd>Strg</kbd> + <kbd>\u2190</kbd> = Erster Schritt<br>\
|
|||||||
root.helpHoverEffects=Durch das Hovern über den Typherleitungsbaum und die Unifikation können zusätzliche Informationen \
|
root.helpHoverEffects=Durch das Hovern über den Typherleitungsbaum und die Unifikation können zusätzliche Informationen \
|
||||||
angezeigt werden. Das Hovern über eine beliebige Variable im Typherleitungsbaum oder der Unifikation führt dazu, dass \
|
angezeigt werden. Das Hovern über eine beliebige Variable im Typherleitungsbaum oder der Unifikation führt dazu, dass \
|
||||||
alle Vorkommen dieser Variable farblich hervorgehoben werden. Beim Hovern über die Schrift einer beliebigen Regel im \
|
alle Vorkommen dieser Variable farblich hervorgehoben werden. Beim Hovern über die Schrift einer beliebigen Regel im \
|
||||||
Typherleitungsbaum wird die Regel allgemein und die Instanziierung aller vorkommenden Variablen angezeigt.
|
Typherleitungsbaum wird die Regel allgemein und die Instanziierung aller vorkommenden Variablen angezeigt. \
|
||||||
|
Außerdem wird der von diesem Schritt erzeugte Constraint hervorgehoben.
|
||||||
root.helpFirstStepButton=Je nach Stand der Algorithmusausführung ändert sich die Funktion des Knopfs. \
|
root.helpFirstStepButton=Je nach Stand der Algorithmusausführung ändert sich die Funktion des Knopfs. \
|
||||||
Wenn aktuell der Baum aufgebaut wird, springt die Anzeige nach Benutzen des Knopfs zurück zum ersten Schritt des \
|
Wenn aktuell der Baum aufgebaut wird, springt die Anzeige nach Benutzen des Knopfs zurück zum ersten Schritt des \
|
||||||
Typherleitungsbaums. Wenn bereits die Unifikation durchgeführt wird, springt die Anzeige nach Benutzen des Knopfs \
|
Typherleitungsbaums. Wenn bereits die Unifikation durchgeführt wird, springt die Anzeige nach Benutzen des Knopfs \
|
||||||
|
@ -72,7 +72,7 @@ root.helpShortcuts=<kbd>Ctrl</kbd> + <kbd>\u2190</kbd> = First step<br>\
|
|||||||
root.helpHoverEffects=Additional information can be displayed by hovering over the inference tree and the unification. \
|
root.helpHoverEffects=Additional information can be displayed by hovering over the inference tree and the unification. \
|
||||||
Hovering over an arbitrary variable in the tree or the unification highlights all occurences of this variable. Hovering \
|
Hovering over an arbitrary variable in the tree or the unification highlights all occurences of this variable. Hovering \
|
||||||
over the label of an inference rule in the tree displays the general scheme of the rule as well as the instantiation of \
|
over the label of an inference rule in the tree displays the general scheme of the rule as well as the instantiation of \
|
||||||
all occuring variables.
|
all occuring variables. Additionally the constraint added in that step is highlighted in the unification area above.
|
||||||
root.helpFirstStepButton=The function of the button depends on the current state of the algorithm. \
|
root.helpFirstStepButton=The function of the button depends on the current state of the algorithm. \
|
||||||
If the tree is currently being built up, clicking on the button shows the first step of the inference tree. \
|
If the tree is currently being 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 \
|
If the unification algorithm is already in progress, clicking on the button shows the last step of the inference \
|
||||||
|
@ -65,10 +65,6 @@ class LambdaParserTest {
|
|||||||
void complicatedTerm() {
|
void complicatedTerm() {
|
||||||
LambdaParser parser = new LambdaParser("(λx.λy.x y 5)(λz.z)(true)");
|
LambdaParser parser = new LambdaParser("(λx.λy.x y 5)(λz.z)(true)");
|
||||||
Result<LambdaTerm, ParseError> term = parser.parse();
|
Result<LambdaTerm, ParseError> term = parser.parse();
|
||||||
if (term.isError()) {
|
|
||||||
System.err.println(term.unwrapError());
|
|
||||||
System.err.println(term.unwrapError().getCause());
|
|
||||||
}
|
|
||||||
assertEquals(
|
assertEquals(
|
||||||
new AppTerm(
|
new AppTerm(
|
||||||
new AppTerm(
|
new AppTerm(
|
||||||
|
Loading…
Reference in New Issue
Block a user