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-01-30 10:41:26 +01:00
commit 1b2f1a1cd6
43 changed files with 898 additions and 324 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
frontend/src/mathjax-adapter.ts
View File

@ -9,13 +9,11 @@ declare let window: {
};
export abstract class MathjaxAdapter extends LitElement {
protected execTypeset() {
protected execTypeset(shadowRoot: ShadowRoot | null) {
if (window.MathJax !== undefined) {
window.MathJax.typesetShadow(this.shadowRoot, () => this.calculateSteps());
window.MathJax.typesetShadow(shadowRoot, () => this.calculateSteps());
}
}
// @ts-ignore
render(): TemplateResult {
return html`<mjx-doc id="mjx-document"><mjx-head></mjx-head><mjx-body>
@ -25,14 +23,15 @@ export abstract class MathjaxAdapter extends LitElement {
protected abstract showStep(n: number): void;
protected abstract calculateSteps(): void;
protected calculateSteps(): void {
}
connectedCallback() {
super.connectedCallback();
if (window.MathJax === undefined || !window.MathJax.isInitialized) {
window.addEventListener('mathjax-initialized', () => this.execTypeset());
window.addEventListener('mathjax-initialized', () => this.execTypeset(this.shadowRoot));
} else {
this.execTypeset();
this.execTypeset(this.shadowRoot);
}
}
}

4
frontend/src/mathjax-display.ts
View File

@ -7,12 +7,8 @@ class MathjaxDisplay extends MathjaxAdapter {
return super.render();
}
protected showStep(_n: number): void {
}
protected calculateSteps(): void {
}
}
customElements.define('tc-display', MathjaxDisplay);

22
frontend/src/mathjax-unification.ts
View File

@ -1,17 +1,33 @@
import {MathjaxAdapter} from "./mathjax-adapter";
import {TemplateResult} from "lit-html";
import {html} from "lit-element";
class MathjaxUnification extends MathjaxAdapter {
private content: String = "Loading...";
private latex: String[] = [];
static get properties() {
return {
content: {type: String}
}
}
render(): TemplateResult {
return super.render();
return html`<mjx-doc id="mjx-document"><mjx-head></mjx-head><mjx-body>
<div id="tc-content">${this.content}</div>
</mjx-body></mjx-doc>`;
}
protected showStep(n: number): void {
this.content = this.latex[n];
this.updateComplete.then(() => this.execTypeset(this.shadowRoot));
protected showStep(_n: number): void {
}
protected calculateSteps(): void {
public setTex(tex: String): void {
console.log(tex);
this.latex.push(tex);
console.log(this.latex)
}
}

14
frontend/styles/view/main/drawer-content.css Normal file
View File

@ -0,0 +1,14 @@
#ruleContainer {
overflow: auto;
margin: 1px;
height: 100%;
max-width: 256px;
padding: 1.1em 0.5em 0.5em 0.5em;
}
#drawerContent {
padding: 0.5em 0;
width: 100%;
height: 100%;
align-items: center;
}

9
frontend/styles/view/main/help-dialog.css Normal file
View File

@ -0,0 +1,9 @@
#contentLayout {
height: 80vh;
}
#headingLayout {
width: 80vw;
align-items: center;
justify-content: center;
}

30
frontend/styles/view/main/inference-rule-field.css Normal file
View File

@ -0,0 +1,30 @@
#inferenceRuleField {
display: flex;
align-items: center;
border: 2px solid #e8e8e8;
border-radius: 5px;
box-shadow: 0 4px 8px 0 rgba(0, 0, 0, 0.2), 0 6px 20px 0 rgba(0, 0, 0, 0.19);
margin-top: 0.25em;
margin-bottom: 0.25em;
padding: 0px;
}
#headerField {
border-bottom: 2px solid #e8e8e8;
background-color: #f8f8f8;
align-items: center;
justify-content: center;
width: 100%;
padding: 0.5em 0em;
}
#ruleName {
margin: 1px;
}
#main {
align-items: center;
width: 100%;
margin: 0px;
padding-top: 0.2em;
}

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

@ -13,3 +13,7 @@
#inputField {
height: 2.3em;
}
#inputBar {
align-items: center;
}

6
frontend/styles/view/main/upper-bar.css
View File

@ -1,5 +1,7 @@
#header {
height: var(--lumo-size-xl);
width: 100%;
align-items: center;
}
#header img {
@ -16,7 +18,7 @@
cursor: pointer;
}
#icon {
#helpIcon {
margin-left: auto;
margin-right: 1em;
}
@ -33,7 +35,7 @@
@media (min-width: 1000px) {
#inputBar {
margin-left: 30em;
margin-left: 26em;
}
#viewTitle {

26
pom.xml
View File

@ -103,6 +103,17 @@
<version>3.8.1</version>
<scope>test</scope>
</dependency>
<dependency>
<groupId>org.springframework.boot</groupId>
<artifactId>spring-boot-starter-test</artifactId>
<scope>test</scope>
<exclusions>
<exclusion>
<groupId>org.junit.vintage</groupId>
<artifactId>junit-vintage-engine</artifactId>
</exclusion>
</exclusions>
</dependency>
<dependency>
<groupId>org.junit.jupiter</groupId>
@ -172,6 +183,21 @@
<artifactId>maven-surefire-plugin</artifactId>
<version>2.22.2</version>
</plugin>
<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-failsafe-plugin</artifactId>
<version>2.22.2</version>
<executions>
<execution>
<goals>
<goal>integration-test</goal>
</goals>
</execution>
</executions>
<configuration>
<trimStackTrace>false</trimStackTrace>
</configuration>
</plugin>
<plugin>
<groupId>org.jacoco</groupId>
<artifactId>jacoco-maven-plugin</artifactId>

19
src/main/java/edu/kit/typicalc/model/Constraint.java
View File

@ -2,6 +2,8 @@ package edu.kit.typicalc.model;
import edu.kit.typicalc.model.type.Type;
import java.util.Objects;
/**
* Constrains two types to be equal.
*/
@ -35,4 +37,21 @@ public class Constraint {
return b;
}
@Override
public boolean equals(Object o) {
if (this == o) {
return true;
}
if (o == null || getClass() != o.getClass()) {
return false;
}
Constraint that = (Constraint) o;
return (a.equals(that.a) && b.equals(that.b))
|| (a.equals(that.b) && b.equals(that.a));
}
@Override
public int hashCode() {
return Objects.hash(a, b);
}
}

24
src/main/java/edu/kit/typicalc/model/Substitution.java
View File

@ -3,6 +3,8 @@ package edu.kit.typicalc.model;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeVariable;
import java.util.Objects;
/**
* A substitution specifies that some type should be replaced by a different type.
*/
@ -36,4 +38,26 @@ public class Substitution {
Type getType() {
return b;
}
@Override
public String toString() {
return "Substitution[" + a + " => " + b + "]";
}
@Override
public boolean equals(Object o) {
if (this == o) {
return true;
}
if (o == null || getClass() != o.getClass()) {
return false;
}
Substitution that = (Substitution) o;
return a.equals(that.a) && b.equals(that.b);
}
@Override
public int hashCode() {
return Objects.hash(a, b);
}
}

15
src/main/java/edu/kit/typicalc/model/UnificationError.java
View File

@ -1,5 +1,18 @@
package edu.kit.typicalc.model;
/**
* Errors that can occur during unification.
*
* @see Unification
* @see UnificationStep
*/
public enum UnificationError {
INFINITE_TYPE
/**
* Unification would lead to an infinite type.
*/
INFINITE_TYPE,
/**
* Some {@link edu.kit.typicalc.model.type.NamedType} is not equal to another type.
*/
DIFFERENT_TYPES
}

7
src/main/java/edu/kit/typicalc/model/parser/LambdaLexer.java
View File

@ -108,6 +108,7 @@ public class LambdaLexer {
return new Result<>(t);
default:
if (Character.isLetter(c)) {
int startPos = pos;
// identifier
StringBuilder sb = new StringBuilder();
do {
@ -133,17 +134,17 @@ public class LambdaLexer {
type = TokenType.VARIABLE;
break;
}
return new Result<>(new Token(type, sb.toString(), pos));
return new Result<>(new Token(type, sb.toString(), startPos));
} else if (Character.isDigit(c)) {
int startPos = pos;
// number literal
StringBuilder sb = new StringBuilder();
do {
sb.append(term.charAt(pos));
advance();
} while (pos < term.length() && Character.isDigit(term.charAt(pos)));
return new Result<>(new Token(TokenType.NUMBER, sb.toString(), pos));
return new Result<>(new Token(TokenType.NUMBER, sb.toString(), startPos));
} else {
//throw new ParseException("Illegal character '" + term.charAt(pos) + "'");
return new Result<>(null, ParseError.UNEXPECTED_CHARACTER);
}
}

3
src/main/java/edu/kit/typicalc/model/parser/LambdaParser.java
View File

@ -58,10 +58,11 @@ public class LambdaParser {
* @param type the token type to compare the current token type to
*/
private Optional<ParseError> expect(TokenType type) {
Token lastToken = token;
TokenType current = token.getType();
Optional<ParseError> error = nextToken();
if (current != type) {
return Optional.of(ParseError.UNEXPECTED_TOKEN.withToken(token));
return Optional.of(ParseError.UNEXPECTED_TOKEN.withToken(lastToken));
}
return error;
}

21
src/main/java/edu/kit/typicalc/model/parser/Token.java
View File

@ -1,5 +1,7 @@
package edu.kit.typicalc.model.parser;
import java.util.Objects;
/**
* A token of the Prolog language.
*/
@ -73,6 +75,23 @@ public class Token {
@Override
public String toString() {
return type + "(\"" + text + "\")";
return type + "(\"" + text + "\")[" + pos + "]";
}
@Override
public boolean equals(Object o) {
if (this == o) {
return true;
}
if (o == null || getClass() != o.getClass()) {
return false;
}
Token token = (Token) o;
return pos == token.pos && type == token.type && Objects.equals(text, token.text);
}
@Override
public int hashCode() {
return Objects.hash(type, text, pos);
}
}

35
src/main/java/edu/kit/typicalc/model/term/TermVisitorTree.java
View File

@ -11,12 +11,13 @@ public interface TermVisitorTree {
* Returns an {@link edu.kit.typicalc.model.step.AppStep} suiting the given application (lambda term)
* to type-infer and the type assumptions to consider.
* Simultaneously assembles the tree's constraint list.
*
* @param appTerm the application (lambda term) to build the inference step structure for,
* i.e. the lambda term in the conclusion of the returned inference step
* i.e. the lambda term in the conclusion of the returned inference step
* @param typeAssumptions the type assumptions to consider,
* i.e. the type assumptions in the conclusion of the returned inference step
* i.e. the type assumptions in the conclusion of the returned inference step
* @param conclusionType the type that the lambda term in the conclusion
* of the returned inference step will be assigned
* of the returned inference step will be assigned
* @return an {@link edu.kit.typicalc.model.step.AppStep}
*/
InferenceStep visit(AppTerm appTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType);
@ -25,12 +26,13 @@ public interface TermVisitorTree {
* Returns an {@link edu.kit.typicalc.model.step.AbsStep} suiting the given abstraction (lambda term)
* to type-infer and the type assumptions to consider.
* Simultaneously assembles the tree's constraint list.
*
* @param absTerm the abstraction (lambda term) to build the inference step structure for,
* i.e. the lambda term in the conclusion of the returned inference step
* i.e. the lambda term in the conclusion of the returned inference step
* @param typeAssumptions the type assumptions to consider,
* i.e. the type assumptions in the conclusion of the returned inference step
* i.e. the type assumptions in the conclusion of the returned inference step
* @param conclusionType the type that the lambda term in the conclusion
* of the returned inference step will be assigned
* of the returned inference step will be assigned
* @return an {@link edu.kit.typicalc.model.step.AbsStep}
*/
InferenceStep visit(AbsTerm absTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType);
@ -39,12 +41,13 @@ public interface TermVisitorTree {
* Returns an {@link edu.kit.typicalc.model.step.LetStep} suiting the given let expression (lambda term)
* to type-infer and the type assumptions to consider.
* Simultaneously assembles the tree's constraint list.
*
* @param letTerm the let expression (lambda term) to build the inference step structure for,
* i.e. the lambda term in the conclusion of the returned inference step
* i.e. the lambda term in the conclusion of the returned inference step
* @param typeAssumptions the type assumptions to consider,
* i.e. the type assumptions in the conclusion of the returned inference step
* i.e. the type assumptions in the conclusion of the returned inference step
* @param conclusionType the type that the lambda term in the conclusion
* of the returned inference step will be assigned
* of the returned inference step will be assigned
* @return an {@link edu.kit.typicalc.model.step.LetStep}
*/
InferenceStep visit(LetTerm letTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType);
@ -53,12 +56,13 @@ public interface TermVisitorTree {
* Returns an {@link edu.kit.typicalc.model.step.ConstStep} suiting the given constant
* to type-infer and the type assumptions to consider.
* Simultaneously assembles the tree's constraint list.
*
* @param constTerm the constant to build the inference step structure for,
* i.e. the lambda term in the conclusion of the returned inference step
* i.e. the lambda term in the conclusion of the returned inference step
* @param typeAssumptions the type assumptions to consider,
* i.e. the type assumptions in the conclusion of the returned inference step
* i.e. the type assumptions in the conclusion of the returned inference step
* @param conclusionType the type that the lambda term in the conclusion
* of the returned inference step will be assigned
* of the returned inference step will be assigned
* @return an {@link edu.kit.typicalc.model.step.ConstStep}
*/
InferenceStep visit(ConstTerm constTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType);
@ -67,12 +71,13 @@ public interface TermVisitorTree {
* Returns an {@link edu.kit.typicalc.model.step.VarStep} suiting the given variable (lambda term)
* to type-infer and the type assumptions to consider.
* Simultaneously assembles the tree's constraint list.
*
* @param varTerm the variable (lambda term) to build the inference step structure for,
* i.e. the lambda term in the conclusion of the returned inference step
* i.e. the lambda term in the conclusion of the returned inference step
* @param typeAssumptions the type assumptions to consider,
* i.e. the type assumptions in the conclusion of the returned inference step
* i.e. the type assumptions in the conclusion of the returned inference step
* @param conclusionType the type that the lambda term in the conclusion
* of the returned inference step will be assigned
* of the returned inference step will be assigned
* @return an {@link edu.kit.typicalc.model.step.VarStep}
*/
InferenceStep visit(VarTerm varTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType)

40
src/main/java/edu/kit/typicalc/model/type/FunctionType.java
View File

@ -10,8 +10,8 @@ import java.util.Objects;
*/
public class FunctionType extends Type {
private Type parameter;
private Type output;
private final Type parameter;
private final Type output;
/**
* Initializes a new FunctionType with the given parameter and output types.
* @param parameter the type of this function’s parameter
@ -41,23 +41,7 @@ public class FunctionType extends Type {
*/
@Override
public FunctionType substitute(TypeVariable a, Type b) {
boolean first = false;
boolean second = false;
if (this.parameter.contains(a)) {
first = true;
}
if (this.output.contains(a)) {
second = true;
}
if (first && second) {
return new FunctionType(parameter.substitute(a, b), output.substitute(a, b));
} else if (first) {
return new FunctionType(parameter.substitute(a, b), output);
} else if (second) {
return new FunctionType(parameter, output.substitute(a, b));
} else {
return this;
}
return new FunctionType(parameter.substitute(a, b), output.substitute(a, b));
}
/**
@ -76,9 +60,9 @@ public class FunctionType extends Type {
* @param type the other type
* @return unification steps necessary, or an error if that is impossible
*/
@Override
public Result<UnificationActions, UnificationError> constrainEqualTo(Type type) {
//TODO
return null;
return type.constrainEqualToFunction(this);
}
/**
@ -87,9 +71,9 @@ public class FunctionType extends Type {
* @param type the function type
* @return unification steps necessary, or an error if that is impossible
*/
public Result<UnificationActions, UnificationError> constrainEqualToFunction(Type type) {
//TODO
return null;
@Override
public Result<UnificationActions, UnificationError> constrainEqualToFunction(FunctionType type) {
return UnificationUtil.functionFunction(this, type);
}
/**
@ -98,9 +82,9 @@ public class FunctionType extends Type {
* @param type the named type
* @return unification steps necessary, or an error if that is impossible
*/
@Override
public Result<UnificationActions, UnificationError> constrainEqualToNamedType(NamedType type) {
//TODO
return null;
return UnificationUtil.functionNamed(this, type);
}
/**
@ -109,9 +93,9 @@ public class FunctionType extends Type {
* @param type the type variable
* @return the unification steps necessary, or an error if that is impossible
*/
@Override
public Result<UnificationActions, UnificationError> constrainEqualToVariable(TypeVariable type) {
//TODO
return null;
return UnificationUtil.functionVariable(this, type);
}
/**

211
src/main/java/edu/kit/typicalc/model/type/NamedType.java
View File

@ -9,122 +9,121 @@ import java.util.Objects;
* Models a simple named type.
*/
public class NamedType extends Type {
/**
* boolean type
*/
public static final NamedType BOOLEAN = new NamedType("boolean");
/**
* int type
*/
public static final NamedType INT = new NamedType("int");
/**
* boolean type
*/
public static final NamedType BOOLEAN = new NamedType("boolean");
/**
* int type
*/
public static final NamedType INT = new NamedType("int");
private String name;
private final String name;
/**
* Initializes a new NamedType with the given name.
* @param name the name of this type
*/
public NamedType(String name) {
this.name = name;
}
/**
* Initializes a new NamedType with the given name.
* @param name the name of this type
*/
public NamedType(String name) {
this.name = name;
}
/**
* Returns the name of the named type.
* @return the name of this type
*/
public String getName() {
return name;
}
/**
* Returns the name of the named type.
* @return the name of this type
*/
public String getName() {
return name;
}
/**
* Checks whether some type occurs in this type.
* @param x the type to look for
* @return whether the specified type is equal to this type
*/
public boolean contains(Type x) {
return this.equals(x);
}
/**
* Checks whether some type occurs in this type.
* @param x the type to look for
* @return whether the specified type is equal to this type
*/
public boolean contains(Type x) {
return this.equals(x);
}
/**
* Substitutes a type variable for a different type.
* @param a the type to replace
* @param b the type to insert
* @return itself, or b if a is equal to this object
*/
@Override
public Type substitute(TypeVariable a, Type b) {
//TODO: Methode überhaupt sinnvoll?
return null;
}
/**
* Substitutes a type variable for a different type.
* @param a the type to replace
* @param b the type to insert
* @return itself, or b if a is equal to this object
*/
@Override
public Type substitute(TypeVariable a, Type b) {
return this;
}
/**
* Accepts a visitor.
* @param typeVisitor the visitor that wants to visit this
*/
@Override
public void accept(TypeVisitor typeVisitor) {
typeVisitor.visit(this);
}
/**
* Accepts a visitor.
* @param typeVisitor the visitor that wants to visit this
*/
@Override
public void accept(TypeVisitor typeVisitor) {
typeVisitor.visit(this);
}
/**
* Computes the necessary constraints (and substitution) to unify this type with
* another. This method uses the constrainEqualToNamedType method on the other
* type.
* @param type the other type
* @return unification steps necessary, or an error if that is impossible
*/
public Result<UnificationActions, UnificationError> constrainEqualTo(Type type) {
//TODO
return null;
}
/**
* Computes the necessary constraints (and substitution) to unify this type with
* another. This method uses the constrainEqualToNamedType method on the other
* type.
* @param type the other type
* @return unification steps necessary, or an error if that is impossible
*/
@Override
public Result<UnificationActions, UnificationError> constrainEqualTo(Type type) {
return type.constrainEqualToNamedType(this);
}
/**
* Computes the necessary constraints (and substitution) to unify this type with a
* function type.
* @param type the function type
* @return unification steps necessary, or an error if that is impossible
*/
public Result<UnificationActions, UnificationError> constrainEqualToFunction(Type type) {
//TODO
return null;
}
/**
* Computes the necessary constraints (and substitution) to unify this type with a
* function type.
* @param type the function type
* @return unification steps necessary, or an error if that is impossible
*/
@Override
public Result<UnificationActions, UnificationError> constrainEqualToFunction(FunctionType type) {
return UnificationUtil.functionNamed(type, this);
}
/**
* Computes the necessary constraints (and substitution) to unify this type with a
* named type.
* @param type the named type
* @return unification steps necessary, or an error if that is impossible
*/
public Result<UnificationActions, UnificationError> constrainEqualToNamedType(NamedType type) {
//TODO
return null;
}
/**
* Computes the necessary constraints (and substitution) to unify this type with a
* named type.
* @param type the named type
* @return unification steps necessary, or an error if that is impossible
*/
@Override
public Result<UnificationActions, UnificationError> constrainEqualToNamedType(NamedType type) {
return UnificationUtil.namedNamed(this, type);
}
/**
* Computes the necessary constraints (and substitution) to unify this type with a
* type variable.
* @param type the type variable
* @return the unification steps necessary, or an error if that is impossible
*/
public Result<UnificationActions, UnificationError> constrainEqualToVariable(TypeVariable type) {
//TODO
return null;
}
/**
* Computes the necessary constraints (and substitution) to unify this type with a
* type variable.
* @param type the type variable
* @return the unification steps necessary, or an error if that is impossible
*/
@Override
public Result<UnificationActions, UnificationError> constrainEqualToVariable(TypeVariable type) {
return UnificationUtil.variableNamed(type, this);
}
@Override
public boolean equals(Object o) {
if (this == o) {
return true;
}
if (o == null || getClass() != o.getClass()) {
return false;
}
NamedType namedType = (NamedType) o;
return Objects.equals(name, namedType.name);
}
@Override
public boolean equals(Object o) {
if (this == o) {
return true;
}
if (o == null || getClass() != o.getClass()) {
return false;
}
NamedType namedType = (NamedType) o;
return Objects.equals(name, namedType.name);
}
@Override
public int hashCode() {
return Objects.hash(name);
}
@Override
public int hashCode() {
return Objects.hash(name);
}
}

2
src/main/java/edu/kit/typicalc/model/type/Type.java
View File

@ -42,7 +42,7 @@ public abstract class Type {
* @param type the function type
* @return unification steps necessary, or an error if that is impossible
*/
public abstract Result<UnificationActions, UnificationError> constrainEqualToFunction(Type type);
public abstract Result<UnificationActions, UnificationError> constrainEqualToFunction(FunctionType type);
/**
* Computes the necessary constraints (and substitution) to unify this type with a

7
src/main/java/edu/kit/typicalc/model/type/TypeAbstraction.java
View File

@ -2,6 +2,7 @@ package edu.kit.typicalc.model.type;
import edu.kit.typicalc.model.TypeVariableFactory;
import java.util.Collections;
import java.util.List;
import java.util.Objects;
@ -11,8 +12,8 @@ import java.util.Objects;
*/
public class TypeAbstraction {
private Type type;
private List<TypeVariable> quantifiedVariables;
private final Type type;
private final List<TypeVariable> quantifiedVariables;
/**
* Initializes a new type abstraction with its type and the type variables bound by
* the for-all quantifier.
@ -31,7 +32,7 @@ public class TypeAbstraction {
*/
public TypeAbstraction(Type type) {
this.type = type;
this.quantifiedVariables = null;
this.quantifiedVariables = Collections.emptyList();
}
/**

28
src/main/java/edu/kit/typicalc/model/type/TypeVariable.java
View File

@ -56,6 +56,7 @@ public class TypeVariable extends Type {
* @param b the type to insert
* @return itself, or b if a is equal to this object
*/
@Override
public Type substitute(TypeVariable a, Type b) {
if (this.equals(a)) {
return b;
@ -64,6 +65,10 @@ public class TypeVariable extends Type {
}
}
/**
* Accepts a visitor.
* @param typeVisitor the visitor that wants to visit this
*/
public void accept(TypeVisitor typeVisitor) {
typeVisitor.visit(this);
}
@ -75,9 +80,9 @@ public class TypeVariable extends Type {
* @param type the other type
* @return unification steps necessary, or an error if that is impossible
*/
@Override
public Result<UnificationActions, UnificationError> constrainEqualTo(Type type) {
//TODO
return null;
return type.constrainEqualToVariable(this);
}
/**
@ -86,9 +91,9 @@ public class TypeVariable extends Type {
* @param type the function type
* @return unification steps necessary, or an error if that is impossible
*/
public Result<UnificationActions, UnificationError> constrainEqualToFunction(Type type) {
//TODO
return null;
@Override
public Result<UnificationActions, UnificationError> constrainEqualToFunction(FunctionType type) {
return UnificationUtil.functionVariable(type, this);
}
/**
@ -97,9 +102,9 @@ public class TypeVariable extends Type {
* @param type the named type
* @return unification steps necessary, or an error if that is impossible
*/
@Override
public Result<UnificationActions, UnificationError> constrainEqualToNamedType(NamedType type) {
//TODO
return null;
return UnificationUtil.variableNamed(this, type);
}
/**
@ -108,9 +113,14 @@ public class TypeVariable extends Type {
* @param type the type variable
* @return the unification steps necessary, or an error if that is impossible
*/
@Override
public Result<UnificationActions, UnificationError> constrainEqualToVariable(TypeVariable type) {
//TODO
return null;
return UnificationUtil.variableVariable(type, this);
}
@Override
public String toString() {
return "TypeVariable[" + kind + "_" + index + "]";
}
@Override

30
src/main/java/edu/kit/typicalc/model/type/TypeVisitor.java
View File

@ -4,21 +4,21 @@ package edu.kit.typicalc.model.type;
* Can be implemented to process Type objects.
*/
public interface TypeVisitor {
/**
* Visit a named type.
* @param named the type to be visited
*/
void visit(NamedType named);
/**
* Visit a named type.
* @param named the type to be visited
*/
void visit(NamedType named);
/**
* Visit a type variable
* @param variable the variable to be visited
*/
void visit(TypeVariable variable);
/**
* Visit a type variable
* @param variable the variable to be visited
*/
void visit(TypeVariable variable);
/**
* Visit a function.
* @param function the function to be visited
*/
void visit(FunctionType function);
/**
* Visit a function.
* @param function the function to be visited
*/
void visit(FunctionType function);
}

18
src/main/java/edu/kit/typicalc/model/type/UnificationActions.java
View File

@ -4,14 +4,15 @@ import edu.kit.typicalc.model.Constraint;
import edu.kit.typicalc.model.Substitution;
import java.util.Collection;
import java.util.Collections;
import java.util.Optional;
/**
* Models the necessary actions to process a constraint.
*/
public class UnificationActions {
private Collection<Constraint> constraints;
private Optional<Substitution> substitution;
private final Collection<Constraint> constraints;
private final Optional<Substitution> substitution;
/**
* Initializes this object using the provided constraints and substitution.
@ -23,6 +24,14 @@ public class UnificationActions {
this.substitution = substitution;
}
/**
* Initializes an empty object.
*/
protected UnificationActions() {
this.constraints = Collections.emptyList();
this.substitution = Optional.empty();
}
/**
* Getter for constraints
* @return the constraints stored in this object
@ -30,7 +39,10 @@ public class UnificationActions {
public Collection<Constraint> getConstraints() {
return constraints;
}
/**
* Getter for substitution
* @return the substitution stored in this object
*/
public Optional<Substitution> getSubstitution() {
return substitution;
}

60
src/main/java/edu/kit/typicalc/model/type/UnificationUtil.java Normal file
View File

@ -0,0 +1,60 @@
package edu.kit.typicalc.model.type;
import edu.kit.typicalc.model.Constraint;
import edu.kit.typicalc.model.Substitution;
import edu.kit.typicalc.model.UnificationError;
import edu.kit.typicalc.util.Result;
import java.util.Collections;
import java.util.List;
import java.util.Optional;
/**
* Utility class to avoid unification logic duplication in type methods.
*/
final class UnificationUtil {
// TODO: document class? implementation detail?
private UnificationUtil() {
}
static Result<UnificationActions, UnificationError> functionFunction(FunctionType a, FunctionType b) {
return new Result<>(new UnificationActions(List.of(
new Constraint(a.getParameter(), b.getParameter()),
new Constraint(a.getOutput(), b.getOutput())), Optional.empty()));
}
static Result<UnificationActions, UnificationError> functionNamed(FunctionType a, NamedType b) {
return new Result<>(null, UnificationError.DIFFERENT_TYPES);
}
static Result<UnificationActions, UnificationError> functionVariable(FunctionType a, TypeVariable b) {
if (a.contains(b)) {
return new Result<>(null, UnificationError.INFINITE_TYPE);
}
return new Result<>(new UnificationActions(Collections.emptyList(),
Optional.of(new Substitution(b, a))));
}
static Result<UnificationActions, UnificationError> variableNamed(TypeVariable a, NamedType b) {
return new Result<>(new UnificationActions(Collections.emptyList(),
Optional.of(new Substitution(a, b))));
}
static Result<UnificationActions, UnificationError> variableVariable(TypeVariable a, TypeVariable b) {
if (!a.equals(b)) {
return new Result<>(new UnificationActions(Collections.emptyList(),
Optional.of(new Substitution(a, b))));
} else {
return new Result<>(new UnificationActions());
}
}
static Result<UnificationActions, UnificationError> namedNamed(NamedType a, NamedType b) {
if (a != b) {
return new Result<>(null, UnificationError.DIFFERENT_TYPES);
} else {
return new Result<>(new UnificationActions());
}
}
}

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

@ -22,7 +22,8 @@ public class StartPageView extends VerticalLayout implements ControlPanelView {
private final Div content;
private final ControlPanel controlPanel;
MathjaxProofTree mjxPT;
MathjaxProofTree tree;
MathjaxUnification unification;
public StartPageView() {
// todo implement correctly
@ -35,18 +36,20 @@ public class StartPageView extends VerticalLayout implements ControlPanelView {
scroller.setScrollDirection(Scroller.ScrollDirection.BOTH);
setAlignItems(Alignment.CENTER);
add(scroller, controlPanel);
disableControlPanel();
// disableControlPanel();
createContent();
}
private void createContent() {
String[] strings = new String[]{"$\\tau_0$", "$\\tau_1$", "$\\tau_2$", "$\\tau_3$", "$\\tau_4$",
"$\\tau_5$", "$\\tau_6$", "$\\tau_7$", "$\\tau_8$", "$\\tau_9$", "$\\tau_{10}$", "$\\tau_{11}$",
"$\\tau_{12}$", "$\\tau_{13}$", "$\\tau_{14}$"};
content.add(new MathjaxDisplay(getTranslation("abs-rule")));
content.add(new MathjaxUnification("\\(conswwwwwwWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWW"
+ "WWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWW"
+ "WWWWWWWWWWWWWWWWWWWWWtraint test \\vdash \\)"));
mjxPT = new MathjaxProofTree(getTranslation("demo-tree"));
content.add(mjxPT);
unification = new MathjaxUnification(strings);
tree = new MathjaxProofTree(getTranslation("demo-tree"));
content.add(unification);
content.add(tree);
content.add(new MathjaxProofTree(getTranslation("demo-tree")));
content.add(new MathjaxProofTree(getTranslation("demo-tree")));
content.add(new MathjaxProofTree(getTranslation("demo-tree")));
@ -55,8 +58,8 @@ public class StartPageView extends VerticalLayout implements ControlPanelView {
private void disableControlPanel() {
// todo disable everything
// controlPanel.setEnabledFirstStep(false);
// controlPanel.setEnabledLastStep(false);
controlPanel.setEnabledFirstStep(false);
controlPanel.setEnabledLastStep(false);
controlPanel.setEnabledNextStep(false);
controlPanel.setEnabledPreviousStep(false);
controlPanel.setEnabledShareButton(false);
@ -66,21 +69,33 @@ public class StartPageView extends VerticalLayout implements ControlPanelView {
public void shareButton() {
}
private int currentStep = 0;
private void refreshElements(int currentStep) {
unification.showStep(currentStep);
tree.showStep(currentStep < tree.getStepCount() ? currentStep : tree.getStepCount() - 1);
}
@Override
public void firstStepButton() {
mjxPT.showStep(0);
currentStep = currentStep > tree.getStepCount() ? tree.getStepCount() - 1 : 0;
refreshElements(currentStep);
}
@Override
public void lastStepButton() {
mjxPT.showStep(5);
currentStep = currentStep < tree.getStepCount() - 1 ? tree.getStepCount() - 1 : unification.getStepCount() - 1;
refreshElements(currentStep);
}
@Override
public void nextStepButton() {
currentStep = currentStep < unification.getStepCount() - 1 ? currentStep + 1 : currentStep;
refreshElements(currentStep);
}
@Override
public void previousStepButton() {
currentStep = currentStep > 0 ? currentStep - 1 : currentStep;
refreshElements(currentStep);
}
}

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

@ -76,7 +76,7 @@ public class LatexCreator implements StepVisitor, TermVisitor, TypeVisitor {
/**
* @return the LaTeX-code for constraints nad unification
*/
protected String getUnification() {
protected String[] getUnification() {
return null;
} // todo implement
@ -88,7 +88,7 @@ public class LatexCreator implements StepVisitor, TermVisitor, TypeVisitor {
} // todo implement
private String conclusionToLatex(Conclusion conclusion) {
// todo implement
return "{some text}";
}

27
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxUnification.java
View File

@ -1,11 +1,8 @@
package edu.kit.typicalc.view.content.typeinferencecontent;
import com.vaadin.flow.component.ClientCallable;
import com.vaadin.flow.component.Tag;
import com.vaadin.flow.component.dependency.JsModule;
import com.vaadin.flow.component.html.Div;
import com.vaadin.flow.component.littemplate.LitTemplate;
import com.vaadin.flow.component.template.Id;
import edu.kit.typicalc.view.MathjaxAdapter;
/**
@ -17,33 +14,29 @@ import edu.kit.typicalc.view.MathjaxAdapter;
@JsModule("./src/mathjax-unification.ts")
public class MathjaxUnification extends LitTemplate implements MathjaxAdapter {
private int stepCount = -1;
@Id("tc-content")
private Div content;
private final String[] latex;
/**
* Creates a new HTML element that renders the constraints and unification and
* calculates the steps.
* @param latex the LaTeX-String to render with MathJax
* @param latex the LaTeX-String[] to render with MathJax
*/
public MathjaxUnification(String latex) {
content.add(latex);
}
@ClientCallable
private void setStepCount(int stepCount) {
this.stepCount = stepCount;
public MathjaxUnification(String[] latex) {
this.latex = latex;
for (String s : latex) {
getElement().callJsFunction("setTex", s);
}
showStep(0);
}
@Override
public int getStepCount() {
return this.stepCount;
return this.latex.length;
}
@Override
public void showStep(int n) {
// todo implement
getElement().callJsFunction("showStep", n);
}
@Override

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

@ -32,15 +32,10 @@ public class TypeInferenceView extends HorizontalLayout
}
private void buildView(TypeInfererInterface typeInferer) {
if (typeInferer == null) {
// todo throw exception
unification = new MathjaxUnification("\\vdash test");
tree = new MathjaxProofTree(getTranslation("demo-tree"));
} else {
LatexCreator lc = new LatexCreator(typeInferer);
unification = new MathjaxUnification(lc.getUnification());
tree = new MathjaxProofTree(lc.getTree());
}
// todo implement correctly
LatexCreator lc = new LatexCreator(typeInferer);
unification = new MathjaxUnification(lc.getUnification());
tree = new MathjaxProofTree(lc.getTree());
add(unification);
add(new Scroller(tree));
}
@ -50,32 +45,32 @@ public class TypeInferenceView extends HorizontalLayout
// todo implement
}
//todo implement correctly
private void refreshElements(int currentStep) {
unification.showStep(currentStep);
tree.showStep(currentStep < tree.getStepCount() ? currentStep : tree.getStepCount() - 1);
}
@Override
public void firstStepButton() {
currentStep = 0;
unification.showStep(currentStep);
tree.showStep(currentStep);
currentStep = currentStep > tree.getStepCount() ? tree.getStepCount() - 1 : 0;
refreshElements(currentStep);
}
@Override
public void lastStepButton() {
currentStep = unification.getStepCount() - 1;
unification.showStep(currentStep);
tree.showStep(tree.getStepCount() - 1);
currentStep = currentStep < tree.getStepCount() - 1 ? tree.getStepCount() - 1 : unification.getStepCount() - 1;
refreshElements(currentStep);
}
@Override
public void nextStepButton() {
currentStep++;
unification.showStep(currentStep);
tree.showStep(currentStep);
currentStep = currentStep < unification.getStepCount() - 1 ? currentStep + 1 : currentStep;
refreshElements(currentStep);
}
@Override
public void previousStepButton() {
currentStep--;
unification.showStep(currentStep);
tree.showStep(currentStep);
currentStep = currentStep > 0 ? currentStep - 1 : currentStep;
refreshElements(currentStep);
}
}

39
src/main/java/edu/kit/typicalc/view/main/DrawerContent.java
View File

@ -1,10 +1,45 @@
package edu.kit.typicalc.view.main;
import com.vaadin.flow.component.dependency.CssImport;
import com.vaadin.flow.component.html.H3;
import com.vaadin.flow.component.orderedlayout.VerticalLayout;
import com.vaadin.flow.i18n.LocaleChangeEvent;
import com.vaadin.flow.i18n.LocaleChangeObserver;
public class DrawerContent extends VerticalLayout {
@CssImport("./styles/view/main/drawer-content.css")
public class DrawerContent extends VerticalLayout implements LocaleChangeObserver {
private static final long serialVersionUID = -5751275682270653335L;
/*
* IDs for the imported CSS file
*/
private static final String RULE_CONTAINER_ID = "ruleContainer";
private static final String DRAWER_CONTENT_ID = "drawerContent";
private final H3 heading;
private final VerticalLayout ruleContainer;
public DrawerContent() {
//TODO implement
heading = new H3(getTranslation("root.inferenceRules"));
ruleContainer = new VerticalLayout();
ruleContainer.setId(RULE_CONTAINER_ID);
initRuleContainer();
add(heading, ruleContainer);
setId(DRAWER_CONTENT_ID);
}
private void initRuleContainer() {
//TODO just demo content, exchange with correct rules
ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule"));
ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule"));
ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule"));
ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule"));
ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule"));
}
@Override
public void localeChange(LocaleChangeEvent event) {
heading.setText(getTranslation("root.inferenceRules"));
}
}

9
src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java
View File

@ -11,12 +11,17 @@ import java.util.List;
import java.util.function.Consumer;
public class ExampleDialog extends Dialog implements LocaleChangeObserver {
private static final long serialVersionUID = 8718432784530464215L;
private static final List<String> EXAMPLES =
List.of("λx.x", "λx.λy.y x", "λx.λy.y (x x)", "let f = λx. g y y in f 3", "(λx.x x) (λx.x x)");
private final Paragraph instruction;
public ExampleDialog(Consumer<String> callback) {
VerticalLayout layout = new VerticalLayout();
layout.add(new Paragraph(getTranslation("root.selectExample")));
instruction = new Paragraph(getTranslation("root.selectExample"));
layout.add(instruction);
for (String term : EXAMPLES) {
Button button = new Button(term);
button.addClickListener(click -> callback.accept(term));
@ -27,6 +32,6 @@ public class ExampleDialog extends Dialog implements LocaleChangeObserver {
@Override
public void localeChange(LocaleChangeEvent event) {
// TODO
instruction.setText(getTranslation("root.selectExample"));
}
}

43
src/main/java/edu/kit/typicalc/view/main/HelpDialog.java Normal file
View File

@ -0,0 +1,43 @@
package edu.kit.typicalc.view.main;
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.orderedlayout.HorizontalLayout;
import com.vaadin.flow.component.orderedlayout.VerticalLayout;
import com.vaadin.flow.i18n.LocaleChangeEvent;
import com.vaadin.flow.i18n.LocaleChangeObserver;
@CssImport("./styles/view/main/help-dialog.css")
public class HelpDialog extends Dialog implements LocaleChangeObserver {
private static final long serialVersionUID = 4470277770276296164L;
/*
* IDs for the imported CSS file
*/
private static final String HEADING_LAYOUT_ID = "headingLayout";
private static final String CONTENT_LAYOUT_ID = "contentLayout";
private final H3 heading;
private final H5 inputSyntax;
public HelpDialog() {
final HorizontalLayout headingLayout = new HorizontalLayout();
heading = new H3(getTranslation("root.operatingHelp"));
headingLayout.setId(HEADING_LAYOUT_ID);
headingLayout.add(heading);
final VerticalLayout contentLayout = new VerticalLayout();
inputSyntax = new H5(getTranslation("root.inputSyntax"));
contentLayout.setId(CONTENT_LAYOUT_ID);
contentLayout.add(inputSyntax);
add(headingLayout, contentLayout);
}
@Override
public void localeChange(LocaleChangeEvent event) {
heading.setText(getTranslation("root.operatingHelp"));
inputSyntax.setText(getTranslation("root.inputSyntax"));
}
}

43
src/main/java/edu/kit/typicalc/view/main/InferenceRuleField.java
View File

@ -2,29 +2,58 @@ package edu.kit.typicalc.view.main;
import com.vaadin.flow.component.UI;
import com.vaadin.flow.component.button.Button;
import com.vaadin.flow.component.dependency.CssImport;
import com.vaadin.flow.component.dependency.JsModule;
import com.vaadin.flow.component.html.Div;
import com.vaadin.flow.component.html.H4;
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.i18n.LocaleChangeEvent;
import com.vaadin.flow.i18n.LocaleChangeObserver;
@CssImport("./styles/view/main/inference-rule-field.css")
@JsModule("./src/copy-to-clipboard.js")
public class InferenceRuleField extends Div implements LocaleChangeObserver {
public class InferenceRuleField extends VerticalLayout implements LocaleChangeObserver {
private static final long serialVersionUID = -8551851183297707985L;
/*
* Id's for the imported css-file
*/
private static final String INFERENCE_RULE_FIELD_ID = "inferenceRuleField";
private static final String HEADER_ID = "headerField";
private static final String MAIN_ID = "main";
private static final String RULE_NAME_ID = "ruleName";
private final String latex;
private final String nameKey;
private final Button copyButton;
private final H4 ruleName;
private final MathjaxDisplay rule;
public InferenceRuleField(final String latex, final String nameKey) {
this.latex = latex;
this.nameKey = nameKey;
this.copyButton = new Button(getTranslation("root.copyLatex"),
event -> UI.getCurrent().getPage().executeJs("window.copyToClipboard($0)", latex));
final HorizontalLayout header = new HorizontalLayout();
header.setId(HEADER_ID);
this.ruleName = new H4(getTranslation(nameKey));
ruleName.setId(RULE_NAME_ID);
header.add(ruleName);
final VerticalLayout main = new VerticalLayout();
main.setId(MAIN_ID);
this.copyButton = new Button(getTranslation("root.copyLatex"), new Icon(VaadinIcon.CLIPBOARD));
this.rule = new MathjaxDisplay(latex); //TODO scale, when method implemented
copyButton.addClickListener(event -> UI.getCurrent().getPage().executeJs("window.copyToClipboard($0)", latex));
main.add(rule, copyButton);
add(header, main);
setId(INFERENCE_RULE_FIELD_ID);
}
@Override
public void localeChange(LocaleChangeEvent event) {
copyButton.setText(getTranslation("root.copyLatex"));
//TODO use nameKey to change name of rule, when attribute is created
ruleName.setText(getTranslation(nameKey));
}
}

37
src/main/java/edu/kit/typicalc/view/main/InputBar.java
View File

@ -3,7 +3,8 @@ package edu.kit.typicalc.view.main;
import java.util.Optional;
import java.util.function.Consumer;
import com.vaadin.flow.component.textfield.TextArea;
import com.vaadin.flow.component.textfield.TextField;
import org.apache.commons.lang3.StringUtils;
import com.vaadin.componentfactory.Tooltip;
import com.vaadin.componentfactory.TooltipAlignment;
@ -14,7 +15,6 @@ import com.vaadin.flow.component.dependency.CssImport;
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.FlexComponent;
import com.vaadin.flow.component.orderedlayout.HorizontalLayout;
import com.vaadin.flow.i18n.LocaleChangeEvent;
import com.vaadin.flow.i18n.LocaleChangeObserver;
@ -24,37 +24,42 @@ import com.vaadin.flow.i18n.LocaleChangeObserver;
*/
@CssImport("./styles/view/main/input-bar.css")
public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
private static final long serialVersionUID = -6099700300418752958L;
/*
* Id's for the imported css-file
*/
private static final String INPUT_FIELD_ID = "inputField";
private static final String INPUT_BAR_ID = "inputBar";
private final Tooltip infoTooltip;
private final Icon infoIcon;
private final Button exampleButton;
private final Button lambdaButton;
private final TextArea inputField;
private final TextField inputField;
private final Button inferTypeButton;
/**
* Creates an InputBar with a Consumer-object to call the inferType()-method in UpperBar.
* The current user input is passed as the methods argument.
* The current user input is passed as the methods argument.
*
* @param callback Consumer to call the inferType()-method in UpperBar
*/
protected InputBar(final Consumer<String> callback) {
infoIcon = new Icon(VaadinIcon.INFO_CIRCLE);
// TODO: where is this tooltip supposed to show up?
infoTooltip = new Tooltip();
infoIcon = new Icon(VaadinIcon.INFO_CIRCLE);
// TODO: where is this tooltip supposed to show up? next to icon, currently not working
infoTooltip = new Tooltip(infoIcon, TooltipPosition.LEFT, TooltipAlignment.LEFT);
infoTooltip.add(new H5("Hallo"));
initInfoTooltip();
infoTooltip.attachToComponent(infoIcon);
infoTooltip.setPosition(TooltipPosition.BOTTOM);
infoTooltip.setAlignment(TooltipAlignment.TOP);
inputField = new TextArea();
inputField.setId("inputField");
inputField = new TextField();
inputField.setId(INPUT_FIELD_ID);
inputField.setClearButtonVisible(true);
//TODO seems to be the only solution to "immediately" parse backslash
inputField.addValueChangeListener(event -> {
if (inputField.getOptionalValue().isPresent()) {
String value = inputField.getValue();
value = value.replace("\\", "λ");
value = value.replace("\\", "λ"); //TODO exchange magic strings
inputField.setValue(value);
}
});
@ -63,8 +68,8 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
inferTypeButton = new Button(getTranslation("root.typeInfer"), event -> onTypeInferButtonClick(callback));
inferTypeButton.addThemeVariants(ButtonVariant.LUMO_PRIMARY);
add(infoIcon, infoTooltip, exampleButton, lambdaButton, inputField, inferTypeButton);
setAlignItems(FlexComponent.Alignment.CENTER);
add(infoTooltip, infoIcon, exampleButton, lambdaButton, inputField, inferTypeButton);
setId(INPUT_BAR_ID);
}
private void onTypeInferButtonClick(final Consumer<String> callback) {
@ -87,7 +92,7 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
}
private void initInfoTooltip() {
infoTooltip.add(new H5("Hallo"));
infoTooltip.add(new H5("Hallo"));
}
@Override

13
src/main/java/edu/kit/typicalc/view/main/MainViewImpl.java
View File

@ -9,6 +9,9 @@ import com.vaadin.flow.component.html.Span;
import com.vaadin.flow.component.notification.Notification;
import com.vaadin.flow.component.notification.Notification.Position;
import com.vaadin.flow.component.notification.NotificationVariant;
import com.vaadin.flow.component.orderedlayout.FlexComponent;
import com.vaadin.flow.component.orderedlayout.VerticalLayout;
import edu.kit.typicalc.model.ModelImpl;
import edu.kit.typicalc.model.TypeInfererInterface;
import edu.kit.typicalc.model.parser.ParseError;
@ -17,7 +20,7 @@ import edu.kit.typicalc.view.content.typeinferencecontent.TypeInferenceView;
/**
* Contains all the displayed components and builds the applications user interface (UI).
* Vaadins app layout provides the rough structure of the UI. Using this structure the UI always
* Vaadin's app layout provides the rough structure of the UI. Using this structure the UI always
* consists of an upper bar at the top of the screen and a drawer on the left side of
* the screen.
*/
@ -25,6 +28,7 @@ import edu.kit.typicalc.view.content.typeinferencecontent.TypeInferenceView;
@JsModule("./styles/shared-styles.js")
@JavaScript("./src/tex-svg-full.js")
public class MainViewImpl extends AppLayout implements MainView {
private static final long serialVersionUID = -2411433187835906976L;
/**
* Creates a new MainViewImpl.
@ -43,13 +47,16 @@ public class MainViewImpl extends AppLayout implements MainView {
@Override
public void displayError(final ParseError error) {
//TODO add error keys to bundle
//TODO add error keys to bundle
final VerticalLayout container = new VerticalLayout();
final Span errorText = new Span(getTranslation("root." + error.toString()));
final Notification errorNotification = new Notification();
final Button closeButton = new Button(getTranslation("root.close"), event -> errorNotification.close());
errorNotification.addThemeVariants(NotificationVariant.LUMO_ERROR);
errorNotification.add(errorText, closeButton);
container.add(errorText, closeButton);
container.setAlignItems(FlexComponent.Alignment.CENTER);
errorNotification.add(container);
errorNotification.setPosition(Position.MIDDLE);
errorNotification.open();
}

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

@ -4,27 +4,35 @@ import java.util.HashMap;
import com.vaadin.flow.component.applayout.DrawerToggle;
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.FlexComponent;
import com.vaadin.flow.component.orderedlayout.HorizontalLayout;
import com.vaadin.flow.i18n.LocaleChangeEvent;
import com.vaadin.flow.i18n.LocaleChangeObserver;
import edu.kit.typicalc.view.content.infocontent.StartPageView;
import edu.kit.typicalc.view.main.MainView.MainViewListener;
@CssImport("./styles/view/main/upper-bar.css")
/**
* Contains all the components constantly shown in the upper part of the webage.
*/
public class UpperBar extends HorizontalLayout implements LocaleChangeObserver {
@CssImport("./styles/view/main/upper-bar.css")
public class UpperBar extends HorizontalLayout {
private static final long serialVersionUID = -7344967027514015830L;
/*
* Id's for the imported css-file
*/
private static final String VIEW_TITLE_ID = "viewTitle";
private static final String INPUT_BAR_ID = "inputBar";
private static final String HELP_ICON_ID = "helpIcon";
private static final String UPPER_BAR_ID = "header";
private final H1 viewTitle;
private final InputBar inputBar;
private final Icon helpDialogIcon;
private final Icon helpIcon;
private final MainViewListener presenter;
private final transient MainViewListener presenter;
/**
* Initializes a new UpperBar with the provided mainViewListener.
@ -35,20 +43,18 @@ public class UpperBar extends HorizontalLayout implements LocaleChangeObserver {
this.presenter = presenter;
this.viewTitle = new H1(getTranslation("root.typicalc"));
viewTitle.setId("viewTitle");
this.inputBar = new InputBar(this::typeInfer);
inputBar.setId("inputBar");
this.helpDialogIcon = new Icon(VaadinIcon.QUESTION_CIRCLE);
helpDialogIcon.setId("icon");
viewTitle.addClickListener(event -> this.getUI().get().navigate(StartPageView.class));
add(new DrawerToggle(), viewTitle, inputBar, helpDialogIcon);
setId("header");
getThemeList().set("dark", true); // remove magic string
setWidthFull();
viewTitle.setId(VIEW_TITLE_ID);
this.inputBar = new InputBar(this::typeInfer);
inputBar.setId(INPUT_BAR_ID);
this.helpIcon = new Icon(VaadinIcon.QUESTION_CIRCLE);
helpIcon.addClickListener(event -> onHelpIconClick());
helpIcon.setId(HELP_ICON_ID);
add(new DrawerToggle(), viewTitle, inputBar, helpIcon);
setId(UPPER_BAR_ID);
getThemeList().set("dark", true); //TODO remove magic string
setSpacing(false);
setAlignItems(FlexComponent.Alignment.CENTER);
}
/**
@ -60,12 +66,8 @@ public class UpperBar extends HorizontalLayout implements LocaleChangeObserver {
presenter.typeInferLambdaString(lambdaString, new HashMap<>());
}
private void createHelpDialog() {
//TODO create help dialog here --> maybe move to separate class if too big
}
@Override
public void localeChange(LocaleChangeEvent event) {
// TODO Auto-generated method stub
}
private void onHelpIconClick() {
Dialog helpDialog = new HelpDialog();
helpDialog.open();
}
}

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

@ -5,6 +5,10 @@ root.lambda=\u03BB
root.examplebutton=📂
root.selectExample=Beispiel auswählen:
root.typeInfer=Typisieren
root.operatingHelp=Bedienhilfen
root.inputSyntax=Eingabe Syntax
root.inferenceRules=Ableitungsregeln
root.absRule=Abs-Regel
abs-rule=\
\\begin{prooftree}\

9
src/test/java/edu/kit/typicalc/model/parser/LambdaParserTest.java
View File

@ -9,6 +9,7 @@ import edu.kit.typicalc.model.term.IntegerTerm;
import edu.kit.typicalc.model.term.LambdaTerm;
import edu.kit.typicalc.model.term.LetTerm;
import edu.kit.typicalc.model.term.VarTerm;
import edu.kit.typicalc.model.parser.Token.TokenType;
import edu.kit.typicalc.util.Result;
import org.junit.jupiter.api.Test;
@ -85,12 +86,16 @@ class LambdaParserTest {
LambdaParser parser = new LambdaParser("");
assertEquals(ParseError.TOO_FEW_TOKENS, parser.parse().unwrapError());
parser = new LambdaParser("x)");
assertEquals(ParseError.UNEXPECTED_TOKEN, parser.parse().unwrapError());
ParseError error = parser.parse().unwrapError();
assertEquals(ParseError.UNEXPECTED_TOKEN, error);
assertEquals(new Token(TokenType.RP, ")", 1), error.getCause());
parser = new LambdaParser("??");
assertEquals(ParseError.UNEXPECTED_CHARACTER, parser.parse().unwrapError());
parser = new LambdaParser("123333333333333");
assertEquals(ParseError.UNEXPECTED_CHARACTER, parser.parse().unwrapError());
parser = new LambdaParser("x 123333333333333");
assertEquals(ParseError.UNEXPECTED_CHARACTER, parser.parse().unwrapError());
error = parser.parse().unwrapError();
assertEquals(ParseError.UNEXPECTED_CHARACTER, error);
assertEquals(new Token(TokenType.NUMBER, "123333333333333", 2), error.getCause());
}
}

11
src/test/java/edu/kit/typicalc/model/type/FunctionTypeTest.java
View File

@ -1,22 +1,11 @@
package edu.kit.typicalc.model.type;
import org.junit.jupiter.api.AfterEach;
import org.junit.jupiter.api.BeforeEach;
import org.junit.jupiter.api.Test;
import static org.junit.jupiter.api.Assertions.*;
class FunctionTypeTest {
@BeforeEach
void setUp() {
}
@AfterEach
void tearDown() {
}
@Test
void substitute() {
TypeVariable typeVariable1 = new TypeVariable(TypeVaribaleKind.USER_INPUT, 1);

77
src/test/java/edu/kit/typicalc/model/type/UnificationTest.java Normal file
View File

@ -0,0 +1,77 @@
package edu.kit.typicalc.model.type;
import edu.kit.typicalc.model.Constraint;
import edu.kit.typicalc.model.Substitution;
import edu.kit.typicalc.model.UnificationError;
import org.junit.jupiter.api.Test;
import java.util.Collection;
import static org.junit.jupiter.api.Assertions.assertEquals;
import static org.junit.jupiter.api.Assertions.assertTrue;
class UnificationTest {
@Test
void all() {
TypeVariable a1 = new TypeVariable(TypeVaribaleKind.TREE, 1);
TypeVariable a2 = new TypeVariable(TypeVaribaleKind.TREE, 2);
TypeVariable a3 = new TypeVariable(TypeVaribaleKind.TREE, 3);
FunctionType id = new FunctionType(a1, a1);
FunctionType fun = new FunctionType(a2, a3);
NamedType string = new NamedType("string");
NamedType object = new NamedType("object");
// Function constraints
UnificationError error = id.constrainEqualTo(a1).unwrapError();
assertEquals(UnificationError.INFINITE_TYPE, error);
UnificationActions actions = id.constrainEqualTo(a2).unwrap();
assertEquals(new Substitution(a2, id), actions.getSubstitution().get());
assertTrue(actions.getConstraints().isEmpty());
error = id.constrainEqualTo(string).unwrapError();
assertEquals(UnificationError.DIFFERENT_TYPES, error);
actions = id.constrainEqualTo(fun).unwrap();
assertTrue(actions.getSubstitution().isEmpty());
Collection<Constraint> constraints = actions.getConstraints();
assertEquals(2, constraints.size());
assertTrue(constraints.contains(new Constraint(a1, a2)));
assertTrue(constraints.contains(new Constraint(a1, a3)));
// Variable constraints
actions = a1.constrainEqualTo(a1).unwrap();
assertTrue(actions.getConstraints().isEmpty());
assertTrue(actions.getSubstitution().isEmpty());
actions = a1.constrainEqualTo(a2).unwrap();
assertTrue(actions.getConstraints().isEmpty());
assertEquals(new Substitution(a1, a2), actions.getSubstitution().get());
error = a1.constrainEqualTo(id).unwrapError();
assertEquals(UnificationError.INFINITE_TYPE, error);
actions = a2.constrainEqualTo(id).unwrap();
assertEquals(new Substitution(a2, id), actions.getSubstitution().get());
assertTrue(actions.getConstraints().isEmpty());
actions = a1.constrainEqualTo(string).unwrap();
assertTrue(actions.getConstraints().isEmpty());
assertEquals(new Substitution(a1, string), actions.getSubstitution().get());
// Named type constraints
actions = string.constrainEqualTo(string).unwrap();
assertTrue(actions.getConstraints().isEmpty());
assertTrue(actions.getSubstitution().isEmpty());
error = string.constrainEqualTo(object).unwrapError();
assertEquals(UnificationError.DIFFERENT_TYPES, error);
error = string.constrainEqualTo(id).unwrapError();
assertEquals(UnificationError.DIFFERENT_TYPES, error);
actions = string.constrainEqualTo(a1).unwrap();
assertTrue(actions.getConstraints().isEmpty());
assertEquals(new Substitution(a1, string), actions.getSubstitution().get());
}
}

27
src/test/java/edu/kit/typicalc/view/AbstractIT.java Normal file
View File

@ -0,0 +1,27 @@
package edu.kit.typicalc.view;
import org.junit.Before;
import org.junit.Rule;
import com.vaadin.testbench.IPAddress;
import com.vaadin.testbench.ScreenshotOnFailureRule;
import com.vaadin.testbench.TestBenchTestCase;
import org.openqa.selenium.firefox.FirefoxDriver;
/**
* Base class for all our integration tests, allowing us to change the applicable driver,
* test URL or other configurations in one place.
*/
public abstract class AbstractIT extends TestBenchTestCase {
@Rule
public ScreenshotOnFailureRule rule = new ScreenshotOnFailureRule(this,
true);
@Before
public void setUp() {
setDriver(new FirefoxDriver());
getDriver().get("http://127.0.0.1:8080");
}
}

93
src/test/java/edu/kit/typicalc/view/ScreenshotIT.java Normal file
View File

@ -0,0 +1,93 @@
package edu.kit.typicalc.view;
import static org.junit.Assert.assertTrue;
import java.io.File;
import java.io.IOException;
import edu.kit.typicalc.view.main.MainViewImpl;
import org.junit.Test;
import org.openqa.selenium.HasCapabilities;
import com.vaadin.testbench.Parameters;
import com.vaadin.testbench.commands.TestBenchCommandExecutor;
/**
* This example contains usage examples of screenshot comparison feature.
* <p>
*/
public class ScreenshotIT extends AbstractIT {
/**
* We'll want to perform some additional setup functions, so we override the
* setUp() method.
*/
@Override
public void setUp() {
super.setUp();
// Set a fixed viewport size so the screenshot is always the same
// resolution
testBench().resizeViewPortTo(1000, 500);
// Define the directory for reference screenshots and for error files
Parameters.setScreenshotReferenceDirectory("src/test/resources/screenshots");
Parameters.setScreenshotErrorDirectory("target/screenshot_errors");
}
@Test
public void initialView() throws Exception {
// Change this calculation after running the test once to see how errors
// in screenshots are verified.
// The output is placed in target/screenshot_errors
generateReferenceIfNotFound("initialView");
// Compare screen with reference image with id "oneplustwo" from the
// reference image directory. Reference image filenames also contain
// browser, version and platform.
assertTrue(
"Screenshot comparison for 'initialView' failed, see "
+ Parameters.getScreenshotErrorDirectory()
+ " for error images",
testBench().compareScreen("initialView"));
}
/**
* Generates a reference screenshot if no reference exists.
* <p>
* This method only exists for demonstration purposes. Normally you should
* perform this task manually after verifying that the screenshots look
* correct.
*
* @param referenceId
* the id of the reference image
* @throws IOException
*/
private void generateReferenceIfNotFound(String referenceId)
throws IOException {
String refName = ((TestBenchCommandExecutor) testBench())
.getReferenceNameGenerator().generateName(referenceId,
((HasCapabilities) getDriver()).getCapabilities());
File referenceFile = new File(
Parameters.getScreenshotReferenceDirectory(), refName + ".png");
if (referenceFile.exists()) {
return;
}
if (!referenceFile.getParentFile().exists()) {
referenceFile.getParentFile().mkdirs();
}
File errorFile = new File(Parameters.getScreenshotErrorDirectory(),
referenceFile.getName());
// Take a screenshot and move it to the reference location
testBench().compareScreen(referenceId);
errorFile.renameTo(referenceFile);
System.out.println("Created new reference file in " + referenceFile);
}
}

1
src/test/resources/checkstyle-suppressions.xml
View File

@ -5,5 +5,6 @@
<suppressions>
<suppress files="src/main/resources/*" checks=".*" />
<suppress files="src/test/resources/*" checks=".*" />
</suppressions>

5
src/test/resources/checkstyle.xml
View File

@ -8,6 +8,11 @@
<property name="severity" value="warning"/>
<module name="TreeWalker">
<property name="tabWidth" value="4"/>
<module name="RegexpSinglelineJava">
<property name="format" value="^\t"/>
<property name="message" value="Line has leading tab characters; indentation should be performed with spaces only."/>
<property name="ignoreComments" value="true"/>
</module>
<module name="JavadocType">
<property name="scope" value="package"/>
<property name="severity" value="info"/>