merge

package.json

@@ -16,7 +16,6 @@
     "@vaadin/vaadin-combo-box": "5.4.7",
     "@vaadin/vaadin-confirm-dialog": "1.3.0",
     "@vaadin/vaadin-context-menu": "4.5.0",
-    "@vaadin/vaadin-cookie-consent": "1.2.0",
     "@vaadin/vaadin-core-shrinkwrap": "18.0.5",
     "@vaadin/vaadin-crud": "1.3.0",
     "@vaadin/vaadin-custom-field": "1.3.0",
@@ -29,7 +28,6 @@
     "@vaadin/vaadin-icons": "4.3.2",
     "@vaadin/vaadin-item": "2.3.0",
     "@vaadin/vaadin-list-box": "1.4.0",
-    "@vaadin/vaadin-login": "1.2.0",
     "@vaadin/vaadin-lumo-styles": "1.6.0",
     "@vaadin/vaadin-material-styles": "1.3.2",
     "@vaadin/vaadin-menu-bar": "1.2.1",
@@ -37,16 +35,12 @@
     "@vaadin/vaadin-ordered-layout": "1.4.0",
     "@vaadin/vaadin-progress-bar": "1.3.0",
     "@vaadin/vaadin-radio-button": "1.5.1",
-    "@vaadin/vaadin-rich-text-editor": "1.3.0",
     "@vaadin/vaadin-select": "2.4.0",
     "@vaadin/vaadin-shrinkwrap": "18.0.5",
     "@vaadin/vaadin-split-layout": "4.3.0",
     "@vaadin/vaadin-tabs": "3.2.0",
     "@vaadin/vaadin-text-field": "2.8.2",
-    "@vaadin/vaadin-time-picker": "2.4.0",
-    "@vaadin/vaadin-upload": "4.4.1",
     "lit-element": "2.3.1",
-    "@vaadin/vaadin-date-time-picker": "1.4.0",
     "@vaadin/form": "./target/flow-frontend/form",
     "@vaadin/vaadin-avatar": "1.0.3",
     "open": "^7.2.1"
@@ -85,42 +79,33 @@
       "@vaadin/vaadin-icons": "4.3.2",
       "@vaadin/vaadin-split-layout": "4.3.0",
       "@vaadin/vaadin-combo-box": "5.4.7",
-      "@vaadin/vaadin-cookie-consent": "1.2.0",
       "@vaadin/vaadin-core-shrinkwrap": "18.0.5",
-      "@vaadin/vaadin-upload": "4.4.1",
       "@vaadin/vaadin-dialog": "2.5.2",
       "@vaadin/vaadin-select": "2.4.0",
       "@vaadin/vaadin-app-layout": "2.2.0",
       "@vaadin/vaadin-item": "2.3.0",
       "@vaadin/vaadin-board": "2.2.0",
       "@vaadin/vaadin-notification": "1.6.0",
-      "@vaadin/vaadin-charts": "7.0.0",
       "@vaadin/vaadin-grid-pro": "2.2.2",
       "@vaadin/vaadin-progress-bar": "1.3.0",
       "@vaadin/vaadin-shrinkwrap": "18.0.5",
       "@vaadin/vaadin-ordered-layout": "1.4.0",
-      "@vaadin/vaadin-login": "1.2.0",
       "@vaadin/vaadin-button": "2.4.0",
-      "@vaadin/vaadin-date-picker": "4.4.1",
       "@vaadin/vaadin-text-field": "2.8.2",
       "@vaadin/vaadin-menu-bar": "1.2.1",
       "@vaadin/vaadin-form-layout": "2.3.0",
-      "@vaadin/vaadin-accordion": "1.2.0",
       "@polymer/iron-list": "3.1.0",
       "@vaadin/vaadin-confirm-dialog": "1.3.0",
       "@vaadin/vaadin-list-box": "1.4.0",
       "@vaadin/vaadin-checkbox": "2.5.0",
       "@vaadin/vaadin-details": "1.2.0",
       "@polymer/iron-icon": "3.0.1",
-      "@vaadin/vaadin-time-picker": "2.4.0",
       "@vaadin/vaadin-context-menu": "4.5.0",
       "@vaadin/vaadin-tabs": "3.2.0",
       "@vaadin/vaadin-radio-button": "1.5.1",
       "@vaadin/vaadin-lumo-styles": "1.6.0",
       "@vaadin/vaadin-material-styles": "1.3.2",
-      "@vaadin/vaadin-rich-text-editor": "1.3.0",
       "@vaadin/vaadin-custom-field": "1.3.0",
-      "@vaadin/vaadin-date-time-picker": "1.4.0",
       "lit-element": "2.3.1",
       "@vaadin/vaadin-avatar": "1.0.3",
       "open": "^7.2.1"

pom.xml

@@ -50,7 +50,7 @@
             <snapshots>
                 <enabled>false</enabled>
             </snapshots>
-        </pluginRepository> 
+        </pluginRepository>
     </pluginRepositories>
 
     <dependencyManagement>

src/main/java/edu/kit/typicalc/model/Conclusion.java

@@ -1,5 +1,12 @@
 package edu.kit.typicalc.model;
 
+import edu.kit.typicalc.model.term.LambdaTerm;
+import edu.kit.typicalc.model.term.VarTerm;
+import edu.kit.typicalc.model.type.Type;
+import edu.kit.typicalc.model.type.TypeAbstraction;
+
+import java.util.Map;
+
 /**
  * Models the conclusion of an inference rule and consists of a list of type assumptions, a lambda term and a type.
  * This class is used in inference steps to represent the conclusion of that specific application of the inference rule.

src/main/java/edu/kit/typicalc/model/Constraint.java

@@ -1,5 +1,7 @@
 package edu.kit.typicalc.model;
 
+import edu.kit.typicalc.model.type.Type;
+
 /**
  * Constrains two types to be equal.
  */

src/main/java/edu/kit/typicalc/model/Substitution.java

@@ -1,5 +1,8 @@
 package edu.kit.typicalc.model;
 
+import edu.kit.typicalc.model.type.Type;
+import edu.kit.typicalc.model.type.TypeVariable;
+
 /**
  * A substitution specifies that some type should be replaced by a different type.
  */

src/main/java/edu/kit/typicalc/model/Tree.java

@@ -1,6 +1,13 @@
 package edu.kit.typicalc.model;
 
+import edu.kit.typicalc.model.step.InferenceStep;
+import edu.kit.typicalc.model.term.LambdaTerm;
+import edu.kit.typicalc.model.term.TermVisitor;
+import edu.kit.typicalc.model.term.VarTerm;
+import edu.kit.typicalc.model.type.TypeAbstraction;
+
 import java.util.List;
+import java.util.Map;
 
 /**
  * Models the proof tree formed when the type of a lambda term is inferred.

src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java

@@ -1,5 +1,8 @@
 package edu.kit.typicalc.model;
 
+import edu.kit.typicalc.model.type.Type;
+import edu.kit.typicalc.model.type.TypeVariable;
+
 import java.util.List;
 
 /**

src/main/java/edu/kit/typicalc/model/TypeInferer.java

@@ -1,8 +1,13 @@
 package edu.kit.typicalc.model;
 
 import edu.kit.typicalc.model.step.InferenceStep;
+import edu.kit.typicalc.model.term.LambdaTerm;
+import edu.kit.typicalc.model.term.VarTerm;
+import edu.kit.typicalc.model.type.Type;
+import edu.kit.typicalc.model.type.TypeAbstraction;
 
 import java.util.List;
+import java.util.Map;
 
 /**
  * The type inferer is responsible for the whole type inference of a given lambda term, taking

src/main/java/edu/kit/typicalc/model/TypeInfererInterface.java

@@ -1,6 +1,7 @@
 package edu.kit.typicalc.model;
 
 import edu.kit.typicalc.model.step.InferenceStep;
+import edu.kit.typicalc.model.type.Type;
 
 import java.util.List;
 

src/main/java/edu/kit/typicalc/model/TypeInfererLet.java

@@ -1,6 +1,11 @@
 package edu.kit.typicalc.model;
 
+import edu.kit.typicalc.model.term.LambdaTerm;
+import edu.kit.typicalc.model.term.VarTerm;
+import edu.kit.typicalc.model.type.TypeAbstraction;
+
 import java.util.List;
+import java.util.Map;
 
 /**
  * Instances of this subclass of TypeInferer are used to execute the sub-inference starting in let steps.

src/main/java/edu/kit/typicalc/model/TypeVariableFactory.java

@@ -1,5 +1,7 @@
 package edu.kit.typicalc.model;
 
+import edu.kit.typicalc.model.type.TypeVariable;
+
 /**
  * Provides unique type variables on demand.
  */

