Commit 980b2d83 authored by Arne Keller's avatar Arne Keller
Browse files

Various style improvements and fixes

- more documentation
- up to date screenshots
- SonarLint suggestions
parent 1def7789
Pipeline #170493 passed with stages
in 3 minutes and 54 seconds
......@@ -27,6 +27,16 @@ Do not worry if the debugger breaks at a `SilentExitException`. This is a Spring
After the application has started, you can view your it at http://localhost:8080/ in your browser.
You can now also attach break points in code for debugging purposes, by clicking next to a line number in any source file.
### Running tests
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
you will get a 100% match on the first attempt.)
## Technical documentation
Documentation on the application is contained in this file and the Javadocs in each source file.
A quick description of the UI layer can be found in `src/main/java/view/OVERVIEW.md`.
## Fuzzing with [JQF](https://github.com/rohanpadhye/JQF)
### [Zest](https://github.com/rohanpadhye/JQF/wiki/Fuzzing-with-Zest)
......
#slide-layout {
align-items: center;
justify-content: center;
padding: 0;
}
#slide-explanation {
......
#inference-rule-field {
.inference-rule-field {
display: flex;
align-items: center;
border: 2px solid #e8e8e8;
......
......@@ -141,7 +141,7 @@ public class LambdaLexer {
private Result<Token, ParseError> parseAtomToken(char c) {
// only allow ascii characters in variable names
if (Character.isLetter(c) && (int) c < 128) {
if (Character.isLetter(c) && c < 128) {
int startPos = pos;
// identifier or keyword
StringBuilder sb = new StringBuilder();
......@@ -149,8 +149,8 @@ public class LambdaLexer {
sb.append(term.charAt(pos));
advance();
} while (pos < term.length() && Character.isLetterOrDigit(term.charAt(pos))
&& (int) term.charAt(pos) < 128);
if (pos < term.length() && (int) term.charAt(pos) >= 128) {
&& term.charAt(pos) < 128);
if (pos < term.length() && term.charAt(pos) >= 128) {
return new Result<>(null,
ParseError.unexpectedCharacter2(term.charAt(pos), pos, term, errorType)
.expectedType(TokenType.VARIABLE));
......
......@@ -116,9 +116,9 @@ public class LambdaParser {
private Result<AbsTerm, ParseError> parseAbstraction() {
nextToken();
Result<VarTerm, ParseError> var = parseVar();
if (var.isError()) {
return new Result<>(var);
Result<VarTerm, ParseError> varTerm = parseVar();
if (varTerm.isError()) {
return varTerm.castError();
}
Optional<ParseError> next = expect(TokenType.DOT);
if (next.isPresent()) {
......@@ -126,9 +126,9 @@ public class LambdaParser {
}
Result<LambdaTerm, ParseError> body = parseTerm(false);
if (body.isError()) {
return new Result<>(body);
return body.castError();
}
return new Result<>(new AbsTerm(var.unwrap(), body.unwrap()));
return new Result<>(new AbsTerm(varTerm.unwrap(), body.unwrap()));
}
/**
......@@ -156,9 +156,9 @@ public class LambdaParser {
if (error.isPresent()) {
return new Result<>(null, error.get());
}
Result<VarTerm, ParseError> var = parseVar();
if (var.isError()) {
return new Result<>(var);
Result<VarTerm, ParseError> varTerm = parseVar();
if (varTerm.isError()) {
return new Result<>(varTerm);
}
error = expect(TokenType.EQUALS);
if (error.isPresent()) {
......@@ -176,7 +176,7 @@ public class LambdaParser {
if (body.isError()) {
return new Result<>(body);
}
return new Result<>(new LetTerm(var.unwrap(), def.unwrap(), body.unwrap()));
return new Result<>(new LetTerm(varTerm.unwrap(), def.unwrap(), body.unwrap()));
}
/**
......@@ -187,8 +187,8 @@ public class LambdaParser {
private Result<LambdaTerm, ParseError> parsePart() {
switch (token.getType()) {
case VARIABLE:
Result<VarTerm, ParseError> var = parseVar();
return new Result<>(var.unwrap()); // variable token can always be parsed
Result<VarTerm, ParseError> varTerm = parseVar();
return new Result<>(varTerm.unwrap()); // variable token can always be parsed
case LAMBDA:
return new Result<>(parseAbstraction());
case LET:
......
......@@ -44,9 +44,9 @@ public class TypeAssumptionParser {
Matcher typeVariableMatcher = TYPE_VARIABLE_PATTERN.matcher(text);
if (typeVariableMatcher.matches()) {
int typeVariableIndex = Integer.parseInt(typeVariableMatcher.group(1));
TypeVariable var = new TypeVariable(TypeVariableKind.USER_INPUT, typeVariableIndex);
var.setUniqueIndex(typeVariableUniqueIndex);
return var;
TypeVariable variable = new TypeVariable(TypeVariableKind.USER_INPUT, typeVariableIndex);
variable.setUniqueIndex(typeVariableUniqueIndex);
return variable;
} else {
return new NamedType(text);
}
......@@ -159,8 +159,8 @@ public class TypeAssumptionParser {
TypeVariable v = new TypeVariable(TypeVariableKind.USER_INPUT, i);
v.setUniqueIndex(typeVariableUniqueIndex);
for (TypeVariable var : quantifiedVariables) {
if (var.equals(v)) {
for (TypeVariable variable : quantifiedVariables) {
if (variable.equals(v)) {
return new Result<>(null,
ParseError.unexpectedToken(currentToken, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR)
.additionalInformation(AdditionalInformation.DUPLICATETYPE));
......
......@@ -13,18 +13,18 @@ import java.util.Set;
* Representation of an abstraction term with its two sub-lambda terms.
*/
public class AbsTerm extends LambdaTerm {
private final VarTerm var;
private final VarTerm varTerm;
private final LambdaTerm body;
/**
* Initializes a new abstraction term with the variable bound
* by the abstraction and the lambda term of the abstraction.
*
* @param var the variable bound by the abstraction
* @param varTerm the variable bound by the abstraction
* @param body the lambda term of the abstraction
*/
public AbsTerm(VarTerm var, LambdaTerm body) {
this.var = var;
public AbsTerm(VarTerm varTerm, LambdaTerm body) {
this.varTerm = varTerm;
this.body = body;
}
......@@ -34,7 +34,7 @@ public class AbsTerm extends LambdaTerm {
* @return the variable of this abstraction
*/
public VarTerm getVariable() {
return var;
return varTerm;
}
/**
......@@ -54,7 +54,7 @@ public class AbsTerm extends LambdaTerm {
@Override
public Set<VarTerm> getFreeVariables() {
Set<VarTerm> set = new HashSet<>(this.body.getFreeVariables());
set.remove(this.var);
set.remove(this.varTerm);
return set;
}
......@@ -70,7 +70,7 @@ public class AbsTerm extends LambdaTerm {
@Override
public String toString() {
return "λ" + var + "." + body;
return "λ" + varTerm + "." + body;
}
@Override
......@@ -82,11 +82,11 @@ public class AbsTerm extends LambdaTerm {
return false;
}
AbsTerm absTerm = (AbsTerm) o;
return Objects.equals(var, absTerm.var) && Objects.equals(body, absTerm.body);
return Objects.equals(varTerm, absTerm.varTerm) && Objects.equals(body, absTerm.body);
}
@Override
public int hashCode() {
return Objects.hash(var, body);
return Objects.hash(varTerm, body);
}
}
......@@ -55,9 +55,11 @@ public class ScopingVisitor implements TermVisitor {
@Override
public void visit(IntegerTerm intTerm) {
/* constant term doesn't need to be scoped */
}
@Override
public void visit(BooleanTerm boolTerm) {
/* constant term doesn't need to be scoped */
}
}
......@@ -47,7 +47,7 @@ public class TypeAbstraction {
public TypeAbstraction(Type type, Map<VarTerm, TypeAbstraction> typeAssumptions) {
this.type = type;
Set<TypeVariable> varsToBeQuantified = type.getFreeTypeVariables();
typeAssumptions.forEach((var, abs) -> varsToBeQuantified.removeAll(abs.getFreeTypeVariables()));
typeAssumptions.forEach((variable, abs) -> varsToBeQuantified.removeAll(abs.getFreeTypeVariables()));
this.quantifiedVariables = new TreeSet<>(varsToBeQuantified);
}
......@@ -60,9 +60,9 @@ public class TypeAbstraction {
*/
public Type instantiate(TypeVariableFactory typeVarFactory) {
Type instantiatedType = this.type;
for (TypeVariable var : this.quantifiedVariables) {
for (TypeVariable variable : this.quantifiedVariables) {
TypeVariable newVariable = typeVarFactory.nextTypeVariable();
instantiatedType = instantiatedType.substitute(var, newVariable);
instantiatedType = instantiatedType.substitute(variable, newVariable);
}
return instantiatedType;
}
......
......@@ -47,10 +47,20 @@ public class TypeVariable extends Type implements Comparable<TypeVariable> {
return index;
}
/**
* Set the unique index of this type variable.
* Note that the caller is responsible for setting this variable correctly.
*
* @param uniqueIndex the unique index
* @see edu.kit.typicalc.model.term.ScopingVisitor
*/
public void setUniqueIndex(int uniqueIndex) {
this.uniqueIndex = uniqueIndex;
}
/**
* @return the unique index of this type variable
*/
public int getUniqueIndex() {
return uniqueIndex;
}
......@@ -168,9 +178,9 @@ public class TypeVariable extends Type implements Comparable<TypeVariable> {
}
@Override
public int compareTo(TypeVariable var) {
public int compareTo(TypeVariable variable) {
return Comparator.comparing(TypeVariable::getKind)
.thenComparing(TypeVariable::getIndex)
.compare(this, var);
.compare(this, variable);
}
}
# Basic structure of the main application screen (TypeInferenceView, layout: MainViewImpl)
```
+--------------------------------------------------------------------------+
| UpperBar: language select, InputBar, help button |
| - InputBar: syntax button, input fields, character/example/submit button |
+--------------------------------------------------------------------------+
| |
| left, hidden by default: middle: right, visible by default: |
| TypeInferenceRules MathjaxUnification MathjaxExplanation |
| MathjaxProofTree |
| |
+--------------------------------------------------------------------------+
| ControlPanel: share button, first/previous/next/last buttons |
+--------------------------------------------------------------------------+
```
## Non-obvious architecture decisions
### Showing the proof tree step-by-step
In `mathjax-proof-tree.ts` the fully rendered MathJax output is analyzed and grouped into pieces.
Styles are applied such that only the final conclusion is initially visible.
When navigating to another step, the respective elements are styled to be visible/hidden.
Note: MathJax is only involved when initially rendering the full tree!
### Highlighting type variables + Tooltips on steps
See `mathjax-style-hacks.ts` for a detailed description of the first stage: capturing hover events (= the user moved
the mouse cursor over a relevant element). Note that the same method is used in `mathjax-proof-tree.ts` and
`mathjax-unification.ts` (where the event is just forwarded to the proof tree element).
If a type variable is targeted, a custom style definition is created that colors all instances of this variable
(see `mathjax-proof-tree.ts`, function `handleMouseEvent` for details). It is applied to both the proof tree element
and the unification element.
If a step label is targeted, a tooltip is rendered next to it (was very annoying to fine-tune).
### Different LaTeX created for MathJax / share dialog
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
LaTeX macros are unlikely to be defined in the user's environment).
Note that the actual content is the same for both "modes".
\ No newline at end of file
......@@ -45,7 +45,7 @@ public class ImageSlide extends Slide implements LocaleChangeObserver {
public void localeChange(LocaleChangeEvent event) {
slideLayout.removeAll();
explanation.setText(getTranslation(explanationKey));
slideLayout.add(new Image(getTranslation(imageKey), ""), explanation);
slideLayout.add(explanation, new Image(getTranslation(imageKey), ""));
}
}
......@@ -98,10 +98,8 @@ public class StartPageView extends VerticalLayout implements ControlPanelView, L
Slide slide4 = new ImageSlide("root.image4", "root.text4");
Slide slide5 = new ImageSlide("root.image5", "root.text5");
Slide slide6 = new ImageSlide("root.image6", "root.text6");
Slide slide7 = new ImageSlide("root.image7", "root.text7");
Slide slide8 = new ImageSlide("root.image8", "root.text8");
return new Carousel(slide0, slide1, slide2, slide3, slide4, slide5, slide6, slide7, slide8).withoutNavigation()
return new Carousel(slide0, slide1, slide2, slide3, slide4, slide5, slide6).withoutNavigation()
.withoutSwipe();
}
......
......@@ -59,12 +59,12 @@ public class ExplanationCreatorUnification {
/**
* Generates LaTeX code from the provided type inferer for the unification algorithm.
*
* @param typeInferer the TypeInfererInterface to create the LaTeX-code from
*
* @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 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
*/
......@@ -83,7 +83,7 @@ public class ExplanationCreatorUnification {
/**
* 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() {
......@@ -92,10 +92,10 @@ public class ExplanationCreatorUnification {
private void buildTexts(boolean isLetUnification) {
String initialPrefix = isLetUnification ? LET_KEY_PREFIX : KEY_PREFIX;
String letVariable = isLetUnification
String letVariableName = isLetUnification
? toLatex(new LatexCreatorTerm(this.letVariable.get(), mode).getLatex()) : "";
String constraintSet = toLatex(letCounterToLatex(CONSTRAINT_SET));
String finalText = provider.getTranslation(initialPrefix + "initial", locale, constraintSet, letVariable);
String finalText = provider.getTranslation(initialPrefix + "initial", locale, constraintSet, letVariableName);
unificationTexts.add(finalText);
createUnficationTexts();
......@@ -103,13 +103,13 @@ public class ExplanationCreatorUnification {
createMGU();
createFinalType(isLetUnification);
if (isLetUnification) {
createLetUnficiationFinish();
createLetUnificationFinish();
}
}
}
private void createLetUnficiationFinish() {
String typeAssumptions =
private void createLetUnificationFinish() {
String typeAssumptions =
typeAssumptionsToLatex(typeInferer.getFirstInferenceStep().getConclusion().getTypeAssumptions(), mode);
String letVariableLatex = toLatex(new LatexCreatorTerm(this.letVariable.get(), mode).getLatex());
String gamma = toLatex(GAMMA + APOSTROPHE);
......@@ -128,12 +128,11 @@ public class ExplanationCreatorUnification {
}
private String createTypeAbstraction(String typeAssumptions) {
return new StringBuilder(TYPE_ABSTRACTION + PAREN_LEFT + letCounterToLatex(SIGMA) + PAREN_LEFT).
append(new LatexCreatorType(typeInferer.getFirstInferenceStep().getConclusion().getType(), mode)
.getLatex()).
append("" + PAREN_RIGHT + COMMA + letCounterToLatex(SIGMA) + PAREN_LEFT).
append(typeAssumptions).
append("" + PAREN_RIGHT + PAREN_RIGHT).toString();
return TYPE_ABSTRACTION + PAREN_LEFT + letCounterToLatex(SIGMA) + PAREN_LEFT
+ new LatexCreatorType(typeInferer.getFirstInferenceStep().getConclusion().getType(), mode)
.getLatex()
+ PAREN_RIGHT + COMMA + letCounterToLatex(SIGMA) + PAREN_LEFT
+ typeAssumptions + PAREN_RIGHT + PAREN_RIGHT;
}
private void createFinalType(boolean isLetUnification) {
......
......@@ -103,10 +103,10 @@ public class LatexCreator implements StepVisitor {
return conclusion;
}
private String generateVarStepPremise(VarStep var) {
String assumptions = typeAssumptionsToLatex(var.getConclusion().getTypeAssumptions(), mode);
String term = new LatexCreatorTerm(var.getConclusion().getLambdaTerm(), mode).getLatex();
String type = generateTypeAbstraction(var.getTypeAbsInPremise(), mode);
private String generateVarStepPremise(VarStep varStep) {
String assumptions = typeAssumptionsToLatex(varStep.getConclusion().getTypeAssumptions(), mode);
String term = new LatexCreatorTerm(varStep.getConclusion().getLambdaTerm(), mode).getLatex();
String type = generateTypeAbstraction(varStep.getTypeAbsInPremise(), mode);
return PAREN_LEFT + assumptions + PAREN_RIGHT + PAREN_LEFT + term
+ PAREN_RIGHT + EQUALS + type;
}
......
......@@ -215,10 +215,10 @@ public class LatexCreatorConstraints implements StepVisitor {
private String createLetConstraints(List<Constraint> letConstraints) {
StringBuilder result = new StringBuilder();
letConstraints.forEach(constraint -> {
letConstraints.forEach(constraint ->
result.append(createSingleConstraint(constraint, mode))
.append(DOLLAR_SIGN).append(COMMA).append(DOLLAR_SIGN);
});
.append(DOLLAR_SIGN).append(COMMA).append(DOLLAR_SIGN)
);
if (!letConstraints.isEmpty()) {
// remove last comma and dollar signs
result.deleteCharAt(result.length() - 1);
......
......@@ -28,7 +28,7 @@ public class InferenceRuleField extends VerticalLayout implements LocaleChangeOb
/*
* IDs for the imported .css-file
*/
private static final String INFERENCE_RULE_FIELD_ID = "inference-rule-field";
private static final String INFERENCE_RULE_FIELD_CLASS = "inference-rule-field";
private static final String HEADER_ID = "inference-rule-header";
private static final String MAIN_ID = "inference-rule-content";
private static final String RULE_NAME_ID = "rule-name";
......@@ -64,7 +64,7 @@ public class InferenceRuleField extends VerticalLayout implements LocaleChangeOb
VerticalLayout content = new VerticalLayout(rule);
content.setId(MAIN_ID);
add(header, content);
setId(INFERENCE_RULE_FIELD_ID);
setClassName(INFERENCE_RULE_FIELD_CLASS);
}
@Override
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment