diff --git a/package.json b/package.json index 0c29c51..0ab1f39 100644 --- a/package.json +++ b/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" diff --git a/pom.xml b/pom.xml index 335834e..bd5d430 100644 --- a/pom.xml +++ b/pom.xml @@ -50,7 +50,7 @@ false - + diff --git a/src/main/java/edu/kit/typicalc/model/Conclusion.java b/src/main/java/edu/kit/typicalc/model/Conclusion.java index 6006dd8..763667d 100644 --- a/src/main/java/edu/kit/typicalc/model/Conclusion.java +++ b/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. diff --git a/src/main/java/edu/kit/typicalc/model/Constraint.java b/src/main/java/edu/kit/typicalc/model/Constraint.java index 226c41a..34c9a49 100644 --- a/src/main/java/edu/kit/typicalc/model/Constraint.java +++ b/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. */ diff --git a/src/main/java/edu/kit/typicalc/model/Substitution.java b/src/main/java/edu/kit/typicalc/model/Substitution.java index e922a3f..65f6713 100644 --- a/src/main/java/edu/kit/typicalc/model/Substitution.java +++ b/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. */ diff --git a/src/main/java/edu/kit/typicalc/model/Tree.java b/src/main/java/edu/kit/typicalc/model/Tree.java index b2eb221..6c7eb80 100644 --- a/src/main/java/edu/kit/typicalc/model/Tree.java +++ b/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. diff --git a/src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java b/src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java index 0118a87..87878fd 100644 --- a/src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java +++ b/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; /** diff --git a/src/main/java/edu/kit/typicalc/model/TypeInferer.java b/src/main/java/edu/kit/typicalc/model/TypeInferer.java index 1e41602..67de596 100644 --- a/src/main/java/edu/kit/typicalc/model/TypeInferer.java +++ b/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 diff --git a/src/main/java/edu/kit/typicalc/model/TypeInfererInterface.java b/src/main/java/edu/kit/typicalc/model/TypeInfererInterface.java index ab83d2c..2f78826 100644 --- a/src/main/java/edu/kit/typicalc/model/TypeInfererInterface.java +++ b/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; diff --git a/src/main/java/edu/kit/typicalc/model/TypeInfererLet.java b/src/main/java/edu/kit/typicalc/model/TypeInfererLet.java index 23eb32e..eb359be 100644 --- a/src/main/java/edu/kit/typicalc/model/TypeInfererLet.java +++ b/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. diff --git a/src/main/java/edu/kit/typicalc/model/TypeVariableFactory.java b/src/main/java/edu/kit/typicalc/model/TypeVariableFactory.java index 1f746a6..3a9669e 100644 --- a/src/main/java/edu/kit/typicalc/model/TypeVariableFactory.java +++ b/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. */ diff --git a/src/main/java/edu/kit/typicalc/model/UnificationStep.java b/src/main/java/edu/kit/typicalc/model/UnificationStep.java new file mode 100644 index 0000000..f2b40be --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/UnificationStep.java @@ -0,0 +1,4 @@ +package edu.kit.typicalc.model; + +public class UnificationStep { +} diff --git a/src/main/java/edu/kit/typicalc/model/parser/LambdaLexer.java b/src/main/java/edu/kit/typicalc/model/parser/LambdaLexer.java new file mode 100644 index 0000000..252c167 --- /dev/null +++ b/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 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); + } + } + } +} \ No newline at end of file diff --git a/src/main/java/edu/kit/typicalc/model/parser/LambdaParser.java b/src/main/java/edu/kit/typicalc/model/parser/LambdaParser.java new file mode 100644 index 0000000..2625ec9 --- /dev/null +++ b/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 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 nextToken() { + Result 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 parse() { + Result 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 parseTerm() { + switch (token.getType()) { + case LAMBDA: + Result abs = parseAbstraction(); + return new Result<>(abs.unwrap(), abs.unwrapError()); + case LET: + Result let = parseLet(); + return new Result<>(let.unwrap(), let.unwrapError()); + default: + return parseApplication(); + } + } + + private Result parseAbstraction() { + nextToken(); + Result var = parseVar(); + if (!expect(TokenType.DOT)) { + // TODO + } + Result 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 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 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 parseAtom() { + switch (token.getType()) { + case VARIABLE: + Result 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 term = parseTerm(); + expect(TokenType.RP); + return term; + } + } + + private Result parseVar() { + String s = token.getText(); + if (!expect(TokenType.VARIABLE)) { + return new Result<>(null, ParseError.UNEXPECTED_TOKEN); + } + return new Result<>(new VarTerm(s)); + } +} diff --git a/src/main/java/edu/kit/typicalc/model/parser/ParseError.java b/src/main/java/edu/kit/typicalc/model/parser/ParseError.java new file mode 100644 index 0000000..bd75ef0 --- /dev/null +++ b/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 +} diff --git a/src/main/java/edu/kit/typicalc/model/parser/Token.java b/src/main/java/edu/kit/typicalc/model/parser/Token.java new file mode 100644 index 0000000..3394e28 --- /dev/null +++ b/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 + "\")"; + } +} diff --git a/src/main/java/edu/kit/typicalc/model/step/InferenceStep.java b/src/main/java/edu/kit/typicalc/model/step/InferenceStep.java index 02cddd7..c167a26 100644 --- a/src/main/java/edu/kit/typicalc/model/step/InferenceStep.java +++ b/src/main/java/edu/kit/typicalc/model/step/InferenceStep.java @@ -15,7 +15,4 @@ public abstract class InferenceStep { */ public abstract void accept(StepVisitor stepVisitor); -} - - - +} \ No newline at end of file diff --git a/src/main/java/edu/kit/typicalc/model/term/AbsTerm.java b/src/main/java/edu/kit/typicalc/model/term/AbsTerm.java new file mode 100644 index 0000000..d14aa44 --- /dev/null +++ b/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 + } +} diff --git a/src/main/java/edu/kit/typicalc/model/term/AppTerm.java b/src/main/java/edu/kit/typicalc/model/term/AppTerm.java new file mode 100644 index 0000000..62fe32c --- /dev/null +++ b/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) { + } +} diff --git a/src/main/java/edu/kit/typicalc/model/term/BooleanTerm.java b/src/main/java/edu/kit/typicalc/model/term/BooleanTerm.java new file mode 100644 index 0000000..358a722 --- /dev/null +++ b/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 + } +} diff --git a/src/main/java/edu/kit/typicalc/model/term/ConstTerm.java b/src/main/java/edu/kit/typicalc/model/term/ConstTerm.java new file mode 100644 index 0000000..694f82f --- /dev/null +++ b/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 { +} diff --git a/src/main/java/edu/kit/typicalc/model/term/IntegerTerm.java b/src/main/java/edu/kit/typicalc/model/term/IntegerTerm.java new file mode 100644 index 0000000..5cb35f8 --- /dev/null +++ b/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 + } +} diff --git a/src/main/java/edu/kit/typicalc/model/term/LambdaTerm.java b/src/main/java/edu/kit/typicalc/model/term/LambdaTerm.java new file mode 100644 index 0000000..6945106 --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/term/LambdaTerm.java @@ -0,0 +1,4 @@ +package edu.kit.typicalc.model.term; + +public class LambdaTerm { +} diff --git a/src/main/java/edu/kit/typicalc/model/term/LetTerm.java b/src/main/java/edu/kit/typicalc/model/term/LetTerm.java new file mode 100644 index 0000000..ad70177 --- /dev/null +++ b/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) { + } +} diff --git a/src/main/java/edu/kit/typicalc/model/term/TermVisitor.java b/src/main/java/edu/kit/typicalc/model/term/TermVisitor.java new file mode 100644 index 0000000..c35bec0 --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/term/TermVisitor.java @@ -0,0 +1,4 @@ +package edu.kit.typicalc.model.term; + +public interface TermVisitor { +} diff --git a/src/main/java/edu/kit/typicalc/model/term/VarTerm.java b/src/main/java/edu/kit/typicalc/model/term/VarTerm.java new file mode 100644 index 0000000..f2254bf --- /dev/null +++ b/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(); + } +} diff --git a/src/main/java/edu/kit/typicalc/model/type/Type.java b/src/main/java/edu/kit/typicalc/model/type/Type.java new file mode 100644 index 0000000..f321ac8 --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/type/Type.java @@ -0,0 +1,4 @@ +package edu.kit.typicalc.model.type; + +public abstract class Type { +} diff --git a/src/main/java/edu/kit/typicalc/model/type/TypeAbstraction.java b/src/main/java/edu/kit/typicalc/model/type/TypeAbstraction.java new file mode 100644 index 0000000..681f18c --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/type/TypeAbstraction.java @@ -0,0 +1,4 @@ +package edu.kit.typicalc.model.type; + +public class TypeAbstraction { +} diff --git a/src/main/java/edu/kit/typicalc/model/type/TypeVariable.java b/src/main/java/edu/kit/typicalc/model/type/TypeVariable.java new file mode 100644 index 0000000..3c394fe --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/type/TypeVariable.java @@ -0,0 +1,4 @@ +package edu.kit.typicalc.model.type; + +public class TypeVariable { +} diff --git a/src/main/java/edu/kit/typicalc/util/Result.java b/src/main/java/edu/kit/typicalc/util/Result.java new file mode 100644 index 0000000..8cc01c1 --- /dev/null +++ b/src/main/java/edu/kit/typicalc/util/Result.java @@ -0,0 +1,28 @@ +package edu.kit.typicalc.util; + +public class Result { + 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; + } +}