src/main/java/edu/kit/typicalc/model/UnificationStep.java

@@ -0,0 +1,4 @@
+package edu.kit.typicalc.model;
+
+public class UnificationStep {
+}

src/main/java/edu/kit/typicalc/model/parser/LambdaLexer.java

@@ -0,0 +1,114 @@
+package edu.kit.typicalc.model.parser;
+
+import edu.kit.typicalc.model.parser.Token.TokenType;
+import edu.kit.typicalc.util.Result;
+
+/**
+ * This class lexes a term given as String into tokens.
+ * Tokens are lexed one by one as requested by the parser.
+ */
+public class LambdaLexer {
+    /**
+     * The given term as a String
+     */
+    private final String term;
+    /**
+     * current position in the term
+     */
+    private int pos = 0;
+
+    /**
+     * Constructs a lexer that lexes the given term
+     * @param term the term to lex
+     */
+    public LambdaLexer(String term) {
+        this.term = term;
+    }
+
+    /**
+     * Advances the current char to the next char in the term.
+     */
+    private void advance() {
+        pos += 1;
+    }
+
+    /**
+     * Lexes and returns the next token.
+     * @return the next token
+     */
+    public Result<Token, ParseError> nextToken() {
+        while (pos < term.length() && Character.isWhitespace(term.charAt(pos))) {
+            advance();
+        }
+        if (pos >= term.length()) {
+            // term ended, return EOF
+            return new Result<>(new Token(TokenType.EOF, "", pos));
+        }
+        Token t;
+        char c = term.charAt(pos);
+        switch (c) {
+            // bunch of single-character tokens
+            case '.':
+                t = new Token(TokenType.DOT, ".", pos);
+                advance();
+                return new Result<>(t);
+            case '(':
+                t = new Token(TokenType.LP, "(", pos);
+                advance();
+                return new Result<>(t);
+            case ')':
+                t = new Token(TokenType.RP, ")", pos);
+                advance();
+                return new Result<>(t);
+            case '=':
+                t = new Token(TokenType.EQ, "=", pos);
+                advance();
+                return new Result<>(t);
+            case '\\':
+            case 'λ':
+                t = new Token(TokenType.LAMBDA, c+"", pos);
+                advance();
+                return new Result<>(t);
+            default:
+                if (Character.isLetter(c)) {
+                    // identifier
+                    StringBuilder sb = new StringBuilder();
+                    do {
+                        sb.append(term.charAt(pos));
+                        advance();
+                    } while (pos < term.length() && Character.isLetterOrDigit(term.charAt(pos)));
+                    String s = sb.toString();
+                    TokenType type;
+                    switch (s) {
+                        case "let":
+                            type = TokenType.LET;
+                            break;
+                        case "in":
+                            type = TokenType.IN;
+                            break;
+                        case "true":
+                            type = TokenType.TRUE;
+                            break;
+                        case "false":
+                            type = TokenType.FALSE;
+                            break;
+                        default:
+                            type = TokenType.VARIABLE;
+                            break;
+                    }
+                    return new Result<>(new Token(type, sb.toString(), pos));
+                } else if (Character.isDigit(c)) {
+                    // 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));
+                } else {
+                    //throw new ParseException("Illegal character '" + term.charAt(pos) + "'");
+                    return new Result<>(null, ParseError.UNEXPECTED_CHARACTER);
+                }
+        }
+    }
+}

src/main/java/edu/kit/typicalc/model/parser/LambdaParser.java

@@ -0,0 +1,171 @@
+package edu.kit.typicalc.model.parser;
+
+import edu.kit.typicalc.model.parser.Token.TokenType;
+import edu.kit.typicalc.model.term.AbsTerm;
+import edu.kit.typicalc.model.term.AppTerm;
+import edu.kit.typicalc.model.term.BooleanTerm;
+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.util.Result;
+
+import java.util.EnumSet;
+import java.util.Optional;
+import java.util.Set;
+
+public class LambdaParser {
+    /**
+     * lexer to translate a String into tokens
+     */
+    private final LambdaLexer lexer;
+    /**
+     * Next token to use while parsing.
+     * The following invariant holds:
+     * When calling a parseX method, token is the first token of X
+     * (as opposed to the last token of the previous construct).
+     */
+    private Token token;
+
+    private static final Set<TokenType> atomStartTokens
+            = EnumSet.of(TokenType.VARIABLE, TokenType.NUMBER, TokenType.TRUE,
+            TokenType.FALSE, TokenType.LP);
+
+    /**
+     * Constructs a parser with the specified String
+     * @param term String to parse
+     */
+    public LambdaParser(String term) {
+        this.lexer = new LambdaLexer(term);
+        nextToken();
+    }
+
+    /**
+     * Sets token to the next available token.
+     */
+    private Optional<ParseError> nextToken() {
+        Result<Token, ParseError> nextToken = lexer.nextToken();
+        if (nextToken.isError()) {
+            return Optional.of(nextToken.unwrapError());
+        }
+        token = nextToken.unwrap();
+        return Optional.empty();
+    }
+
+    /**
+     * Checks that the token type of current token matches the token type given as parameter.
+     * If successful, returns that token and advances to the next token.
+     * Returns false otherwise.
+     * @param type the token type to compare the current token type to
+     */
+    private boolean expect(TokenType type) {
+        TokenType current = token.getType();
+        nextToken(); // TODO: Fehlerbehandlung
+        return current == type;
+    }
+
+    /**
+     * Parses the String given in the constructor as a term.
+     * @return the term given by the String
+     */
+    public Result<LambdaTerm, ParseError> parse() {
+        Result<LambdaTerm, ParseError> t = parseTerm();
+        if (!expect(TokenType.EOF)) {
+            return new Result<>(null, ParseError.TOO_MANY_TOKENS);
+        }
+        return t;
+    }
+
+    /**
+     * Parses a term.
+     * @return the term, or an error
+     */
+    private Result<LambdaTerm, ParseError> parseTerm() {
+        switch (token.getType()) {
+            case LAMBDA:
+                Result<AbsTerm, ParseError> abs = parseAbstraction();
+                return new Result<>(abs.unwrap(), abs.unwrapError());
+            case LET:
+                Result<LetTerm, ParseError> let = parseLet();
+                return new Result<>(let.unwrap(), let.unwrapError());
+            default:
+                return parseApplication();
+        }
+    }
+
+    private Result<AbsTerm, ParseError> parseAbstraction() {
+        nextToken();
+        Result<VarTerm, ParseError> var = parseVar();
+        if (!expect(TokenType.DOT)) {
+            // TODO
+        }
+        Result<LambdaTerm, ParseError> body = parseTerm();
+        // TODO: Fehlerbehandlung
+        return new Result(new AbsTerm(var.unwrap(), body.unwrap()));
+    }
+
+    /**
+     * Parses an application or constructs of higher precedence.
+     * @return the term, or an error
+     */
+    private Result<LambdaTerm, ParseError> parseApplication() {
+        LambdaTerm left = parseAtom().unwrap(); // TODO: Fehlerbehandlung
+        while (atomStartTokens.contains(token.getType())) {
+            LambdaTerm atom = parseAtom().unwrap(); // TODO: Fehlerbehandlung
+            left = new AppTerm(left, atom);
+        }
+        return new Result<>(left);
+    }
+
+    private Result<LetTerm, ParseError> parseLet() {
+        // TODO: Fehlerbehandlung
+        expect(TokenType.LET);
+        VarTerm var = parseVar().unwrap();
+        expect(TokenType.EQ);
+        LambdaTerm def = parseTerm().unwrap();
+        expect(TokenType.IN);
+        LambdaTerm body = parseTerm().unwrap();
+        return new Result<>(new LetTerm(var, def, body));
+    }
+
+    /**
+     * Parses an atom (variable or number) or a parenthesised expression.
+     * @return the term
+     */
+    private Result<LambdaTerm, ParseError> parseAtom() {
+        switch (token.getType()) {
+            case VARIABLE:
+                Result<VarTerm, ParseError> var = parseVar();
+                return new Result<>(var.unwrap(), var.unwrapError());
+            case NUMBER:
+                String number = token.getText();
+                int n;
+                try {
+                    n = Integer.parseInt(number);
+                } catch (NumberFormatException e) {
+                    return new Result<>(null, ParseError.UNEXPECTED_CHARACTER);
+                }
+                nextToken();
+                return new Result<>(new IntegerTerm(n));
+            case TRUE:
+            case FALSE:
+                String boolText = token.getText();
+                boolean b = Boolean.parseBoolean(boolText);
+                nextToken();
+                return new Result<>(new BooleanTerm(b));
+            default:
+                expect(TokenType.LP);
+                Result<LambdaTerm, ParseError> term = parseTerm();
+                expect(TokenType.RP);
+                return term;
+        }
+    }
+
+    private Result<VarTerm, ParseError> parseVar() {
+        String s = token.getText();
+        if (!expect(TokenType.VARIABLE)) {
+            return new Result<>(null, ParseError.UNEXPECTED_TOKEN);
+        }
+        return new Result<>(new VarTerm(s));
+    }
+}

src/main/java/edu/kit/typicalc/model/parser/ParseError.java

@@ -0,0 +1,7 @@
+package edu.kit.typicalc.model.parser;
+
+public enum ParseError {
+    UNEXPECTED_TOKEN,
+    TOO_MANY_TOKENS,
+    UNEXPECTED_CHARACTER
+}

src/main/java/edu/kit/typicalc/model/parser/Token.java

@@ -0,0 +1,78 @@
+package edu.kit.typicalc.model.parser;
+
+/**
+ * A token of the Prolog language.
+ */
+public class Token {
+    /**
+     * Used to distinguish what kind of token we have.
+     * Most of them stand for exactly one character.
+     * VARIABLE and NUMBER have a regular expression associated with them.
+     * EOF is a special token to indicate that the end of file is reached.
+     */
+    enum TokenType {
+        LAMBDA, // λ or a backslash
+        VARIABLE, // [a-z][a-zA-Z0-9]* except "let" or "in" or constants
+        LET, // let
+        IN, // in
+        TRUE, // true
+        FALSE, // false
+        NUMBER, // [0-9]+
+        LP, // (
+        RP, // )
+        DOT, // .
+        EQ, // =
+        EOF // pseudo token if end of file is reached
+    }
+
+    /**
+     * token type of this Token
+     */
+    private final TokenType type;
+    /**
+     * the text of this token in the source code
+     */
+    private final String text;
+    private final int pos;
+
+    /**
+     * Constructs a token.
+     * @param type the token type
+     * @param text text of this token in the source code
+     * @param pos position this token begins
+     */
+    public Token(TokenType type, String text, int pos) {
+        this.type = type;
+        this.text = text;
+        this.pos = pos;
+    }
+
+    /**
+     * Returns the token type
+     * @return token type
+     */
+    public TokenType getType() {
+        return type;
+    }
+
+    /**
+     * Returns the text of this token in the source code
+     * @return text of this token in the source code
+     */
+    public String getText() {
+        return text;
+    }
+
+    /**
+     * Returns the position this token is in
+     * @return position this token is in
+     */
+    public int getPos() {
+        return pos;
+    }
+
+    @Override
+    public String toString() {
+        return type + "(\"" + text + "\")";
+    }
+}

src/main/java/edu/kit/typicalc/model/step/InferenceStep.java

@@ -15,7 +15,4 @@ public abstract class InferenceStep {
      */
     public abstract void accept(StepVisitor stepVisitor);
 
-}
+}
-
-
-

src/main/java/edu/kit/typicalc/model/term/AbsTerm.java

@@ -0,0 +1,7 @@
+package edu.kit.typicalc.model.term;
+
+public class AbsTerm extends LambdaTerm {
+	public AbsTerm(VarTerm var, LambdaTerm body) {
+		// TODO
+	}
+}

src/main/java/edu/kit/typicalc/model/term/AppTerm.java

@@ -0,0 +1,6 @@
+package edu.kit.typicalc.model.term;
+
+public class AppTerm extends LambdaTerm {
+	public AppTerm(LambdaTerm left, LambdaTerm atom) {
+	}
+}

src/main/java/edu/kit/typicalc/model/term/BooleanTerm.java

@@ -0,0 +1,7 @@
+package edu.kit.typicalc.model.term;
+
+public class BooleanTerm extends ConstTerm {
+	public BooleanTerm(boolean value) {
+		// TODO
+	}
+}

src/main/java/edu/kit/typicalc/model/term/ConstTerm.java

@@ -0,0 +1,4 @@
+package edu.kit.typicalc.model.term;
+
+public class ConstTerm extends LambdaTerm {
+}

src/main/java/edu/kit/typicalc/model/term/IntegerTerm.java

@@ -0,0 +1,7 @@
+package edu.kit.typicalc.model.term;
+
+public class IntegerTerm extends ConstTerm {
+	public IntegerTerm(int value) {
+		// TODO
+	}
+}

src/main/java/edu/kit/typicalc/model/term/LambdaTerm.java

@@ -0,0 +1,4 @@
+package edu.kit.typicalc.model.term;
+
+public class LambdaTerm {
+}

src/main/java/edu/kit/typicalc/model/term/LetTerm.java

@@ -0,0 +1,6 @@
+package edu.kit.typicalc.model.term;
+
+public class LetTerm extends LambdaTerm {
+	public LetTerm(VarTerm var, LambdaTerm def, LambdaTerm body) {
+	}
+}

src/main/java/edu/kit/typicalc/model/term/TermVisitor.java

@@ -0,0 +1,4 @@
+package edu.kit.typicalc.model.term;
+
+public interface TermVisitor {
+}

src/main/java/edu/kit/typicalc/model/term/VarTerm.java

@@ -0,0 +1,7 @@
+package edu.kit.typicalc.model.term;
+
+public class VarTerm extends LambdaTerm {
+	public VarTerm(String s) {
+		super();
+	}
+}

src/main/java/edu/kit/typicalc/model/type/Type.java

@@ -0,0 +1,4 @@
+package edu.kit.typicalc.model.type;
+
+public abstract class Type {
+}

src/main/java/edu/kit/typicalc/model/type/TypeAbstraction.java

@@ -0,0 +1,4 @@
+package edu.kit.typicalc.model.type;
+
+public class TypeAbstraction {
+}

src/main/java/edu/kit/typicalc/model/type/TypeVariable.java

@@ -0,0 +1,4 @@
+package edu.kit.typicalc.model.type;
+
+public class TypeVariable {
+}

src/main/java/edu/kit/typicalc/util/Result.java

@@ -0,0 +1,28 @@
+package edu.kit.typicalc.util;
+
+public class Result<T, E> {
+	private final T value;
+	private final E error;
+
+	public Result(T value) {
+		this.value = value;
+		this.error = null;
+	}
+
+	public Result(T value, E error) { // TODO: Java does not allow both constructors otherwise
+		this.value = value;
+		this.error = error;
+	}
+
+	public boolean isError() {
+		return error != null;
+	}
+
+	public T unwrap() {
+		return value;
+	}
+
+	public E unwrapError() {
+		return error;
+	}
+}